gaussian_division_zero_remainder_divides

Exact expanded first-order arithmetic statement

forall a b q r. (exists ge_division_product_zero_remainder_equation. ((exists ge_first_rp_zero_remainder_equationproduct ge_first_rn_zero_remainder_equationproduct ge_first_ip_zero_remainder_equationproduct ge_first_in_zero_remainder_equationproduct ge_second_rp_zero_remainder_equationproduct ge_second_rn_zero_remainder_equationproduct ge_second_ip_zero_remainder_equationproduct ge_second_in_zero_remainder_equationproduct. ((exists ge_representation_real_code_zero_remainder_equationproductfirst ge_representation_imaginary_code_zero_remainder_equationproductfirst. (((b) = ((ge_representation_real_code_zero_remainder_equationproductfirst) + (ge_representation_imaginary_code_zero_remainder_equationproductfirst)) * S ((ge_representation_real_code_zero_remainder_equationproductfirst) + (ge_representation_imaginary_code_zero_remainder_equationproductfirst)) + ((ge_representation_imaginary_code_zero_remainder_equationproductfirst) + (ge_representation_imaginary_code_zero_remainder_equationproductfirst))) /\ ((exists ge_balance_positive_zero_remainder_equationproductfirstreal ge_balance_negative_zero_remainder_equationproductfirstreal. (((((ge_representation_real_code_zero_remainder_equationproductfirst) = 2 * (ge_balance_positive_zero_remainder_equationproductfirstreal) /\ (ge_balance_negative_zero_remainder_equationproductfirstreal) = 0) \/ exists ge_signed_half_zero_remainder_equationproductfirstrealdecode. (((ge_representation_real_code_zero_remainder_equationproductfirst) = 2 * ge_signed_half_zero_remainder_equationproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductfirstreal) = 0) /\ (ge_balance_negative_zero_remainder_equationproductfirstreal) = S ge_signed_half_zero_remainder_equationproductfirstrealdecode))) /\ ((ge_first_rp_zero_remainder_equationproduct) + ge_balance_negative_zero_remainder_equationproductfirstreal = (ge_first_rn_zero_remainder_equationproduct) + ge_balance_positive_zero_remainder_equationproductfirstreal))) /\ (exists ge_balance_positive_zero_remainder_equationproductfirstimaginary ge_balance_negative_zero_remainder_equationproductfirstimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationproductfirst) = 2 * (ge_balance_positive_zero_remainder_equationproductfirstimaginary) /\ (ge_balance_negative_zero_remainder_equationproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationproductfirst) = 2 * ge_signed_half_zero_remainder_equationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationproductfirstimaginary) = S ge_signed_half_zero_remainder_equationproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_remainder_equationproduct) + ge_balance_negative_zero_remainder_equationproductfirstimaginary = (ge_first_in_zero_remainder_equationproduct) + ge_balance_positive_zero_remainder_equationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_remainder_equationproductsecond ge_representation_imaginary_code_zero_remainder_equationproductsecond. (((q) = ((ge_representation_real_code_zero_remainder_equationproductsecond) + (ge_representation_imaginary_code_zero_remainder_equationproductsecond)) * S ((ge_representation_real_code_zero_remainder_equationproductsecond) + (ge_representation_imaginary_code_zero_remainder_equationproductsecond)) + ((ge_representation_imaginary_code_zero_remainder_equationproductsecond) + (ge_representation_imaginary_code_zero_remainder_equationproductsecond))) /\ ((exists ge_balance_positive_zero_remainder_equationproductsecondreal ge_balance_negative_zero_remainder_equationproductsecondreal. (((((ge_representation_real_code_zero_remainder_equationproductsecond) = 2 * (ge_balance_positive_zero_remainder_equationproductsecondreal) /\ (ge_balance_negative_zero_remainder_equationproductsecondreal) = 0) \/ exists ge_signed_half_zero_remainder_equationproductsecondrealdecode. (((ge_representation_real_code_zero_remainder_equationproductsecond) = 2 * ge_signed_half_zero_remainder_equationproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductsecondreal) = 0) /\ (ge_balance_negative_zero_remainder_equationproductsecondreal) = S ge_signed_half_zero_remainder_equationproductsecondrealdecode))) /\ ((ge_second_rp_zero_remainder_equationproduct) + ge_balance_negative_zero_remainder_equationproductsecondreal = (ge_second_rn_zero_remainder_equationproduct) + ge_balance_positive_zero_remainder_equationproductsecondreal))) /\ (exists ge_balance_positive_zero_remainder_equationproductsecondimaginary ge_balance_negative_zero_remainder_equationproductsecondimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationproductsecond) = 2 * (ge_balance_positive_zero_remainder_equationproductsecondimaginary) /\ (ge_balance_negative_zero_remainder_equationproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationproductsecond) = 2 * ge_signed_half_zero_remainder_equationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationproductsecondimaginary) = S ge_signed_half_zero_remainder_equationproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_remainder_equationproduct) + ge_balance_negative_zero_remainder_equationproductsecondimaginary = (ge_second_in_zero_remainder_equationproduct) + ge_balance_positive_zero_remainder_equationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_remainder_equationproductoutput ge_representation_imaginary_code_zero_remainder_equationproductoutput. (((ge_division_product_zero_remainder_equation) = ((ge_representation_real_code_zero_remainder_equationproductoutput) + (ge_representation_imaginary_code_zero_remainder_equationproductoutput)) * S ((ge_representation_real_code_zero_remainder_equationproductoutput) + (ge_representation_imaginary_code_zero_remainder_equationproductoutput)) + ((ge_representation_imaginary_code_zero_remainder_equationproductoutput) + (ge_representation_imaginary_code_zero_remainder_equationproductoutput))) /\ ((exists ge_balance_positive_zero_remainder_equationproductoutputreal ge_balance_negative_zero_remainder_equationproductoutputreal. (((((ge_representation_real_code_zero_remainder_equationproductoutput) = 2 * (ge_balance_positive_zero_remainder_equationproductoutputreal) /\ (ge_balance_negative_zero_remainder_equationproductoutputreal) = 0) \/ exists ge_signed_half_zero_remainder_equationproductoutputrealdecode. (((ge_representation_real_code_zero_remainder_equationproductoutput) = 2 * ge_signed_half_zero_remainder_equationproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductoutputreal) = 0) /\ (ge_balance_negative_zero_remainder_equationproductoutputreal) = S ge_signed_half_zero_remainder_equationproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_remainder_equationproduct) * (ge_second_rp_zero_remainder_equationproduct))) + (((ge_first_rn_zero_remainder_equationproduct) * (ge_second_rn_zero_remainder_equationproduct))))) + (((((ge_first_ip_zero_remainder_equationproduct) * (ge_second_in_zero_remainder_equationproduct))) + (((ge_first_in_zero_remainder_equationproduct) * (ge_second_ip_zero_remainder_equationproduct))))))) + ge_balance_negative_zero_remainder_equationproductoutputreal = (((((((ge_first_rp_zero_remainder_equationproduct) * (ge_second_rn_zero_remainder_equationproduct))) + (((ge_first_rn_zero_remainder_equationproduct) * (ge_second_rp_zero_remainder_equationproduct))))) + (((((ge_first_ip_zero_remainder_equationproduct) * (ge_second_ip_zero_remainder_equationproduct))) + (((ge_first_in_zero_remainder_equationproduct) * (ge_second_in_zero_remainder_equationproduct))))))) + ge_balance_positive_zero_remainder_equationproductoutputreal))) /\ (exists ge_balance_positive_zero_remainder_equationproductoutputimaginary ge_balance_negative_zero_remainder_equationproductoutputimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationproductoutput) = 2 * (ge_balance_positive_zero_remainder_equationproductoutputimaginary) /\ (ge_balance_negative_zero_remainder_equationproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationproductoutput) = 2 * ge_signed_half_zero_remainder_equationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationproductoutputimaginary) = S ge_signed_half_zero_remainder_equationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_remainder_equationproduct) * (ge_second_ip_zero_remainder_equationproduct))) + (((ge_first_rn_zero_remainder_equationproduct) * (ge_second_in_zero_remainder_equationproduct))))) + (((((ge_first_ip_zero_remainder_equationproduct) * (ge_second_rp_zero_remainder_equationproduct))) + (((ge_first_in_zero_remainder_equationproduct) * (ge_second_rn_zero_remainder_equationproduct))))))) + ge_balance_negative_zero_remainder_equationproductoutputimaginary = (((((((ge_first_rp_zero_remainder_equationproduct) * (ge_second_in_zero_remainder_equationproduct))) + (((ge_first_rn_zero_remainder_equationproduct) * (ge_second_ip_zero_remainder_equationproduct))))) + (((((ge_first_ip_zero_remainder_equationproduct) * (ge_second_rn_zero_remainder_equationproduct))) + (((ge_first_in_zero_remainder_equationproduct) * (ge_second_rp_zero_remainder_equationproduct))))))) + ge_balance_positive_zero_remainder_equationproductoutputimaginary))))))))) /\ (exists ge_first_rp_zero_remainder_equationsum ge_first_rn_zero_remainder_equationsum ge_first_ip_zero_remainder_equationsum ge_first_in_zero_remainder_equationsum ge_second_rp_zero_remainder_equationsum ge_second_rn_zero_remainder_equationsum ge_second_ip_zero_remainder_equationsum ge_second_in_zero_remainder_equationsum. ((exists ge_representation_real_code_zero_remainder_equationsumfirst ge_representation_imaginary_code_zero_remainder_equationsumfirst. (((ge_division_product_zero_remainder_equation) = ((ge_representation_real_code_zero_remainder_equationsumfirst) + (ge_representation_imaginary_code_zero_remainder_equationsumfirst)) * S ((ge_representation_real_code_zero_remainder_equationsumfirst) + (ge_representation_imaginary_code_zero_remainder_equationsumfirst)) + ((ge_representation_imaginary_code_zero_remainder_equationsumfirst) + (ge_representation_imaginary_code_zero_remainder_equationsumfirst))) /\ ((exists ge_balance_positive_zero_remainder_equationsumfirstreal ge_balance_negative_zero_remainder_equationsumfirstreal. (((((ge_representation_real_code_zero_remainder_equationsumfirst) = 2 * (ge_balance_positive_zero_remainder_equationsumfirstreal) /\ (ge_balance_negative_zero_remainder_equationsumfirstreal) = 0) \/ exists ge_signed_half_zero_remainder_equationsumfirstrealdecode. (((ge_representation_real_code_zero_remainder_equationsumfirst) = 2 * ge_signed_half_zero_remainder_equationsumfirstrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumfirstreal) = 0) /\ (ge_balance_negative_zero_remainder_equationsumfirstreal) = S ge_signed_half_zero_remainder_equationsumfirstrealdecode))) /\ ((ge_first_rp_zero_remainder_equationsum) + ge_balance_negative_zero_remainder_equationsumfirstreal = (ge_first_rn_zero_remainder_equationsum) + ge_balance_positive_zero_remainder_equationsumfirstreal))) /\ (exists ge_balance_positive_zero_remainder_equationsumfirstimaginary ge_balance_negative_zero_remainder_equationsumfirstimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationsumfirst) = 2 * (ge_balance_positive_zero_remainder_equationsumfirstimaginary) /\ (ge_balance_negative_zero_remainder_equationsumfirstimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationsumfirstimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationsumfirst) = 2 * ge_signed_half_zero_remainder_equationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumfirstimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationsumfirstimaginary) = S ge_signed_half_zero_remainder_equationsumfirstimaginarydecode))) /\ ((ge_first_ip_zero_remainder_equationsum) + ge_balance_negative_zero_remainder_equationsumfirstimaginary = (ge_first_in_zero_remainder_equationsum) + ge_balance_positive_zero_remainder_equationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_remainder_equationsumsecond ge_representation_imaginary_code_zero_remainder_equationsumsecond. (((r) = ((ge_representation_real_code_zero_remainder_equationsumsecond) + (ge_representation_imaginary_code_zero_remainder_equationsumsecond)) * S ((ge_representation_real_code_zero_remainder_equationsumsecond) + (ge_representation_imaginary_code_zero_remainder_equationsumsecond)) + ((ge_representation_imaginary_code_zero_remainder_equationsumsecond) + (ge_representation_imaginary_code_zero_remainder_equationsumsecond))) /\ ((exists ge_balance_positive_zero_remainder_equationsumsecondreal ge_balance_negative_zero_remainder_equationsumsecondreal. (((((ge_representation_real_code_zero_remainder_equationsumsecond) = 2 * (ge_balance_positive_zero_remainder_equationsumsecondreal) /\ (ge_balance_negative_zero_remainder_equationsumsecondreal) = 0) \/ exists ge_signed_half_zero_remainder_equationsumsecondrealdecode. (((ge_representation_real_code_zero_remainder_equationsumsecond) = 2 * ge_signed_half_zero_remainder_equationsumsecondrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumsecondreal) = 0) /\ (ge_balance_negative_zero_remainder_equationsumsecondreal) = S ge_signed_half_zero_remainder_equationsumsecondrealdecode))) /\ ((ge_second_rp_zero_remainder_equationsum) + ge_balance_negative_zero_remainder_equationsumsecondreal = (ge_second_rn_zero_remainder_equationsum) + ge_balance_positive_zero_remainder_equationsumsecondreal))) /\ (exists ge_balance_positive_zero_remainder_equationsumsecondimaginary ge_balance_negative_zero_remainder_equationsumsecondimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationsumsecond) = 2 * (ge_balance_positive_zero_remainder_equationsumsecondimaginary) /\ (ge_balance_negative_zero_remainder_equationsumsecondimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationsumsecondimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationsumsecond) = 2 * ge_signed_half_zero_remainder_equationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumsecondimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationsumsecondimaginary) = S ge_signed_half_zero_remainder_equationsumsecondimaginarydecode))) /\ ((ge_second_ip_zero_remainder_equationsum) + ge_balance_negative_zero_remainder_equationsumsecondimaginary = (ge_second_in_zero_remainder_equationsum) + ge_balance_positive_zero_remainder_equationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_remainder_equationsumoutput ge_representation_imaginary_code_zero_remainder_equationsumoutput. (((a) = ((ge_representation_real_code_zero_remainder_equationsumoutput) + (ge_representation_imaginary_code_zero_remainder_equationsumoutput)) * S ((ge_representation_real_code_zero_remainder_equationsumoutput) + (ge_representation_imaginary_code_zero_remainder_equationsumoutput)) + ((ge_representation_imaginary_code_zero_remainder_equationsumoutput) + (ge_representation_imaginary_code_zero_remainder_equationsumoutput))) /\ ((exists ge_balance_positive_zero_remainder_equationsumoutputreal ge_balance_negative_zero_remainder_equationsumoutputreal. (((((ge_representation_real_code_zero_remainder_equationsumoutput) = 2 * (ge_balance_positive_zero_remainder_equationsumoutputreal) /\ (ge_balance_negative_zero_remainder_equationsumoutputreal) = 0) \/ exists ge_signed_half_zero_remainder_equationsumoutputrealdecode. (((ge_representation_real_code_zero_remainder_equationsumoutput) = 2 * ge_signed_half_zero_remainder_equationsumoutputrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumoutputreal) = 0) /\ (ge_balance_negative_zero_remainder_equationsumoutputreal) = S ge_signed_half_zero_remainder_equationsumoutputrealdecode))) /\ ((((ge_first_rp_zero_remainder_equationsum) + (ge_second_rp_zero_remainder_equationsum))) + ge_balance_negative_zero_remainder_equationsumoutputreal = (((ge_first_rn_zero_remainder_equationsum) + (ge_second_rn_zero_remainder_equationsum))) + ge_balance_positive_zero_remainder_equationsumoutputreal))) /\ (exists ge_balance_positive_zero_remainder_equationsumoutputimaginary ge_balance_negative_zero_remainder_equationsumoutputimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationsumoutput) = 2 * (ge_balance_positive_zero_remainder_equationsumoutputimaginary) /\ (ge_balance_negative_zero_remainder_equationsumoutputimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationsumoutputimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationsumoutput) = 2 * ge_signed_half_zero_remainder_equationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumoutputimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationsumoutputimaginary) = S ge_signed_half_zero_remainder_equationsumoutputimaginarydecode))) /\ ((((ge_first_ip_zero_remainder_equationsum) + (ge_second_ip_zero_remainder_equationsum))) + ge_balance_negative_zero_remainder_equationsumoutputimaginary = (((ge_first_in_zero_remainder_equationsum) + (ge_second_in_zero_remainder_equationsum))) + ge_balance_positive_zero_remainder_equationsumoutputimaginary))))))))))) -> r=0 -> (exists gr_quotient_zero_remainder_divides. (exists ge_first_rp_zero_remainder_dividesproduct ge_first_rn_zero_remainder_dividesproduct ge_first_ip_zero_remainder_dividesproduct ge_first_in_zero_remainder_dividesproduct ge_second_rp_zero_remainder_dividesproduct ge_second_rn_zero_remainder_dividesproduct ge_second_ip_zero_remainder_dividesproduct ge_second_in_zero_remainder_dividesproduct. ((exists ge_representation_real_code_zero_remainder_dividesproductfirst ge_representation_imaginary_code_zero_remainder_dividesproductfirst. (((b) = ((ge_representation_real_code_zero_remainder_dividesproductfirst) + (ge_representation_imaginary_code_zero_remainder_dividesproductfirst)) * S ((ge_representation_real_code_zero_remainder_dividesproductfirst) + (ge_representation_imaginary_code_zero_remainder_dividesproductfirst)) + ((ge_representation_imaginary_code_zero_remainder_dividesproductfirst) + (ge_representation_imaginary_code_zero_remainder_dividesproductfirst))) /\ ((exists ge_balance_positive_zero_remainder_dividesproductfirstreal ge_balance_negative_zero_remainder_dividesproductfirstreal. (((((ge_representation_real_code_zero_remainder_dividesproductfirst) = 2 * (ge_balance_positive_zero_remainder_dividesproductfirstreal) /\ (ge_balance_negative_zero_remainder_dividesproductfirstreal) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductfirstrealdecode. (((ge_representation_real_code_zero_remainder_dividesproductfirst) = 2 * ge_signed_half_zero_remainder_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductfirstreal) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductfirstreal) = S ge_signed_half_zero_remainder_dividesproductfirstrealdecode))) /\ ((ge_first_rp_zero_remainder_dividesproduct) + ge_balance_negative_zero_remainder_dividesproductfirstreal = (ge_first_rn_zero_remainder_dividesproduct) + ge_balance_positive_zero_remainder_dividesproductfirstreal))) /\ (exists ge_balance_positive_zero_remainder_dividesproductfirstimaginary ge_balance_negative_zero_remainder_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_zero_remainder_dividesproductfirst) = 2 * (ge_balance_positive_zero_remainder_dividesproductfirstimaginary) /\ (ge_balance_negative_zero_remainder_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_dividesproductfirst) = 2 * ge_signed_half_zero_remainder_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductfirstimaginary) = S ge_signed_half_zero_remainder_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_remainder_dividesproduct) + ge_balance_negative_zero_remainder_dividesproductfirstimaginary = (ge_first_in_zero_remainder_dividesproduct) + ge_balance_positive_zero_remainder_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_remainder_dividesproductsecond ge_representation_imaginary_code_zero_remainder_dividesproductsecond. (((gr_quotient_zero_remainder_divides) = ((ge_representation_real_code_zero_remainder_dividesproductsecond) + (ge_representation_imaginary_code_zero_remainder_dividesproductsecond)) * S ((ge_representation_real_code_zero_remainder_dividesproductsecond) + (ge_representation_imaginary_code_zero_remainder_dividesproductsecond)) + ((ge_representation_imaginary_code_zero_remainder_dividesproductsecond) + (ge_representation_imaginary_code_zero_remainder_dividesproductsecond))) /\ ((exists ge_balance_positive_zero_remainder_dividesproductsecondreal ge_balance_negative_zero_remainder_dividesproductsecondreal. (((((ge_representation_real_code_zero_remainder_dividesproductsecond) = 2 * (ge_balance_positive_zero_remainder_dividesproductsecondreal) /\ (ge_balance_negative_zero_remainder_dividesproductsecondreal) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductsecondrealdecode. (((ge_representation_real_code_zero_remainder_dividesproductsecond) = 2 * ge_signed_half_zero_remainder_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductsecondreal) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductsecondreal) = S ge_signed_half_zero_remainder_dividesproductsecondrealdecode))) /\ ((ge_second_rp_zero_remainder_dividesproduct) + ge_balance_negative_zero_remainder_dividesproductsecondreal = (ge_second_rn_zero_remainder_dividesproduct) + ge_balance_positive_zero_remainder_dividesproductsecondreal))) /\ (exists ge_balance_positive_zero_remainder_dividesproductsecondimaginary ge_balance_negative_zero_remainder_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_zero_remainder_dividesproductsecond) = 2 * (ge_balance_positive_zero_remainder_dividesproductsecondimaginary) /\ (ge_balance_negative_zero_remainder_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_dividesproductsecond) = 2 * ge_signed_half_zero_remainder_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductsecondimaginary) = S ge_signed_half_zero_remainder_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_remainder_dividesproduct) + ge_balance_negative_zero_remainder_dividesproductsecondimaginary = (ge_second_in_zero_remainder_dividesproduct) + ge_balance_positive_zero_remainder_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_remainder_dividesproductoutput ge_representation_imaginary_code_zero_remainder_dividesproductoutput. (((a) = ((ge_representation_real_code_zero_remainder_dividesproductoutput) + (ge_representation_imaginary_code_zero_remainder_dividesproductoutput)) * S ((ge_representation_real_code_zero_remainder_dividesproductoutput) + (ge_representation_imaginary_code_zero_remainder_dividesproductoutput)) + ((ge_representation_imaginary_code_zero_remainder_dividesproductoutput) + (ge_representation_imaginary_code_zero_remainder_dividesproductoutput))) /\ ((exists ge_balance_positive_zero_remainder_dividesproductoutputreal ge_balance_negative_zero_remainder_dividesproductoutputreal. (((((ge_representation_real_code_zero_remainder_dividesproductoutput) = 2 * (ge_balance_positive_zero_remainder_dividesproductoutputreal) /\ (ge_balance_negative_zero_remainder_dividesproductoutputreal) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductoutputrealdecode. (((ge_representation_real_code_zero_remainder_dividesproductoutput) = 2 * ge_signed_half_zero_remainder_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductoutputreal) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductoutputreal) = S ge_signed_half_zero_remainder_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_remainder_dividesproduct) * (ge_second_rp_zero_remainder_dividesproduct))) + (((ge_first_rn_zero_remainder_dividesproduct) * (ge_second_rn_zero_remainder_dividesproduct))))) + (((((ge_first_ip_zero_remainder_dividesproduct) * (ge_second_in_zero_remainder_dividesproduct))) + (((ge_first_in_zero_remainder_dividesproduct) * (ge_second_ip_zero_remainder_dividesproduct))))))) + ge_balance_negative_zero_remainder_dividesproductoutputreal = (((((((ge_first_rp_zero_remainder_dividesproduct) * (ge_second_rn_zero_remainder_dividesproduct))) + (((ge_first_rn_zero_remainder_dividesproduct) * (ge_second_rp_zero_remainder_dividesproduct))))) + (((((ge_first_ip_zero_remainder_dividesproduct) * (ge_second_ip_zero_remainder_dividesproduct))) + (((ge_first_in_zero_remainder_dividesproduct) * (ge_second_in_zero_remainder_dividesproduct))))))) + ge_balance_positive_zero_remainder_dividesproductoutputreal))) /\ (exists ge_balance_positive_zero_remainder_dividesproductoutputimaginary ge_balance_negative_zero_remainder_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_zero_remainder_dividesproductoutput) = 2 * (ge_balance_positive_zero_remainder_dividesproductoutputimaginary) /\ (ge_balance_negative_zero_remainder_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_dividesproductoutput) = 2 * ge_signed_half_zero_remainder_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductoutputimaginary) = S ge_signed_half_zero_remainder_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_remainder_dividesproduct) * (ge_second_ip_zero_remainder_dividesproduct))) + (((ge_first_rn_zero_remainder_dividesproduct) * (ge_second_in_zero_remainder_dividesproduct))))) + (((((ge_first_ip_zero_remainder_dividesproduct) * (ge_second_rp_zero_remainder_dividesproduct))) + (((ge_first_in_zero_remainder_dividesproduct) * (ge_second_rn_zero_remainder_dividesproduct))))))) + ge_balance_negative_zero_remainder_dividesproductoutputimaginary = (((((((ge_first_rp_zero_remainder_dividesproduct) * (ge_second_in_zero_remainder_dividesproduct))) + (((ge_first_rn_zero_remainder_dividesproduct) * (ge_second_ip_zero_remainder_dividesproduct))))) + (((((ge_first_ip_zero_remainder_dividesproduct) * (ge_second_rn_zero_remainder_dividesproduct))) + (((ge_first_in_zero_remainder_dividesproduct) * (ge_second_rp_zero_remainder_dividesproduct))))))) + ge_balance_positive_zero_remainder_dividesproductoutputimaginary))))))))))