gaussian_common_divisor_subtract

forall d a b c. (exists gr_quotient_difference_first_divisor. (exists ge_first_rp_difference_first_divisorproduct ge_first_rn_difference_first_divisorproduct ge_first_ip_difference_first_divisorproduct ge_first_in_difference_first_divisorproduct ge_second_rp_difference_first_divisorproduct ge_second_rn_difference_first_divisorproduct ge_second_ip_difference_first_divisorproduct ge_second_in_difference_first_divisorproduct. ((exists ge_representation_real_code_difference_first_divisorproductfirst ge_representation_imaginary_code_difference_first_divisorproductfirst. (((d) = ((ge_representation_real_code_difference_first_divisorproductfirst) + (ge_representation_imaginary_code_difference_first_divisorproductfirst)) * S ((ge_representation_real_code_difference_first_divisorproductfirst) + (ge_representation_imaginary_code_difference_first_divisorproductfirst)) + ((ge_representation_imaginary_code_difference_first_divisorproductfirst) + (ge_representation_imaginary_code_difference_first_divisorproductfirst))) /\ ((exists ge_balance_positive_difference_first_divisorproductfirstreal ge_balance_negative_difference_first_divisorproductfirstreal. (((((ge_representation_real_code_difference_first_divisorproductfirst) = 2 * (ge_balance_positive_difference_first_divisorproductfirstreal) /\ (ge_balance_negative_difference_first_divisorproductfirstreal) = 0) \/ exists ge_signed_half_difference_first_divisorproductfirstrealdecode. (((ge_representation_real_code_difference_first_divisorproductfirst) = 2 * ge_signed_half_difference_first_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_difference_first_divisorproductfirstreal) = 0) /\ (ge_balance_negative_difference_first_divisorproductfirstreal) = S ge_signed_half_difference_first_divisorproductfirstrealdecode))) /\ ((ge_first_rp_difference_first_divisorproduct) + ge_balance_negative_difference_first_divisorproductfirstreal = (ge_first_rn_difference_first_divisorproduct) + ge_balance_positive_difference_first_divisorproductfirstreal))) /\ (exists ge_balance_positive_difference_first_divisorproductfirstimaginary ge_balance_negative_difference_first_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_difference_first_divisorproductfirst) = 2 * (ge_balance_positive_difference_first_divisorproductfirstimaginary) /\ (ge_balance_negative_difference_first_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_difference_first_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_difference_first_divisorproductfirst) = 2 * ge_signed_half_difference_first_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_first_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_difference_first_divisorproductfirstimaginary) = S ge_signed_half_difference_first_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_difference_first_divisorproduct) + ge_balance_negative_difference_first_divisorproductfirstimaginary = (ge_first_in_difference_first_divisorproduct) + ge_balance_positive_difference_first_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_first_divisorproductsecond ge_representation_imaginary_code_difference_first_divisorproductsecond. (((gr_quotient_difference_first_divisor) = ((ge_representation_real_code_difference_first_divisorproductsecond) + (ge_representation_imaginary_code_difference_first_divisorproductsecond)) * S ((ge_representation_real_code_difference_first_divisorproductsecond) + (ge_representation_imaginary_code_difference_first_divisorproductsecond)) + ((ge_representation_imaginary_code_difference_first_divisorproductsecond) + (ge_representation_imaginary_code_difference_first_divisorproductsecond))) /\ ((exists ge_balance_positive_difference_first_divisorproductsecondreal ge_balance_negative_difference_first_divisorproductsecondreal. (((((ge_representation_real_code_difference_first_divisorproductsecond) = 2 * (ge_balance_positive_difference_first_divisorproductsecondreal) /\ (ge_balance_negative_difference_first_divisorproductsecondreal) = 0) \/ exists ge_signed_half_difference_first_divisorproductsecondrealdecode. (((ge_representation_real_code_difference_first_divisorproductsecond) = 2 * ge_signed_half_difference_first_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_difference_first_divisorproductsecondreal) = 0) /\ (ge_balance_negative_difference_first_divisorproductsecondreal) = S ge_signed_half_difference_first_divisorproductsecondrealdecode))) /\ ((ge_second_rp_difference_first_divisorproduct) + ge_balance_negative_difference_first_divisorproductsecondreal = (ge_second_rn_difference_first_divisorproduct) + ge_balance_positive_difference_first_divisorproductsecondreal))) /\ (exists ge_balance_positive_difference_first_divisorproductsecondimaginary ge_balance_negative_difference_first_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_difference_first_divisorproductsecond) = 2 * (ge_balance_positive_difference_first_divisorproductsecondimaginary) /\ (ge_balance_negative_difference_first_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_difference_first_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_difference_first_divisorproductsecond) = 2 * ge_signed_half_difference_first_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_first_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_difference_first_divisorproductsecondimaginary) = S ge_signed_half_difference_first_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_difference_first_divisorproduct) + ge_balance_negative_difference_first_divisorproductsecondimaginary = (ge_second_in_difference_first_divisorproduct) + ge_balance_positive_difference_first_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_first_divisorproductoutput ge_representation_imaginary_code_difference_first_divisorproductoutput. (((a) = ((ge_representation_real_code_difference_first_divisorproductoutput) + (ge_representation_imaginary_code_difference_first_divisorproductoutput)) * S ((ge_representation_real_code_difference_first_divisorproductoutput) + (ge_representation_imaginary_code_difference_first_divisorproductoutput)) + ((ge_representation_imaginary_code_difference_first_divisorproductoutput) + (ge_representation_imaginary_code_difference_first_divisorproductoutput))) /\ ((exists ge_balance_positive_difference_first_divisorproductoutputreal ge_balance_negative_difference_first_divisorproductoutputreal. (((((ge_representation_real_code_difference_first_divisorproductoutput) = 2 * (ge_balance_positive_difference_first_divisorproductoutputreal) /\ (ge_balance_negative_difference_first_divisorproductoutputreal) = 0) \/ exists ge_signed_half_difference_first_divisorproductoutputrealdecode. (((ge_representation_real_code_difference_first_divisorproductoutput) = 2 * ge_signed_half_difference_first_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_difference_first_divisorproductoutputreal) = 0) /\ (ge_balance_negative_difference_first_divisorproductoutputreal) = S ge_signed_half_difference_first_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_difference_first_divisorproduct) * (ge_second_rp_difference_first_divisorproduct))) + (((ge_first_rn_difference_first_divisorproduct) * (ge_second_rn_difference_first_divisorproduct))))) + (((((ge_first_ip_difference_first_divisorproduct) * (ge_second_in_difference_first_divisorproduct))) + (((ge_first_in_difference_first_divisorproduct) * (ge_second_ip_difference_first_divisorproduct))))))) + ge_balance_negative_difference_first_divisorproductoutputreal = (((((((ge_first_rp_difference_first_divisorproduct) * (ge_second_rn_difference_first_divisorproduct))) + (((ge_first_rn_difference_first_divisorproduct) * (ge_second_rp_difference_first_divisorproduct))))) + (((((ge_first_ip_difference_first_divisorproduct) * (ge_second_ip_difference_first_divisorproduct))) + (((ge_first_in_difference_first_divisorproduct) * (ge_second_in_difference_first_divisorproduct))))))) + ge_balance_positive_difference_first_divisorproductoutputreal))) /\ (exists ge_balance_positive_difference_first_divisorproductoutputimaginary ge_balance_negative_difference_first_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_difference_first_divisorproductoutput) = 2 * (ge_balance_positive_difference_first_divisorproductoutputimaginary) /\ (ge_balance_negative_difference_first_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_difference_first_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_difference_first_divisorproductoutput) = 2 * ge_signed_half_difference_first_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_first_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_difference_first_divisorproductoutputimaginary) = S ge_signed_half_difference_first_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_difference_first_divisorproduct) * (ge_second_ip_difference_first_divisorproduct))) + (((ge_first_rn_difference_first_divisorproduct) * (ge_second_in_difference_first_divisorproduct))))) + (((((ge_first_ip_difference_first_divisorproduct) * (ge_second_rp_difference_first_divisorproduct))) + (((ge_first_in_difference_first_divisorproduct) * (ge_second_rn_difference_first_divisorproduct))))))) + ge_balance_negative_difference_first_divisorproductoutputimaginary = (((((((ge_first_rp_difference_first_divisorproduct) * (ge_second_in_difference_first_divisorproduct))) + (((ge_first_rn_difference_first_divisorproduct) * (ge_second_ip_difference_first_divisorproduct))))) + (((((ge_first_ip_difference_first_divisorproduct) * (ge_second_rn_difference_first_divisorproduct))) + (((ge_first_in_difference_first_divisorproduct) * (ge_second_rp_difference_first_divisorproduct))))))) + ge_balance_positive_difference_first_divisorproductoutputimaginary)))))))))) -> (exists gr_quotient_difference_second_divisor. (exists ge_first_rp_difference_second_divisorproduct ge_first_rn_difference_second_divisorproduct ge_first_ip_difference_second_divisorproduct ge_first_in_difference_second_divisorproduct ge_second_rp_difference_second_divisorproduct ge_second_rn_difference_second_divisorproduct ge_second_ip_difference_second_divisorproduct ge_second_in_difference_second_divisorproduct. ((exists ge_representation_real_code_difference_second_divisorproductfirst ge_representation_imaginary_code_difference_second_divisorproductfirst. (((d) = ((ge_representation_real_code_difference_second_divisorproductfirst) + (ge_representation_imaginary_code_difference_second_divisorproductfirst)) * S ((ge_representation_real_code_difference_second_divisorproductfirst) + (ge_representation_imaginary_code_difference_second_divisorproductfirst)) + ((ge_representation_imaginary_code_difference_second_divisorproductfirst) + (ge_representation_imaginary_code_difference_second_divisorproductfirst))) /\ ((exists ge_balance_positive_difference_second_divisorproductfirstreal ge_balance_negative_difference_second_divisorproductfirstreal. (((((ge_representation_real_code_difference_second_divisorproductfirst) = 2 * (ge_balance_positive_difference_second_divisorproductfirstreal) /\ (ge_balance_negative_difference_second_divisorproductfirstreal) = 0) \/ exists ge_signed_half_difference_second_divisorproductfirstrealdecode. (((ge_representation_real_code_difference_second_divisorproductfirst) = 2 * ge_signed_half_difference_second_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_difference_second_divisorproductfirstreal) = 0) /\ (ge_balance_negative_difference_second_divisorproductfirstreal) = S ge_signed_half_difference_second_divisorproductfirstrealdecode))) /\ ((ge_first_rp_difference_second_divisorproduct) + ge_balance_negative_difference_second_divisorproductfirstreal = (ge_first_rn_difference_second_divisorproduct) + ge_balance_positive_difference_second_divisorproductfirstreal))) /\ (exists ge_balance_positive_difference_second_divisorproductfirstimaginary ge_balance_negative_difference_second_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_difference_second_divisorproductfirst) = 2 * (ge_balance_positive_difference_second_divisorproductfirstimaginary) /\ (ge_balance_negative_difference_second_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_difference_second_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_difference_second_divisorproductfirst) = 2 * ge_signed_half_difference_second_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_second_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_difference_second_divisorproductfirstimaginary) = S ge_signed_half_difference_second_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_difference_second_divisorproduct) + ge_balance_negative_difference_second_divisorproductfirstimaginary = (ge_first_in_difference_second_divisorproduct) + ge_balance_positive_difference_second_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_second_divisorproductsecond ge_representation_imaginary_code_difference_second_divisorproductsecond. (((gr_quotient_difference_second_divisor) = ((ge_representation_real_code_difference_second_divisorproductsecond) + (ge_representation_imaginary_code_difference_second_divisorproductsecond)) * S ((ge_representation_real_code_difference_second_divisorproductsecond) + (ge_representation_imaginary_code_difference_second_divisorproductsecond)) + ((ge_representation_imaginary_code_difference_second_divisorproductsecond) + (ge_representation_imaginary_code_difference_second_divisorproductsecond))) /\ ((exists ge_balance_positive_difference_second_divisorproductsecondreal ge_balance_negative_difference_second_divisorproductsecondreal. (((((ge_representation_real_code_difference_second_divisorproductsecond) = 2 * (ge_balance_positive_difference_second_divisorproductsecondreal) /\ (ge_balance_negative_difference_second_divisorproductsecondreal) = 0) \/ exists ge_signed_half_difference_second_divisorproductsecondrealdecode. (((ge_representation_real_code_difference_second_divisorproductsecond) = 2 * ge_signed_half_difference_second_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_difference_second_divisorproductsecondreal) = 0) /\ (ge_balance_negative_difference_second_divisorproductsecondreal) = S ge_signed_half_difference_second_divisorproductsecondrealdecode))) /\ ((ge_second_rp_difference_second_divisorproduct) + ge_balance_negative_difference_second_divisorproductsecondreal = (ge_second_rn_difference_second_divisorproduct) + ge_balance_positive_difference_second_divisorproductsecondreal))) /\ (exists ge_balance_positive_difference_second_divisorproductsecondimaginary ge_balance_negative_difference_second_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_difference_second_divisorproductsecond) = 2 * (ge_balance_positive_difference_second_divisorproductsecondimaginary) /\ (ge_balance_negative_difference_second_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_difference_second_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_difference_second_divisorproductsecond) = 2 * ge_signed_half_difference_second_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_second_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_difference_second_divisorproductsecondimaginary) = S ge_signed_half_difference_second_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_difference_second_divisorproduct) + ge_balance_negative_difference_second_divisorproductsecondimaginary = (ge_second_in_difference_second_divisorproduct) + ge_balance_positive_difference_second_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_second_divisorproductoutput ge_representation_imaginary_code_difference_second_divisorproductoutput. (((b) = ((ge_representation_real_code_difference_second_divisorproductoutput) + (ge_representation_imaginary_code_difference_second_divisorproductoutput)) * S ((ge_representation_real_code_difference_second_divisorproductoutput) + (ge_representation_imaginary_code_difference_second_divisorproductoutput)) + ((ge_representation_imaginary_code_difference_second_divisorproductoutput) + (ge_representation_imaginary_code_difference_second_divisorproductoutput))) /\ ((exists ge_balance_positive_difference_second_divisorproductoutputreal ge_balance_negative_difference_second_divisorproductoutputreal. (((((ge_representation_real_code_difference_second_divisorproductoutput) = 2 * (ge_balance_positive_difference_second_divisorproductoutputreal) /\ (ge_balance_negative_difference_second_divisorproductoutputreal) = 0) \/ exists ge_signed_half_difference_second_divisorproductoutputrealdecode. (((ge_representation_real_code_difference_second_divisorproductoutput) = 2 * ge_signed_half_difference_second_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_difference_second_divisorproductoutputreal) = 0) /\ (ge_balance_negative_difference_second_divisorproductoutputreal) = S ge_signed_half_difference_second_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_difference_second_divisorproduct) * (ge_second_rp_difference_second_divisorproduct))) + (((ge_first_rn_difference_second_divisorproduct) * (ge_second_rn_difference_second_divisorproduct))))) + (((((ge_first_ip_difference_second_divisorproduct) * (ge_second_in_difference_second_divisorproduct))) + (((ge_first_in_difference_second_divisorproduct) * (ge_second_ip_difference_second_divisorproduct))))))) + ge_balance_negative_difference_second_divisorproductoutputreal = (((((((ge_first_rp_difference_second_divisorproduct) * (ge_second_rn_difference_second_divisorproduct))) + (((ge_first_rn_difference_second_divisorproduct) * (ge_second_rp_difference_second_divisorproduct))))) + (((((ge_first_ip_difference_second_divisorproduct) * (ge_second_ip_difference_second_divisorproduct))) + (((ge_first_in_difference_second_divisorproduct) * (ge_second_in_difference_second_divisorproduct))))))) + ge_balance_positive_difference_second_divisorproductoutputreal))) /\ (exists ge_balance_positive_difference_second_divisorproductoutputimaginary ge_balance_negative_difference_second_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_difference_second_divisorproductoutput) = 2 * (ge_balance_positive_difference_second_divisorproductoutputimaginary) /\ (ge_balance_negative_difference_second_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_difference_second_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_difference_second_divisorproductoutput) = 2 * ge_signed_half_difference_second_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_second_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_difference_second_divisorproductoutputimaginary) = S ge_signed_half_difference_second_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_difference_second_divisorproduct) * (ge_second_ip_difference_second_divisorproduct))) + (((ge_first_rn_difference_second_divisorproduct) * (ge_second_in_difference_second_divisorproduct))))) + (((((ge_first_ip_difference_second_divisorproduct) * (ge_second_rp_difference_second_divisorproduct))) + (((ge_first_in_difference_second_divisorproduct) * (ge_second_rn_difference_second_divisorproduct))))))) + ge_balance_negative_difference_second_divisorproductoutputimaginary = (((((((ge_first_rp_difference_second_divisorproduct) * (ge_second_in_difference_second_divisorproduct))) + (((ge_first_rn_difference_second_divisorproduct) * (ge_second_ip_difference_second_divisorproduct))))) + (((((ge_first_ip_difference_second_divisorproduct) * (ge_second_rn_difference_second_divisorproduct))) + (((ge_first_in_difference_second_divisorproduct) * (ge_second_rp_difference_second_divisorproduct))))))) + ge_balance_positive_difference_second_divisorproductoutputimaginary)))))))))) -> (exists ge_first_rp_difference_equation ge_first_rn_difference_equation ge_first_ip_difference_equation ge_first_in_difference_equation ge_second_rp_difference_equation ge_second_rn_difference_equation ge_second_ip_difference_equation ge_second_in_difference_equation. ((exists ge_representation_real_code_difference_equationfirst ge_representation_imaginary_code_difference_equationfirst. (((c) = ((ge_representation_real_code_difference_equationfirst) + (ge_representation_imaginary_code_difference_equationfirst)) * S ((ge_representation_real_code_difference_equationfirst) + (ge_representation_imaginary_code_difference_equationfirst)) + ((ge_representation_imaginary_code_difference_equationfirst) + (ge_representation_imaginary_code_difference_equationfirst))) /\ ((exists ge_balance_positive_difference_equationfirstreal ge_balance_negative_difference_equationfirstreal. (((((ge_representation_real_code_difference_equationfirst) = 2 * (ge_balance_positive_difference_equationfirstreal) /\ (ge_balance_negative_difference_equationfirstreal) = 0) \/ exists ge_signed_half_difference_equationfirstrealdecode. (((ge_representation_real_code_difference_equationfirst) = 2 * ge_signed_half_difference_equationfirstrealdecode + 1 /\ (ge_balance_positive_difference_equationfirstreal) = 0) /\ (ge_balance_negative_difference_equationfirstreal) = S ge_signed_half_difference_equationfirstrealdecode))) /\ ((ge_first_rp_difference_equation) + ge_balance_negative_difference_equationfirstreal = (ge_first_rn_difference_equation) + ge_balance_positive_difference_equationfirstreal))) /\ (exists ge_balance_positive_difference_equationfirstimaginary ge_balance_negative_difference_equationfirstimaginary. (((((ge_representation_imaginary_code_difference_equationfirst) = 2 * (ge_balance_positive_difference_equationfirstimaginary) /\ (ge_balance_negative_difference_equationfirstimaginary) = 0) \/ exists ge_signed_half_difference_equationfirstimaginarydecode. (((ge_representation_imaginary_code_difference_equationfirst) = 2 * ge_signed_half_difference_equationfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_equationfirstimaginary) = 0) /\ (ge_balance_negative_difference_equationfirstimaginary) = S ge_signed_half_difference_equationfirstimaginarydecode))) /\ ((ge_first_ip_difference_equation) + ge_balance_negative_difference_equationfirstimaginary = (ge_first_in_difference_equation) + ge_balance_positive_difference_equationfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_equationsecond ge_representation_imaginary_code_difference_equationsecond. (((b) = ((ge_representation_real_code_difference_equationsecond) + (ge_representation_imaginary_code_difference_equationsecond)) * S ((ge_representation_real_code_difference_equationsecond) + (ge_representation_imaginary_code_difference_equationsecond)) + ((ge_representation_imaginary_code_difference_equationsecond) + (ge_representation_imaginary_code_difference_equationsecond))) /\ ((exists ge_balance_positive_difference_equationsecondreal ge_balance_negative_difference_equationsecondreal. (((((ge_representation_real_code_difference_equationsecond) = 2 * (ge_balance_positive_difference_equationsecondreal) /\ (ge_balance_negative_difference_equationsecondreal) = 0) \/ exists ge_signed_half_difference_equationsecondrealdecode. (((ge_representation_real_code_difference_equationsecond) = 2 * ge_signed_half_difference_equationsecondrealdecode + 1 /\ (ge_balance_positive_difference_equationsecondreal) = 0) /\ (ge_balance_negative_difference_equationsecondreal) = S ge_signed_half_difference_equationsecondrealdecode))) /\ ((ge_second_rp_difference_equation) + ge_balance_negative_difference_equationsecondreal = (ge_second_rn_difference_equation) + ge_balance_positive_difference_equationsecondreal))) /\ (exists ge_balance_positive_difference_equationsecondimaginary ge_balance_negative_difference_equationsecondimaginary. (((((ge_representation_imaginary_code_difference_equationsecond) = 2 * (ge_balance_positive_difference_equationsecondimaginary) /\ (ge_balance_negative_difference_equationsecondimaginary) = 0) \/ exists ge_signed_half_difference_equationsecondimaginarydecode. (((ge_representation_imaginary_code_difference_equationsecond) = 2 * ge_signed_half_difference_equationsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_equationsecondimaginary) = 0) /\ (ge_balance_negative_difference_equationsecondimaginary) = S ge_signed_half_difference_equationsecondimaginarydecode))) /\ ((ge_second_ip_difference_equation) + ge_balance_negative_difference_equationsecondimaginary = (ge_second_in_difference_equation) + ge_balance_positive_difference_equationsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_equationoutput ge_representation_imaginary_code_difference_equationoutput. (((a) = ((ge_representation_real_code_difference_equationoutput) + (ge_representation_imaginary_code_difference_equationoutput)) * S ((ge_representation_real_code_difference_equationoutput) + (ge_representation_imaginary_code_difference_equationoutput)) + ((ge_representation_imaginary_code_difference_equationoutput) + (ge_representation_imaginary_code_difference_equationoutput))) /\ ((exists ge_balance_positive_difference_equationoutputreal ge_balance_negative_difference_equationoutputreal. (((((ge_representation_real_code_difference_equationoutput) = 2 * (ge_balance_positive_difference_equationoutputreal) /\ (ge_balance_negative_difference_equationoutputreal) = 0) \/ exists ge_signed_half_difference_equationoutputrealdecode. (((ge_representation_real_code_difference_equationoutput) = 2 * ge_signed_half_difference_equationoutputrealdecode + 1 /\ (ge_balance_positive_difference_equationoutputreal) = 0) /\ (ge_balance_negative_difference_equationoutputreal) = S ge_signed_half_difference_equationoutputrealdecode))) /\ ((((ge_first_rp_difference_equation) + (ge_second_rp_difference_equation))) + ge_balance_negative_difference_equationoutputreal = (((ge_first_rn_difference_equation) + (ge_second_rn_difference_equation))) + ge_balance_positive_difference_equationoutputreal))) /\ (exists ge_balance_positive_difference_equationoutputimaginary ge_balance_negative_difference_equationoutputimaginary. (((((ge_representation_imaginary_code_difference_equationoutput) = 2 * (ge_balance_positive_difference_equationoutputimaginary) /\ (ge_balance_negative_difference_equationoutputimaginary) = 0) \/ exists ge_signed_half_difference_equationoutputimaginarydecode. (((ge_representation_imaginary_code_difference_equationoutput) = 2 * ge_signed_half_difference_equationoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_equationoutputimaginary) = 0) /\ (ge_balance_negative_difference_equationoutputimaginary) = S ge_signed_half_difference_equationoutputimaginarydecode))) /\ ((((ge_first_ip_difference_equation) + (ge_second_ip_difference_equation))) + ge_balance_negative_difference_equationoutputimaginary = (((ge_first_in_difference_equation) + (ge_second_in_difference_equation))) + ge_balance_positive_difference_equationoutputimaginary))))))))) -> (exists gr_quotient_difference_result. (exists ge_first_rp_difference_resultproduct ge_first_rn_difference_resultproduct ge_first_ip_difference_resultproduct ge_first_in_difference_resultproduct ge_second_rp_difference_resultproduct ge_second_rn_difference_resultproduct ge_second_ip_difference_resultproduct ge_second_in_difference_resultproduct. ((exists ge_representation_real_code_difference_resultproductfirst ge_representation_imaginary_code_difference_resultproductfirst. (((d) = ((ge_representation_real_code_difference_resultproductfirst) + (ge_representation_imaginary_code_difference_resultproductfirst)) * S ((ge_representation_real_code_difference_resultproductfirst) + (ge_representation_imaginary_code_difference_resultproductfirst)) + ((ge_representation_imaginary_code_difference_resultproductfirst) + (ge_representation_imaginary_code_difference_resultproductfirst))) /\ ((exists ge_balance_positive_difference_resultproductfirstreal ge_balance_negative_difference_resultproductfirstreal. (((((ge_representation_real_code_difference_resultproductfirst) = 2 * (ge_balance_positive_difference_resultproductfirstreal) /\ (ge_balance_negative_difference_resultproductfirstreal) = 0) \/ exists ge_signed_half_difference_resultproductfirstrealdecode. (((ge_representation_real_code_difference_resultproductfirst) = 2 * ge_signed_half_difference_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_difference_resultproductfirstreal) = 0) /\ (ge_balance_negative_difference_resultproductfirstreal) = S ge_signed_half_difference_resultproductfirstrealdecode))) /\ ((ge_first_rp_difference_resultproduct) + ge_balance_negative_difference_resultproductfirstreal = (ge_first_rn_difference_resultproduct) + ge_balance_positive_difference_resultproductfirstreal))) /\ (exists ge_balance_positive_difference_resultproductfirstimaginary ge_balance_negative_difference_resultproductfirstimaginary. (((((ge_representation_imaginary_code_difference_resultproductfirst) = 2 * (ge_balance_positive_difference_resultproductfirstimaginary) /\ (ge_balance_negative_difference_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_difference_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_difference_resultproductfirst) = 2 * ge_signed_half_difference_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_difference_resultproductfirstimaginary) = S ge_signed_half_difference_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_difference_resultproduct) + ge_balance_negative_difference_resultproductfirstimaginary = (ge_first_in_difference_resultproduct) + ge_balance_positive_difference_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_resultproductsecond ge_representation_imaginary_code_difference_resultproductsecond. (((gr_quotient_difference_result) = ((ge_representation_real_code_difference_resultproductsecond) + (ge_representation_imaginary_code_difference_resultproductsecond)) * S ((ge_representation_real_code_difference_resultproductsecond) + (ge_representation_imaginary_code_difference_resultproductsecond)) + ((ge_representation_imaginary_code_difference_resultproductsecond) + (ge_representation_imaginary_code_difference_resultproductsecond))) /\ ((exists ge_balance_positive_difference_resultproductsecondreal ge_balance_negative_difference_resultproductsecondreal. (((((ge_representation_real_code_difference_resultproductsecond) = 2 * (ge_balance_positive_difference_resultproductsecondreal) /\ (ge_balance_negative_difference_resultproductsecondreal) = 0) \/ exists ge_signed_half_difference_resultproductsecondrealdecode. (((ge_representation_real_code_difference_resultproductsecond) = 2 * ge_signed_half_difference_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_difference_resultproductsecondreal) = 0) /\ (ge_balance_negative_difference_resultproductsecondreal) = S ge_signed_half_difference_resultproductsecondrealdecode))) /\ ((ge_second_rp_difference_resultproduct) + ge_balance_negative_difference_resultproductsecondreal = (ge_second_rn_difference_resultproduct) + ge_balance_positive_difference_resultproductsecondreal))) /\ (exists ge_balance_positive_difference_resultproductsecondimaginary ge_balance_negative_difference_resultproductsecondimaginary. (((((ge_representation_imaginary_code_difference_resultproductsecond) = 2 * (ge_balance_positive_difference_resultproductsecondimaginary) /\ (ge_balance_negative_difference_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_difference_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_difference_resultproductsecond) = 2 * ge_signed_half_difference_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_difference_resultproductsecondimaginary) = S ge_signed_half_difference_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_difference_resultproduct) + ge_balance_negative_difference_resultproductsecondimaginary = (ge_second_in_difference_resultproduct) + ge_balance_positive_difference_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_resultproductoutput ge_representation_imaginary_code_difference_resultproductoutput. (((c) = ((ge_representation_real_code_difference_resultproductoutput) + (ge_representation_imaginary_code_difference_resultproductoutput)) * S ((ge_representation_real_code_difference_resultproductoutput) + (ge_representation_imaginary_code_difference_resultproductoutput)) + ((ge_representation_imaginary_code_difference_resultproductoutput) + (ge_representation_imaginary_code_difference_resultproductoutput))) /\ ((exists ge_balance_positive_difference_resultproductoutputreal ge_balance_negative_difference_resultproductoutputreal. (((((ge_representation_real_code_difference_resultproductoutput) = 2 * (ge_balance_positive_difference_resultproductoutputreal) /\ (ge_balance_negative_difference_resultproductoutputreal) = 0) \/ exists ge_signed_half_difference_resultproductoutputrealdecode. (((ge_representation_real_code_difference_resultproductoutput) = 2 * ge_signed_half_difference_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_difference_resultproductoutputreal) = 0) /\ (ge_balance_negative_difference_resultproductoutputreal) = S ge_signed_half_difference_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_difference_resultproduct) * (ge_second_rp_difference_resultproduct))) + (((ge_first_rn_difference_resultproduct) * (ge_second_rn_difference_resultproduct))))) + (((((ge_first_ip_difference_resultproduct) * (ge_second_in_difference_resultproduct))) + (((ge_first_in_difference_resultproduct) * (ge_second_ip_difference_resultproduct))))))) + ge_balance_negative_difference_resultproductoutputreal = (((((((ge_first_rp_difference_resultproduct) * (ge_second_rn_difference_resultproduct))) + (((ge_first_rn_difference_resultproduct) * (ge_second_rp_difference_resultproduct))))) + (((((ge_first_ip_difference_resultproduct) * (ge_second_ip_difference_resultproduct))) + (((ge_first_in_difference_resultproduct) * (ge_second_in_difference_resultproduct))))))) + ge_balance_positive_difference_resultproductoutputreal))) /\ (exists ge_balance_positive_difference_resultproductoutputimaginary ge_balance_negative_difference_resultproductoutputimaginary. (((((ge_representation_imaginary_code_difference_resultproductoutput) = 2 * (ge_balance_positive_difference_resultproductoutputimaginary) /\ (ge_balance_negative_difference_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_difference_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_difference_resultproductoutput) = 2 * ge_signed_half_difference_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_difference_resultproductoutputimaginary) = S ge_signed_half_difference_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_difference_resultproduct) * (ge_second_ip_difference_resultproduct))) + (((ge_first_rn_difference_resultproduct) * (ge_second_in_difference_resultproduct))))) + (((((ge_first_ip_difference_resultproduct) * (ge_second_rp_difference_resultproduct))) + (((ge_first_in_difference_resultproduct) * (ge_second_rn_difference_resultproduct))))))) + ge_balance_negative_difference_resultproductoutputimaginary = (((((((ge_first_rp_difference_resultproduct) * (ge_second_in_difference_resultproduct))) + (((ge_first_rn_difference_resultproduct) * (ge_second_ip_difference_resultproduct))))) + (((((ge_first_ip_difference_resultproduct) * (ge_second_rn_difference_resultproduct))) + (((ge_first_in_difference_resultproduct) * (ge_second_rp_difference_resultproduct))))))) + ge_balance_positive_difference_resultproductoutputimaginary))))))))))