gaussian_divides_product_left

Exact expanded first-order arithmetic statement

forall d a b c. (exists gr_quotient_product_divisor. (exists ge_first_rp_product_divisorproduct ge_first_rn_product_divisorproduct ge_first_ip_product_divisorproduct ge_first_in_product_divisorproduct ge_second_rp_product_divisorproduct ge_second_rn_product_divisorproduct ge_second_ip_product_divisorproduct ge_second_in_product_divisorproduct. ((exists ge_representation_real_code_product_divisorproductfirst ge_representation_imaginary_code_product_divisorproductfirst. (((d) = ((ge_representation_real_code_product_divisorproductfirst) + (ge_representation_imaginary_code_product_divisorproductfirst)) * S ((ge_representation_real_code_product_divisorproductfirst) + (ge_representation_imaginary_code_product_divisorproductfirst)) + ((ge_representation_imaginary_code_product_divisorproductfirst) + (ge_representation_imaginary_code_product_divisorproductfirst))) /\ ((exists ge_balance_positive_product_divisorproductfirstreal ge_balance_negative_product_divisorproductfirstreal. (((((ge_representation_real_code_product_divisorproductfirst) = 2 * (ge_balance_positive_product_divisorproductfirstreal) /\ (ge_balance_negative_product_divisorproductfirstreal) = 0) \/ exists ge_signed_half_product_divisorproductfirstrealdecode. (((ge_representation_real_code_product_divisorproductfirst) = 2 * ge_signed_half_product_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_product_divisorproductfirstreal) = 0) /\ (ge_balance_negative_product_divisorproductfirstreal) = S ge_signed_half_product_divisorproductfirstrealdecode))) /\ ((ge_first_rp_product_divisorproduct) + ge_balance_negative_product_divisorproductfirstreal = (ge_first_rn_product_divisorproduct) + ge_balance_positive_product_divisorproductfirstreal))) /\ (exists ge_balance_positive_product_divisorproductfirstimaginary ge_balance_negative_product_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_product_divisorproductfirst) = 2 * (ge_balance_positive_product_divisorproductfirstimaginary) /\ (ge_balance_negative_product_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_product_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_product_divisorproductfirst) = 2 * ge_signed_half_product_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_product_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_product_divisorproductfirstimaginary) = S ge_signed_half_product_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_product_divisorproduct) + ge_balance_negative_product_divisorproductfirstimaginary = (ge_first_in_product_divisorproduct) + ge_balance_positive_product_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_divisorproductsecond ge_representation_imaginary_code_product_divisorproductsecond. (((gr_quotient_product_divisor) = ((ge_representation_real_code_product_divisorproductsecond) + (ge_representation_imaginary_code_product_divisorproductsecond)) * S ((ge_representation_real_code_product_divisorproductsecond) + (ge_representation_imaginary_code_product_divisorproductsecond)) + ((ge_representation_imaginary_code_product_divisorproductsecond) + (ge_representation_imaginary_code_product_divisorproductsecond))) /\ ((exists ge_balance_positive_product_divisorproductsecondreal ge_balance_negative_product_divisorproductsecondreal. (((((ge_representation_real_code_product_divisorproductsecond) = 2 * (ge_balance_positive_product_divisorproductsecondreal) /\ (ge_balance_negative_product_divisorproductsecondreal) = 0) \/ exists ge_signed_half_product_divisorproductsecondrealdecode. (((ge_representation_real_code_product_divisorproductsecond) = 2 * ge_signed_half_product_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_product_divisorproductsecondreal) = 0) /\ (ge_balance_negative_product_divisorproductsecondreal) = S ge_signed_half_product_divisorproductsecondrealdecode))) /\ ((ge_second_rp_product_divisorproduct) + ge_balance_negative_product_divisorproductsecondreal = (ge_second_rn_product_divisorproduct) + ge_balance_positive_product_divisorproductsecondreal))) /\ (exists ge_balance_positive_product_divisorproductsecondimaginary ge_balance_negative_product_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_product_divisorproductsecond) = 2 * (ge_balance_positive_product_divisorproductsecondimaginary) /\ (ge_balance_negative_product_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_product_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_product_divisorproductsecond) = 2 * ge_signed_half_product_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_product_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_product_divisorproductsecondimaginary) = S ge_signed_half_product_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_product_divisorproduct) + ge_balance_negative_product_divisorproductsecondimaginary = (ge_second_in_product_divisorproduct) + ge_balance_positive_product_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_product_divisorproductoutput ge_representation_imaginary_code_product_divisorproductoutput. (((a) = ((ge_representation_real_code_product_divisorproductoutput) + (ge_representation_imaginary_code_product_divisorproductoutput)) * S ((ge_representation_real_code_product_divisorproductoutput) + (ge_representation_imaginary_code_product_divisorproductoutput)) + ((ge_representation_imaginary_code_product_divisorproductoutput) + (ge_representation_imaginary_code_product_divisorproductoutput))) /\ ((exists ge_balance_positive_product_divisorproductoutputreal ge_balance_negative_product_divisorproductoutputreal. (((((ge_representation_real_code_product_divisorproductoutput) = 2 * (ge_balance_positive_product_divisorproductoutputreal) /\ (ge_balance_negative_product_divisorproductoutputreal) = 0) \/ exists ge_signed_half_product_divisorproductoutputrealdecode. (((ge_representation_real_code_product_divisorproductoutput) = 2 * ge_signed_half_product_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_product_divisorproductoutputreal) = 0) /\ (ge_balance_negative_product_divisorproductoutputreal) = S ge_signed_half_product_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_product_divisorproduct) * (ge_second_rp_product_divisorproduct))) + (((ge_first_rn_product_divisorproduct) * (ge_second_rn_product_divisorproduct))))) + (((((ge_first_ip_product_divisorproduct) * (ge_second_in_product_divisorproduct))) + (((ge_first_in_product_divisorproduct) * (ge_second_ip_product_divisorproduct))))))) + ge_balance_negative_product_divisorproductoutputreal = (((((((ge_first_rp_product_divisorproduct) * (ge_second_rn_product_divisorproduct))) + (((ge_first_rn_product_divisorproduct) * (ge_second_rp_product_divisorproduct))))) + (((((ge_first_ip_product_divisorproduct) * (ge_second_ip_product_divisorproduct))) + (((ge_first_in_product_divisorproduct) * (ge_second_in_product_divisorproduct))))))) + ge_balance_positive_product_divisorproductoutputreal))) /\ (exists ge_balance_positive_product_divisorproductoutputimaginary ge_balance_negative_product_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_product_divisorproductoutput) = 2 * (ge_balance_positive_product_divisorproductoutputimaginary) /\ (ge_balance_negative_product_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_product_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_product_divisorproductoutput) = 2 * ge_signed_half_product_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_product_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_product_divisorproductoutputimaginary) = S ge_signed_half_product_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_divisorproduct) * (ge_second_ip_product_divisorproduct))) + (((ge_first_rn_product_divisorproduct) * (ge_second_in_product_divisorproduct))))) + (((((ge_first_ip_product_divisorproduct) * (ge_second_rp_product_divisorproduct))) + (((ge_first_in_product_divisorproduct) * (ge_second_rn_product_divisorproduct))))))) + ge_balance_negative_product_divisorproductoutputimaginary = (((((((ge_first_rp_product_divisorproduct) * (ge_second_in_product_divisorproduct))) + (((ge_first_rn_product_divisorproduct) * (ge_second_ip_product_divisorproduct))))) + (((((ge_first_ip_product_divisorproduct) * (ge_second_rn_product_divisorproduct))) + (((ge_first_in_product_divisorproduct) * (ge_second_rp_product_divisorproduct))))))) + ge_balance_positive_product_divisorproductoutputimaginary)))))))))) -> (exists ge_first_rp_product_multiple ge_first_rn_product_multiple ge_first_ip_product_multiple ge_first_in_product_multiple ge_second_rp_product_multiple ge_second_rn_product_multiple ge_second_ip_product_multiple ge_second_in_product_multiple. ((exists ge_representation_real_code_product_multiplefirst ge_representation_imaginary_code_product_multiplefirst. (((a) = ((ge_representation_real_code_product_multiplefirst) + (ge_representation_imaginary_code_product_multiplefirst)) * S ((ge_representation_real_code_product_multiplefirst) + (ge_representation_imaginary_code_product_multiplefirst)) + ((ge_representation_imaginary_code_product_multiplefirst) + (ge_representation_imaginary_code_product_multiplefirst))) /\ ((exists ge_balance_positive_product_multiplefirstreal ge_balance_negative_product_multiplefirstreal. (((((ge_representation_real_code_product_multiplefirst) = 2 * (ge_balance_positive_product_multiplefirstreal) /\ (ge_balance_negative_product_multiplefirstreal) = 0) \/ exists ge_signed_half_product_multiplefirstrealdecode. (((ge_representation_real_code_product_multiplefirst) = 2 * ge_signed_half_product_multiplefirstrealdecode + 1 /\ (ge_balance_positive_product_multiplefirstreal) = 0) /\ (ge_balance_negative_product_multiplefirstreal) = S ge_signed_half_product_multiplefirstrealdecode))) /\ ((ge_first_rp_product_multiple) + ge_balance_negative_product_multiplefirstreal = (ge_first_rn_product_multiple) + ge_balance_positive_product_multiplefirstreal))) /\ (exists ge_balance_positive_product_multiplefirstimaginary ge_balance_negative_product_multiplefirstimaginary. (((((ge_representation_imaginary_code_product_multiplefirst) = 2 * (ge_balance_positive_product_multiplefirstimaginary) /\ (ge_balance_negative_product_multiplefirstimaginary) = 0) \/ exists ge_signed_half_product_multiplefirstimaginarydecode. (((ge_representation_imaginary_code_product_multiplefirst) = 2 * ge_signed_half_product_multiplefirstimaginarydecode + 1 /\ (ge_balance_positive_product_multiplefirstimaginary) = 0) /\ (ge_balance_negative_product_multiplefirstimaginary) = S ge_signed_half_product_multiplefirstimaginarydecode))) /\ ((ge_first_ip_product_multiple) + ge_balance_negative_product_multiplefirstimaginary = (ge_first_in_product_multiple) + ge_balance_positive_product_multiplefirstimaginary)))))) /\ ((exists ge_representation_real_code_product_multiplesecond ge_representation_imaginary_code_product_multiplesecond. (((b) = ((ge_representation_real_code_product_multiplesecond) + (ge_representation_imaginary_code_product_multiplesecond)) * S ((ge_representation_real_code_product_multiplesecond) + (ge_representation_imaginary_code_product_multiplesecond)) + ((ge_representation_imaginary_code_product_multiplesecond) + (ge_representation_imaginary_code_product_multiplesecond))) /\ ((exists ge_balance_positive_product_multiplesecondreal ge_balance_negative_product_multiplesecondreal. (((((ge_representation_real_code_product_multiplesecond) = 2 * (ge_balance_positive_product_multiplesecondreal) /\ (ge_balance_negative_product_multiplesecondreal) = 0) \/ exists ge_signed_half_product_multiplesecondrealdecode. (((ge_representation_real_code_product_multiplesecond) = 2 * ge_signed_half_product_multiplesecondrealdecode + 1 /\ (ge_balance_positive_product_multiplesecondreal) = 0) /\ (ge_balance_negative_product_multiplesecondreal) = S ge_signed_half_product_multiplesecondrealdecode))) /\ ((ge_second_rp_product_multiple) + ge_balance_negative_product_multiplesecondreal = (ge_second_rn_product_multiple) + ge_balance_positive_product_multiplesecondreal))) /\ (exists ge_balance_positive_product_multiplesecondimaginary ge_balance_negative_product_multiplesecondimaginary. (((((ge_representation_imaginary_code_product_multiplesecond) = 2 * (ge_balance_positive_product_multiplesecondimaginary) /\ (ge_balance_negative_product_multiplesecondimaginary) = 0) \/ exists ge_signed_half_product_multiplesecondimaginarydecode. (((ge_representation_imaginary_code_product_multiplesecond) = 2 * ge_signed_half_product_multiplesecondimaginarydecode + 1 /\ (ge_balance_positive_product_multiplesecondimaginary) = 0) /\ (ge_balance_negative_product_multiplesecondimaginary) = S ge_signed_half_product_multiplesecondimaginarydecode))) /\ ((ge_second_ip_product_multiple) + ge_balance_negative_product_multiplesecondimaginary = (ge_second_in_product_multiple) + ge_balance_positive_product_multiplesecondimaginary)))))) /\ (exists ge_representation_real_code_product_multipleoutput ge_representation_imaginary_code_product_multipleoutput. (((c) = ((ge_representation_real_code_product_multipleoutput) + (ge_representation_imaginary_code_product_multipleoutput)) * S ((ge_representation_real_code_product_multipleoutput) + (ge_representation_imaginary_code_product_multipleoutput)) + ((ge_representation_imaginary_code_product_multipleoutput) + (ge_representation_imaginary_code_product_multipleoutput))) /\ ((exists ge_balance_positive_product_multipleoutputreal ge_balance_negative_product_multipleoutputreal. (((((ge_representation_real_code_product_multipleoutput) = 2 * (ge_balance_positive_product_multipleoutputreal) /\ (ge_balance_negative_product_multipleoutputreal) = 0) \/ exists ge_signed_half_product_multipleoutputrealdecode. (((ge_representation_real_code_product_multipleoutput) = 2 * ge_signed_half_product_multipleoutputrealdecode + 1 /\ (ge_balance_positive_product_multipleoutputreal) = 0) /\ (ge_balance_negative_product_multipleoutputreal) = S ge_signed_half_product_multipleoutputrealdecode))) /\ ((((((((ge_first_rp_product_multiple) * (ge_second_rp_product_multiple))) + (((ge_first_rn_product_multiple) * (ge_second_rn_product_multiple))))) + (((((ge_first_ip_product_multiple) * (ge_second_in_product_multiple))) + (((ge_first_in_product_multiple) * (ge_second_ip_product_multiple))))))) + ge_balance_negative_product_multipleoutputreal = (((((((ge_first_rp_product_multiple) * (ge_second_rn_product_multiple))) + (((ge_first_rn_product_multiple) * (ge_second_rp_product_multiple))))) + (((((ge_first_ip_product_multiple) * (ge_second_ip_product_multiple))) + (((ge_first_in_product_multiple) * (ge_second_in_product_multiple))))))) + ge_balance_positive_product_multipleoutputreal))) /\ (exists ge_balance_positive_product_multipleoutputimaginary ge_balance_negative_product_multipleoutputimaginary. (((((ge_representation_imaginary_code_product_multipleoutput) = 2 * (ge_balance_positive_product_multipleoutputimaginary) /\ (ge_balance_negative_product_multipleoutputimaginary) = 0) \/ exists ge_signed_half_product_multipleoutputimaginarydecode. (((ge_representation_imaginary_code_product_multipleoutput) = 2 * ge_signed_half_product_multipleoutputimaginarydecode + 1 /\ (ge_balance_positive_product_multipleoutputimaginary) = 0) /\ (ge_balance_negative_product_multipleoutputimaginary) = S ge_signed_half_product_multipleoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_multiple) * (ge_second_ip_product_multiple))) + (((ge_first_rn_product_multiple) * (ge_second_in_product_multiple))))) + (((((ge_first_ip_product_multiple) * (ge_second_rp_product_multiple))) + (((ge_first_in_product_multiple) * (ge_second_rn_product_multiple))))))) + ge_balance_negative_product_multipleoutputimaginary = (((((((ge_first_rp_product_multiple) * (ge_second_in_product_multiple))) + (((ge_first_rn_product_multiple) * (ge_second_ip_product_multiple))))) + (((((ge_first_ip_product_multiple) * (ge_second_rn_product_multiple))) + (((ge_first_in_product_multiple) * (ge_second_rp_product_multiple))))))) + ge_balance_positive_product_multipleoutputimaginary))))))))) -> (exists gr_quotient_product_divides. (exists ge_first_rp_product_dividesproduct ge_first_rn_product_dividesproduct ge_first_ip_product_dividesproduct ge_first_in_product_dividesproduct ge_second_rp_product_dividesproduct ge_second_rn_product_dividesproduct ge_second_ip_product_dividesproduct ge_second_in_product_dividesproduct. ((exists ge_representation_real_code_product_dividesproductfirst ge_representation_imaginary_code_product_dividesproductfirst. (((d) = ((ge_representation_real_code_product_dividesproductfirst) + (ge_representation_imaginary_code_product_dividesproductfirst)) * S ((ge_representation_real_code_product_dividesproductfirst) + (ge_representation_imaginary_code_product_dividesproductfirst)) + ((ge_representation_imaginary_code_product_dividesproductfirst) + (ge_representation_imaginary_code_product_dividesproductfirst))) /\ ((exists ge_balance_positive_product_dividesproductfirstreal ge_balance_negative_product_dividesproductfirstreal. (((((ge_representation_real_code_product_dividesproductfirst) = 2 * (ge_balance_positive_product_dividesproductfirstreal) /\ (ge_balance_negative_product_dividesproductfirstreal) = 0) \/ exists ge_signed_half_product_dividesproductfirstrealdecode. (((ge_representation_real_code_product_dividesproductfirst) = 2 * ge_signed_half_product_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_product_dividesproductfirstreal) = 0) /\ (ge_balance_negative_product_dividesproductfirstreal) = S ge_signed_half_product_dividesproductfirstrealdecode))) /\ ((ge_first_rp_product_dividesproduct) + ge_balance_negative_product_dividesproductfirstreal = (ge_first_rn_product_dividesproduct) + ge_balance_positive_product_dividesproductfirstreal))) /\ (exists ge_balance_positive_product_dividesproductfirstimaginary ge_balance_negative_product_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_product_dividesproductfirst) = 2 * (ge_balance_positive_product_dividesproductfirstimaginary) /\ (ge_balance_negative_product_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_product_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_product_dividesproductfirst) = 2 * ge_signed_half_product_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_product_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_product_dividesproductfirstimaginary) = S ge_signed_half_product_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_product_dividesproduct) + ge_balance_negative_product_dividesproductfirstimaginary = (ge_first_in_product_dividesproduct) + ge_balance_positive_product_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_product_dividesproductsecond ge_representation_imaginary_code_product_dividesproductsecond. (((gr_quotient_product_divides) = ((ge_representation_real_code_product_dividesproductsecond) + (ge_representation_imaginary_code_product_dividesproductsecond)) * S ((ge_representation_real_code_product_dividesproductsecond) + (ge_representation_imaginary_code_product_dividesproductsecond)) + ((ge_representation_imaginary_code_product_dividesproductsecond) + (ge_representation_imaginary_code_product_dividesproductsecond))) /\ ((exists ge_balance_positive_product_dividesproductsecondreal ge_balance_negative_product_dividesproductsecondreal. (((((ge_representation_real_code_product_dividesproductsecond) = 2 * (ge_balance_positive_product_dividesproductsecondreal) /\ (ge_balance_negative_product_dividesproductsecondreal) = 0) \/ exists ge_signed_half_product_dividesproductsecondrealdecode. (((ge_representation_real_code_product_dividesproductsecond) = 2 * ge_signed_half_product_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_product_dividesproductsecondreal) = 0) /\ (ge_balance_negative_product_dividesproductsecondreal) = S ge_signed_half_product_dividesproductsecondrealdecode))) /\ ((ge_second_rp_product_dividesproduct) + ge_balance_negative_product_dividesproductsecondreal = (ge_second_rn_product_dividesproduct) + ge_balance_positive_product_dividesproductsecondreal))) /\ (exists ge_balance_positive_product_dividesproductsecondimaginary ge_balance_negative_product_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_product_dividesproductsecond) = 2 * (ge_balance_positive_product_dividesproductsecondimaginary) /\ (ge_balance_negative_product_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_product_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_product_dividesproductsecond) = 2 * ge_signed_half_product_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_product_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_product_dividesproductsecondimaginary) = S ge_signed_half_product_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_product_dividesproduct) + ge_balance_negative_product_dividesproductsecondimaginary = (ge_second_in_product_dividesproduct) + ge_balance_positive_product_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_product_dividesproductoutput ge_representation_imaginary_code_product_dividesproductoutput. (((c) = ((ge_representation_real_code_product_dividesproductoutput) + (ge_representation_imaginary_code_product_dividesproductoutput)) * S ((ge_representation_real_code_product_dividesproductoutput) + (ge_representation_imaginary_code_product_dividesproductoutput)) + ((ge_representation_imaginary_code_product_dividesproductoutput) + (ge_representation_imaginary_code_product_dividesproductoutput))) /\ ((exists ge_balance_positive_product_dividesproductoutputreal ge_balance_negative_product_dividesproductoutputreal. (((((ge_representation_real_code_product_dividesproductoutput) = 2 * (ge_balance_positive_product_dividesproductoutputreal) /\ (ge_balance_negative_product_dividesproductoutputreal) = 0) \/ exists ge_signed_half_product_dividesproductoutputrealdecode. (((ge_representation_real_code_product_dividesproductoutput) = 2 * ge_signed_half_product_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_product_dividesproductoutputreal) = 0) /\ (ge_balance_negative_product_dividesproductoutputreal) = S ge_signed_half_product_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_product_dividesproduct) * (ge_second_rp_product_dividesproduct))) + (((ge_first_rn_product_dividesproduct) * (ge_second_rn_product_dividesproduct))))) + (((((ge_first_ip_product_dividesproduct) * (ge_second_in_product_dividesproduct))) + (((ge_first_in_product_dividesproduct) * (ge_second_ip_product_dividesproduct))))))) + ge_balance_negative_product_dividesproductoutputreal = (((((((ge_first_rp_product_dividesproduct) * (ge_second_rn_product_dividesproduct))) + (((ge_first_rn_product_dividesproduct) * (ge_second_rp_product_dividesproduct))))) + (((((ge_first_ip_product_dividesproduct) * (ge_second_ip_product_dividesproduct))) + (((ge_first_in_product_dividesproduct) * (ge_second_in_product_dividesproduct))))))) + ge_balance_positive_product_dividesproductoutputreal))) /\ (exists ge_balance_positive_product_dividesproductoutputimaginary ge_balance_negative_product_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_product_dividesproductoutput) = 2 * (ge_balance_positive_product_dividesproductoutputimaginary) /\ (ge_balance_negative_product_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_product_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_product_dividesproductoutput) = 2 * ge_signed_half_product_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_product_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_product_dividesproductoutputimaginary) = S ge_signed_half_product_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_product_dividesproduct) * (ge_second_ip_product_dividesproduct))) + (((ge_first_rn_product_dividesproduct) * (ge_second_in_product_dividesproduct))))) + (((((ge_first_ip_product_dividesproduct) * (ge_second_rp_product_dividesproduct))) + (((ge_first_in_product_dividesproduct) * (ge_second_rn_product_dividesproduct))))))) + ge_balance_negative_product_dividesproductoutputimaginary = (((((((ge_first_rp_product_dividesproduct) * (ge_second_in_product_dividesproduct))) + (((ge_first_rn_product_dividesproduct) * (ge_second_ip_product_dividesproduct))))) + (((((ge_first_ip_product_dividesproduct) * (ge_second_rn_product_dividesproduct))) + (((ge_first_in_product_dividesproduct) * (ge_second_rp_product_dividesproduct))))))) + ge_balance_positive_product_dividesproductoutputimaginary))))))))))