gaussian_irreducible_dvd_product

Exact expanded first-order arithmetic statement

forall p a b c. (((exists ge_real_positive_prime_irreduciblecarrier ge_real_negative_prime_irreduciblecarrier ge_imaginary_positive_prime_irreduciblecarrier ge_imaginary_negative_prime_irreduciblecarrier. (exists ge_real_code_prime_irreduciblecarrierdecode ge_imaginary_code_prime_irreduciblecarrierdecode. (((p) = ((ge_real_code_prime_irreduciblecarrierdecode) + (ge_imaginary_code_prime_irreduciblecarrierdecode)) * S ((ge_real_code_prime_irreduciblecarrierdecode) + (ge_imaginary_code_prime_irreduciblecarrierdecode)) + ((ge_imaginary_code_prime_irreduciblecarrierdecode) + (ge_imaginary_code_prime_irreduciblecarrierdecode))) /\ (((((ge_real_code_prime_irreduciblecarrierdecode) = 2 * (ge_real_positive_prime_irreduciblecarrier) /\ (ge_real_negative_prime_irreduciblecarrier) = 0) \/ exists ge_signed_half_ge_prime_irreduciblecarrierdecode_real. (((ge_real_code_prime_irreduciblecarrierdecode) = 2 * ge_signed_half_ge_prime_irreduciblecarrierdecode_real + 1 /\ (ge_real_positive_prime_irreduciblecarrier) = 0) /\ (ge_real_negative_prime_irreduciblecarrier) = S ge_signed_half_ge_prime_irreduciblecarrierdecode_real))) /\ ((((ge_imaginary_code_prime_irreduciblecarrierdecode) = 2 * (ge_imaginary_positive_prime_irreduciblecarrier) /\ (ge_imaginary_negative_prime_irreduciblecarrier) = 0) \/ exists ge_signed_half_ge_prime_irreduciblecarrierdecode_imaginary. (((ge_imaginary_code_prime_irreduciblecarrierdecode) = 2 * ge_signed_half_ge_prime_irreduciblecarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_prime_irreduciblecarrier) = 0) /\ (ge_imaginary_negative_prime_irreduciblecarrier) = S ge_signed_half_ge_prime_irreduciblecarrierdecode_imaginary))))))) /\ ((~((p)=0)) /\ ((~(exists gr_inverse_prime_irreduciblenonunit. (exists ge_first_rp_prime_irreduciblenonunitidentity ge_first_rn_prime_irreduciblenonunitidentity ge_first_ip_prime_irreduciblenonunitidentity ge_first_in_prime_irreduciblenonunitidentity ge_second_rp_prime_irreduciblenonunitidentity ge_second_rn_prime_irreduciblenonunitidentity ge_second_ip_prime_irreduciblenonunitidentity ge_second_in_prime_irreduciblenonunitidentity. ((exists ge_representation_real_code_prime_irreduciblenonunitidentityfirst ge_representation_imaginary_code_prime_irreduciblenonunitidentityfirst. (((p) = ((ge_representation_real_code_prime_irreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreduciblenonunitidentityfirst)) * S ((ge_representation_real_code_prime_irreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreduciblenonunitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreduciblenonunitidentityfirst) + (ge_representation_imaginary_code_prime_irreduciblenonunitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreduciblenonunitidentityfirstreal ge_balance_negative_prime_irreduciblenonunitidentityfirstreal. (((((ge_representation_real_code_prime_irreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreduciblenonunitidentityfirstreal) /\ (ge_balance_negative_prime_irreduciblenonunitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreduciblenonunitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreduciblenonunitidentityfirst) = 2 * ge_signed_half_prime_irreduciblenonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblenonunitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreduciblenonunitidentityfirstreal) = S ge_signed_half_prime_irreduciblenonunitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreduciblenonunitidentity) + ge_balance_negative_prime_irreduciblenonunitidentityfirstreal = (ge_first_rn_prime_irreduciblenonunitidentity) + ge_balance_positive_prime_irreduciblenonunitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreduciblenonunitidentityfirstimaginary ge_balance_negative_prime_irreduciblenonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreduciblenonunitidentityfirst) = 2 * (ge_balance_positive_prime_irreduciblenonunitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreduciblenonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblenonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblenonunitidentityfirst) = 2 * ge_signed_half_prime_irreduciblenonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblenonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblenonunitidentityfirstimaginary) = S ge_signed_half_prime_irreduciblenonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreduciblenonunitidentity) + ge_balance_negative_prime_irreduciblenonunitidentityfirstimaginary = (ge_first_in_prime_irreduciblenonunitidentity) + ge_balance_positive_prime_irreduciblenonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreduciblenonunitidentitysecond ge_representation_imaginary_code_prime_irreduciblenonunitidentitysecond. (((gr_inverse_prime_irreduciblenonunit) = ((ge_representation_real_code_prime_irreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreduciblenonunitidentitysecond)) * S ((ge_representation_real_code_prime_irreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreduciblenonunitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreduciblenonunitidentitysecond) + (ge_representation_imaginary_code_prime_irreduciblenonunitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreduciblenonunitidentitysecondreal ge_balance_negative_prime_irreduciblenonunitidentitysecondreal. (((((ge_representation_real_code_prime_irreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreduciblenonunitidentitysecondreal) /\ (ge_balance_negative_prime_irreduciblenonunitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreduciblenonunitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreduciblenonunitidentitysecond) = 2 * ge_signed_half_prime_irreduciblenonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblenonunitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreduciblenonunitidentitysecondreal) = S ge_signed_half_prime_irreduciblenonunitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreduciblenonunitidentity) + ge_balance_negative_prime_irreduciblenonunitidentitysecondreal = (ge_second_rn_prime_irreduciblenonunitidentity) + ge_balance_positive_prime_irreduciblenonunitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreduciblenonunitidentitysecondimaginary ge_balance_negative_prime_irreduciblenonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreduciblenonunitidentitysecond) = 2 * (ge_balance_positive_prime_irreduciblenonunitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreduciblenonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblenonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblenonunitidentitysecond) = 2 * ge_signed_half_prime_irreduciblenonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblenonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblenonunitidentitysecondimaginary) = S ge_signed_half_prime_irreduciblenonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreduciblenonunitidentity) + ge_balance_negative_prime_irreduciblenonunitidentitysecondimaginary = (ge_second_in_prime_irreduciblenonunitidentity) + ge_balance_positive_prime_irreduciblenonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreduciblenonunitidentityoutput ge_representation_imaginary_code_prime_irreduciblenonunitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreduciblenonunitidentityoutput)) * S ((ge_representation_real_code_prime_irreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreduciblenonunitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreduciblenonunitidentityoutput) + (ge_representation_imaginary_code_prime_irreduciblenonunitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreduciblenonunitidentityoutputreal ge_balance_negative_prime_irreduciblenonunitidentityoutputreal. (((((ge_representation_real_code_prime_irreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreduciblenonunitidentityoutputreal) /\ (ge_balance_negative_prime_irreduciblenonunitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreduciblenonunitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreduciblenonunitidentityoutput) = 2 * ge_signed_half_prime_irreduciblenonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblenonunitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreduciblenonunitidentityoutputreal) = S ge_signed_half_prime_irreduciblenonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreduciblenonunitidentity) * (ge_second_rp_prime_irreduciblenonunitidentity))) + (((ge_first_rn_prime_irreduciblenonunitidentity) * (ge_second_rn_prime_irreduciblenonunitidentity))))) + (((((ge_first_ip_prime_irreduciblenonunitidentity) * (ge_second_in_prime_irreduciblenonunitidentity))) + (((ge_first_in_prime_irreduciblenonunitidentity) * (ge_second_ip_prime_irreduciblenonunitidentity))))))) + ge_balance_negative_prime_irreduciblenonunitidentityoutputreal = (((((((ge_first_rp_prime_irreduciblenonunitidentity) * (ge_second_rn_prime_irreduciblenonunitidentity))) + (((ge_first_rn_prime_irreduciblenonunitidentity) * (ge_second_rp_prime_irreduciblenonunitidentity))))) + (((((ge_first_ip_prime_irreduciblenonunitidentity) * (ge_second_ip_prime_irreduciblenonunitidentity))) + (((ge_first_in_prime_irreduciblenonunitidentity) * (ge_second_in_prime_irreduciblenonunitidentity))))))) + ge_balance_positive_prime_irreduciblenonunitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreduciblenonunitidentityoutputimaginary ge_balance_negative_prime_irreduciblenonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreduciblenonunitidentityoutput) = 2 * (ge_balance_positive_prime_irreduciblenonunitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreduciblenonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblenonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblenonunitidentityoutput) = 2 * ge_signed_half_prime_irreduciblenonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblenonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblenonunitidentityoutputimaginary) = S ge_signed_half_prime_irreduciblenonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreduciblenonunitidentity) * (ge_second_ip_prime_irreduciblenonunitidentity))) + (((ge_first_rn_prime_irreduciblenonunitidentity) * (ge_second_in_prime_irreduciblenonunitidentity))))) + (((((ge_first_ip_prime_irreduciblenonunitidentity) * (ge_second_rp_prime_irreduciblenonunitidentity))) + (((ge_first_in_prime_irreduciblenonunitidentity) * (ge_second_rn_prime_irreduciblenonunitidentity))))))) + ge_balance_negative_prime_irreduciblenonunitidentityoutputimaginary = (((((((ge_first_rp_prime_irreduciblenonunitidentity) * (ge_second_in_prime_irreduciblenonunitidentity))) + (((ge_first_rn_prime_irreduciblenonunitidentity) * (ge_second_ip_prime_irreduciblenonunitidentity))))) + (((((ge_first_ip_prime_irreduciblenonunitidentity) * (ge_second_rn_prime_irreduciblenonunitidentity))) + (((ge_first_in_prime_irreduciblenonunitidentity) * (ge_second_rp_prime_irreduciblenonunitidentity))))))) + ge_balance_positive_prime_irreduciblenonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_prime_irreducible gr_second_factor_prime_irreducible. (exists ge_first_rp_prime_irreduciblefactorization ge_first_rn_prime_irreduciblefactorization ge_first_ip_prime_irreduciblefactorization ge_first_in_prime_irreduciblefactorization ge_second_rp_prime_irreduciblefactorization ge_second_rn_prime_irreduciblefactorization ge_second_ip_prime_irreduciblefactorization ge_second_in_prime_irreduciblefactorization. ((exists ge_representation_real_code_prime_irreduciblefactorizationfirst ge_representation_imaginary_code_prime_irreduciblefactorizationfirst. (((gr_first_factor_prime_irreducible) = ((ge_representation_real_code_prime_irreduciblefactorizationfirst) + (ge_representation_imaginary_code_prime_irreduciblefactorizationfirst)) * S ((ge_representation_real_code_prime_irreduciblefactorizationfirst) + (ge_representation_imaginary_code_prime_irreduciblefactorizationfirst)) + ((ge_representation_imaginary_code_prime_irreduciblefactorizationfirst) + (ge_representation_imaginary_code_prime_irreduciblefactorizationfirst))) /\ ((exists ge_balance_positive_prime_irreduciblefactorizationfirstreal ge_balance_negative_prime_irreduciblefactorizationfirstreal. (((((ge_representation_real_code_prime_irreduciblefactorizationfirst) = 2 * (ge_balance_positive_prime_irreduciblefactorizationfirstreal) /\ (ge_balance_negative_prime_irreduciblefactorizationfirstreal) = 0) \/ exists ge_signed_half_prime_irreduciblefactorizationfirstrealdecode. (((ge_representation_real_code_prime_irreduciblefactorizationfirst) = 2 * ge_signed_half_prime_irreduciblefactorizationfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblefactorizationfirstreal) = 0) /\ (ge_balance_negative_prime_irreduciblefactorizationfirstreal) = S ge_signed_half_prime_irreduciblefactorizationfirstrealdecode))) /\ ((ge_first_rp_prime_irreduciblefactorization) + ge_balance_negative_prime_irreduciblefactorizationfirstreal = (ge_first_rn_prime_irreduciblefactorization) + ge_balance_positive_prime_irreduciblefactorizationfirstreal))) /\ (exists ge_balance_positive_prime_irreduciblefactorizationfirstimaginary ge_balance_negative_prime_irreduciblefactorizationfirstimaginary. (((((ge_representation_imaginary_code_prime_irreduciblefactorizationfirst) = 2 * (ge_balance_positive_prime_irreduciblefactorizationfirstimaginary) /\ (ge_balance_negative_prime_irreduciblefactorizationfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblefactorizationfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblefactorizationfirst) = 2 * ge_signed_half_prime_irreduciblefactorizationfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblefactorizationfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblefactorizationfirstimaginary) = S ge_signed_half_prime_irreduciblefactorizationfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreduciblefactorization) + ge_balance_negative_prime_irreduciblefactorizationfirstimaginary = (ge_first_in_prime_irreduciblefactorization) + ge_balance_positive_prime_irreduciblefactorizationfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreduciblefactorizationsecond ge_representation_imaginary_code_prime_irreduciblefactorizationsecond. (((gr_second_factor_prime_irreducible) = ((ge_representation_real_code_prime_irreduciblefactorizationsecond) + (ge_representation_imaginary_code_prime_irreduciblefactorizationsecond)) * S ((ge_representation_real_code_prime_irreduciblefactorizationsecond) + (ge_representation_imaginary_code_prime_irreduciblefactorizationsecond)) + ((ge_representation_imaginary_code_prime_irreduciblefactorizationsecond) + (ge_representation_imaginary_code_prime_irreduciblefactorizationsecond))) /\ ((exists ge_balance_positive_prime_irreduciblefactorizationsecondreal ge_balance_negative_prime_irreduciblefactorizationsecondreal. (((((ge_representation_real_code_prime_irreduciblefactorizationsecond) = 2 * (ge_balance_positive_prime_irreduciblefactorizationsecondreal) /\ (ge_balance_negative_prime_irreduciblefactorizationsecondreal) = 0) \/ exists ge_signed_half_prime_irreduciblefactorizationsecondrealdecode. (((ge_representation_real_code_prime_irreduciblefactorizationsecond) = 2 * ge_signed_half_prime_irreduciblefactorizationsecondrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblefactorizationsecondreal) = 0) /\ (ge_balance_negative_prime_irreduciblefactorizationsecondreal) = S ge_signed_half_prime_irreduciblefactorizationsecondrealdecode))) /\ ((ge_second_rp_prime_irreduciblefactorization) + ge_balance_negative_prime_irreduciblefactorizationsecondreal = (ge_second_rn_prime_irreduciblefactorization) + ge_balance_positive_prime_irreduciblefactorizationsecondreal))) /\ (exists ge_balance_positive_prime_irreduciblefactorizationsecondimaginary ge_balance_negative_prime_irreduciblefactorizationsecondimaginary. (((((ge_representation_imaginary_code_prime_irreduciblefactorizationsecond) = 2 * (ge_balance_positive_prime_irreduciblefactorizationsecondimaginary) /\ (ge_balance_negative_prime_irreduciblefactorizationsecondimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblefactorizationsecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblefactorizationsecond) = 2 * ge_signed_half_prime_irreduciblefactorizationsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblefactorizationsecondimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblefactorizationsecondimaginary) = S ge_signed_half_prime_irreduciblefactorizationsecondimaginarydecode))) /\ ((ge_second_ip_prime_irreduciblefactorization) + ge_balance_negative_prime_irreduciblefactorizationsecondimaginary = (ge_second_in_prime_irreduciblefactorization) + ge_balance_positive_prime_irreduciblefactorizationsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreduciblefactorizationoutput ge_representation_imaginary_code_prime_irreduciblefactorizationoutput. (((p) = ((ge_representation_real_code_prime_irreduciblefactorizationoutput) + (ge_representation_imaginary_code_prime_irreduciblefactorizationoutput)) * S ((ge_representation_real_code_prime_irreduciblefactorizationoutput) + (ge_representation_imaginary_code_prime_irreduciblefactorizationoutput)) + ((ge_representation_imaginary_code_prime_irreduciblefactorizationoutput) + (ge_representation_imaginary_code_prime_irreduciblefactorizationoutput))) /\ ((exists ge_balance_positive_prime_irreduciblefactorizationoutputreal ge_balance_negative_prime_irreduciblefactorizationoutputreal. (((((ge_representation_real_code_prime_irreduciblefactorizationoutput) = 2 * (ge_balance_positive_prime_irreduciblefactorizationoutputreal) /\ (ge_balance_negative_prime_irreduciblefactorizationoutputreal) = 0) \/ exists ge_signed_half_prime_irreduciblefactorizationoutputrealdecode. (((ge_representation_real_code_prime_irreduciblefactorizationoutput) = 2 * ge_signed_half_prime_irreduciblefactorizationoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblefactorizationoutputreal) = 0) /\ (ge_balance_negative_prime_irreduciblefactorizationoutputreal) = S ge_signed_half_prime_irreduciblefactorizationoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreduciblefactorization) * (ge_second_rp_prime_irreduciblefactorization))) + (((ge_first_rn_prime_irreduciblefactorization) * (ge_second_rn_prime_irreduciblefactorization))))) + (((((ge_first_ip_prime_irreduciblefactorization) * (ge_second_in_prime_irreduciblefactorization))) + (((ge_first_in_prime_irreduciblefactorization) * (ge_second_ip_prime_irreduciblefactorization))))))) + ge_balance_negative_prime_irreduciblefactorizationoutputreal = (((((((ge_first_rp_prime_irreduciblefactorization) * (ge_second_rn_prime_irreduciblefactorization))) + (((ge_first_rn_prime_irreduciblefactorization) * (ge_second_rp_prime_irreduciblefactorization))))) + (((((ge_first_ip_prime_irreduciblefactorization) * (ge_second_ip_prime_irreduciblefactorization))) + (((ge_first_in_prime_irreduciblefactorization) * (ge_second_in_prime_irreduciblefactorization))))))) + ge_balance_positive_prime_irreduciblefactorizationoutputreal))) /\ (exists ge_balance_positive_prime_irreduciblefactorizationoutputimaginary ge_balance_negative_prime_irreduciblefactorizationoutputimaginary. (((((ge_representation_imaginary_code_prime_irreduciblefactorizationoutput) = 2 * (ge_balance_positive_prime_irreduciblefactorizationoutputimaginary) /\ (ge_balance_negative_prime_irreduciblefactorizationoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblefactorizationoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblefactorizationoutput) = 2 * ge_signed_half_prime_irreduciblefactorizationoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblefactorizationoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblefactorizationoutputimaginary) = S ge_signed_half_prime_irreduciblefactorizationoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreduciblefactorization) * (ge_second_ip_prime_irreduciblefactorization))) + (((ge_first_rn_prime_irreduciblefactorization) * (ge_second_in_prime_irreduciblefactorization))))) + (((((ge_first_ip_prime_irreduciblefactorization) * (ge_second_rp_prime_irreduciblefactorization))) + (((ge_first_in_prime_irreduciblefactorization) * (ge_second_rn_prime_irreduciblefactorization))))))) + ge_balance_negative_prime_irreduciblefactorizationoutputimaginary = (((((((ge_first_rp_prime_irreduciblefactorization) * (ge_second_in_prime_irreduciblefactorization))) + (((ge_first_rn_prime_irreduciblefactorization) * (ge_second_ip_prime_irreduciblefactorization))))) + (((((ge_first_ip_prime_irreduciblefactorization) * (ge_second_rn_prime_irreduciblefactorization))) + (((ge_first_in_prime_irreduciblefactorization) * (ge_second_rp_prime_irreduciblefactorization))))))) + ge_balance_positive_prime_irreduciblefactorizationoutputimaginary))))))))) -> (exists gr_inverse_prime_irreduciblefirst_unit. (exists ge_first_rp_prime_irreduciblefirst_unitidentity ge_first_rn_prime_irreduciblefirst_unitidentity ge_first_ip_prime_irreduciblefirst_unitidentity ge_first_in_prime_irreduciblefirst_unitidentity ge_second_rp_prime_irreduciblefirst_unitidentity ge_second_rn_prime_irreduciblefirst_unitidentity ge_second_ip_prime_irreduciblefirst_unitidentity ge_second_in_prime_irreduciblefirst_unitidentity. ((exists ge_representation_real_code_prime_irreduciblefirst_unitidentityfirst ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityfirst. (((gr_first_factor_prime_irreducible) = ((ge_representation_real_code_prime_irreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityfirst)) * S ((ge_representation_real_code_prime_irreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreduciblefirst_unitidentityfirstreal ge_balance_negative_prime_irreduciblefirst_unitidentityfirstreal. (((((ge_representation_real_code_prime_irreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreduciblefirst_unitidentityfirstreal) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreduciblefirst_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_prime_irreduciblefirst_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblefirst_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentityfirstreal) = S ge_signed_half_prime_irreduciblefirst_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreduciblefirst_unitidentity) + ge_balance_negative_prime_irreduciblefirst_unitidentityfirstreal = (ge_first_rn_prime_irreduciblefirst_unitidentity) + ge_balance_positive_prime_irreduciblefirst_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreduciblefirst_unitidentityfirstimaginary ge_balance_negative_prime_irreduciblefirst_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreduciblefirst_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblefirst_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityfirst) = 2 * ge_signed_half_prime_irreduciblefirst_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblefirst_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentityfirstimaginary) = S ge_signed_half_prime_irreduciblefirst_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreduciblefirst_unitidentity) + ge_balance_negative_prime_irreduciblefirst_unitidentityfirstimaginary = (ge_first_in_prime_irreduciblefirst_unitidentity) + ge_balance_positive_prime_irreduciblefirst_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreduciblefirst_unitidentitysecond ge_representation_imaginary_code_prime_irreduciblefirst_unitidentitysecond. (((gr_inverse_prime_irreduciblefirst_unit) = ((ge_representation_real_code_prime_irreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreduciblefirst_unitidentitysecond)) * S ((ge_representation_real_code_prime_irreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreduciblefirst_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreduciblefirst_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreduciblefirst_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreduciblefirst_unitidentitysecondreal ge_balance_negative_prime_irreduciblefirst_unitidentitysecondreal. (((((ge_representation_real_code_prime_irreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreduciblefirst_unitidentitysecondreal) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreduciblefirst_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_prime_irreduciblefirst_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblefirst_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentitysecondreal) = S ge_signed_half_prime_irreduciblefirst_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreduciblefirst_unitidentity) + ge_balance_negative_prime_irreduciblefirst_unitidentitysecondreal = (ge_second_rn_prime_irreduciblefirst_unitidentity) + ge_balance_positive_prime_irreduciblefirst_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreduciblefirst_unitidentitysecondimaginary ge_balance_negative_prime_irreduciblefirst_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreduciblefirst_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreduciblefirst_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblefirst_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblefirst_unitidentitysecond) = 2 * ge_signed_half_prime_irreduciblefirst_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblefirst_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentitysecondimaginary) = S ge_signed_half_prime_irreduciblefirst_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreduciblefirst_unitidentity) + ge_balance_negative_prime_irreduciblefirst_unitidentitysecondimaginary = (ge_second_in_prime_irreduciblefirst_unitidentity) + ge_balance_positive_prime_irreduciblefirst_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreduciblefirst_unitidentityoutput ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityoutput)) * S ((ge_representation_real_code_prime_irreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreduciblefirst_unitidentityoutputreal ge_balance_negative_prime_irreduciblefirst_unitidentityoutputreal. (((((ge_representation_real_code_prime_irreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreduciblefirst_unitidentityoutputreal) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreduciblefirst_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_prime_irreduciblefirst_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblefirst_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentityoutputreal) = S ge_signed_half_prime_irreduciblefirst_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreduciblefirst_unitidentity) * (ge_second_rp_prime_irreduciblefirst_unitidentity))) + (((ge_first_rn_prime_irreduciblefirst_unitidentity) * (ge_second_rn_prime_irreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_irreduciblefirst_unitidentity) * (ge_second_in_prime_irreduciblefirst_unitidentity))) + (((ge_first_in_prime_irreduciblefirst_unitidentity) * (ge_second_ip_prime_irreduciblefirst_unitidentity))))))) + ge_balance_negative_prime_irreduciblefirst_unitidentityoutputreal = (((((((ge_first_rp_prime_irreduciblefirst_unitidentity) * (ge_second_rn_prime_irreduciblefirst_unitidentity))) + (((ge_first_rn_prime_irreduciblefirst_unitidentity) * (ge_second_rp_prime_irreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_irreduciblefirst_unitidentity) * (ge_second_ip_prime_irreduciblefirst_unitidentity))) + (((ge_first_in_prime_irreduciblefirst_unitidentity) * (ge_second_in_prime_irreduciblefirst_unitidentity))))))) + ge_balance_positive_prime_irreduciblefirst_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreduciblefirst_unitidentityoutputimaginary ge_balance_negative_prime_irreduciblefirst_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreduciblefirst_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblefirst_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblefirst_unitidentityoutput) = 2 * ge_signed_half_prime_irreduciblefirst_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblefirst_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblefirst_unitidentityoutputimaginary) = S ge_signed_half_prime_irreduciblefirst_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreduciblefirst_unitidentity) * (ge_second_ip_prime_irreduciblefirst_unitidentity))) + (((ge_first_rn_prime_irreduciblefirst_unitidentity) * (ge_second_in_prime_irreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_irreduciblefirst_unitidentity) * (ge_second_rp_prime_irreduciblefirst_unitidentity))) + (((ge_first_in_prime_irreduciblefirst_unitidentity) * (ge_second_rn_prime_irreduciblefirst_unitidentity))))))) + ge_balance_negative_prime_irreduciblefirst_unitidentityoutputimaginary = (((((((ge_first_rp_prime_irreduciblefirst_unitidentity) * (ge_second_in_prime_irreduciblefirst_unitidentity))) + (((ge_first_rn_prime_irreduciblefirst_unitidentity) * (ge_second_ip_prime_irreduciblefirst_unitidentity))))) + (((((ge_first_ip_prime_irreduciblefirst_unitidentity) * (ge_second_rn_prime_irreduciblefirst_unitidentity))) + (((ge_first_in_prime_irreduciblefirst_unitidentity) * (ge_second_rp_prime_irreduciblefirst_unitidentity))))))) + ge_balance_positive_prime_irreduciblefirst_unitidentityoutputimaginary)))))))))) \/ (exists gr_inverse_prime_irreduciblesecond_unit. (exists ge_first_rp_prime_irreduciblesecond_unitidentity ge_first_rn_prime_irreduciblesecond_unitidentity ge_first_ip_prime_irreduciblesecond_unitidentity ge_first_in_prime_irreduciblesecond_unitidentity ge_second_rp_prime_irreduciblesecond_unitidentity ge_second_rn_prime_irreduciblesecond_unitidentity ge_second_ip_prime_irreduciblesecond_unitidentity ge_second_in_prime_irreduciblesecond_unitidentity. ((exists ge_representation_real_code_prime_irreduciblesecond_unitidentityfirst ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityfirst. (((gr_second_factor_prime_irreducible) = ((ge_representation_real_code_prime_irreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityfirst)) * S ((ge_representation_real_code_prime_irreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityfirst)) + ((ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityfirst) + (ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityfirst))) /\ ((exists ge_balance_positive_prime_irreduciblesecond_unitidentityfirstreal ge_balance_negative_prime_irreduciblesecond_unitidentityfirstreal. (((((ge_representation_real_code_prime_irreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreduciblesecond_unitidentityfirstreal) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentityfirstreal) = 0) \/ exists ge_signed_half_prime_irreduciblesecond_unitidentityfirstrealdecode. (((ge_representation_real_code_prime_irreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_prime_irreduciblesecond_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblesecond_unitidentityfirstreal) = 0) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentityfirstreal) = S ge_signed_half_prime_irreduciblesecond_unitidentityfirstrealdecode))) /\ ((ge_first_rp_prime_irreduciblesecond_unitidentity) + ge_balance_negative_prime_irreduciblesecond_unitidentityfirstreal = (ge_first_rn_prime_irreduciblesecond_unitidentity) + ge_balance_positive_prime_irreduciblesecond_unitidentityfirstreal))) /\ (exists ge_balance_positive_prime_irreduciblesecond_unitidentityfirstimaginary ge_balance_negative_prime_irreduciblesecond_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityfirst) = 2 * (ge_balance_positive_prime_irreduciblesecond_unitidentityfirstimaginary) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblesecond_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityfirst) = 2 * ge_signed_half_prime_irreduciblesecond_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblesecond_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentityfirstimaginary) = S ge_signed_half_prime_irreduciblesecond_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_prime_irreduciblesecond_unitidentity) + ge_balance_negative_prime_irreduciblesecond_unitidentityfirstimaginary = (ge_first_in_prime_irreduciblesecond_unitidentity) + ge_balance_positive_prime_irreduciblesecond_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_irreduciblesecond_unitidentitysecond ge_representation_imaginary_code_prime_irreduciblesecond_unitidentitysecond. (((gr_inverse_prime_irreduciblesecond_unit) = ((ge_representation_real_code_prime_irreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreduciblesecond_unitidentitysecond)) * S ((ge_representation_real_code_prime_irreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreduciblesecond_unitidentitysecond)) + ((ge_representation_imaginary_code_prime_irreduciblesecond_unitidentitysecond) + (ge_representation_imaginary_code_prime_irreduciblesecond_unitidentitysecond))) /\ ((exists ge_balance_positive_prime_irreduciblesecond_unitidentitysecondreal ge_balance_negative_prime_irreduciblesecond_unitidentitysecondreal. (((((ge_representation_real_code_prime_irreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreduciblesecond_unitidentitysecondreal) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentitysecondreal) = 0) \/ exists ge_signed_half_prime_irreduciblesecond_unitidentitysecondrealdecode. (((ge_representation_real_code_prime_irreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_prime_irreduciblesecond_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblesecond_unitidentitysecondreal) = 0) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentitysecondreal) = S ge_signed_half_prime_irreduciblesecond_unitidentitysecondrealdecode))) /\ ((ge_second_rp_prime_irreduciblesecond_unitidentity) + ge_balance_negative_prime_irreduciblesecond_unitidentitysecondreal = (ge_second_rn_prime_irreduciblesecond_unitidentity) + ge_balance_positive_prime_irreduciblesecond_unitidentitysecondreal))) /\ (exists ge_balance_positive_prime_irreduciblesecond_unitidentitysecondimaginary ge_balance_negative_prime_irreduciblesecond_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_prime_irreduciblesecond_unitidentitysecond) = 2 * (ge_balance_positive_prime_irreduciblesecond_unitidentitysecondimaginary) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblesecond_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblesecond_unitidentitysecond) = 2 * ge_signed_half_prime_irreduciblesecond_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblesecond_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentitysecondimaginary) = S ge_signed_half_prime_irreduciblesecond_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_prime_irreduciblesecond_unitidentity) + ge_balance_negative_prime_irreduciblesecond_unitidentitysecondimaginary = (ge_second_in_prime_irreduciblesecond_unitidentity) + ge_balance_positive_prime_irreduciblesecond_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_prime_irreduciblesecond_unitidentityoutput ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityoutput. (((6) = ((ge_representation_real_code_prime_irreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityoutput)) * S ((ge_representation_real_code_prime_irreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityoutput)) + ((ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityoutput) + (ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityoutput))) /\ ((exists ge_balance_positive_prime_irreduciblesecond_unitidentityoutputreal ge_balance_negative_prime_irreduciblesecond_unitidentityoutputreal. (((((ge_representation_real_code_prime_irreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreduciblesecond_unitidentityoutputreal) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentityoutputreal) = 0) \/ exists ge_signed_half_prime_irreduciblesecond_unitidentityoutputrealdecode. (((ge_representation_real_code_prime_irreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_prime_irreduciblesecond_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_prime_irreduciblesecond_unitidentityoutputreal) = 0) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentityoutputreal) = S ge_signed_half_prime_irreduciblesecond_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_prime_irreduciblesecond_unitidentity) * (ge_second_rp_prime_irreduciblesecond_unitidentity))) + (((ge_first_rn_prime_irreduciblesecond_unitidentity) * (ge_second_rn_prime_irreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_irreduciblesecond_unitidentity) * (ge_second_in_prime_irreduciblesecond_unitidentity))) + (((ge_first_in_prime_irreduciblesecond_unitidentity) * (ge_second_ip_prime_irreduciblesecond_unitidentity))))))) + ge_balance_negative_prime_irreduciblesecond_unitidentityoutputreal = (((((((ge_first_rp_prime_irreduciblesecond_unitidentity) * (ge_second_rn_prime_irreduciblesecond_unitidentity))) + (((ge_first_rn_prime_irreduciblesecond_unitidentity) * (ge_second_rp_prime_irreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_irreduciblesecond_unitidentity) * (ge_second_ip_prime_irreduciblesecond_unitidentity))) + (((ge_first_in_prime_irreduciblesecond_unitidentity) * (ge_second_in_prime_irreduciblesecond_unitidentity))))))) + ge_balance_positive_prime_irreduciblesecond_unitidentityoutputreal))) /\ (exists ge_balance_positive_prime_irreduciblesecond_unitidentityoutputimaginary ge_balance_negative_prime_irreduciblesecond_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityoutput) = 2 * (ge_balance_positive_prime_irreduciblesecond_unitidentityoutputimaginary) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_prime_irreduciblesecond_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_prime_irreduciblesecond_unitidentityoutput) = 2 * ge_signed_half_prime_irreduciblesecond_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_irreduciblesecond_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_prime_irreduciblesecond_unitidentityoutputimaginary) = S ge_signed_half_prime_irreduciblesecond_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_irreduciblesecond_unitidentity) * (ge_second_ip_prime_irreduciblesecond_unitidentity))) + (((ge_first_rn_prime_irreduciblesecond_unitidentity) * (ge_second_in_prime_irreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_irreduciblesecond_unitidentity) * (ge_second_rp_prime_irreduciblesecond_unitidentity))) + (((ge_first_in_prime_irreduciblesecond_unitidentity) * (ge_second_rn_prime_irreduciblesecond_unitidentity))))))) + ge_balance_negative_prime_irreduciblesecond_unitidentityoutputimaginary = (((((((ge_first_rp_prime_irreduciblesecond_unitidentity) * (ge_second_in_prime_irreduciblesecond_unitidentity))) + (((ge_first_rn_prime_irreduciblesecond_unitidentity) * (ge_second_ip_prime_irreduciblesecond_unitidentity))))) + (((((ge_first_ip_prime_irreduciblesecond_unitidentity) * (ge_second_rn_prime_irreduciblesecond_unitidentity))) + (((ge_first_in_prime_irreduciblesecond_unitidentity) * (ge_second_rp_prime_irreduciblesecond_unitidentity))))))) + ge_balance_positive_prime_irreduciblesecond_unitidentityoutputimaginary))))))))))))))) -> (exists ge_first_rp_prime_product ge_first_rn_prime_product ge_first_ip_prime_product ge_first_in_prime_product ge_second_rp_prime_product ge_second_rn_prime_product ge_second_ip_prime_product ge_second_in_prime_product. ((exists ge_representation_real_code_prime_productfirst ge_representation_imaginary_code_prime_productfirst. (((a) = ((ge_representation_real_code_prime_productfirst) + (ge_representation_imaginary_code_prime_productfirst)) * S ((ge_representation_real_code_prime_productfirst) + (ge_representation_imaginary_code_prime_productfirst)) + ((ge_representation_imaginary_code_prime_productfirst) + (ge_representation_imaginary_code_prime_productfirst))) /\ ((exists ge_balance_positive_prime_productfirstreal ge_balance_negative_prime_productfirstreal. (((((ge_representation_real_code_prime_productfirst) = 2 * (ge_balance_positive_prime_productfirstreal) /\ (ge_balance_negative_prime_productfirstreal) = 0) \/ exists ge_signed_half_prime_productfirstrealdecode. (((ge_representation_real_code_prime_productfirst) = 2 * ge_signed_half_prime_productfirstrealdecode + 1 /\ (ge_balance_positive_prime_productfirstreal) = 0) /\ (ge_balance_negative_prime_productfirstreal) = S ge_signed_half_prime_productfirstrealdecode))) /\ ((ge_first_rp_prime_product) + ge_balance_negative_prime_productfirstreal = (ge_first_rn_prime_product) + ge_balance_positive_prime_productfirstreal))) /\ (exists ge_balance_positive_prime_productfirstimaginary ge_balance_negative_prime_productfirstimaginary. (((((ge_representation_imaginary_code_prime_productfirst) = 2 * (ge_balance_positive_prime_productfirstimaginary) /\ (ge_balance_negative_prime_productfirstimaginary) = 0) \/ exists ge_signed_half_prime_productfirstimaginarydecode. (((ge_representation_imaginary_code_prime_productfirst) = 2 * ge_signed_half_prime_productfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_productfirstimaginary) = 0) /\ (ge_balance_negative_prime_productfirstimaginary) = S ge_signed_half_prime_productfirstimaginarydecode))) /\ ((ge_first_ip_prime_product) + ge_balance_negative_prime_productfirstimaginary = (ge_first_in_prime_product) + ge_balance_positive_prime_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_productsecond ge_representation_imaginary_code_prime_productsecond. (((b) = ((ge_representation_real_code_prime_productsecond) + (ge_representation_imaginary_code_prime_productsecond)) * S ((ge_representation_real_code_prime_productsecond) + (ge_representation_imaginary_code_prime_productsecond)) + ((ge_representation_imaginary_code_prime_productsecond) + (ge_representation_imaginary_code_prime_productsecond))) /\ ((exists ge_balance_positive_prime_productsecondreal ge_balance_negative_prime_productsecondreal. (((((ge_representation_real_code_prime_productsecond) = 2 * (ge_balance_positive_prime_productsecondreal) /\ (ge_balance_negative_prime_productsecondreal) = 0) \/ exists ge_signed_half_prime_productsecondrealdecode. (((ge_representation_real_code_prime_productsecond) = 2 * ge_signed_half_prime_productsecondrealdecode + 1 /\ (ge_balance_positive_prime_productsecondreal) = 0) /\ (ge_balance_negative_prime_productsecondreal) = S ge_signed_half_prime_productsecondrealdecode))) /\ ((ge_second_rp_prime_product) + ge_balance_negative_prime_productsecondreal = (ge_second_rn_prime_product) + ge_balance_positive_prime_productsecondreal))) /\ (exists ge_balance_positive_prime_productsecondimaginary ge_balance_negative_prime_productsecondimaginary. (((((ge_representation_imaginary_code_prime_productsecond) = 2 * (ge_balance_positive_prime_productsecondimaginary) /\ (ge_balance_negative_prime_productsecondimaginary) = 0) \/ exists ge_signed_half_prime_productsecondimaginarydecode. (((ge_representation_imaginary_code_prime_productsecond) = 2 * ge_signed_half_prime_productsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_productsecondimaginary) = 0) /\ (ge_balance_negative_prime_productsecondimaginary) = S ge_signed_half_prime_productsecondimaginarydecode))) /\ ((ge_second_ip_prime_product) + ge_balance_negative_prime_productsecondimaginary = (ge_second_in_prime_product) + ge_balance_positive_prime_productsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_productoutput ge_representation_imaginary_code_prime_productoutput. (((c) = ((ge_representation_real_code_prime_productoutput) + (ge_representation_imaginary_code_prime_productoutput)) * S ((ge_representation_real_code_prime_productoutput) + (ge_representation_imaginary_code_prime_productoutput)) + ((ge_representation_imaginary_code_prime_productoutput) + (ge_representation_imaginary_code_prime_productoutput))) /\ ((exists ge_balance_positive_prime_productoutputreal ge_balance_negative_prime_productoutputreal. (((((ge_representation_real_code_prime_productoutput) = 2 * (ge_balance_positive_prime_productoutputreal) /\ (ge_balance_negative_prime_productoutputreal) = 0) \/ exists ge_signed_half_prime_productoutputrealdecode. (((ge_representation_real_code_prime_productoutput) = 2 * ge_signed_half_prime_productoutputrealdecode + 1 /\ (ge_balance_positive_prime_productoutputreal) = 0) /\ (ge_balance_negative_prime_productoutputreal) = S ge_signed_half_prime_productoutputrealdecode))) /\ ((((((((ge_first_rp_prime_product) * (ge_second_rp_prime_product))) + (((ge_first_rn_prime_product) * (ge_second_rn_prime_product))))) + (((((ge_first_ip_prime_product) * (ge_second_in_prime_product))) + (((ge_first_in_prime_product) * (ge_second_ip_prime_product))))))) + ge_balance_negative_prime_productoutputreal = (((((((ge_first_rp_prime_product) * (ge_second_rn_prime_product))) + (((ge_first_rn_prime_product) * (ge_second_rp_prime_product))))) + (((((ge_first_ip_prime_product) * (ge_second_ip_prime_product))) + (((ge_first_in_prime_product) * (ge_second_in_prime_product))))))) + ge_balance_positive_prime_productoutputreal))) /\ (exists ge_balance_positive_prime_productoutputimaginary ge_balance_negative_prime_productoutputimaginary. (((((ge_representation_imaginary_code_prime_productoutput) = 2 * (ge_balance_positive_prime_productoutputimaginary) /\ (ge_balance_negative_prime_productoutputimaginary) = 0) \/ exists ge_signed_half_prime_productoutputimaginarydecode. (((ge_representation_imaginary_code_prime_productoutput) = 2 * ge_signed_half_prime_productoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_productoutputimaginary) = 0) /\ (ge_balance_negative_prime_productoutputimaginary) = S ge_signed_half_prime_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_product) * (ge_second_ip_prime_product))) + (((ge_first_rn_prime_product) * (ge_second_in_prime_product))))) + (((((ge_first_ip_prime_product) * (ge_second_rp_prime_product))) + (((ge_first_in_prime_product) * (ge_second_rn_prime_product))))))) + ge_balance_negative_prime_productoutputimaginary = (((((((ge_first_rp_prime_product) * (ge_second_in_prime_product))) + (((ge_first_rn_prime_product) * (ge_second_ip_prime_product))))) + (((((ge_first_ip_prime_product) * (ge_second_rn_prime_product))) + (((ge_first_in_prime_product) * (ge_second_rp_prime_product))))))) + ge_balance_positive_prime_productoutputimaginary))))))))) -> (exists gr_quotient_prime_divisor. (exists ge_first_rp_prime_divisorproduct ge_first_rn_prime_divisorproduct ge_first_ip_prime_divisorproduct ge_first_in_prime_divisorproduct ge_second_rp_prime_divisorproduct ge_second_rn_prime_divisorproduct ge_second_ip_prime_divisorproduct ge_second_in_prime_divisorproduct. ((exists ge_representation_real_code_prime_divisorproductfirst ge_representation_imaginary_code_prime_divisorproductfirst. (((p) = ((ge_representation_real_code_prime_divisorproductfirst) + (ge_representation_imaginary_code_prime_divisorproductfirst)) * S ((ge_representation_real_code_prime_divisorproductfirst) + (ge_representation_imaginary_code_prime_divisorproductfirst)) + ((ge_representation_imaginary_code_prime_divisorproductfirst) + (ge_representation_imaginary_code_prime_divisorproductfirst))) /\ ((exists ge_balance_positive_prime_divisorproductfirstreal ge_balance_negative_prime_divisorproductfirstreal. (((((ge_representation_real_code_prime_divisorproductfirst) = 2 * (ge_balance_positive_prime_divisorproductfirstreal) /\ (ge_balance_negative_prime_divisorproductfirstreal) = 0) \/ exists ge_signed_half_prime_divisorproductfirstrealdecode. (((ge_representation_real_code_prime_divisorproductfirst) = 2 * ge_signed_half_prime_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_divisorproductfirstreal) = 0) /\ (ge_balance_negative_prime_divisorproductfirstreal) = S ge_signed_half_prime_divisorproductfirstrealdecode))) /\ ((ge_first_rp_prime_divisorproduct) + ge_balance_negative_prime_divisorproductfirstreal = (ge_first_rn_prime_divisorproduct) + ge_balance_positive_prime_divisorproductfirstreal))) /\ (exists ge_balance_positive_prime_divisorproductfirstimaginary ge_balance_negative_prime_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_prime_divisorproductfirst) = 2 * (ge_balance_positive_prime_divisorproductfirstimaginary) /\ (ge_balance_negative_prime_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_divisorproductfirst) = 2 * ge_signed_half_prime_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_divisorproductfirstimaginary) = S ge_signed_half_prime_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_divisorproduct) + ge_balance_negative_prime_divisorproductfirstimaginary = (ge_first_in_prime_divisorproduct) + ge_balance_positive_prime_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_divisorproductsecond ge_representation_imaginary_code_prime_divisorproductsecond. (((gr_quotient_prime_divisor) = ((ge_representation_real_code_prime_divisorproductsecond) + (ge_representation_imaginary_code_prime_divisorproductsecond)) * S ((ge_representation_real_code_prime_divisorproductsecond) + (ge_representation_imaginary_code_prime_divisorproductsecond)) + ((ge_representation_imaginary_code_prime_divisorproductsecond) + (ge_representation_imaginary_code_prime_divisorproductsecond))) /\ ((exists ge_balance_positive_prime_divisorproductsecondreal ge_balance_negative_prime_divisorproductsecondreal. (((((ge_representation_real_code_prime_divisorproductsecond) = 2 * (ge_balance_positive_prime_divisorproductsecondreal) /\ (ge_balance_negative_prime_divisorproductsecondreal) = 0) \/ exists ge_signed_half_prime_divisorproductsecondrealdecode. (((ge_representation_real_code_prime_divisorproductsecond) = 2 * ge_signed_half_prime_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_divisorproductsecondreal) = 0) /\ (ge_balance_negative_prime_divisorproductsecondreal) = S ge_signed_half_prime_divisorproductsecondrealdecode))) /\ ((ge_second_rp_prime_divisorproduct) + ge_balance_negative_prime_divisorproductsecondreal = (ge_second_rn_prime_divisorproduct) + ge_balance_positive_prime_divisorproductsecondreal))) /\ (exists ge_balance_positive_prime_divisorproductsecondimaginary ge_balance_negative_prime_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_prime_divisorproductsecond) = 2 * (ge_balance_positive_prime_divisorproductsecondimaginary) /\ (ge_balance_negative_prime_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_divisorproductsecond) = 2 * ge_signed_half_prime_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_divisorproductsecondimaginary) = S ge_signed_half_prime_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_divisorproduct) + ge_balance_negative_prime_divisorproductsecondimaginary = (ge_second_in_prime_divisorproduct) + ge_balance_positive_prime_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_divisorproductoutput ge_representation_imaginary_code_prime_divisorproductoutput. (((c) = ((ge_representation_real_code_prime_divisorproductoutput) + (ge_representation_imaginary_code_prime_divisorproductoutput)) * S ((ge_representation_real_code_prime_divisorproductoutput) + (ge_representation_imaginary_code_prime_divisorproductoutput)) + ((ge_representation_imaginary_code_prime_divisorproductoutput) + (ge_representation_imaginary_code_prime_divisorproductoutput))) /\ ((exists ge_balance_positive_prime_divisorproductoutputreal ge_balance_negative_prime_divisorproductoutputreal. (((((ge_representation_real_code_prime_divisorproductoutput) = 2 * (ge_balance_positive_prime_divisorproductoutputreal) /\ (ge_balance_negative_prime_divisorproductoutputreal) = 0) \/ exists ge_signed_half_prime_divisorproductoutputrealdecode. (((ge_representation_real_code_prime_divisorproductoutput) = 2 * ge_signed_half_prime_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_divisorproductoutputreal) = 0) /\ (ge_balance_negative_prime_divisorproductoutputreal) = S ge_signed_half_prime_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_divisorproduct) * (ge_second_rp_prime_divisorproduct))) + (((ge_first_rn_prime_divisorproduct) * (ge_second_rn_prime_divisorproduct))))) + (((((ge_first_ip_prime_divisorproduct) * (ge_second_in_prime_divisorproduct))) + (((ge_first_in_prime_divisorproduct) * (ge_second_ip_prime_divisorproduct))))))) + ge_balance_negative_prime_divisorproductoutputreal = (((((((ge_first_rp_prime_divisorproduct) * (ge_second_rn_prime_divisorproduct))) + (((ge_first_rn_prime_divisorproduct) * (ge_second_rp_prime_divisorproduct))))) + (((((ge_first_ip_prime_divisorproduct) * (ge_second_ip_prime_divisorproduct))) + (((ge_first_in_prime_divisorproduct) * (ge_second_in_prime_divisorproduct))))))) + ge_balance_positive_prime_divisorproductoutputreal))) /\ (exists ge_balance_positive_prime_divisorproductoutputimaginary ge_balance_negative_prime_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_prime_divisorproductoutput) = 2 * (ge_balance_positive_prime_divisorproductoutputimaginary) /\ (ge_balance_negative_prime_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_divisorproductoutput) = 2 * ge_signed_half_prime_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_divisorproductoutputimaginary) = S ge_signed_half_prime_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_divisorproduct) * (ge_second_ip_prime_divisorproduct))) + (((ge_first_rn_prime_divisorproduct) * (ge_second_in_prime_divisorproduct))))) + (((((ge_first_ip_prime_divisorproduct) * (ge_second_rp_prime_divisorproduct))) + (((ge_first_in_prime_divisorproduct) * (ge_second_rn_prime_divisorproduct))))))) + ge_balance_negative_prime_divisorproductoutputimaginary = (((((((ge_first_rp_prime_divisorproduct) * (ge_second_in_prime_divisorproduct))) + (((ge_first_rn_prime_divisorproduct) * (ge_second_ip_prime_divisorproduct))))) + (((((ge_first_ip_prime_divisorproduct) * (ge_second_rn_prime_divisorproduct))) + (((ge_first_in_prime_divisorproduct) * (ge_second_rp_prime_divisorproduct))))))) + ge_balance_positive_prime_divisorproductoutputimaginary)))))))))) -> (exists gr_quotient_prime_first. (exists ge_first_rp_prime_firstproduct ge_first_rn_prime_firstproduct ge_first_ip_prime_firstproduct ge_first_in_prime_firstproduct ge_second_rp_prime_firstproduct ge_second_rn_prime_firstproduct ge_second_ip_prime_firstproduct ge_second_in_prime_firstproduct. ((exists ge_representation_real_code_prime_firstproductfirst ge_representation_imaginary_code_prime_firstproductfirst. (((p) = ((ge_representation_real_code_prime_firstproductfirst) + (ge_representation_imaginary_code_prime_firstproductfirst)) * S ((ge_representation_real_code_prime_firstproductfirst) + (ge_representation_imaginary_code_prime_firstproductfirst)) + ((ge_representation_imaginary_code_prime_firstproductfirst) + (ge_representation_imaginary_code_prime_firstproductfirst))) /\ ((exists ge_balance_positive_prime_firstproductfirstreal ge_balance_negative_prime_firstproductfirstreal. (((((ge_representation_real_code_prime_firstproductfirst) = 2 * (ge_balance_positive_prime_firstproductfirstreal) /\ (ge_balance_negative_prime_firstproductfirstreal) = 0) \/ exists ge_signed_half_prime_firstproductfirstrealdecode. (((ge_representation_real_code_prime_firstproductfirst) = 2 * ge_signed_half_prime_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_firstproductfirstreal) = 0) /\ (ge_balance_negative_prime_firstproductfirstreal) = S ge_signed_half_prime_firstproductfirstrealdecode))) /\ ((ge_first_rp_prime_firstproduct) + ge_balance_negative_prime_firstproductfirstreal = (ge_first_rn_prime_firstproduct) + ge_balance_positive_prime_firstproductfirstreal))) /\ (exists ge_balance_positive_prime_firstproductfirstimaginary ge_balance_negative_prime_firstproductfirstimaginary. (((((ge_representation_imaginary_code_prime_firstproductfirst) = 2 * (ge_balance_positive_prime_firstproductfirstimaginary) /\ (ge_balance_negative_prime_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_firstproductfirst) = 2 * ge_signed_half_prime_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_firstproductfirstimaginary) = S ge_signed_half_prime_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_firstproduct) + ge_balance_negative_prime_firstproductfirstimaginary = (ge_first_in_prime_firstproduct) + ge_balance_positive_prime_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_firstproductsecond ge_representation_imaginary_code_prime_firstproductsecond. (((gr_quotient_prime_first) = ((ge_representation_real_code_prime_firstproductsecond) + (ge_representation_imaginary_code_prime_firstproductsecond)) * S ((ge_representation_real_code_prime_firstproductsecond) + (ge_representation_imaginary_code_prime_firstproductsecond)) + ((ge_representation_imaginary_code_prime_firstproductsecond) + (ge_representation_imaginary_code_prime_firstproductsecond))) /\ ((exists ge_balance_positive_prime_firstproductsecondreal ge_balance_negative_prime_firstproductsecondreal. (((((ge_representation_real_code_prime_firstproductsecond) = 2 * (ge_balance_positive_prime_firstproductsecondreal) /\ (ge_balance_negative_prime_firstproductsecondreal) = 0) \/ exists ge_signed_half_prime_firstproductsecondrealdecode. (((ge_representation_real_code_prime_firstproductsecond) = 2 * ge_signed_half_prime_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_firstproductsecondreal) = 0) /\ (ge_balance_negative_prime_firstproductsecondreal) = S ge_signed_half_prime_firstproductsecondrealdecode))) /\ ((ge_second_rp_prime_firstproduct) + ge_balance_negative_prime_firstproductsecondreal = (ge_second_rn_prime_firstproduct) + ge_balance_positive_prime_firstproductsecondreal))) /\ (exists ge_balance_positive_prime_firstproductsecondimaginary ge_balance_negative_prime_firstproductsecondimaginary. (((((ge_representation_imaginary_code_prime_firstproductsecond) = 2 * (ge_balance_positive_prime_firstproductsecondimaginary) /\ (ge_balance_negative_prime_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_firstproductsecond) = 2 * ge_signed_half_prime_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_firstproductsecondimaginary) = S ge_signed_half_prime_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_firstproduct) + ge_balance_negative_prime_firstproductsecondimaginary = (ge_second_in_prime_firstproduct) + ge_balance_positive_prime_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_firstproductoutput ge_representation_imaginary_code_prime_firstproductoutput. (((a) = ((ge_representation_real_code_prime_firstproductoutput) + (ge_representation_imaginary_code_prime_firstproductoutput)) * S ((ge_representation_real_code_prime_firstproductoutput) + (ge_representation_imaginary_code_prime_firstproductoutput)) + ((ge_representation_imaginary_code_prime_firstproductoutput) + (ge_representation_imaginary_code_prime_firstproductoutput))) /\ ((exists ge_balance_positive_prime_firstproductoutputreal ge_balance_negative_prime_firstproductoutputreal. (((((ge_representation_real_code_prime_firstproductoutput) = 2 * (ge_balance_positive_prime_firstproductoutputreal) /\ (ge_balance_negative_prime_firstproductoutputreal) = 0) \/ exists ge_signed_half_prime_firstproductoutputrealdecode. (((ge_representation_real_code_prime_firstproductoutput) = 2 * ge_signed_half_prime_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_firstproductoutputreal) = 0) /\ (ge_balance_negative_prime_firstproductoutputreal) = S ge_signed_half_prime_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_firstproduct) * (ge_second_rp_prime_firstproduct))) + (((ge_first_rn_prime_firstproduct) * (ge_second_rn_prime_firstproduct))))) + (((((ge_first_ip_prime_firstproduct) * (ge_second_in_prime_firstproduct))) + (((ge_first_in_prime_firstproduct) * (ge_second_ip_prime_firstproduct))))))) + ge_balance_negative_prime_firstproductoutputreal = (((((((ge_first_rp_prime_firstproduct) * (ge_second_rn_prime_firstproduct))) + (((ge_first_rn_prime_firstproduct) * (ge_second_rp_prime_firstproduct))))) + (((((ge_first_ip_prime_firstproduct) * (ge_second_ip_prime_firstproduct))) + (((ge_first_in_prime_firstproduct) * (ge_second_in_prime_firstproduct))))))) + ge_balance_positive_prime_firstproductoutputreal))) /\ (exists ge_balance_positive_prime_firstproductoutputimaginary ge_balance_negative_prime_firstproductoutputimaginary. (((((ge_representation_imaginary_code_prime_firstproductoutput) = 2 * (ge_balance_positive_prime_firstproductoutputimaginary) /\ (ge_balance_negative_prime_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_firstproductoutput) = 2 * ge_signed_half_prime_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_firstproductoutputimaginary) = S ge_signed_half_prime_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_firstproduct) * (ge_second_ip_prime_firstproduct))) + (((ge_first_rn_prime_firstproduct) * (ge_second_in_prime_firstproduct))))) + (((((ge_first_ip_prime_firstproduct) * (ge_second_rp_prime_firstproduct))) + (((ge_first_in_prime_firstproduct) * (ge_second_rn_prime_firstproduct))))))) + ge_balance_negative_prime_firstproductoutputimaginary = (((((((ge_first_rp_prime_firstproduct) * (ge_second_in_prime_firstproduct))) + (((ge_first_rn_prime_firstproduct) * (ge_second_ip_prime_firstproduct))))) + (((((ge_first_ip_prime_firstproduct) * (ge_second_rn_prime_firstproduct))) + (((ge_first_in_prime_firstproduct) * (ge_second_rp_prime_firstproduct))))))) + ge_balance_positive_prime_firstproductoutputimaginary)))))))))) \/ (exists gr_quotient_prime_second. (exists ge_first_rp_prime_secondproduct ge_first_rn_prime_secondproduct ge_first_ip_prime_secondproduct ge_first_in_prime_secondproduct ge_second_rp_prime_secondproduct ge_second_rn_prime_secondproduct ge_second_ip_prime_secondproduct ge_second_in_prime_secondproduct. ((exists ge_representation_real_code_prime_secondproductfirst ge_representation_imaginary_code_prime_secondproductfirst. (((p) = ((ge_representation_real_code_prime_secondproductfirst) + (ge_representation_imaginary_code_prime_secondproductfirst)) * S ((ge_representation_real_code_prime_secondproductfirst) + (ge_representation_imaginary_code_prime_secondproductfirst)) + ((ge_representation_imaginary_code_prime_secondproductfirst) + (ge_representation_imaginary_code_prime_secondproductfirst))) /\ ((exists ge_balance_positive_prime_secondproductfirstreal ge_balance_negative_prime_secondproductfirstreal. (((((ge_representation_real_code_prime_secondproductfirst) = 2 * (ge_balance_positive_prime_secondproductfirstreal) /\ (ge_balance_negative_prime_secondproductfirstreal) = 0) \/ exists ge_signed_half_prime_secondproductfirstrealdecode. (((ge_representation_real_code_prime_secondproductfirst) = 2 * ge_signed_half_prime_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_prime_secondproductfirstreal) = 0) /\ (ge_balance_negative_prime_secondproductfirstreal) = S ge_signed_half_prime_secondproductfirstrealdecode))) /\ ((ge_first_rp_prime_secondproduct) + ge_balance_negative_prime_secondproductfirstreal = (ge_first_rn_prime_secondproduct) + ge_balance_positive_prime_secondproductfirstreal))) /\ (exists ge_balance_positive_prime_secondproductfirstimaginary ge_balance_negative_prime_secondproductfirstimaginary. (((((ge_representation_imaginary_code_prime_secondproductfirst) = 2 * (ge_balance_positive_prime_secondproductfirstimaginary) /\ (ge_balance_negative_prime_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_prime_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_prime_secondproductfirst) = 2 * ge_signed_half_prime_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_prime_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_prime_secondproductfirstimaginary) = S ge_signed_half_prime_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_prime_secondproduct) + ge_balance_negative_prime_secondproductfirstimaginary = (ge_first_in_prime_secondproduct) + ge_balance_positive_prime_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_prime_secondproductsecond ge_representation_imaginary_code_prime_secondproductsecond. (((gr_quotient_prime_second) = ((ge_representation_real_code_prime_secondproductsecond) + (ge_representation_imaginary_code_prime_secondproductsecond)) * S ((ge_representation_real_code_prime_secondproductsecond) + (ge_representation_imaginary_code_prime_secondproductsecond)) + ((ge_representation_imaginary_code_prime_secondproductsecond) + (ge_representation_imaginary_code_prime_secondproductsecond))) /\ ((exists ge_balance_positive_prime_secondproductsecondreal ge_balance_negative_prime_secondproductsecondreal. (((((ge_representation_real_code_prime_secondproductsecond) = 2 * (ge_balance_positive_prime_secondproductsecondreal) /\ (ge_balance_negative_prime_secondproductsecondreal) = 0) \/ exists ge_signed_half_prime_secondproductsecondrealdecode. (((ge_representation_real_code_prime_secondproductsecond) = 2 * ge_signed_half_prime_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_prime_secondproductsecondreal) = 0) /\ (ge_balance_negative_prime_secondproductsecondreal) = S ge_signed_half_prime_secondproductsecondrealdecode))) /\ ((ge_second_rp_prime_secondproduct) + ge_balance_negative_prime_secondproductsecondreal = (ge_second_rn_prime_secondproduct) + ge_balance_positive_prime_secondproductsecondreal))) /\ (exists ge_balance_positive_prime_secondproductsecondimaginary ge_balance_negative_prime_secondproductsecondimaginary. (((((ge_representation_imaginary_code_prime_secondproductsecond) = 2 * (ge_balance_positive_prime_secondproductsecondimaginary) /\ (ge_balance_negative_prime_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_prime_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_prime_secondproductsecond) = 2 * ge_signed_half_prime_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_prime_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_prime_secondproductsecondimaginary) = S ge_signed_half_prime_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_prime_secondproduct) + ge_balance_negative_prime_secondproductsecondimaginary = (ge_second_in_prime_secondproduct) + ge_balance_positive_prime_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_prime_secondproductoutput ge_representation_imaginary_code_prime_secondproductoutput. (((b) = ((ge_representation_real_code_prime_secondproductoutput) + (ge_representation_imaginary_code_prime_secondproductoutput)) * S ((ge_representation_real_code_prime_secondproductoutput) + (ge_representation_imaginary_code_prime_secondproductoutput)) + ((ge_representation_imaginary_code_prime_secondproductoutput) + (ge_representation_imaginary_code_prime_secondproductoutput))) /\ ((exists ge_balance_positive_prime_secondproductoutputreal ge_balance_negative_prime_secondproductoutputreal. (((((ge_representation_real_code_prime_secondproductoutput) = 2 * (ge_balance_positive_prime_secondproductoutputreal) /\ (ge_balance_negative_prime_secondproductoutputreal) = 0) \/ exists ge_signed_half_prime_secondproductoutputrealdecode. (((ge_representation_real_code_prime_secondproductoutput) = 2 * ge_signed_half_prime_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_prime_secondproductoutputreal) = 0) /\ (ge_balance_negative_prime_secondproductoutputreal) = S ge_signed_half_prime_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_prime_secondproduct) * (ge_second_rp_prime_secondproduct))) + (((ge_first_rn_prime_secondproduct) * (ge_second_rn_prime_secondproduct))))) + (((((ge_first_ip_prime_secondproduct) * (ge_second_in_prime_secondproduct))) + (((ge_first_in_prime_secondproduct) * (ge_second_ip_prime_secondproduct))))))) + ge_balance_negative_prime_secondproductoutputreal = (((((((ge_first_rp_prime_secondproduct) * (ge_second_rn_prime_secondproduct))) + (((ge_first_rn_prime_secondproduct) * (ge_second_rp_prime_secondproduct))))) + (((((ge_first_ip_prime_secondproduct) * (ge_second_ip_prime_secondproduct))) + (((ge_first_in_prime_secondproduct) * (ge_second_in_prime_secondproduct))))))) + ge_balance_positive_prime_secondproductoutputreal))) /\ (exists ge_balance_positive_prime_secondproductoutputimaginary ge_balance_negative_prime_secondproductoutputimaginary. (((((ge_representation_imaginary_code_prime_secondproductoutput) = 2 * (ge_balance_positive_prime_secondproductoutputimaginary) /\ (ge_balance_negative_prime_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_prime_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_prime_secondproductoutput) = 2 * ge_signed_half_prime_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_prime_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_prime_secondproductoutputimaginary) = S ge_signed_half_prime_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_prime_secondproduct) * (ge_second_ip_prime_secondproduct))) + (((ge_first_rn_prime_secondproduct) * (ge_second_in_prime_secondproduct))))) + (((((ge_first_ip_prime_secondproduct) * (ge_second_rp_prime_secondproduct))) + (((ge_first_in_prime_secondproduct) * (ge_second_rn_prime_secondproduct))))))) + ge_balance_negative_prime_secondproductoutputimaginary = (((((((ge_first_rp_prime_secondproduct) * (ge_second_in_prime_secondproduct))) + (((ge_first_rn_prime_secondproduct) * (ge_second_ip_prime_secondproduct))))) + (((((ge_first_ip_prime_secondproduct) * (ge_second_rn_prime_secondproduct))) + (((ge_first_in_prime_secondproduct) * (ge_second_rp_prime_secondproduct))))))) + ge_balance_positive_prime_secondproductoutputimaginary))))))))))