gaussian_irreducible_is_prime

Exact expanded first-order arithmetic statement

forall p. (((exists ge_real_positive_irreducible_prime_sourcecarrier ge_real_negative_irreducible_prime_sourcecarrier ge_imaginary_positive_irreducible_prime_sourcecarrier ge_imaginary_negative_irreducible_prime_sourcecarrier. (exists ge_real_code_irreducible_prime_sourcecarrierdecode ge_imaginary_code_irreducible_prime_sourcecarrierdecode. (((p) = ((ge_real_code_irreducible_prime_sourcecarrierdecode) + (ge_imaginary_code_irreducible_prime_sourcecarrierdecode)) * S ((ge_real_code_irreducible_prime_sourcecarrierdecode) + (ge_imaginary_code_irreducible_prime_sourcecarrierdecode)) + ((ge_imaginary_code_irreducible_prime_sourcecarrierdecode) + (ge_imaginary_code_irreducible_prime_sourcecarrierdecode))) /\ (((((ge_real_code_irreducible_prime_sourcecarrierdecode) = 2 * (ge_real_positive_irreducible_prime_sourcecarrier) /\ (ge_real_negative_irreducible_prime_sourcecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_real. (((ge_real_code_irreducible_prime_sourcecarrierdecode) = 2 * ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_real + 1 /\ (ge_real_positive_irreducible_prime_sourcecarrier) = 0) /\ (ge_real_negative_irreducible_prime_sourcecarrier) = S ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_prime_sourcecarrierdecode) = 2 * (ge_imaginary_positive_irreducible_prime_sourcecarrier) /\ (ge_imaginary_negative_irreducible_prime_sourcecarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_imaginary. (((ge_imaginary_code_irreducible_prime_sourcecarrierdecode) = 2 * ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_prime_sourcecarrier) = 0) /\ (ge_imaginary_negative_irreducible_prime_sourcecarrier) = S ge_signed_half_ge_irreducible_prime_sourcecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_irreducible_prime_sourcenonunit. (exists ge_first_rp_irreducible_prime_sourcenonunitidentity ge_first_rn_irreducible_prime_sourcenonunitidentity ge_first_ip_irreducible_prime_sourcenonunitidentity ge_first_in_irreducible_prime_sourcenonunitidentity ge_second_rp_irreducible_prime_sourcenonunitidentity ge_second_rn_irreducible_prime_sourcenonunitidentity ge_second_ip_irreducible_prime_sourcenonunitidentity ge_second_in_irreducible_prime_sourcenonunitidentity. ((exists ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst. (((p) = ((ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstreal ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prime_sourcenonunitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstreal) = S ge_signed_half_irreducible_prime_sourcenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_sourcenonunitidentity) + ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstreal = (ge_first_rn_irreducible_prime_sourcenonunitidentity) + ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstimaginary ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstimaginary) = S ge_signed_half_irreducible_prime_sourcenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_sourcenonunitidentity) + ge_balance_negative_irreducible_prime_sourcenonunitidentityfirstimaginary = (ge_first_in_irreducible_prime_sourcenonunitidentity) + ge_balance_positive_irreducible_prime_sourcenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond. (((gr_inverse_irreducible_prime_sourcenonunit) = ((ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondreal ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prime_sourcenonunitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondreal) = S ge_signed_half_irreducible_prime_sourcenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_sourcenonunitidentity) + ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondreal = (ge_second_rn_irreducible_prime_sourcenonunitidentity) + ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondimaginary ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondimaginary) = S ge_signed_half_irreducible_prime_sourcenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_sourcenonunitidentity) + ge_balance_negative_irreducible_prime_sourcenonunitidentitysecondimaginary = (ge_second_in_irreducible_prime_sourcenonunitidentity) + ge_balance_positive_irreducible_prime_sourcenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputreal ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prime_sourcenonunitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputreal) = S ge_signed_half_irreducible_prime_sourcenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcenonunitidentity) * (ge_second_rp_irreducible_prime_sourcenonunitidentity))) + (((ge_first_rn_irreducible_prime_sourcenonunitidentity) * (ge_second_rn_irreducible_prime_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcenonunitidentity) * (ge_second_in_irreducible_prime_sourcenonunitidentity))) + (((ge_first_in_irreducible_prime_sourcenonunitidentity) * (ge_second_ip_irreducible_prime_sourcenonunitidentity))))))) + ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputreal = (((((((ge_first_rp_irreducible_prime_sourcenonunitidentity) * (ge_second_rn_irreducible_prime_sourcenonunitidentity))) + (((ge_first_rn_irreducible_prime_sourcenonunitidentity) * (ge_second_rp_irreducible_prime_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcenonunitidentity) * (ge_second_ip_irreducible_prime_sourcenonunitidentity))) + (((ge_first_in_irreducible_prime_sourcenonunitidentity) * (ge_second_in_irreducible_prime_sourcenonunitidentity))))))) + ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputimaginary ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcenonunitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputimaginary) = S ge_signed_half_irreducible_prime_sourcenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcenonunitidentity) * (ge_second_ip_irreducible_prime_sourcenonunitidentity))) + (((ge_first_rn_irreducible_prime_sourcenonunitidentity) * (ge_second_in_irreducible_prime_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcenonunitidentity) * (ge_second_rp_irreducible_prime_sourcenonunitidentity))) + (((ge_first_in_irreducible_prime_sourcenonunitidentity) * (ge_second_rn_irreducible_prime_sourcenonunitidentity))))))) + ge_balance_negative_irreducible_prime_sourcenonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prime_sourcenonunitidentity) * (ge_second_in_irreducible_prime_sourcenonunitidentity))) + (((ge_first_rn_irreducible_prime_sourcenonunitidentity) * (ge_second_ip_irreducible_prime_sourcenonunitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcenonunitidentity) * (ge_second_rn_irreducible_prime_sourcenonunitidentity))) + (((ge_first_in_irreducible_prime_sourcenonunitidentity) * (ge_second_rp_irreducible_prime_sourcenonunitidentity))))))) + ge_balance_positive_irreducible_prime_sourcenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_prime_source gr_second_factor_irreducible_prime_source. (exists ge_first_rp_irreducible_prime_sourcefactorization ge_first_rn_irreducible_prime_sourcefactorization ge_first_ip_irreducible_prime_sourcefactorization ge_first_in_irreducible_prime_sourcefactorization ge_second_rp_irreducible_prime_sourcefactorization ge_second_rn_irreducible_prime_sourcefactorization ge_second_ip_irreducible_prime_sourcefactorization ge_second_in_irreducible_prime_sourcefactorization. ((exists ge_representation_real_code_irreducible_prime_sourcefactorizationfirst ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst. (((gr_first_factor_irreducible_prime_source) = ((ge_representation_real_code_irreducible_prime_sourcefactorizationfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst)) * S ((ge_representation_real_code_irreducible_prime_sourcefactorizationfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefactorizationfirstreal ge_balance_negative_irreducible_prime_sourcefactorizationfirstreal. (((((ge_representation_real_code_irreducible_prime_sourcefactorizationfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationfirstreal) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationfirstrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefactorizationfirst) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationfirstreal) = S ge_signed_half_irreducible_prime_sourcefactorizationfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_sourcefactorization) + ge_balance_negative_irreducible_prime_sourcefactorizationfirstreal = (ge_first_rn_irreducible_prime_sourcefactorization) + ge_balance_positive_irreducible_prime_sourcefactorizationfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefactorizationfirstimaginary ge_balance_negative_irreducible_prime_sourcefactorizationfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationfirstimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationfirst) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationfirstimaginary) = S ge_signed_half_irreducible_prime_sourcefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_sourcefactorization) + ge_balance_negative_irreducible_prime_sourcefactorizationfirstimaginary = (ge_first_in_irreducible_prime_sourcefactorization) + ge_balance_positive_irreducible_prime_sourcefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_sourcefactorizationsecond ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond. (((gr_second_factor_irreducible_prime_source) = ((ge_representation_real_code_irreducible_prime_sourcefactorizationsecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond)) * S ((ge_representation_real_code_irreducible_prime_sourcefactorizationsecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefactorizationsecondreal ge_balance_negative_irreducible_prime_sourcefactorizationsecondreal. (((((ge_representation_real_code_irreducible_prime_sourcefactorizationsecond) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationsecondreal) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationsecondrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefactorizationsecond) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationsecondreal) = S ge_signed_half_irreducible_prime_sourcefactorizationsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_sourcefactorization) + ge_balance_negative_irreducible_prime_sourcefactorizationsecondreal = (ge_second_rn_irreducible_prime_sourcefactorization) + ge_balance_positive_irreducible_prime_sourcefactorizationsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefactorizationsecondimaginary ge_balance_negative_irreducible_prime_sourcefactorizationsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationsecondimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationsecond) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationsecondimaginary) = S ge_signed_half_irreducible_prime_sourcefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_sourcefactorization) + ge_balance_negative_irreducible_prime_sourcefactorizationsecondimaginary = (ge_second_in_irreducible_prime_sourcefactorization) + ge_balance_positive_irreducible_prime_sourcefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_sourcefactorizationoutput ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput. (((p) = ((ge_representation_real_code_irreducible_prime_sourcefactorizationoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput)) * S ((ge_representation_real_code_irreducible_prime_sourcefactorizationoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefactorizationoutputreal ge_balance_negative_irreducible_prime_sourcefactorizationoutputreal. (((((ge_representation_real_code_irreducible_prime_sourcefactorizationoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationoutputreal) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationoutputrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefactorizationoutput) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationoutputreal) = S ge_signed_half_irreducible_prime_sourcefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcefactorization) * (ge_second_rp_irreducible_prime_sourcefactorization))) + (((ge_first_rn_irreducible_prime_sourcefactorization) * (ge_second_rn_irreducible_prime_sourcefactorization))))) + (((((ge_first_ip_irreducible_prime_sourcefactorization) * (ge_second_in_irreducible_prime_sourcefactorization))) + (((ge_first_in_irreducible_prime_sourcefactorization) * (ge_second_ip_irreducible_prime_sourcefactorization))))))) + ge_balance_negative_irreducible_prime_sourcefactorizationoutputreal = (((((((ge_first_rp_irreducible_prime_sourcefactorization) * (ge_second_rn_irreducible_prime_sourcefactorization))) + (((ge_first_rn_irreducible_prime_sourcefactorization) * (ge_second_rp_irreducible_prime_sourcefactorization))))) + (((((ge_first_ip_irreducible_prime_sourcefactorization) * (ge_second_ip_irreducible_prime_sourcefactorization))) + (((ge_first_in_irreducible_prime_sourcefactorization) * (ge_second_in_irreducible_prime_sourcefactorization))))))) + ge_balance_positive_irreducible_prime_sourcefactorizationoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefactorizationoutputimaginary ge_balance_negative_irreducible_prime_sourcefactorizationoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcefactorizationoutputimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefactorizationoutput) = 2 * ge_signed_half_irreducible_prime_sourcefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefactorizationoutputimaginary) = S ge_signed_half_irreducible_prime_sourcefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcefactorization) * (ge_second_ip_irreducible_prime_sourcefactorization))) + (((ge_first_rn_irreducible_prime_sourcefactorization) * (ge_second_in_irreducible_prime_sourcefactorization))))) + (((((ge_first_ip_irreducible_prime_sourcefactorization) * (ge_second_rp_irreducible_prime_sourcefactorization))) + (((ge_first_in_irreducible_prime_sourcefactorization) * (ge_second_rn_irreducible_prime_sourcefactorization))))))) + ge_balance_negative_irreducible_prime_sourcefactorizationoutputimaginary = (((((((ge_first_rp_irreducible_prime_sourcefactorization) * (ge_second_in_irreducible_prime_sourcefactorization))) + (((ge_first_rn_irreducible_prime_sourcefactorization) * (ge_second_ip_irreducible_prime_sourcefactorization))))) + (((((ge_first_ip_irreducible_prime_sourcefactorization) * (ge_second_rn_irreducible_prime_sourcefactorization))) + (((ge_first_in_irreducible_prime_sourcefactorization) * (ge_second_rp_irreducible_prime_sourcefactorization))))))) + ge_balance_positive_irreducible_prime_sourcefactorizationoutputimaginary))))))))) -> (exists gr_inverse_irreducible_prime_sourcefirst_unit. (exists ge_first_rp_irreducible_prime_sourcefirst_unitidentity ge_first_rn_irreducible_prime_sourcefirst_unitidentity ge_first_ip_irreducible_prime_sourcefirst_unitidentity ge_first_in_irreducible_prime_sourcefirst_unitidentity ge_second_rp_irreducible_prime_sourcefirst_unitidentity ge_second_rn_irreducible_prime_sourcefirst_unitidentity ge_second_ip_irreducible_prime_sourcefirst_unitidentity ge_second_in_irreducible_prime_sourcefirst_unitidentity. ((exists ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst. (((gr_first_factor_irreducible_prime_source) = ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstreal ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstreal) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstreal = (ge_first_rn_irreducible_prime_sourcefirst_unitidentity) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstimaginary ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstimaginary) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentityfirstimaginary = (ge_first_in_irreducible_prime_sourcefirst_unitidentity) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond. (((gr_inverse_irreducible_prime_sourcefirst_unit) = ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondreal ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondreal) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_sourcefirst_unitidentity) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondreal = (ge_second_rn_irreducible_prime_sourcefirst_unitidentity) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondimaginary ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondimaginary) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_sourcefirst_unitidentity) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentitysecondimaginary = (ge_second_in_irreducible_prime_sourcefirst_unitidentity) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputreal ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prime_sourcefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputreal) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rp_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rn_irreducible_prime_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) * (ge_second_in_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_prime_sourcefirst_unitidentity) * (ge_second_ip_irreducible_prime_sourcefirst_unitidentity))))))) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputreal = (((((((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rn_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rp_irreducible_prime_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) * (ge_second_ip_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_prime_sourcefirst_unitidentity) * (ge_second_in_irreducible_prime_sourcefirst_unitidentity))))))) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputimaginary ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcefirst_unitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputimaginary) = S ge_signed_half_irreducible_prime_sourcefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) * (ge_second_ip_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcefirst_unitidentity) * (ge_second_in_irreducible_prime_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rp_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rn_irreducible_prime_sourcefirst_unitidentity))))))) + ge_balance_negative_irreducible_prime_sourcefirst_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prime_sourcefirst_unitidentity) * (ge_second_in_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcefirst_unitidentity) * (ge_second_ip_irreducible_prime_sourcefirst_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rn_irreducible_prime_sourcefirst_unitidentity))) + (((ge_first_in_irreducible_prime_sourcefirst_unitidentity) * (ge_second_rp_irreducible_prime_sourcefirst_unitidentity))))))) + ge_balance_positive_irreducible_prime_sourcefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_irreducible_prime_sourcesecond_unit. (exists ge_first_rp_irreducible_prime_sourcesecond_unitidentity ge_first_rn_irreducible_prime_sourcesecond_unitidentity ge_first_ip_irreducible_prime_sourcesecond_unitidentity ge_first_in_irreducible_prime_sourcesecond_unitidentity ge_second_rp_irreducible_prime_sourcesecond_unitidentity ge_second_rn_irreducible_prime_sourcesecond_unitidentity ge_second_ip_irreducible_prime_sourcesecond_unitidentity ge_second_in_irreducible_prime_sourcesecond_unitidentity. ((exists ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst. (((gr_second_factor_irreducible_prime_source) = ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst)) * S ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstreal ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstreal. (((((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstreal) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstreal) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstreal = (ge_first_rn_irreducible_prime_sourcesecond_unitidentity) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstimaginary ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityfirst) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstimaginary) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentityfirstimaginary = (ge_first_in_irreducible_prime_sourcesecond_unitidentity) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond. (((gr_inverse_irreducible_prime_sourcesecond_unit) = ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond)) * S ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondreal ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondreal. (((((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondreal) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondreal) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_sourcesecond_unitidentity) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondreal = (ge_second_rn_irreducible_prime_sourcesecond_unitidentity) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondimaginary ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentitysecond) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondimaginary) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_sourcesecond_unitidentity) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentitysecondimaginary = (ge_second_in_irreducible_prime_sourcesecond_unitidentity) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput)) * S ((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputreal ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputreal. (((((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputreal) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prime_sourcesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputreal) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rp_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rn_irreducible_prime_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) * (ge_second_in_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_prime_sourcesecond_unitidentity) * (ge_second_ip_irreducible_prime_sourcesecond_unitidentity))))))) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputreal = (((((((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rn_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rp_irreducible_prime_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) * (ge_second_ip_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_prime_sourcesecond_unitidentity) * (ge_second_in_irreducible_prime_sourcesecond_unitidentity))))))) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputimaginary ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_sourcesecond_unitidentityoutput) = 2 * ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputimaginary) = S ge_signed_half_irreducible_prime_sourcesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) * (ge_second_ip_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcesecond_unitidentity) * (ge_second_in_irreducible_prime_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rp_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rn_irreducible_prime_sourcesecond_unitidentity))))))) + ge_balance_negative_irreducible_prime_sourcesecond_unitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prime_sourcesecond_unitidentity) * (ge_second_in_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_rn_irreducible_prime_sourcesecond_unitidentity) * (ge_second_ip_irreducible_prime_sourcesecond_unitidentity))))) + (((((ge_first_ip_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rn_irreducible_prime_sourcesecond_unitidentity))) + (((ge_first_in_irreducible_prime_sourcesecond_unitidentity) * (ge_second_rp_irreducible_prime_sourcesecond_unitidentity))))))) + ge_balance_positive_irreducible_prime_sourcesecond_unitidentityoutputimaginary))))))))))))))) -> (((exists ge_real_positive_irreducible_prime_resultcarrier ge_real_negative_irreducible_prime_resultcarrier ge_imaginary_positive_irreducible_prime_resultcarrier ge_imaginary_negative_irreducible_prime_resultcarrier. (exists ge_real_code_irreducible_prime_resultcarrierdecode ge_imaginary_code_irreducible_prime_resultcarrierdecode. (((p) = ((ge_real_code_irreducible_prime_resultcarrierdecode) + (ge_imaginary_code_irreducible_prime_resultcarrierdecode)) * S ((ge_real_code_irreducible_prime_resultcarrierdecode) + (ge_imaginary_code_irreducible_prime_resultcarrierdecode)) + ((ge_imaginary_code_irreducible_prime_resultcarrierdecode) + (ge_imaginary_code_irreducible_prime_resultcarrierdecode))) /\ (((((ge_real_code_irreducible_prime_resultcarrierdecode) = 2 * (ge_real_positive_irreducible_prime_resultcarrier) /\ (ge_real_negative_irreducible_prime_resultcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prime_resultcarrierdecode_real. (((ge_real_code_irreducible_prime_resultcarrierdecode) = 2 * ge_signed_half_ge_irreducible_prime_resultcarrierdecode_real + 1 /\ (ge_real_positive_irreducible_prime_resultcarrier) = 0) /\ (ge_real_negative_irreducible_prime_resultcarrier) = S ge_signed_half_ge_irreducible_prime_resultcarrierdecode_real))) /\ ((((ge_imaginary_code_irreducible_prime_resultcarrierdecode) = 2 * (ge_imaginary_positive_irreducible_prime_resultcarrier) /\ (ge_imaginary_negative_irreducible_prime_resultcarrier) = 0) \/ exists ge_signed_half_ge_irreducible_prime_resultcarrierdecode_imaginary. (((ge_imaginary_code_irreducible_prime_resultcarrierdecode) = 2 * ge_signed_half_ge_irreducible_prime_resultcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_irreducible_prime_resultcarrier) = 0) /\ (ge_imaginary_negative_irreducible_prime_resultcarrier) = S ge_signed_half_ge_irreducible_prime_resultcarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_irreducible_prime_resultnonunit. (exists ge_first_rp_irreducible_prime_resultnonunitidentity ge_first_rn_irreducible_prime_resultnonunitidentity ge_first_ip_irreducible_prime_resultnonunitidentity ge_first_in_irreducible_prime_resultnonunitidentity ge_second_rp_irreducible_prime_resultnonunitidentity ge_second_rn_irreducible_prime_resultnonunitidentity ge_second_ip_irreducible_prime_resultnonunitidentity ge_second_in_irreducible_prime_resultnonunitidentity. ((exists ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst. (((p) = ((ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst)) * S ((ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultnonunitidentityfirstreal ge_balance_negative_irreducible_prime_resultnonunitidentityfirstreal. (((((ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentityfirstreal) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentityfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultnonunitidentityfirst) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityfirstreal) = S ge_signed_half_irreducible_prime_resultnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultnonunitidentity) + ge_balance_negative_irreducible_prime_resultnonunitidentityfirstreal = (ge_first_rn_irreducible_prime_resultnonunitidentity) + ge_balance_positive_irreducible_prime_resultnonunitidentityfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultnonunitidentityfirstimaginary ge_balance_negative_irreducible_prime_resultnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentityfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityfirst) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityfirstimaginary) = S ge_signed_half_irreducible_prime_resultnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultnonunitidentity) + ge_balance_negative_irreducible_prime_resultnonunitidentityfirstimaginary = (ge_first_in_irreducible_prime_resultnonunitidentity) + ge_balance_positive_irreducible_prime_resultnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond. (((gr_inverse_irreducible_prime_resultnonunit) = ((ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond)) * S ((ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultnonunitidentitysecondreal ge_balance_negative_irreducible_prime_resultnonunitidentitysecondreal. (((((ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentitysecondreal) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentitysecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultnonunitidentitysecond) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentitysecondreal) = S ge_signed_half_irreducible_prime_resultnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultnonunitidentity) + ge_balance_negative_irreducible_prime_resultnonunitidentitysecondreal = (ge_second_rn_irreducible_prime_resultnonunitidentity) + ge_balance_positive_irreducible_prime_resultnonunitidentitysecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultnonunitidentitysecondimaginary ge_balance_negative_irreducible_prime_resultnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentitysecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentitysecond) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentitysecondimaginary) = S ge_signed_half_irreducible_prime_resultnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultnonunitidentity) + ge_balance_negative_irreducible_prime_resultnonunitidentitysecondimaginary = (ge_second_in_irreducible_prime_resultnonunitidentity) + ge_balance_positive_irreducible_prime_resultnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput. (((6) = ((ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput)) * S ((ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput) + (ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultnonunitidentityoutputreal ge_balance_negative_irreducible_prime_resultnonunitidentityoutputreal. (((((ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentityoutputreal) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentityoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultnonunitidentityoutput) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityoutputreal) = S ge_signed_half_irreducible_prime_resultnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultnonunitidentity) * (ge_second_rp_irreducible_prime_resultnonunitidentity))) + (((ge_first_rn_irreducible_prime_resultnonunitidentity) * (ge_second_rn_irreducible_prime_resultnonunitidentity))))) + (((((ge_first_ip_irreducible_prime_resultnonunitidentity) * (ge_second_in_irreducible_prime_resultnonunitidentity))) + (((ge_first_in_irreducible_prime_resultnonunitidentity) * (ge_second_ip_irreducible_prime_resultnonunitidentity))))))) + ge_balance_negative_irreducible_prime_resultnonunitidentityoutputreal = (((((((ge_first_rp_irreducible_prime_resultnonunitidentity) * (ge_second_rn_irreducible_prime_resultnonunitidentity))) + (((ge_first_rn_irreducible_prime_resultnonunitidentity) * (ge_second_rp_irreducible_prime_resultnonunitidentity))))) + (((((ge_first_ip_irreducible_prime_resultnonunitidentity) * (ge_second_ip_irreducible_prime_resultnonunitidentity))) + (((ge_first_in_irreducible_prime_resultnonunitidentity) * (ge_second_in_irreducible_prime_resultnonunitidentity))))))) + ge_balance_positive_irreducible_prime_resultnonunitidentityoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultnonunitidentityoutputimaginary ge_balance_negative_irreducible_prime_resultnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput) = 2 * (ge_balance_positive_irreducible_prime_resultnonunitidentityoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultnonunitidentityoutput) = 2 * ge_signed_half_irreducible_prime_resultnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultnonunitidentityoutputimaginary) = S ge_signed_half_irreducible_prime_resultnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultnonunitidentity) * (ge_second_ip_irreducible_prime_resultnonunitidentity))) + (((ge_first_rn_irreducible_prime_resultnonunitidentity) * (ge_second_in_irreducible_prime_resultnonunitidentity))))) + (((((ge_first_ip_irreducible_prime_resultnonunitidentity) * (ge_second_rp_irreducible_prime_resultnonunitidentity))) + (((ge_first_in_irreducible_prime_resultnonunitidentity) * (ge_second_rn_irreducible_prime_resultnonunitidentity))))))) + ge_balance_negative_irreducible_prime_resultnonunitidentityoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultnonunitidentity) * (ge_second_in_irreducible_prime_resultnonunitidentity))) + (((ge_first_rn_irreducible_prime_resultnonunitidentity) * (ge_second_ip_irreducible_prime_resultnonunitidentity))))) + (((((ge_first_ip_irreducible_prime_resultnonunitidentity) * (ge_second_rn_irreducible_prime_resultnonunitidentity))) + (((ge_first_in_irreducible_prime_resultnonunitidentity) * (ge_second_rp_irreducible_prime_resultnonunitidentity))))))) + ge_balance_positive_irreducible_prime_resultnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_irreducible_prime_result gr_second_factor_irreducible_prime_result gr_product_irreducible_prime_result. (exists ge_first_rp_irreducible_prime_resultproduct ge_first_rn_irreducible_prime_resultproduct ge_first_ip_irreducible_prime_resultproduct ge_first_in_irreducible_prime_resultproduct ge_second_rp_irreducible_prime_resultproduct ge_second_rn_irreducible_prime_resultproduct ge_second_ip_irreducible_prime_resultproduct ge_second_in_irreducible_prime_resultproduct. ((exists ge_representation_real_code_irreducible_prime_resultproductfirst ge_representation_imaginary_code_irreducible_prime_resultproductfirst. (((gr_first_factor_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultproductfirst)) * S ((ge_representation_real_code_irreducible_prime_resultproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultproductfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultproductfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultproductfirstreal ge_balance_negative_irreducible_prime_resultproductfirstreal. (((((ge_representation_real_code_irreducible_prime_resultproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultproductfirstreal) /\ (ge_balance_negative_irreducible_prime_resultproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultproductfirst) = 2 * ge_signed_half_irreducible_prime_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductfirstreal) = S ge_signed_half_irreducible_prime_resultproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultproduct) + ge_balance_negative_irreducible_prime_resultproductfirstreal = (ge_first_rn_irreducible_prime_resultproduct) + ge_balance_positive_irreducible_prime_resultproductfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultproductfirstimaginary ge_balance_negative_irreducible_prime_resultproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultproductfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultproductfirst) = 2 * ge_signed_half_irreducible_prime_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductfirstimaginary) = S ge_signed_half_irreducible_prime_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultproduct) + ge_balance_negative_irreducible_prime_resultproductfirstimaginary = (ge_first_in_irreducible_prime_resultproduct) + ge_balance_positive_irreducible_prime_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultproductsecond ge_representation_imaginary_code_irreducible_prime_resultproductsecond. (((gr_second_factor_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultproductsecond)) * S ((ge_representation_real_code_irreducible_prime_resultproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultproductsecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultproductsecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultproductsecondreal ge_balance_negative_irreducible_prime_resultproductsecondreal. (((((ge_representation_real_code_irreducible_prime_resultproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultproductsecondreal) /\ (ge_balance_negative_irreducible_prime_resultproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductsecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultproductsecond) = 2 * ge_signed_half_irreducible_prime_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductsecondreal) = S ge_signed_half_irreducible_prime_resultproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultproduct) + ge_balance_negative_irreducible_prime_resultproductsecondreal = (ge_second_rn_irreducible_prime_resultproduct) + ge_balance_positive_irreducible_prime_resultproductsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultproductsecondimaginary ge_balance_negative_irreducible_prime_resultproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultproductsecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultproductsecond) = 2 * ge_signed_half_irreducible_prime_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductsecondimaginary) = S ge_signed_half_irreducible_prime_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultproduct) + ge_balance_negative_irreducible_prime_resultproductsecondimaginary = (ge_second_in_irreducible_prime_resultproduct) + ge_balance_positive_irreducible_prime_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultproductoutput ge_representation_imaginary_code_irreducible_prime_resultproductoutput. (((gr_product_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultproductoutput)) * S ((ge_representation_real_code_irreducible_prime_resultproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultproductoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultproductoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultproductoutputreal ge_balance_negative_irreducible_prime_resultproductoutputreal. (((((ge_representation_real_code_irreducible_prime_resultproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultproductoutputreal) /\ (ge_balance_negative_irreducible_prime_resultproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultproductoutput) = 2 * ge_signed_half_irreducible_prime_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductoutputreal) = S ge_signed_half_irreducible_prime_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultproduct) * (ge_second_rp_irreducible_prime_resultproduct))) + (((ge_first_rn_irreducible_prime_resultproduct) * (ge_second_rn_irreducible_prime_resultproduct))))) + (((((ge_first_ip_irreducible_prime_resultproduct) * (ge_second_in_irreducible_prime_resultproduct))) + (((ge_first_in_irreducible_prime_resultproduct) * (ge_second_ip_irreducible_prime_resultproduct))))))) + ge_balance_negative_irreducible_prime_resultproductoutputreal = (((((((ge_first_rp_irreducible_prime_resultproduct) * (ge_second_rn_irreducible_prime_resultproduct))) + (((ge_first_rn_irreducible_prime_resultproduct) * (ge_second_rp_irreducible_prime_resultproduct))))) + (((((ge_first_ip_irreducible_prime_resultproduct) * (ge_second_ip_irreducible_prime_resultproduct))) + (((ge_first_in_irreducible_prime_resultproduct) * (ge_second_in_irreducible_prime_resultproduct))))))) + ge_balance_positive_irreducible_prime_resultproductoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultproductoutputimaginary ge_balance_negative_irreducible_prime_resultproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultproductoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultproductoutput) = 2 * ge_signed_half_irreducible_prime_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultproductoutputimaginary) = S ge_signed_half_irreducible_prime_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultproduct) * (ge_second_ip_irreducible_prime_resultproduct))) + (((ge_first_rn_irreducible_prime_resultproduct) * (ge_second_in_irreducible_prime_resultproduct))))) + (((((ge_first_ip_irreducible_prime_resultproduct) * (ge_second_rp_irreducible_prime_resultproduct))) + (((ge_first_in_irreducible_prime_resultproduct) * (ge_second_rn_irreducible_prime_resultproduct))))))) + ge_balance_negative_irreducible_prime_resultproductoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultproduct) * (ge_second_in_irreducible_prime_resultproduct))) + (((ge_first_rn_irreducible_prime_resultproduct) * (ge_second_ip_irreducible_prime_resultproduct))))) + (((((ge_first_ip_irreducible_prime_resultproduct) * (ge_second_rn_irreducible_prime_resultproduct))) + (((ge_first_in_irreducible_prime_resultproduct) * (ge_second_rp_irreducible_prime_resultproduct))))))) + ge_balance_positive_irreducible_prime_resultproductoutputimaginary))))))))) -> (exists gr_quotient_irreducible_prime_resultdivisor. (exists ge_first_rp_irreducible_prime_resultdivisorproduct ge_first_rn_irreducible_prime_resultdivisorproduct ge_first_ip_irreducible_prime_resultdivisorproduct ge_first_in_irreducible_prime_resultdivisorproduct ge_second_rp_irreducible_prime_resultdivisorproduct ge_second_rn_irreducible_prime_resultdivisorproduct ge_second_ip_irreducible_prime_resultdivisorproduct ge_second_in_irreducible_prime_resultdivisorproduct. ((exists ge_representation_real_code_irreducible_prime_resultdivisorproductfirst ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst. (((p) = ((ge_representation_real_code_irreducible_prime_resultdivisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst)) * S ((ge_representation_real_code_irreducible_prime_resultdivisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultdivisorproductfirstreal ge_balance_negative_irreducible_prime_resultdivisorproductfirstreal. (((((ge_representation_real_code_irreducible_prime_resultdivisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductfirstreal) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultdivisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductfirstreal) = S ge_signed_half_irreducible_prime_resultdivisorproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultdivisorproduct) + ge_balance_negative_irreducible_prime_resultdivisorproductfirstreal = (ge_first_rn_irreducible_prime_resultdivisorproduct) + ge_balance_positive_irreducible_prime_resultdivisorproductfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultdivisorproductfirstimaginary ge_balance_negative_irreducible_prime_resultdivisorproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductfirstimaginary) = S ge_signed_half_irreducible_prime_resultdivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultdivisorproduct) + ge_balance_negative_irreducible_prime_resultdivisorproductfirstimaginary = (ge_first_in_irreducible_prime_resultdivisorproduct) + ge_balance_positive_irreducible_prime_resultdivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultdivisorproductsecond ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond. (((gr_quotient_irreducible_prime_resultdivisor) = ((ge_representation_real_code_irreducible_prime_resultdivisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond)) * S ((ge_representation_real_code_irreducible_prime_resultdivisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultdivisorproductsecondreal ge_balance_negative_irreducible_prime_resultdivisorproductsecondreal. (((((ge_representation_real_code_irreducible_prime_resultdivisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductsecondreal) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductsecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultdivisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductsecondreal) = S ge_signed_half_irreducible_prime_resultdivisorproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultdivisorproduct) + ge_balance_negative_irreducible_prime_resultdivisorproductsecondreal = (ge_second_rn_irreducible_prime_resultdivisorproduct) + ge_balance_positive_irreducible_prime_resultdivisorproductsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultdivisorproductsecondimaginary ge_balance_negative_irreducible_prime_resultdivisorproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductsecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductsecondimaginary) = S ge_signed_half_irreducible_prime_resultdivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultdivisorproduct) + ge_balance_negative_irreducible_prime_resultdivisorproductsecondimaginary = (ge_second_in_irreducible_prime_resultdivisorproduct) + ge_balance_positive_irreducible_prime_resultdivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultdivisorproductoutput ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput. (((gr_product_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultdivisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput)) * S ((ge_representation_real_code_irreducible_prime_resultdivisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultdivisorproductoutputreal ge_balance_negative_irreducible_prime_resultdivisorproductoutputreal. (((((ge_representation_real_code_irreducible_prime_resultdivisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductoutputreal) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultdivisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductoutputreal) = S ge_signed_half_irreducible_prime_resultdivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultdivisorproduct) * (ge_second_rp_irreducible_prime_resultdivisorproduct))) + (((ge_first_rn_irreducible_prime_resultdivisorproduct) * (ge_second_rn_irreducible_prime_resultdivisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultdivisorproduct) * (ge_second_in_irreducible_prime_resultdivisorproduct))) + (((ge_first_in_irreducible_prime_resultdivisorproduct) * (ge_second_ip_irreducible_prime_resultdivisorproduct))))))) + ge_balance_negative_irreducible_prime_resultdivisorproductoutputreal = (((((((ge_first_rp_irreducible_prime_resultdivisorproduct) * (ge_second_rn_irreducible_prime_resultdivisorproduct))) + (((ge_first_rn_irreducible_prime_resultdivisorproduct) * (ge_second_rp_irreducible_prime_resultdivisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultdivisorproduct) * (ge_second_ip_irreducible_prime_resultdivisorproduct))) + (((ge_first_in_irreducible_prime_resultdivisorproduct) * (ge_second_in_irreducible_prime_resultdivisorproduct))))))) + ge_balance_positive_irreducible_prime_resultdivisorproductoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultdivisorproductoutputimaginary ge_balance_negative_irreducible_prime_resultdivisorproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultdivisorproductoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultdivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultdivisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultdivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultdivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultdivisorproductoutputimaginary) = S ge_signed_half_irreducible_prime_resultdivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultdivisorproduct) * (ge_second_ip_irreducible_prime_resultdivisorproduct))) + (((ge_first_rn_irreducible_prime_resultdivisorproduct) * (ge_second_in_irreducible_prime_resultdivisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultdivisorproduct) * (ge_second_rp_irreducible_prime_resultdivisorproduct))) + (((ge_first_in_irreducible_prime_resultdivisorproduct) * (ge_second_rn_irreducible_prime_resultdivisorproduct))))))) + ge_balance_negative_irreducible_prime_resultdivisorproductoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultdivisorproduct) * (ge_second_in_irreducible_prime_resultdivisorproduct))) + (((ge_first_rn_irreducible_prime_resultdivisorproduct) * (ge_second_ip_irreducible_prime_resultdivisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultdivisorproduct) * (ge_second_rn_irreducible_prime_resultdivisorproduct))) + (((ge_first_in_irreducible_prime_resultdivisorproduct) * (ge_second_rp_irreducible_prime_resultdivisorproduct))))))) + ge_balance_positive_irreducible_prime_resultdivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_irreducible_prime_resultfirst_divisor. (exists ge_first_rp_irreducible_prime_resultfirst_divisorproduct ge_first_rn_irreducible_prime_resultfirst_divisorproduct ge_first_ip_irreducible_prime_resultfirst_divisorproduct ge_first_in_irreducible_prime_resultfirst_divisorproduct ge_second_rp_irreducible_prime_resultfirst_divisorproduct ge_second_rn_irreducible_prime_resultfirst_divisorproduct ge_second_ip_irreducible_prime_resultfirst_divisorproduct ge_second_in_irreducible_prime_resultfirst_divisorproduct. ((exists ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst. (((p) = ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst)) * S ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstreal ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstreal. (((((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstreal) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstreal) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstreal = (ge_first_rn_irreducible_prime_resultfirst_divisorproduct) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstimaginary ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstimaginary) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductfirstimaginary = (ge_first_in_irreducible_prime_resultfirst_divisorproduct) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond. (((gr_quotient_irreducible_prime_resultfirst_divisor) = ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond)) * S ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondreal ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondreal. (((((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondreal) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondreal) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultfirst_divisorproduct) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondreal = (ge_second_rn_irreducible_prime_resultfirst_divisorproduct) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondimaginary ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondimaginary) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultfirst_divisorproduct) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductsecondimaginary = (ge_second_in_irreducible_prime_resultfirst_divisorproduct) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput. (((gr_first_factor_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput)) * S ((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputreal ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputreal. (((((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputreal) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultfirst_divisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputreal) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rp_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rn_irreducible_prime_resultfirst_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) * (ge_second_in_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_in_irreducible_prime_resultfirst_divisorproduct) * (ge_second_ip_irreducible_prime_resultfirst_divisorproduct))))))) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputreal = (((((((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rn_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rp_irreducible_prime_resultfirst_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) * (ge_second_ip_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_in_irreducible_prime_resultfirst_divisorproduct) * (ge_second_in_irreducible_prime_resultfirst_divisorproduct))))))) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputimaginary ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultfirst_divisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputimaginary) = S ge_signed_half_irreducible_prime_resultfirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) * (ge_second_ip_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultfirst_divisorproduct) * (ge_second_in_irreducible_prime_resultfirst_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rp_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_in_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rn_irreducible_prime_resultfirst_divisorproduct))))))) + ge_balance_negative_irreducible_prime_resultfirst_divisorproductoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultfirst_divisorproduct) * (ge_second_in_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultfirst_divisorproduct) * (ge_second_ip_irreducible_prime_resultfirst_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rn_irreducible_prime_resultfirst_divisorproduct))) + (((ge_first_in_irreducible_prime_resultfirst_divisorproduct) * (ge_second_rp_irreducible_prime_resultfirst_divisorproduct))))))) + ge_balance_positive_irreducible_prime_resultfirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_irreducible_prime_resultsecond_divisor. (exists ge_first_rp_irreducible_prime_resultsecond_divisorproduct ge_first_rn_irreducible_prime_resultsecond_divisorproduct ge_first_ip_irreducible_prime_resultsecond_divisorproduct ge_first_in_irreducible_prime_resultsecond_divisorproduct ge_second_rp_irreducible_prime_resultsecond_divisorproduct ge_second_rn_irreducible_prime_resultsecond_divisorproduct ge_second_ip_irreducible_prime_resultsecond_divisorproduct ge_second_in_irreducible_prime_resultsecond_divisorproduct. ((exists ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst. (((p) = ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst)) * S ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst)) + ((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst))) /\ ((exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstreal ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstreal. (((((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstreal) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstrealdecode. (((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstreal) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstreal = (ge_first_rn_irreducible_prime_resultsecond_divisorproduct) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstimaginary ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstimaginary) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductfirst) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstimaginary) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductfirstimaginary = (ge_first_in_irreducible_prime_resultsecond_divisorproduct) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond. (((gr_quotient_irreducible_prime_resultsecond_divisor) = ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond)) * S ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond)) + ((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond))) /\ ((exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondreal ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondreal. (((((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondreal) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondrealdecode. (((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondreal) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_irreducible_prime_resultsecond_divisorproduct) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondreal = (ge_second_rn_irreducible_prime_resultsecond_divisorproduct) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondimaginary ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondimaginary) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductsecond) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondimaginary) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_irreducible_prime_resultsecond_divisorproduct) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductsecondimaginary = (ge_second_in_irreducible_prime_resultsecond_divisorproduct) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput. (((gr_second_factor_irreducible_prime_result) = ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput)) * S ((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput)) + ((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput) + (ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput))) /\ ((exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputreal ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputreal. (((((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputreal) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputrealdecode. (((ge_representation_real_code_irreducible_prime_resultsecond_divisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputreal) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rp_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rn_irreducible_prime_resultsecond_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) * (ge_second_in_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_in_irreducible_prime_resultsecond_divisorproduct) * (ge_second_ip_irreducible_prime_resultsecond_divisorproduct))))))) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputreal = (((((((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rn_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rp_irreducible_prime_resultsecond_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) * (ge_second_ip_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_in_irreducible_prime_resultsecond_divisorproduct) * (ge_second_in_irreducible_prime_resultsecond_divisorproduct))))))) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputimaginary ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput) = 2 * (ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputimaginary) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_irreducible_prime_resultsecond_divisorproductoutput) = 2 * ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputimaginary) = S ge_signed_half_irreducible_prime_resultsecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) * (ge_second_ip_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultsecond_divisorproduct) * (ge_second_in_irreducible_prime_resultsecond_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rp_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_in_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rn_irreducible_prime_resultsecond_divisorproduct))))))) + ge_balance_negative_irreducible_prime_resultsecond_divisorproductoutputimaginary = (((((((ge_first_rp_irreducible_prime_resultsecond_divisorproduct) * (ge_second_in_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_rn_irreducible_prime_resultsecond_divisorproduct) * (ge_second_ip_irreducible_prime_resultsecond_divisorproduct))))) + (((((ge_first_ip_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rn_irreducible_prime_resultsecond_divisorproduct))) + (((ge_first_in_irreducible_prime_resultsecond_divisorproduct) * (ge_second_rp_irreducible_prime_resultsecond_divisorproduct))))))) + ge_balance_positive_irreducible_prime_resultsecond_divisorproductoutputimaginary)))))))))))))))