gaussian_divides_product_right

Exact expanded first-order arithmetic statement

forall d a b c. (exists gr_quotient_product_right_divisor. (exists ge_first_rp_product_right_divisorproduct ge_first_rn_product_right_divisorproduct ge_first_ip_product_right_divisorproduct ge_first_in_product_right_divisorproduct ge_second_rp_product_right_divisorproduct ge_second_rn_product_right_divisorproduct ge_second_ip_product_right_divisorproduct ge_second_in_product_right_divisorproduct. ((exists ge_representation_real_code_product_right_divisorproductfirst ge_representation_imaginary_code_product_right_divisorproductfirst. (((d) = ((ge_representation_real_code_product_right_divisorproductfirst) + (ge_representation_imaginary_code_product_right_divisorproductfirst)) * S ((ge_representation_real_code_product_right_divisorproductfirst) + (ge_representation_imaginary_code_product_right_divisorproductfirst)) + ((ge_representation_imaginary_code_product_right_divisorproductfirst) + (ge_representation_imaginary_code_product_right_divisorproductfirst))) /\ ((exists ge_balance_positive_product_right_divisorproductfirstreal ge_balance_negative_product_right_divisorproductfirstreal. (((((ge_representation_real_code_product_right_divisorproductfirst) = 2 * (ge_balance_positive_product_right_divisorproductfirstreal) /\ (ge_balance_negative_product_right_divisorproductfirstreal) = 0) \/ exists ge_signed_half_product_right_divisorproductfirstrealdecode. (((ge_representation_real_code_product_right_divisorproductfirst) = 2 * ge_signed_half_product_right_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_product_right_divisorproductfirstreal) = 0) /\ (ge_balance_negative_product_right_divisorproductfirstreal) = S ge_signed_half_product_right_divisorproductfirstrealdecode))) /\ ((ge_first_rp_product_right_divisorproduct) + ge_balance_negative_product_right_divisorproductfirstreal = (ge_first_rn_product_right_divisorproduct) + ge_balance_positive_product_right_divisorproductfirstreal))) /\ (exists ge_balance_positive_product_right_divisorproductfirstimaginary ge_balance_negative_product_right_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_product_right_divisorproductfirst) = 2 * (ge_balance_positive_product_right_divisorproductfirstimaginary) /\ (ge_balance_negative_product_right_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_product_right_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_product_right_divisorproductfirst) = 2 * ge_signed_half_product_right_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_product_right_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_product_right_divisorproductfirstimaginary) = S ge_signed_half_product_right_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_product_right_divisorproduct) + ge_balance_negative_product_right_divisorproductfirstimaginary = (ge_first_in_product_right_divisorproduct) + ge_balance_positive_product_right_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_right_divisorproductsecond ge_representation_imaginary_code_product_right_divisorproductsecond. (((gr_quotient_product_right_divisor) = ((ge_representation_real_code_product_right_divisorproductsecond) + (ge_representation_imaginary_code_product_right_divisorproductsecond)) * S ((ge_representation_real_code_product_right_divisorproductsecond) + (ge_representation_imaginary_code_product_right_divisorproductsecond)) + ((ge_representation_imaginary_code_product_right_divisorproductsecond) + (ge_representation_imaginary_code_product_right_divisorproductsecond))) /\ ((exists ge_balance_positive_product_right_divisorproductsecondreal ge_balance_negative_product_right_divisorproductsecondreal. (((((ge_representation_real_code_product_right_divisorproductsecond) = 2 * (ge_balance_positive_product_right_divisorproductsecondreal) /\ (ge_balance_negative_product_right_divisorproductsecondreal) = 0) \/ exists ge_signed_half_product_right_divisorproductsecondrealdecode. (((ge_representation_real_code_product_right_divisorproductsecond) = 2 * ge_signed_half_product_right_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_product_right_divisorproductsecondreal) = 0) /\ (ge_balance_negative_product_right_divisorproductsecondreal) = S ge_signed_half_product_right_divisorproductsecondrealdecode))) /\ ((ge_second_rp_product_right_divisorproduct) + ge_balance_negative_product_right_divisorproductsecondreal = (ge_second_rn_product_right_divisorproduct) + ge_balance_positive_product_right_divisorproductsecondreal))) /\ (exists ge_balance_positive_product_right_divisorproductsecondimaginary ge_balance_negative_product_right_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_product_right_divisorproductsecond) = 2 * (ge_balance_positive_product_right_divisorproductsecondimaginary) /\ (ge_balance_negative_product_right_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_product_right_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_product_right_divisorproductsecond) = 2 * ge_signed_half_product_right_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_product_right_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_product_right_divisorproductsecondimaginary) = S ge_signed_half_product_right_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_product_right_divisorproduct) + ge_balance_negative_product_right_divisorproductsecondimaginary = (ge_second_in_product_right_divisorproduct) + ge_balance_positive_product_right_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_product_right_divisorproductoutput ge_representation_imaginary_code_product_right_divisorproductoutput. (((b) = ((ge_representation_real_code_product_right_divisorproductoutput) + (ge_representation_imaginary_code_product_right_divisorproductoutput)) * S ((ge_representation_real_code_product_right_divisorproductoutput) + (ge_representation_imaginary_code_product_right_divisorproductoutput)) + ((ge_representation_imaginary_code_product_right_divisorproductoutput) + (ge_representation_imaginary_code_product_right_divisorproductoutput))) /\ ((exists ge_balance_positive_product_right_divisorproductoutputreal ge_balance_negative_product_right_divisorproductoutputreal. (((((ge_representation_real_code_product_right_divisorproductoutput) = 2 * (ge_balance_positive_product_right_divisorproductoutputreal) /\ (ge_balance_negative_product_right_divisorproductoutputreal) = 0) \/ exists ge_signed_half_product_right_divisorproductoutputrealdecode. (((ge_representation_real_code_product_right_divisorproductoutput) = 2 * ge_signed_half_product_right_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_product_right_divisorproductoutputreal) = 0) /\ (ge_balance_negative_product_right_divisorproductoutputreal) = S ge_signed_half_product_right_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_product_right_divisorproduct) * (ge_second_rp_product_right_divisorproduct))) + (((ge_first_rn_product_right_divisorproduct) * (ge_second_rn_product_right_divisorproduct))))) + (((((ge_first_ip_product_right_divisorproduct) * (ge_second_in_product_right_divisorproduct))) + (((ge_first_in_product_right_divisorproduct) * (ge_second_ip_product_right_divisorproduct))))))) + ge_balance_negative_product_right_divisorproductoutputreal = (((((((ge_first_rp_product_right_divisorproduct) * (ge_second_rn_product_right_divisorproduct))) + (((ge_first_rn_product_right_divisorproduct) * (ge_second_rp_product_right_divisorproduct))))) + (((((ge_first_ip_product_right_divisorproduct) * (ge_second_ip_product_right_divisorproduct))) + (((ge_first_in_product_right_divisorproduct) * (ge_second_in_product_right_divisorproduct))))))) + ge_balance_positive_product_right_divisorproductoutputreal))) /\ (exists ge_balance_positive_product_right_divisorproductoutputimaginary ge_balance_negative_product_right_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_product_right_divisorproductoutput) = 2 * (ge_balance_positive_product_right_divisorproductoutputimaginary) /\ (ge_balance_negative_product_right_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_product_right_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_product_right_divisorproductoutput) = 2 * ge_signed_half_product_right_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_product_right_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_product_right_divisorproductoutputimaginary) = S ge_signed_half_product_right_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_right_divisorproduct) * (ge_second_ip_product_right_divisorproduct))) + (((ge_first_rn_product_right_divisorproduct) * (ge_second_in_product_right_divisorproduct))))) + (((((ge_first_ip_product_right_divisorproduct) * (ge_second_rp_product_right_divisorproduct))) + (((ge_first_in_product_right_divisorproduct) * (ge_second_rn_product_right_divisorproduct))))))) + ge_balance_negative_product_right_divisorproductoutputimaginary = (((((((ge_first_rp_product_right_divisorproduct) * (ge_second_in_product_right_divisorproduct))) + (((ge_first_rn_product_right_divisorproduct) * (ge_second_ip_product_right_divisorproduct))))) + (((((ge_first_ip_product_right_divisorproduct) * (ge_second_rn_product_right_divisorproduct))) + (((ge_first_in_product_right_divisorproduct) * (ge_second_rp_product_right_divisorproduct))))))) + ge_balance_positive_product_right_divisorproductoutputimaginary)))))))))) -> (exists ge_first_rp_product_right_multiple ge_first_rn_product_right_multiple ge_first_ip_product_right_multiple ge_first_in_product_right_multiple ge_second_rp_product_right_multiple ge_second_rn_product_right_multiple ge_second_ip_product_right_multiple ge_second_in_product_right_multiple. ((exists ge_representation_real_code_product_right_multiplefirst ge_representation_imaginary_code_product_right_multiplefirst. (((a) = ((ge_representation_real_code_product_right_multiplefirst) + (ge_representation_imaginary_code_product_right_multiplefirst)) * S ((ge_representation_real_code_product_right_multiplefirst) + (ge_representation_imaginary_code_product_right_multiplefirst)) + ((ge_representation_imaginary_code_product_right_multiplefirst) + (ge_representation_imaginary_code_product_right_multiplefirst))) /\ ((exists ge_balance_positive_product_right_multiplefirstreal ge_balance_negative_product_right_multiplefirstreal. (((((ge_representation_real_code_product_right_multiplefirst) = 2 * (ge_balance_positive_product_right_multiplefirstreal) /\ (ge_balance_negative_product_right_multiplefirstreal) = 0) \/ exists ge_signed_half_product_right_multiplefirstrealdecode. (((ge_representation_real_code_product_right_multiplefirst) = 2 * ge_signed_half_product_right_multiplefirstrealdecode + 1 /\ (ge_balance_positive_product_right_multiplefirstreal) = 0) /\ (ge_balance_negative_product_right_multiplefirstreal) = S ge_signed_half_product_right_multiplefirstrealdecode))) /\ ((ge_first_rp_product_right_multiple) + ge_balance_negative_product_right_multiplefirstreal = (ge_first_rn_product_right_multiple) + ge_balance_positive_product_right_multiplefirstreal))) /\ (exists ge_balance_positive_product_right_multiplefirstimaginary ge_balance_negative_product_right_multiplefirstimaginary. (((((ge_representation_imaginary_code_product_right_multiplefirst) = 2 * (ge_balance_positive_product_right_multiplefirstimaginary) /\ (ge_balance_negative_product_right_multiplefirstimaginary) = 0) \/ exists ge_signed_half_product_right_multiplefirstimaginarydecode. (((ge_representation_imaginary_code_product_right_multiplefirst) = 2 * ge_signed_half_product_right_multiplefirstimaginarydecode + 1 /\ (ge_balance_positive_product_right_multiplefirstimaginary) = 0) /\ (ge_balance_negative_product_right_multiplefirstimaginary) = S ge_signed_half_product_right_multiplefirstimaginarydecode))) /\ ((ge_first_ip_product_right_multiple) + ge_balance_negative_product_right_multiplefirstimaginary = (ge_first_in_product_right_multiple) + ge_balance_positive_product_right_multiplefirstimaginary)))))) /\ ((exists ge_representation_real_code_product_right_multiplesecond ge_representation_imaginary_code_product_right_multiplesecond. (((b) = ((ge_representation_real_code_product_right_multiplesecond) + (ge_representation_imaginary_code_product_right_multiplesecond)) * S ((ge_representation_real_code_product_right_multiplesecond) + (ge_representation_imaginary_code_product_right_multiplesecond)) + ((ge_representation_imaginary_code_product_right_multiplesecond) + (ge_representation_imaginary_code_product_right_multiplesecond))) /\ ((exists ge_balance_positive_product_right_multiplesecondreal ge_balance_negative_product_right_multiplesecondreal. (((((ge_representation_real_code_product_right_multiplesecond) = 2 * (ge_balance_positive_product_right_multiplesecondreal) /\ (ge_balance_negative_product_right_multiplesecondreal) = 0) \/ exists ge_signed_half_product_right_multiplesecondrealdecode. (((ge_representation_real_code_product_right_multiplesecond) = 2 * ge_signed_half_product_right_multiplesecondrealdecode + 1 /\ (ge_balance_positive_product_right_multiplesecondreal) = 0) /\ (ge_balance_negative_product_right_multiplesecondreal) = S ge_signed_half_product_right_multiplesecondrealdecode))) /\ ((ge_second_rp_product_right_multiple) + ge_balance_negative_product_right_multiplesecondreal = (ge_second_rn_product_right_multiple) + ge_balance_positive_product_right_multiplesecondreal))) /\ (exists ge_balance_positive_product_right_multiplesecondimaginary ge_balance_negative_product_right_multiplesecondimaginary. (((((ge_representation_imaginary_code_product_right_multiplesecond) = 2 * (ge_balance_positive_product_right_multiplesecondimaginary) /\ (ge_balance_negative_product_right_multiplesecondimaginary) = 0) \/ exists ge_signed_half_product_right_multiplesecondimaginarydecode. (((ge_representation_imaginary_code_product_right_multiplesecond) = 2 * ge_signed_half_product_right_multiplesecondimaginarydecode + 1 /\ (ge_balance_positive_product_right_multiplesecondimaginary) = 0) /\ (ge_balance_negative_product_right_multiplesecondimaginary) = S ge_signed_half_product_right_multiplesecondimaginarydecode))) /\ ((ge_second_ip_product_right_multiple) + ge_balance_negative_product_right_multiplesecondimaginary = (ge_second_in_product_right_multiple) + ge_balance_positive_product_right_multiplesecondimaginary)))))) /\ (exists ge_representation_real_code_product_right_multipleoutput ge_representation_imaginary_code_product_right_multipleoutput. (((c) = ((ge_representation_real_code_product_right_multipleoutput) + (ge_representation_imaginary_code_product_right_multipleoutput)) * S ((ge_representation_real_code_product_right_multipleoutput) + (ge_representation_imaginary_code_product_right_multipleoutput)) + ((ge_representation_imaginary_code_product_right_multipleoutput) + (ge_representation_imaginary_code_product_right_multipleoutput))) /\ ((exists ge_balance_positive_product_right_multipleoutputreal ge_balance_negative_product_right_multipleoutputreal. (((((ge_representation_real_code_product_right_multipleoutput) = 2 * (ge_balance_positive_product_right_multipleoutputreal) /\ (ge_balance_negative_product_right_multipleoutputreal) = 0) \/ exists ge_signed_half_product_right_multipleoutputrealdecode. (((ge_representation_real_code_product_right_multipleoutput) = 2 * ge_signed_half_product_right_multipleoutputrealdecode + 1 /\ (ge_balance_positive_product_right_multipleoutputreal) = 0) /\ (ge_balance_negative_product_right_multipleoutputreal) = S ge_signed_half_product_right_multipleoutputrealdecode))) /\ ((((((((ge_first_rp_product_right_multiple) * (ge_second_rp_product_right_multiple))) + (((ge_first_rn_product_right_multiple) * (ge_second_rn_product_right_multiple))))) + (((((ge_first_ip_product_right_multiple) * (ge_second_in_product_right_multiple))) + (((ge_first_in_product_right_multiple) * (ge_second_ip_product_right_multiple))))))) + ge_balance_negative_product_right_multipleoutputreal = (((((((ge_first_rp_product_right_multiple) * (ge_second_rn_product_right_multiple))) + (((ge_first_rn_product_right_multiple) * (ge_second_rp_product_right_multiple))))) + (((((ge_first_ip_product_right_multiple) * (ge_second_ip_product_right_multiple))) + (((ge_first_in_product_right_multiple) * (ge_second_in_product_right_multiple))))))) + ge_balance_positive_product_right_multipleoutputreal))) /\ (exists ge_balance_positive_product_right_multipleoutputimaginary ge_balance_negative_product_right_multipleoutputimaginary. (((((ge_representation_imaginary_code_product_right_multipleoutput) = 2 * (ge_balance_positive_product_right_multipleoutputimaginary) /\ (ge_balance_negative_product_right_multipleoutputimaginary) = 0) \/ exists ge_signed_half_product_right_multipleoutputimaginarydecode. (((ge_representation_imaginary_code_product_right_multipleoutput) = 2 * ge_signed_half_product_right_multipleoutputimaginarydecode + 1 /\ (ge_balance_positive_product_right_multipleoutputimaginary) = 0) /\ (ge_balance_negative_product_right_multipleoutputimaginary) = S ge_signed_half_product_right_multipleoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_right_multiple) * (ge_second_ip_product_right_multiple))) + (((ge_first_rn_product_right_multiple) * (ge_second_in_product_right_multiple))))) + (((((ge_first_ip_product_right_multiple) * (ge_second_rp_product_right_multiple))) + (((ge_first_in_product_right_multiple) * (ge_second_rn_product_right_multiple))))))) + ge_balance_negative_product_right_multipleoutputimaginary = (((((((ge_first_rp_product_right_multiple) * (ge_second_in_product_right_multiple))) + (((ge_first_rn_product_right_multiple) * (ge_second_ip_product_right_multiple))))) + (((((ge_first_ip_product_right_multiple) * (ge_second_rn_product_right_multiple))) + (((ge_first_in_product_right_multiple) * (ge_second_rp_product_right_multiple))))))) + ge_balance_positive_product_right_multipleoutputimaginary))))))))) -> (exists gr_quotient_product_right_divides. (exists ge_first_rp_product_right_dividesproduct ge_first_rn_product_right_dividesproduct ge_first_ip_product_right_dividesproduct ge_first_in_product_right_dividesproduct ge_second_rp_product_right_dividesproduct ge_second_rn_product_right_dividesproduct ge_second_ip_product_right_dividesproduct ge_second_in_product_right_dividesproduct. ((exists ge_representation_real_code_product_right_dividesproductfirst ge_representation_imaginary_code_product_right_dividesproductfirst. (((d) = ((ge_representation_real_code_product_right_dividesproductfirst) + (ge_representation_imaginary_code_product_right_dividesproductfirst)) * S ((ge_representation_real_code_product_right_dividesproductfirst) + (ge_representation_imaginary_code_product_right_dividesproductfirst)) + ((ge_representation_imaginary_code_product_right_dividesproductfirst) + (ge_representation_imaginary_code_product_right_dividesproductfirst))) /\ ((exists ge_balance_positive_product_right_dividesproductfirstreal ge_balance_negative_product_right_dividesproductfirstreal. (((((ge_representation_real_code_product_right_dividesproductfirst) = 2 * (ge_balance_positive_product_right_dividesproductfirstreal) /\ (ge_balance_negative_product_right_dividesproductfirstreal) = 0) \/ exists ge_signed_half_product_right_dividesproductfirstrealdecode. (((ge_representation_real_code_product_right_dividesproductfirst) = 2 * ge_signed_half_product_right_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_product_right_dividesproductfirstreal) = 0) /\ (ge_balance_negative_product_right_dividesproductfirstreal) = S ge_signed_half_product_right_dividesproductfirstrealdecode))) /\ ((ge_first_rp_product_right_dividesproduct) + ge_balance_negative_product_right_dividesproductfirstreal = (ge_first_rn_product_right_dividesproduct) + ge_balance_positive_product_right_dividesproductfirstreal))) /\ (exists ge_balance_positive_product_right_dividesproductfirstimaginary ge_balance_negative_product_right_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_product_right_dividesproductfirst) = 2 * (ge_balance_positive_product_right_dividesproductfirstimaginary) /\ (ge_balance_negative_product_right_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_product_right_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_product_right_dividesproductfirst) = 2 * ge_signed_half_product_right_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_product_right_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_product_right_dividesproductfirstimaginary) = S ge_signed_half_product_right_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_product_right_dividesproduct) + ge_balance_negative_product_right_dividesproductfirstimaginary = (ge_first_in_product_right_dividesproduct) + ge_balance_positive_product_right_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_right_dividesproductsecond ge_representation_imaginary_code_product_right_dividesproductsecond. (((gr_quotient_product_right_divides) = ((ge_representation_real_code_product_right_dividesproductsecond) + (ge_representation_imaginary_code_product_right_dividesproductsecond)) * S ((ge_representation_real_code_product_right_dividesproductsecond) + (ge_representation_imaginary_code_product_right_dividesproductsecond)) + ((ge_representation_imaginary_code_product_right_dividesproductsecond) + (ge_representation_imaginary_code_product_right_dividesproductsecond))) /\ ((exists ge_balance_positive_product_right_dividesproductsecondreal ge_balance_negative_product_right_dividesproductsecondreal. (((((ge_representation_real_code_product_right_dividesproductsecond) = 2 * (ge_balance_positive_product_right_dividesproductsecondreal) /\ (ge_balance_negative_product_right_dividesproductsecondreal) = 0) \/ exists ge_signed_half_product_right_dividesproductsecondrealdecode. (((ge_representation_real_code_product_right_dividesproductsecond) = 2 * ge_signed_half_product_right_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_product_right_dividesproductsecondreal) = 0) /\ (ge_balance_negative_product_right_dividesproductsecondreal) = S ge_signed_half_product_right_dividesproductsecondrealdecode))) /\ ((ge_second_rp_product_right_dividesproduct) + ge_balance_negative_product_right_dividesproductsecondreal = (ge_second_rn_product_right_dividesproduct) + ge_balance_positive_product_right_dividesproductsecondreal))) /\ (exists ge_balance_positive_product_right_dividesproductsecondimaginary ge_balance_negative_product_right_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_product_right_dividesproductsecond) = 2 * (ge_balance_positive_product_right_dividesproductsecondimaginary) /\ (ge_balance_negative_product_right_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_product_right_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_product_right_dividesproductsecond) = 2 * ge_signed_half_product_right_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_product_right_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_product_right_dividesproductsecondimaginary) = S ge_signed_half_product_right_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_product_right_dividesproduct) + ge_balance_negative_product_right_dividesproductsecondimaginary = (ge_second_in_product_right_dividesproduct) + ge_balance_positive_product_right_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_product_right_dividesproductoutput ge_representation_imaginary_code_product_right_dividesproductoutput. (((c) = ((ge_representation_real_code_product_right_dividesproductoutput) + (ge_representation_imaginary_code_product_right_dividesproductoutput)) * S ((ge_representation_real_code_product_right_dividesproductoutput) + (ge_representation_imaginary_code_product_right_dividesproductoutput)) + ((ge_representation_imaginary_code_product_right_dividesproductoutput) + (ge_representation_imaginary_code_product_right_dividesproductoutput))) /\ ((exists ge_balance_positive_product_right_dividesproductoutputreal ge_balance_negative_product_right_dividesproductoutputreal. (((((ge_representation_real_code_product_right_dividesproductoutput) = 2 * (ge_balance_positive_product_right_dividesproductoutputreal) /\ (ge_balance_negative_product_right_dividesproductoutputreal) = 0) \/ exists ge_signed_half_product_right_dividesproductoutputrealdecode. (((ge_representation_real_code_product_right_dividesproductoutput) = 2 * ge_signed_half_product_right_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_product_right_dividesproductoutputreal) = 0) /\ (ge_balance_negative_product_right_dividesproductoutputreal) = S ge_signed_half_product_right_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_product_right_dividesproduct) * (ge_second_rp_product_right_dividesproduct))) + (((ge_first_rn_product_right_dividesproduct) * (ge_second_rn_product_right_dividesproduct))))) + (((((ge_first_ip_product_right_dividesproduct) * (ge_second_in_product_right_dividesproduct))) + (((ge_first_in_product_right_dividesproduct) * (ge_second_ip_product_right_dividesproduct))))))) + ge_balance_negative_product_right_dividesproductoutputreal = (((((((ge_first_rp_product_right_dividesproduct) * (ge_second_rn_product_right_dividesproduct))) + (((ge_first_rn_product_right_dividesproduct) * (ge_second_rp_product_right_dividesproduct))))) + (((((ge_first_ip_product_right_dividesproduct) * (ge_second_ip_product_right_dividesproduct))) + (((ge_first_in_product_right_dividesproduct) * (ge_second_in_product_right_dividesproduct))))))) + ge_balance_positive_product_right_dividesproductoutputreal))) /\ (exists ge_balance_positive_product_right_dividesproductoutputimaginary ge_balance_negative_product_right_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_product_right_dividesproductoutput) = 2 * (ge_balance_positive_product_right_dividesproductoutputimaginary) /\ (ge_balance_negative_product_right_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_product_right_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_product_right_dividesproductoutput) = 2 * ge_signed_half_product_right_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_product_right_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_product_right_dividesproductoutputimaginary) = S ge_signed_half_product_right_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_right_dividesproduct) * (ge_second_ip_product_right_dividesproduct))) + (((ge_first_rn_product_right_dividesproduct) * (ge_second_in_product_right_dividesproduct))))) + (((((ge_first_ip_product_right_dividesproduct) * (ge_second_rp_product_right_dividesproduct))) + (((ge_first_in_product_right_dividesproduct) * (ge_second_rn_product_right_dividesproduct))))))) + ge_balance_negative_product_right_dividesproductoutputimaginary = (((((((ge_first_rp_product_right_dividesproduct) * (ge_second_in_product_right_dividesproduct))) + (((ge_first_rn_product_right_dividesproduct) * (ge_second_ip_product_right_dividesproduct))))) + (((((ge_first_ip_product_right_dividesproduct) * (ge_second_rn_product_right_dividesproduct))) + (((ge_first_in_product_right_dividesproduct) * (ge_second_rp_product_right_dividesproduct))))))) + ge_balance_positive_product_right_dividesproductoutputimaginary))))))))))