gaussian_irreducible_iff_prime

Exact expanded first-order arithmetic statement

forall p. ((((exists ge_real_positive_iff_irreducible_firstcarrier ge_real_negative_iff_irreducible_firstcarrier ge_imaginary_positive_iff_irreducible_firstcarrier ge_imaginary_negative_iff_irreducible_firstcarrier. (exists ge_real_code_iff_irreducible_firstcarrierdecode ge_imaginary_code_iff_irreducible_firstcarrierdecode. (((p) = ((ge_real_code_iff_irreducible_firstcarrierdecode) + (ge_imaginary_code_iff_irreducible_firstcarrierdecode)) * S ((ge_real_code_iff_irreducible_firstcarrierdecode) + (ge_imaginary_code_iff_irreducible_firstcarrierdecode)) + ((ge_imaginary_code_iff_irreducible_firstcarrierdecode) + (ge_imaginary_code_iff_irreducible_firstcarrierdecode))) /\ (((((ge_real_code_iff_irreducible_firstcarrierdecode) = 2 * (ge_real_positive_iff_irreducible_firstcarrier) /\ (ge_real_negative_iff_irreducible_firstcarrier) = 0) \/ exists ge_signed_half_ge_iff_irreducible_firstcarrierdecode_real. (((ge_real_code_iff_irreducible_firstcarrierdecode) = 2 * ge_signed_half_ge_iff_irreducible_firstcarrierdecode_real + 1 /\ (ge_real_positive_iff_irreducible_firstcarrier) = 0) /\ (ge_real_negative_iff_irreducible_firstcarrier) = S ge_signed_half_ge_iff_irreducible_firstcarrierdecode_real))) /\ ((((ge_imaginary_code_iff_irreducible_firstcarrierdecode) = 2 * (ge_imaginary_positive_iff_irreducible_firstcarrier) /\ (ge_imaginary_negative_iff_irreducible_firstcarrier) = 0) \/ exists ge_signed_half_ge_iff_irreducible_firstcarrierdecode_imaginary. (((ge_imaginary_code_iff_irreducible_firstcarrierdecode) = 2 * ge_signed_half_ge_iff_irreducible_firstcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_iff_irreducible_firstcarrier) = 0) /\ (ge_imaginary_negative_iff_irreducible_firstcarrier) = S ge_signed_half_ge_iff_irreducible_firstcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_iff_irreducible_firstnonunit. (exists ge_first_rp_iff_irreducible_firstnonunitidentity ge_first_rn_iff_irreducible_firstnonunitidentity ge_first_ip_iff_irreducible_firstnonunitidentity ge_first_in_iff_irreducible_firstnonunitidentity ge_second_rp_iff_irreducible_firstnonunitidentity ge_second_rn_iff_irreducible_firstnonunitidentity ge_second_ip_iff_irreducible_firstnonunitidentity ge_second_in_iff_irreducible_firstnonunitidentity. ((exists ge_representation_real_code_iff_irreducible_firstnonunitidentityfirst ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityfirst. (((p) = ((ge_representation_real_code_iff_irreducible_firstnonunitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityfirst)) * S ((ge_representation_real_code_iff_irreducible_firstnonunitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityfirst)) + ((ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityfirst))) /\ ((exists ge_balance_positive_iff_irreducible_firstnonunitidentityfirstreal ge_balance_negative_iff_irreducible_firstnonunitidentityfirstreal. (((((ge_representation_real_code_iff_irreducible_firstnonunitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_firstnonunitidentityfirstreal) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstnonunitidentityfirstrealdecode. (((ge_representation_real_code_iff_irreducible_firstnonunitidentityfirst) = 2 * ge_signed_half_iff_irreducible_firstnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentityfirstreal) = S ge_signed_half_iff_irreducible_firstnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_iff_irreducible_firstnonunitidentity) + ge_balance_negative_iff_irreducible_firstnonunitidentityfirstreal = (ge_first_rn_iff_irreducible_firstnonunitidentity) + ge_balance_positive_iff_irreducible_firstnonunitidentityfirstreal))) /\ (exists ge_balance_positive_iff_irreducible_firstnonunitidentityfirstimaginary ge_balance_negative_iff_irreducible_firstnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_firstnonunitidentityfirstimaginary) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityfirst) = 2 * ge_signed_half_iff_irreducible_firstnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentityfirstimaginary) = S ge_signed_half_iff_irreducible_firstnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_iff_irreducible_firstnonunitidentity) + ge_balance_negative_iff_irreducible_firstnonunitidentityfirstimaginary = (ge_first_in_iff_irreducible_firstnonunitidentity) + ge_balance_positive_iff_irreducible_firstnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_irreducible_firstnonunitidentitysecond ge_representation_imaginary_code_iff_irreducible_firstnonunitidentitysecond. (((gr_inverse_iff_irreducible_firstnonunit) = ((ge_representation_real_code_iff_irreducible_firstnonunitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_firstnonunitidentitysecond)) * S ((ge_representation_real_code_iff_irreducible_firstnonunitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_firstnonunitidentitysecond)) + ((ge_representation_imaginary_code_iff_irreducible_firstnonunitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_firstnonunitidentitysecond))) /\ ((exists ge_balance_positive_iff_irreducible_firstnonunitidentitysecondreal ge_balance_negative_iff_irreducible_firstnonunitidentitysecondreal. (((((ge_representation_real_code_iff_irreducible_firstnonunitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_firstnonunitidentitysecondreal) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstnonunitidentitysecondrealdecode. (((ge_representation_real_code_iff_irreducible_firstnonunitidentitysecond) = 2 * ge_signed_half_iff_irreducible_firstnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentitysecondreal) = S ge_signed_half_iff_irreducible_firstnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_iff_irreducible_firstnonunitidentity) + ge_balance_negative_iff_irreducible_firstnonunitidentitysecondreal = (ge_second_rn_iff_irreducible_firstnonunitidentity) + ge_balance_positive_iff_irreducible_firstnonunitidentitysecondreal))) /\ (exists ge_balance_positive_iff_irreducible_firstnonunitidentitysecondimaginary ge_balance_negative_iff_irreducible_firstnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstnonunitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_firstnonunitidentitysecondimaginary) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstnonunitidentitysecond) = 2 * ge_signed_half_iff_irreducible_firstnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentitysecondimaginary) = S ge_signed_half_iff_irreducible_firstnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_iff_irreducible_firstnonunitidentity) + ge_balance_negative_iff_irreducible_firstnonunitidentitysecondimaginary = (ge_second_in_iff_irreducible_firstnonunitidentity) + ge_balance_positive_iff_irreducible_firstnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_iff_irreducible_firstnonunitidentityoutput ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityoutput. (((6) = ((ge_representation_real_code_iff_irreducible_firstnonunitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityoutput)) * S ((ge_representation_real_code_iff_irreducible_firstnonunitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityoutput)) + ((ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityoutput))) /\ ((exists ge_balance_positive_iff_irreducible_firstnonunitidentityoutputreal ge_balance_negative_iff_irreducible_firstnonunitidentityoutputreal. (((((ge_representation_real_code_iff_irreducible_firstnonunitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_firstnonunitidentityoutputreal) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstnonunitidentityoutputrealdecode. (((ge_representation_real_code_iff_irreducible_firstnonunitidentityoutput) = 2 * ge_signed_half_iff_irreducible_firstnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentityoutputreal) = S ge_signed_half_iff_irreducible_firstnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_iff_irreducible_firstnonunitidentity) * (ge_second_rp_iff_irreducible_firstnonunitidentity))) + (((ge_first_rn_iff_irreducible_firstnonunitidentity) * (ge_second_rn_iff_irreducible_firstnonunitidentity))))) + (((((ge_first_ip_iff_irreducible_firstnonunitidentity) * (ge_second_in_iff_irreducible_firstnonunitidentity))) + (((ge_first_in_iff_irreducible_firstnonunitidentity) * (ge_second_ip_iff_irreducible_firstnonunitidentity))))))) + ge_balance_negative_iff_irreducible_firstnonunitidentityoutputreal = (((((((ge_first_rp_iff_irreducible_firstnonunitidentity) * (ge_second_rn_iff_irreducible_firstnonunitidentity))) + (((ge_first_rn_iff_irreducible_firstnonunitidentity) * (ge_second_rp_iff_irreducible_firstnonunitidentity))))) + (((((ge_first_ip_iff_irreducible_firstnonunitidentity) * (ge_second_ip_iff_irreducible_firstnonunitidentity))) + (((ge_first_in_iff_irreducible_firstnonunitidentity) * (ge_second_in_iff_irreducible_firstnonunitidentity))))))) + ge_balance_positive_iff_irreducible_firstnonunitidentityoutputreal))) /\ (exists ge_balance_positive_iff_irreducible_firstnonunitidentityoutputimaginary ge_balance_negative_iff_irreducible_firstnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_firstnonunitidentityoutputimaginary) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstnonunitidentityoutput) = 2 * ge_signed_half_iff_irreducible_firstnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstnonunitidentityoutputimaginary) = S ge_signed_half_iff_irreducible_firstnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_irreducible_firstnonunitidentity) * (ge_second_ip_iff_irreducible_firstnonunitidentity))) + (((ge_first_rn_iff_irreducible_firstnonunitidentity) * (ge_second_in_iff_irreducible_firstnonunitidentity))))) + (((((ge_first_ip_iff_irreducible_firstnonunitidentity) * (ge_second_rp_iff_irreducible_firstnonunitidentity))) + (((ge_first_in_iff_irreducible_firstnonunitidentity) * (ge_second_rn_iff_irreducible_firstnonunitidentity))))))) + ge_balance_negative_iff_irreducible_firstnonunitidentityoutputimaginary = (((((((ge_first_rp_iff_irreducible_firstnonunitidentity) * (ge_second_in_iff_irreducible_firstnonunitidentity))) + (((ge_first_rn_iff_irreducible_firstnonunitidentity) * (ge_second_ip_iff_irreducible_firstnonunitidentity))))) + (((((ge_first_ip_iff_irreducible_firstnonunitidentity) * (ge_second_rn_iff_irreducible_firstnonunitidentity))) + (((ge_first_in_iff_irreducible_firstnonunitidentity) * (ge_second_rp_iff_irreducible_firstnonunitidentity))))))) + ge_balance_positive_iff_irreducible_firstnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_iff_irreducible_first gr_second_factor_iff_irreducible_first. (exists ge_first_rp_iff_irreducible_firstfactorization ge_first_rn_iff_irreducible_firstfactorization ge_first_ip_iff_irreducible_firstfactorization ge_first_in_iff_irreducible_firstfactorization ge_second_rp_iff_irreducible_firstfactorization ge_second_rn_iff_irreducible_firstfactorization ge_second_ip_iff_irreducible_firstfactorization ge_second_in_iff_irreducible_firstfactorization. ((exists ge_representation_real_code_iff_irreducible_firstfactorizationfirst ge_representation_imaginary_code_iff_irreducible_firstfactorizationfirst. (((gr_first_factor_iff_irreducible_first) = ((ge_representation_real_code_iff_irreducible_firstfactorizationfirst) + (ge_representation_imaginary_code_iff_irreducible_firstfactorizationfirst)) * S ((ge_representation_real_code_iff_irreducible_firstfactorizationfirst) + (ge_representation_imaginary_code_iff_irreducible_firstfactorizationfirst)) + ((ge_representation_imaginary_code_iff_irreducible_firstfactorizationfirst) + (ge_representation_imaginary_code_iff_irreducible_firstfactorizationfirst))) /\ ((exists ge_balance_positive_iff_irreducible_firstfactorizationfirstreal ge_balance_negative_iff_irreducible_firstfactorizationfirstreal. (((((ge_representation_real_code_iff_irreducible_firstfactorizationfirst) = 2 * (ge_balance_positive_iff_irreducible_firstfactorizationfirstreal) /\ (ge_balance_negative_iff_irreducible_firstfactorizationfirstreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstfactorizationfirstrealdecode. (((ge_representation_real_code_iff_irreducible_firstfactorizationfirst) = 2 * ge_signed_half_iff_irreducible_firstfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfactorizationfirstreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstfactorizationfirstreal) = S ge_signed_half_iff_irreducible_firstfactorizationfirstrealdecode))) /\ ((ge_first_rp_iff_irreducible_firstfactorization) + ge_balance_negative_iff_irreducible_firstfactorizationfirstreal = (ge_first_rn_iff_irreducible_firstfactorization) + ge_balance_positive_iff_irreducible_firstfactorizationfirstreal))) /\ (exists ge_balance_positive_iff_irreducible_firstfactorizationfirstimaginary ge_balance_negative_iff_irreducible_firstfactorizationfirstimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstfactorizationfirst) = 2 * (ge_balance_positive_iff_irreducible_firstfactorizationfirstimaginary) /\ (ge_balance_negative_iff_irreducible_firstfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstfactorizationfirst) = 2 * ge_signed_half_iff_irreducible_firstfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstfactorizationfirstimaginary) = S ge_signed_half_iff_irreducible_firstfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_iff_irreducible_firstfactorization) + ge_balance_negative_iff_irreducible_firstfactorizationfirstimaginary = (ge_first_in_iff_irreducible_firstfactorization) + ge_balance_positive_iff_irreducible_firstfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_irreducible_firstfactorizationsecond ge_representation_imaginary_code_iff_irreducible_firstfactorizationsecond. (((gr_second_factor_iff_irreducible_first) = ((ge_representation_real_code_iff_irreducible_firstfactorizationsecond) + (ge_representation_imaginary_code_iff_irreducible_firstfactorizationsecond)) * S ((ge_representation_real_code_iff_irreducible_firstfactorizationsecond) + (ge_representation_imaginary_code_iff_irreducible_firstfactorizationsecond)) + ((ge_representation_imaginary_code_iff_irreducible_firstfactorizationsecond) + (ge_representation_imaginary_code_iff_irreducible_firstfactorizationsecond))) /\ ((exists ge_balance_positive_iff_irreducible_firstfactorizationsecondreal ge_balance_negative_iff_irreducible_firstfactorizationsecondreal. (((((ge_representation_real_code_iff_irreducible_firstfactorizationsecond) = 2 * (ge_balance_positive_iff_irreducible_firstfactorizationsecondreal) /\ (ge_balance_negative_iff_irreducible_firstfactorizationsecondreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstfactorizationsecondrealdecode. (((ge_representation_real_code_iff_irreducible_firstfactorizationsecond) = 2 * ge_signed_half_iff_irreducible_firstfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfactorizationsecondreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstfactorizationsecondreal) = S ge_signed_half_iff_irreducible_firstfactorizationsecondrealdecode))) /\ ((ge_second_rp_iff_irreducible_firstfactorization) + ge_balance_negative_iff_irreducible_firstfactorizationsecondreal = (ge_second_rn_iff_irreducible_firstfactorization) + ge_balance_positive_iff_irreducible_firstfactorizationsecondreal))) /\ (exists ge_balance_positive_iff_irreducible_firstfactorizationsecondimaginary ge_balance_negative_iff_irreducible_firstfactorizationsecondimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstfactorizationsecond) = 2 * (ge_balance_positive_iff_irreducible_firstfactorizationsecondimaginary) /\ (ge_balance_negative_iff_irreducible_firstfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstfactorizationsecond) = 2 * ge_signed_half_iff_irreducible_firstfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstfactorizationsecondimaginary) = S ge_signed_half_iff_irreducible_firstfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_iff_irreducible_firstfactorization) + ge_balance_negative_iff_irreducible_firstfactorizationsecondimaginary = (ge_second_in_iff_irreducible_firstfactorization) + ge_balance_positive_iff_irreducible_firstfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_irreducible_firstfactorizationoutput ge_representation_imaginary_code_iff_irreducible_firstfactorizationoutput. (((p) = ((ge_representation_real_code_iff_irreducible_firstfactorizationoutput) + (ge_representation_imaginary_code_iff_irreducible_firstfactorizationoutput)) * S ((ge_representation_real_code_iff_irreducible_firstfactorizationoutput) + (ge_representation_imaginary_code_iff_irreducible_firstfactorizationoutput)) + ((ge_representation_imaginary_code_iff_irreducible_firstfactorizationoutput) + (ge_representation_imaginary_code_iff_irreducible_firstfactorizationoutput))) /\ ((exists ge_balance_positive_iff_irreducible_firstfactorizationoutputreal ge_balance_negative_iff_irreducible_firstfactorizationoutputreal. (((((ge_representation_real_code_iff_irreducible_firstfactorizationoutput) = 2 * (ge_balance_positive_iff_irreducible_firstfactorizationoutputreal) /\ (ge_balance_negative_iff_irreducible_firstfactorizationoutputreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstfactorizationoutputrealdecode. (((ge_representation_real_code_iff_irreducible_firstfactorizationoutput) = 2 * ge_signed_half_iff_irreducible_firstfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfactorizationoutputreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstfactorizationoutputreal) = S ge_signed_half_iff_irreducible_firstfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_iff_irreducible_firstfactorization) * (ge_second_rp_iff_irreducible_firstfactorization))) + (((ge_first_rn_iff_irreducible_firstfactorization) * (ge_second_rn_iff_irreducible_firstfactorization))))) + (((((ge_first_ip_iff_irreducible_firstfactorization) * (ge_second_in_iff_irreducible_firstfactorization))) + (((ge_first_in_iff_irreducible_firstfactorization) * (ge_second_ip_iff_irreducible_firstfactorization))))))) + ge_balance_negative_iff_irreducible_firstfactorizationoutputreal = (((((((ge_first_rp_iff_irreducible_firstfactorization) * (ge_second_rn_iff_irreducible_firstfactorization))) + (((ge_first_rn_iff_irreducible_firstfactorization) * (ge_second_rp_iff_irreducible_firstfactorization))))) + (((((ge_first_ip_iff_irreducible_firstfactorization) * (ge_second_ip_iff_irreducible_firstfactorization))) + (((ge_first_in_iff_irreducible_firstfactorization) * (ge_second_in_iff_irreducible_firstfactorization))))))) + ge_balance_positive_iff_irreducible_firstfactorizationoutputreal))) /\ (exists ge_balance_positive_iff_irreducible_firstfactorizationoutputimaginary ge_balance_negative_iff_irreducible_firstfactorizationoutputimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstfactorizationoutput) = 2 * (ge_balance_positive_iff_irreducible_firstfactorizationoutputimaginary) /\ (ge_balance_negative_iff_irreducible_firstfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstfactorizationoutput) = 2 * ge_signed_half_iff_irreducible_firstfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstfactorizationoutputimaginary) = S ge_signed_half_iff_irreducible_firstfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_irreducible_firstfactorization) * (ge_second_ip_iff_irreducible_firstfactorization))) + (((ge_first_rn_iff_irreducible_firstfactorization) * (ge_second_in_iff_irreducible_firstfactorization))))) + (((((ge_first_ip_iff_irreducible_firstfactorization) * (ge_second_rp_iff_irreducible_firstfactorization))) + (((ge_first_in_iff_irreducible_firstfactorization) * (ge_second_rn_iff_irreducible_firstfactorization))))))) + ge_balance_negative_iff_irreducible_firstfactorizationoutputimaginary = (((((((ge_first_rp_iff_irreducible_firstfactorization) * (ge_second_in_iff_irreducible_firstfactorization))) + (((ge_first_rn_iff_irreducible_firstfactorization) * (ge_second_ip_iff_irreducible_firstfactorization))))) + (((((ge_first_ip_iff_irreducible_firstfactorization) * (ge_second_rn_iff_irreducible_firstfactorization))) + (((ge_first_in_iff_irreducible_firstfactorization) * (ge_second_rp_iff_irreducible_firstfactorization))))))) + ge_balance_positive_iff_irreducible_firstfactorizationoutputimaginary))))))))) -> (exists gr_inverse_iff_irreducible_firstfirst_unit. (exists ge_first_rp_iff_irreducible_firstfirst_unitidentity ge_first_rn_iff_irreducible_firstfirst_unitidentity ge_first_ip_iff_irreducible_firstfirst_unitidentity ge_first_in_iff_irreducible_firstfirst_unitidentity ge_second_rp_iff_irreducible_firstfirst_unitidentity ge_second_rn_iff_irreducible_firstfirst_unitidentity ge_second_ip_iff_irreducible_firstfirst_unitidentity ge_second_in_iff_irreducible_firstfirst_unitidentity. ((exists ge_representation_real_code_iff_irreducible_firstfirst_unitidentityfirst ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityfirst. (((gr_first_factor_iff_irreducible_first) = ((ge_representation_real_code_iff_irreducible_firstfirst_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityfirst)) * S ((ge_representation_real_code_iff_irreducible_firstfirst_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_iff_irreducible_firstfirst_unitidentityfirstreal ge_balance_negative_iff_irreducible_firstfirst_unitidentityfirstreal. (((((ge_representation_real_code_iff_irreducible_firstfirst_unitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_firstfirst_unitidentityfirstreal) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_iff_irreducible_firstfirst_unitidentityfirst) = 2 * ge_signed_half_iff_irreducible_firstfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentityfirstreal) = S ge_signed_half_iff_irreducible_firstfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_iff_irreducible_firstfirst_unitidentity) + ge_balance_negative_iff_irreducible_firstfirst_unitidentityfirstreal = (ge_first_rn_iff_irreducible_firstfirst_unitidentity) + ge_balance_positive_iff_irreducible_firstfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_iff_irreducible_firstfirst_unitidentityfirstimaginary ge_balance_negative_iff_irreducible_firstfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_firstfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityfirst) = 2 * ge_signed_half_iff_irreducible_firstfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentityfirstimaginary) = S ge_signed_half_iff_irreducible_firstfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_iff_irreducible_firstfirst_unitidentity) + ge_balance_negative_iff_irreducible_firstfirst_unitidentityfirstimaginary = (ge_first_in_iff_irreducible_firstfirst_unitidentity) + ge_balance_positive_iff_irreducible_firstfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_irreducible_firstfirst_unitidentitysecond ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentitysecond. (((gr_inverse_iff_irreducible_firstfirst_unit) = ((ge_representation_real_code_iff_irreducible_firstfirst_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentitysecond)) * S ((ge_representation_real_code_iff_irreducible_firstfirst_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_iff_irreducible_firstfirst_unitidentitysecondreal ge_balance_negative_iff_irreducible_firstfirst_unitidentitysecondreal. (((((ge_representation_real_code_iff_irreducible_firstfirst_unitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_firstfirst_unitidentitysecondreal) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_iff_irreducible_firstfirst_unitidentitysecond) = 2 * ge_signed_half_iff_irreducible_firstfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentitysecondreal) = S ge_signed_half_iff_irreducible_firstfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_iff_irreducible_firstfirst_unitidentity) + ge_balance_negative_iff_irreducible_firstfirst_unitidentitysecondreal = (ge_second_rn_iff_irreducible_firstfirst_unitidentity) + ge_balance_positive_iff_irreducible_firstfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_iff_irreducible_firstfirst_unitidentitysecondimaginary ge_balance_negative_iff_irreducible_firstfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_firstfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentitysecond) = 2 * ge_signed_half_iff_irreducible_firstfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentitysecondimaginary) = S ge_signed_half_iff_irreducible_firstfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_iff_irreducible_firstfirst_unitidentity) + ge_balance_negative_iff_irreducible_firstfirst_unitidentitysecondimaginary = (ge_second_in_iff_irreducible_firstfirst_unitidentity) + ge_balance_positive_iff_irreducible_firstfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_iff_irreducible_firstfirst_unitidentityoutput ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_iff_irreducible_firstfirst_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityoutput)) * S ((ge_representation_real_code_iff_irreducible_firstfirst_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_iff_irreducible_firstfirst_unitidentityoutputreal ge_balance_negative_iff_irreducible_firstfirst_unitidentityoutputreal. (((((ge_representation_real_code_iff_irreducible_firstfirst_unitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_firstfirst_unitidentityoutputreal) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_iff_irreducible_firstfirst_unitidentityoutput) = 2 * ge_signed_half_iff_irreducible_firstfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentityoutputreal) = S ge_signed_half_iff_irreducible_firstfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_iff_irreducible_firstfirst_unitidentity) * (ge_second_rp_iff_irreducible_firstfirst_unitidentity))) + (((ge_first_rn_iff_irreducible_firstfirst_unitidentity) * (ge_second_rn_iff_irreducible_firstfirst_unitidentity))))) + (((((ge_first_ip_iff_irreducible_firstfirst_unitidentity) * (ge_second_in_iff_irreducible_firstfirst_unitidentity))) + (((ge_first_in_iff_irreducible_firstfirst_unitidentity) * (ge_second_ip_iff_irreducible_firstfirst_unitidentity))))))) + ge_balance_negative_iff_irreducible_firstfirst_unitidentityoutputreal = (((((((ge_first_rp_iff_irreducible_firstfirst_unitidentity) * (ge_second_rn_iff_irreducible_firstfirst_unitidentity))) + (((ge_first_rn_iff_irreducible_firstfirst_unitidentity) * (ge_second_rp_iff_irreducible_firstfirst_unitidentity))))) + (((((ge_first_ip_iff_irreducible_firstfirst_unitidentity) * (ge_second_ip_iff_irreducible_firstfirst_unitidentity))) + (((ge_first_in_iff_irreducible_firstfirst_unitidentity) * (ge_second_in_iff_irreducible_firstfirst_unitidentity))))))) + ge_balance_positive_iff_irreducible_firstfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_iff_irreducible_firstfirst_unitidentityoutputimaginary ge_balance_negative_iff_irreducible_firstfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_firstfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstfirst_unitidentityoutput) = 2 * ge_signed_half_iff_irreducible_firstfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstfirst_unitidentityoutputimaginary) = S ge_signed_half_iff_irreducible_firstfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_irreducible_firstfirst_unitidentity) * (ge_second_ip_iff_irreducible_firstfirst_unitidentity))) + (((ge_first_rn_iff_irreducible_firstfirst_unitidentity) * (ge_second_in_iff_irreducible_firstfirst_unitidentity))))) + (((((ge_first_ip_iff_irreducible_firstfirst_unitidentity) * (ge_second_rp_iff_irreducible_firstfirst_unitidentity))) + (((ge_first_in_iff_irreducible_firstfirst_unitidentity) * (ge_second_rn_iff_irreducible_firstfirst_unitidentity))))))) + ge_balance_negative_iff_irreducible_firstfirst_unitidentityoutputimaginary = (((((((ge_first_rp_iff_irreducible_firstfirst_unitidentity) * (ge_second_in_iff_irreducible_firstfirst_unitidentity))) + (((ge_first_rn_iff_irreducible_firstfirst_unitidentity) * (ge_second_ip_iff_irreducible_firstfirst_unitidentity))))) + (((((ge_first_ip_iff_irreducible_firstfirst_unitidentity) * (ge_second_rn_iff_irreducible_firstfirst_unitidentity))) + (((ge_first_in_iff_irreducible_firstfirst_unitidentity) * (ge_second_rp_iff_irreducible_firstfirst_unitidentity))))))) + ge_balance_positive_iff_irreducible_firstfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_iff_irreducible_firstsecond_unit. (exists ge_first_rp_iff_irreducible_firstsecond_unitidentity ge_first_rn_iff_irreducible_firstsecond_unitidentity ge_first_ip_iff_irreducible_firstsecond_unitidentity ge_first_in_iff_irreducible_firstsecond_unitidentity ge_second_rp_iff_irreducible_firstsecond_unitidentity ge_second_rn_iff_irreducible_firstsecond_unitidentity ge_second_ip_iff_irreducible_firstsecond_unitidentity ge_second_in_iff_irreducible_firstsecond_unitidentity. ((exists ge_representation_real_code_iff_irreducible_firstsecond_unitidentityfirst ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityfirst. (((gr_second_factor_iff_irreducible_first) = ((ge_representation_real_code_iff_irreducible_firstsecond_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityfirst)) * S ((ge_representation_real_code_iff_irreducible_firstsecond_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_iff_irreducible_firstsecond_unitidentityfirstreal ge_balance_negative_iff_irreducible_firstsecond_unitidentityfirstreal. (((((ge_representation_real_code_iff_irreducible_firstsecond_unitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_firstsecond_unitidentityfirstreal) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_iff_irreducible_firstsecond_unitidentityfirst) = 2 * ge_signed_half_iff_irreducible_firstsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentityfirstreal) = S ge_signed_half_iff_irreducible_firstsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_iff_irreducible_firstsecond_unitidentity) + ge_balance_negative_iff_irreducible_firstsecond_unitidentityfirstreal = (ge_first_rn_iff_irreducible_firstsecond_unitidentity) + ge_balance_positive_iff_irreducible_firstsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_iff_irreducible_firstsecond_unitidentityfirstimaginary ge_balance_negative_iff_irreducible_firstsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_firstsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityfirst) = 2 * ge_signed_half_iff_irreducible_firstsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentityfirstimaginary) = S ge_signed_half_iff_irreducible_firstsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_iff_irreducible_firstsecond_unitidentity) + ge_balance_negative_iff_irreducible_firstsecond_unitidentityfirstimaginary = (ge_first_in_iff_irreducible_firstsecond_unitidentity) + ge_balance_positive_iff_irreducible_firstsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_irreducible_firstsecond_unitidentitysecond ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentitysecond. (((gr_inverse_iff_irreducible_firstsecond_unit) = ((ge_representation_real_code_iff_irreducible_firstsecond_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentitysecond)) * S ((ge_representation_real_code_iff_irreducible_firstsecond_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_iff_irreducible_firstsecond_unitidentitysecondreal ge_balance_negative_iff_irreducible_firstsecond_unitidentitysecondreal. (((((ge_representation_real_code_iff_irreducible_firstsecond_unitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_firstsecond_unitidentitysecondreal) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_iff_irreducible_firstsecond_unitidentitysecond) = 2 * ge_signed_half_iff_irreducible_firstsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentitysecondreal) = S ge_signed_half_iff_irreducible_firstsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_iff_irreducible_firstsecond_unitidentity) + ge_balance_negative_iff_irreducible_firstsecond_unitidentitysecondreal = (ge_second_rn_iff_irreducible_firstsecond_unitidentity) + ge_balance_positive_iff_irreducible_firstsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_iff_irreducible_firstsecond_unitidentitysecondimaginary ge_balance_negative_iff_irreducible_firstsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_firstsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentitysecond) = 2 * ge_signed_half_iff_irreducible_firstsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentitysecondimaginary) = S ge_signed_half_iff_irreducible_firstsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_iff_irreducible_firstsecond_unitidentity) + ge_balance_negative_iff_irreducible_firstsecond_unitidentitysecondimaginary = (ge_second_in_iff_irreducible_firstsecond_unitidentity) + ge_balance_positive_iff_irreducible_firstsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_iff_irreducible_firstsecond_unitidentityoutput ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_iff_irreducible_firstsecond_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityoutput)) * S ((ge_representation_real_code_iff_irreducible_firstsecond_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_iff_irreducible_firstsecond_unitidentityoutputreal ge_balance_negative_iff_irreducible_firstsecond_unitidentityoutputreal. (((((ge_representation_real_code_iff_irreducible_firstsecond_unitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_firstsecond_unitidentityoutputreal) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_iff_irreducible_firstsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_iff_irreducible_firstsecond_unitidentityoutput) = 2 * ge_signed_half_iff_irreducible_firstsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_firstsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentityoutputreal) = S ge_signed_half_iff_irreducible_firstsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_iff_irreducible_firstsecond_unitidentity) * (ge_second_rp_iff_irreducible_firstsecond_unitidentity))) + (((ge_first_rn_iff_irreducible_firstsecond_unitidentity) * (ge_second_rn_iff_irreducible_firstsecond_unitidentity))))) + (((((ge_first_ip_iff_irreducible_firstsecond_unitidentity) * (ge_second_in_iff_irreducible_firstsecond_unitidentity))) + (((ge_first_in_iff_irreducible_firstsecond_unitidentity) * (ge_second_ip_iff_irreducible_firstsecond_unitidentity))))))) + ge_balance_negative_iff_irreducible_firstsecond_unitidentityoutputreal = (((((((ge_first_rp_iff_irreducible_firstsecond_unitidentity) * (ge_second_rn_iff_irreducible_firstsecond_unitidentity))) + (((ge_first_rn_iff_irreducible_firstsecond_unitidentity) * (ge_second_rp_iff_irreducible_firstsecond_unitidentity))))) + (((((ge_first_ip_iff_irreducible_firstsecond_unitidentity) * (ge_second_ip_iff_irreducible_firstsecond_unitidentity))) + (((ge_first_in_iff_irreducible_firstsecond_unitidentity) * (ge_second_in_iff_irreducible_firstsecond_unitidentity))))))) + ge_balance_positive_iff_irreducible_firstsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_iff_irreducible_firstsecond_unitidentityoutputimaginary ge_balance_negative_iff_irreducible_firstsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_firstsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_firstsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_firstsecond_unitidentityoutput) = 2 * ge_signed_half_iff_irreducible_firstsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_firstsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_firstsecond_unitidentityoutputimaginary) = S ge_signed_half_iff_irreducible_firstsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_irreducible_firstsecond_unitidentity) * (ge_second_ip_iff_irreducible_firstsecond_unitidentity))) + (((ge_first_rn_iff_irreducible_firstsecond_unitidentity) * (ge_second_in_iff_irreducible_firstsecond_unitidentity))))) + (((((ge_first_ip_iff_irreducible_firstsecond_unitidentity) * (ge_second_rp_iff_irreducible_firstsecond_unitidentity))) + (((ge_first_in_iff_irreducible_firstsecond_unitidentity) * (ge_second_rn_iff_irreducible_firstsecond_unitidentity))))))) + ge_balance_negative_iff_irreducible_firstsecond_unitidentityoutputimaginary = (((((((ge_first_rp_iff_irreducible_firstsecond_unitidentity) * (ge_second_in_iff_irreducible_firstsecond_unitidentity))) + (((ge_first_rn_iff_irreducible_firstsecond_unitidentity) * (ge_second_ip_iff_irreducible_firstsecond_unitidentity))))) + (((((ge_first_ip_iff_irreducible_firstsecond_unitidentity) * (ge_second_rn_iff_irreducible_firstsecond_unitidentity))) + (((ge_first_in_iff_irreducible_firstsecond_unitidentity) * (ge_second_rp_iff_irreducible_firstsecond_unitidentity))))))) + ge_balance_positive_iff_irreducible_firstsecond_unitidentityoutputimaginary))))))))))))))) -> (((exists ge_real_positive_iff_prime_firstcarrier ge_real_negative_iff_prime_firstcarrier ge_imaginary_positive_iff_prime_firstcarrier ge_imaginary_negative_iff_prime_firstcarrier. (exists ge_real_code_iff_prime_firstcarrierdecode ge_imaginary_code_iff_prime_firstcarrierdecode. (((p) = ((ge_real_code_iff_prime_firstcarrierdecode) + (ge_imaginary_code_iff_prime_firstcarrierdecode)) * S ((ge_real_code_iff_prime_firstcarrierdecode) + (ge_imaginary_code_iff_prime_firstcarrierdecode)) + ((ge_imaginary_code_iff_prime_firstcarrierdecode) + (ge_imaginary_code_iff_prime_firstcarrierdecode))) /\ (((((ge_real_code_iff_prime_firstcarrierdecode) = 2 * (ge_real_positive_iff_prime_firstcarrier) /\ (ge_real_negative_iff_prime_firstcarrier) = 0) \/ exists ge_signed_half_ge_iff_prime_firstcarrierdecode_real. (((ge_real_code_iff_prime_firstcarrierdecode) = 2 * ge_signed_half_ge_iff_prime_firstcarrierdecode_real + 1 /\ (ge_real_positive_iff_prime_firstcarrier) = 0) /\ (ge_real_negative_iff_prime_firstcarrier) = S ge_signed_half_ge_iff_prime_firstcarrierdecode_real))) /\ ((((ge_imaginary_code_iff_prime_firstcarrierdecode) = 2 * (ge_imaginary_positive_iff_prime_firstcarrier) /\ (ge_imaginary_negative_iff_prime_firstcarrier) = 0) \/ exists ge_signed_half_ge_iff_prime_firstcarrierdecode_imaginary. (((ge_imaginary_code_iff_prime_firstcarrierdecode) = 2 * ge_signed_half_ge_iff_prime_firstcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_iff_prime_firstcarrier) = 0) /\ (ge_imaginary_negative_iff_prime_firstcarrier) = S ge_signed_half_ge_iff_prime_firstcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_iff_prime_firstnonunit. (exists ge_first_rp_iff_prime_firstnonunitidentity ge_first_rn_iff_prime_firstnonunitidentity ge_first_ip_iff_prime_firstnonunitidentity ge_first_in_iff_prime_firstnonunitidentity ge_second_rp_iff_prime_firstnonunitidentity ge_second_rn_iff_prime_firstnonunitidentity ge_second_ip_iff_prime_firstnonunitidentity ge_second_in_iff_prime_firstnonunitidentity. ((exists ge_representation_real_code_iff_prime_firstnonunitidentityfirst ge_representation_imaginary_code_iff_prime_firstnonunitidentityfirst. (((p) = ((ge_representation_real_code_iff_prime_firstnonunitidentityfirst) + (ge_representation_imaginary_code_iff_prime_firstnonunitidentityfirst)) * S ((ge_representation_real_code_iff_prime_firstnonunitidentityfirst) + (ge_representation_imaginary_code_iff_prime_firstnonunitidentityfirst)) + ((ge_representation_imaginary_code_iff_prime_firstnonunitidentityfirst) + (ge_representation_imaginary_code_iff_prime_firstnonunitidentityfirst))) /\ ((exists ge_balance_positive_iff_prime_firstnonunitidentityfirstreal ge_balance_negative_iff_prime_firstnonunitidentityfirstreal. (((((ge_representation_real_code_iff_prime_firstnonunitidentityfirst) = 2 * (ge_balance_positive_iff_prime_firstnonunitidentityfirstreal) /\ (ge_balance_negative_iff_prime_firstnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_iff_prime_firstnonunitidentityfirstrealdecode. (((ge_representation_real_code_iff_prime_firstnonunitidentityfirst) = 2 * ge_signed_half_iff_prime_firstnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_iff_prime_firstnonunitidentityfirstreal) = S ge_signed_half_iff_prime_firstnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_iff_prime_firstnonunitidentity) + ge_balance_negative_iff_prime_firstnonunitidentityfirstreal = (ge_first_rn_iff_prime_firstnonunitidentity) + ge_balance_positive_iff_prime_firstnonunitidentityfirstreal))) /\ (exists ge_balance_positive_iff_prime_firstnonunitidentityfirstimaginary ge_balance_negative_iff_prime_firstnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_firstnonunitidentityfirst) = 2 * (ge_balance_positive_iff_prime_firstnonunitidentityfirstimaginary) /\ (ge_balance_negative_iff_prime_firstnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstnonunitidentityfirst) = 2 * ge_signed_half_iff_prime_firstnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstnonunitidentityfirstimaginary) = S ge_signed_half_iff_prime_firstnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_firstnonunitidentity) + ge_balance_negative_iff_prime_firstnonunitidentityfirstimaginary = (ge_first_in_iff_prime_firstnonunitidentity) + ge_balance_positive_iff_prime_firstnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_firstnonunitidentitysecond ge_representation_imaginary_code_iff_prime_firstnonunitidentitysecond. (((gr_inverse_iff_prime_firstnonunit) = ((ge_representation_real_code_iff_prime_firstnonunitidentitysecond) + (ge_representation_imaginary_code_iff_prime_firstnonunitidentitysecond)) * S ((ge_representation_real_code_iff_prime_firstnonunitidentitysecond) + (ge_representation_imaginary_code_iff_prime_firstnonunitidentitysecond)) + ((ge_representation_imaginary_code_iff_prime_firstnonunitidentitysecond) + (ge_representation_imaginary_code_iff_prime_firstnonunitidentitysecond))) /\ ((exists ge_balance_positive_iff_prime_firstnonunitidentitysecondreal ge_balance_negative_iff_prime_firstnonunitidentitysecondreal. (((((ge_representation_real_code_iff_prime_firstnonunitidentitysecond) = 2 * (ge_balance_positive_iff_prime_firstnonunitidentitysecondreal) /\ (ge_balance_negative_iff_prime_firstnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_iff_prime_firstnonunitidentitysecondrealdecode. (((ge_representation_real_code_iff_prime_firstnonunitidentitysecond) = 2 * ge_signed_half_iff_prime_firstnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_iff_prime_firstnonunitidentitysecondreal) = S ge_signed_half_iff_prime_firstnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_iff_prime_firstnonunitidentity) + ge_balance_negative_iff_prime_firstnonunitidentitysecondreal = (ge_second_rn_iff_prime_firstnonunitidentity) + ge_balance_positive_iff_prime_firstnonunitidentitysecondreal))) /\ (exists ge_balance_positive_iff_prime_firstnonunitidentitysecondimaginary ge_balance_negative_iff_prime_firstnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_iff_prime_firstnonunitidentitysecond) = 2 * (ge_balance_positive_iff_prime_firstnonunitidentitysecondimaginary) /\ (ge_balance_negative_iff_prime_firstnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstnonunitidentitysecond) = 2 * ge_signed_half_iff_prime_firstnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstnonunitidentitysecondimaginary) = S ge_signed_half_iff_prime_firstnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_firstnonunitidentity) + ge_balance_negative_iff_prime_firstnonunitidentitysecondimaginary = (ge_second_in_iff_prime_firstnonunitidentity) + ge_balance_positive_iff_prime_firstnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_firstnonunitidentityoutput ge_representation_imaginary_code_iff_prime_firstnonunitidentityoutput. (((6) = ((ge_representation_real_code_iff_prime_firstnonunitidentityoutput) + (ge_representation_imaginary_code_iff_prime_firstnonunitidentityoutput)) * S ((ge_representation_real_code_iff_prime_firstnonunitidentityoutput) + (ge_representation_imaginary_code_iff_prime_firstnonunitidentityoutput)) + ((ge_representation_imaginary_code_iff_prime_firstnonunitidentityoutput) + (ge_representation_imaginary_code_iff_prime_firstnonunitidentityoutput))) /\ ((exists ge_balance_positive_iff_prime_firstnonunitidentityoutputreal ge_balance_negative_iff_prime_firstnonunitidentityoutputreal. (((((ge_representation_real_code_iff_prime_firstnonunitidentityoutput) = 2 * (ge_balance_positive_iff_prime_firstnonunitidentityoutputreal) /\ (ge_balance_negative_iff_prime_firstnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_iff_prime_firstnonunitidentityoutputrealdecode. (((ge_representation_real_code_iff_prime_firstnonunitidentityoutput) = 2 * ge_signed_half_iff_prime_firstnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_iff_prime_firstnonunitidentityoutputreal) = S ge_signed_half_iff_prime_firstnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_firstnonunitidentity) * (ge_second_rp_iff_prime_firstnonunitidentity))) + (((ge_first_rn_iff_prime_firstnonunitidentity) * (ge_second_rn_iff_prime_firstnonunitidentity))))) + (((((ge_first_ip_iff_prime_firstnonunitidentity) * (ge_second_in_iff_prime_firstnonunitidentity))) + (((ge_first_in_iff_prime_firstnonunitidentity) * (ge_second_ip_iff_prime_firstnonunitidentity))))))) + ge_balance_negative_iff_prime_firstnonunitidentityoutputreal = (((((((ge_first_rp_iff_prime_firstnonunitidentity) * (ge_second_rn_iff_prime_firstnonunitidentity))) + (((ge_first_rn_iff_prime_firstnonunitidentity) * (ge_second_rp_iff_prime_firstnonunitidentity))))) + (((((ge_first_ip_iff_prime_firstnonunitidentity) * (ge_second_ip_iff_prime_firstnonunitidentity))) + (((ge_first_in_iff_prime_firstnonunitidentity) * (ge_second_in_iff_prime_firstnonunitidentity))))))) + ge_balance_positive_iff_prime_firstnonunitidentityoutputreal))) /\ (exists ge_balance_positive_iff_prime_firstnonunitidentityoutputimaginary ge_balance_negative_iff_prime_firstnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_firstnonunitidentityoutput) = 2 * (ge_balance_positive_iff_prime_firstnonunitidentityoutputimaginary) /\ (ge_balance_negative_iff_prime_firstnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstnonunitidentityoutput) = 2 * ge_signed_half_iff_prime_firstnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstnonunitidentityoutputimaginary) = S ge_signed_half_iff_prime_firstnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_firstnonunitidentity) * (ge_second_ip_iff_prime_firstnonunitidentity))) + (((ge_first_rn_iff_prime_firstnonunitidentity) * (ge_second_in_iff_prime_firstnonunitidentity))))) + (((((ge_first_ip_iff_prime_firstnonunitidentity) * (ge_second_rp_iff_prime_firstnonunitidentity))) + (((ge_first_in_iff_prime_firstnonunitidentity) * (ge_second_rn_iff_prime_firstnonunitidentity))))))) + ge_balance_negative_iff_prime_firstnonunitidentityoutputimaginary = (((((((ge_first_rp_iff_prime_firstnonunitidentity) * (ge_second_in_iff_prime_firstnonunitidentity))) + (((ge_first_rn_iff_prime_firstnonunitidentity) * (ge_second_ip_iff_prime_firstnonunitidentity))))) + (((((ge_first_ip_iff_prime_firstnonunitidentity) * (ge_second_rn_iff_prime_firstnonunitidentity))) + (((ge_first_in_iff_prime_firstnonunitidentity) * (ge_second_rp_iff_prime_firstnonunitidentity))))))) + ge_balance_positive_iff_prime_firstnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_iff_prime_first gr_second_factor_iff_prime_first gr_product_iff_prime_first. (exists ge_first_rp_iff_prime_firstproduct ge_first_rn_iff_prime_firstproduct ge_first_ip_iff_prime_firstproduct ge_first_in_iff_prime_firstproduct ge_second_rp_iff_prime_firstproduct ge_second_rn_iff_prime_firstproduct ge_second_ip_iff_prime_firstproduct ge_second_in_iff_prime_firstproduct. ((exists ge_representation_real_code_iff_prime_firstproductfirst ge_representation_imaginary_code_iff_prime_firstproductfirst. (((gr_first_factor_iff_prime_first) = ((ge_representation_real_code_iff_prime_firstproductfirst) + (ge_representation_imaginary_code_iff_prime_firstproductfirst)) * S ((ge_representation_real_code_iff_prime_firstproductfirst) + (ge_representation_imaginary_code_iff_prime_firstproductfirst)) + ((ge_representation_imaginary_code_iff_prime_firstproductfirst) + (ge_representation_imaginary_code_iff_prime_firstproductfirst))) /\ ((exists ge_balance_positive_iff_prime_firstproductfirstreal ge_balance_negative_iff_prime_firstproductfirstreal. (((((ge_representation_real_code_iff_prime_firstproductfirst) = 2 * (ge_balance_positive_iff_prime_firstproductfirstreal) /\ (ge_balance_negative_iff_prime_firstproductfirstreal) = 0) \/ exists ge_signed_half_iff_prime_firstproductfirstrealdecode. (((ge_representation_real_code_iff_prime_firstproductfirst) = 2 * ge_signed_half_iff_prime_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstproductfirstreal) = 0) /\ (ge_balance_negative_iff_prime_firstproductfirstreal) = S ge_signed_half_iff_prime_firstproductfirstrealdecode))) /\ ((ge_first_rp_iff_prime_firstproduct) + ge_balance_negative_iff_prime_firstproductfirstreal = (ge_first_rn_iff_prime_firstproduct) + ge_balance_positive_iff_prime_firstproductfirstreal))) /\ (exists ge_balance_positive_iff_prime_firstproductfirstimaginary ge_balance_negative_iff_prime_firstproductfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_firstproductfirst) = 2 * (ge_balance_positive_iff_prime_firstproductfirstimaginary) /\ (ge_balance_negative_iff_prime_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstproductfirst) = 2 * ge_signed_half_iff_prime_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstproductfirstimaginary) = S ge_signed_half_iff_prime_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_firstproduct) + ge_balance_negative_iff_prime_firstproductfirstimaginary = (ge_first_in_iff_prime_firstproduct) + ge_balance_positive_iff_prime_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_firstproductsecond ge_representation_imaginary_code_iff_prime_firstproductsecond. (((gr_second_factor_iff_prime_first) = ((ge_representation_real_code_iff_prime_firstproductsecond) + (ge_representation_imaginary_code_iff_prime_firstproductsecond)) * S ((ge_representation_real_code_iff_prime_firstproductsecond) + (ge_representation_imaginary_code_iff_prime_firstproductsecond)) + ((ge_representation_imaginary_code_iff_prime_firstproductsecond) + (ge_representation_imaginary_code_iff_prime_firstproductsecond))) /\ ((exists ge_balance_positive_iff_prime_firstproductsecondreal ge_balance_negative_iff_prime_firstproductsecondreal. (((((ge_representation_real_code_iff_prime_firstproductsecond) = 2 * (ge_balance_positive_iff_prime_firstproductsecondreal) /\ (ge_balance_negative_iff_prime_firstproductsecondreal) = 0) \/ exists ge_signed_half_iff_prime_firstproductsecondrealdecode. (((ge_representation_real_code_iff_prime_firstproductsecond) = 2 * ge_signed_half_iff_prime_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstproductsecondreal) = 0) /\ (ge_balance_negative_iff_prime_firstproductsecondreal) = S ge_signed_half_iff_prime_firstproductsecondrealdecode))) /\ ((ge_second_rp_iff_prime_firstproduct) + ge_balance_negative_iff_prime_firstproductsecondreal = (ge_second_rn_iff_prime_firstproduct) + ge_balance_positive_iff_prime_firstproductsecondreal))) /\ (exists ge_balance_positive_iff_prime_firstproductsecondimaginary ge_balance_negative_iff_prime_firstproductsecondimaginary. (((((ge_representation_imaginary_code_iff_prime_firstproductsecond) = 2 * (ge_balance_positive_iff_prime_firstproductsecondimaginary) /\ (ge_balance_negative_iff_prime_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstproductsecond) = 2 * ge_signed_half_iff_prime_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstproductsecondimaginary) = S ge_signed_half_iff_prime_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_firstproduct) + ge_balance_negative_iff_prime_firstproductsecondimaginary = (ge_second_in_iff_prime_firstproduct) + ge_balance_positive_iff_prime_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_firstproductoutput ge_representation_imaginary_code_iff_prime_firstproductoutput. (((gr_product_iff_prime_first) = ((ge_representation_real_code_iff_prime_firstproductoutput) + (ge_representation_imaginary_code_iff_prime_firstproductoutput)) * S ((ge_representation_real_code_iff_prime_firstproductoutput) + (ge_representation_imaginary_code_iff_prime_firstproductoutput)) + ((ge_representation_imaginary_code_iff_prime_firstproductoutput) + (ge_representation_imaginary_code_iff_prime_firstproductoutput))) /\ ((exists ge_balance_positive_iff_prime_firstproductoutputreal ge_balance_negative_iff_prime_firstproductoutputreal. (((((ge_representation_real_code_iff_prime_firstproductoutput) = 2 * (ge_balance_positive_iff_prime_firstproductoutputreal) /\ (ge_balance_negative_iff_prime_firstproductoutputreal) = 0) \/ exists ge_signed_half_iff_prime_firstproductoutputrealdecode. (((ge_representation_real_code_iff_prime_firstproductoutput) = 2 * ge_signed_half_iff_prime_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstproductoutputreal) = 0) /\ (ge_balance_negative_iff_prime_firstproductoutputreal) = S ge_signed_half_iff_prime_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_firstproduct) * (ge_second_rp_iff_prime_firstproduct))) + (((ge_first_rn_iff_prime_firstproduct) * (ge_second_rn_iff_prime_firstproduct))))) + (((((ge_first_ip_iff_prime_firstproduct) * (ge_second_in_iff_prime_firstproduct))) + (((ge_first_in_iff_prime_firstproduct) * (ge_second_ip_iff_prime_firstproduct))))))) + ge_balance_negative_iff_prime_firstproductoutputreal = (((((((ge_first_rp_iff_prime_firstproduct) * (ge_second_rn_iff_prime_firstproduct))) + (((ge_first_rn_iff_prime_firstproduct) * (ge_second_rp_iff_prime_firstproduct))))) + (((((ge_first_ip_iff_prime_firstproduct) * (ge_second_ip_iff_prime_firstproduct))) + (((ge_first_in_iff_prime_firstproduct) * (ge_second_in_iff_prime_firstproduct))))))) + ge_balance_positive_iff_prime_firstproductoutputreal))) /\ (exists ge_balance_positive_iff_prime_firstproductoutputimaginary ge_balance_negative_iff_prime_firstproductoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_firstproductoutput) = 2 * (ge_balance_positive_iff_prime_firstproductoutputimaginary) /\ (ge_balance_negative_iff_prime_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstproductoutput) = 2 * ge_signed_half_iff_prime_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstproductoutputimaginary) = S ge_signed_half_iff_prime_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_firstproduct) * (ge_second_ip_iff_prime_firstproduct))) + (((ge_first_rn_iff_prime_firstproduct) * (ge_second_in_iff_prime_firstproduct))))) + (((((ge_first_ip_iff_prime_firstproduct) * (ge_second_rp_iff_prime_firstproduct))) + (((ge_first_in_iff_prime_firstproduct) * (ge_second_rn_iff_prime_firstproduct))))))) + ge_balance_negative_iff_prime_firstproductoutputimaginary = (((((((ge_first_rp_iff_prime_firstproduct) * (ge_second_in_iff_prime_firstproduct))) + (((ge_first_rn_iff_prime_firstproduct) * (ge_second_ip_iff_prime_firstproduct))))) + (((((ge_first_ip_iff_prime_firstproduct) * (ge_second_rn_iff_prime_firstproduct))) + (((ge_first_in_iff_prime_firstproduct) * (ge_second_rp_iff_prime_firstproduct))))))) + ge_balance_positive_iff_prime_firstproductoutputimaginary))))))))) -> (exists gr_quotient_iff_prime_firstdivisor. (exists ge_first_rp_iff_prime_firstdivisorproduct ge_first_rn_iff_prime_firstdivisorproduct ge_first_ip_iff_prime_firstdivisorproduct ge_first_in_iff_prime_firstdivisorproduct ge_second_rp_iff_prime_firstdivisorproduct ge_second_rn_iff_prime_firstdivisorproduct ge_second_ip_iff_prime_firstdivisorproduct ge_second_in_iff_prime_firstdivisorproduct. ((exists ge_representation_real_code_iff_prime_firstdivisorproductfirst ge_representation_imaginary_code_iff_prime_firstdivisorproductfirst. (((p) = ((ge_representation_real_code_iff_prime_firstdivisorproductfirst) + (ge_representation_imaginary_code_iff_prime_firstdivisorproductfirst)) * S ((ge_representation_real_code_iff_prime_firstdivisorproductfirst) + (ge_representation_imaginary_code_iff_prime_firstdivisorproductfirst)) + ((ge_representation_imaginary_code_iff_prime_firstdivisorproductfirst) + (ge_representation_imaginary_code_iff_prime_firstdivisorproductfirst))) /\ ((exists ge_balance_positive_iff_prime_firstdivisorproductfirstreal ge_balance_negative_iff_prime_firstdivisorproductfirstreal. (((((ge_representation_real_code_iff_prime_firstdivisorproductfirst) = 2 * (ge_balance_positive_iff_prime_firstdivisorproductfirstreal) /\ (ge_balance_negative_iff_prime_firstdivisorproductfirstreal) = 0) \/ exists ge_signed_half_iff_prime_firstdivisorproductfirstrealdecode. (((ge_representation_real_code_iff_prime_firstdivisorproductfirst) = 2 * ge_signed_half_iff_prime_firstdivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstdivisorproductfirstreal) = 0) /\ (ge_balance_negative_iff_prime_firstdivisorproductfirstreal) = S ge_signed_half_iff_prime_firstdivisorproductfirstrealdecode))) /\ ((ge_first_rp_iff_prime_firstdivisorproduct) + ge_balance_negative_iff_prime_firstdivisorproductfirstreal = (ge_first_rn_iff_prime_firstdivisorproduct) + ge_balance_positive_iff_prime_firstdivisorproductfirstreal))) /\ (exists ge_balance_positive_iff_prime_firstdivisorproductfirstimaginary ge_balance_negative_iff_prime_firstdivisorproductfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_firstdivisorproductfirst) = 2 * (ge_balance_positive_iff_prime_firstdivisorproductfirstimaginary) /\ (ge_balance_negative_iff_prime_firstdivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstdivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstdivisorproductfirst) = 2 * ge_signed_half_iff_prime_firstdivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstdivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstdivisorproductfirstimaginary) = S ge_signed_half_iff_prime_firstdivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_firstdivisorproduct) + ge_balance_negative_iff_prime_firstdivisorproductfirstimaginary = (ge_first_in_iff_prime_firstdivisorproduct) + ge_balance_positive_iff_prime_firstdivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_firstdivisorproductsecond ge_representation_imaginary_code_iff_prime_firstdivisorproductsecond. (((gr_quotient_iff_prime_firstdivisor) = ((ge_representation_real_code_iff_prime_firstdivisorproductsecond) + (ge_representation_imaginary_code_iff_prime_firstdivisorproductsecond)) * S ((ge_representation_real_code_iff_prime_firstdivisorproductsecond) + (ge_representation_imaginary_code_iff_prime_firstdivisorproductsecond)) + ((ge_representation_imaginary_code_iff_prime_firstdivisorproductsecond) + (ge_representation_imaginary_code_iff_prime_firstdivisorproductsecond))) /\ ((exists ge_balance_positive_iff_prime_firstdivisorproductsecondreal ge_balance_negative_iff_prime_firstdivisorproductsecondreal. (((((ge_representation_real_code_iff_prime_firstdivisorproductsecond) = 2 * (ge_balance_positive_iff_prime_firstdivisorproductsecondreal) /\ (ge_balance_negative_iff_prime_firstdivisorproductsecondreal) = 0) \/ exists ge_signed_half_iff_prime_firstdivisorproductsecondrealdecode. (((ge_representation_real_code_iff_prime_firstdivisorproductsecond) = 2 * ge_signed_half_iff_prime_firstdivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstdivisorproductsecondreal) = 0) /\ (ge_balance_negative_iff_prime_firstdivisorproductsecondreal) = S ge_signed_half_iff_prime_firstdivisorproductsecondrealdecode))) /\ ((ge_second_rp_iff_prime_firstdivisorproduct) + ge_balance_negative_iff_prime_firstdivisorproductsecondreal = (ge_second_rn_iff_prime_firstdivisorproduct) + ge_balance_positive_iff_prime_firstdivisorproductsecondreal))) /\ (exists ge_balance_positive_iff_prime_firstdivisorproductsecondimaginary ge_balance_negative_iff_prime_firstdivisorproductsecondimaginary. (((((ge_representation_imaginary_code_iff_prime_firstdivisorproductsecond) = 2 * (ge_balance_positive_iff_prime_firstdivisorproductsecondimaginary) /\ (ge_balance_negative_iff_prime_firstdivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstdivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstdivisorproductsecond) = 2 * ge_signed_half_iff_prime_firstdivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstdivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstdivisorproductsecondimaginary) = S ge_signed_half_iff_prime_firstdivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_firstdivisorproduct) + ge_balance_negative_iff_prime_firstdivisorproductsecondimaginary = (ge_second_in_iff_prime_firstdivisorproduct) + ge_balance_positive_iff_prime_firstdivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_firstdivisorproductoutput ge_representation_imaginary_code_iff_prime_firstdivisorproductoutput. (((gr_product_iff_prime_first) = ((ge_representation_real_code_iff_prime_firstdivisorproductoutput) + (ge_representation_imaginary_code_iff_prime_firstdivisorproductoutput)) * S ((ge_representation_real_code_iff_prime_firstdivisorproductoutput) + (ge_representation_imaginary_code_iff_prime_firstdivisorproductoutput)) + ((ge_representation_imaginary_code_iff_prime_firstdivisorproductoutput) + (ge_representation_imaginary_code_iff_prime_firstdivisorproductoutput))) /\ ((exists ge_balance_positive_iff_prime_firstdivisorproductoutputreal ge_balance_negative_iff_prime_firstdivisorproductoutputreal. (((((ge_representation_real_code_iff_prime_firstdivisorproductoutput) = 2 * (ge_balance_positive_iff_prime_firstdivisorproductoutputreal) /\ (ge_balance_negative_iff_prime_firstdivisorproductoutputreal) = 0) \/ exists ge_signed_half_iff_prime_firstdivisorproductoutputrealdecode. (((ge_representation_real_code_iff_prime_firstdivisorproductoutput) = 2 * ge_signed_half_iff_prime_firstdivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstdivisorproductoutputreal) = 0) /\ (ge_balance_negative_iff_prime_firstdivisorproductoutputreal) = S ge_signed_half_iff_prime_firstdivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_firstdivisorproduct) * (ge_second_rp_iff_prime_firstdivisorproduct))) + (((ge_first_rn_iff_prime_firstdivisorproduct) * (ge_second_rn_iff_prime_firstdivisorproduct))))) + (((((ge_first_ip_iff_prime_firstdivisorproduct) * (ge_second_in_iff_prime_firstdivisorproduct))) + (((ge_first_in_iff_prime_firstdivisorproduct) * (ge_second_ip_iff_prime_firstdivisorproduct))))))) + ge_balance_negative_iff_prime_firstdivisorproductoutputreal = (((((((ge_first_rp_iff_prime_firstdivisorproduct) * (ge_second_rn_iff_prime_firstdivisorproduct))) + (((ge_first_rn_iff_prime_firstdivisorproduct) * (ge_second_rp_iff_prime_firstdivisorproduct))))) + (((((ge_first_ip_iff_prime_firstdivisorproduct) * (ge_second_ip_iff_prime_firstdivisorproduct))) + (((ge_first_in_iff_prime_firstdivisorproduct) * (ge_second_in_iff_prime_firstdivisorproduct))))))) + ge_balance_positive_iff_prime_firstdivisorproductoutputreal))) /\ (exists ge_balance_positive_iff_prime_firstdivisorproductoutputimaginary ge_balance_negative_iff_prime_firstdivisorproductoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_firstdivisorproductoutput) = 2 * (ge_balance_positive_iff_prime_firstdivisorproductoutputimaginary) /\ (ge_balance_negative_iff_prime_firstdivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstdivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstdivisorproductoutput) = 2 * ge_signed_half_iff_prime_firstdivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstdivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstdivisorproductoutputimaginary) = S ge_signed_half_iff_prime_firstdivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_firstdivisorproduct) * (ge_second_ip_iff_prime_firstdivisorproduct))) + (((ge_first_rn_iff_prime_firstdivisorproduct) * (ge_second_in_iff_prime_firstdivisorproduct))))) + (((((ge_first_ip_iff_prime_firstdivisorproduct) * (ge_second_rp_iff_prime_firstdivisorproduct))) + (((ge_first_in_iff_prime_firstdivisorproduct) * (ge_second_rn_iff_prime_firstdivisorproduct))))))) + ge_balance_negative_iff_prime_firstdivisorproductoutputimaginary = (((((((ge_first_rp_iff_prime_firstdivisorproduct) * (ge_second_in_iff_prime_firstdivisorproduct))) + (((ge_first_rn_iff_prime_firstdivisorproduct) * (ge_second_ip_iff_prime_firstdivisorproduct))))) + (((((ge_first_ip_iff_prime_firstdivisorproduct) * (ge_second_rn_iff_prime_firstdivisorproduct))) + (((ge_first_in_iff_prime_firstdivisorproduct) * (ge_second_rp_iff_prime_firstdivisorproduct))))))) + ge_balance_positive_iff_prime_firstdivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_iff_prime_firstfirst_divisor. (exists ge_first_rp_iff_prime_firstfirst_divisorproduct ge_first_rn_iff_prime_firstfirst_divisorproduct ge_first_ip_iff_prime_firstfirst_divisorproduct ge_first_in_iff_prime_firstfirst_divisorproduct ge_second_rp_iff_prime_firstfirst_divisorproduct ge_second_rn_iff_prime_firstfirst_divisorproduct ge_second_ip_iff_prime_firstfirst_divisorproduct ge_second_in_iff_prime_firstfirst_divisorproduct. ((exists ge_representation_real_code_iff_prime_firstfirst_divisorproductfirst ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductfirst. (((p) = ((ge_representation_real_code_iff_prime_firstfirst_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductfirst)) * S ((ge_representation_real_code_iff_prime_firstfirst_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductfirst)) + ((ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductfirst))) /\ ((exists ge_balance_positive_iff_prime_firstfirst_divisorproductfirstreal ge_balance_negative_iff_prime_firstfirst_divisorproductfirstreal. (((((ge_representation_real_code_iff_prime_firstfirst_divisorproductfirst) = 2 * (ge_balance_positive_iff_prime_firstfirst_divisorproductfirstreal) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_iff_prime_firstfirst_divisorproductfirstrealdecode. (((ge_representation_real_code_iff_prime_firstfirst_divisorproductfirst) = 2 * ge_signed_half_iff_prime_firstfirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstfirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductfirstreal) = S ge_signed_half_iff_prime_firstfirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_iff_prime_firstfirst_divisorproduct) + ge_balance_negative_iff_prime_firstfirst_divisorproductfirstreal = (ge_first_rn_iff_prime_firstfirst_divisorproduct) + ge_balance_positive_iff_prime_firstfirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_iff_prime_firstfirst_divisorproductfirstimaginary ge_balance_negative_iff_prime_firstfirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductfirst) = 2 * (ge_balance_positive_iff_prime_firstfirst_divisorproductfirstimaginary) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstfirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductfirst) = 2 * ge_signed_half_iff_prime_firstfirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstfirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductfirstimaginary) = S ge_signed_half_iff_prime_firstfirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_firstfirst_divisorproduct) + ge_balance_negative_iff_prime_firstfirst_divisorproductfirstimaginary = (ge_first_in_iff_prime_firstfirst_divisorproduct) + ge_balance_positive_iff_prime_firstfirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_firstfirst_divisorproductsecond ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductsecond. (((gr_quotient_iff_prime_firstfirst_divisor) = ((ge_representation_real_code_iff_prime_firstfirst_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductsecond)) * S ((ge_representation_real_code_iff_prime_firstfirst_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductsecond)) + ((ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductsecond))) /\ ((exists ge_balance_positive_iff_prime_firstfirst_divisorproductsecondreal ge_balance_negative_iff_prime_firstfirst_divisorproductsecondreal. (((((ge_representation_real_code_iff_prime_firstfirst_divisorproductsecond) = 2 * (ge_balance_positive_iff_prime_firstfirst_divisorproductsecondreal) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_iff_prime_firstfirst_divisorproductsecondrealdecode. (((ge_representation_real_code_iff_prime_firstfirst_divisorproductsecond) = 2 * ge_signed_half_iff_prime_firstfirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstfirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductsecondreal) = S ge_signed_half_iff_prime_firstfirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_iff_prime_firstfirst_divisorproduct) + ge_balance_negative_iff_prime_firstfirst_divisorproductsecondreal = (ge_second_rn_iff_prime_firstfirst_divisorproduct) + ge_balance_positive_iff_prime_firstfirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_iff_prime_firstfirst_divisorproductsecondimaginary ge_balance_negative_iff_prime_firstfirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductsecond) = 2 * (ge_balance_positive_iff_prime_firstfirst_divisorproductsecondimaginary) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstfirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductsecond) = 2 * ge_signed_half_iff_prime_firstfirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstfirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductsecondimaginary) = S ge_signed_half_iff_prime_firstfirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_firstfirst_divisorproduct) + ge_balance_negative_iff_prime_firstfirst_divisorproductsecondimaginary = (ge_second_in_iff_prime_firstfirst_divisorproduct) + ge_balance_positive_iff_prime_firstfirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_firstfirst_divisorproductoutput ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductoutput. (((gr_first_factor_iff_prime_first) = ((ge_representation_real_code_iff_prime_firstfirst_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductoutput)) * S ((ge_representation_real_code_iff_prime_firstfirst_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductoutput)) + ((ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductoutput))) /\ ((exists ge_balance_positive_iff_prime_firstfirst_divisorproductoutputreal ge_balance_negative_iff_prime_firstfirst_divisorproductoutputreal. (((((ge_representation_real_code_iff_prime_firstfirst_divisorproductoutput) = 2 * (ge_balance_positive_iff_prime_firstfirst_divisorproductoutputreal) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_iff_prime_firstfirst_divisorproductoutputrealdecode. (((ge_representation_real_code_iff_prime_firstfirst_divisorproductoutput) = 2 * ge_signed_half_iff_prime_firstfirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstfirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductoutputreal) = S ge_signed_half_iff_prime_firstfirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_firstfirst_divisorproduct) * (ge_second_rp_iff_prime_firstfirst_divisorproduct))) + (((ge_first_rn_iff_prime_firstfirst_divisorproduct) * (ge_second_rn_iff_prime_firstfirst_divisorproduct))))) + (((((ge_first_ip_iff_prime_firstfirst_divisorproduct) * (ge_second_in_iff_prime_firstfirst_divisorproduct))) + (((ge_first_in_iff_prime_firstfirst_divisorproduct) * (ge_second_ip_iff_prime_firstfirst_divisorproduct))))))) + ge_balance_negative_iff_prime_firstfirst_divisorproductoutputreal = (((((((ge_first_rp_iff_prime_firstfirst_divisorproduct) * (ge_second_rn_iff_prime_firstfirst_divisorproduct))) + (((ge_first_rn_iff_prime_firstfirst_divisorproduct) * (ge_second_rp_iff_prime_firstfirst_divisorproduct))))) + (((((ge_first_ip_iff_prime_firstfirst_divisorproduct) * (ge_second_ip_iff_prime_firstfirst_divisorproduct))) + (((ge_first_in_iff_prime_firstfirst_divisorproduct) * (ge_second_in_iff_prime_firstfirst_divisorproduct))))))) + ge_balance_positive_iff_prime_firstfirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_iff_prime_firstfirst_divisorproductoutputimaginary ge_balance_negative_iff_prime_firstfirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductoutput) = 2 * (ge_balance_positive_iff_prime_firstfirst_divisorproductoutputimaginary) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstfirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstfirst_divisorproductoutput) = 2 * ge_signed_half_iff_prime_firstfirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstfirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstfirst_divisorproductoutputimaginary) = S ge_signed_half_iff_prime_firstfirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_firstfirst_divisorproduct) * (ge_second_ip_iff_prime_firstfirst_divisorproduct))) + (((ge_first_rn_iff_prime_firstfirst_divisorproduct) * (ge_second_in_iff_prime_firstfirst_divisorproduct))))) + (((((ge_first_ip_iff_prime_firstfirst_divisorproduct) * (ge_second_rp_iff_prime_firstfirst_divisorproduct))) + (((ge_first_in_iff_prime_firstfirst_divisorproduct) * (ge_second_rn_iff_prime_firstfirst_divisorproduct))))))) + ge_balance_negative_iff_prime_firstfirst_divisorproductoutputimaginary = (((((((ge_first_rp_iff_prime_firstfirst_divisorproduct) * (ge_second_in_iff_prime_firstfirst_divisorproduct))) + (((ge_first_rn_iff_prime_firstfirst_divisorproduct) * (ge_second_ip_iff_prime_firstfirst_divisorproduct))))) + (((((ge_first_ip_iff_prime_firstfirst_divisorproduct) * (ge_second_rn_iff_prime_firstfirst_divisorproduct))) + (((ge_first_in_iff_prime_firstfirst_divisorproduct) * (ge_second_rp_iff_prime_firstfirst_divisorproduct))))))) + ge_balance_positive_iff_prime_firstfirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_iff_prime_firstsecond_divisor. (exists ge_first_rp_iff_prime_firstsecond_divisorproduct ge_first_rn_iff_prime_firstsecond_divisorproduct ge_first_ip_iff_prime_firstsecond_divisorproduct ge_first_in_iff_prime_firstsecond_divisorproduct ge_second_rp_iff_prime_firstsecond_divisorproduct ge_second_rn_iff_prime_firstsecond_divisorproduct ge_second_ip_iff_prime_firstsecond_divisorproduct ge_second_in_iff_prime_firstsecond_divisorproduct. ((exists ge_representation_real_code_iff_prime_firstsecond_divisorproductfirst ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductfirst. (((p) = ((ge_representation_real_code_iff_prime_firstsecond_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductfirst)) * S ((ge_representation_real_code_iff_prime_firstsecond_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductfirst)) + ((ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductfirst))) /\ ((exists ge_balance_positive_iff_prime_firstsecond_divisorproductfirstreal ge_balance_negative_iff_prime_firstsecond_divisorproductfirstreal. (((((ge_representation_real_code_iff_prime_firstsecond_divisorproductfirst) = 2 * (ge_balance_positive_iff_prime_firstsecond_divisorproductfirstreal) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_iff_prime_firstsecond_divisorproductfirstrealdecode. (((ge_representation_real_code_iff_prime_firstsecond_divisorproductfirst) = 2 * ge_signed_half_iff_prime_firstsecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstsecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductfirstreal) = S ge_signed_half_iff_prime_firstsecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_iff_prime_firstsecond_divisorproduct) + ge_balance_negative_iff_prime_firstsecond_divisorproductfirstreal = (ge_first_rn_iff_prime_firstsecond_divisorproduct) + ge_balance_positive_iff_prime_firstsecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_iff_prime_firstsecond_divisorproductfirstimaginary ge_balance_negative_iff_prime_firstsecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductfirst) = 2 * (ge_balance_positive_iff_prime_firstsecond_divisorproductfirstimaginary) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstsecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductfirst) = 2 * ge_signed_half_iff_prime_firstsecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstsecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductfirstimaginary) = S ge_signed_half_iff_prime_firstsecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_firstsecond_divisorproduct) + ge_balance_negative_iff_prime_firstsecond_divisorproductfirstimaginary = (ge_first_in_iff_prime_firstsecond_divisorproduct) + ge_balance_positive_iff_prime_firstsecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_firstsecond_divisorproductsecond ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductsecond. (((gr_quotient_iff_prime_firstsecond_divisor) = ((ge_representation_real_code_iff_prime_firstsecond_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductsecond)) * S ((ge_representation_real_code_iff_prime_firstsecond_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductsecond)) + ((ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductsecond))) /\ ((exists ge_balance_positive_iff_prime_firstsecond_divisorproductsecondreal ge_balance_negative_iff_prime_firstsecond_divisorproductsecondreal. (((((ge_representation_real_code_iff_prime_firstsecond_divisorproductsecond) = 2 * (ge_balance_positive_iff_prime_firstsecond_divisorproductsecondreal) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_iff_prime_firstsecond_divisorproductsecondrealdecode. (((ge_representation_real_code_iff_prime_firstsecond_divisorproductsecond) = 2 * ge_signed_half_iff_prime_firstsecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstsecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductsecondreal) = S ge_signed_half_iff_prime_firstsecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_iff_prime_firstsecond_divisorproduct) + ge_balance_negative_iff_prime_firstsecond_divisorproductsecondreal = (ge_second_rn_iff_prime_firstsecond_divisorproduct) + ge_balance_positive_iff_prime_firstsecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_iff_prime_firstsecond_divisorproductsecondimaginary ge_balance_negative_iff_prime_firstsecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductsecond) = 2 * (ge_balance_positive_iff_prime_firstsecond_divisorproductsecondimaginary) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstsecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductsecond) = 2 * ge_signed_half_iff_prime_firstsecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstsecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductsecondimaginary) = S ge_signed_half_iff_prime_firstsecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_firstsecond_divisorproduct) + ge_balance_negative_iff_prime_firstsecond_divisorproductsecondimaginary = (ge_second_in_iff_prime_firstsecond_divisorproduct) + ge_balance_positive_iff_prime_firstsecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_firstsecond_divisorproductoutput ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductoutput. (((gr_second_factor_iff_prime_first) = ((ge_representation_real_code_iff_prime_firstsecond_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductoutput)) * S ((ge_representation_real_code_iff_prime_firstsecond_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductoutput)) + ((ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductoutput))) /\ ((exists ge_balance_positive_iff_prime_firstsecond_divisorproductoutputreal ge_balance_negative_iff_prime_firstsecond_divisorproductoutputreal. (((((ge_representation_real_code_iff_prime_firstsecond_divisorproductoutput) = 2 * (ge_balance_positive_iff_prime_firstsecond_divisorproductoutputreal) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_iff_prime_firstsecond_divisorproductoutputrealdecode. (((ge_representation_real_code_iff_prime_firstsecond_divisorproductoutput) = 2 * ge_signed_half_iff_prime_firstsecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_firstsecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductoutputreal) = S ge_signed_half_iff_prime_firstsecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_firstsecond_divisorproduct) * (ge_second_rp_iff_prime_firstsecond_divisorproduct))) + (((ge_first_rn_iff_prime_firstsecond_divisorproduct) * (ge_second_rn_iff_prime_firstsecond_divisorproduct))))) + (((((ge_first_ip_iff_prime_firstsecond_divisorproduct) * (ge_second_in_iff_prime_firstsecond_divisorproduct))) + (((ge_first_in_iff_prime_firstsecond_divisorproduct) * (ge_second_ip_iff_prime_firstsecond_divisorproduct))))))) + ge_balance_negative_iff_prime_firstsecond_divisorproductoutputreal = (((((((ge_first_rp_iff_prime_firstsecond_divisorproduct) * (ge_second_rn_iff_prime_firstsecond_divisorproduct))) + (((ge_first_rn_iff_prime_firstsecond_divisorproduct) * (ge_second_rp_iff_prime_firstsecond_divisorproduct))))) + (((((ge_first_ip_iff_prime_firstsecond_divisorproduct) * (ge_second_ip_iff_prime_firstsecond_divisorproduct))) + (((ge_first_in_iff_prime_firstsecond_divisorproduct) * (ge_second_in_iff_prime_firstsecond_divisorproduct))))))) + ge_balance_positive_iff_prime_firstsecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_iff_prime_firstsecond_divisorproductoutputimaginary ge_balance_negative_iff_prime_firstsecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductoutput) = 2 * (ge_balance_positive_iff_prime_firstsecond_divisorproductoutputimaginary) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_firstsecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_firstsecond_divisorproductoutput) = 2 * ge_signed_half_iff_prime_firstsecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_firstsecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_firstsecond_divisorproductoutputimaginary) = S ge_signed_half_iff_prime_firstsecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_firstsecond_divisorproduct) * (ge_second_ip_iff_prime_firstsecond_divisorproduct))) + (((ge_first_rn_iff_prime_firstsecond_divisorproduct) * (ge_second_in_iff_prime_firstsecond_divisorproduct))))) + (((((ge_first_ip_iff_prime_firstsecond_divisorproduct) * (ge_second_rp_iff_prime_firstsecond_divisorproduct))) + (((ge_first_in_iff_prime_firstsecond_divisorproduct) * (ge_second_rn_iff_prime_firstsecond_divisorproduct))))))) + ge_balance_negative_iff_prime_firstsecond_divisorproductoutputimaginary = (((((((ge_first_rp_iff_prime_firstsecond_divisorproduct) * (ge_second_in_iff_prime_firstsecond_divisorproduct))) + (((ge_first_rn_iff_prime_firstsecond_divisorproduct) * (ge_second_ip_iff_prime_firstsecond_divisorproduct))))) + (((((ge_first_ip_iff_prime_firstsecond_divisorproduct) * (ge_second_rn_iff_prime_firstsecond_divisorproduct))) + (((ge_first_in_iff_prime_firstsecond_divisorproduct) * (ge_second_rp_iff_prime_firstsecond_divisorproduct))))))) + ge_balance_positive_iff_prime_firstsecond_divisorproductoutputimaginary)))))))))))))))) /\ ((((exists ge_real_positive_iff_prime_secondcarrier ge_real_negative_iff_prime_secondcarrier ge_imaginary_positive_iff_prime_secondcarrier ge_imaginary_negative_iff_prime_secondcarrier. (exists ge_real_code_iff_prime_secondcarrierdecode ge_imaginary_code_iff_prime_secondcarrierdecode. (((p) = ((ge_real_code_iff_prime_secondcarrierdecode) + (ge_imaginary_code_iff_prime_secondcarrierdecode)) * S ((ge_real_code_iff_prime_secondcarrierdecode) + (ge_imaginary_code_iff_prime_secondcarrierdecode)) + ((ge_imaginary_code_iff_prime_secondcarrierdecode) + (ge_imaginary_code_iff_prime_secondcarrierdecode))) /\ (((((ge_real_code_iff_prime_secondcarrierdecode) = 2 * (ge_real_positive_iff_prime_secondcarrier) /\ (ge_real_negative_iff_prime_secondcarrier) = 0) \/ exists ge_signed_half_ge_iff_prime_secondcarrierdecode_real. (((ge_real_code_iff_prime_secondcarrierdecode) = 2 * ge_signed_half_ge_iff_prime_secondcarrierdecode_real + 1 /\ (ge_real_positive_iff_prime_secondcarrier) = 0) /\ (ge_real_negative_iff_prime_secondcarrier) = S ge_signed_half_ge_iff_prime_secondcarrierdecode_real))) /\ ((((ge_imaginary_code_iff_prime_secondcarrierdecode) = 2 * (ge_imaginary_positive_iff_prime_secondcarrier) /\ (ge_imaginary_negative_iff_prime_secondcarrier) = 0) \/ exists ge_signed_half_ge_iff_prime_secondcarrierdecode_imaginary. (((ge_imaginary_code_iff_prime_secondcarrierdecode) = 2 * ge_signed_half_ge_iff_prime_secondcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_iff_prime_secondcarrier) = 0) /\ (ge_imaginary_negative_iff_prime_secondcarrier) = S ge_signed_half_ge_iff_prime_secondcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_iff_prime_secondnonunit. (exists ge_first_rp_iff_prime_secondnonunitidentity ge_first_rn_iff_prime_secondnonunitidentity ge_first_ip_iff_prime_secondnonunitidentity ge_first_in_iff_prime_secondnonunitidentity ge_second_rp_iff_prime_secondnonunitidentity ge_second_rn_iff_prime_secondnonunitidentity ge_second_ip_iff_prime_secondnonunitidentity ge_second_in_iff_prime_secondnonunitidentity. ((exists ge_representation_real_code_iff_prime_secondnonunitidentityfirst ge_representation_imaginary_code_iff_prime_secondnonunitidentityfirst. (((p) = ((ge_representation_real_code_iff_prime_secondnonunitidentityfirst) + (ge_representation_imaginary_code_iff_prime_secondnonunitidentityfirst)) * S ((ge_representation_real_code_iff_prime_secondnonunitidentityfirst) + (ge_representation_imaginary_code_iff_prime_secondnonunitidentityfirst)) + ((ge_representation_imaginary_code_iff_prime_secondnonunitidentityfirst) + (ge_representation_imaginary_code_iff_prime_secondnonunitidentityfirst))) /\ ((exists ge_balance_positive_iff_prime_secondnonunitidentityfirstreal ge_balance_negative_iff_prime_secondnonunitidentityfirstreal. (((((ge_representation_real_code_iff_prime_secondnonunitidentityfirst) = 2 * (ge_balance_positive_iff_prime_secondnonunitidentityfirstreal) /\ (ge_balance_negative_iff_prime_secondnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_iff_prime_secondnonunitidentityfirstrealdecode. (((ge_representation_real_code_iff_prime_secondnonunitidentityfirst) = 2 * ge_signed_half_iff_prime_secondnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_iff_prime_secondnonunitidentityfirstreal) = S ge_signed_half_iff_prime_secondnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_iff_prime_secondnonunitidentity) + ge_balance_negative_iff_prime_secondnonunitidentityfirstreal = (ge_first_rn_iff_prime_secondnonunitidentity) + ge_balance_positive_iff_prime_secondnonunitidentityfirstreal))) /\ (exists ge_balance_positive_iff_prime_secondnonunitidentityfirstimaginary ge_balance_negative_iff_prime_secondnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_secondnonunitidentityfirst) = 2 * (ge_balance_positive_iff_prime_secondnonunitidentityfirstimaginary) /\ (ge_balance_negative_iff_prime_secondnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondnonunitidentityfirst) = 2 * ge_signed_half_iff_prime_secondnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondnonunitidentityfirstimaginary) = S ge_signed_half_iff_prime_secondnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_secondnonunitidentity) + ge_balance_negative_iff_prime_secondnonunitidentityfirstimaginary = (ge_first_in_iff_prime_secondnonunitidentity) + ge_balance_positive_iff_prime_secondnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_secondnonunitidentitysecond ge_representation_imaginary_code_iff_prime_secondnonunitidentitysecond. (((gr_inverse_iff_prime_secondnonunit) = ((ge_representation_real_code_iff_prime_secondnonunitidentitysecond) + (ge_representation_imaginary_code_iff_prime_secondnonunitidentitysecond)) * S ((ge_representation_real_code_iff_prime_secondnonunitidentitysecond) + (ge_representation_imaginary_code_iff_prime_secondnonunitidentitysecond)) + ((ge_representation_imaginary_code_iff_prime_secondnonunitidentitysecond) + (ge_representation_imaginary_code_iff_prime_secondnonunitidentitysecond))) /\ ((exists ge_balance_positive_iff_prime_secondnonunitidentitysecondreal ge_balance_negative_iff_prime_secondnonunitidentitysecondreal. (((((ge_representation_real_code_iff_prime_secondnonunitidentitysecond) = 2 * (ge_balance_positive_iff_prime_secondnonunitidentitysecondreal) /\ (ge_balance_negative_iff_prime_secondnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_iff_prime_secondnonunitidentitysecondrealdecode. (((ge_representation_real_code_iff_prime_secondnonunitidentitysecond) = 2 * ge_signed_half_iff_prime_secondnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_iff_prime_secondnonunitidentitysecondreal) = S ge_signed_half_iff_prime_secondnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_iff_prime_secondnonunitidentity) + ge_balance_negative_iff_prime_secondnonunitidentitysecondreal = (ge_second_rn_iff_prime_secondnonunitidentity) + ge_balance_positive_iff_prime_secondnonunitidentitysecondreal))) /\ (exists ge_balance_positive_iff_prime_secondnonunitidentitysecondimaginary ge_balance_negative_iff_prime_secondnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_iff_prime_secondnonunitidentitysecond) = 2 * (ge_balance_positive_iff_prime_secondnonunitidentitysecondimaginary) /\ (ge_balance_negative_iff_prime_secondnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondnonunitidentitysecond) = 2 * ge_signed_half_iff_prime_secondnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondnonunitidentitysecondimaginary) = S ge_signed_half_iff_prime_secondnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_secondnonunitidentity) + ge_balance_negative_iff_prime_secondnonunitidentitysecondimaginary = (ge_second_in_iff_prime_secondnonunitidentity) + ge_balance_positive_iff_prime_secondnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_secondnonunitidentityoutput ge_representation_imaginary_code_iff_prime_secondnonunitidentityoutput. (((6) = ((ge_representation_real_code_iff_prime_secondnonunitidentityoutput) + (ge_representation_imaginary_code_iff_prime_secondnonunitidentityoutput)) * S ((ge_representation_real_code_iff_prime_secondnonunitidentityoutput) + (ge_representation_imaginary_code_iff_prime_secondnonunitidentityoutput)) + ((ge_representation_imaginary_code_iff_prime_secondnonunitidentityoutput) + (ge_representation_imaginary_code_iff_prime_secondnonunitidentityoutput))) /\ ((exists ge_balance_positive_iff_prime_secondnonunitidentityoutputreal ge_balance_negative_iff_prime_secondnonunitidentityoutputreal. (((((ge_representation_real_code_iff_prime_secondnonunitidentityoutput) = 2 * (ge_balance_positive_iff_prime_secondnonunitidentityoutputreal) /\ (ge_balance_negative_iff_prime_secondnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_iff_prime_secondnonunitidentityoutputrealdecode. (((ge_representation_real_code_iff_prime_secondnonunitidentityoutput) = 2 * ge_signed_half_iff_prime_secondnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_iff_prime_secondnonunitidentityoutputreal) = S ge_signed_half_iff_prime_secondnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_secondnonunitidentity) * (ge_second_rp_iff_prime_secondnonunitidentity))) + (((ge_first_rn_iff_prime_secondnonunitidentity) * (ge_second_rn_iff_prime_secondnonunitidentity))))) + (((((ge_first_ip_iff_prime_secondnonunitidentity) * (ge_second_in_iff_prime_secondnonunitidentity))) + (((ge_first_in_iff_prime_secondnonunitidentity) * (ge_second_ip_iff_prime_secondnonunitidentity))))))) + ge_balance_negative_iff_prime_secondnonunitidentityoutputreal = (((((((ge_first_rp_iff_prime_secondnonunitidentity) * (ge_second_rn_iff_prime_secondnonunitidentity))) + (((ge_first_rn_iff_prime_secondnonunitidentity) * (ge_second_rp_iff_prime_secondnonunitidentity))))) + (((((ge_first_ip_iff_prime_secondnonunitidentity) * (ge_second_ip_iff_prime_secondnonunitidentity))) + (((ge_first_in_iff_prime_secondnonunitidentity) * (ge_second_in_iff_prime_secondnonunitidentity))))))) + ge_balance_positive_iff_prime_secondnonunitidentityoutputreal))) /\ (exists ge_balance_positive_iff_prime_secondnonunitidentityoutputimaginary ge_balance_negative_iff_prime_secondnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_secondnonunitidentityoutput) = 2 * (ge_balance_positive_iff_prime_secondnonunitidentityoutputimaginary) /\ (ge_balance_negative_iff_prime_secondnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondnonunitidentityoutput) = 2 * ge_signed_half_iff_prime_secondnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondnonunitidentityoutputimaginary) = S ge_signed_half_iff_prime_secondnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_secondnonunitidentity) * (ge_second_ip_iff_prime_secondnonunitidentity))) + (((ge_first_rn_iff_prime_secondnonunitidentity) * (ge_second_in_iff_prime_secondnonunitidentity))))) + (((((ge_first_ip_iff_prime_secondnonunitidentity) * (ge_second_rp_iff_prime_secondnonunitidentity))) + (((ge_first_in_iff_prime_secondnonunitidentity) * (ge_second_rn_iff_prime_secondnonunitidentity))))))) + ge_balance_negative_iff_prime_secondnonunitidentityoutputimaginary = (((((((ge_first_rp_iff_prime_secondnonunitidentity) * (ge_second_in_iff_prime_secondnonunitidentity))) + (((ge_first_rn_iff_prime_secondnonunitidentity) * (ge_second_ip_iff_prime_secondnonunitidentity))))) + (((((ge_first_ip_iff_prime_secondnonunitidentity) * (ge_second_rn_iff_prime_secondnonunitidentity))) + (((ge_first_in_iff_prime_secondnonunitidentity) * (ge_second_rp_iff_prime_secondnonunitidentity))))))) + ge_balance_positive_iff_prime_secondnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_iff_prime_second gr_second_factor_iff_prime_second gr_product_iff_prime_second. (exists ge_first_rp_iff_prime_secondproduct ge_first_rn_iff_prime_secondproduct ge_first_ip_iff_prime_secondproduct ge_first_in_iff_prime_secondproduct ge_second_rp_iff_prime_secondproduct ge_second_rn_iff_prime_secondproduct ge_second_ip_iff_prime_secondproduct ge_second_in_iff_prime_secondproduct. ((exists ge_representation_real_code_iff_prime_secondproductfirst ge_representation_imaginary_code_iff_prime_secondproductfirst. (((gr_first_factor_iff_prime_second) = ((ge_representation_real_code_iff_prime_secondproductfirst) + (ge_representation_imaginary_code_iff_prime_secondproductfirst)) * S ((ge_representation_real_code_iff_prime_secondproductfirst) + (ge_representation_imaginary_code_iff_prime_secondproductfirst)) + ((ge_representation_imaginary_code_iff_prime_secondproductfirst) + (ge_representation_imaginary_code_iff_prime_secondproductfirst))) /\ ((exists ge_balance_positive_iff_prime_secondproductfirstreal ge_balance_negative_iff_prime_secondproductfirstreal. (((((ge_representation_real_code_iff_prime_secondproductfirst) = 2 * (ge_balance_positive_iff_prime_secondproductfirstreal) /\ (ge_balance_negative_iff_prime_secondproductfirstreal) = 0) \/ exists ge_signed_half_iff_prime_secondproductfirstrealdecode. (((ge_representation_real_code_iff_prime_secondproductfirst) = 2 * ge_signed_half_iff_prime_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondproductfirstreal) = 0) /\ (ge_balance_negative_iff_prime_secondproductfirstreal) = S ge_signed_half_iff_prime_secondproductfirstrealdecode))) /\ ((ge_first_rp_iff_prime_secondproduct) + ge_balance_negative_iff_prime_secondproductfirstreal = (ge_first_rn_iff_prime_secondproduct) + ge_balance_positive_iff_prime_secondproductfirstreal))) /\ (exists ge_balance_positive_iff_prime_secondproductfirstimaginary ge_balance_negative_iff_prime_secondproductfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_secondproductfirst) = 2 * (ge_balance_positive_iff_prime_secondproductfirstimaginary) /\ (ge_balance_negative_iff_prime_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondproductfirst) = 2 * ge_signed_half_iff_prime_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondproductfirstimaginary) = S ge_signed_half_iff_prime_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_secondproduct) + ge_balance_negative_iff_prime_secondproductfirstimaginary = (ge_first_in_iff_prime_secondproduct) + ge_balance_positive_iff_prime_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_secondproductsecond ge_representation_imaginary_code_iff_prime_secondproductsecond. (((gr_second_factor_iff_prime_second) = ((ge_representation_real_code_iff_prime_secondproductsecond) + (ge_representation_imaginary_code_iff_prime_secondproductsecond)) * S ((ge_representation_real_code_iff_prime_secondproductsecond) + (ge_representation_imaginary_code_iff_prime_secondproductsecond)) + ((ge_representation_imaginary_code_iff_prime_secondproductsecond) + (ge_representation_imaginary_code_iff_prime_secondproductsecond))) /\ ((exists ge_balance_positive_iff_prime_secondproductsecondreal ge_balance_negative_iff_prime_secondproductsecondreal. (((((ge_representation_real_code_iff_prime_secondproductsecond) = 2 * (ge_balance_positive_iff_prime_secondproductsecondreal) /\ (ge_balance_negative_iff_prime_secondproductsecondreal) = 0) \/ exists ge_signed_half_iff_prime_secondproductsecondrealdecode. (((ge_representation_real_code_iff_prime_secondproductsecond) = 2 * ge_signed_half_iff_prime_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondproductsecondreal) = 0) /\ (ge_balance_negative_iff_prime_secondproductsecondreal) = S ge_signed_half_iff_prime_secondproductsecondrealdecode))) /\ ((ge_second_rp_iff_prime_secondproduct) + ge_balance_negative_iff_prime_secondproductsecondreal = (ge_second_rn_iff_prime_secondproduct) + ge_balance_positive_iff_prime_secondproductsecondreal))) /\ (exists ge_balance_positive_iff_prime_secondproductsecondimaginary ge_balance_negative_iff_prime_secondproductsecondimaginary. (((((ge_representation_imaginary_code_iff_prime_secondproductsecond) = 2 * (ge_balance_positive_iff_prime_secondproductsecondimaginary) /\ (ge_balance_negative_iff_prime_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondproductsecond) = 2 * ge_signed_half_iff_prime_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondproductsecondimaginary) = S ge_signed_half_iff_prime_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_secondproduct) + ge_balance_negative_iff_prime_secondproductsecondimaginary = (ge_second_in_iff_prime_secondproduct) + ge_balance_positive_iff_prime_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_secondproductoutput ge_representation_imaginary_code_iff_prime_secondproductoutput. (((gr_product_iff_prime_second) = ((ge_representation_real_code_iff_prime_secondproductoutput) + (ge_representation_imaginary_code_iff_prime_secondproductoutput)) * S ((ge_representation_real_code_iff_prime_secondproductoutput) + (ge_representation_imaginary_code_iff_prime_secondproductoutput)) + ((ge_representation_imaginary_code_iff_prime_secondproductoutput) + (ge_representation_imaginary_code_iff_prime_secondproductoutput))) /\ ((exists ge_balance_positive_iff_prime_secondproductoutputreal ge_balance_negative_iff_prime_secondproductoutputreal. (((((ge_representation_real_code_iff_prime_secondproductoutput) = 2 * (ge_balance_positive_iff_prime_secondproductoutputreal) /\ (ge_balance_negative_iff_prime_secondproductoutputreal) = 0) \/ exists ge_signed_half_iff_prime_secondproductoutputrealdecode. (((ge_representation_real_code_iff_prime_secondproductoutput) = 2 * ge_signed_half_iff_prime_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondproductoutputreal) = 0) /\ (ge_balance_negative_iff_prime_secondproductoutputreal) = S ge_signed_half_iff_prime_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_secondproduct) * (ge_second_rp_iff_prime_secondproduct))) + (((ge_first_rn_iff_prime_secondproduct) * (ge_second_rn_iff_prime_secondproduct))))) + (((((ge_first_ip_iff_prime_secondproduct) * (ge_second_in_iff_prime_secondproduct))) + (((ge_first_in_iff_prime_secondproduct) * (ge_second_ip_iff_prime_secondproduct))))))) + ge_balance_negative_iff_prime_secondproductoutputreal = (((((((ge_first_rp_iff_prime_secondproduct) * (ge_second_rn_iff_prime_secondproduct))) + (((ge_first_rn_iff_prime_secondproduct) * (ge_second_rp_iff_prime_secondproduct))))) + (((((ge_first_ip_iff_prime_secondproduct) * (ge_second_ip_iff_prime_secondproduct))) + (((ge_first_in_iff_prime_secondproduct) * (ge_second_in_iff_prime_secondproduct))))))) + ge_balance_positive_iff_prime_secondproductoutputreal))) /\ (exists ge_balance_positive_iff_prime_secondproductoutputimaginary ge_balance_negative_iff_prime_secondproductoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_secondproductoutput) = 2 * (ge_balance_positive_iff_prime_secondproductoutputimaginary) /\ (ge_balance_negative_iff_prime_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondproductoutput) = 2 * ge_signed_half_iff_prime_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondproductoutputimaginary) = S ge_signed_half_iff_prime_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_secondproduct) * (ge_second_ip_iff_prime_secondproduct))) + (((ge_first_rn_iff_prime_secondproduct) * (ge_second_in_iff_prime_secondproduct))))) + (((((ge_first_ip_iff_prime_secondproduct) * (ge_second_rp_iff_prime_secondproduct))) + (((ge_first_in_iff_prime_secondproduct) * (ge_second_rn_iff_prime_secondproduct))))))) + ge_balance_negative_iff_prime_secondproductoutputimaginary = (((((((ge_first_rp_iff_prime_secondproduct) * (ge_second_in_iff_prime_secondproduct))) + (((ge_first_rn_iff_prime_secondproduct) * (ge_second_ip_iff_prime_secondproduct))))) + (((((ge_first_ip_iff_prime_secondproduct) * (ge_second_rn_iff_prime_secondproduct))) + (((ge_first_in_iff_prime_secondproduct) * (ge_second_rp_iff_prime_secondproduct))))))) + ge_balance_positive_iff_prime_secondproductoutputimaginary))))))))) -> (exists gr_quotient_iff_prime_seconddivisor. (exists ge_first_rp_iff_prime_seconddivisorproduct ge_first_rn_iff_prime_seconddivisorproduct ge_first_ip_iff_prime_seconddivisorproduct ge_first_in_iff_prime_seconddivisorproduct ge_second_rp_iff_prime_seconddivisorproduct ge_second_rn_iff_prime_seconddivisorproduct ge_second_ip_iff_prime_seconddivisorproduct ge_second_in_iff_prime_seconddivisorproduct. ((exists ge_representation_real_code_iff_prime_seconddivisorproductfirst ge_representation_imaginary_code_iff_prime_seconddivisorproductfirst. (((p) = ((ge_representation_real_code_iff_prime_seconddivisorproductfirst) + (ge_representation_imaginary_code_iff_prime_seconddivisorproductfirst)) * S ((ge_representation_real_code_iff_prime_seconddivisorproductfirst) + (ge_representation_imaginary_code_iff_prime_seconddivisorproductfirst)) + ((ge_representation_imaginary_code_iff_prime_seconddivisorproductfirst) + (ge_representation_imaginary_code_iff_prime_seconddivisorproductfirst))) /\ ((exists ge_balance_positive_iff_prime_seconddivisorproductfirstreal ge_balance_negative_iff_prime_seconddivisorproductfirstreal. (((((ge_representation_real_code_iff_prime_seconddivisorproductfirst) = 2 * (ge_balance_positive_iff_prime_seconddivisorproductfirstreal) /\ (ge_balance_negative_iff_prime_seconddivisorproductfirstreal) = 0) \/ exists ge_signed_half_iff_prime_seconddivisorproductfirstrealdecode. (((ge_representation_real_code_iff_prime_seconddivisorproductfirst) = 2 * ge_signed_half_iff_prime_seconddivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_seconddivisorproductfirstreal) = 0) /\ (ge_balance_negative_iff_prime_seconddivisorproductfirstreal) = S ge_signed_half_iff_prime_seconddivisorproductfirstrealdecode))) /\ ((ge_first_rp_iff_prime_seconddivisorproduct) + ge_balance_negative_iff_prime_seconddivisorproductfirstreal = (ge_first_rn_iff_prime_seconddivisorproduct) + ge_balance_positive_iff_prime_seconddivisorproductfirstreal))) /\ (exists ge_balance_positive_iff_prime_seconddivisorproductfirstimaginary ge_balance_negative_iff_prime_seconddivisorproductfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_seconddivisorproductfirst) = 2 * (ge_balance_positive_iff_prime_seconddivisorproductfirstimaginary) /\ (ge_balance_negative_iff_prime_seconddivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_seconddivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_seconddivisorproductfirst) = 2 * ge_signed_half_iff_prime_seconddivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_seconddivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_seconddivisorproductfirstimaginary) = S ge_signed_half_iff_prime_seconddivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_seconddivisorproduct) + ge_balance_negative_iff_prime_seconddivisorproductfirstimaginary = (ge_first_in_iff_prime_seconddivisorproduct) + ge_balance_positive_iff_prime_seconddivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_seconddivisorproductsecond ge_representation_imaginary_code_iff_prime_seconddivisorproductsecond. (((gr_quotient_iff_prime_seconddivisor) = ((ge_representation_real_code_iff_prime_seconddivisorproductsecond) + (ge_representation_imaginary_code_iff_prime_seconddivisorproductsecond)) * S ((ge_representation_real_code_iff_prime_seconddivisorproductsecond) + (ge_representation_imaginary_code_iff_prime_seconddivisorproductsecond)) + ((ge_representation_imaginary_code_iff_prime_seconddivisorproductsecond) + (ge_representation_imaginary_code_iff_prime_seconddivisorproductsecond))) /\ ((exists ge_balance_positive_iff_prime_seconddivisorproductsecondreal ge_balance_negative_iff_prime_seconddivisorproductsecondreal. (((((ge_representation_real_code_iff_prime_seconddivisorproductsecond) = 2 * (ge_balance_positive_iff_prime_seconddivisorproductsecondreal) /\ (ge_balance_negative_iff_prime_seconddivisorproductsecondreal) = 0) \/ exists ge_signed_half_iff_prime_seconddivisorproductsecondrealdecode. (((ge_representation_real_code_iff_prime_seconddivisorproductsecond) = 2 * ge_signed_half_iff_prime_seconddivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_seconddivisorproductsecondreal) = 0) /\ (ge_balance_negative_iff_prime_seconddivisorproductsecondreal) = S ge_signed_half_iff_prime_seconddivisorproductsecondrealdecode))) /\ ((ge_second_rp_iff_prime_seconddivisorproduct) + ge_balance_negative_iff_prime_seconddivisorproductsecondreal = (ge_second_rn_iff_prime_seconddivisorproduct) + ge_balance_positive_iff_prime_seconddivisorproductsecondreal))) /\ (exists ge_balance_positive_iff_prime_seconddivisorproductsecondimaginary ge_balance_negative_iff_prime_seconddivisorproductsecondimaginary. (((((ge_representation_imaginary_code_iff_prime_seconddivisorproductsecond) = 2 * (ge_balance_positive_iff_prime_seconddivisorproductsecondimaginary) /\ (ge_balance_negative_iff_prime_seconddivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_seconddivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_seconddivisorproductsecond) = 2 * ge_signed_half_iff_prime_seconddivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_seconddivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_seconddivisorproductsecondimaginary) = S ge_signed_half_iff_prime_seconddivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_seconddivisorproduct) + ge_balance_negative_iff_prime_seconddivisorproductsecondimaginary = (ge_second_in_iff_prime_seconddivisorproduct) + ge_balance_positive_iff_prime_seconddivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_seconddivisorproductoutput ge_representation_imaginary_code_iff_prime_seconddivisorproductoutput. (((gr_product_iff_prime_second) = ((ge_representation_real_code_iff_prime_seconddivisorproductoutput) + (ge_representation_imaginary_code_iff_prime_seconddivisorproductoutput)) * S ((ge_representation_real_code_iff_prime_seconddivisorproductoutput) + (ge_representation_imaginary_code_iff_prime_seconddivisorproductoutput)) + ((ge_representation_imaginary_code_iff_prime_seconddivisorproductoutput) + (ge_representation_imaginary_code_iff_prime_seconddivisorproductoutput))) /\ ((exists ge_balance_positive_iff_prime_seconddivisorproductoutputreal ge_balance_negative_iff_prime_seconddivisorproductoutputreal. (((((ge_representation_real_code_iff_prime_seconddivisorproductoutput) = 2 * (ge_balance_positive_iff_prime_seconddivisorproductoutputreal) /\ (ge_balance_negative_iff_prime_seconddivisorproductoutputreal) = 0) \/ exists ge_signed_half_iff_prime_seconddivisorproductoutputrealdecode. (((ge_representation_real_code_iff_prime_seconddivisorproductoutput) = 2 * ge_signed_half_iff_prime_seconddivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_seconddivisorproductoutputreal) = 0) /\ (ge_balance_negative_iff_prime_seconddivisorproductoutputreal) = S ge_signed_half_iff_prime_seconddivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_seconddivisorproduct) * (ge_second_rp_iff_prime_seconddivisorproduct))) + (((ge_first_rn_iff_prime_seconddivisorproduct) * (ge_second_rn_iff_prime_seconddivisorproduct))))) + (((((ge_first_ip_iff_prime_seconddivisorproduct) * (ge_second_in_iff_prime_seconddivisorproduct))) + (((ge_first_in_iff_prime_seconddivisorproduct) * (ge_second_ip_iff_prime_seconddivisorproduct))))))) + ge_balance_negative_iff_prime_seconddivisorproductoutputreal = (((((((ge_first_rp_iff_prime_seconddivisorproduct) * (ge_second_rn_iff_prime_seconddivisorproduct))) + (((ge_first_rn_iff_prime_seconddivisorproduct) * (ge_second_rp_iff_prime_seconddivisorproduct))))) + (((((ge_first_ip_iff_prime_seconddivisorproduct) * (ge_second_ip_iff_prime_seconddivisorproduct))) + (((ge_first_in_iff_prime_seconddivisorproduct) * (ge_second_in_iff_prime_seconddivisorproduct))))))) + ge_balance_positive_iff_prime_seconddivisorproductoutputreal))) /\ (exists ge_balance_positive_iff_prime_seconddivisorproductoutputimaginary ge_balance_negative_iff_prime_seconddivisorproductoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_seconddivisorproductoutput) = 2 * (ge_balance_positive_iff_prime_seconddivisorproductoutputimaginary) /\ (ge_balance_negative_iff_prime_seconddivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_seconddivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_seconddivisorproductoutput) = 2 * ge_signed_half_iff_prime_seconddivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_seconddivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_seconddivisorproductoutputimaginary) = S ge_signed_half_iff_prime_seconddivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_seconddivisorproduct) * (ge_second_ip_iff_prime_seconddivisorproduct))) + (((ge_first_rn_iff_prime_seconddivisorproduct) * (ge_second_in_iff_prime_seconddivisorproduct))))) + (((((ge_first_ip_iff_prime_seconddivisorproduct) * (ge_second_rp_iff_prime_seconddivisorproduct))) + (((ge_first_in_iff_prime_seconddivisorproduct) * (ge_second_rn_iff_prime_seconddivisorproduct))))))) + ge_balance_negative_iff_prime_seconddivisorproductoutputimaginary = (((((((ge_first_rp_iff_prime_seconddivisorproduct) * (ge_second_in_iff_prime_seconddivisorproduct))) + (((ge_first_rn_iff_prime_seconddivisorproduct) * (ge_second_ip_iff_prime_seconddivisorproduct))))) + (((((ge_first_ip_iff_prime_seconddivisorproduct) * (ge_second_rn_iff_prime_seconddivisorproduct))) + (((ge_first_in_iff_prime_seconddivisorproduct) * (ge_second_rp_iff_prime_seconddivisorproduct))))))) + ge_balance_positive_iff_prime_seconddivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_iff_prime_secondfirst_divisor. (exists ge_first_rp_iff_prime_secondfirst_divisorproduct ge_first_rn_iff_prime_secondfirst_divisorproduct ge_first_ip_iff_prime_secondfirst_divisorproduct ge_first_in_iff_prime_secondfirst_divisorproduct ge_second_rp_iff_prime_secondfirst_divisorproduct ge_second_rn_iff_prime_secondfirst_divisorproduct ge_second_ip_iff_prime_secondfirst_divisorproduct ge_second_in_iff_prime_secondfirst_divisorproduct. ((exists ge_representation_real_code_iff_prime_secondfirst_divisorproductfirst ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductfirst. (((p) = ((ge_representation_real_code_iff_prime_secondfirst_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductfirst)) * S ((ge_representation_real_code_iff_prime_secondfirst_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductfirst)) + ((ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductfirst))) /\ ((exists ge_balance_positive_iff_prime_secondfirst_divisorproductfirstreal ge_balance_negative_iff_prime_secondfirst_divisorproductfirstreal. (((((ge_representation_real_code_iff_prime_secondfirst_divisorproductfirst) = 2 * (ge_balance_positive_iff_prime_secondfirst_divisorproductfirstreal) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_iff_prime_secondfirst_divisorproductfirstrealdecode. (((ge_representation_real_code_iff_prime_secondfirst_divisorproductfirst) = 2 * ge_signed_half_iff_prime_secondfirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondfirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductfirstreal) = S ge_signed_half_iff_prime_secondfirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_iff_prime_secondfirst_divisorproduct) + ge_balance_negative_iff_prime_secondfirst_divisorproductfirstreal = (ge_first_rn_iff_prime_secondfirst_divisorproduct) + ge_balance_positive_iff_prime_secondfirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_iff_prime_secondfirst_divisorproductfirstimaginary ge_balance_negative_iff_prime_secondfirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductfirst) = 2 * (ge_balance_positive_iff_prime_secondfirst_divisorproductfirstimaginary) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondfirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductfirst) = 2 * ge_signed_half_iff_prime_secondfirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondfirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductfirstimaginary) = S ge_signed_half_iff_prime_secondfirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_secondfirst_divisorproduct) + ge_balance_negative_iff_prime_secondfirst_divisorproductfirstimaginary = (ge_first_in_iff_prime_secondfirst_divisorproduct) + ge_balance_positive_iff_prime_secondfirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_secondfirst_divisorproductsecond ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductsecond. (((gr_quotient_iff_prime_secondfirst_divisor) = ((ge_representation_real_code_iff_prime_secondfirst_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductsecond)) * S ((ge_representation_real_code_iff_prime_secondfirst_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductsecond)) + ((ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductsecond))) /\ ((exists ge_balance_positive_iff_prime_secondfirst_divisorproductsecondreal ge_balance_negative_iff_prime_secondfirst_divisorproductsecondreal. (((((ge_representation_real_code_iff_prime_secondfirst_divisorproductsecond) = 2 * (ge_balance_positive_iff_prime_secondfirst_divisorproductsecondreal) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_iff_prime_secondfirst_divisorproductsecondrealdecode. (((ge_representation_real_code_iff_prime_secondfirst_divisorproductsecond) = 2 * ge_signed_half_iff_prime_secondfirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondfirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductsecondreal) = S ge_signed_half_iff_prime_secondfirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_iff_prime_secondfirst_divisorproduct) + ge_balance_negative_iff_prime_secondfirst_divisorproductsecondreal = (ge_second_rn_iff_prime_secondfirst_divisorproduct) + ge_balance_positive_iff_prime_secondfirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_iff_prime_secondfirst_divisorproductsecondimaginary ge_balance_negative_iff_prime_secondfirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductsecond) = 2 * (ge_balance_positive_iff_prime_secondfirst_divisorproductsecondimaginary) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondfirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductsecond) = 2 * ge_signed_half_iff_prime_secondfirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondfirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductsecondimaginary) = S ge_signed_half_iff_prime_secondfirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_secondfirst_divisorproduct) + ge_balance_negative_iff_prime_secondfirst_divisorproductsecondimaginary = (ge_second_in_iff_prime_secondfirst_divisorproduct) + ge_balance_positive_iff_prime_secondfirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_secondfirst_divisorproductoutput ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductoutput. (((gr_first_factor_iff_prime_second) = ((ge_representation_real_code_iff_prime_secondfirst_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductoutput)) * S ((ge_representation_real_code_iff_prime_secondfirst_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductoutput)) + ((ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductoutput))) /\ ((exists ge_balance_positive_iff_prime_secondfirst_divisorproductoutputreal ge_balance_negative_iff_prime_secondfirst_divisorproductoutputreal. (((((ge_representation_real_code_iff_prime_secondfirst_divisorproductoutput) = 2 * (ge_balance_positive_iff_prime_secondfirst_divisorproductoutputreal) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_iff_prime_secondfirst_divisorproductoutputrealdecode. (((ge_representation_real_code_iff_prime_secondfirst_divisorproductoutput) = 2 * ge_signed_half_iff_prime_secondfirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondfirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductoutputreal) = S ge_signed_half_iff_prime_secondfirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_secondfirst_divisorproduct) * (ge_second_rp_iff_prime_secondfirst_divisorproduct))) + (((ge_first_rn_iff_prime_secondfirst_divisorproduct) * (ge_second_rn_iff_prime_secondfirst_divisorproduct))))) + (((((ge_first_ip_iff_prime_secondfirst_divisorproduct) * (ge_second_in_iff_prime_secondfirst_divisorproduct))) + (((ge_first_in_iff_prime_secondfirst_divisorproduct) * (ge_second_ip_iff_prime_secondfirst_divisorproduct))))))) + ge_balance_negative_iff_prime_secondfirst_divisorproductoutputreal = (((((((ge_first_rp_iff_prime_secondfirst_divisorproduct) * (ge_second_rn_iff_prime_secondfirst_divisorproduct))) + (((ge_first_rn_iff_prime_secondfirst_divisorproduct) * (ge_second_rp_iff_prime_secondfirst_divisorproduct))))) + (((((ge_first_ip_iff_prime_secondfirst_divisorproduct) * (ge_second_ip_iff_prime_secondfirst_divisorproduct))) + (((ge_first_in_iff_prime_secondfirst_divisorproduct) * (ge_second_in_iff_prime_secondfirst_divisorproduct))))))) + ge_balance_positive_iff_prime_secondfirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_iff_prime_secondfirst_divisorproductoutputimaginary ge_balance_negative_iff_prime_secondfirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductoutput) = 2 * (ge_balance_positive_iff_prime_secondfirst_divisorproductoutputimaginary) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondfirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondfirst_divisorproductoutput) = 2 * ge_signed_half_iff_prime_secondfirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondfirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondfirst_divisorproductoutputimaginary) = S ge_signed_half_iff_prime_secondfirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_secondfirst_divisorproduct) * (ge_second_ip_iff_prime_secondfirst_divisorproduct))) + (((ge_first_rn_iff_prime_secondfirst_divisorproduct) * (ge_second_in_iff_prime_secondfirst_divisorproduct))))) + (((((ge_first_ip_iff_prime_secondfirst_divisorproduct) * (ge_second_rp_iff_prime_secondfirst_divisorproduct))) + (((ge_first_in_iff_prime_secondfirst_divisorproduct) * (ge_second_rn_iff_prime_secondfirst_divisorproduct))))))) + ge_balance_negative_iff_prime_secondfirst_divisorproductoutputimaginary = (((((((ge_first_rp_iff_prime_secondfirst_divisorproduct) * (ge_second_in_iff_prime_secondfirst_divisorproduct))) + (((ge_first_rn_iff_prime_secondfirst_divisorproduct) * (ge_second_ip_iff_prime_secondfirst_divisorproduct))))) + (((((ge_first_ip_iff_prime_secondfirst_divisorproduct) * (ge_second_rn_iff_prime_secondfirst_divisorproduct))) + (((ge_first_in_iff_prime_secondfirst_divisorproduct) * (ge_second_rp_iff_prime_secondfirst_divisorproduct))))))) + ge_balance_positive_iff_prime_secondfirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_iff_prime_secondsecond_divisor. (exists ge_first_rp_iff_prime_secondsecond_divisorproduct ge_first_rn_iff_prime_secondsecond_divisorproduct ge_first_ip_iff_prime_secondsecond_divisorproduct ge_first_in_iff_prime_secondsecond_divisorproduct ge_second_rp_iff_prime_secondsecond_divisorproduct ge_second_rn_iff_prime_secondsecond_divisorproduct ge_second_ip_iff_prime_secondsecond_divisorproduct ge_second_in_iff_prime_secondsecond_divisorproduct. ((exists ge_representation_real_code_iff_prime_secondsecond_divisorproductfirst ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductfirst. (((p) = ((ge_representation_real_code_iff_prime_secondsecond_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductfirst)) * S ((ge_representation_real_code_iff_prime_secondsecond_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductfirst)) + ((ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductfirst) + (ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductfirst))) /\ ((exists ge_balance_positive_iff_prime_secondsecond_divisorproductfirstreal ge_balance_negative_iff_prime_secondsecond_divisorproductfirstreal. (((((ge_representation_real_code_iff_prime_secondsecond_divisorproductfirst) = 2 * (ge_balance_positive_iff_prime_secondsecond_divisorproductfirstreal) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_iff_prime_secondsecond_divisorproductfirstrealdecode. (((ge_representation_real_code_iff_prime_secondsecond_divisorproductfirst) = 2 * ge_signed_half_iff_prime_secondsecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondsecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductfirstreal) = S ge_signed_half_iff_prime_secondsecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_iff_prime_secondsecond_divisorproduct) + ge_balance_negative_iff_prime_secondsecond_divisorproductfirstreal = (ge_first_rn_iff_prime_secondsecond_divisorproduct) + ge_balance_positive_iff_prime_secondsecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_iff_prime_secondsecond_divisorproductfirstimaginary ge_balance_negative_iff_prime_secondsecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductfirst) = 2 * (ge_balance_positive_iff_prime_secondsecond_divisorproductfirstimaginary) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondsecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductfirst) = 2 * ge_signed_half_iff_prime_secondsecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondsecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductfirstimaginary) = S ge_signed_half_iff_prime_secondsecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_iff_prime_secondsecond_divisorproduct) + ge_balance_negative_iff_prime_secondsecond_divisorproductfirstimaginary = (ge_first_in_iff_prime_secondsecond_divisorproduct) + ge_balance_positive_iff_prime_secondsecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_prime_secondsecond_divisorproductsecond ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductsecond. (((gr_quotient_iff_prime_secondsecond_divisor) = ((ge_representation_real_code_iff_prime_secondsecond_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductsecond)) * S ((ge_representation_real_code_iff_prime_secondsecond_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductsecond)) + ((ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductsecond) + (ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductsecond))) /\ ((exists ge_balance_positive_iff_prime_secondsecond_divisorproductsecondreal ge_balance_negative_iff_prime_secondsecond_divisorproductsecondreal. (((((ge_representation_real_code_iff_prime_secondsecond_divisorproductsecond) = 2 * (ge_balance_positive_iff_prime_secondsecond_divisorproductsecondreal) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_iff_prime_secondsecond_divisorproductsecondrealdecode. (((ge_representation_real_code_iff_prime_secondsecond_divisorproductsecond) = 2 * ge_signed_half_iff_prime_secondsecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondsecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductsecondreal) = S ge_signed_half_iff_prime_secondsecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_iff_prime_secondsecond_divisorproduct) + ge_balance_negative_iff_prime_secondsecond_divisorproductsecondreal = (ge_second_rn_iff_prime_secondsecond_divisorproduct) + ge_balance_positive_iff_prime_secondsecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_iff_prime_secondsecond_divisorproductsecondimaginary ge_balance_negative_iff_prime_secondsecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductsecond) = 2 * (ge_balance_positive_iff_prime_secondsecond_divisorproductsecondimaginary) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondsecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductsecond) = 2 * ge_signed_half_iff_prime_secondsecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondsecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductsecondimaginary) = S ge_signed_half_iff_prime_secondsecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_iff_prime_secondsecond_divisorproduct) + ge_balance_negative_iff_prime_secondsecond_divisorproductsecondimaginary = (ge_second_in_iff_prime_secondsecond_divisorproduct) + ge_balance_positive_iff_prime_secondsecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_prime_secondsecond_divisorproductoutput ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductoutput. (((gr_second_factor_iff_prime_second) = ((ge_representation_real_code_iff_prime_secondsecond_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductoutput)) * S ((ge_representation_real_code_iff_prime_secondsecond_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductoutput)) + ((ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductoutput) + (ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductoutput))) /\ ((exists ge_balance_positive_iff_prime_secondsecond_divisorproductoutputreal ge_balance_negative_iff_prime_secondsecond_divisorproductoutputreal. (((((ge_representation_real_code_iff_prime_secondsecond_divisorproductoutput) = 2 * (ge_balance_positive_iff_prime_secondsecond_divisorproductoutputreal) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_iff_prime_secondsecond_divisorproductoutputrealdecode. (((ge_representation_real_code_iff_prime_secondsecond_divisorproductoutput) = 2 * ge_signed_half_iff_prime_secondsecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_iff_prime_secondsecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductoutputreal) = S ge_signed_half_iff_prime_secondsecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_iff_prime_secondsecond_divisorproduct) * (ge_second_rp_iff_prime_secondsecond_divisorproduct))) + (((ge_first_rn_iff_prime_secondsecond_divisorproduct) * (ge_second_rn_iff_prime_secondsecond_divisorproduct))))) + (((((ge_first_ip_iff_prime_secondsecond_divisorproduct) * (ge_second_in_iff_prime_secondsecond_divisorproduct))) + (((ge_first_in_iff_prime_secondsecond_divisorproduct) * (ge_second_ip_iff_prime_secondsecond_divisorproduct))))))) + ge_balance_negative_iff_prime_secondsecond_divisorproductoutputreal = (((((((ge_first_rp_iff_prime_secondsecond_divisorproduct) * (ge_second_rn_iff_prime_secondsecond_divisorproduct))) + (((ge_first_rn_iff_prime_secondsecond_divisorproduct) * (ge_second_rp_iff_prime_secondsecond_divisorproduct))))) + (((((ge_first_ip_iff_prime_secondsecond_divisorproduct) * (ge_second_ip_iff_prime_secondsecond_divisorproduct))) + (((ge_first_in_iff_prime_secondsecond_divisorproduct) * (ge_second_in_iff_prime_secondsecond_divisorproduct))))))) + ge_balance_positive_iff_prime_secondsecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_iff_prime_secondsecond_divisorproductoutputimaginary ge_balance_negative_iff_prime_secondsecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductoutput) = 2 * (ge_balance_positive_iff_prime_secondsecond_divisorproductoutputimaginary) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_iff_prime_secondsecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_iff_prime_secondsecond_divisorproductoutput) = 2 * ge_signed_half_iff_prime_secondsecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_prime_secondsecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_iff_prime_secondsecond_divisorproductoutputimaginary) = S ge_signed_half_iff_prime_secondsecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_prime_secondsecond_divisorproduct) * (ge_second_ip_iff_prime_secondsecond_divisorproduct))) + (((ge_first_rn_iff_prime_secondsecond_divisorproduct) * (ge_second_in_iff_prime_secondsecond_divisorproduct))))) + (((((ge_first_ip_iff_prime_secondsecond_divisorproduct) * (ge_second_rp_iff_prime_secondsecond_divisorproduct))) + (((ge_first_in_iff_prime_secondsecond_divisorproduct) * (ge_second_rn_iff_prime_secondsecond_divisorproduct))))))) + ge_balance_negative_iff_prime_secondsecond_divisorproductoutputimaginary = (((((((ge_first_rp_iff_prime_secondsecond_divisorproduct) * (ge_second_in_iff_prime_secondsecond_divisorproduct))) + (((ge_first_rn_iff_prime_secondsecond_divisorproduct) * (ge_second_ip_iff_prime_secondsecond_divisorproduct))))) + (((((ge_first_ip_iff_prime_secondsecond_divisorproduct) * (ge_second_rn_iff_prime_secondsecond_divisorproduct))) + (((ge_first_in_iff_prime_secondsecond_divisorproduct) * (ge_second_rp_iff_prime_secondsecond_divisorproduct))))))) + ge_balance_positive_iff_prime_secondsecond_divisorproductoutputimaginary))))))))))))))) -> (((exists ge_real_positive_iff_irreducible_secondcarrier ge_real_negative_iff_irreducible_secondcarrier ge_imaginary_positive_iff_irreducible_secondcarrier ge_imaginary_negative_iff_irreducible_secondcarrier. (exists ge_real_code_iff_irreducible_secondcarrierdecode ge_imaginary_code_iff_irreducible_secondcarrierdecode. (((p) = ((ge_real_code_iff_irreducible_secondcarrierdecode) + (ge_imaginary_code_iff_irreducible_secondcarrierdecode)) * S ((ge_real_code_iff_irreducible_secondcarrierdecode) + (ge_imaginary_code_iff_irreducible_secondcarrierdecode)) + ((ge_imaginary_code_iff_irreducible_secondcarrierdecode) + (ge_imaginary_code_iff_irreducible_secondcarrierdecode))) /\ (((((ge_real_code_iff_irreducible_secondcarrierdecode) = 2 * (ge_real_positive_iff_irreducible_secondcarrier) /\ (ge_real_negative_iff_irreducible_secondcarrier) = 0) \/ exists ge_signed_half_ge_iff_irreducible_secondcarrierdecode_real. (((ge_real_code_iff_irreducible_secondcarrierdecode) = 2 * ge_signed_half_ge_iff_irreducible_secondcarrierdecode_real + 1 /\ (ge_real_positive_iff_irreducible_secondcarrier) = 0) /\ (ge_real_negative_iff_irreducible_secondcarrier) = S ge_signed_half_ge_iff_irreducible_secondcarrierdecode_real))) /\ ((((ge_imaginary_code_iff_irreducible_secondcarrierdecode) = 2 * (ge_imaginary_positive_iff_irreducible_secondcarrier) /\ (ge_imaginary_negative_iff_irreducible_secondcarrier) = 0) \/ exists ge_signed_half_ge_iff_irreducible_secondcarrierdecode_imaginary. (((ge_imaginary_code_iff_irreducible_secondcarrierdecode) = 2 * ge_signed_half_ge_iff_irreducible_secondcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_iff_irreducible_secondcarrier) = 0) /\ (ge_imaginary_negative_iff_irreducible_secondcarrier) = S ge_signed_half_ge_iff_irreducible_secondcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_iff_irreducible_secondnonunit. (exists ge_first_rp_iff_irreducible_secondnonunitidentity ge_first_rn_iff_irreducible_secondnonunitidentity ge_first_ip_iff_irreducible_secondnonunitidentity ge_first_in_iff_irreducible_secondnonunitidentity ge_second_rp_iff_irreducible_secondnonunitidentity ge_second_rn_iff_irreducible_secondnonunitidentity ge_second_ip_iff_irreducible_secondnonunitidentity ge_second_in_iff_irreducible_secondnonunitidentity. ((exists ge_representation_real_code_iff_irreducible_secondnonunitidentityfirst ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityfirst. (((p) = ((ge_representation_real_code_iff_irreducible_secondnonunitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityfirst)) * S ((ge_representation_real_code_iff_irreducible_secondnonunitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityfirst)) + ((ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityfirst))) /\ ((exists ge_balance_positive_iff_irreducible_secondnonunitidentityfirstreal ge_balance_negative_iff_irreducible_secondnonunitidentityfirstreal. (((((ge_representation_real_code_iff_irreducible_secondnonunitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_secondnonunitidentityfirstreal) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondnonunitidentityfirstrealdecode. (((ge_representation_real_code_iff_irreducible_secondnonunitidentityfirst) = 2 * ge_signed_half_iff_irreducible_secondnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentityfirstreal) = S ge_signed_half_iff_irreducible_secondnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_iff_irreducible_secondnonunitidentity) + ge_balance_negative_iff_irreducible_secondnonunitidentityfirstreal = (ge_first_rn_iff_irreducible_secondnonunitidentity) + ge_balance_positive_iff_irreducible_secondnonunitidentityfirstreal))) /\ (exists ge_balance_positive_iff_irreducible_secondnonunitidentityfirstimaginary ge_balance_negative_iff_irreducible_secondnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_secondnonunitidentityfirstimaginary) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityfirst) = 2 * ge_signed_half_iff_irreducible_secondnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentityfirstimaginary) = S ge_signed_half_iff_irreducible_secondnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_iff_irreducible_secondnonunitidentity) + ge_balance_negative_iff_irreducible_secondnonunitidentityfirstimaginary = (ge_first_in_iff_irreducible_secondnonunitidentity) + ge_balance_positive_iff_irreducible_secondnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_irreducible_secondnonunitidentitysecond ge_representation_imaginary_code_iff_irreducible_secondnonunitidentitysecond. (((gr_inverse_iff_irreducible_secondnonunit) = ((ge_representation_real_code_iff_irreducible_secondnonunitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_secondnonunitidentitysecond)) * S ((ge_representation_real_code_iff_irreducible_secondnonunitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_secondnonunitidentitysecond)) + ((ge_representation_imaginary_code_iff_irreducible_secondnonunitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_secondnonunitidentitysecond))) /\ ((exists ge_balance_positive_iff_irreducible_secondnonunitidentitysecondreal ge_balance_negative_iff_irreducible_secondnonunitidentitysecondreal. (((((ge_representation_real_code_iff_irreducible_secondnonunitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_secondnonunitidentitysecondreal) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondnonunitidentitysecondrealdecode. (((ge_representation_real_code_iff_irreducible_secondnonunitidentitysecond) = 2 * ge_signed_half_iff_irreducible_secondnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentitysecondreal) = S ge_signed_half_iff_irreducible_secondnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_iff_irreducible_secondnonunitidentity) + ge_balance_negative_iff_irreducible_secondnonunitidentitysecondreal = (ge_second_rn_iff_irreducible_secondnonunitidentity) + ge_balance_positive_iff_irreducible_secondnonunitidentitysecondreal))) /\ (exists ge_balance_positive_iff_irreducible_secondnonunitidentitysecondimaginary ge_balance_negative_iff_irreducible_secondnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondnonunitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_secondnonunitidentitysecondimaginary) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondnonunitidentitysecond) = 2 * ge_signed_half_iff_irreducible_secondnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentitysecondimaginary) = S ge_signed_half_iff_irreducible_secondnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_iff_irreducible_secondnonunitidentity) + ge_balance_negative_iff_irreducible_secondnonunitidentitysecondimaginary = (ge_second_in_iff_irreducible_secondnonunitidentity) + ge_balance_positive_iff_irreducible_secondnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_iff_irreducible_secondnonunitidentityoutput ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityoutput. (((6) = ((ge_representation_real_code_iff_irreducible_secondnonunitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityoutput)) * S ((ge_representation_real_code_iff_irreducible_secondnonunitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityoutput)) + ((ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityoutput))) /\ ((exists ge_balance_positive_iff_irreducible_secondnonunitidentityoutputreal ge_balance_negative_iff_irreducible_secondnonunitidentityoutputreal. (((((ge_representation_real_code_iff_irreducible_secondnonunitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_secondnonunitidentityoutputreal) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondnonunitidentityoutputrealdecode. (((ge_representation_real_code_iff_irreducible_secondnonunitidentityoutput) = 2 * ge_signed_half_iff_irreducible_secondnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentityoutputreal) = S ge_signed_half_iff_irreducible_secondnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_iff_irreducible_secondnonunitidentity) * (ge_second_rp_iff_irreducible_secondnonunitidentity))) + (((ge_first_rn_iff_irreducible_secondnonunitidentity) * (ge_second_rn_iff_irreducible_secondnonunitidentity))))) + (((((ge_first_ip_iff_irreducible_secondnonunitidentity) * (ge_second_in_iff_irreducible_secondnonunitidentity))) + (((ge_first_in_iff_irreducible_secondnonunitidentity) * (ge_second_ip_iff_irreducible_secondnonunitidentity))))))) + ge_balance_negative_iff_irreducible_secondnonunitidentityoutputreal = (((((((ge_first_rp_iff_irreducible_secondnonunitidentity) * (ge_second_rn_iff_irreducible_secondnonunitidentity))) + (((ge_first_rn_iff_irreducible_secondnonunitidentity) * (ge_second_rp_iff_irreducible_secondnonunitidentity))))) + (((((ge_first_ip_iff_irreducible_secondnonunitidentity) * (ge_second_ip_iff_irreducible_secondnonunitidentity))) + (((ge_first_in_iff_irreducible_secondnonunitidentity) * (ge_second_in_iff_irreducible_secondnonunitidentity))))))) + ge_balance_positive_iff_irreducible_secondnonunitidentityoutputreal))) /\ (exists ge_balance_positive_iff_irreducible_secondnonunitidentityoutputimaginary ge_balance_negative_iff_irreducible_secondnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_secondnonunitidentityoutputimaginary) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondnonunitidentityoutput) = 2 * ge_signed_half_iff_irreducible_secondnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondnonunitidentityoutputimaginary) = S ge_signed_half_iff_irreducible_secondnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_irreducible_secondnonunitidentity) * (ge_second_ip_iff_irreducible_secondnonunitidentity))) + (((ge_first_rn_iff_irreducible_secondnonunitidentity) * (ge_second_in_iff_irreducible_secondnonunitidentity))))) + (((((ge_first_ip_iff_irreducible_secondnonunitidentity) * (ge_second_rp_iff_irreducible_secondnonunitidentity))) + (((ge_first_in_iff_irreducible_secondnonunitidentity) * (ge_second_rn_iff_irreducible_secondnonunitidentity))))))) + ge_balance_negative_iff_irreducible_secondnonunitidentityoutputimaginary = (((((((ge_first_rp_iff_irreducible_secondnonunitidentity) * (ge_second_in_iff_irreducible_secondnonunitidentity))) + (((ge_first_rn_iff_irreducible_secondnonunitidentity) * (ge_second_ip_iff_irreducible_secondnonunitidentity))))) + (((((ge_first_ip_iff_irreducible_secondnonunitidentity) * (ge_second_rn_iff_irreducible_secondnonunitidentity))) + (((ge_first_in_iff_irreducible_secondnonunitidentity) * (ge_second_rp_iff_irreducible_secondnonunitidentity))))))) + ge_balance_positive_iff_irreducible_secondnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_iff_irreducible_second gr_second_factor_iff_irreducible_second. (exists ge_first_rp_iff_irreducible_secondfactorization ge_first_rn_iff_irreducible_secondfactorization ge_first_ip_iff_irreducible_secondfactorization ge_first_in_iff_irreducible_secondfactorization ge_second_rp_iff_irreducible_secondfactorization ge_second_rn_iff_irreducible_secondfactorization ge_second_ip_iff_irreducible_secondfactorization ge_second_in_iff_irreducible_secondfactorization. ((exists ge_representation_real_code_iff_irreducible_secondfactorizationfirst ge_representation_imaginary_code_iff_irreducible_secondfactorizationfirst. (((gr_first_factor_iff_irreducible_second) = ((ge_representation_real_code_iff_irreducible_secondfactorizationfirst) + (ge_representation_imaginary_code_iff_irreducible_secondfactorizationfirst)) * S ((ge_representation_real_code_iff_irreducible_secondfactorizationfirst) + (ge_representation_imaginary_code_iff_irreducible_secondfactorizationfirst)) + ((ge_representation_imaginary_code_iff_irreducible_secondfactorizationfirst) + (ge_representation_imaginary_code_iff_irreducible_secondfactorizationfirst))) /\ ((exists ge_balance_positive_iff_irreducible_secondfactorizationfirstreal ge_balance_negative_iff_irreducible_secondfactorizationfirstreal. (((((ge_representation_real_code_iff_irreducible_secondfactorizationfirst) = 2 * (ge_balance_positive_iff_irreducible_secondfactorizationfirstreal) /\ (ge_balance_negative_iff_irreducible_secondfactorizationfirstreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondfactorizationfirstrealdecode. (((ge_representation_real_code_iff_irreducible_secondfactorizationfirst) = 2 * ge_signed_half_iff_irreducible_secondfactorizationfirstrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfactorizationfirstreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondfactorizationfirstreal) = S ge_signed_half_iff_irreducible_secondfactorizationfirstrealdecode))) /\ ((ge_first_rp_iff_irreducible_secondfactorization) + ge_balance_negative_iff_irreducible_secondfactorizationfirstreal = (ge_first_rn_iff_irreducible_secondfactorization) + ge_balance_positive_iff_irreducible_secondfactorizationfirstreal))) /\ (exists ge_balance_positive_iff_irreducible_secondfactorizationfirstimaginary ge_balance_negative_iff_irreducible_secondfactorizationfirstimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondfactorizationfirst) = 2 * (ge_balance_positive_iff_irreducible_secondfactorizationfirstimaginary) /\ (ge_balance_negative_iff_irreducible_secondfactorizationfirstimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondfactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondfactorizationfirst) = 2 * ge_signed_half_iff_irreducible_secondfactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfactorizationfirstimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondfactorizationfirstimaginary) = S ge_signed_half_iff_irreducible_secondfactorizationfirstimaginarydecode))) /\ ((ge_first_ip_iff_irreducible_secondfactorization) + ge_balance_negative_iff_irreducible_secondfactorizationfirstimaginary = (ge_first_in_iff_irreducible_secondfactorization) + ge_balance_positive_iff_irreducible_secondfactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_irreducible_secondfactorizationsecond ge_representation_imaginary_code_iff_irreducible_secondfactorizationsecond. (((gr_second_factor_iff_irreducible_second) = ((ge_representation_real_code_iff_irreducible_secondfactorizationsecond) + (ge_representation_imaginary_code_iff_irreducible_secondfactorizationsecond)) * S ((ge_representation_real_code_iff_irreducible_secondfactorizationsecond) + (ge_representation_imaginary_code_iff_irreducible_secondfactorizationsecond)) + ((ge_representation_imaginary_code_iff_irreducible_secondfactorizationsecond) + (ge_representation_imaginary_code_iff_irreducible_secondfactorizationsecond))) /\ ((exists ge_balance_positive_iff_irreducible_secondfactorizationsecondreal ge_balance_negative_iff_irreducible_secondfactorizationsecondreal. (((((ge_representation_real_code_iff_irreducible_secondfactorizationsecond) = 2 * (ge_balance_positive_iff_irreducible_secondfactorizationsecondreal) /\ (ge_balance_negative_iff_irreducible_secondfactorizationsecondreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondfactorizationsecondrealdecode. (((ge_representation_real_code_iff_irreducible_secondfactorizationsecond) = 2 * ge_signed_half_iff_irreducible_secondfactorizationsecondrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfactorizationsecondreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondfactorizationsecondreal) = S ge_signed_half_iff_irreducible_secondfactorizationsecondrealdecode))) /\ ((ge_second_rp_iff_irreducible_secondfactorization) + ge_balance_negative_iff_irreducible_secondfactorizationsecondreal = (ge_second_rn_iff_irreducible_secondfactorization) + ge_balance_positive_iff_irreducible_secondfactorizationsecondreal))) /\ (exists ge_balance_positive_iff_irreducible_secondfactorizationsecondimaginary ge_balance_negative_iff_irreducible_secondfactorizationsecondimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondfactorizationsecond) = 2 * (ge_balance_positive_iff_irreducible_secondfactorizationsecondimaginary) /\ (ge_balance_negative_iff_irreducible_secondfactorizationsecondimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondfactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondfactorizationsecond) = 2 * ge_signed_half_iff_irreducible_secondfactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfactorizationsecondimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondfactorizationsecondimaginary) = S ge_signed_half_iff_irreducible_secondfactorizationsecondimaginarydecode))) /\ ((ge_second_ip_iff_irreducible_secondfactorization) + ge_balance_negative_iff_irreducible_secondfactorizationsecondimaginary = (ge_second_in_iff_irreducible_secondfactorization) + ge_balance_positive_iff_irreducible_secondfactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_iff_irreducible_secondfactorizationoutput ge_representation_imaginary_code_iff_irreducible_secondfactorizationoutput. (((p) = ((ge_representation_real_code_iff_irreducible_secondfactorizationoutput) + (ge_representation_imaginary_code_iff_irreducible_secondfactorizationoutput)) * S ((ge_representation_real_code_iff_irreducible_secondfactorizationoutput) + (ge_representation_imaginary_code_iff_irreducible_secondfactorizationoutput)) + ((ge_representation_imaginary_code_iff_irreducible_secondfactorizationoutput) + (ge_representation_imaginary_code_iff_irreducible_secondfactorizationoutput))) /\ ((exists ge_balance_positive_iff_irreducible_secondfactorizationoutputreal ge_balance_negative_iff_irreducible_secondfactorizationoutputreal. (((((ge_representation_real_code_iff_irreducible_secondfactorizationoutput) = 2 * (ge_balance_positive_iff_irreducible_secondfactorizationoutputreal) /\ (ge_balance_negative_iff_irreducible_secondfactorizationoutputreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondfactorizationoutputrealdecode. (((ge_representation_real_code_iff_irreducible_secondfactorizationoutput) = 2 * ge_signed_half_iff_irreducible_secondfactorizationoutputrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfactorizationoutputreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondfactorizationoutputreal) = S ge_signed_half_iff_irreducible_secondfactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_iff_irreducible_secondfactorization) * (ge_second_rp_iff_irreducible_secondfactorization))) + (((ge_first_rn_iff_irreducible_secondfactorization) * (ge_second_rn_iff_irreducible_secondfactorization))))) + (((((ge_first_ip_iff_irreducible_secondfactorization) * (ge_second_in_iff_irreducible_secondfactorization))) + (((ge_first_in_iff_irreducible_secondfactorization) * (ge_second_ip_iff_irreducible_secondfactorization))))))) + ge_balance_negative_iff_irreducible_secondfactorizationoutputreal = (((((((ge_first_rp_iff_irreducible_secondfactorization) * (ge_second_rn_iff_irreducible_secondfactorization))) + (((ge_first_rn_iff_irreducible_secondfactorization) * (ge_second_rp_iff_irreducible_secondfactorization))))) + (((((ge_first_ip_iff_irreducible_secondfactorization) * (ge_second_ip_iff_irreducible_secondfactorization))) + (((ge_first_in_iff_irreducible_secondfactorization) * (ge_second_in_iff_irreducible_secondfactorization))))))) + ge_balance_positive_iff_irreducible_secondfactorizationoutputreal))) /\ (exists ge_balance_positive_iff_irreducible_secondfactorizationoutputimaginary ge_balance_negative_iff_irreducible_secondfactorizationoutputimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondfactorizationoutput) = 2 * (ge_balance_positive_iff_irreducible_secondfactorizationoutputimaginary) /\ (ge_balance_negative_iff_irreducible_secondfactorizationoutputimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondfactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondfactorizationoutput) = 2 * ge_signed_half_iff_irreducible_secondfactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfactorizationoutputimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondfactorizationoutputimaginary) = S ge_signed_half_iff_irreducible_secondfactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_irreducible_secondfactorization) * (ge_second_ip_iff_irreducible_secondfactorization))) + (((ge_first_rn_iff_irreducible_secondfactorization) * (ge_second_in_iff_irreducible_secondfactorization))))) + (((((ge_first_ip_iff_irreducible_secondfactorization) * (ge_second_rp_iff_irreducible_secondfactorization))) + (((ge_first_in_iff_irreducible_secondfactorization) * (ge_second_rn_iff_irreducible_secondfactorization))))))) + ge_balance_negative_iff_irreducible_secondfactorizationoutputimaginary = (((((((ge_first_rp_iff_irreducible_secondfactorization) * (ge_second_in_iff_irreducible_secondfactorization))) + (((ge_first_rn_iff_irreducible_secondfactorization) * (ge_second_ip_iff_irreducible_secondfactorization))))) + (((((ge_first_ip_iff_irreducible_secondfactorization) * (ge_second_rn_iff_irreducible_secondfactorization))) + (((ge_first_in_iff_irreducible_secondfactorization) * (ge_second_rp_iff_irreducible_secondfactorization))))))) + ge_balance_positive_iff_irreducible_secondfactorizationoutputimaginary))))))))) -> (exists gr_inverse_iff_irreducible_secondfirst_unit. (exists ge_first_rp_iff_irreducible_secondfirst_unitidentity ge_first_rn_iff_irreducible_secondfirst_unitidentity ge_first_ip_iff_irreducible_secondfirst_unitidentity ge_first_in_iff_irreducible_secondfirst_unitidentity ge_second_rp_iff_irreducible_secondfirst_unitidentity ge_second_rn_iff_irreducible_secondfirst_unitidentity ge_second_ip_iff_irreducible_secondfirst_unitidentity ge_second_in_iff_irreducible_secondfirst_unitidentity. ((exists ge_representation_real_code_iff_irreducible_secondfirst_unitidentityfirst ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityfirst. (((gr_first_factor_iff_irreducible_second) = ((ge_representation_real_code_iff_irreducible_secondfirst_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityfirst)) * S ((ge_representation_real_code_iff_irreducible_secondfirst_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityfirst)) + ((ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityfirst))) /\ ((exists ge_balance_positive_iff_irreducible_secondfirst_unitidentityfirstreal ge_balance_negative_iff_irreducible_secondfirst_unitidentityfirstreal. (((((ge_representation_real_code_iff_irreducible_secondfirst_unitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_secondfirst_unitidentityfirstreal) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondfirst_unitidentityfirstrealdecode. (((ge_representation_real_code_iff_irreducible_secondfirst_unitidentityfirst) = 2 * ge_signed_half_iff_irreducible_secondfirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentityfirstreal) = S ge_signed_half_iff_irreducible_secondfirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_iff_irreducible_secondfirst_unitidentity) + ge_balance_negative_iff_irreducible_secondfirst_unitidentityfirstreal = (ge_first_rn_iff_irreducible_secondfirst_unitidentity) + ge_balance_positive_iff_irreducible_secondfirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_iff_irreducible_secondfirst_unitidentityfirstimaginary ge_balance_negative_iff_irreducible_secondfirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_secondfirst_unitidentityfirstimaginary) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondfirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityfirst) = 2 * ge_signed_half_iff_irreducible_secondfirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentityfirstimaginary) = S ge_signed_half_iff_irreducible_secondfirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_iff_irreducible_secondfirst_unitidentity) + ge_balance_negative_iff_irreducible_secondfirst_unitidentityfirstimaginary = (ge_first_in_iff_irreducible_secondfirst_unitidentity) + ge_balance_positive_iff_irreducible_secondfirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_irreducible_secondfirst_unitidentitysecond ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentitysecond. (((gr_inverse_iff_irreducible_secondfirst_unit) = ((ge_representation_real_code_iff_irreducible_secondfirst_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentitysecond)) * S ((ge_representation_real_code_iff_irreducible_secondfirst_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentitysecond)) + ((ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentitysecond))) /\ ((exists ge_balance_positive_iff_irreducible_secondfirst_unitidentitysecondreal ge_balance_negative_iff_irreducible_secondfirst_unitidentitysecondreal. (((((ge_representation_real_code_iff_irreducible_secondfirst_unitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_secondfirst_unitidentitysecondreal) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondfirst_unitidentitysecondrealdecode. (((ge_representation_real_code_iff_irreducible_secondfirst_unitidentitysecond) = 2 * ge_signed_half_iff_irreducible_secondfirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentitysecondreal) = S ge_signed_half_iff_irreducible_secondfirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_iff_irreducible_secondfirst_unitidentity) + ge_balance_negative_iff_irreducible_secondfirst_unitidentitysecondreal = (ge_second_rn_iff_irreducible_secondfirst_unitidentity) + ge_balance_positive_iff_irreducible_secondfirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_iff_irreducible_secondfirst_unitidentitysecondimaginary ge_balance_negative_iff_irreducible_secondfirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_secondfirst_unitidentitysecondimaginary) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondfirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentitysecond) = 2 * ge_signed_half_iff_irreducible_secondfirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentitysecondimaginary) = S ge_signed_half_iff_irreducible_secondfirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_iff_irreducible_secondfirst_unitidentity) + ge_balance_negative_iff_irreducible_secondfirst_unitidentitysecondimaginary = (ge_second_in_iff_irreducible_secondfirst_unitidentity) + ge_balance_positive_iff_irreducible_secondfirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_iff_irreducible_secondfirst_unitidentityoutput ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityoutput. (((6) = ((ge_representation_real_code_iff_irreducible_secondfirst_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityoutput)) * S ((ge_representation_real_code_iff_irreducible_secondfirst_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityoutput)) + ((ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityoutput))) /\ ((exists ge_balance_positive_iff_irreducible_secondfirst_unitidentityoutputreal ge_balance_negative_iff_irreducible_secondfirst_unitidentityoutputreal. (((((ge_representation_real_code_iff_irreducible_secondfirst_unitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_secondfirst_unitidentityoutputreal) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondfirst_unitidentityoutputrealdecode. (((ge_representation_real_code_iff_irreducible_secondfirst_unitidentityoutput) = 2 * ge_signed_half_iff_irreducible_secondfirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentityoutputreal) = S ge_signed_half_iff_irreducible_secondfirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_iff_irreducible_secondfirst_unitidentity) * (ge_second_rp_iff_irreducible_secondfirst_unitidentity))) + (((ge_first_rn_iff_irreducible_secondfirst_unitidentity) * (ge_second_rn_iff_irreducible_secondfirst_unitidentity))))) + (((((ge_first_ip_iff_irreducible_secondfirst_unitidentity) * (ge_second_in_iff_irreducible_secondfirst_unitidentity))) + (((ge_first_in_iff_irreducible_secondfirst_unitidentity) * (ge_second_ip_iff_irreducible_secondfirst_unitidentity))))))) + ge_balance_negative_iff_irreducible_secondfirst_unitidentityoutputreal = (((((((ge_first_rp_iff_irreducible_secondfirst_unitidentity) * (ge_second_rn_iff_irreducible_secondfirst_unitidentity))) + (((ge_first_rn_iff_irreducible_secondfirst_unitidentity) * (ge_second_rp_iff_irreducible_secondfirst_unitidentity))))) + (((((ge_first_ip_iff_irreducible_secondfirst_unitidentity) * (ge_second_ip_iff_irreducible_secondfirst_unitidentity))) + (((ge_first_in_iff_irreducible_secondfirst_unitidentity) * (ge_second_in_iff_irreducible_secondfirst_unitidentity))))))) + ge_balance_positive_iff_irreducible_secondfirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_iff_irreducible_secondfirst_unitidentityoutputimaginary ge_balance_negative_iff_irreducible_secondfirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_secondfirst_unitidentityoutputimaginary) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondfirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondfirst_unitidentityoutput) = 2 * ge_signed_half_iff_irreducible_secondfirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondfirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondfirst_unitidentityoutputimaginary) = S ge_signed_half_iff_irreducible_secondfirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_irreducible_secondfirst_unitidentity) * (ge_second_ip_iff_irreducible_secondfirst_unitidentity))) + (((ge_first_rn_iff_irreducible_secondfirst_unitidentity) * (ge_second_in_iff_irreducible_secondfirst_unitidentity))))) + (((((ge_first_ip_iff_irreducible_secondfirst_unitidentity) * (ge_second_rp_iff_irreducible_secondfirst_unitidentity))) + (((ge_first_in_iff_irreducible_secondfirst_unitidentity) * (ge_second_rn_iff_irreducible_secondfirst_unitidentity))))))) + ge_balance_negative_iff_irreducible_secondfirst_unitidentityoutputimaginary = (((((((ge_first_rp_iff_irreducible_secondfirst_unitidentity) * (ge_second_in_iff_irreducible_secondfirst_unitidentity))) + (((ge_first_rn_iff_irreducible_secondfirst_unitidentity) * (ge_second_ip_iff_irreducible_secondfirst_unitidentity))))) + (((((ge_first_ip_iff_irreducible_secondfirst_unitidentity) * (ge_second_rn_iff_irreducible_secondfirst_unitidentity))) + (((ge_first_in_iff_irreducible_secondfirst_unitidentity) * (ge_second_rp_iff_irreducible_secondfirst_unitidentity))))))) + ge_balance_positive_iff_irreducible_secondfirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_iff_irreducible_secondsecond_unit. (exists ge_first_rp_iff_irreducible_secondsecond_unitidentity ge_first_rn_iff_irreducible_secondsecond_unitidentity ge_first_ip_iff_irreducible_secondsecond_unitidentity ge_first_in_iff_irreducible_secondsecond_unitidentity ge_second_rp_iff_irreducible_secondsecond_unitidentity ge_second_rn_iff_irreducible_secondsecond_unitidentity ge_second_ip_iff_irreducible_secondsecond_unitidentity ge_second_in_iff_irreducible_secondsecond_unitidentity. ((exists ge_representation_real_code_iff_irreducible_secondsecond_unitidentityfirst ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityfirst. (((gr_second_factor_iff_irreducible_second) = ((ge_representation_real_code_iff_irreducible_secondsecond_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityfirst)) * S ((ge_representation_real_code_iff_irreducible_secondsecond_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityfirst)) + ((ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityfirst) + (ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityfirst))) /\ ((exists ge_balance_positive_iff_irreducible_secondsecond_unitidentityfirstreal ge_balance_negative_iff_irreducible_secondsecond_unitidentityfirstreal. (((((ge_representation_real_code_iff_irreducible_secondsecond_unitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_secondsecond_unitidentityfirstreal) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondsecond_unitidentityfirstrealdecode. (((ge_representation_real_code_iff_irreducible_secondsecond_unitidentityfirst) = 2 * ge_signed_half_iff_irreducible_secondsecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondsecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentityfirstreal) = S ge_signed_half_iff_irreducible_secondsecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_iff_irreducible_secondsecond_unitidentity) + ge_balance_negative_iff_irreducible_secondsecond_unitidentityfirstreal = (ge_first_rn_iff_irreducible_secondsecond_unitidentity) + ge_balance_positive_iff_irreducible_secondsecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_iff_irreducible_secondsecond_unitidentityfirstimaginary ge_balance_negative_iff_irreducible_secondsecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityfirst) = 2 * (ge_balance_positive_iff_irreducible_secondsecond_unitidentityfirstimaginary) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondsecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityfirst) = 2 * ge_signed_half_iff_irreducible_secondsecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondsecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentityfirstimaginary) = S ge_signed_half_iff_irreducible_secondsecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_iff_irreducible_secondsecond_unitidentity) + ge_balance_negative_iff_irreducible_secondsecond_unitidentityfirstimaginary = (ge_first_in_iff_irreducible_secondsecond_unitidentity) + ge_balance_positive_iff_irreducible_secondsecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_iff_irreducible_secondsecond_unitidentitysecond ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentitysecond. (((gr_inverse_iff_irreducible_secondsecond_unit) = ((ge_representation_real_code_iff_irreducible_secondsecond_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentitysecond)) * S ((ge_representation_real_code_iff_irreducible_secondsecond_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentitysecond)) + ((ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentitysecond) + (ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentitysecond))) /\ ((exists ge_balance_positive_iff_irreducible_secondsecond_unitidentitysecondreal ge_balance_negative_iff_irreducible_secondsecond_unitidentitysecondreal. (((((ge_representation_real_code_iff_irreducible_secondsecond_unitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_secondsecond_unitidentitysecondreal) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondsecond_unitidentitysecondrealdecode. (((ge_representation_real_code_iff_irreducible_secondsecond_unitidentitysecond) = 2 * ge_signed_half_iff_irreducible_secondsecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondsecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentitysecondreal) = S ge_signed_half_iff_irreducible_secondsecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_iff_irreducible_secondsecond_unitidentity) + ge_balance_negative_iff_irreducible_secondsecond_unitidentitysecondreal = (ge_second_rn_iff_irreducible_secondsecond_unitidentity) + ge_balance_positive_iff_irreducible_secondsecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_iff_irreducible_secondsecond_unitidentitysecondimaginary ge_balance_negative_iff_irreducible_secondsecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentitysecond) = 2 * (ge_balance_positive_iff_irreducible_secondsecond_unitidentitysecondimaginary) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondsecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentitysecond) = 2 * ge_signed_half_iff_irreducible_secondsecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondsecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentitysecondimaginary) = S ge_signed_half_iff_irreducible_secondsecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_iff_irreducible_secondsecond_unitidentity) + ge_balance_negative_iff_irreducible_secondsecond_unitidentitysecondimaginary = (ge_second_in_iff_irreducible_secondsecond_unitidentity) + ge_balance_positive_iff_irreducible_secondsecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_iff_irreducible_secondsecond_unitidentityoutput ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityoutput. (((6) = ((ge_representation_real_code_iff_irreducible_secondsecond_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityoutput)) * S ((ge_representation_real_code_iff_irreducible_secondsecond_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityoutput)) + ((ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityoutput) + (ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityoutput))) /\ ((exists ge_balance_positive_iff_irreducible_secondsecond_unitidentityoutputreal ge_balance_negative_iff_irreducible_secondsecond_unitidentityoutputreal. (((((ge_representation_real_code_iff_irreducible_secondsecond_unitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_secondsecond_unitidentityoutputreal) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_iff_irreducible_secondsecond_unitidentityoutputrealdecode. (((ge_representation_real_code_iff_irreducible_secondsecond_unitidentityoutput) = 2 * ge_signed_half_iff_irreducible_secondsecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_iff_irreducible_secondsecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentityoutputreal) = S ge_signed_half_iff_irreducible_secondsecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_iff_irreducible_secondsecond_unitidentity) * (ge_second_rp_iff_irreducible_secondsecond_unitidentity))) + (((ge_first_rn_iff_irreducible_secondsecond_unitidentity) * (ge_second_rn_iff_irreducible_secondsecond_unitidentity))))) + (((((ge_first_ip_iff_irreducible_secondsecond_unitidentity) * (ge_second_in_iff_irreducible_secondsecond_unitidentity))) + (((ge_first_in_iff_irreducible_secondsecond_unitidentity) * (ge_second_ip_iff_irreducible_secondsecond_unitidentity))))))) + ge_balance_negative_iff_irreducible_secondsecond_unitidentityoutputreal = (((((((ge_first_rp_iff_irreducible_secondsecond_unitidentity) * (ge_second_rn_iff_irreducible_secondsecond_unitidentity))) + (((ge_first_rn_iff_irreducible_secondsecond_unitidentity) * (ge_second_rp_iff_irreducible_secondsecond_unitidentity))))) + (((((ge_first_ip_iff_irreducible_secondsecond_unitidentity) * (ge_second_ip_iff_irreducible_secondsecond_unitidentity))) + (((ge_first_in_iff_irreducible_secondsecond_unitidentity) * (ge_second_in_iff_irreducible_secondsecond_unitidentity))))))) + ge_balance_positive_iff_irreducible_secondsecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_iff_irreducible_secondsecond_unitidentityoutputimaginary ge_balance_negative_iff_irreducible_secondsecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityoutput) = 2 * (ge_balance_positive_iff_irreducible_secondsecond_unitidentityoutputimaginary) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_iff_irreducible_secondsecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_iff_irreducible_secondsecond_unitidentityoutput) = 2 * ge_signed_half_iff_irreducible_secondsecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_iff_irreducible_secondsecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_iff_irreducible_secondsecond_unitidentityoutputimaginary) = S ge_signed_half_iff_irreducible_secondsecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_iff_irreducible_secondsecond_unitidentity) * (ge_second_ip_iff_irreducible_secondsecond_unitidentity))) + (((ge_first_rn_iff_irreducible_secondsecond_unitidentity) * (ge_second_in_iff_irreducible_secondsecond_unitidentity))))) + (((((ge_first_ip_iff_irreducible_secondsecond_unitidentity) * (ge_second_rp_iff_irreducible_secondsecond_unitidentity))) + (((ge_first_in_iff_irreducible_secondsecond_unitidentity) * (ge_second_rn_iff_irreducible_secondsecond_unitidentity))))))) + ge_balance_negative_iff_irreducible_secondsecond_unitidentityoutputimaginary = (((((((ge_first_rp_iff_irreducible_secondsecond_unitidentity) * (ge_second_in_iff_irreducible_secondsecond_unitidentity))) + (((ge_first_rn_iff_irreducible_secondsecond_unitidentity) * (ge_second_ip_iff_irreducible_secondsecond_unitidentity))))) + (((((ge_first_ip_iff_irreducible_secondsecond_unitidentity) * (ge_second_rn_iff_irreducible_secondsecond_unitidentity))) + (((ge_first_in_iff_irreducible_secondsecond_unitidentity) * (ge_second_rp_iff_irreducible_secondsecond_unitidentity))))))) + ge_balance_positive_iff_irreducible_secondsecond_unitidentityoutputimaginary))))))))))))))))