gaussian_factor_associate_code_transport

Exact expanded first-order arithmetic statement

forall a b c d. a=c -> b=d -> (exists gr_unit_associate_code_source. ((exists gr_inverse_associate_code_sourceunit. (exists ge_first_rp_associate_code_sourceunitidentity ge_first_rn_associate_code_sourceunitidentity ge_first_ip_associate_code_sourceunitidentity ge_first_in_associate_code_sourceunitidentity ge_second_rp_associate_code_sourceunitidentity ge_second_rn_associate_code_sourceunitidentity ge_second_ip_associate_code_sourceunitidentity ge_second_in_associate_code_sourceunitidentity. ((exists ge_representation_real_code_associate_code_sourceunitidentityfirst ge_representation_imaginary_code_associate_code_sourceunitidentityfirst. (((gr_unit_associate_code_source) = ((ge_representation_real_code_associate_code_sourceunitidentityfirst) + (ge_representation_imaginary_code_associate_code_sourceunitidentityfirst)) * S ((ge_representation_real_code_associate_code_sourceunitidentityfirst) + (ge_representation_imaginary_code_associate_code_sourceunitidentityfirst)) + ((ge_representation_imaginary_code_associate_code_sourceunitidentityfirst) + (ge_representation_imaginary_code_associate_code_sourceunitidentityfirst))) /\ ((exists ge_balance_positive_associate_code_sourceunitidentityfirstreal ge_balance_negative_associate_code_sourceunitidentityfirstreal. (((((ge_representation_real_code_associate_code_sourceunitidentityfirst) = 2 * (ge_balance_positive_associate_code_sourceunitidentityfirstreal) /\ (ge_balance_negative_associate_code_sourceunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_code_sourceunitidentityfirstrealdecode. (((ge_representation_real_code_associate_code_sourceunitidentityfirst) = 2 * ge_signed_half_associate_code_sourceunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_code_sourceunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_code_sourceunitidentityfirstreal) = S ge_signed_half_associate_code_sourceunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_code_sourceunitidentity) + ge_balance_negative_associate_code_sourceunitidentityfirstreal = (ge_first_rn_associate_code_sourceunitidentity) + ge_balance_positive_associate_code_sourceunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_code_sourceunitidentityfirstimaginary ge_balance_negative_associate_code_sourceunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_code_sourceunitidentityfirst) = 2 * (ge_balance_positive_associate_code_sourceunitidentityfirstimaginary) /\ (ge_balance_negative_associate_code_sourceunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_code_sourceunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_code_sourceunitidentityfirst) = 2 * ge_signed_half_associate_code_sourceunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_code_sourceunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_code_sourceunitidentityfirstimaginary) = S ge_signed_half_associate_code_sourceunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_code_sourceunitidentity) + ge_balance_negative_associate_code_sourceunitidentityfirstimaginary = (ge_first_in_associate_code_sourceunitidentity) + ge_balance_positive_associate_code_sourceunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_code_sourceunitidentitysecond ge_representation_imaginary_code_associate_code_sourceunitidentitysecond. (((gr_inverse_associate_code_sourceunit) = ((ge_representation_real_code_associate_code_sourceunitidentitysecond) + (ge_representation_imaginary_code_associate_code_sourceunitidentitysecond)) * S ((ge_representation_real_code_associate_code_sourceunitidentitysecond) + (ge_representation_imaginary_code_associate_code_sourceunitidentitysecond)) + ((ge_representation_imaginary_code_associate_code_sourceunitidentitysecond) + (ge_representation_imaginary_code_associate_code_sourceunitidentitysecond))) /\ ((exists ge_balance_positive_associate_code_sourceunitidentitysecondreal ge_balance_negative_associate_code_sourceunitidentitysecondreal. (((((ge_representation_real_code_associate_code_sourceunitidentitysecond) = 2 * (ge_balance_positive_associate_code_sourceunitidentitysecondreal) /\ (ge_balance_negative_associate_code_sourceunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_code_sourceunitidentitysecondrealdecode. (((ge_representation_real_code_associate_code_sourceunitidentitysecond) = 2 * ge_signed_half_associate_code_sourceunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_code_sourceunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_code_sourceunitidentitysecondreal) = S ge_signed_half_associate_code_sourceunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_code_sourceunitidentity) + ge_balance_negative_associate_code_sourceunitidentitysecondreal = (ge_second_rn_associate_code_sourceunitidentity) + ge_balance_positive_associate_code_sourceunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_code_sourceunitidentitysecondimaginary ge_balance_negative_associate_code_sourceunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_code_sourceunitidentitysecond) = 2 * (ge_balance_positive_associate_code_sourceunitidentitysecondimaginary) /\ (ge_balance_negative_associate_code_sourceunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_code_sourceunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_code_sourceunitidentitysecond) = 2 * ge_signed_half_associate_code_sourceunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_code_sourceunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_code_sourceunitidentitysecondimaginary) = S ge_signed_half_associate_code_sourceunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_code_sourceunitidentity) + ge_balance_negative_associate_code_sourceunitidentitysecondimaginary = (ge_second_in_associate_code_sourceunitidentity) + ge_balance_positive_associate_code_sourceunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_code_sourceunitidentityoutput ge_representation_imaginary_code_associate_code_sourceunitidentityoutput. (((6) = ((ge_representation_real_code_associate_code_sourceunitidentityoutput) + (ge_representation_imaginary_code_associate_code_sourceunitidentityoutput)) * S ((ge_representation_real_code_associate_code_sourceunitidentityoutput) + (ge_representation_imaginary_code_associate_code_sourceunitidentityoutput)) + ((ge_representation_imaginary_code_associate_code_sourceunitidentityoutput) + (ge_representation_imaginary_code_associate_code_sourceunitidentityoutput))) /\ ((exists ge_balance_positive_associate_code_sourceunitidentityoutputreal ge_balance_negative_associate_code_sourceunitidentityoutputreal. (((((ge_representation_real_code_associate_code_sourceunitidentityoutput) = 2 * (ge_balance_positive_associate_code_sourceunitidentityoutputreal) /\ (ge_balance_negative_associate_code_sourceunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_code_sourceunitidentityoutputrealdecode. (((ge_representation_real_code_associate_code_sourceunitidentityoutput) = 2 * ge_signed_half_associate_code_sourceunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_code_sourceunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_code_sourceunitidentityoutputreal) = S ge_signed_half_associate_code_sourceunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_code_sourceunitidentity) * (ge_second_rp_associate_code_sourceunitidentity))) + (((ge_first_rn_associate_code_sourceunitidentity) * (ge_second_rn_associate_code_sourceunitidentity))))) + (((((ge_first_ip_associate_code_sourceunitidentity) * (ge_second_in_associate_code_sourceunitidentity))) + (((ge_first_in_associate_code_sourceunitidentity) * (ge_second_ip_associate_code_sourceunitidentity))))))) + ge_balance_negative_associate_code_sourceunitidentityoutputreal = (((((((ge_first_rp_associate_code_sourceunitidentity) * (ge_second_rn_associate_code_sourceunitidentity))) + (((ge_first_rn_associate_code_sourceunitidentity) * (ge_second_rp_associate_code_sourceunitidentity))))) + (((((ge_first_ip_associate_code_sourceunitidentity) * (ge_second_ip_associate_code_sourceunitidentity))) + (((ge_first_in_associate_code_sourceunitidentity) * (ge_second_in_associate_code_sourceunitidentity))))))) + ge_balance_positive_associate_code_sourceunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_code_sourceunitidentityoutputimaginary ge_balance_negative_associate_code_sourceunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_code_sourceunitidentityoutput) = 2 * (ge_balance_positive_associate_code_sourceunitidentityoutputimaginary) /\ (ge_balance_negative_associate_code_sourceunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_code_sourceunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_code_sourceunitidentityoutput) = 2 * ge_signed_half_associate_code_sourceunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_code_sourceunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_code_sourceunitidentityoutputimaginary) = S ge_signed_half_associate_code_sourceunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_code_sourceunitidentity) * (ge_second_ip_associate_code_sourceunitidentity))) + (((ge_first_rn_associate_code_sourceunitidentity) * (ge_second_in_associate_code_sourceunitidentity))))) + (((((ge_first_ip_associate_code_sourceunitidentity) * (ge_second_rp_associate_code_sourceunitidentity))) + (((ge_first_in_associate_code_sourceunitidentity) * (ge_second_rn_associate_code_sourceunitidentity))))))) + ge_balance_negative_associate_code_sourceunitidentityoutputimaginary = (((((((ge_first_rp_associate_code_sourceunitidentity) * (ge_second_in_associate_code_sourceunitidentity))) + (((ge_first_rn_associate_code_sourceunitidentity) * (ge_second_ip_associate_code_sourceunitidentity))))) + (((((ge_first_ip_associate_code_sourceunitidentity) * (ge_second_rn_associate_code_sourceunitidentity))) + (((ge_first_in_associate_code_sourceunitidentity) * (ge_second_rp_associate_code_sourceunitidentity))))))) + ge_balance_positive_associate_code_sourceunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_code_sourcetransport ge_first_rn_associate_code_sourcetransport ge_first_ip_associate_code_sourcetransport ge_first_in_associate_code_sourcetransport ge_second_rp_associate_code_sourcetransport ge_second_rn_associate_code_sourcetransport ge_second_ip_associate_code_sourcetransport ge_second_in_associate_code_sourcetransport. ((exists ge_representation_real_code_associate_code_sourcetransportfirst ge_representation_imaginary_code_associate_code_sourcetransportfirst. (((gr_unit_associate_code_source) = ((ge_representation_real_code_associate_code_sourcetransportfirst) + (ge_representation_imaginary_code_associate_code_sourcetransportfirst)) * S ((ge_representation_real_code_associate_code_sourcetransportfirst) + (ge_representation_imaginary_code_associate_code_sourcetransportfirst)) + ((ge_representation_imaginary_code_associate_code_sourcetransportfirst) + (ge_representation_imaginary_code_associate_code_sourcetransportfirst))) /\ ((exists ge_balance_positive_associate_code_sourcetransportfirstreal ge_balance_negative_associate_code_sourcetransportfirstreal. (((((ge_representation_real_code_associate_code_sourcetransportfirst) = 2 * (ge_balance_positive_associate_code_sourcetransportfirstreal) /\ (ge_balance_negative_associate_code_sourcetransportfirstreal) = 0) \/ exists ge_signed_half_associate_code_sourcetransportfirstrealdecode. (((ge_representation_real_code_associate_code_sourcetransportfirst) = 2 * ge_signed_half_associate_code_sourcetransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_code_sourcetransportfirstreal) = 0) /\ (ge_balance_negative_associate_code_sourcetransportfirstreal) = S ge_signed_half_associate_code_sourcetransportfirstrealdecode))) /\ ((ge_first_rp_associate_code_sourcetransport) + ge_balance_negative_associate_code_sourcetransportfirstreal = (ge_first_rn_associate_code_sourcetransport) + ge_balance_positive_associate_code_sourcetransportfirstreal))) /\ (exists ge_balance_positive_associate_code_sourcetransportfirstimaginary ge_balance_negative_associate_code_sourcetransportfirstimaginary. (((((ge_representation_imaginary_code_associate_code_sourcetransportfirst) = 2 * (ge_balance_positive_associate_code_sourcetransportfirstimaginary) /\ (ge_balance_negative_associate_code_sourcetransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_code_sourcetransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_code_sourcetransportfirst) = 2 * ge_signed_half_associate_code_sourcetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_code_sourcetransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_code_sourcetransportfirstimaginary) = S ge_signed_half_associate_code_sourcetransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_code_sourcetransport) + ge_balance_negative_associate_code_sourcetransportfirstimaginary = (ge_first_in_associate_code_sourcetransport) + ge_balance_positive_associate_code_sourcetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_code_sourcetransportsecond ge_representation_imaginary_code_associate_code_sourcetransportsecond. (((a) = ((ge_representation_real_code_associate_code_sourcetransportsecond) + (ge_representation_imaginary_code_associate_code_sourcetransportsecond)) * S ((ge_representation_real_code_associate_code_sourcetransportsecond) + (ge_representation_imaginary_code_associate_code_sourcetransportsecond)) + ((ge_representation_imaginary_code_associate_code_sourcetransportsecond) + (ge_representation_imaginary_code_associate_code_sourcetransportsecond))) /\ ((exists ge_balance_positive_associate_code_sourcetransportsecondreal ge_balance_negative_associate_code_sourcetransportsecondreal. (((((ge_representation_real_code_associate_code_sourcetransportsecond) = 2 * (ge_balance_positive_associate_code_sourcetransportsecondreal) /\ (ge_balance_negative_associate_code_sourcetransportsecondreal) = 0) \/ exists ge_signed_half_associate_code_sourcetransportsecondrealdecode. (((ge_representation_real_code_associate_code_sourcetransportsecond) = 2 * ge_signed_half_associate_code_sourcetransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_code_sourcetransportsecondreal) = 0) /\ (ge_balance_negative_associate_code_sourcetransportsecondreal) = S ge_signed_half_associate_code_sourcetransportsecondrealdecode))) /\ ((ge_second_rp_associate_code_sourcetransport) + ge_balance_negative_associate_code_sourcetransportsecondreal = (ge_second_rn_associate_code_sourcetransport) + ge_balance_positive_associate_code_sourcetransportsecondreal))) /\ (exists ge_balance_positive_associate_code_sourcetransportsecondimaginary ge_balance_negative_associate_code_sourcetransportsecondimaginary. (((((ge_representation_imaginary_code_associate_code_sourcetransportsecond) = 2 * (ge_balance_positive_associate_code_sourcetransportsecondimaginary) /\ (ge_balance_negative_associate_code_sourcetransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_code_sourcetransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_code_sourcetransportsecond) = 2 * ge_signed_half_associate_code_sourcetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_code_sourcetransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_code_sourcetransportsecondimaginary) = S ge_signed_half_associate_code_sourcetransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_code_sourcetransport) + ge_balance_negative_associate_code_sourcetransportsecondimaginary = (ge_second_in_associate_code_sourcetransport) + ge_balance_positive_associate_code_sourcetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_code_sourcetransportoutput ge_representation_imaginary_code_associate_code_sourcetransportoutput. (((b) = ((ge_representation_real_code_associate_code_sourcetransportoutput) + (ge_representation_imaginary_code_associate_code_sourcetransportoutput)) * S ((ge_representation_real_code_associate_code_sourcetransportoutput) + (ge_representation_imaginary_code_associate_code_sourcetransportoutput)) + ((ge_representation_imaginary_code_associate_code_sourcetransportoutput) + (ge_representation_imaginary_code_associate_code_sourcetransportoutput))) /\ ((exists ge_balance_positive_associate_code_sourcetransportoutputreal ge_balance_negative_associate_code_sourcetransportoutputreal. (((((ge_representation_real_code_associate_code_sourcetransportoutput) = 2 * (ge_balance_positive_associate_code_sourcetransportoutputreal) /\ (ge_balance_negative_associate_code_sourcetransportoutputreal) = 0) \/ exists ge_signed_half_associate_code_sourcetransportoutputrealdecode. (((ge_representation_real_code_associate_code_sourcetransportoutput) = 2 * ge_signed_half_associate_code_sourcetransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_code_sourcetransportoutputreal) = 0) /\ (ge_balance_negative_associate_code_sourcetransportoutputreal) = S ge_signed_half_associate_code_sourcetransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_code_sourcetransport) * (ge_second_rp_associate_code_sourcetransport))) + (((ge_first_rn_associate_code_sourcetransport) * (ge_second_rn_associate_code_sourcetransport))))) + (((((ge_first_ip_associate_code_sourcetransport) * (ge_second_in_associate_code_sourcetransport))) + (((ge_first_in_associate_code_sourcetransport) * (ge_second_ip_associate_code_sourcetransport))))))) + ge_balance_negative_associate_code_sourcetransportoutputreal = (((((((ge_first_rp_associate_code_sourcetransport) * (ge_second_rn_associate_code_sourcetransport))) + (((ge_first_rn_associate_code_sourcetransport) * (ge_second_rp_associate_code_sourcetransport))))) + (((((ge_first_ip_associate_code_sourcetransport) * (ge_second_ip_associate_code_sourcetransport))) + (((ge_first_in_associate_code_sourcetransport) * (ge_second_in_associate_code_sourcetransport))))))) + ge_balance_positive_associate_code_sourcetransportoutputreal))) /\ (exists ge_balance_positive_associate_code_sourcetransportoutputimaginary ge_balance_negative_associate_code_sourcetransportoutputimaginary. (((((ge_representation_imaginary_code_associate_code_sourcetransportoutput) = 2 * (ge_balance_positive_associate_code_sourcetransportoutputimaginary) /\ (ge_balance_negative_associate_code_sourcetransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_code_sourcetransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_code_sourcetransportoutput) = 2 * ge_signed_half_associate_code_sourcetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_code_sourcetransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_code_sourcetransportoutputimaginary) = S ge_signed_half_associate_code_sourcetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_code_sourcetransport) * (ge_second_ip_associate_code_sourcetransport))) + (((ge_first_rn_associate_code_sourcetransport) * (ge_second_in_associate_code_sourcetransport))))) + (((((ge_first_ip_associate_code_sourcetransport) * (ge_second_rp_associate_code_sourcetransport))) + (((ge_first_in_associate_code_sourcetransport) * (ge_second_rn_associate_code_sourcetransport))))))) + ge_balance_negative_associate_code_sourcetransportoutputimaginary = (((((((ge_first_rp_associate_code_sourcetransport) * (ge_second_in_associate_code_sourcetransport))) + (((ge_first_rn_associate_code_sourcetransport) * (ge_second_ip_associate_code_sourcetransport))))) + (((((ge_first_ip_associate_code_sourcetransport) * (ge_second_rn_associate_code_sourcetransport))) + (((ge_first_in_associate_code_sourcetransport) * (ge_second_rp_associate_code_sourcetransport))))))) + ge_balance_positive_associate_code_sourcetransportoutputimaginary))))))))))) -> (exists gr_unit_associate_code_target. ((exists gr_inverse_associate_code_targetunit. (exists ge_first_rp_associate_code_targetunitidentity ge_first_rn_associate_code_targetunitidentity ge_first_ip_associate_code_targetunitidentity ge_first_in_associate_code_targetunitidentity ge_second_rp_associate_code_targetunitidentity ge_second_rn_associate_code_targetunitidentity ge_second_ip_associate_code_targetunitidentity ge_second_in_associate_code_targetunitidentity. ((exists ge_representation_real_code_associate_code_targetunitidentityfirst ge_representation_imaginary_code_associate_code_targetunitidentityfirst. (((gr_unit_associate_code_target) = ((ge_representation_real_code_associate_code_targetunitidentityfirst) + (ge_representation_imaginary_code_associate_code_targetunitidentityfirst)) * S ((ge_representation_real_code_associate_code_targetunitidentityfirst) + (ge_representation_imaginary_code_associate_code_targetunitidentityfirst)) + ((ge_representation_imaginary_code_associate_code_targetunitidentityfirst) + (ge_representation_imaginary_code_associate_code_targetunitidentityfirst))) /\ ((exists ge_balance_positive_associate_code_targetunitidentityfirstreal ge_balance_negative_associate_code_targetunitidentityfirstreal. (((((ge_representation_real_code_associate_code_targetunitidentityfirst) = 2 * (ge_balance_positive_associate_code_targetunitidentityfirstreal) /\ (ge_balance_negative_associate_code_targetunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_code_targetunitidentityfirstrealdecode. (((ge_representation_real_code_associate_code_targetunitidentityfirst) = 2 * ge_signed_half_associate_code_targetunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_code_targetunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_code_targetunitidentityfirstreal) = S ge_signed_half_associate_code_targetunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_code_targetunitidentity) + ge_balance_negative_associate_code_targetunitidentityfirstreal = (ge_first_rn_associate_code_targetunitidentity) + ge_balance_positive_associate_code_targetunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_code_targetunitidentityfirstimaginary ge_balance_negative_associate_code_targetunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_code_targetunitidentityfirst) = 2 * (ge_balance_positive_associate_code_targetunitidentityfirstimaginary) /\ (ge_balance_negative_associate_code_targetunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_code_targetunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_code_targetunitidentityfirst) = 2 * ge_signed_half_associate_code_targetunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_code_targetunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_code_targetunitidentityfirstimaginary) = S ge_signed_half_associate_code_targetunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_code_targetunitidentity) + ge_balance_negative_associate_code_targetunitidentityfirstimaginary = (ge_first_in_associate_code_targetunitidentity) + ge_balance_positive_associate_code_targetunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_code_targetunitidentitysecond ge_representation_imaginary_code_associate_code_targetunitidentitysecond. (((gr_inverse_associate_code_targetunit) = ((ge_representation_real_code_associate_code_targetunitidentitysecond) + (ge_representation_imaginary_code_associate_code_targetunitidentitysecond)) * S ((ge_representation_real_code_associate_code_targetunitidentitysecond) + (ge_representation_imaginary_code_associate_code_targetunitidentitysecond)) + ((ge_representation_imaginary_code_associate_code_targetunitidentitysecond) + (ge_representation_imaginary_code_associate_code_targetunitidentitysecond))) /\ ((exists ge_balance_positive_associate_code_targetunitidentitysecondreal ge_balance_negative_associate_code_targetunitidentitysecondreal. (((((ge_representation_real_code_associate_code_targetunitidentitysecond) = 2 * (ge_balance_positive_associate_code_targetunitidentitysecondreal) /\ (ge_balance_negative_associate_code_targetunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_code_targetunitidentitysecondrealdecode. (((ge_representation_real_code_associate_code_targetunitidentitysecond) = 2 * ge_signed_half_associate_code_targetunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_code_targetunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_code_targetunitidentitysecondreal) = S ge_signed_half_associate_code_targetunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_code_targetunitidentity) + ge_balance_negative_associate_code_targetunitidentitysecondreal = (ge_second_rn_associate_code_targetunitidentity) + ge_balance_positive_associate_code_targetunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_code_targetunitidentitysecondimaginary ge_balance_negative_associate_code_targetunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_code_targetunitidentitysecond) = 2 * (ge_balance_positive_associate_code_targetunitidentitysecondimaginary) /\ (ge_balance_negative_associate_code_targetunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_code_targetunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_code_targetunitidentitysecond) = 2 * ge_signed_half_associate_code_targetunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_code_targetunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_code_targetunitidentitysecondimaginary) = S ge_signed_half_associate_code_targetunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_code_targetunitidentity) + ge_balance_negative_associate_code_targetunitidentitysecondimaginary = (ge_second_in_associate_code_targetunitidentity) + ge_balance_positive_associate_code_targetunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_code_targetunitidentityoutput ge_representation_imaginary_code_associate_code_targetunitidentityoutput. (((6) = ((ge_representation_real_code_associate_code_targetunitidentityoutput) + (ge_representation_imaginary_code_associate_code_targetunitidentityoutput)) * S ((ge_representation_real_code_associate_code_targetunitidentityoutput) + (ge_representation_imaginary_code_associate_code_targetunitidentityoutput)) + ((ge_representation_imaginary_code_associate_code_targetunitidentityoutput) + (ge_representation_imaginary_code_associate_code_targetunitidentityoutput))) /\ ((exists ge_balance_positive_associate_code_targetunitidentityoutputreal ge_balance_negative_associate_code_targetunitidentityoutputreal. (((((ge_representation_real_code_associate_code_targetunitidentityoutput) = 2 * (ge_balance_positive_associate_code_targetunitidentityoutputreal) /\ (ge_balance_negative_associate_code_targetunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_code_targetunitidentityoutputrealdecode. (((ge_representation_real_code_associate_code_targetunitidentityoutput) = 2 * ge_signed_half_associate_code_targetunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_code_targetunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_code_targetunitidentityoutputreal) = S ge_signed_half_associate_code_targetunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_code_targetunitidentity) * (ge_second_rp_associate_code_targetunitidentity))) + (((ge_first_rn_associate_code_targetunitidentity) * (ge_second_rn_associate_code_targetunitidentity))))) + (((((ge_first_ip_associate_code_targetunitidentity) * (ge_second_in_associate_code_targetunitidentity))) + (((ge_first_in_associate_code_targetunitidentity) * (ge_second_ip_associate_code_targetunitidentity))))))) + ge_balance_negative_associate_code_targetunitidentityoutputreal = (((((((ge_first_rp_associate_code_targetunitidentity) * (ge_second_rn_associate_code_targetunitidentity))) + (((ge_first_rn_associate_code_targetunitidentity) * (ge_second_rp_associate_code_targetunitidentity))))) + (((((ge_first_ip_associate_code_targetunitidentity) * (ge_second_ip_associate_code_targetunitidentity))) + (((ge_first_in_associate_code_targetunitidentity) * (ge_second_in_associate_code_targetunitidentity))))))) + ge_balance_positive_associate_code_targetunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_code_targetunitidentityoutputimaginary ge_balance_negative_associate_code_targetunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_code_targetunitidentityoutput) = 2 * (ge_balance_positive_associate_code_targetunitidentityoutputimaginary) /\ (ge_balance_negative_associate_code_targetunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_code_targetunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_code_targetunitidentityoutput) = 2 * ge_signed_half_associate_code_targetunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_code_targetunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_code_targetunitidentityoutputimaginary) = S ge_signed_half_associate_code_targetunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_code_targetunitidentity) * (ge_second_ip_associate_code_targetunitidentity))) + (((ge_first_rn_associate_code_targetunitidentity) * (ge_second_in_associate_code_targetunitidentity))))) + (((((ge_first_ip_associate_code_targetunitidentity) * (ge_second_rp_associate_code_targetunitidentity))) + (((ge_first_in_associate_code_targetunitidentity) * (ge_second_rn_associate_code_targetunitidentity))))))) + ge_balance_negative_associate_code_targetunitidentityoutputimaginary = (((((((ge_first_rp_associate_code_targetunitidentity) * (ge_second_in_associate_code_targetunitidentity))) + (((ge_first_rn_associate_code_targetunitidentity) * (ge_second_ip_associate_code_targetunitidentity))))) + (((((ge_first_ip_associate_code_targetunitidentity) * (ge_second_rn_associate_code_targetunitidentity))) + (((ge_first_in_associate_code_targetunitidentity) * (ge_second_rp_associate_code_targetunitidentity))))))) + ge_balance_positive_associate_code_targetunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_code_targettransport ge_first_rn_associate_code_targettransport ge_first_ip_associate_code_targettransport ge_first_in_associate_code_targettransport ge_second_rp_associate_code_targettransport ge_second_rn_associate_code_targettransport ge_second_ip_associate_code_targettransport ge_second_in_associate_code_targettransport. ((exists ge_representation_real_code_associate_code_targettransportfirst ge_representation_imaginary_code_associate_code_targettransportfirst. (((gr_unit_associate_code_target) = ((ge_representation_real_code_associate_code_targettransportfirst) + (ge_representation_imaginary_code_associate_code_targettransportfirst)) * S ((ge_representation_real_code_associate_code_targettransportfirst) + (ge_representation_imaginary_code_associate_code_targettransportfirst)) + ((ge_representation_imaginary_code_associate_code_targettransportfirst) + (ge_representation_imaginary_code_associate_code_targettransportfirst))) /\ ((exists ge_balance_positive_associate_code_targettransportfirstreal ge_balance_negative_associate_code_targettransportfirstreal. (((((ge_representation_real_code_associate_code_targettransportfirst) = 2 * (ge_balance_positive_associate_code_targettransportfirstreal) /\ (ge_balance_negative_associate_code_targettransportfirstreal) = 0) \/ exists ge_signed_half_associate_code_targettransportfirstrealdecode. (((ge_representation_real_code_associate_code_targettransportfirst) = 2 * ge_signed_half_associate_code_targettransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_code_targettransportfirstreal) = 0) /\ (ge_balance_negative_associate_code_targettransportfirstreal) = S ge_signed_half_associate_code_targettransportfirstrealdecode))) /\ ((ge_first_rp_associate_code_targettransport) + ge_balance_negative_associate_code_targettransportfirstreal = (ge_first_rn_associate_code_targettransport) + ge_balance_positive_associate_code_targettransportfirstreal))) /\ (exists ge_balance_positive_associate_code_targettransportfirstimaginary ge_balance_negative_associate_code_targettransportfirstimaginary. (((((ge_representation_imaginary_code_associate_code_targettransportfirst) = 2 * (ge_balance_positive_associate_code_targettransportfirstimaginary) /\ (ge_balance_negative_associate_code_targettransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_code_targettransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_code_targettransportfirst) = 2 * ge_signed_half_associate_code_targettransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_code_targettransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_code_targettransportfirstimaginary) = S ge_signed_half_associate_code_targettransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_code_targettransport) + ge_balance_negative_associate_code_targettransportfirstimaginary = (ge_first_in_associate_code_targettransport) + ge_balance_positive_associate_code_targettransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_code_targettransportsecond ge_representation_imaginary_code_associate_code_targettransportsecond. (((c) = ((ge_representation_real_code_associate_code_targettransportsecond) + (ge_representation_imaginary_code_associate_code_targettransportsecond)) * S ((ge_representation_real_code_associate_code_targettransportsecond) + (ge_representation_imaginary_code_associate_code_targettransportsecond)) + ((ge_representation_imaginary_code_associate_code_targettransportsecond) + (ge_representation_imaginary_code_associate_code_targettransportsecond))) /\ ((exists ge_balance_positive_associate_code_targettransportsecondreal ge_balance_negative_associate_code_targettransportsecondreal. (((((ge_representation_real_code_associate_code_targettransportsecond) = 2 * (ge_balance_positive_associate_code_targettransportsecondreal) /\ (ge_balance_negative_associate_code_targettransportsecondreal) = 0) \/ exists ge_signed_half_associate_code_targettransportsecondrealdecode. (((ge_representation_real_code_associate_code_targettransportsecond) = 2 * ge_signed_half_associate_code_targettransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_code_targettransportsecondreal) = 0) /\ (ge_balance_negative_associate_code_targettransportsecondreal) = S ge_signed_half_associate_code_targettransportsecondrealdecode))) /\ ((ge_second_rp_associate_code_targettransport) + ge_balance_negative_associate_code_targettransportsecondreal = (ge_second_rn_associate_code_targettransport) + ge_balance_positive_associate_code_targettransportsecondreal))) /\ (exists ge_balance_positive_associate_code_targettransportsecondimaginary ge_balance_negative_associate_code_targettransportsecondimaginary. (((((ge_representation_imaginary_code_associate_code_targettransportsecond) = 2 * (ge_balance_positive_associate_code_targettransportsecondimaginary) /\ (ge_balance_negative_associate_code_targettransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_code_targettransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_code_targettransportsecond) = 2 * ge_signed_half_associate_code_targettransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_code_targettransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_code_targettransportsecondimaginary) = S ge_signed_half_associate_code_targettransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_code_targettransport) + ge_balance_negative_associate_code_targettransportsecondimaginary = (ge_second_in_associate_code_targettransport) + ge_balance_positive_associate_code_targettransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_code_targettransportoutput ge_representation_imaginary_code_associate_code_targettransportoutput. (((d) = ((ge_representation_real_code_associate_code_targettransportoutput) + (ge_representation_imaginary_code_associate_code_targettransportoutput)) * S ((ge_representation_real_code_associate_code_targettransportoutput) + (ge_representation_imaginary_code_associate_code_targettransportoutput)) + ((ge_representation_imaginary_code_associate_code_targettransportoutput) + (ge_representation_imaginary_code_associate_code_targettransportoutput))) /\ ((exists ge_balance_positive_associate_code_targettransportoutputreal ge_balance_negative_associate_code_targettransportoutputreal. (((((ge_representation_real_code_associate_code_targettransportoutput) = 2 * (ge_balance_positive_associate_code_targettransportoutputreal) /\ (ge_balance_negative_associate_code_targettransportoutputreal) = 0) \/ exists ge_signed_half_associate_code_targettransportoutputrealdecode. (((ge_representation_real_code_associate_code_targettransportoutput) = 2 * ge_signed_half_associate_code_targettransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_code_targettransportoutputreal) = 0) /\ (ge_balance_negative_associate_code_targettransportoutputreal) = S ge_signed_half_associate_code_targettransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_code_targettransport) * (ge_second_rp_associate_code_targettransport))) + (((ge_first_rn_associate_code_targettransport) * (ge_second_rn_associate_code_targettransport))))) + (((((ge_first_ip_associate_code_targettransport) * (ge_second_in_associate_code_targettransport))) + (((ge_first_in_associate_code_targettransport) * (ge_second_ip_associate_code_targettransport))))))) + ge_balance_negative_associate_code_targettransportoutputreal = (((((((ge_first_rp_associate_code_targettransport) * (ge_second_rn_associate_code_targettransport))) + (((ge_first_rn_associate_code_targettransport) * (ge_second_rp_associate_code_targettransport))))) + (((((ge_first_ip_associate_code_targettransport) * (ge_second_ip_associate_code_targettransport))) + (((ge_first_in_associate_code_targettransport) * (ge_second_in_associate_code_targettransport))))))) + ge_balance_positive_associate_code_targettransportoutputreal))) /\ (exists ge_balance_positive_associate_code_targettransportoutputimaginary ge_balance_negative_associate_code_targettransportoutputimaginary. (((((ge_representation_imaginary_code_associate_code_targettransportoutput) = 2 * (ge_balance_positive_associate_code_targettransportoutputimaginary) /\ (ge_balance_negative_associate_code_targettransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_code_targettransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_code_targettransportoutput) = 2 * ge_signed_half_associate_code_targettransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_code_targettransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_code_targettransportoutputimaginary) = S ge_signed_half_associate_code_targettransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_code_targettransport) * (ge_second_ip_associate_code_targettransport))) + (((ge_first_rn_associate_code_targettransport) * (ge_second_in_associate_code_targettransport))))) + (((((ge_first_ip_associate_code_targettransport) * (ge_second_rp_associate_code_targettransport))) + (((ge_first_in_associate_code_targettransport) * (ge_second_rn_associate_code_targettransport))))))) + ge_balance_negative_associate_code_targettransportoutputimaginary = (((((((ge_first_rp_associate_code_targettransport) * (ge_second_in_associate_code_targettransport))) + (((ge_first_rn_associate_code_targettransport) * (ge_second_ip_associate_code_targettransport))))) + (((((ge_first_ip_associate_code_targettransport) * (ge_second_rn_associate_code_targettransport))) + (((ge_first_in_associate_code_targettransport) * (ge_second_rp_associate_code_targettransport))))))) + ge_balance_positive_associate_code_targettransportoutputimaginary)))))))))))