gaussian_common_divisor_add

Exact expanded first-order arithmetic statement

forall d a b c. (exists gr_quotient_sum_first_divisor. (exists ge_first_rp_sum_first_divisorproduct ge_first_rn_sum_first_divisorproduct ge_first_ip_sum_first_divisorproduct ge_first_in_sum_first_divisorproduct ge_second_rp_sum_first_divisorproduct ge_second_rn_sum_first_divisorproduct ge_second_ip_sum_first_divisorproduct ge_second_in_sum_first_divisorproduct. ((exists ge_representation_real_code_sum_first_divisorproductfirst ge_representation_imaginary_code_sum_first_divisorproductfirst. (((d) = ((ge_representation_real_code_sum_first_divisorproductfirst) + (ge_representation_imaginary_code_sum_first_divisorproductfirst)) * S ((ge_representation_real_code_sum_first_divisorproductfirst) + (ge_representation_imaginary_code_sum_first_divisorproductfirst)) + ((ge_representation_imaginary_code_sum_first_divisorproductfirst) + (ge_representation_imaginary_code_sum_first_divisorproductfirst))) /\ ((exists ge_balance_positive_sum_first_divisorproductfirstreal ge_balance_negative_sum_first_divisorproductfirstreal. (((((ge_representation_real_code_sum_first_divisorproductfirst) = 2 * (ge_balance_positive_sum_first_divisorproductfirstreal) /\ (ge_balance_negative_sum_first_divisorproductfirstreal) = 0) \/ exists ge_signed_half_sum_first_divisorproductfirstrealdecode. (((ge_representation_real_code_sum_first_divisorproductfirst) = 2 * ge_signed_half_sum_first_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_sum_first_divisorproductfirstreal) = 0) /\ (ge_balance_negative_sum_first_divisorproductfirstreal) = S ge_signed_half_sum_first_divisorproductfirstrealdecode))) /\ ((ge_first_rp_sum_first_divisorproduct) + ge_balance_negative_sum_first_divisorproductfirstreal = (ge_first_rn_sum_first_divisorproduct) + ge_balance_positive_sum_first_divisorproductfirstreal))) /\ (exists ge_balance_positive_sum_first_divisorproductfirstimaginary ge_balance_negative_sum_first_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_sum_first_divisorproductfirst) = 2 * (ge_balance_positive_sum_first_divisorproductfirstimaginary) /\ (ge_balance_negative_sum_first_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_sum_first_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_sum_first_divisorproductfirst) = 2 * ge_signed_half_sum_first_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_sum_first_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_sum_first_divisorproductfirstimaginary) = S ge_signed_half_sum_first_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_sum_first_divisorproduct) + ge_balance_negative_sum_first_divisorproductfirstimaginary = (ge_first_in_sum_first_divisorproduct) + ge_balance_positive_sum_first_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_sum_first_divisorproductsecond ge_representation_imaginary_code_sum_first_divisorproductsecond. (((gr_quotient_sum_first_divisor) = ((ge_representation_real_code_sum_first_divisorproductsecond) + (ge_representation_imaginary_code_sum_first_divisorproductsecond)) * S ((ge_representation_real_code_sum_first_divisorproductsecond) + (ge_representation_imaginary_code_sum_first_divisorproductsecond)) + ((ge_representation_imaginary_code_sum_first_divisorproductsecond) + (ge_representation_imaginary_code_sum_first_divisorproductsecond))) /\ ((exists ge_balance_positive_sum_first_divisorproductsecondreal ge_balance_negative_sum_first_divisorproductsecondreal. (((((ge_representation_real_code_sum_first_divisorproductsecond) = 2 * (ge_balance_positive_sum_first_divisorproductsecondreal) /\ (ge_balance_negative_sum_first_divisorproductsecondreal) = 0) \/ exists ge_signed_half_sum_first_divisorproductsecondrealdecode. (((ge_representation_real_code_sum_first_divisorproductsecond) = 2 * ge_signed_half_sum_first_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_sum_first_divisorproductsecondreal) = 0) /\ (ge_balance_negative_sum_first_divisorproductsecondreal) = S ge_signed_half_sum_first_divisorproductsecondrealdecode))) /\ ((ge_second_rp_sum_first_divisorproduct) + ge_balance_negative_sum_first_divisorproductsecondreal = (ge_second_rn_sum_first_divisorproduct) + ge_balance_positive_sum_first_divisorproductsecondreal))) /\ (exists ge_balance_positive_sum_first_divisorproductsecondimaginary ge_balance_negative_sum_first_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_sum_first_divisorproductsecond) = 2 * (ge_balance_positive_sum_first_divisorproductsecondimaginary) /\ (ge_balance_negative_sum_first_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_sum_first_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_sum_first_divisorproductsecond) = 2 * ge_signed_half_sum_first_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_sum_first_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_sum_first_divisorproductsecondimaginary) = S ge_signed_half_sum_first_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_sum_first_divisorproduct) + ge_balance_negative_sum_first_divisorproductsecondimaginary = (ge_second_in_sum_first_divisorproduct) + ge_balance_positive_sum_first_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_sum_first_divisorproductoutput ge_representation_imaginary_code_sum_first_divisorproductoutput. (((a) = ((ge_representation_real_code_sum_first_divisorproductoutput) + (ge_representation_imaginary_code_sum_first_divisorproductoutput)) * S ((ge_representation_real_code_sum_first_divisorproductoutput) + (ge_representation_imaginary_code_sum_first_divisorproductoutput)) + ((ge_representation_imaginary_code_sum_first_divisorproductoutput) + (ge_representation_imaginary_code_sum_first_divisorproductoutput))) /\ ((exists ge_balance_positive_sum_first_divisorproductoutputreal ge_balance_negative_sum_first_divisorproductoutputreal. (((((ge_representation_real_code_sum_first_divisorproductoutput) = 2 * (ge_balance_positive_sum_first_divisorproductoutputreal) /\ (ge_balance_negative_sum_first_divisorproductoutputreal) = 0) \/ exists ge_signed_half_sum_first_divisorproductoutputrealdecode. (((ge_representation_real_code_sum_first_divisorproductoutput) = 2 * ge_signed_half_sum_first_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_sum_first_divisorproductoutputreal) = 0) /\ (ge_balance_negative_sum_first_divisorproductoutputreal) = S ge_signed_half_sum_first_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_sum_first_divisorproduct) * (ge_second_rp_sum_first_divisorproduct))) + (((ge_first_rn_sum_first_divisorproduct) * (ge_second_rn_sum_first_divisorproduct))))) + (((((ge_first_ip_sum_first_divisorproduct) * (ge_second_in_sum_first_divisorproduct))) + (((ge_first_in_sum_first_divisorproduct) * (ge_second_ip_sum_first_divisorproduct))))))) + ge_balance_negative_sum_first_divisorproductoutputreal = (((((((ge_first_rp_sum_first_divisorproduct) * (ge_second_rn_sum_first_divisorproduct))) + (((ge_first_rn_sum_first_divisorproduct) * (ge_second_rp_sum_first_divisorproduct))))) + (((((ge_first_ip_sum_first_divisorproduct) * (ge_second_ip_sum_first_divisorproduct))) + (((ge_first_in_sum_first_divisorproduct) * (ge_second_in_sum_first_divisorproduct))))))) + ge_balance_positive_sum_first_divisorproductoutputreal))) /\ (exists ge_balance_positive_sum_first_divisorproductoutputimaginary ge_balance_negative_sum_first_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_sum_first_divisorproductoutput) = 2 * (ge_balance_positive_sum_first_divisorproductoutputimaginary) /\ (ge_balance_negative_sum_first_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_sum_first_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_sum_first_divisorproductoutput) = 2 * ge_signed_half_sum_first_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_sum_first_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_sum_first_divisorproductoutputimaginary) = S ge_signed_half_sum_first_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_sum_first_divisorproduct) * (ge_second_ip_sum_first_divisorproduct))) + (((ge_first_rn_sum_first_divisorproduct) * (ge_second_in_sum_first_divisorproduct))))) + (((((ge_first_ip_sum_first_divisorproduct) * (ge_second_rp_sum_first_divisorproduct))) + (((ge_first_in_sum_first_divisorproduct) * (ge_second_rn_sum_first_divisorproduct))))))) + ge_balance_negative_sum_first_divisorproductoutputimaginary = (((((((ge_first_rp_sum_first_divisorproduct) * (ge_second_in_sum_first_divisorproduct))) + (((ge_first_rn_sum_first_divisorproduct) * (ge_second_ip_sum_first_divisorproduct))))) + (((((ge_first_ip_sum_first_divisorproduct) * (ge_second_rn_sum_first_divisorproduct))) + (((ge_first_in_sum_first_divisorproduct) * (ge_second_rp_sum_first_divisorproduct))))))) + ge_balance_positive_sum_first_divisorproductoutputimaginary)))))))))) -> (exists gr_quotient_sum_second_divisor. (exists ge_first_rp_sum_second_divisorproduct ge_first_rn_sum_second_divisorproduct ge_first_ip_sum_second_divisorproduct ge_first_in_sum_second_divisorproduct ge_second_rp_sum_second_divisorproduct ge_second_rn_sum_second_divisorproduct ge_second_ip_sum_second_divisorproduct ge_second_in_sum_second_divisorproduct. ((exists ge_representation_real_code_sum_second_divisorproductfirst ge_representation_imaginary_code_sum_second_divisorproductfirst. (((d) = ((ge_representation_real_code_sum_second_divisorproductfirst) + (ge_representation_imaginary_code_sum_second_divisorproductfirst)) * S ((ge_representation_real_code_sum_second_divisorproductfirst) + (ge_representation_imaginary_code_sum_second_divisorproductfirst)) + ((ge_representation_imaginary_code_sum_second_divisorproductfirst) + (ge_representation_imaginary_code_sum_second_divisorproductfirst))) /\ ((exists ge_balance_positive_sum_second_divisorproductfirstreal ge_balance_negative_sum_second_divisorproductfirstreal. (((((ge_representation_real_code_sum_second_divisorproductfirst) = 2 * (ge_balance_positive_sum_second_divisorproductfirstreal) /\ (ge_balance_negative_sum_second_divisorproductfirstreal) = 0) \/ exists ge_signed_half_sum_second_divisorproductfirstrealdecode. (((ge_representation_real_code_sum_second_divisorproductfirst) = 2 * ge_signed_half_sum_second_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_sum_second_divisorproductfirstreal) = 0) /\ (ge_balance_negative_sum_second_divisorproductfirstreal) = S ge_signed_half_sum_second_divisorproductfirstrealdecode))) /\ ((ge_first_rp_sum_second_divisorproduct) + ge_balance_negative_sum_second_divisorproductfirstreal = (ge_first_rn_sum_second_divisorproduct) + ge_balance_positive_sum_second_divisorproductfirstreal))) /\ (exists ge_balance_positive_sum_second_divisorproductfirstimaginary ge_balance_negative_sum_second_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_sum_second_divisorproductfirst) = 2 * (ge_balance_positive_sum_second_divisorproductfirstimaginary) /\ (ge_balance_negative_sum_second_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_sum_second_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_sum_second_divisorproductfirst) = 2 * ge_signed_half_sum_second_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_sum_second_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_sum_second_divisorproductfirstimaginary) = S ge_signed_half_sum_second_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_sum_second_divisorproduct) + ge_balance_negative_sum_second_divisorproductfirstimaginary = (ge_first_in_sum_second_divisorproduct) + ge_balance_positive_sum_second_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_sum_second_divisorproductsecond ge_representation_imaginary_code_sum_second_divisorproductsecond. (((gr_quotient_sum_second_divisor) = ((ge_representation_real_code_sum_second_divisorproductsecond) + (ge_representation_imaginary_code_sum_second_divisorproductsecond)) * S ((ge_representation_real_code_sum_second_divisorproductsecond) + (ge_representation_imaginary_code_sum_second_divisorproductsecond)) + ((ge_representation_imaginary_code_sum_second_divisorproductsecond) + (ge_representation_imaginary_code_sum_second_divisorproductsecond))) /\ ((exists ge_balance_positive_sum_second_divisorproductsecondreal ge_balance_negative_sum_second_divisorproductsecondreal. (((((ge_representation_real_code_sum_second_divisorproductsecond) = 2 * (ge_balance_positive_sum_second_divisorproductsecondreal) /\ (ge_balance_negative_sum_second_divisorproductsecondreal) = 0) \/ exists ge_signed_half_sum_second_divisorproductsecondrealdecode. (((ge_representation_real_code_sum_second_divisorproductsecond) = 2 * ge_signed_half_sum_second_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_sum_second_divisorproductsecondreal) = 0) /\ (ge_balance_negative_sum_second_divisorproductsecondreal) = S ge_signed_half_sum_second_divisorproductsecondrealdecode))) /\ ((ge_second_rp_sum_second_divisorproduct) + ge_balance_negative_sum_second_divisorproductsecondreal = (ge_second_rn_sum_second_divisorproduct) + ge_balance_positive_sum_second_divisorproductsecondreal))) /\ (exists ge_balance_positive_sum_second_divisorproductsecondimaginary ge_balance_negative_sum_second_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_sum_second_divisorproductsecond) = 2 * (ge_balance_positive_sum_second_divisorproductsecondimaginary) /\ (ge_balance_negative_sum_second_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_sum_second_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_sum_second_divisorproductsecond) = 2 * ge_signed_half_sum_second_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_sum_second_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_sum_second_divisorproductsecondimaginary) = S ge_signed_half_sum_second_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_sum_second_divisorproduct) + ge_balance_negative_sum_second_divisorproductsecondimaginary = (ge_second_in_sum_second_divisorproduct) + ge_balance_positive_sum_second_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_sum_second_divisorproductoutput ge_representation_imaginary_code_sum_second_divisorproductoutput. (((b) = ((ge_representation_real_code_sum_second_divisorproductoutput) + (ge_representation_imaginary_code_sum_second_divisorproductoutput)) * S ((ge_representation_real_code_sum_second_divisorproductoutput) + (ge_representation_imaginary_code_sum_second_divisorproductoutput)) + ((ge_representation_imaginary_code_sum_second_divisorproductoutput) + (ge_representation_imaginary_code_sum_second_divisorproductoutput))) /\ ((exists ge_balance_positive_sum_second_divisorproductoutputreal ge_balance_negative_sum_second_divisorproductoutputreal. (((((ge_representation_real_code_sum_second_divisorproductoutput) = 2 * (ge_balance_positive_sum_second_divisorproductoutputreal) /\ (ge_balance_negative_sum_second_divisorproductoutputreal) = 0) \/ exists ge_signed_half_sum_second_divisorproductoutputrealdecode. (((ge_representation_real_code_sum_second_divisorproductoutput) = 2 * ge_signed_half_sum_second_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_sum_second_divisorproductoutputreal) = 0) /\ (ge_balance_negative_sum_second_divisorproductoutputreal) = S ge_signed_half_sum_second_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_sum_second_divisorproduct) * (ge_second_rp_sum_second_divisorproduct))) + (((ge_first_rn_sum_second_divisorproduct) * (ge_second_rn_sum_second_divisorproduct))))) + (((((ge_first_ip_sum_second_divisorproduct) * (ge_second_in_sum_second_divisorproduct))) + (((ge_first_in_sum_second_divisorproduct) * (ge_second_ip_sum_second_divisorproduct))))))) + ge_balance_negative_sum_second_divisorproductoutputreal = (((((((ge_first_rp_sum_second_divisorproduct) * (ge_second_rn_sum_second_divisorproduct))) + (((ge_first_rn_sum_second_divisorproduct) * (ge_second_rp_sum_second_divisorproduct))))) + (((((ge_first_ip_sum_second_divisorproduct) * (ge_second_ip_sum_second_divisorproduct))) + (((ge_first_in_sum_second_divisorproduct) * (ge_second_in_sum_second_divisorproduct))))))) + ge_balance_positive_sum_second_divisorproductoutputreal))) /\ (exists ge_balance_positive_sum_second_divisorproductoutputimaginary ge_balance_negative_sum_second_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_sum_second_divisorproductoutput) = 2 * (ge_balance_positive_sum_second_divisorproductoutputimaginary) /\ (ge_balance_negative_sum_second_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_sum_second_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_sum_second_divisorproductoutput) = 2 * ge_signed_half_sum_second_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_sum_second_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_sum_second_divisorproductoutputimaginary) = S ge_signed_half_sum_second_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_sum_second_divisorproduct) * (ge_second_ip_sum_second_divisorproduct))) + (((ge_first_rn_sum_second_divisorproduct) * (ge_second_in_sum_second_divisorproduct))))) + (((((ge_first_ip_sum_second_divisorproduct) * (ge_second_rp_sum_second_divisorproduct))) + (((ge_first_in_sum_second_divisorproduct) * (ge_second_rn_sum_second_divisorproduct))))))) + ge_balance_negative_sum_second_divisorproductoutputimaginary = (((((((ge_first_rp_sum_second_divisorproduct) * (ge_second_in_sum_second_divisorproduct))) + (((ge_first_rn_sum_second_divisorproduct) * (ge_second_ip_sum_second_divisorproduct))))) + (((((ge_first_ip_sum_second_divisorproduct) * (ge_second_rn_sum_second_divisorproduct))) + (((ge_first_in_sum_second_divisorproduct) * (ge_second_rp_sum_second_divisorproduct))))))) + ge_balance_positive_sum_second_divisorproductoutputimaginary)))))))))) -> (exists ge_first_rp_sum_given ge_first_rn_sum_given ge_first_ip_sum_given ge_first_in_sum_given ge_second_rp_sum_given ge_second_rn_sum_given ge_second_ip_sum_given ge_second_in_sum_given. ((exists ge_representation_real_code_sum_givenfirst ge_representation_imaginary_code_sum_givenfirst. (((a) = ((ge_representation_real_code_sum_givenfirst) + (ge_representation_imaginary_code_sum_givenfirst)) * S ((ge_representation_real_code_sum_givenfirst) + (ge_representation_imaginary_code_sum_givenfirst)) + ((ge_representation_imaginary_code_sum_givenfirst) + (ge_representation_imaginary_code_sum_givenfirst))) /\ ((exists ge_balance_positive_sum_givenfirstreal ge_balance_negative_sum_givenfirstreal. (((((ge_representation_real_code_sum_givenfirst) = 2 * (ge_balance_positive_sum_givenfirstreal) /\ (ge_balance_negative_sum_givenfirstreal) = 0) \/ exists ge_signed_half_sum_givenfirstrealdecode. (((ge_representation_real_code_sum_givenfirst) = 2 * ge_signed_half_sum_givenfirstrealdecode + 1 /\ (ge_balance_positive_sum_givenfirstreal) = 0) /\ (ge_balance_negative_sum_givenfirstreal) = S ge_signed_half_sum_givenfirstrealdecode))) /\ ((ge_first_rp_sum_given) + ge_balance_negative_sum_givenfirstreal = (ge_first_rn_sum_given) + ge_balance_positive_sum_givenfirstreal))) /\ (exists ge_balance_positive_sum_givenfirstimaginary ge_balance_negative_sum_givenfirstimaginary. (((((ge_representation_imaginary_code_sum_givenfirst) = 2 * (ge_balance_positive_sum_givenfirstimaginary) /\ (ge_balance_negative_sum_givenfirstimaginary) = 0) \/ exists ge_signed_half_sum_givenfirstimaginarydecode. (((ge_representation_imaginary_code_sum_givenfirst) = 2 * ge_signed_half_sum_givenfirstimaginarydecode + 1 /\ (ge_balance_positive_sum_givenfirstimaginary) = 0) /\ (ge_balance_negative_sum_givenfirstimaginary) = S ge_signed_half_sum_givenfirstimaginarydecode))) /\ ((ge_first_ip_sum_given) + ge_balance_negative_sum_givenfirstimaginary = (ge_first_in_sum_given) + ge_balance_positive_sum_givenfirstimaginary)))))) /\ ((exists ge_representation_real_code_sum_givensecond ge_representation_imaginary_code_sum_givensecond. (((b) = ((ge_representation_real_code_sum_givensecond) + (ge_representation_imaginary_code_sum_givensecond)) * S ((ge_representation_real_code_sum_givensecond) + (ge_representation_imaginary_code_sum_givensecond)) + ((ge_representation_imaginary_code_sum_givensecond) + (ge_representation_imaginary_code_sum_givensecond))) /\ ((exists ge_balance_positive_sum_givensecondreal ge_balance_negative_sum_givensecondreal. (((((ge_representation_real_code_sum_givensecond) = 2 * (ge_balance_positive_sum_givensecondreal) /\ (ge_balance_negative_sum_givensecondreal) = 0) \/ exists ge_signed_half_sum_givensecondrealdecode. (((ge_representation_real_code_sum_givensecond) = 2 * ge_signed_half_sum_givensecondrealdecode + 1 /\ (ge_balance_positive_sum_givensecondreal) = 0) /\ (ge_balance_negative_sum_givensecondreal) = S ge_signed_half_sum_givensecondrealdecode))) /\ ((ge_second_rp_sum_given) + ge_balance_negative_sum_givensecondreal = (ge_second_rn_sum_given) + ge_balance_positive_sum_givensecondreal))) /\ (exists ge_balance_positive_sum_givensecondimaginary ge_balance_negative_sum_givensecondimaginary. (((((ge_representation_imaginary_code_sum_givensecond) = 2 * (ge_balance_positive_sum_givensecondimaginary) /\ (ge_balance_negative_sum_givensecondimaginary) = 0) \/ exists ge_signed_half_sum_givensecondimaginarydecode. (((ge_representation_imaginary_code_sum_givensecond) = 2 * ge_signed_half_sum_givensecondimaginarydecode + 1 /\ (ge_balance_positive_sum_givensecondimaginary) = 0) /\ (ge_balance_negative_sum_givensecondimaginary) = S ge_signed_half_sum_givensecondimaginarydecode))) /\ ((ge_second_ip_sum_given) + ge_balance_negative_sum_givensecondimaginary = (ge_second_in_sum_given) + ge_balance_positive_sum_givensecondimaginary)))))) /\ (exists ge_representation_real_code_sum_givenoutput ge_representation_imaginary_code_sum_givenoutput. (((c) = ((ge_representation_real_code_sum_givenoutput) + (ge_representation_imaginary_code_sum_givenoutput)) * S ((ge_representation_real_code_sum_givenoutput) + (ge_representation_imaginary_code_sum_givenoutput)) + ((ge_representation_imaginary_code_sum_givenoutput) + (ge_representation_imaginary_code_sum_givenoutput))) /\ ((exists ge_balance_positive_sum_givenoutputreal ge_balance_negative_sum_givenoutputreal. (((((ge_representation_real_code_sum_givenoutput) = 2 * (ge_balance_positive_sum_givenoutputreal) /\ (ge_balance_negative_sum_givenoutputreal) = 0) \/ exists ge_signed_half_sum_givenoutputrealdecode. (((ge_representation_real_code_sum_givenoutput) = 2 * ge_signed_half_sum_givenoutputrealdecode + 1 /\ (ge_balance_positive_sum_givenoutputreal) = 0) /\ (ge_balance_negative_sum_givenoutputreal) = S ge_signed_half_sum_givenoutputrealdecode))) /\ ((((ge_first_rp_sum_given) + (ge_second_rp_sum_given))) + ge_balance_negative_sum_givenoutputreal = (((ge_first_rn_sum_given) + (ge_second_rn_sum_given))) + ge_balance_positive_sum_givenoutputreal))) /\ (exists ge_balance_positive_sum_givenoutputimaginary ge_balance_negative_sum_givenoutputimaginary. (((((ge_representation_imaginary_code_sum_givenoutput) = 2 * (ge_balance_positive_sum_givenoutputimaginary) /\ (ge_balance_negative_sum_givenoutputimaginary) = 0) \/ exists ge_signed_half_sum_givenoutputimaginarydecode. (((ge_representation_imaginary_code_sum_givenoutput) = 2 * ge_signed_half_sum_givenoutputimaginarydecode + 1 /\ (ge_balance_positive_sum_givenoutputimaginary) = 0) /\ (ge_balance_negative_sum_givenoutputimaginary) = S ge_signed_half_sum_givenoutputimaginarydecode))) /\ ((((ge_first_ip_sum_given) + (ge_second_ip_sum_given))) + ge_balance_negative_sum_givenoutputimaginary = (((ge_first_in_sum_given) + (ge_second_in_sum_given))) + ge_balance_positive_sum_givenoutputimaginary))))))))) -> (exists gr_quotient_sum_result. (exists ge_first_rp_sum_resultproduct ge_first_rn_sum_resultproduct ge_first_ip_sum_resultproduct ge_first_in_sum_resultproduct ge_second_rp_sum_resultproduct ge_second_rn_sum_resultproduct ge_second_ip_sum_resultproduct ge_second_in_sum_resultproduct. ((exists ge_representation_real_code_sum_resultproductfirst ge_representation_imaginary_code_sum_resultproductfirst. (((d) = ((ge_representation_real_code_sum_resultproductfirst) + (ge_representation_imaginary_code_sum_resultproductfirst)) * S ((ge_representation_real_code_sum_resultproductfirst) + (ge_representation_imaginary_code_sum_resultproductfirst)) + ((ge_representation_imaginary_code_sum_resultproductfirst) + (ge_representation_imaginary_code_sum_resultproductfirst))) /\ ((exists ge_balance_positive_sum_resultproductfirstreal ge_balance_negative_sum_resultproductfirstreal. (((((ge_representation_real_code_sum_resultproductfirst) = 2 * (ge_balance_positive_sum_resultproductfirstreal) /\ (ge_balance_negative_sum_resultproductfirstreal) = 0) \/ exists ge_signed_half_sum_resultproductfirstrealdecode. (((ge_representation_real_code_sum_resultproductfirst) = 2 * ge_signed_half_sum_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_sum_resultproductfirstreal) = 0) /\ (ge_balance_negative_sum_resultproductfirstreal) = S ge_signed_half_sum_resultproductfirstrealdecode))) /\ ((ge_first_rp_sum_resultproduct) + ge_balance_negative_sum_resultproductfirstreal = (ge_first_rn_sum_resultproduct) + ge_balance_positive_sum_resultproductfirstreal))) /\ (exists ge_balance_positive_sum_resultproductfirstimaginary ge_balance_negative_sum_resultproductfirstimaginary. (((((ge_representation_imaginary_code_sum_resultproductfirst) = 2 * (ge_balance_positive_sum_resultproductfirstimaginary) /\ (ge_balance_negative_sum_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_sum_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_sum_resultproductfirst) = 2 * ge_signed_half_sum_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_sum_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_sum_resultproductfirstimaginary) = S ge_signed_half_sum_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_sum_resultproduct) + ge_balance_negative_sum_resultproductfirstimaginary = (ge_first_in_sum_resultproduct) + ge_balance_positive_sum_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_sum_resultproductsecond ge_representation_imaginary_code_sum_resultproductsecond. (((gr_quotient_sum_result) = ((ge_representation_real_code_sum_resultproductsecond) + (ge_representation_imaginary_code_sum_resultproductsecond)) * S ((ge_representation_real_code_sum_resultproductsecond) + (ge_representation_imaginary_code_sum_resultproductsecond)) + ((ge_representation_imaginary_code_sum_resultproductsecond) + (ge_representation_imaginary_code_sum_resultproductsecond))) /\ ((exists ge_balance_positive_sum_resultproductsecondreal ge_balance_negative_sum_resultproductsecondreal. (((((ge_representation_real_code_sum_resultproductsecond) = 2 * (ge_balance_positive_sum_resultproductsecondreal) /\ (ge_balance_negative_sum_resultproductsecondreal) = 0) \/ exists ge_signed_half_sum_resultproductsecondrealdecode. (((ge_representation_real_code_sum_resultproductsecond) = 2 * ge_signed_half_sum_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_sum_resultproductsecondreal) = 0) /\ (ge_balance_negative_sum_resultproductsecondreal) = S ge_signed_half_sum_resultproductsecondrealdecode))) /\ ((ge_second_rp_sum_resultproduct) + ge_balance_negative_sum_resultproductsecondreal = (ge_second_rn_sum_resultproduct) + ge_balance_positive_sum_resultproductsecondreal))) /\ (exists ge_balance_positive_sum_resultproductsecondimaginary ge_balance_negative_sum_resultproductsecondimaginary. (((((ge_representation_imaginary_code_sum_resultproductsecond) = 2 * (ge_balance_positive_sum_resultproductsecondimaginary) /\ (ge_balance_negative_sum_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_sum_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_sum_resultproductsecond) = 2 * ge_signed_half_sum_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_sum_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_sum_resultproductsecondimaginary) = S ge_signed_half_sum_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_sum_resultproduct) + ge_balance_negative_sum_resultproductsecondimaginary = (ge_second_in_sum_resultproduct) + ge_balance_positive_sum_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_sum_resultproductoutput ge_representation_imaginary_code_sum_resultproductoutput. (((c) = ((ge_representation_real_code_sum_resultproductoutput) + (ge_representation_imaginary_code_sum_resultproductoutput)) * S ((ge_representation_real_code_sum_resultproductoutput) + (ge_representation_imaginary_code_sum_resultproductoutput)) + ((ge_representation_imaginary_code_sum_resultproductoutput) + (ge_representation_imaginary_code_sum_resultproductoutput))) /\ ((exists ge_balance_positive_sum_resultproductoutputreal ge_balance_negative_sum_resultproductoutputreal. (((((ge_representation_real_code_sum_resultproductoutput) = 2 * (ge_balance_positive_sum_resultproductoutputreal) /\ (ge_balance_negative_sum_resultproductoutputreal) = 0) \/ exists ge_signed_half_sum_resultproductoutputrealdecode. (((ge_representation_real_code_sum_resultproductoutput) = 2 * ge_signed_half_sum_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_sum_resultproductoutputreal) = 0) /\ (ge_balance_negative_sum_resultproductoutputreal) = S ge_signed_half_sum_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_sum_resultproduct) * (ge_second_rp_sum_resultproduct))) + (((ge_first_rn_sum_resultproduct) * (ge_second_rn_sum_resultproduct))))) + (((((ge_first_ip_sum_resultproduct) * (ge_second_in_sum_resultproduct))) + (((ge_first_in_sum_resultproduct) * (ge_second_ip_sum_resultproduct))))))) + ge_balance_negative_sum_resultproductoutputreal = (((((((ge_first_rp_sum_resultproduct) * (ge_second_rn_sum_resultproduct))) + (((ge_first_rn_sum_resultproduct) * (ge_second_rp_sum_resultproduct))))) + (((((ge_first_ip_sum_resultproduct) * (ge_second_ip_sum_resultproduct))) + (((ge_first_in_sum_resultproduct) * (ge_second_in_sum_resultproduct))))))) + ge_balance_positive_sum_resultproductoutputreal))) /\ (exists ge_balance_positive_sum_resultproductoutputimaginary ge_balance_negative_sum_resultproductoutputimaginary. (((((ge_representation_imaginary_code_sum_resultproductoutput) = 2 * (ge_balance_positive_sum_resultproductoutputimaginary) /\ (ge_balance_negative_sum_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_sum_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_sum_resultproductoutput) = 2 * ge_signed_half_sum_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_sum_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_sum_resultproductoutputimaginary) = S ge_signed_half_sum_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_sum_resultproduct) * (ge_second_ip_sum_resultproduct))) + (((ge_first_rn_sum_resultproduct) * (ge_second_in_sum_resultproduct))))) + (((((ge_first_ip_sum_resultproduct) * (ge_second_rp_sum_resultproduct))) + (((ge_first_in_sum_resultproduct) * (ge_second_rn_sum_resultproduct))))))) + ge_balance_negative_sum_resultproductoutputimaginary = (((((((ge_first_rp_sum_resultproduct) * (ge_second_in_sum_resultproduct))) + (((ge_first_rn_sum_resultproduct) * (ge_second_ip_sum_resultproduct))))) + (((((ge_first_ip_sum_resultproduct) * (ge_second_rn_sum_resultproduct))) + (((ge_first_in_sum_resultproduct) * (ge_second_rp_sum_resultproduct))))))) + ge_balance_positive_sum_resultproductoutputimaginary))))))))))