gaussian_associate_symmetric

forall a b. (exists gr_unit_associate_forward. ((exists gr_inverse_associate_forwardunit. (exists ge_first_rp_associate_forwardunitidentity ge_first_rn_associate_forwardunitidentity ge_first_ip_associate_forwardunitidentity ge_first_in_associate_forwardunitidentity ge_second_rp_associate_forwardunitidentity ge_second_rn_associate_forwardunitidentity ge_second_ip_associate_forwardunitidentity ge_second_in_associate_forwardunitidentity. ((exists ge_representation_real_code_associate_forwardunitidentityfirst ge_representation_imaginary_code_associate_forwardunitidentityfirst. (((gr_unit_associate_forward) = ((ge_representation_real_code_associate_forwardunitidentityfirst) + (ge_representation_imaginary_code_associate_forwardunitidentityfirst)) * S ((ge_representation_real_code_associate_forwardunitidentityfirst) + (ge_representation_imaginary_code_associate_forwardunitidentityfirst)) + ((ge_representation_imaginary_code_associate_forwardunitidentityfirst) + (ge_representation_imaginary_code_associate_forwardunitidentityfirst))) /\ ((exists ge_balance_positive_associate_forwardunitidentityfirstreal ge_balance_negative_associate_forwardunitidentityfirstreal. (((((ge_representation_real_code_associate_forwardunitidentityfirst) = 2 * (ge_balance_positive_associate_forwardunitidentityfirstreal) /\ (ge_balance_negative_associate_forwardunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_forwardunitidentityfirstrealdecode. (((ge_representation_real_code_associate_forwardunitidentityfirst) = 2 * ge_signed_half_associate_forwardunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_forwardunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_forwardunitidentityfirstreal) = S ge_signed_half_associate_forwardunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_forwardunitidentity) + ge_balance_negative_associate_forwardunitidentityfirstreal = (ge_first_rn_associate_forwardunitidentity) + ge_balance_positive_associate_forwardunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_forwardunitidentityfirstimaginary ge_balance_negative_associate_forwardunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_forwardunitidentityfirst) = 2 * (ge_balance_positive_associate_forwardunitidentityfirstimaginary) /\ (ge_balance_negative_associate_forwardunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_forwardunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_forwardunitidentityfirst) = 2 * ge_signed_half_associate_forwardunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_forwardunitidentityfirstimaginary) = S ge_signed_half_associate_forwardunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_forwardunitidentity) + ge_balance_negative_associate_forwardunitidentityfirstimaginary = (ge_first_in_associate_forwardunitidentity) + ge_balance_positive_associate_forwardunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_forwardunitidentitysecond ge_representation_imaginary_code_associate_forwardunitidentitysecond. (((gr_inverse_associate_forwardunit) = ((ge_representation_real_code_associate_forwardunitidentitysecond) + (ge_representation_imaginary_code_associate_forwardunitidentitysecond)) * S ((ge_representation_real_code_associate_forwardunitidentitysecond) + (ge_representation_imaginary_code_associate_forwardunitidentitysecond)) + ((ge_representation_imaginary_code_associate_forwardunitidentitysecond) + (ge_representation_imaginary_code_associate_forwardunitidentitysecond))) /\ ((exists ge_balance_positive_associate_forwardunitidentitysecondreal ge_balance_negative_associate_forwardunitidentitysecondreal. (((((ge_representation_real_code_associate_forwardunitidentitysecond) = 2 * (ge_balance_positive_associate_forwardunitidentitysecondreal) /\ (ge_balance_negative_associate_forwardunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_forwardunitidentitysecondrealdecode. (((ge_representation_real_code_associate_forwardunitidentitysecond) = 2 * ge_signed_half_associate_forwardunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_forwardunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_forwardunitidentitysecondreal) = S ge_signed_half_associate_forwardunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_forwardunitidentity) + ge_balance_negative_associate_forwardunitidentitysecondreal = (ge_second_rn_associate_forwardunitidentity) + ge_balance_positive_associate_forwardunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_forwardunitidentitysecondimaginary ge_balance_negative_associate_forwardunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_forwardunitidentitysecond) = 2 * (ge_balance_positive_associate_forwardunitidentitysecondimaginary) /\ (ge_balance_negative_associate_forwardunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_forwardunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_forwardunitidentitysecond) = 2 * ge_signed_half_associate_forwardunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_forwardunitidentitysecondimaginary) = S ge_signed_half_associate_forwardunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_forwardunitidentity) + ge_balance_negative_associate_forwardunitidentitysecondimaginary = (ge_second_in_associate_forwardunitidentity) + ge_balance_positive_associate_forwardunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_forwardunitidentityoutput ge_representation_imaginary_code_associate_forwardunitidentityoutput. (((6) = ((ge_representation_real_code_associate_forwardunitidentityoutput) + (ge_representation_imaginary_code_associate_forwardunitidentityoutput)) * S ((ge_representation_real_code_associate_forwardunitidentityoutput) + (ge_representation_imaginary_code_associate_forwardunitidentityoutput)) + ((ge_representation_imaginary_code_associate_forwardunitidentityoutput) + (ge_representation_imaginary_code_associate_forwardunitidentityoutput))) /\ ((exists ge_balance_positive_associate_forwardunitidentityoutputreal ge_balance_negative_associate_forwardunitidentityoutputreal. (((((ge_representation_real_code_associate_forwardunitidentityoutput) = 2 * (ge_balance_positive_associate_forwardunitidentityoutputreal) /\ (ge_balance_negative_associate_forwardunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_forwardunitidentityoutputrealdecode. (((ge_representation_real_code_associate_forwardunitidentityoutput) = 2 * ge_signed_half_associate_forwardunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_forwardunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_forwardunitidentityoutputreal) = S ge_signed_half_associate_forwardunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_forwardunitidentity) * (ge_second_rp_associate_forwardunitidentity))) + (((ge_first_rn_associate_forwardunitidentity) * (ge_second_rn_associate_forwardunitidentity))))) + (((((ge_first_ip_associate_forwardunitidentity) * (ge_second_in_associate_forwardunitidentity))) + (((ge_first_in_associate_forwardunitidentity) * (ge_second_ip_associate_forwardunitidentity))))))) + ge_balance_negative_associate_forwardunitidentityoutputreal = (((((((ge_first_rp_associate_forwardunitidentity) * (ge_second_rn_associate_forwardunitidentity))) + (((ge_first_rn_associate_forwardunitidentity) * (ge_second_rp_associate_forwardunitidentity))))) + (((((ge_first_ip_associate_forwardunitidentity) * (ge_second_ip_associate_forwardunitidentity))) + (((ge_first_in_associate_forwardunitidentity) * (ge_second_in_associate_forwardunitidentity))))))) + ge_balance_positive_associate_forwardunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_forwardunitidentityoutputimaginary ge_balance_negative_associate_forwardunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_forwardunitidentityoutput) = 2 * (ge_balance_positive_associate_forwardunitidentityoutputimaginary) /\ (ge_balance_negative_associate_forwardunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_forwardunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_forwardunitidentityoutput) = 2 * ge_signed_half_associate_forwardunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_forwardunitidentityoutputimaginary) = S ge_signed_half_associate_forwardunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_forwardunitidentity) * (ge_second_ip_associate_forwardunitidentity))) + (((ge_first_rn_associate_forwardunitidentity) * (ge_second_in_associate_forwardunitidentity))))) + (((((ge_first_ip_associate_forwardunitidentity) * (ge_second_rp_associate_forwardunitidentity))) + (((ge_first_in_associate_forwardunitidentity) * (ge_second_rn_associate_forwardunitidentity))))))) + ge_balance_negative_associate_forwardunitidentityoutputimaginary = (((((((ge_first_rp_associate_forwardunitidentity) * (ge_second_in_associate_forwardunitidentity))) + (((ge_first_rn_associate_forwardunitidentity) * (ge_second_ip_associate_forwardunitidentity))))) + (((((ge_first_ip_associate_forwardunitidentity) * (ge_second_rn_associate_forwardunitidentity))) + (((ge_first_in_associate_forwardunitidentity) * (ge_second_rp_associate_forwardunitidentity))))))) + ge_balance_positive_associate_forwardunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_forwardtransport ge_first_rn_associate_forwardtransport ge_first_ip_associate_forwardtransport ge_first_in_associate_forwardtransport ge_second_rp_associate_forwardtransport ge_second_rn_associate_forwardtransport ge_second_ip_associate_forwardtransport ge_second_in_associate_forwardtransport. ((exists ge_representation_real_code_associate_forwardtransportfirst ge_representation_imaginary_code_associate_forwardtransportfirst. (((gr_unit_associate_forward) = ((ge_representation_real_code_associate_forwardtransportfirst) + (ge_representation_imaginary_code_associate_forwardtransportfirst)) * S ((ge_representation_real_code_associate_forwardtransportfirst) + (ge_representation_imaginary_code_associate_forwardtransportfirst)) + ((ge_representation_imaginary_code_associate_forwardtransportfirst) + (ge_representation_imaginary_code_associate_forwardtransportfirst))) /\ ((exists ge_balance_positive_associate_forwardtransportfirstreal ge_balance_negative_associate_forwardtransportfirstreal. (((((ge_representation_real_code_associate_forwardtransportfirst) = 2 * (ge_balance_positive_associate_forwardtransportfirstreal) /\ (ge_balance_negative_associate_forwardtransportfirstreal) = 0) \/ exists ge_signed_half_associate_forwardtransportfirstrealdecode. (((ge_representation_real_code_associate_forwardtransportfirst) = 2 * ge_signed_half_associate_forwardtransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_forwardtransportfirstreal) = 0) /\ (ge_balance_negative_associate_forwardtransportfirstreal) = S ge_signed_half_associate_forwardtransportfirstrealdecode))) /\ ((ge_first_rp_associate_forwardtransport) + ge_balance_negative_associate_forwardtransportfirstreal = (ge_first_rn_associate_forwardtransport) + ge_balance_positive_associate_forwardtransportfirstreal))) /\ (exists ge_balance_positive_associate_forwardtransportfirstimaginary ge_balance_negative_associate_forwardtransportfirstimaginary. (((((ge_representation_imaginary_code_associate_forwardtransportfirst) = 2 * (ge_balance_positive_associate_forwardtransportfirstimaginary) /\ (ge_balance_negative_associate_forwardtransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_forwardtransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_forwardtransportfirst) = 2 * ge_signed_half_associate_forwardtransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardtransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_forwardtransportfirstimaginary) = S ge_signed_half_associate_forwardtransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_forwardtransport) + ge_balance_negative_associate_forwardtransportfirstimaginary = (ge_first_in_associate_forwardtransport) + ge_balance_positive_associate_forwardtransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_forwardtransportsecond ge_representation_imaginary_code_associate_forwardtransportsecond. (((a) = ((ge_representation_real_code_associate_forwardtransportsecond) + (ge_representation_imaginary_code_associate_forwardtransportsecond)) * S ((ge_representation_real_code_associate_forwardtransportsecond) + (ge_representation_imaginary_code_associate_forwardtransportsecond)) + ((ge_representation_imaginary_code_associate_forwardtransportsecond) + (ge_representation_imaginary_code_associate_forwardtransportsecond))) /\ ((exists ge_balance_positive_associate_forwardtransportsecondreal ge_balance_negative_associate_forwardtransportsecondreal. (((((ge_representation_real_code_associate_forwardtransportsecond) = 2 * (ge_balance_positive_associate_forwardtransportsecondreal) /\ (ge_balance_negative_associate_forwardtransportsecondreal) = 0) \/ exists ge_signed_half_associate_forwardtransportsecondrealdecode. (((ge_representation_real_code_associate_forwardtransportsecond) = 2 * ge_signed_half_associate_forwardtransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_forwardtransportsecondreal) = 0) /\ (ge_balance_negative_associate_forwardtransportsecondreal) = S ge_signed_half_associate_forwardtransportsecondrealdecode))) /\ ((ge_second_rp_associate_forwardtransport) + ge_balance_negative_associate_forwardtransportsecondreal = (ge_second_rn_associate_forwardtransport) + ge_balance_positive_associate_forwardtransportsecondreal))) /\ (exists ge_balance_positive_associate_forwardtransportsecondimaginary ge_balance_negative_associate_forwardtransportsecondimaginary. (((((ge_representation_imaginary_code_associate_forwardtransportsecond) = 2 * (ge_balance_positive_associate_forwardtransportsecondimaginary) /\ (ge_balance_negative_associate_forwardtransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_forwardtransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_forwardtransportsecond) = 2 * ge_signed_half_associate_forwardtransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardtransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_forwardtransportsecondimaginary) = S ge_signed_half_associate_forwardtransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_forwardtransport) + ge_balance_negative_associate_forwardtransportsecondimaginary = (ge_second_in_associate_forwardtransport) + ge_balance_positive_associate_forwardtransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_forwardtransportoutput ge_representation_imaginary_code_associate_forwardtransportoutput. (((b) = ((ge_representation_real_code_associate_forwardtransportoutput) + (ge_representation_imaginary_code_associate_forwardtransportoutput)) * S ((ge_representation_real_code_associate_forwardtransportoutput) + (ge_representation_imaginary_code_associate_forwardtransportoutput)) + ((ge_representation_imaginary_code_associate_forwardtransportoutput) + (ge_representation_imaginary_code_associate_forwardtransportoutput))) /\ ((exists ge_balance_positive_associate_forwardtransportoutputreal ge_balance_negative_associate_forwardtransportoutputreal. (((((ge_representation_real_code_associate_forwardtransportoutput) = 2 * (ge_balance_positive_associate_forwardtransportoutputreal) /\ (ge_balance_negative_associate_forwardtransportoutputreal) = 0) \/ exists ge_signed_half_associate_forwardtransportoutputrealdecode. (((ge_representation_real_code_associate_forwardtransportoutput) = 2 * ge_signed_half_associate_forwardtransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_forwardtransportoutputreal) = 0) /\ (ge_balance_negative_associate_forwardtransportoutputreal) = S ge_signed_half_associate_forwardtransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_forwardtransport) * (ge_second_rp_associate_forwardtransport))) + (((ge_first_rn_associate_forwardtransport) * (ge_second_rn_associate_forwardtransport))))) + (((((ge_first_ip_associate_forwardtransport) * (ge_second_in_associate_forwardtransport))) + (((ge_first_in_associate_forwardtransport) * (ge_second_ip_associate_forwardtransport))))))) + ge_balance_negative_associate_forwardtransportoutputreal = (((((((ge_first_rp_associate_forwardtransport) * (ge_second_rn_associate_forwardtransport))) + (((ge_first_rn_associate_forwardtransport) * (ge_second_rp_associate_forwardtransport))))) + (((((ge_first_ip_associate_forwardtransport) * (ge_second_ip_associate_forwardtransport))) + (((ge_first_in_associate_forwardtransport) * (ge_second_in_associate_forwardtransport))))))) + ge_balance_positive_associate_forwardtransportoutputreal))) /\ (exists ge_balance_positive_associate_forwardtransportoutputimaginary ge_balance_negative_associate_forwardtransportoutputimaginary. (((((ge_representation_imaginary_code_associate_forwardtransportoutput) = 2 * (ge_balance_positive_associate_forwardtransportoutputimaginary) /\ (ge_balance_negative_associate_forwardtransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_forwardtransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_forwardtransportoutput) = 2 * ge_signed_half_associate_forwardtransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_forwardtransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_forwardtransportoutputimaginary) = S ge_signed_half_associate_forwardtransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_forwardtransport) * (ge_second_ip_associate_forwardtransport))) + (((ge_first_rn_associate_forwardtransport) * (ge_second_in_associate_forwardtransport))))) + (((((ge_first_ip_associate_forwardtransport) * (ge_second_rp_associate_forwardtransport))) + (((ge_first_in_associate_forwardtransport) * (ge_second_rn_associate_forwardtransport))))))) + ge_balance_negative_associate_forwardtransportoutputimaginary = (((((((ge_first_rp_associate_forwardtransport) * (ge_second_in_associate_forwardtransport))) + (((ge_first_rn_associate_forwardtransport) * (ge_second_ip_associate_forwardtransport))))) + (((((ge_first_ip_associate_forwardtransport) * (ge_second_rn_associate_forwardtransport))) + (((ge_first_in_associate_forwardtransport) * (ge_second_rp_associate_forwardtransport))))))) + ge_balance_positive_associate_forwardtransportoutputimaginary))))))))))) -> (exists gr_unit_associate_reverse. ((exists gr_inverse_associate_reverseunit. (exists ge_first_rp_associate_reverseunitidentity ge_first_rn_associate_reverseunitidentity ge_first_ip_associate_reverseunitidentity ge_first_in_associate_reverseunitidentity ge_second_rp_associate_reverseunitidentity ge_second_rn_associate_reverseunitidentity ge_second_ip_associate_reverseunitidentity ge_second_in_associate_reverseunitidentity. ((exists ge_representation_real_code_associate_reverseunitidentityfirst ge_representation_imaginary_code_associate_reverseunitidentityfirst. (((gr_unit_associate_reverse) = ((ge_representation_real_code_associate_reverseunitidentityfirst) + (ge_representation_imaginary_code_associate_reverseunitidentityfirst)) * S ((ge_representation_real_code_associate_reverseunitidentityfirst) + (ge_representation_imaginary_code_associate_reverseunitidentityfirst)) + ((ge_representation_imaginary_code_associate_reverseunitidentityfirst) + (ge_representation_imaginary_code_associate_reverseunitidentityfirst))) /\ ((exists ge_balance_positive_associate_reverseunitidentityfirstreal ge_balance_negative_associate_reverseunitidentityfirstreal. (((((ge_representation_real_code_associate_reverseunitidentityfirst) = 2 * (ge_balance_positive_associate_reverseunitidentityfirstreal) /\ (ge_balance_negative_associate_reverseunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_reverseunitidentityfirstrealdecode. (((ge_representation_real_code_associate_reverseunitidentityfirst) = 2 * ge_signed_half_associate_reverseunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_reverseunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_reverseunitidentityfirstreal) = S ge_signed_half_associate_reverseunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_reverseunitidentity) + ge_balance_negative_associate_reverseunitidentityfirstreal = (ge_first_rn_associate_reverseunitidentity) + ge_balance_positive_associate_reverseunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_reverseunitidentityfirstimaginary ge_balance_negative_associate_reverseunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_reverseunitidentityfirst) = 2 * (ge_balance_positive_associate_reverseunitidentityfirstimaginary) /\ (ge_balance_negative_associate_reverseunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_reverseunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_reverseunitidentityfirst) = 2 * ge_signed_half_associate_reverseunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_reverseunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_reverseunitidentityfirstimaginary) = S ge_signed_half_associate_reverseunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_reverseunitidentity) + ge_balance_negative_associate_reverseunitidentityfirstimaginary = (ge_first_in_associate_reverseunitidentity) + ge_balance_positive_associate_reverseunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_reverseunitidentitysecond ge_representation_imaginary_code_associate_reverseunitidentitysecond. (((gr_inverse_associate_reverseunit) = ((ge_representation_real_code_associate_reverseunitidentitysecond) + (ge_representation_imaginary_code_associate_reverseunitidentitysecond)) * S ((ge_representation_real_code_associate_reverseunitidentitysecond) + (ge_representation_imaginary_code_associate_reverseunitidentitysecond)) + ((ge_representation_imaginary_code_associate_reverseunitidentitysecond) + (ge_representation_imaginary_code_associate_reverseunitidentitysecond))) /\ ((exists ge_balance_positive_associate_reverseunitidentitysecondreal ge_balance_negative_associate_reverseunitidentitysecondreal. (((((ge_representation_real_code_associate_reverseunitidentitysecond) = 2 * (ge_balance_positive_associate_reverseunitidentitysecondreal) /\ (ge_balance_negative_associate_reverseunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_reverseunitidentitysecondrealdecode. (((ge_representation_real_code_associate_reverseunitidentitysecond) = 2 * ge_signed_half_associate_reverseunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_reverseunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_reverseunitidentitysecondreal) = S ge_signed_half_associate_reverseunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_reverseunitidentity) + ge_balance_negative_associate_reverseunitidentitysecondreal = (ge_second_rn_associate_reverseunitidentity) + ge_balance_positive_associate_reverseunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_reverseunitidentitysecondimaginary ge_balance_negative_associate_reverseunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_reverseunitidentitysecond) = 2 * (ge_balance_positive_associate_reverseunitidentitysecondimaginary) /\ (ge_balance_negative_associate_reverseunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_reverseunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_reverseunitidentitysecond) = 2 * ge_signed_half_associate_reverseunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_reverseunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_reverseunitidentitysecondimaginary) = S ge_signed_half_associate_reverseunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_reverseunitidentity) + ge_balance_negative_associate_reverseunitidentitysecondimaginary = (ge_second_in_associate_reverseunitidentity) + ge_balance_positive_associate_reverseunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_reverseunitidentityoutput ge_representation_imaginary_code_associate_reverseunitidentityoutput. (((6) = ((ge_representation_real_code_associate_reverseunitidentityoutput) + (ge_representation_imaginary_code_associate_reverseunitidentityoutput)) * S ((ge_representation_real_code_associate_reverseunitidentityoutput) + (ge_representation_imaginary_code_associate_reverseunitidentityoutput)) + ((ge_representation_imaginary_code_associate_reverseunitidentityoutput) + (ge_representation_imaginary_code_associate_reverseunitidentityoutput))) /\ ((exists ge_balance_positive_associate_reverseunitidentityoutputreal ge_balance_negative_associate_reverseunitidentityoutputreal. (((((ge_representation_real_code_associate_reverseunitidentityoutput) = 2 * (ge_balance_positive_associate_reverseunitidentityoutputreal) /\ (ge_balance_negative_associate_reverseunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_reverseunitidentityoutputrealdecode. (((ge_representation_real_code_associate_reverseunitidentityoutput) = 2 * ge_signed_half_associate_reverseunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_reverseunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_reverseunitidentityoutputreal) = S ge_signed_half_associate_reverseunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_reverseunitidentity) * (ge_second_rp_associate_reverseunitidentity))) + (((ge_first_rn_associate_reverseunitidentity) * (ge_second_rn_associate_reverseunitidentity))))) + (((((ge_first_ip_associate_reverseunitidentity) * (ge_second_in_associate_reverseunitidentity))) + (((ge_first_in_associate_reverseunitidentity) * (ge_second_ip_associate_reverseunitidentity))))))) + ge_balance_negative_associate_reverseunitidentityoutputreal = (((((((ge_first_rp_associate_reverseunitidentity) * (ge_second_rn_associate_reverseunitidentity))) + (((ge_first_rn_associate_reverseunitidentity) * (ge_second_rp_associate_reverseunitidentity))))) + (((((ge_first_ip_associate_reverseunitidentity) * (ge_second_ip_associate_reverseunitidentity))) + (((ge_first_in_associate_reverseunitidentity) * (ge_second_in_associate_reverseunitidentity))))))) + ge_balance_positive_associate_reverseunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_reverseunitidentityoutputimaginary ge_balance_negative_associate_reverseunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_reverseunitidentityoutput) = 2 * (ge_balance_positive_associate_reverseunitidentityoutputimaginary) /\ (ge_balance_negative_associate_reverseunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_reverseunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_reverseunitidentityoutput) = 2 * ge_signed_half_associate_reverseunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_reverseunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_reverseunitidentityoutputimaginary) = S ge_signed_half_associate_reverseunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_reverseunitidentity) * (ge_second_ip_associate_reverseunitidentity))) + (((ge_first_rn_associate_reverseunitidentity) * (ge_second_in_associate_reverseunitidentity))))) + (((((ge_first_ip_associate_reverseunitidentity) * (ge_second_rp_associate_reverseunitidentity))) + (((ge_first_in_associate_reverseunitidentity) * (ge_second_rn_associate_reverseunitidentity))))))) + ge_balance_negative_associate_reverseunitidentityoutputimaginary = (((((((ge_first_rp_associate_reverseunitidentity) * (ge_second_in_associate_reverseunitidentity))) + (((ge_first_rn_associate_reverseunitidentity) * (ge_second_ip_associate_reverseunitidentity))))) + (((((ge_first_ip_associate_reverseunitidentity) * (ge_second_rn_associate_reverseunitidentity))) + (((ge_first_in_associate_reverseunitidentity) * (ge_second_rp_associate_reverseunitidentity))))))) + ge_balance_positive_associate_reverseunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_reversetransport ge_first_rn_associate_reversetransport ge_first_ip_associate_reversetransport ge_first_in_associate_reversetransport ge_second_rp_associate_reversetransport ge_second_rn_associate_reversetransport ge_second_ip_associate_reversetransport ge_second_in_associate_reversetransport. ((exists ge_representation_real_code_associate_reversetransportfirst ge_representation_imaginary_code_associate_reversetransportfirst. (((gr_unit_associate_reverse) = ((ge_representation_real_code_associate_reversetransportfirst) + (ge_representation_imaginary_code_associate_reversetransportfirst)) * S ((ge_representation_real_code_associate_reversetransportfirst) + (ge_representation_imaginary_code_associate_reversetransportfirst)) + ((ge_representation_imaginary_code_associate_reversetransportfirst) + (ge_representation_imaginary_code_associate_reversetransportfirst))) /\ ((exists ge_balance_positive_associate_reversetransportfirstreal ge_balance_negative_associate_reversetransportfirstreal. (((((ge_representation_real_code_associate_reversetransportfirst) = 2 * (ge_balance_positive_associate_reversetransportfirstreal) /\ (ge_balance_negative_associate_reversetransportfirstreal) = 0) \/ exists ge_signed_half_associate_reversetransportfirstrealdecode. (((ge_representation_real_code_associate_reversetransportfirst) = 2 * ge_signed_half_associate_reversetransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_reversetransportfirstreal) = 0) /\ (ge_balance_negative_associate_reversetransportfirstreal) = S ge_signed_half_associate_reversetransportfirstrealdecode))) /\ ((ge_first_rp_associate_reversetransport) + ge_balance_negative_associate_reversetransportfirstreal = (ge_first_rn_associate_reversetransport) + ge_balance_positive_associate_reversetransportfirstreal))) /\ (exists ge_balance_positive_associate_reversetransportfirstimaginary ge_balance_negative_associate_reversetransportfirstimaginary. (((((ge_representation_imaginary_code_associate_reversetransportfirst) = 2 * (ge_balance_positive_associate_reversetransportfirstimaginary) /\ (ge_balance_negative_associate_reversetransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_reversetransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_reversetransportfirst) = 2 * ge_signed_half_associate_reversetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_reversetransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_reversetransportfirstimaginary) = S ge_signed_half_associate_reversetransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_reversetransport) + ge_balance_negative_associate_reversetransportfirstimaginary = (ge_first_in_associate_reversetransport) + ge_balance_positive_associate_reversetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_reversetransportsecond ge_representation_imaginary_code_associate_reversetransportsecond. (((b) = ((ge_representation_real_code_associate_reversetransportsecond) + (ge_representation_imaginary_code_associate_reversetransportsecond)) * S ((ge_representation_real_code_associate_reversetransportsecond) + (ge_representation_imaginary_code_associate_reversetransportsecond)) + ((ge_representation_imaginary_code_associate_reversetransportsecond) + (ge_representation_imaginary_code_associate_reversetransportsecond))) /\ ((exists ge_balance_positive_associate_reversetransportsecondreal ge_balance_negative_associate_reversetransportsecondreal. (((((ge_representation_real_code_associate_reversetransportsecond) = 2 * (ge_balance_positive_associate_reversetransportsecondreal) /\ (ge_balance_negative_associate_reversetransportsecondreal) = 0) \/ exists ge_signed_half_associate_reversetransportsecondrealdecode. (((ge_representation_real_code_associate_reversetransportsecond) = 2 * ge_signed_half_associate_reversetransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_reversetransportsecondreal) = 0) /\ (ge_balance_negative_associate_reversetransportsecondreal) = S ge_signed_half_associate_reversetransportsecondrealdecode))) /\ ((ge_second_rp_associate_reversetransport) + ge_balance_negative_associate_reversetransportsecondreal = (ge_second_rn_associate_reversetransport) + ge_balance_positive_associate_reversetransportsecondreal))) /\ (exists ge_balance_positive_associate_reversetransportsecondimaginary ge_balance_negative_associate_reversetransportsecondimaginary. (((((ge_representation_imaginary_code_associate_reversetransportsecond) = 2 * (ge_balance_positive_associate_reversetransportsecondimaginary) /\ (ge_balance_negative_associate_reversetransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_reversetransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_reversetransportsecond) = 2 * ge_signed_half_associate_reversetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_reversetransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_reversetransportsecondimaginary) = S ge_signed_half_associate_reversetransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_reversetransport) + ge_balance_negative_associate_reversetransportsecondimaginary = (ge_second_in_associate_reversetransport) + ge_balance_positive_associate_reversetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_reversetransportoutput ge_representation_imaginary_code_associate_reversetransportoutput. (((a) = ((ge_representation_real_code_associate_reversetransportoutput) + (ge_representation_imaginary_code_associate_reversetransportoutput)) * S ((ge_representation_real_code_associate_reversetransportoutput) + (ge_representation_imaginary_code_associate_reversetransportoutput)) + ((ge_representation_imaginary_code_associate_reversetransportoutput) + (ge_representation_imaginary_code_associate_reversetransportoutput))) /\ ((exists ge_balance_positive_associate_reversetransportoutputreal ge_balance_negative_associate_reversetransportoutputreal. (((((ge_representation_real_code_associate_reversetransportoutput) = 2 * (ge_balance_positive_associate_reversetransportoutputreal) /\ (ge_balance_negative_associate_reversetransportoutputreal) = 0) \/ exists ge_signed_half_associate_reversetransportoutputrealdecode. (((ge_representation_real_code_associate_reversetransportoutput) = 2 * ge_signed_half_associate_reversetransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_reversetransportoutputreal) = 0) /\ (ge_balance_negative_associate_reversetransportoutputreal) = S ge_signed_half_associate_reversetransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_reversetransport) * (ge_second_rp_associate_reversetransport))) + (((ge_first_rn_associate_reversetransport) * (ge_second_rn_associate_reversetransport))))) + (((((ge_first_ip_associate_reversetransport) * (ge_second_in_associate_reversetransport))) + (((ge_first_in_associate_reversetransport) * (ge_second_ip_associate_reversetransport))))))) + ge_balance_negative_associate_reversetransportoutputreal = (((((((ge_first_rp_associate_reversetransport) * (ge_second_rn_associate_reversetransport))) + (((ge_first_rn_associate_reversetransport) * (ge_second_rp_associate_reversetransport))))) + (((((ge_first_ip_associate_reversetransport) * (ge_second_ip_associate_reversetransport))) + (((ge_first_in_associate_reversetransport) * (ge_second_in_associate_reversetransport))))))) + ge_balance_positive_associate_reversetransportoutputreal))) /\ (exists ge_balance_positive_associate_reversetransportoutputimaginary ge_balance_negative_associate_reversetransportoutputimaginary. (((((ge_representation_imaginary_code_associate_reversetransportoutput) = 2 * (ge_balance_positive_associate_reversetransportoutputimaginary) /\ (ge_balance_negative_associate_reversetransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_reversetransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_reversetransportoutput) = 2 * ge_signed_half_associate_reversetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_reversetransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_reversetransportoutputimaginary) = S ge_signed_half_associate_reversetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_reversetransport) * (ge_second_ip_associate_reversetransport))) + (((ge_first_rn_associate_reversetransport) * (ge_second_in_associate_reversetransport))))) + (((((ge_first_ip_associate_reversetransport) * (ge_second_rp_associate_reversetransport))) + (((ge_first_in_associate_reversetransport) * (ge_second_rn_associate_reversetransport))))))) + ge_balance_negative_associate_reversetransportoutputimaginary = (((((((ge_first_rp_associate_reversetransport) * (ge_second_in_associate_reversetransport))) + (((ge_first_rn_associate_reversetransport) * (ge_second_ip_associate_reversetransport))))) + (((((ge_first_ip_associate_reversetransport) * (ge_second_rn_associate_reversetransport))) + (((ge_first_in_associate_reversetransport) * (ge_second_rp_associate_reversetransport))))))) + ge_balance_positive_associate_reversetransportoutputimaginary)))))))))))