gaussian_associate_divides

Exact expanded first-order arithmetic statement

forall a b. (exists gr_unit_associate_division. ((exists gr_inverse_associate_divisionunit. (exists ge_first_rp_associate_divisionunitidentity ge_first_rn_associate_divisionunitidentity ge_first_ip_associate_divisionunitidentity ge_first_in_associate_divisionunitidentity ge_second_rp_associate_divisionunitidentity ge_second_rn_associate_divisionunitidentity ge_second_ip_associate_divisionunitidentity ge_second_in_associate_divisionunitidentity. ((exists ge_representation_real_code_associate_divisionunitidentityfirst ge_representation_imaginary_code_associate_divisionunitidentityfirst. (((gr_unit_associate_division) = ((ge_representation_real_code_associate_divisionunitidentityfirst) + (ge_representation_imaginary_code_associate_divisionunitidentityfirst)) * S ((ge_representation_real_code_associate_divisionunitidentityfirst) + (ge_representation_imaginary_code_associate_divisionunitidentityfirst)) + ((ge_representation_imaginary_code_associate_divisionunitidentityfirst) + (ge_representation_imaginary_code_associate_divisionunitidentityfirst))) /\ ((exists ge_balance_positive_associate_divisionunitidentityfirstreal ge_balance_negative_associate_divisionunitidentityfirstreal. (((((ge_representation_real_code_associate_divisionunitidentityfirst) = 2 * (ge_balance_positive_associate_divisionunitidentityfirstreal) /\ (ge_balance_negative_associate_divisionunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_divisionunitidentityfirstrealdecode. (((ge_representation_real_code_associate_divisionunitidentityfirst) = 2 * ge_signed_half_associate_divisionunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_divisionunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_divisionunitidentityfirstreal) = S ge_signed_half_associate_divisionunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_divisionunitidentity) + ge_balance_negative_associate_divisionunitidentityfirstreal = (ge_first_rn_associate_divisionunitidentity) + ge_balance_positive_associate_divisionunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_divisionunitidentityfirstimaginary ge_balance_negative_associate_divisionunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_divisionunitidentityfirst) = 2 * (ge_balance_positive_associate_divisionunitidentityfirstimaginary) /\ (ge_balance_negative_associate_divisionunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_divisionunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_divisionunitidentityfirst) = 2 * ge_signed_half_associate_divisionunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_divisionunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_divisionunitidentityfirstimaginary) = S ge_signed_half_associate_divisionunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_divisionunitidentity) + ge_balance_negative_associate_divisionunitidentityfirstimaginary = (ge_first_in_associate_divisionunitidentity) + ge_balance_positive_associate_divisionunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_divisionunitidentitysecond ge_representation_imaginary_code_associate_divisionunitidentitysecond. (((gr_inverse_associate_divisionunit) = ((ge_representation_real_code_associate_divisionunitidentitysecond) + (ge_representation_imaginary_code_associate_divisionunitidentitysecond)) * S ((ge_representation_real_code_associate_divisionunitidentitysecond) + (ge_representation_imaginary_code_associate_divisionunitidentitysecond)) + ((ge_representation_imaginary_code_associate_divisionunitidentitysecond) + (ge_representation_imaginary_code_associate_divisionunitidentitysecond))) /\ ((exists ge_balance_positive_associate_divisionunitidentitysecondreal ge_balance_negative_associate_divisionunitidentitysecondreal. (((((ge_representation_real_code_associate_divisionunitidentitysecond) = 2 * (ge_balance_positive_associate_divisionunitidentitysecondreal) /\ (ge_balance_negative_associate_divisionunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_divisionunitidentitysecondrealdecode. (((ge_representation_real_code_associate_divisionunitidentitysecond) = 2 * ge_signed_half_associate_divisionunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_divisionunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_divisionunitidentitysecondreal) = S ge_signed_half_associate_divisionunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_divisionunitidentity) + ge_balance_negative_associate_divisionunitidentitysecondreal = (ge_second_rn_associate_divisionunitidentity) + ge_balance_positive_associate_divisionunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_divisionunitidentitysecondimaginary ge_balance_negative_associate_divisionunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_divisionunitidentitysecond) = 2 * (ge_balance_positive_associate_divisionunitidentitysecondimaginary) /\ (ge_balance_negative_associate_divisionunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_divisionunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_divisionunitidentitysecond) = 2 * ge_signed_half_associate_divisionunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_divisionunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_divisionunitidentitysecondimaginary) = S ge_signed_half_associate_divisionunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_divisionunitidentity) + ge_balance_negative_associate_divisionunitidentitysecondimaginary = (ge_second_in_associate_divisionunitidentity) + ge_balance_positive_associate_divisionunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_divisionunitidentityoutput ge_representation_imaginary_code_associate_divisionunitidentityoutput. (((6) = ((ge_representation_real_code_associate_divisionunitidentityoutput) + (ge_representation_imaginary_code_associate_divisionunitidentityoutput)) * S ((ge_representation_real_code_associate_divisionunitidentityoutput) + (ge_representation_imaginary_code_associate_divisionunitidentityoutput)) + ((ge_representation_imaginary_code_associate_divisionunitidentityoutput) + (ge_representation_imaginary_code_associate_divisionunitidentityoutput))) /\ ((exists ge_balance_positive_associate_divisionunitidentityoutputreal ge_balance_negative_associate_divisionunitidentityoutputreal. (((((ge_representation_real_code_associate_divisionunitidentityoutput) = 2 * (ge_balance_positive_associate_divisionunitidentityoutputreal) /\ (ge_balance_negative_associate_divisionunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_divisionunitidentityoutputrealdecode. (((ge_representation_real_code_associate_divisionunitidentityoutput) = 2 * ge_signed_half_associate_divisionunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_divisionunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_divisionunitidentityoutputreal) = S ge_signed_half_associate_divisionunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_divisionunitidentity) * (ge_second_rp_associate_divisionunitidentity))) + (((ge_first_rn_associate_divisionunitidentity) * (ge_second_rn_associate_divisionunitidentity))))) + (((((ge_first_ip_associate_divisionunitidentity) * (ge_second_in_associate_divisionunitidentity))) + (((ge_first_in_associate_divisionunitidentity) * (ge_second_ip_associate_divisionunitidentity))))))) + ge_balance_negative_associate_divisionunitidentityoutputreal = (((((((ge_first_rp_associate_divisionunitidentity) * (ge_second_rn_associate_divisionunitidentity))) + (((ge_first_rn_associate_divisionunitidentity) * (ge_second_rp_associate_divisionunitidentity))))) + (((((ge_first_ip_associate_divisionunitidentity) * (ge_second_ip_associate_divisionunitidentity))) + (((ge_first_in_associate_divisionunitidentity) * (ge_second_in_associate_divisionunitidentity))))))) + ge_balance_positive_associate_divisionunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_divisionunitidentityoutputimaginary ge_balance_negative_associate_divisionunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_divisionunitidentityoutput) = 2 * (ge_balance_positive_associate_divisionunitidentityoutputimaginary) /\ (ge_balance_negative_associate_divisionunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_divisionunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_divisionunitidentityoutput) = 2 * ge_signed_half_associate_divisionunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_divisionunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_divisionunitidentityoutputimaginary) = S ge_signed_half_associate_divisionunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_divisionunitidentity) * (ge_second_ip_associate_divisionunitidentity))) + (((ge_first_rn_associate_divisionunitidentity) * (ge_second_in_associate_divisionunitidentity))))) + (((((ge_first_ip_associate_divisionunitidentity) * (ge_second_rp_associate_divisionunitidentity))) + (((ge_first_in_associate_divisionunitidentity) * (ge_second_rn_associate_divisionunitidentity))))))) + ge_balance_negative_associate_divisionunitidentityoutputimaginary = (((((((ge_first_rp_associate_divisionunitidentity) * (ge_second_in_associate_divisionunitidentity))) + (((ge_first_rn_associate_divisionunitidentity) * (ge_second_ip_associate_divisionunitidentity))))) + (((((ge_first_ip_associate_divisionunitidentity) * (ge_second_rn_associate_divisionunitidentity))) + (((ge_first_in_associate_divisionunitidentity) * (ge_second_rp_associate_divisionunitidentity))))))) + ge_balance_positive_associate_divisionunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_divisiontransport ge_first_rn_associate_divisiontransport ge_first_ip_associate_divisiontransport ge_first_in_associate_divisiontransport ge_second_rp_associate_divisiontransport ge_second_rn_associate_divisiontransport ge_second_ip_associate_divisiontransport ge_second_in_associate_divisiontransport. ((exists ge_representation_real_code_associate_divisiontransportfirst ge_representation_imaginary_code_associate_divisiontransportfirst. (((gr_unit_associate_division) = ((ge_representation_real_code_associate_divisiontransportfirst) + (ge_representation_imaginary_code_associate_divisiontransportfirst)) * S ((ge_representation_real_code_associate_divisiontransportfirst) + (ge_representation_imaginary_code_associate_divisiontransportfirst)) + ((ge_representation_imaginary_code_associate_divisiontransportfirst) + (ge_representation_imaginary_code_associate_divisiontransportfirst))) /\ ((exists ge_balance_positive_associate_divisiontransportfirstreal ge_balance_negative_associate_divisiontransportfirstreal. (((((ge_representation_real_code_associate_divisiontransportfirst) = 2 * (ge_balance_positive_associate_divisiontransportfirstreal) /\ (ge_balance_negative_associate_divisiontransportfirstreal) = 0) \/ exists ge_signed_half_associate_divisiontransportfirstrealdecode. (((ge_representation_real_code_associate_divisiontransportfirst) = 2 * ge_signed_half_associate_divisiontransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_divisiontransportfirstreal) = 0) /\ (ge_balance_negative_associate_divisiontransportfirstreal) = S ge_signed_half_associate_divisiontransportfirstrealdecode))) /\ ((ge_first_rp_associate_divisiontransport) + ge_balance_negative_associate_divisiontransportfirstreal = (ge_first_rn_associate_divisiontransport) + ge_balance_positive_associate_divisiontransportfirstreal))) /\ (exists ge_balance_positive_associate_divisiontransportfirstimaginary ge_balance_negative_associate_divisiontransportfirstimaginary. (((((ge_representation_imaginary_code_associate_divisiontransportfirst) = 2 * (ge_balance_positive_associate_divisiontransportfirstimaginary) /\ (ge_balance_negative_associate_divisiontransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_divisiontransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_divisiontransportfirst) = 2 * ge_signed_half_associate_divisiontransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_divisiontransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_divisiontransportfirstimaginary) = S ge_signed_half_associate_divisiontransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_divisiontransport) + ge_balance_negative_associate_divisiontransportfirstimaginary = (ge_first_in_associate_divisiontransport) + ge_balance_positive_associate_divisiontransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_divisiontransportsecond ge_representation_imaginary_code_associate_divisiontransportsecond. (((a) = ((ge_representation_real_code_associate_divisiontransportsecond) + (ge_representation_imaginary_code_associate_divisiontransportsecond)) * S ((ge_representation_real_code_associate_divisiontransportsecond) + (ge_representation_imaginary_code_associate_divisiontransportsecond)) + ((ge_representation_imaginary_code_associate_divisiontransportsecond) + (ge_representation_imaginary_code_associate_divisiontransportsecond))) /\ ((exists ge_balance_positive_associate_divisiontransportsecondreal ge_balance_negative_associate_divisiontransportsecondreal. (((((ge_representation_real_code_associate_divisiontransportsecond) = 2 * (ge_balance_positive_associate_divisiontransportsecondreal) /\ (ge_balance_negative_associate_divisiontransportsecondreal) = 0) \/ exists ge_signed_half_associate_divisiontransportsecondrealdecode. (((ge_representation_real_code_associate_divisiontransportsecond) = 2 * ge_signed_half_associate_divisiontransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_divisiontransportsecondreal) = 0) /\ (ge_balance_negative_associate_divisiontransportsecondreal) = S ge_signed_half_associate_divisiontransportsecondrealdecode))) /\ ((ge_second_rp_associate_divisiontransport) + ge_balance_negative_associate_divisiontransportsecondreal = (ge_second_rn_associate_divisiontransport) + ge_balance_positive_associate_divisiontransportsecondreal))) /\ (exists ge_balance_positive_associate_divisiontransportsecondimaginary ge_balance_negative_associate_divisiontransportsecondimaginary. (((((ge_representation_imaginary_code_associate_divisiontransportsecond) = 2 * (ge_balance_positive_associate_divisiontransportsecondimaginary) /\ (ge_balance_negative_associate_divisiontransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_divisiontransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_divisiontransportsecond) = 2 * ge_signed_half_associate_divisiontransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_divisiontransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_divisiontransportsecondimaginary) = S ge_signed_half_associate_divisiontransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_divisiontransport) + ge_balance_negative_associate_divisiontransportsecondimaginary = (ge_second_in_associate_divisiontransport) + ge_balance_positive_associate_divisiontransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_divisiontransportoutput ge_representation_imaginary_code_associate_divisiontransportoutput. (((b) = ((ge_representation_real_code_associate_divisiontransportoutput) + (ge_representation_imaginary_code_associate_divisiontransportoutput)) * S ((ge_representation_real_code_associate_divisiontransportoutput) + (ge_representation_imaginary_code_associate_divisiontransportoutput)) + ((ge_representation_imaginary_code_associate_divisiontransportoutput) + (ge_representation_imaginary_code_associate_divisiontransportoutput))) /\ ((exists ge_balance_positive_associate_divisiontransportoutputreal ge_balance_negative_associate_divisiontransportoutputreal. (((((ge_representation_real_code_associate_divisiontransportoutput) = 2 * (ge_balance_positive_associate_divisiontransportoutputreal) /\ (ge_balance_negative_associate_divisiontransportoutputreal) = 0) \/ exists ge_signed_half_associate_divisiontransportoutputrealdecode. (((ge_representation_real_code_associate_divisiontransportoutput) = 2 * ge_signed_half_associate_divisiontransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_divisiontransportoutputreal) = 0) /\ (ge_balance_negative_associate_divisiontransportoutputreal) = S ge_signed_half_associate_divisiontransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_divisiontransport) * (ge_second_rp_associate_divisiontransport))) + (((ge_first_rn_associate_divisiontransport) * (ge_second_rn_associate_divisiontransport))))) + (((((ge_first_ip_associate_divisiontransport) * (ge_second_in_associate_divisiontransport))) + (((ge_first_in_associate_divisiontransport) * (ge_second_ip_associate_divisiontransport))))))) + ge_balance_negative_associate_divisiontransportoutputreal = (((((((ge_first_rp_associate_divisiontransport) * (ge_second_rn_associate_divisiontransport))) + (((ge_first_rn_associate_divisiontransport) * (ge_second_rp_associate_divisiontransport))))) + (((((ge_first_ip_associate_divisiontransport) * (ge_second_ip_associate_divisiontransport))) + (((ge_first_in_associate_divisiontransport) * (ge_second_in_associate_divisiontransport))))))) + ge_balance_positive_associate_divisiontransportoutputreal))) /\ (exists ge_balance_positive_associate_divisiontransportoutputimaginary ge_balance_negative_associate_divisiontransportoutputimaginary. (((((ge_representation_imaginary_code_associate_divisiontransportoutput) = 2 * (ge_balance_positive_associate_divisiontransportoutputimaginary) /\ (ge_balance_negative_associate_divisiontransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_divisiontransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_divisiontransportoutput) = 2 * ge_signed_half_associate_divisiontransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_divisiontransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_divisiontransportoutputimaginary) = S ge_signed_half_associate_divisiontransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_divisiontransport) * (ge_second_ip_associate_divisiontransport))) + (((ge_first_rn_associate_divisiontransport) * (ge_second_in_associate_divisiontransport))))) + (((((ge_first_ip_associate_divisiontransport) * (ge_second_rp_associate_divisiontransport))) + (((ge_first_in_associate_divisiontransport) * (ge_second_rn_associate_divisiontransport))))))) + ge_balance_negative_associate_divisiontransportoutputimaginary = (((((((ge_first_rp_associate_divisiontransport) * (ge_second_in_associate_divisiontransport))) + (((ge_first_rn_associate_divisiontransport) * (ge_second_ip_associate_divisiontransport))))) + (((((ge_first_ip_associate_divisiontransport) * (ge_second_rn_associate_divisiontransport))) + (((ge_first_in_associate_divisiontransport) * (ge_second_rp_associate_divisiontransport))))))) + ge_balance_positive_associate_divisiontransportoutputimaginary))))))))))) -> (exists gr_quotient_associate_divides. (exists ge_first_rp_associate_dividesproduct ge_first_rn_associate_dividesproduct ge_first_ip_associate_dividesproduct ge_first_in_associate_dividesproduct ge_second_rp_associate_dividesproduct ge_second_rn_associate_dividesproduct ge_second_ip_associate_dividesproduct ge_second_in_associate_dividesproduct. ((exists ge_representation_real_code_associate_dividesproductfirst ge_representation_imaginary_code_associate_dividesproductfirst. (((a) = ((ge_representation_real_code_associate_dividesproductfirst) + (ge_representation_imaginary_code_associate_dividesproductfirst)) * S ((ge_representation_real_code_associate_dividesproductfirst) + (ge_representation_imaginary_code_associate_dividesproductfirst)) + ((ge_representation_imaginary_code_associate_dividesproductfirst) + (ge_representation_imaginary_code_associate_dividesproductfirst))) /\ ((exists ge_balance_positive_associate_dividesproductfirstreal ge_balance_negative_associate_dividesproductfirstreal. (((((ge_representation_real_code_associate_dividesproductfirst) = 2 * (ge_balance_positive_associate_dividesproductfirstreal) /\ (ge_balance_negative_associate_dividesproductfirstreal) = 0) \/ exists ge_signed_half_associate_dividesproductfirstrealdecode. (((ge_representation_real_code_associate_dividesproductfirst) = 2 * ge_signed_half_associate_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_associate_dividesproductfirstreal) = 0) /\ (ge_balance_negative_associate_dividesproductfirstreal) = S ge_signed_half_associate_dividesproductfirstrealdecode))) /\ ((ge_first_rp_associate_dividesproduct) + ge_balance_negative_associate_dividesproductfirstreal = (ge_first_rn_associate_dividesproduct) + ge_balance_positive_associate_dividesproductfirstreal))) /\ (exists ge_balance_positive_associate_dividesproductfirstimaginary ge_balance_negative_associate_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_associate_dividesproductfirst) = 2 * (ge_balance_positive_associate_dividesproductfirstimaginary) /\ (ge_balance_negative_associate_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_associate_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_associate_dividesproductfirst) = 2 * ge_signed_half_associate_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_associate_dividesproductfirstimaginary) = S ge_signed_half_associate_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_associate_dividesproduct) + ge_balance_negative_associate_dividesproductfirstimaginary = (ge_first_in_associate_dividesproduct) + ge_balance_positive_associate_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_dividesproductsecond ge_representation_imaginary_code_associate_dividesproductsecond. (((gr_quotient_associate_divides) = ((ge_representation_real_code_associate_dividesproductsecond) + (ge_representation_imaginary_code_associate_dividesproductsecond)) * S ((ge_representation_real_code_associate_dividesproductsecond) + (ge_representation_imaginary_code_associate_dividesproductsecond)) + ((ge_representation_imaginary_code_associate_dividesproductsecond) + (ge_representation_imaginary_code_associate_dividesproductsecond))) /\ ((exists ge_balance_positive_associate_dividesproductsecondreal ge_balance_negative_associate_dividesproductsecondreal. (((((ge_representation_real_code_associate_dividesproductsecond) = 2 * (ge_balance_positive_associate_dividesproductsecondreal) /\ (ge_balance_negative_associate_dividesproductsecondreal) = 0) \/ exists ge_signed_half_associate_dividesproductsecondrealdecode. (((ge_representation_real_code_associate_dividesproductsecond) = 2 * ge_signed_half_associate_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_associate_dividesproductsecondreal) = 0) /\ (ge_balance_negative_associate_dividesproductsecondreal) = S ge_signed_half_associate_dividesproductsecondrealdecode))) /\ ((ge_second_rp_associate_dividesproduct) + ge_balance_negative_associate_dividesproductsecondreal = (ge_second_rn_associate_dividesproduct) + ge_balance_positive_associate_dividesproductsecondreal))) /\ (exists ge_balance_positive_associate_dividesproductsecondimaginary ge_balance_negative_associate_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_associate_dividesproductsecond) = 2 * (ge_balance_positive_associate_dividesproductsecondimaginary) /\ (ge_balance_negative_associate_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_associate_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_associate_dividesproductsecond) = 2 * ge_signed_half_associate_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_associate_dividesproductsecondimaginary) = S ge_signed_half_associate_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_associate_dividesproduct) + ge_balance_negative_associate_dividesproductsecondimaginary = (ge_second_in_associate_dividesproduct) + ge_balance_positive_associate_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_dividesproductoutput ge_representation_imaginary_code_associate_dividesproductoutput. (((b) = ((ge_representation_real_code_associate_dividesproductoutput) + (ge_representation_imaginary_code_associate_dividesproductoutput)) * S ((ge_representation_real_code_associate_dividesproductoutput) + (ge_representation_imaginary_code_associate_dividesproductoutput)) + ((ge_representation_imaginary_code_associate_dividesproductoutput) + (ge_representation_imaginary_code_associate_dividesproductoutput))) /\ ((exists ge_balance_positive_associate_dividesproductoutputreal ge_balance_negative_associate_dividesproductoutputreal. (((((ge_representation_real_code_associate_dividesproductoutput) = 2 * (ge_balance_positive_associate_dividesproductoutputreal) /\ (ge_balance_negative_associate_dividesproductoutputreal) = 0) \/ exists ge_signed_half_associate_dividesproductoutputrealdecode. (((ge_representation_real_code_associate_dividesproductoutput) = 2 * ge_signed_half_associate_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_associate_dividesproductoutputreal) = 0) /\ (ge_balance_negative_associate_dividesproductoutputreal) = S ge_signed_half_associate_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_associate_dividesproduct) * (ge_second_rp_associate_dividesproduct))) + (((ge_first_rn_associate_dividesproduct) * (ge_second_rn_associate_dividesproduct))))) + (((((ge_first_ip_associate_dividesproduct) * (ge_second_in_associate_dividesproduct))) + (((ge_first_in_associate_dividesproduct) * (ge_second_ip_associate_dividesproduct))))))) + ge_balance_negative_associate_dividesproductoutputreal = (((((((ge_first_rp_associate_dividesproduct) * (ge_second_rn_associate_dividesproduct))) + (((ge_first_rn_associate_dividesproduct) * (ge_second_rp_associate_dividesproduct))))) + (((((ge_first_ip_associate_dividesproduct) * (ge_second_ip_associate_dividesproduct))) + (((ge_first_in_associate_dividesproduct) * (ge_second_in_associate_dividesproduct))))))) + ge_balance_positive_associate_dividesproductoutputreal))) /\ (exists ge_balance_positive_associate_dividesproductoutputimaginary ge_balance_negative_associate_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_associate_dividesproductoutput) = 2 * (ge_balance_positive_associate_dividesproductoutputimaginary) /\ (ge_balance_negative_associate_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_associate_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_associate_dividesproductoutput) = 2 * ge_signed_half_associate_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_associate_dividesproductoutputimaginary) = S ge_signed_half_associate_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_dividesproduct) * (ge_second_ip_associate_dividesproduct))) + (((ge_first_rn_associate_dividesproduct) * (ge_second_in_associate_dividesproduct))))) + (((((ge_first_ip_associate_dividesproduct) * (ge_second_rp_associate_dividesproduct))) + (((ge_first_in_associate_dividesproduct) * (ge_second_rn_associate_dividesproduct))))))) + ge_balance_negative_associate_dividesproductoutputimaginary = (((((((ge_first_rp_associate_dividesproduct) * (ge_second_in_associate_dividesproduct))) + (((ge_first_rn_associate_dividesproduct) * (ge_second_ip_associate_dividesproduct))))) + (((((ge_first_ip_associate_dividesproduct) * (ge_second_rn_associate_dividesproduct))) + (((ge_first_in_associate_dividesproduct) * (ge_second_rp_associate_dividesproduct))))))) + ge_balance_positive_associate_dividesproductoutputimaginary))))))))))