gaussian_factor_associate_unit

Exact expanded first-order arithmetic statement

forall a b. (exists gr_unit_associate_unit_input. ((exists gr_inverse_associate_unit_inputunit. (exists ge_first_rp_associate_unit_inputunitidentity ge_first_rn_associate_unit_inputunitidentity ge_first_ip_associate_unit_inputunitidentity ge_first_in_associate_unit_inputunitidentity ge_second_rp_associate_unit_inputunitidentity ge_second_rn_associate_unit_inputunitidentity ge_second_ip_associate_unit_inputunitidentity ge_second_in_associate_unit_inputunitidentity. ((exists ge_representation_real_code_associate_unit_inputunitidentityfirst ge_representation_imaginary_code_associate_unit_inputunitidentityfirst. (((gr_unit_associate_unit_input) = ((ge_representation_real_code_associate_unit_inputunitidentityfirst) + (ge_representation_imaginary_code_associate_unit_inputunitidentityfirst)) * S ((ge_representation_real_code_associate_unit_inputunitidentityfirst) + (ge_representation_imaginary_code_associate_unit_inputunitidentityfirst)) + ((ge_representation_imaginary_code_associate_unit_inputunitidentityfirst) + (ge_representation_imaginary_code_associate_unit_inputunitidentityfirst))) /\ ((exists ge_balance_positive_associate_unit_inputunitidentityfirstreal ge_balance_negative_associate_unit_inputunitidentityfirstreal. (((((ge_representation_real_code_associate_unit_inputunitidentityfirst) = 2 * (ge_balance_positive_associate_unit_inputunitidentityfirstreal) /\ (ge_balance_negative_associate_unit_inputunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_unit_inputunitidentityfirstrealdecode. (((ge_representation_real_code_associate_unit_inputunitidentityfirst) = 2 * ge_signed_half_associate_unit_inputunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_unit_inputunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_unit_inputunitidentityfirstreal) = S ge_signed_half_associate_unit_inputunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_unit_inputunitidentity) + ge_balance_negative_associate_unit_inputunitidentityfirstreal = (ge_first_rn_associate_unit_inputunitidentity) + ge_balance_positive_associate_unit_inputunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_unit_inputunitidentityfirstimaginary ge_balance_negative_associate_unit_inputunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_unit_inputunitidentityfirst) = 2 * (ge_balance_positive_associate_unit_inputunitidentityfirstimaginary) /\ (ge_balance_negative_associate_unit_inputunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_unit_inputunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_unit_inputunitidentityfirst) = 2 * ge_signed_half_associate_unit_inputunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_inputunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_unit_inputunitidentityfirstimaginary) = S ge_signed_half_associate_unit_inputunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_unit_inputunitidentity) + ge_balance_negative_associate_unit_inputunitidentityfirstimaginary = (ge_first_in_associate_unit_inputunitidentity) + ge_balance_positive_associate_unit_inputunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_unit_inputunitidentitysecond ge_representation_imaginary_code_associate_unit_inputunitidentitysecond. (((gr_inverse_associate_unit_inputunit) = ((ge_representation_real_code_associate_unit_inputunitidentitysecond) + (ge_representation_imaginary_code_associate_unit_inputunitidentitysecond)) * S ((ge_representation_real_code_associate_unit_inputunitidentitysecond) + (ge_representation_imaginary_code_associate_unit_inputunitidentitysecond)) + ((ge_representation_imaginary_code_associate_unit_inputunitidentitysecond) + (ge_representation_imaginary_code_associate_unit_inputunitidentitysecond))) /\ ((exists ge_balance_positive_associate_unit_inputunitidentitysecondreal ge_balance_negative_associate_unit_inputunitidentitysecondreal. (((((ge_representation_real_code_associate_unit_inputunitidentitysecond) = 2 * (ge_balance_positive_associate_unit_inputunitidentitysecondreal) /\ (ge_balance_negative_associate_unit_inputunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_unit_inputunitidentitysecondrealdecode. (((ge_representation_real_code_associate_unit_inputunitidentitysecond) = 2 * ge_signed_half_associate_unit_inputunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_unit_inputunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_unit_inputunitidentitysecondreal) = S ge_signed_half_associate_unit_inputunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_unit_inputunitidentity) + ge_balance_negative_associate_unit_inputunitidentitysecondreal = (ge_second_rn_associate_unit_inputunitidentity) + ge_balance_positive_associate_unit_inputunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_unit_inputunitidentitysecondimaginary ge_balance_negative_associate_unit_inputunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_unit_inputunitidentitysecond) = 2 * (ge_balance_positive_associate_unit_inputunitidentitysecondimaginary) /\ (ge_balance_negative_associate_unit_inputunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_unit_inputunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_unit_inputunitidentitysecond) = 2 * ge_signed_half_associate_unit_inputunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_inputunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_unit_inputunitidentitysecondimaginary) = S ge_signed_half_associate_unit_inputunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_unit_inputunitidentity) + ge_balance_negative_associate_unit_inputunitidentitysecondimaginary = (ge_second_in_associate_unit_inputunitidentity) + ge_balance_positive_associate_unit_inputunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_unit_inputunitidentityoutput ge_representation_imaginary_code_associate_unit_inputunitidentityoutput. (((6) = ((ge_representation_real_code_associate_unit_inputunitidentityoutput) + (ge_representation_imaginary_code_associate_unit_inputunitidentityoutput)) * S ((ge_representation_real_code_associate_unit_inputunitidentityoutput) + (ge_representation_imaginary_code_associate_unit_inputunitidentityoutput)) + ((ge_representation_imaginary_code_associate_unit_inputunitidentityoutput) + (ge_representation_imaginary_code_associate_unit_inputunitidentityoutput))) /\ ((exists ge_balance_positive_associate_unit_inputunitidentityoutputreal ge_balance_negative_associate_unit_inputunitidentityoutputreal. (((((ge_representation_real_code_associate_unit_inputunitidentityoutput) = 2 * (ge_balance_positive_associate_unit_inputunitidentityoutputreal) /\ (ge_balance_negative_associate_unit_inputunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_unit_inputunitidentityoutputrealdecode. (((ge_representation_real_code_associate_unit_inputunitidentityoutput) = 2 * ge_signed_half_associate_unit_inputunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_unit_inputunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_unit_inputunitidentityoutputreal) = S ge_signed_half_associate_unit_inputunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_unit_inputunitidentity) * (ge_second_rp_associate_unit_inputunitidentity))) + (((ge_first_rn_associate_unit_inputunitidentity) * (ge_second_rn_associate_unit_inputunitidentity))))) + (((((ge_first_ip_associate_unit_inputunitidentity) * (ge_second_in_associate_unit_inputunitidentity))) + (((ge_first_in_associate_unit_inputunitidentity) * (ge_second_ip_associate_unit_inputunitidentity))))))) + ge_balance_negative_associate_unit_inputunitidentityoutputreal = (((((((ge_first_rp_associate_unit_inputunitidentity) * (ge_second_rn_associate_unit_inputunitidentity))) + (((ge_first_rn_associate_unit_inputunitidentity) * (ge_second_rp_associate_unit_inputunitidentity))))) + (((((ge_first_ip_associate_unit_inputunitidentity) * (ge_second_ip_associate_unit_inputunitidentity))) + (((ge_first_in_associate_unit_inputunitidentity) * (ge_second_in_associate_unit_inputunitidentity))))))) + ge_balance_positive_associate_unit_inputunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_unit_inputunitidentityoutputimaginary ge_balance_negative_associate_unit_inputunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_unit_inputunitidentityoutput) = 2 * (ge_balance_positive_associate_unit_inputunitidentityoutputimaginary) /\ (ge_balance_negative_associate_unit_inputunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_unit_inputunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_unit_inputunitidentityoutput) = 2 * ge_signed_half_associate_unit_inputunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_inputunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_unit_inputunitidentityoutputimaginary) = S ge_signed_half_associate_unit_inputunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_unit_inputunitidentity) * (ge_second_ip_associate_unit_inputunitidentity))) + (((ge_first_rn_associate_unit_inputunitidentity) * (ge_second_in_associate_unit_inputunitidentity))))) + (((((ge_first_ip_associate_unit_inputunitidentity) * (ge_second_rp_associate_unit_inputunitidentity))) + (((ge_first_in_associate_unit_inputunitidentity) * (ge_second_rn_associate_unit_inputunitidentity))))))) + ge_balance_negative_associate_unit_inputunitidentityoutputimaginary = (((((((ge_first_rp_associate_unit_inputunitidentity) * (ge_second_in_associate_unit_inputunitidentity))) + (((ge_first_rn_associate_unit_inputunitidentity) * (ge_second_ip_associate_unit_inputunitidentity))))) + (((((ge_first_ip_associate_unit_inputunitidentity) * (ge_second_rn_associate_unit_inputunitidentity))) + (((ge_first_in_associate_unit_inputunitidentity) * (ge_second_rp_associate_unit_inputunitidentity))))))) + ge_balance_positive_associate_unit_inputunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_unit_inputtransport ge_first_rn_associate_unit_inputtransport ge_first_ip_associate_unit_inputtransport ge_first_in_associate_unit_inputtransport ge_second_rp_associate_unit_inputtransport ge_second_rn_associate_unit_inputtransport ge_second_ip_associate_unit_inputtransport ge_second_in_associate_unit_inputtransport. ((exists ge_representation_real_code_associate_unit_inputtransportfirst ge_representation_imaginary_code_associate_unit_inputtransportfirst. (((gr_unit_associate_unit_input) = ((ge_representation_real_code_associate_unit_inputtransportfirst) + (ge_representation_imaginary_code_associate_unit_inputtransportfirst)) * S ((ge_representation_real_code_associate_unit_inputtransportfirst) + (ge_representation_imaginary_code_associate_unit_inputtransportfirst)) + ((ge_representation_imaginary_code_associate_unit_inputtransportfirst) + (ge_representation_imaginary_code_associate_unit_inputtransportfirst))) /\ ((exists ge_balance_positive_associate_unit_inputtransportfirstreal ge_balance_negative_associate_unit_inputtransportfirstreal. (((((ge_representation_real_code_associate_unit_inputtransportfirst) = 2 * (ge_balance_positive_associate_unit_inputtransportfirstreal) /\ (ge_balance_negative_associate_unit_inputtransportfirstreal) = 0) \/ exists ge_signed_half_associate_unit_inputtransportfirstrealdecode. (((ge_representation_real_code_associate_unit_inputtransportfirst) = 2 * ge_signed_half_associate_unit_inputtransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_unit_inputtransportfirstreal) = 0) /\ (ge_balance_negative_associate_unit_inputtransportfirstreal) = S ge_signed_half_associate_unit_inputtransportfirstrealdecode))) /\ ((ge_first_rp_associate_unit_inputtransport) + ge_balance_negative_associate_unit_inputtransportfirstreal = (ge_first_rn_associate_unit_inputtransport) + ge_balance_positive_associate_unit_inputtransportfirstreal))) /\ (exists ge_balance_positive_associate_unit_inputtransportfirstimaginary ge_balance_negative_associate_unit_inputtransportfirstimaginary. (((((ge_representation_imaginary_code_associate_unit_inputtransportfirst) = 2 * (ge_balance_positive_associate_unit_inputtransportfirstimaginary) /\ (ge_balance_negative_associate_unit_inputtransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_unit_inputtransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_unit_inputtransportfirst) = 2 * ge_signed_half_associate_unit_inputtransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_inputtransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_unit_inputtransportfirstimaginary) = S ge_signed_half_associate_unit_inputtransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_unit_inputtransport) + ge_balance_negative_associate_unit_inputtransportfirstimaginary = (ge_first_in_associate_unit_inputtransport) + ge_balance_positive_associate_unit_inputtransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_unit_inputtransportsecond ge_representation_imaginary_code_associate_unit_inputtransportsecond. (((a) = ((ge_representation_real_code_associate_unit_inputtransportsecond) + (ge_representation_imaginary_code_associate_unit_inputtransportsecond)) * S ((ge_representation_real_code_associate_unit_inputtransportsecond) + (ge_representation_imaginary_code_associate_unit_inputtransportsecond)) + ((ge_representation_imaginary_code_associate_unit_inputtransportsecond) + (ge_representation_imaginary_code_associate_unit_inputtransportsecond))) /\ ((exists ge_balance_positive_associate_unit_inputtransportsecondreal ge_balance_negative_associate_unit_inputtransportsecondreal. (((((ge_representation_real_code_associate_unit_inputtransportsecond) = 2 * (ge_balance_positive_associate_unit_inputtransportsecondreal) /\ (ge_balance_negative_associate_unit_inputtransportsecondreal) = 0) \/ exists ge_signed_half_associate_unit_inputtransportsecondrealdecode. (((ge_representation_real_code_associate_unit_inputtransportsecond) = 2 * ge_signed_half_associate_unit_inputtransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_unit_inputtransportsecondreal) = 0) /\ (ge_balance_negative_associate_unit_inputtransportsecondreal) = S ge_signed_half_associate_unit_inputtransportsecondrealdecode))) /\ ((ge_second_rp_associate_unit_inputtransport) + ge_balance_negative_associate_unit_inputtransportsecondreal = (ge_second_rn_associate_unit_inputtransport) + ge_balance_positive_associate_unit_inputtransportsecondreal))) /\ (exists ge_balance_positive_associate_unit_inputtransportsecondimaginary ge_balance_negative_associate_unit_inputtransportsecondimaginary. (((((ge_representation_imaginary_code_associate_unit_inputtransportsecond) = 2 * (ge_balance_positive_associate_unit_inputtransportsecondimaginary) /\ (ge_balance_negative_associate_unit_inputtransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_unit_inputtransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_unit_inputtransportsecond) = 2 * ge_signed_half_associate_unit_inputtransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_inputtransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_unit_inputtransportsecondimaginary) = S ge_signed_half_associate_unit_inputtransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_unit_inputtransport) + ge_balance_negative_associate_unit_inputtransportsecondimaginary = (ge_second_in_associate_unit_inputtransport) + ge_balance_positive_associate_unit_inputtransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_unit_inputtransportoutput ge_representation_imaginary_code_associate_unit_inputtransportoutput. (((b) = ((ge_representation_real_code_associate_unit_inputtransportoutput) + (ge_representation_imaginary_code_associate_unit_inputtransportoutput)) * S ((ge_representation_real_code_associate_unit_inputtransportoutput) + (ge_representation_imaginary_code_associate_unit_inputtransportoutput)) + ((ge_representation_imaginary_code_associate_unit_inputtransportoutput) + (ge_representation_imaginary_code_associate_unit_inputtransportoutput))) /\ ((exists ge_balance_positive_associate_unit_inputtransportoutputreal ge_balance_negative_associate_unit_inputtransportoutputreal. (((((ge_representation_real_code_associate_unit_inputtransportoutput) = 2 * (ge_balance_positive_associate_unit_inputtransportoutputreal) /\ (ge_balance_negative_associate_unit_inputtransportoutputreal) = 0) \/ exists ge_signed_half_associate_unit_inputtransportoutputrealdecode. (((ge_representation_real_code_associate_unit_inputtransportoutput) = 2 * ge_signed_half_associate_unit_inputtransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_unit_inputtransportoutputreal) = 0) /\ (ge_balance_negative_associate_unit_inputtransportoutputreal) = S ge_signed_half_associate_unit_inputtransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_unit_inputtransport) * (ge_second_rp_associate_unit_inputtransport))) + (((ge_first_rn_associate_unit_inputtransport) * (ge_second_rn_associate_unit_inputtransport))))) + (((((ge_first_ip_associate_unit_inputtransport) * (ge_second_in_associate_unit_inputtransport))) + (((ge_first_in_associate_unit_inputtransport) * (ge_second_ip_associate_unit_inputtransport))))))) + ge_balance_negative_associate_unit_inputtransportoutputreal = (((((((ge_first_rp_associate_unit_inputtransport) * (ge_second_rn_associate_unit_inputtransport))) + (((ge_first_rn_associate_unit_inputtransport) * (ge_second_rp_associate_unit_inputtransport))))) + (((((ge_first_ip_associate_unit_inputtransport) * (ge_second_ip_associate_unit_inputtransport))) + (((ge_first_in_associate_unit_inputtransport) * (ge_second_in_associate_unit_inputtransport))))))) + ge_balance_positive_associate_unit_inputtransportoutputreal))) /\ (exists ge_balance_positive_associate_unit_inputtransportoutputimaginary ge_balance_negative_associate_unit_inputtransportoutputimaginary. (((((ge_representation_imaginary_code_associate_unit_inputtransportoutput) = 2 * (ge_balance_positive_associate_unit_inputtransportoutputimaginary) /\ (ge_balance_negative_associate_unit_inputtransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_unit_inputtransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_unit_inputtransportoutput) = 2 * ge_signed_half_associate_unit_inputtransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_inputtransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_unit_inputtransportoutputimaginary) = S ge_signed_half_associate_unit_inputtransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_unit_inputtransport) * (ge_second_ip_associate_unit_inputtransport))) + (((ge_first_rn_associate_unit_inputtransport) * (ge_second_in_associate_unit_inputtransport))))) + (((((ge_first_ip_associate_unit_inputtransport) * (ge_second_rp_associate_unit_inputtransport))) + (((ge_first_in_associate_unit_inputtransport) * (ge_second_rn_associate_unit_inputtransport))))))) + ge_balance_negative_associate_unit_inputtransportoutputimaginary = (((((((ge_first_rp_associate_unit_inputtransport) * (ge_second_in_associate_unit_inputtransport))) + (((ge_first_rn_associate_unit_inputtransport) * (ge_second_ip_associate_unit_inputtransport))))) + (((((ge_first_ip_associate_unit_inputtransport) * (ge_second_rn_associate_unit_inputtransport))) + (((ge_first_in_associate_unit_inputtransport) * (ge_second_rp_associate_unit_inputtransport))))))) + ge_balance_positive_associate_unit_inputtransportoutputimaginary))))))))))) -> (exists gr_inverse_associate_unit_source. (exists ge_first_rp_associate_unit_sourceidentity ge_first_rn_associate_unit_sourceidentity ge_first_ip_associate_unit_sourceidentity ge_first_in_associate_unit_sourceidentity ge_second_rp_associate_unit_sourceidentity ge_second_rn_associate_unit_sourceidentity ge_second_ip_associate_unit_sourceidentity ge_second_in_associate_unit_sourceidentity. ((exists ge_representation_real_code_associate_unit_sourceidentityfirst ge_representation_imaginary_code_associate_unit_sourceidentityfirst. (((a) = ((ge_representation_real_code_associate_unit_sourceidentityfirst) + (ge_representation_imaginary_code_associate_unit_sourceidentityfirst)) * S ((ge_representation_real_code_associate_unit_sourceidentityfirst) + (ge_representation_imaginary_code_associate_unit_sourceidentityfirst)) + ((ge_representation_imaginary_code_associate_unit_sourceidentityfirst) + (ge_representation_imaginary_code_associate_unit_sourceidentityfirst))) /\ ((exists ge_balance_positive_associate_unit_sourceidentityfirstreal ge_balance_negative_associate_unit_sourceidentityfirstreal. (((((ge_representation_real_code_associate_unit_sourceidentityfirst) = 2 * (ge_balance_positive_associate_unit_sourceidentityfirstreal) /\ (ge_balance_negative_associate_unit_sourceidentityfirstreal) = 0) \/ exists ge_signed_half_associate_unit_sourceidentityfirstrealdecode. (((ge_representation_real_code_associate_unit_sourceidentityfirst) = 2 * ge_signed_half_associate_unit_sourceidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_unit_sourceidentityfirstreal) = 0) /\ (ge_balance_negative_associate_unit_sourceidentityfirstreal) = S ge_signed_half_associate_unit_sourceidentityfirstrealdecode))) /\ ((ge_first_rp_associate_unit_sourceidentity) + ge_balance_negative_associate_unit_sourceidentityfirstreal = (ge_first_rn_associate_unit_sourceidentity) + ge_balance_positive_associate_unit_sourceidentityfirstreal))) /\ (exists ge_balance_positive_associate_unit_sourceidentityfirstimaginary ge_balance_negative_associate_unit_sourceidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_unit_sourceidentityfirst) = 2 * (ge_balance_positive_associate_unit_sourceidentityfirstimaginary) /\ (ge_balance_negative_associate_unit_sourceidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_unit_sourceidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_unit_sourceidentityfirst) = 2 * ge_signed_half_associate_unit_sourceidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_sourceidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_unit_sourceidentityfirstimaginary) = S ge_signed_half_associate_unit_sourceidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_unit_sourceidentity) + ge_balance_negative_associate_unit_sourceidentityfirstimaginary = (ge_first_in_associate_unit_sourceidentity) + ge_balance_positive_associate_unit_sourceidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_unit_sourceidentitysecond ge_representation_imaginary_code_associate_unit_sourceidentitysecond. (((gr_inverse_associate_unit_source) = ((ge_representation_real_code_associate_unit_sourceidentitysecond) + (ge_representation_imaginary_code_associate_unit_sourceidentitysecond)) * S ((ge_representation_real_code_associate_unit_sourceidentitysecond) + (ge_representation_imaginary_code_associate_unit_sourceidentitysecond)) + ((ge_representation_imaginary_code_associate_unit_sourceidentitysecond) + (ge_representation_imaginary_code_associate_unit_sourceidentitysecond))) /\ ((exists ge_balance_positive_associate_unit_sourceidentitysecondreal ge_balance_negative_associate_unit_sourceidentitysecondreal. (((((ge_representation_real_code_associate_unit_sourceidentitysecond) = 2 * (ge_balance_positive_associate_unit_sourceidentitysecondreal) /\ (ge_balance_negative_associate_unit_sourceidentitysecondreal) = 0) \/ exists ge_signed_half_associate_unit_sourceidentitysecondrealdecode. (((ge_representation_real_code_associate_unit_sourceidentitysecond) = 2 * ge_signed_half_associate_unit_sourceidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_unit_sourceidentitysecondreal) = 0) /\ (ge_balance_negative_associate_unit_sourceidentitysecondreal) = S ge_signed_half_associate_unit_sourceidentitysecondrealdecode))) /\ ((ge_second_rp_associate_unit_sourceidentity) + ge_balance_negative_associate_unit_sourceidentitysecondreal = (ge_second_rn_associate_unit_sourceidentity) + ge_balance_positive_associate_unit_sourceidentitysecondreal))) /\ (exists ge_balance_positive_associate_unit_sourceidentitysecondimaginary ge_balance_negative_associate_unit_sourceidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_unit_sourceidentitysecond) = 2 * (ge_balance_positive_associate_unit_sourceidentitysecondimaginary) /\ (ge_balance_negative_associate_unit_sourceidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_unit_sourceidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_unit_sourceidentitysecond) = 2 * ge_signed_half_associate_unit_sourceidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_sourceidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_unit_sourceidentitysecondimaginary) = S ge_signed_half_associate_unit_sourceidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_unit_sourceidentity) + ge_balance_negative_associate_unit_sourceidentitysecondimaginary = (ge_second_in_associate_unit_sourceidentity) + ge_balance_positive_associate_unit_sourceidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_unit_sourceidentityoutput ge_representation_imaginary_code_associate_unit_sourceidentityoutput. (((6) = ((ge_representation_real_code_associate_unit_sourceidentityoutput) + (ge_representation_imaginary_code_associate_unit_sourceidentityoutput)) * S ((ge_representation_real_code_associate_unit_sourceidentityoutput) + (ge_representation_imaginary_code_associate_unit_sourceidentityoutput)) + ((ge_representation_imaginary_code_associate_unit_sourceidentityoutput) + (ge_representation_imaginary_code_associate_unit_sourceidentityoutput))) /\ ((exists ge_balance_positive_associate_unit_sourceidentityoutputreal ge_balance_negative_associate_unit_sourceidentityoutputreal. (((((ge_representation_real_code_associate_unit_sourceidentityoutput) = 2 * (ge_balance_positive_associate_unit_sourceidentityoutputreal) /\ (ge_balance_negative_associate_unit_sourceidentityoutputreal) = 0) \/ exists ge_signed_half_associate_unit_sourceidentityoutputrealdecode. (((ge_representation_real_code_associate_unit_sourceidentityoutput) = 2 * ge_signed_half_associate_unit_sourceidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_unit_sourceidentityoutputreal) = 0) /\ (ge_balance_negative_associate_unit_sourceidentityoutputreal) = S ge_signed_half_associate_unit_sourceidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_unit_sourceidentity) * (ge_second_rp_associate_unit_sourceidentity))) + (((ge_first_rn_associate_unit_sourceidentity) * (ge_second_rn_associate_unit_sourceidentity))))) + (((((ge_first_ip_associate_unit_sourceidentity) * (ge_second_in_associate_unit_sourceidentity))) + (((ge_first_in_associate_unit_sourceidentity) * (ge_second_ip_associate_unit_sourceidentity))))))) + ge_balance_negative_associate_unit_sourceidentityoutputreal = (((((((ge_first_rp_associate_unit_sourceidentity) * (ge_second_rn_associate_unit_sourceidentity))) + (((ge_first_rn_associate_unit_sourceidentity) * (ge_second_rp_associate_unit_sourceidentity))))) + (((((ge_first_ip_associate_unit_sourceidentity) * (ge_second_ip_associate_unit_sourceidentity))) + (((ge_first_in_associate_unit_sourceidentity) * (ge_second_in_associate_unit_sourceidentity))))))) + ge_balance_positive_associate_unit_sourceidentityoutputreal))) /\ (exists ge_balance_positive_associate_unit_sourceidentityoutputimaginary ge_balance_negative_associate_unit_sourceidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_unit_sourceidentityoutput) = 2 * (ge_balance_positive_associate_unit_sourceidentityoutputimaginary) /\ (ge_balance_negative_associate_unit_sourceidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_unit_sourceidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_unit_sourceidentityoutput) = 2 * ge_signed_half_associate_unit_sourceidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_sourceidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_unit_sourceidentityoutputimaginary) = S ge_signed_half_associate_unit_sourceidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_unit_sourceidentity) * (ge_second_ip_associate_unit_sourceidentity))) + (((ge_first_rn_associate_unit_sourceidentity) * (ge_second_in_associate_unit_sourceidentity))))) + (((((ge_first_ip_associate_unit_sourceidentity) * (ge_second_rp_associate_unit_sourceidentity))) + (((ge_first_in_associate_unit_sourceidentity) * (ge_second_rn_associate_unit_sourceidentity))))))) + ge_balance_negative_associate_unit_sourceidentityoutputimaginary = (((((((ge_first_rp_associate_unit_sourceidentity) * (ge_second_in_associate_unit_sourceidentity))) + (((ge_first_rn_associate_unit_sourceidentity) * (ge_second_ip_associate_unit_sourceidentity))))) + (((((ge_first_ip_associate_unit_sourceidentity) * (ge_second_rn_associate_unit_sourceidentity))) + (((ge_first_in_associate_unit_sourceidentity) * (ge_second_rp_associate_unit_sourceidentity))))))) + ge_balance_positive_associate_unit_sourceidentityoutputimaginary)))))))))) -> (exists gr_inverse_associate_unit_result. (exists ge_first_rp_associate_unit_resultidentity ge_first_rn_associate_unit_resultidentity ge_first_ip_associate_unit_resultidentity ge_first_in_associate_unit_resultidentity ge_second_rp_associate_unit_resultidentity ge_second_rn_associate_unit_resultidentity ge_second_ip_associate_unit_resultidentity ge_second_in_associate_unit_resultidentity. ((exists ge_representation_real_code_associate_unit_resultidentityfirst ge_representation_imaginary_code_associate_unit_resultidentityfirst. (((b) = ((ge_representation_real_code_associate_unit_resultidentityfirst) + (ge_representation_imaginary_code_associate_unit_resultidentityfirst)) * S ((ge_representation_real_code_associate_unit_resultidentityfirst) + (ge_representation_imaginary_code_associate_unit_resultidentityfirst)) + ((ge_representation_imaginary_code_associate_unit_resultidentityfirst) + (ge_representation_imaginary_code_associate_unit_resultidentityfirst))) /\ ((exists ge_balance_positive_associate_unit_resultidentityfirstreal ge_balance_negative_associate_unit_resultidentityfirstreal. (((((ge_representation_real_code_associate_unit_resultidentityfirst) = 2 * (ge_balance_positive_associate_unit_resultidentityfirstreal) /\ (ge_balance_negative_associate_unit_resultidentityfirstreal) = 0) \/ exists ge_signed_half_associate_unit_resultidentityfirstrealdecode. (((ge_representation_real_code_associate_unit_resultidentityfirst) = 2 * ge_signed_half_associate_unit_resultidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_unit_resultidentityfirstreal) = 0) /\ (ge_balance_negative_associate_unit_resultidentityfirstreal) = S ge_signed_half_associate_unit_resultidentityfirstrealdecode))) /\ ((ge_first_rp_associate_unit_resultidentity) + ge_balance_negative_associate_unit_resultidentityfirstreal = (ge_first_rn_associate_unit_resultidentity) + ge_balance_positive_associate_unit_resultidentityfirstreal))) /\ (exists ge_balance_positive_associate_unit_resultidentityfirstimaginary ge_balance_negative_associate_unit_resultidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_unit_resultidentityfirst) = 2 * (ge_balance_positive_associate_unit_resultidentityfirstimaginary) /\ (ge_balance_negative_associate_unit_resultidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_unit_resultidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_unit_resultidentityfirst) = 2 * ge_signed_half_associate_unit_resultidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_resultidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_unit_resultidentityfirstimaginary) = S ge_signed_half_associate_unit_resultidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_unit_resultidentity) + ge_balance_negative_associate_unit_resultidentityfirstimaginary = (ge_first_in_associate_unit_resultidentity) + ge_balance_positive_associate_unit_resultidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_unit_resultidentitysecond ge_representation_imaginary_code_associate_unit_resultidentitysecond. (((gr_inverse_associate_unit_result) = ((ge_representation_real_code_associate_unit_resultidentitysecond) + (ge_representation_imaginary_code_associate_unit_resultidentitysecond)) * S ((ge_representation_real_code_associate_unit_resultidentitysecond) + (ge_representation_imaginary_code_associate_unit_resultidentitysecond)) + ((ge_representation_imaginary_code_associate_unit_resultidentitysecond) + (ge_representation_imaginary_code_associate_unit_resultidentitysecond))) /\ ((exists ge_balance_positive_associate_unit_resultidentitysecondreal ge_balance_negative_associate_unit_resultidentitysecondreal. (((((ge_representation_real_code_associate_unit_resultidentitysecond) = 2 * (ge_balance_positive_associate_unit_resultidentitysecondreal) /\ (ge_balance_negative_associate_unit_resultidentitysecondreal) = 0) \/ exists ge_signed_half_associate_unit_resultidentitysecondrealdecode. (((ge_representation_real_code_associate_unit_resultidentitysecond) = 2 * ge_signed_half_associate_unit_resultidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_unit_resultidentitysecondreal) = 0) /\ (ge_balance_negative_associate_unit_resultidentitysecondreal) = S ge_signed_half_associate_unit_resultidentitysecondrealdecode))) /\ ((ge_second_rp_associate_unit_resultidentity) + ge_balance_negative_associate_unit_resultidentitysecondreal = (ge_second_rn_associate_unit_resultidentity) + ge_balance_positive_associate_unit_resultidentitysecondreal))) /\ (exists ge_balance_positive_associate_unit_resultidentitysecondimaginary ge_balance_negative_associate_unit_resultidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_unit_resultidentitysecond) = 2 * (ge_balance_positive_associate_unit_resultidentitysecondimaginary) /\ (ge_balance_negative_associate_unit_resultidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_unit_resultidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_unit_resultidentitysecond) = 2 * ge_signed_half_associate_unit_resultidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_resultidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_unit_resultidentitysecondimaginary) = S ge_signed_half_associate_unit_resultidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_unit_resultidentity) + ge_balance_negative_associate_unit_resultidentitysecondimaginary = (ge_second_in_associate_unit_resultidentity) + ge_balance_positive_associate_unit_resultidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_unit_resultidentityoutput ge_representation_imaginary_code_associate_unit_resultidentityoutput. (((6) = ((ge_representation_real_code_associate_unit_resultidentityoutput) + (ge_representation_imaginary_code_associate_unit_resultidentityoutput)) * S ((ge_representation_real_code_associate_unit_resultidentityoutput) + (ge_representation_imaginary_code_associate_unit_resultidentityoutput)) + ((ge_representation_imaginary_code_associate_unit_resultidentityoutput) + (ge_representation_imaginary_code_associate_unit_resultidentityoutput))) /\ ((exists ge_balance_positive_associate_unit_resultidentityoutputreal ge_balance_negative_associate_unit_resultidentityoutputreal. (((((ge_representation_real_code_associate_unit_resultidentityoutput) = 2 * (ge_balance_positive_associate_unit_resultidentityoutputreal) /\ (ge_balance_negative_associate_unit_resultidentityoutputreal) = 0) \/ exists ge_signed_half_associate_unit_resultidentityoutputrealdecode. (((ge_representation_real_code_associate_unit_resultidentityoutput) = 2 * ge_signed_half_associate_unit_resultidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_unit_resultidentityoutputreal) = 0) /\ (ge_balance_negative_associate_unit_resultidentityoutputreal) = S ge_signed_half_associate_unit_resultidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_unit_resultidentity) * (ge_second_rp_associate_unit_resultidentity))) + (((ge_first_rn_associate_unit_resultidentity) * (ge_second_rn_associate_unit_resultidentity))))) + (((((ge_first_ip_associate_unit_resultidentity) * (ge_second_in_associate_unit_resultidentity))) + (((ge_first_in_associate_unit_resultidentity) * (ge_second_ip_associate_unit_resultidentity))))))) + ge_balance_negative_associate_unit_resultidentityoutputreal = (((((((ge_first_rp_associate_unit_resultidentity) * (ge_second_rn_associate_unit_resultidentity))) + (((ge_first_rn_associate_unit_resultidentity) * (ge_second_rp_associate_unit_resultidentity))))) + (((((ge_first_ip_associate_unit_resultidentity) * (ge_second_ip_associate_unit_resultidentity))) + (((ge_first_in_associate_unit_resultidentity) * (ge_second_in_associate_unit_resultidentity))))))) + ge_balance_positive_associate_unit_resultidentityoutputreal))) /\ (exists ge_balance_positive_associate_unit_resultidentityoutputimaginary ge_balance_negative_associate_unit_resultidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_unit_resultidentityoutput) = 2 * (ge_balance_positive_associate_unit_resultidentityoutputimaginary) /\ (ge_balance_negative_associate_unit_resultidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_unit_resultidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_unit_resultidentityoutput) = 2 * ge_signed_half_associate_unit_resultidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_unit_resultidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_unit_resultidentityoutputimaginary) = S ge_signed_half_associate_unit_resultidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_unit_resultidentity) * (ge_second_ip_associate_unit_resultidentity))) + (((ge_first_rn_associate_unit_resultidentity) * (ge_second_in_associate_unit_resultidentity))))) + (((((ge_first_ip_associate_unit_resultidentity) * (ge_second_rp_associate_unit_resultidentity))) + (((ge_first_in_associate_unit_resultidentity) * (ge_second_rn_associate_unit_resultidentity))))))) + ge_balance_negative_associate_unit_resultidentityoutputimaginary = (((((((ge_first_rp_associate_unit_resultidentity) * (ge_second_in_associate_unit_resultidentity))) + (((ge_first_rn_associate_unit_resultidentity) * (ge_second_ip_associate_unit_resultidentity))))) + (((((ge_first_ip_associate_unit_resultidentity) * (ge_second_rn_associate_unit_resultidentity))) + (((ge_first_in_associate_unit_resultidentity) * (ge_second_rp_associate_unit_resultidentity))))))) + ge_balance_positive_associate_unit_resultidentityoutputimaginary))))))))))