gaussian_associate_transitive

Exact expanded first-order arithmetic statement

forall a b c. (exists gr_unit_associate_first. ((exists gr_inverse_associate_firstunit. (exists ge_first_rp_associate_firstunitidentity ge_first_rn_associate_firstunitidentity ge_first_ip_associate_firstunitidentity ge_first_in_associate_firstunitidentity ge_second_rp_associate_firstunitidentity ge_second_rn_associate_firstunitidentity ge_second_ip_associate_firstunitidentity ge_second_in_associate_firstunitidentity. ((exists ge_representation_real_code_associate_firstunitidentityfirst ge_representation_imaginary_code_associate_firstunitidentityfirst. (((gr_unit_associate_first) = ((ge_representation_real_code_associate_firstunitidentityfirst) + (ge_representation_imaginary_code_associate_firstunitidentityfirst)) * S ((ge_representation_real_code_associate_firstunitidentityfirst) + (ge_representation_imaginary_code_associate_firstunitidentityfirst)) + ((ge_representation_imaginary_code_associate_firstunitidentityfirst) + (ge_representation_imaginary_code_associate_firstunitidentityfirst))) /\ ((exists ge_balance_positive_associate_firstunitidentityfirstreal ge_balance_negative_associate_firstunitidentityfirstreal. (((((ge_representation_real_code_associate_firstunitidentityfirst) = 2 * (ge_balance_positive_associate_firstunitidentityfirstreal) /\ (ge_balance_negative_associate_firstunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_firstunitidentityfirstrealdecode. (((ge_representation_real_code_associate_firstunitidentityfirst) = 2 * ge_signed_half_associate_firstunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_firstunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_firstunitidentityfirstreal) = S ge_signed_half_associate_firstunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_firstunitidentity) + ge_balance_negative_associate_firstunitidentityfirstreal = (ge_first_rn_associate_firstunitidentity) + ge_balance_positive_associate_firstunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_firstunitidentityfirstimaginary ge_balance_negative_associate_firstunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_firstunitidentityfirst) = 2 * (ge_balance_positive_associate_firstunitidentityfirstimaginary) /\ (ge_balance_negative_associate_firstunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_firstunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_firstunitidentityfirst) = 2 * ge_signed_half_associate_firstunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_firstunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_firstunitidentityfirstimaginary) = S ge_signed_half_associate_firstunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_firstunitidentity) + ge_balance_negative_associate_firstunitidentityfirstimaginary = (ge_first_in_associate_firstunitidentity) + ge_balance_positive_associate_firstunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_firstunitidentitysecond ge_representation_imaginary_code_associate_firstunitidentitysecond. (((gr_inverse_associate_firstunit) = ((ge_representation_real_code_associate_firstunitidentitysecond) + (ge_representation_imaginary_code_associate_firstunitidentitysecond)) * S ((ge_representation_real_code_associate_firstunitidentitysecond) + (ge_representation_imaginary_code_associate_firstunitidentitysecond)) + ((ge_representation_imaginary_code_associate_firstunitidentitysecond) + (ge_representation_imaginary_code_associate_firstunitidentitysecond))) /\ ((exists ge_balance_positive_associate_firstunitidentitysecondreal ge_balance_negative_associate_firstunitidentitysecondreal. (((((ge_representation_real_code_associate_firstunitidentitysecond) = 2 * (ge_balance_positive_associate_firstunitidentitysecondreal) /\ (ge_balance_negative_associate_firstunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_firstunitidentitysecondrealdecode. (((ge_representation_real_code_associate_firstunitidentitysecond) = 2 * ge_signed_half_associate_firstunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_firstunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_firstunitidentitysecondreal) = S ge_signed_half_associate_firstunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_firstunitidentity) + ge_balance_negative_associate_firstunitidentitysecondreal = (ge_second_rn_associate_firstunitidentity) + ge_balance_positive_associate_firstunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_firstunitidentitysecondimaginary ge_balance_negative_associate_firstunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_firstunitidentitysecond) = 2 * (ge_balance_positive_associate_firstunitidentitysecondimaginary) /\ (ge_balance_negative_associate_firstunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_firstunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_firstunitidentitysecond) = 2 * ge_signed_half_associate_firstunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_firstunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_firstunitidentitysecondimaginary) = S ge_signed_half_associate_firstunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_firstunitidentity) + ge_balance_negative_associate_firstunitidentitysecondimaginary = (ge_second_in_associate_firstunitidentity) + ge_balance_positive_associate_firstunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_firstunitidentityoutput ge_representation_imaginary_code_associate_firstunitidentityoutput. (((6) = ((ge_representation_real_code_associate_firstunitidentityoutput) + (ge_representation_imaginary_code_associate_firstunitidentityoutput)) * S ((ge_representation_real_code_associate_firstunitidentityoutput) + (ge_representation_imaginary_code_associate_firstunitidentityoutput)) + ((ge_representation_imaginary_code_associate_firstunitidentityoutput) + (ge_representation_imaginary_code_associate_firstunitidentityoutput))) /\ ((exists ge_balance_positive_associate_firstunitidentityoutputreal ge_balance_negative_associate_firstunitidentityoutputreal. (((((ge_representation_real_code_associate_firstunitidentityoutput) = 2 * (ge_balance_positive_associate_firstunitidentityoutputreal) /\ (ge_balance_negative_associate_firstunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_firstunitidentityoutputrealdecode. (((ge_representation_real_code_associate_firstunitidentityoutput) = 2 * ge_signed_half_associate_firstunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_firstunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_firstunitidentityoutputreal) = S ge_signed_half_associate_firstunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_firstunitidentity) * (ge_second_rp_associate_firstunitidentity))) + (((ge_first_rn_associate_firstunitidentity) * (ge_second_rn_associate_firstunitidentity))))) + (((((ge_first_ip_associate_firstunitidentity) * (ge_second_in_associate_firstunitidentity))) + (((ge_first_in_associate_firstunitidentity) * (ge_second_ip_associate_firstunitidentity))))))) + ge_balance_negative_associate_firstunitidentityoutputreal = (((((((ge_first_rp_associate_firstunitidentity) * (ge_second_rn_associate_firstunitidentity))) + (((ge_first_rn_associate_firstunitidentity) * (ge_second_rp_associate_firstunitidentity))))) + (((((ge_first_ip_associate_firstunitidentity) * (ge_second_ip_associate_firstunitidentity))) + (((ge_first_in_associate_firstunitidentity) * (ge_second_in_associate_firstunitidentity))))))) + ge_balance_positive_associate_firstunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_firstunitidentityoutputimaginary ge_balance_negative_associate_firstunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_firstunitidentityoutput) = 2 * (ge_balance_positive_associate_firstunitidentityoutputimaginary) /\ (ge_balance_negative_associate_firstunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_firstunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_firstunitidentityoutput) = 2 * ge_signed_half_associate_firstunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_firstunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_firstunitidentityoutputimaginary) = S ge_signed_half_associate_firstunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_firstunitidentity) * (ge_second_ip_associate_firstunitidentity))) + (((ge_first_rn_associate_firstunitidentity) * (ge_second_in_associate_firstunitidentity))))) + (((((ge_first_ip_associate_firstunitidentity) * (ge_second_rp_associate_firstunitidentity))) + (((ge_first_in_associate_firstunitidentity) * (ge_second_rn_associate_firstunitidentity))))))) + ge_balance_negative_associate_firstunitidentityoutputimaginary = (((((((ge_first_rp_associate_firstunitidentity) * (ge_second_in_associate_firstunitidentity))) + (((ge_first_rn_associate_firstunitidentity) * (ge_second_ip_associate_firstunitidentity))))) + (((((ge_first_ip_associate_firstunitidentity) * (ge_second_rn_associate_firstunitidentity))) + (((ge_first_in_associate_firstunitidentity) * (ge_second_rp_associate_firstunitidentity))))))) + ge_balance_positive_associate_firstunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_firsttransport ge_first_rn_associate_firsttransport ge_first_ip_associate_firsttransport ge_first_in_associate_firsttransport ge_second_rp_associate_firsttransport ge_second_rn_associate_firsttransport ge_second_ip_associate_firsttransport ge_second_in_associate_firsttransport. ((exists ge_representation_real_code_associate_firsttransportfirst ge_representation_imaginary_code_associate_firsttransportfirst. (((gr_unit_associate_first) = ((ge_representation_real_code_associate_firsttransportfirst) + (ge_representation_imaginary_code_associate_firsttransportfirst)) * S ((ge_representation_real_code_associate_firsttransportfirst) + (ge_representation_imaginary_code_associate_firsttransportfirst)) + ((ge_representation_imaginary_code_associate_firsttransportfirst) + (ge_representation_imaginary_code_associate_firsttransportfirst))) /\ ((exists ge_balance_positive_associate_firsttransportfirstreal ge_balance_negative_associate_firsttransportfirstreal. (((((ge_representation_real_code_associate_firsttransportfirst) = 2 * (ge_balance_positive_associate_firsttransportfirstreal) /\ (ge_balance_negative_associate_firsttransportfirstreal) = 0) \/ exists ge_signed_half_associate_firsttransportfirstrealdecode. (((ge_representation_real_code_associate_firsttransportfirst) = 2 * ge_signed_half_associate_firsttransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_firsttransportfirstreal) = 0) /\ (ge_balance_negative_associate_firsttransportfirstreal) = S ge_signed_half_associate_firsttransportfirstrealdecode))) /\ ((ge_first_rp_associate_firsttransport) + ge_balance_negative_associate_firsttransportfirstreal = (ge_first_rn_associate_firsttransport) + ge_balance_positive_associate_firsttransportfirstreal))) /\ (exists ge_balance_positive_associate_firsttransportfirstimaginary ge_balance_negative_associate_firsttransportfirstimaginary. (((((ge_representation_imaginary_code_associate_firsttransportfirst) = 2 * (ge_balance_positive_associate_firsttransportfirstimaginary) /\ (ge_balance_negative_associate_firsttransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_firsttransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_firsttransportfirst) = 2 * ge_signed_half_associate_firsttransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_firsttransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_firsttransportfirstimaginary) = S ge_signed_half_associate_firsttransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_firsttransport) + ge_balance_negative_associate_firsttransportfirstimaginary = (ge_first_in_associate_firsttransport) + ge_balance_positive_associate_firsttransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_firsttransportsecond ge_representation_imaginary_code_associate_firsttransportsecond. (((a) = ((ge_representation_real_code_associate_firsttransportsecond) + (ge_representation_imaginary_code_associate_firsttransportsecond)) * S ((ge_representation_real_code_associate_firsttransportsecond) + (ge_representation_imaginary_code_associate_firsttransportsecond)) + ((ge_representation_imaginary_code_associate_firsttransportsecond) + (ge_representation_imaginary_code_associate_firsttransportsecond))) /\ ((exists ge_balance_positive_associate_firsttransportsecondreal ge_balance_negative_associate_firsttransportsecondreal. (((((ge_representation_real_code_associate_firsttransportsecond) = 2 * (ge_balance_positive_associate_firsttransportsecondreal) /\ (ge_balance_negative_associate_firsttransportsecondreal) = 0) \/ exists ge_signed_half_associate_firsttransportsecondrealdecode. (((ge_representation_real_code_associate_firsttransportsecond) = 2 * ge_signed_half_associate_firsttransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_firsttransportsecondreal) = 0) /\ (ge_balance_negative_associate_firsttransportsecondreal) = S ge_signed_half_associate_firsttransportsecondrealdecode))) /\ ((ge_second_rp_associate_firsttransport) + ge_balance_negative_associate_firsttransportsecondreal = (ge_second_rn_associate_firsttransport) + ge_balance_positive_associate_firsttransportsecondreal))) /\ (exists ge_balance_positive_associate_firsttransportsecondimaginary ge_balance_negative_associate_firsttransportsecondimaginary. (((((ge_representation_imaginary_code_associate_firsttransportsecond) = 2 * (ge_balance_positive_associate_firsttransportsecondimaginary) /\ (ge_balance_negative_associate_firsttransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_firsttransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_firsttransportsecond) = 2 * ge_signed_half_associate_firsttransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_firsttransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_firsttransportsecondimaginary) = S ge_signed_half_associate_firsttransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_firsttransport) + ge_balance_negative_associate_firsttransportsecondimaginary = (ge_second_in_associate_firsttransport) + ge_balance_positive_associate_firsttransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_firsttransportoutput ge_representation_imaginary_code_associate_firsttransportoutput. (((b) = ((ge_representation_real_code_associate_firsttransportoutput) + (ge_representation_imaginary_code_associate_firsttransportoutput)) * S ((ge_representation_real_code_associate_firsttransportoutput) + (ge_representation_imaginary_code_associate_firsttransportoutput)) + ((ge_representation_imaginary_code_associate_firsttransportoutput) + (ge_representation_imaginary_code_associate_firsttransportoutput))) /\ ((exists ge_balance_positive_associate_firsttransportoutputreal ge_balance_negative_associate_firsttransportoutputreal. (((((ge_representation_real_code_associate_firsttransportoutput) = 2 * (ge_balance_positive_associate_firsttransportoutputreal) /\ (ge_balance_negative_associate_firsttransportoutputreal) = 0) \/ exists ge_signed_half_associate_firsttransportoutputrealdecode. (((ge_representation_real_code_associate_firsttransportoutput) = 2 * ge_signed_half_associate_firsttransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_firsttransportoutputreal) = 0) /\ (ge_balance_negative_associate_firsttransportoutputreal) = S ge_signed_half_associate_firsttransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_firsttransport) * (ge_second_rp_associate_firsttransport))) + (((ge_first_rn_associate_firsttransport) * (ge_second_rn_associate_firsttransport))))) + (((((ge_first_ip_associate_firsttransport) * (ge_second_in_associate_firsttransport))) + (((ge_first_in_associate_firsttransport) * (ge_second_ip_associate_firsttransport))))))) + ge_balance_negative_associate_firsttransportoutputreal = (((((((ge_first_rp_associate_firsttransport) * (ge_second_rn_associate_firsttransport))) + (((ge_first_rn_associate_firsttransport) * (ge_second_rp_associate_firsttransport))))) + (((((ge_first_ip_associate_firsttransport) * (ge_second_ip_associate_firsttransport))) + (((ge_first_in_associate_firsttransport) * (ge_second_in_associate_firsttransport))))))) + ge_balance_positive_associate_firsttransportoutputreal))) /\ (exists ge_balance_positive_associate_firsttransportoutputimaginary ge_balance_negative_associate_firsttransportoutputimaginary. (((((ge_representation_imaginary_code_associate_firsttransportoutput) = 2 * (ge_balance_positive_associate_firsttransportoutputimaginary) /\ (ge_balance_negative_associate_firsttransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_firsttransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_firsttransportoutput) = 2 * ge_signed_half_associate_firsttransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_firsttransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_firsttransportoutputimaginary) = S ge_signed_half_associate_firsttransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_firsttransport) * (ge_second_ip_associate_firsttransport))) + (((ge_first_rn_associate_firsttransport) * (ge_second_in_associate_firsttransport))))) + (((((ge_first_ip_associate_firsttransport) * (ge_second_rp_associate_firsttransport))) + (((ge_first_in_associate_firsttransport) * (ge_second_rn_associate_firsttransport))))))) + ge_balance_negative_associate_firsttransportoutputimaginary = (((((((ge_first_rp_associate_firsttransport) * (ge_second_in_associate_firsttransport))) + (((ge_first_rn_associate_firsttransport) * (ge_second_ip_associate_firsttransport))))) + (((((ge_first_ip_associate_firsttransport) * (ge_second_rn_associate_firsttransport))) + (((ge_first_in_associate_firsttransport) * (ge_second_rp_associate_firsttransport))))))) + ge_balance_positive_associate_firsttransportoutputimaginary))))))))))) -> (exists gr_unit_associate_second. ((exists gr_inverse_associate_secondunit. (exists ge_first_rp_associate_secondunitidentity ge_first_rn_associate_secondunitidentity ge_first_ip_associate_secondunitidentity ge_first_in_associate_secondunitidentity ge_second_rp_associate_secondunitidentity ge_second_rn_associate_secondunitidentity ge_second_ip_associate_secondunitidentity ge_second_in_associate_secondunitidentity. ((exists ge_representation_real_code_associate_secondunitidentityfirst ge_representation_imaginary_code_associate_secondunitidentityfirst. (((gr_unit_associate_second) = ((ge_representation_real_code_associate_secondunitidentityfirst) + (ge_representation_imaginary_code_associate_secondunitidentityfirst)) * S ((ge_representation_real_code_associate_secondunitidentityfirst) + (ge_representation_imaginary_code_associate_secondunitidentityfirst)) + ((ge_representation_imaginary_code_associate_secondunitidentityfirst) + (ge_representation_imaginary_code_associate_secondunitidentityfirst))) /\ ((exists ge_balance_positive_associate_secondunitidentityfirstreal ge_balance_negative_associate_secondunitidentityfirstreal. (((((ge_representation_real_code_associate_secondunitidentityfirst) = 2 * (ge_balance_positive_associate_secondunitidentityfirstreal) /\ (ge_balance_negative_associate_secondunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_secondunitidentityfirstrealdecode. (((ge_representation_real_code_associate_secondunitidentityfirst) = 2 * ge_signed_half_associate_secondunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_secondunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_secondunitidentityfirstreal) = S ge_signed_half_associate_secondunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_secondunitidentity) + ge_balance_negative_associate_secondunitidentityfirstreal = (ge_first_rn_associate_secondunitidentity) + ge_balance_positive_associate_secondunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_secondunitidentityfirstimaginary ge_balance_negative_associate_secondunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_secondunitidentityfirst) = 2 * (ge_balance_positive_associate_secondunitidentityfirstimaginary) /\ (ge_balance_negative_associate_secondunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_secondunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_secondunitidentityfirst) = 2 * ge_signed_half_associate_secondunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_secondunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_secondunitidentityfirstimaginary) = S ge_signed_half_associate_secondunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_secondunitidentity) + ge_balance_negative_associate_secondunitidentityfirstimaginary = (ge_first_in_associate_secondunitidentity) + ge_balance_positive_associate_secondunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_secondunitidentitysecond ge_representation_imaginary_code_associate_secondunitidentitysecond. (((gr_inverse_associate_secondunit) = ((ge_representation_real_code_associate_secondunitidentitysecond) + (ge_representation_imaginary_code_associate_secondunitidentitysecond)) * S ((ge_representation_real_code_associate_secondunitidentitysecond) + (ge_representation_imaginary_code_associate_secondunitidentitysecond)) + ((ge_representation_imaginary_code_associate_secondunitidentitysecond) + (ge_representation_imaginary_code_associate_secondunitidentitysecond))) /\ ((exists ge_balance_positive_associate_secondunitidentitysecondreal ge_balance_negative_associate_secondunitidentitysecondreal. (((((ge_representation_real_code_associate_secondunitidentitysecond) = 2 * (ge_balance_positive_associate_secondunitidentitysecondreal) /\ (ge_balance_negative_associate_secondunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_secondunitidentitysecondrealdecode. (((ge_representation_real_code_associate_secondunitidentitysecond) = 2 * ge_signed_half_associate_secondunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_secondunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_secondunitidentitysecondreal) = S ge_signed_half_associate_secondunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_secondunitidentity) + ge_balance_negative_associate_secondunitidentitysecondreal = (ge_second_rn_associate_secondunitidentity) + ge_balance_positive_associate_secondunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_secondunitidentitysecondimaginary ge_balance_negative_associate_secondunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_secondunitidentitysecond) = 2 * (ge_balance_positive_associate_secondunitidentitysecondimaginary) /\ (ge_balance_negative_associate_secondunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_secondunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_secondunitidentitysecond) = 2 * ge_signed_half_associate_secondunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_secondunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_secondunitidentitysecondimaginary) = S ge_signed_half_associate_secondunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_secondunitidentity) + ge_balance_negative_associate_secondunitidentitysecondimaginary = (ge_second_in_associate_secondunitidentity) + ge_balance_positive_associate_secondunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_secondunitidentityoutput ge_representation_imaginary_code_associate_secondunitidentityoutput. (((6) = ((ge_representation_real_code_associate_secondunitidentityoutput) + (ge_representation_imaginary_code_associate_secondunitidentityoutput)) * S ((ge_representation_real_code_associate_secondunitidentityoutput) + (ge_representation_imaginary_code_associate_secondunitidentityoutput)) + ((ge_representation_imaginary_code_associate_secondunitidentityoutput) + (ge_representation_imaginary_code_associate_secondunitidentityoutput))) /\ ((exists ge_balance_positive_associate_secondunitidentityoutputreal ge_balance_negative_associate_secondunitidentityoutputreal. (((((ge_representation_real_code_associate_secondunitidentityoutput) = 2 * (ge_balance_positive_associate_secondunitidentityoutputreal) /\ (ge_balance_negative_associate_secondunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_secondunitidentityoutputrealdecode. (((ge_representation_real_code_associate_secondunitidentityoutput) = 2 * ge_signed_half_associate_secondunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_secondunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_secondunitidentityoutputreal) = S ge_signed_half_associate_secondunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_secondunitidentity) * (ge_second_rp_associate_secondunitidentity))) + (((ge_first_rn_associate_secondunitidentity) * (ge_second_rn_associate_secondunitidentity))))) + (((((ge_first_ip_associate_secondunitidentity) * (ge_second_in_associate_secondunitidentity))) + (((ge_first_in_associate_secondunitidentity) * (ge_second_ip_associate_secondunitidentity))))))) + ge_balance_negative_associate_secondunitidentityoutputreal = (((((((ge_first_rp_associate_secondunitidentity) * (ge_second_rn_associate_secondunitidentity))) + (((ge_first_rn_associate_secondunitidentity) * (ge_second_rp_associate_secondunitidentity))))) + (((((ge_first_ip_associate_secondunitidentity) * (ge_second_ip_associate_secondunitidentity))) + (((ge_first_in_associate_secondunitidentity) * (ge_second_in_associate_secondunitidentity))))))) + ge_balance_positive_associate_secondunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_secondunitidentityoutputimaginary ge_balance_negative_associate_secondunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_secondunitidentityoutput) = 2 * (ge_balance_positive_associate_secondunitidentityoutputimaginary) /\ (ge_balance_negative_associate_secondunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_secondunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_secondunitidentityoutput) = 2 * ge_signed_half_associate_secondunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_secondunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_secondunitidentityoutputimaginary) = S ge_signed_half_associate_secondunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_secondunitidentity) * (ge_second_ip_associate_secondunitidentity))) + (((ge_first_rn_associate_secondunitidentity) * (ge_second_in_associate_secondunitidentity))))) + (((((ge_first_ip_associate_secondunitidentity) * (ge_second_rp_associate_secondunitidentity))) + (((ge_first_in_associate_secondunitidentity) * (ge_second_rn_associate_secondunitidentity))))))) + ge_balance_negative_associate_secondunitidentityoutputimaginary = (((((((ge_first_rp_associate_secondunitidentity) * (ge_second_in_associate_secondunitidentity))) + (((ge_first_rn_associate_secondunitidentity) * (ge_second_ip_associate_secondunitidentity))))) + (((((ge_first_ip_associate_secondunitidentity) * (ge_second_rn_associate_secondunitidentity))) + (((ge_first_in_associate_secondunitidentity) * (ge_second_rp_associate_secondunitidentity))))))) + ge_balance_positive_associate_secondunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_secondtransport ge_first_rn_associate_secondtransport ge_first_ip_associate_secondtransport ge_first_in_associate_secondtransport ge_second_rp_associate_secondtransport ge_second_rn_associate_secondtransport ge_second_ip_associate_secondtransport ge_second_in_associate_secondtransport. ((exists ge_representation_real_code_associate_secondtransportfirst ge_representation_imaginary_code_associate_secondtransportfirst. (((gr_unit_associate_second) = ((ge_representation_real_code_associate_secondtransportfirst) + (ge_representation_imaginary_code_associate_secondtransportfirst)) * S ((ge_representation_real_code_associate_secondtransportfirst) + (ge_representation_imaginary_code_associate_secondtransportfirst)) + ((ge_representation_imaginary_code_associate_secondtransportfirst) + (ge_representation_imaginary_code_associate_secondtransportfirst))) /\ ((exists ge_balance_positive_associate_secondtransportfirstreal ge_balance_negative_associate_secondtransportfirstreal. (((((ge_representation_real_code_associate_secondtransportfirst) = 2 * (ge_balance_positive_associate_secondtransportfirstreal) /\ (ge_balance_negative_associate_secondtransportfirstreal) = 0) \/ exists ge_signed_half_associate_secondtransportfirstrealdecode. (((ge_representation_real_code_associate_secondtransportfirst) = 2 * ge_signed_half_associate_secondtransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_secondtransportfirstreal) = 0) /\ (ge_balance_negative_associate_secondtransportfirstreal) = S ge_signed_half_associate_secondtransportfirstrealdecode))) /\ ((ge_first_rp_associate_secondtransport) + ge_balance_negative_associate_secondtransportfirstreal = (ge_first_rn_associate_secondtransport) + ge_balance_positive_associate_secondtransportfirstreal))) /\ (exists ge_balance_positive_associate_secondtransportfirstimaginary ge_balance_negative_associate_secondtransportfirstimaginary. (((((ge_representation_imaginary_code_associate_secondtransportfirst) = 2 * (ge_balance_positive_associate_secondtransportfirstimaginary) /\ (ge_balance_negative_associate_secondtransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_secondtransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_secondtransportfirst) = 2 * ge_signed_half_associate_secondtransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_secondtransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_secondtransportfirstimaginary) = S ge_signed_half_associate_secondtransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_secondtransport) + ge_balance_negative_associate_secondtransportfirstimaginary = (ge_first_in_associate_secondtransport) + ge_balance_positive_associate_secondtransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_secondtransportsecond ge_representation_imaginary_code_associate_secondtransportsecond. (((b) = ((ge_representation_real_code_associate_secondtransportsecond) + (ge_representation_imaginary_code_associate_secondtransportsecond)) * S ((ge_representation_real_code_associate_secondtransportsecond) + (ge_representation_imaginary_code_associate_secondtransportsecond)) + ((ge_representation_imaginary_code_associate_secondtransportsecond) + (ge_representation_imaginary_code_associate_secondtransportsecond))) /\ ((exists ge_balance_positive_associate_secondtransportsecondreal ge_balance_negative_associate_secondtransportsecondreal. (((((ge_representation_real_code_associate_secondtransportsecond) = 2 * (ge_balance_positive_associate_secondtransportsecondreal) /\ (ge_balance_negative_associate_secondtransportsecondreal) = 0) \/ exists ge_signed_half_associate_secondtransportsecondrealdecode. (((ge_representation_real_code_associate_secondtransportsecond) = 2 * ge_signed_half_associate_secondtransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_secondtransportsecondreal) = 0) /\ (ge_balance_negative_associate_secondtransportsecondreal) = S ge_signed_half_associate_secondtransportsecondrealdecode))) /\ ((ge_second_rp_associate_secondtransport) + ge_balance_negative_associate_secondtransportsecondreal = (ge_second_rn_associate_secondtransport) + ge_balance_positive_associate_secondtransportsecondreal))) /\ (exists ge_balance_positive_associate_secondtransportsecondimaginary ge_balance_negative_associate_secondtransportsecondimaginary. (((((ge_representation_imaginary_code_associate_secondtransportsecond) = 2 * (ge_balance_positive_associate_secondtransportsecondimaginary) /\ (ge_balance_negative_associate_secondtransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_secondtransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_secondtransportsecond) = 2 * ge_signed_half_associate_secondtransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_secondtransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_secondtransportsecondimaginary) = S ge_signed_half_associate_secondtransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_secondtransport) + ge_balance_negative_associate_secondtransportsecondimaginary = (ge_second_in_associate_secondtransport) + ge_balance_positive_associate_secondtransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_secondtransportoutput ge_representation_imaginary_code_associate_secondtransportoutput. (((c) = ((ge_representation_real_code_associate_secondtransportoutput) + (ge_representation_imaginary_code_associate_secondtransportoutput)) * S ((ge_representation_real_code_associate_secondtransportoutput) + (ge_representation_imaginary_code_associate_secondtransportoutput)) + ((ge_representation_imaginary_code_associate_secondtransportoutput) + (ge_representation_imaginary_code_associate_secondtransportoutput))) /\ ((exists ge_balance_positive_associate_secondtransportoutputreal ge_balance_negative_associate_secondtransportoutputreal. (((((ge_representation_real_code_associate_secondtransportoutput) = 2 * (ge_balance_positive_associate_secondtransportoutputreal) /\ (ge_balance_negative_associate_secondtransportoutputreal) = 0) \/ exists ge_signed_half_associate_secondtransportoutputrealdecode. (((ge_representation_real_code_associate_secondtransportoutput) = 2 * ge_signed_half_associate_secondtransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_secondtransportoutputreal) = 0) /\ (ge_balance_negative_associate_secondtransportoutputreal) = S ge_signed_half_associate_secondtransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_secondtransport) * (ge_second_rp_associate_secondtransport))) + (((ge_first_rn_associate_secondtransport) * (ge_second_rn_associate_secondtransport))))) + (((((ge_first_ip_associate_secondtransport) * (ge_second_in_associate_secondtransport))) + (((ge_first_in_associate_secondtransport) * (ge_second_ip_associate_secondtransport))))))) + ge_balance_negative_associate_secondtransportoutputreal = (((((((ge_first_rp_associate_secondtransport) * (ge_second_rn_associate_secondtransport))) + (((ge_first_rn_associate_secondtransport) * (ge_second_rp_associate_secondtransport))))) + (((((ge_first_ip_associate_secondtransport) * (ge_second_ip_associate_secondtransport))) + (((ge_first_in_associate_secondtransport) * (ge_second_in_associate_secondtransport))))))) + ge_balance_positive_associate_secondtransportoutputreal))) /\ (exists ge_balance_positive_associate_secondtransportoutputimaginary ge_balance_negative_associate_secondtransportoutputimaginary. (((((ge_representation_imaginary_code_associate_secondtransportoutput) = 2 * (ge_balance_positive_associate_secondtransportoutputimaginary) /\ (ge_balance_negative_associate_secondtransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_secondtransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_secondtransportoutput) = 2 * ge_signed_half_associate_secondtransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_secondtransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_secondtransportoutputimaginary) = S ge_signed_half_associate_secondtransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_secondtransport) * (ge_second_ip_associate_secondtransport))) + (((ge_first_rn_associate_secondtransport) * (ge_second_in_associate_secondtransport))))) + (((((ge_first_ip_associate_secondtransport) * (ge_second_rp_associate_secondtransport))) + (((ge_first_in_associate_secondtransport) * (ge_second_rn_associate_secondtransport))))))) + ge_balance_negative_associate_secondtransportoutputimaginary = (((((((ge_first_rp_associate_secondtransport) * (ge_second_in_associate_secondtransport))) + (((ge_first_rn_associate_secondtransport) * (ge_second_ip_associate_secondtransport))))) + (((((ge_first_ip_associate_secondtransport) * (ge_second_rn_associate_secondtransport))) + (((ge_first_in_associate_secondtransport) * (ge_second_rp_associate_secondtransport))))))) + ge_balance_positive_associate_secondtransportoutputimaginary))))))))))) -> (exists gr_unit_associate_composite. ((exists gr_inverse_associate_compositeunit. (exists ge_first_rp_associate_compositeunitidentity ge_first_rn_associate_compositeunitidentity ge_first_ip_associate_compositeunitidentity ge_first_in_associate_compositeunitidentity ge_second_rp_associate_compositeunitidentity ge_second_rn_associate_compositeunitidentity ge_second_ip_associate_compositeunitidentity ge_second_in_associate_compositeunitidentity. ((exists ge_representation_real_code_associate_compositeunitidentityfirst ge_representation_imaginary_code_associate_compositeunitidentityfirst. (((gr_unit_associate_composite) = ((ge_representation_real_code_associate_compositeunitidentityfirst) + (ge_representation_imaginary_code_associate_compositeunitidentityfirst)) * S ((ge_representation_real_code_associate_compositeunitidentityfirst) + (ge_representation_imaginary_code_associate_compositeunitidentityfirst)) + ((ge_representation_imaginary_code_associate_compositeunitidentityfirst) + (ge_representation_imaginary_code_associate_compositeunitidentityfirst))) /\ ((exists ge_balance_positive_associate_compositeunitidentityfirstreal ge_balance_negative_associate_compositeunitidentityfirstreal. (((((ge_representation_real_code_associate_compositeunitidentityfirst) = 2 * (ge_balance_positive_associate_compositeunitidentityfirstreal) /\ (ge_balance_negative_associate_compositeunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_compositeunitidentityfirstrealdecode. (((ge_representation_real_code_associate_compositeunitidentityfirst) = 2 * ge_signed_half_associate_compositeunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_compositeunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_compositeunitidentityfirstreal) = S ge_signed_half_associate_compositeunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_compositeunitidentity) + ge_balance_negative_associate_compositeunitidentityfirstreal = (ge_first_rn_associate_compositeunitidentity) + ge_balance_positive_associate_compositeunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_compositeunitidentityfirstimaginary ge_balance_negative_associate_compositeunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_compositeunitidentityfirst) = 2 * (ge_balance_positive_associate_compositeunitidentityfirstimaginary) /\ (ge_balance_negative_associate_compositeunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_compositeunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_compositeunitidentityfirst) = 2 * ge_signed_half_associate_compositeunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_compositeunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_compositeunitidentityfirstimaginary) = S ge_signed_half_associate_compositeunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_compositeunitidentity) + ge_balance_negative_associate_compositeunitidentityfirstimaginary = (ge_first_in_associate_compositeunitidentity) + ge_balance_positive_associate_compositeunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_compositeunitidentitysecond ge_representation_imaginary_code_associate_compositeunitidentitysecond. (((gr_inverse_associate_compositeunit) = ((ge_representation_real_code_associate_compositeunitidentitysecond) + (ge_representation_imaginary_code_associate_compositeunitidentitysecond)) * S ((ge_representation_real_code_associate_compositeunitidentitysecond) + (ge_representation_imaginary_code_associate_compositeunitidentitysecond)) + ((ge_representation_imaginary_code_associate_compositeunitidentitysecond) + (ge_representation_imaginary_code_associate_compositeunitidentitysecond))) /\ ((exists ge_balance_positive_associate_compositeunitidentitysecondreal ge_balance_negative_associate_compositeunitidentitysecondreal. (((((ge_representation_real_code_associate_compositeunitidentitysecond) = 2 * (ge_balance_positive_associate_compositeunitidentitysecondreal) /\ (ge_balance_negative_associate_compositeunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_compositeunitidentitysecondrealdecode. (((ge_representation_real_code_associate_compositeunitidentitysecond) = 2 * ge_signed_half_associate_compositeunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_compositeunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_compositeunitidentitysecondreal) = S ge_signed_half_associate_compositeunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_compositeunitidentity) + ge_balance_negative_associate_compositeunitidentitysecondreal = (ge_second_rn_associate_compositeunitidentity) + ge_balance_positive_associate_compositeunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_compositeunitidentitysecondimaginary ge_balance_negative_associate_compositeunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_compositeunitidentitysecond) = 2 * (ge_balance_positive_associate_compositeunitidentitysecondimaginary) /\ (ge_balance_negative_associate_compositeunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_compositeunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_compositeunitidentitysecond) = 2 * ge_signed_half_associate_compositeunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_compositeunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_compositeunitidentitysecondimaginary) = S ge_signed_half_associate_compositeunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_compositeunitidentity) + ge_balance_negative_associate_compositeunitidentitysecondimaginary = (ge_second_in_associate_compositeunitidentity) + ge_balance_positive_associate_compositeunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_compositeunitidentityoutput ge_representation_imaginary_code_associate_compositeunitidentityoutput. (((6) = ((ge_representation_real_code_associate_compositeunitidentityoutput) + (ge_representation_imaginary_code_associate_compositeunitidentityoutput)) * S ((ge_representation_real_code_associate_compositeunitidentityoutput) + (ge_representation_imaginary_code_associate_compositeunitidentityoutput)) + ((ge_representation_imaginary_code_associate_compositeunitidentityoutput) + (ge_representation_imaginary_code_associate_compositeunitidentityoutput))) /\ ((exists ge_balance_positive_associate_compositeunitidentityoutputreal ge_balance_negative_associate_compositeunitidentityoutputreal. (((((ge_representation_real_code_associate_compositeunitidentityoutput) = 2 * (ge_balance_positive_associate_compositeunitidentityoutputreal) /\ (ge_balance_negative_associate_compositeunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_compositeunitidentityoutputrealdecode. (((ge_representation_real_code_associate_compositeunitidentityoutput) = 2 * ge_signed_half_associate_compositeunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_compositeunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_compositeunitidentityoutputreal) = S ge_signed_half_associate_compositeunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_compositeunitidentity) * (ge_second_rp_associate_compositeunitidentity))) + (((ge_first_rn_associate_compositeunitidentity) * (ge_second_rn_associate_compositeunitidentity))))) + (((((ge_first_ip_associate_compositeunitidentity) * (ge_second_in_associate_compositeunitidentity))) + (((ge_first_in_associate_compositeunitidentity) * (ge_second_ip_associate_compositeunitidentity))))))) + ge_balance_negative_associate_compositeunitidentityoutputreal = (((((((ge_first_rp_associate_compositeunitidentity) * (ge_second_rn_associate_compositeunitidentity))) + (((ge_first_rn_associate_compositeunitidentity) * (ge_second_rp_associate_compositeunitidentity))))) + (((((ge_first_ip_associate_compositeunitidentity) * (ge_second_ip_associate_compositeunitidentity))) + (((ge_first_in_associate_compositeunitidentity) * (ge_second_in_associate_compositeunitidentity))))))) + ge_balance_positive_associate_compositeunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_compositeunitidentityoutputimaginary ge_balance_negative_associate_compositeunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_compositeunitidentityoutput) = 2 * (ge_balance_positive_associate_compositeunitidentityoutputimaginary) /\ (ge_balance_negative_associate_compositeunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_compositeunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_compositeunitidentityoutput) = 2 * ge_signed_half_associate_compositeunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_compositeunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_compositeunitidentityoutputimaginary) = S ge_signed_half_associate_compositeunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_compositeunitidentity) * (ge_second_ip_associate_compositeunitidentity))) + (((ge_first_rn_associate_compositeunitidentity) * (ge_second_in_associate_compositeunitidentity))))) + (((((ge_first_ip_associate_compositeunitidentity) * (ge_second_rp_associate_compositeunitidentity))) + (((ge_first_in_associate_compositeunitidentity) * (ge_second_rn_associate_compositeunitidentity))))))) + ge_balance_negative_associate_compositeunitidentityoutputimaginary = (((((((ge_first_rp_associate_compositeunitidentity) * (ge_second_in_associate_compositeunitidentity))) + (((ge_first_rn_associate_compositeunitidentity) * (ge_second_ip_associate_compositeunitidentity))))) + (((((ge_first_ip_associate_compositeunitidentity) * (ge_second_rn_associate_compositeunitidentity))) + (((ge_first_in_associate_compositeunitidentity) * (ge_second_rp_associate_compositeunitidentity))))))) + ge_balance_positive_associate_compositeunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_compositetransport ge_first_rn_associate_compositetransport ge_first_ip_associate_compositetransport ge_first_in_associate_compositetransport ge_second_rp_associate_compositetransport ge_second_rn_associate_compositetransport ge_second_ip_associate_compositetransport ge_second_in_associate_compositetransport. ((exists ge_representation_real_code_associate_compositetransportfirst ge_representation_imaginary_code_associate_compositetransportfirst. (((gr_unit_associate_composite) = ((ge_representation_real_code_associate_compositetransportfirst) + (ge_representation_imaginary_code_associate_compositetransportfirst)) * S ((ge_representation_real_code_associate_compositetransportfirst) + (ge_representation_imaginary_code_associate_compositetransportfirst)) + ((ge_representation_imaginary_code_associate_compositetransportfirst) + (ge_representation_imaginary_code_associate_compositetransportfirst))) /\ ((exists ge_balance_positive_associate_compositetransportfirstreal ge_balance_negative_associate_compositetransportfirstreal. (((((ge_representation_real_code_associate_compositetransportfirst) = 2 * (ge_balance_positive_associate_compositetransportfirstreal) /\ (ge_balance_negative_associate_compositetransportfirstreal) = 0) \/ exists ge_signed_half_associate_compositetransportfirstrealdecode. (((ge_representation_real_code_associate_compositetransportfirst) = 2 * ge_signed_half_associate_compositetransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_compositetransportfirstreal) = 0) /\ (ge_balance_negative_associate_compositetransportfirstreal) = S ge_signed_half_associate_compositetransportfirstrealdecode))) /\ ((ge_first_rp_associate_compositetransport) + ge_balance_negative_associate_compositetransportfirstreal = (ge_first_rn_associate_compositetransport) + ge_balance_positive_associate_compositetransportfirstreal))) /\ (exists ge_balance_positive_associate_compositetransportfirstimaginary ge_balance_negative_associate_compositetransportfirstimaginary. (((((ge_representation_imaginary_code_associate_compositetransportfirst) = 2 * (ge_balance_positive_associate_compositetransportfirstimaginary) /\ (ge_balance_negative_associate_compositetransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_compositetransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_compositetransportfirst) = 2 * ge_signed_half_associate_compositetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_compositetransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_compositetransportfirstimaginary) = S ge_signed_half_associate_compositetransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_compositetransport) + ge_balance_negative_associate_compositetransportfirstimaginary = (ge_first_in_associate_compositetransport) + ge_balance_positive_associate_compositetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_compositetransportsecond ge_representation_imaginary_code_associate_compositetransportsecond. (((a) = ((ge_representation_real_code_associate_compositetransportsecond) + (ge_representation_imaginary_code_associate_compositetransportsecond)) * S ((ge_representation_real_code_associate_compositetransportsecond) + (ge_representation_imaginary_code_associate_compositetransportsecond)) + ((ge_representation_imaginary_code_associate_compositetransportsecond) + (ge_representation_imaginary_code_associate_compositetransportsecond))) /\ ((exists ge_balance_positive_associate_compositetransportsecondreal ge_balance_negative_associate_compositetransportsecondreal. (((((ge_representation_real_code_associate_compositetransportsecond) = 2 * (ge_balance_positive_associate_compositetransportsecondreal) /\ (ge_balance_negative_associate_compositetransportsecondreal) = 0) \/ exists ge_signed_half_associate_compositetransportsecondrealdecode. (((ge_representation_real_code_associate_compositetransportsecond) = 2 * ge_signed_half_associate_compositetransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_compositetransportsecondreal) = 0) /\ (ge_balance_negative_associate_compositetransportsecondreal) = S ge_signed_half_associate_compositetransportsecondrealdecode))) /\ ((ge_second_rp_associate_compositetransport) + ge_balance_negative_associate_compositetransportsecondreal = (ge_second_rn_associate_compositetransport) + ge_balance_positive_associate_compositetransportsecondreal))) /\ (exists ge_balance_positive_associate_compositetransportsecondimaginary ge_balance_negative_associate_compositetransportsecondimaginary. (((((ge_representation_imaginary_code_associate_compositetransportsecond) = 2 * (ge_balance_positive_associate_compositetransportsecondimaginary) /\ (ge_balance_negative_associate_compositetransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_compositetransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_compositetransportsecond) = 2 * ge_signed_half_associate_compositetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_compositetransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_compositetransportsecondimaginary) = S ge_signed_half_associate_compositetransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_compositetransport) + ge_balance_negative_associate_compositetransportsecondimaginary = (ge_second_in_associate_compositetransport) + ge_balance_positive_associate_compositetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_compositetransportoutput ge_representation_imaginary_code_associate_compositetransportoutput. (((c) = ((ge_representation_real_code_associate_compositetransportoutput) + (ge_representation_imaginary_code_associate_compositetransportoutput)) * S ((ge_representation_real_code_associate_compositetransportoutput) + (ge_representation_imaginary_code_associate_compositetransportoutput)) + ((ge_representation_imaginary_code_associate_compositetransportoutput) + (ge_representation_imaginary_code_associate_compositetransportoutput))) /\ ((exists ge_balance_positive_associate_compositetransportoutputreal ge_balance_negative_associate_compositetransportoutputreal. (((((ge_representation_real_code_associate_compositetransportoutput) = 2 * (ge_balance_positive_associate_compositetransportoutputreal) /\ (ge_balance_negative_associate_compositetransportoutputreal) = 0) \/ exists ge_signed_half_associate_compositetransportoutputrealdecode. (((ge_representation_real_code_associate_compositetransportoutput) = 2 * ge_signed_half_associate_compositetransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_compositetransportoutputreal) = 0) /\ (ge_balance_negative_associate_compositetransportoutputreal) = S ge_signed_half_associate_compositetransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_compositetransport) * (ge_second_rp_associate_compositetransport))) + (((ge_first_rn_associate_compositetransport) * (ge_second_rn_associate_compositetransport))))) + (((((ge_first_ip_associate_compositetransport) * (ge_second_in_associate_compositetransport))) + (((ge_first_in_associate_compositetransport) * (ge_second_ip_associate_compositetransport))))))) + ge_balance_negative_associate_compositetransportoutputreal = (((((((ge_first_rp_associate_compositetransport) * (ge_second_rn_associate_compositetransport))) + (((ge_first_rn_associate_compositetransport) * (ge_second_rp_associate_compositetransport))))) + (((((ge_first_ip_associate_compositetransport) * (ge_second_ip_associate_compositetransport))) + (((ge_first_in_associate_compositetransport) * (ge_second_in_associate_compositetransport))))))) + ge_balance_positive_associate_compositetransportoutputreal))) /\ (exists ge_balance_positive_associate_compositetransportoutputimaginary ge_balance_negative_associate_compositetransportoutputimaginary. (((((ge_representation_imaginary_code_associate_compositetransportoutput) = 2 * (ge_balance_positive_associate_compositetransportoutputimaginary) /\ (ge_balance_negative_associate_compositetransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_compositetransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_compositetransportoutput) = 2 * ge_signed_half_associate_compositetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_compositetransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_compositetransportoutputimaginary) = S ge_signed_half_associate_compositetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_compositetransport) * (ge_second_ip_associate_compositetransport))) + (((ge_first_rn_associate_compositetransport) * (ge_second_in_associate_compositetransport))))) + (((((ge_first_ip_associate_compositetransport) * (ge_second_rp_associate_compositetransport))) + (((ge_first_in_associate_compositetransport) * (ge_second_rn_associate_compositetransport))))))) + ge_balance_negative_associate_compositetransportoutputimaginary = (((((((ge_first_rp_associate_compositetransport) * (ge_second_in_associate_compositetransport))) + (((ge_first_rn_associate_compositetransport) * (ge_second_ip_associate_compositetransport))))) + (((((ge_first_ip_associate_compositetransport) * (ge_second_rn_associate_compositetransport))) + (((ge_first_in_associate_compositetransport) * (ge_second_rp_associate_compositetransport))))))) + ge_balance_positive_associate_compositetransportoutputimaginary)))))))))))