gaussian_common_divisor_of_bezout

forall d g a b u v. (exists gr_quotient_bezout_divisor_first. (exists ge_first_rp_bezout_divisor_firstproduct ge_first_rn_bezout_divisor_firstproduct ge_first_ip_bezout_divisor_firstproduct ge_first_in_bezout_divisor_firstproduct ge_second_rp_bezout_divisor_firstproduct ge_second_rn_bezout_divisor_firstproduct ge_second_ip_bezout_divisor_firstproduct ge_second_in_bezout_divisor_firstproduct. ((exists ge_representation_real_code_bezout_divisor_firstproductfirst ge_representation_imaginary_code_bezout_divisor_firstproductfirst. (((d) = ((ge_representation_real_code_bezout_divisor_firstproductfirst) + (ge_representation_imaginary_code_bezout_divisor_firstproductfirst)) * S ((ge_representation_real_code_bezout_divisor_firstproductfirst) + (ge_representation_imaginary_code_bezout_divisor_firstproductfirst)) + ((ge_representation_imaginary_code_bezout_divisor_firstproductfirst) + (ge_representation_imaginary_code_bezout_divisor_firstproductfirst))) /\ ((exists ge_balance_positive_bezout_divisor_firstproductfirstreal ge_balance_negative_bezout_divisor_firstproductfirstreal. (((((ge_representation_real_code_bezout_divisor_firstproductfirst) = 2 * (ge_balance_positive_bezout_divisor_firstproductfirstreal) /\ (ge_balance_negative_bezout_divisor_firstproductfirstreal) = 0) \/ exists ge_signed_half_bezout_divisor_firstproductfirstrealdecode. (((ge_representation_real_code_bezout_divisor_firstproductfirst) = 2 * ge_signed_half_bezout_divisor_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_firstproductfirstreal) = 0) /\ (ge_balance_negative_bezout_divisor_firstproductfirstreal) = S ge_signed_half_bezout_divisor_firstproductfirstrealdecode))) /\ ((ge_first_rp_bezout_divisor_firstproduct) + ge_balance_negative_bezout_divisor_firstproductfirstreal = (ge_first_rn_bezout_divisor_firstproduct) + ge_balance_positive_bezout_divisor_firstproductfirstreal))) /\ (exists ge_balance_positive_bezout_divisor_firstproductfirstimaginary ge_balance_negative_bezout_divisor_firstproductfirstimaginary. (((((ge_representation_imaginary_code_bezout_divisor_firstproductfirst) = 2 * (ge_balance_positive_bezout_divisor_firstproductfirstimaginary) /\ (ge_balance_negative_bezout_divisor_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_firstproductfirst) = 2 * ge_signed_half_bezout_divisor_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_firstproductfirstimaginary) = S ge_signed_half_bezout_divisor_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_bezout_divisor_firstproduct) + ge_balance_negative_bezout_divisor_firstproductfirstimaginary = (ge_first_in_bezout_divisor_firstproduct) + ge_balance_positive_bezout_divisor_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_divisor_firstproductsecond ge_representation_imaginary_code_bezout_divisor_firstproductsecond. (((gr_quotient_bezout_divisor_first) = ((ge_representation_real_code_bezout_divisor_firstproductsecond) + (ge_representation_imaginary_code_bezout_divisor_firstproductsecond)) * S ((ge_representation_real_code_bezout_divisor_firstproductsecond) + (ge_representation_imaginary_code_bezout_divisor_firstproductsecond)) + ((ge_representation_imaginary_code_bezout_divisor_firstproductsecond) + (ge_representation_imaginary_code_bezout_divisor_firstproductsecond))) /\ ((exists ge_balance_positive_bezout_divisor_firstproductsecondreal ge_balance_negative_bezout_divisor_firstproductsecondreal. (((((ge_representation_real_code_bezout_divisor_firstproductsecond) = 2 * (ge_balance_positive_bezout_divisor_firstproductsecondreal) /\ (ge_balance_negative_bezout_divisor_firstproductsecondreal) = 0) \/ exists ge_signed_half_bezout_divisor_firstproductsecondrealdecode. (((ge_representation_real_code_bezout_divisor_firstproductsecond) = 2 * ge_signed_half_bezout_divisor_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_firstproductsecondreal) = 0) /\ (ge_balance_negative_bezout_divisor_firstproductsecondreal) = S ge_signed_half_bezout_divisor_firstproductsecondrealdecode))) /\ ((ge_second_rp_bezout_divisor_firstproduct) + ge_balance_negative_bezout_divisor_firstproductsecondreal = (ge_second_rn_bezout_divisor_firstproduct) + ge_balance_positive_bezout_divisor_firstproductsecondreal))) /\ (exists ge_balance_positive_bezout_divisor_firstproductsecondimaginary ge_balance_negative_bezout_divisor_firstproductsecondimaginary. (((((ge_representation_imaginary_code_bezout_divisor_firstproductsecond) = 2 * (ge_balance_positive_bezout_divisor_firstproductsecondimaginary) /\ (ge_balance_negative_bezout_divisor_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_firstproductsecond) = 2 * ge_signed_half_bezout_divisor_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_firstproductsecondimaginary) = S ge_signed_half_bezout_divisor_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_bezout_divisor_firstproduct) + ge_balance_negative_bezout_divisor_firstproductsecondimaginary = (ge_second_in_bezout_divisor_firstproduct) + ge_balance_positive_bezout_divisor_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_divisor_firstproductoutput ge_representation_imaginary_code_bezout_divisor_firstproductoutput. (((a) = ((ge_representation_real_code_bezout_divisor_firstproductoutput) + (ge_representation_imaginary_code_bezout_divisor_firstproductoutput)) * S ((ge_representation_real_code_bezout_divisor_firstproductoutput) + (ge_representation_imaginary_code_bezout_divisor_firstproductoutput)) + ((ge_representation_imaginary_code_bezout_divisor_firstproductoutput) + (ge_representation_imaginary_code_bezout_divisor_firstproductoutput))) /\ ((exists ge_balance_positive_bezout_divisor_firstproductoutputreal ge_balance_negative_bezout_divisor_firstproductoutputreal. (((((ge_representation_real_code_bezout_divisor_firstproductoutput) = 2 * (ge_balance_positive_bezout_divisor_firstproductoutputreal) /\ (ge_balance_negative_bezout_divisor_firstproductoutputreal) = 0) \/ exists ge_signed_half_bezout_divisor_firstproductoutputrealdecode. (((ge_representation_real_code_bezout_divisor_firstproductoutput) = 2 * ge_signed_half_bezout_divisor_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_firstproductoutputreal) = 0) /\ (ge_balance_negative_bezout_divisor_firstproductoutputreal) = S ge_signed_half_bezout_divisor_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_divisor_firstproduct) * (ge_second_rp_bezout_divisor_firstproduct))) + (((ge_first_rn_bezout_divisor_firstproduct) * (ge_second_rn_bezout_divisor_firstproduct))))) + (((((ge_first_ip_bezout_divisor_firstproduct) * (ge_second_in_bezout_divisor_firstproduct))) + (((ge_first_in_bezout_divisor_firstproduct) * (ge_second_ip_bezout_divisor_firstproduct))))))) + ge_balance_negative_bezout_divisor_firstproductoutputreal = (((((((ge_first_rp_bezout_divisor_firstproduct) * (ge_second_rn_bezout_divisor_firstproduct))) + (((ge_first_rn_bezout_divisor_firstproduct) * (ge_second_rp_bezout_divisor_firstproduct))))) + (((((ge_first_ip_bezout_divisor_firstproduct) * (ge_second_ip_bezout_divisor_firstproduct))) + (((ge_first_in_bezout_divisor_firstproduct) * (ge_second_in_bezout_divisor_firstproduct))))))) + ge_balance_positive_bezout_divisor_firstproductoutputreal))) /\ (exists ge_balance_positive_bezout_divisor_firstproductoutputimaginary ge_balance_negative_bezout_divisor_firstproductoutputimaginary. (((((ge_representation_imaginary_code_bezout_divisor_firstproductoutput) = 2 * (ge_balance_positive_bezout_divisor_firstproductoutputimaginary) /\ (ge_balance_negative_bezout_divisor_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_firstproductoutput) = 2 * ge_signed_half_bezout_divisor_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_firstproductoutputimaginary) = S ge_signed_half_bezout_divisor_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_divisor_firstproduct) * (ge_second_ip_bezout_divisor_firstproduct))) + (((ge_first_rn_bezout_divisor_firstproduct) * (ge_second_in_bezout_divisor_firstproduct))))) + (((((ge_first_ip_bezout_divisor_firstproduct) * (ge_second_rp_bezout_divisor_firstproduct))) + (((ge_first_in_bezout_divisor_firstproduct) * (ge_second_rn_bezout_divisor_firstproduct))))))) + ge_balance_negative_bezout_divisor_firstproductoutputimaginary = (((((((ge_first_rp_bezout_divisor_firstproduct) * (ge_second_in_bezout_divisor_firstproduct))) + (((ge_first_rn_bezout_divisor_firstproduct) * (ge_second_ip_bezout_divisor_firstproduct))))) + (((((ge_first_ip_bezout_divisor_firstproduct) * (ge_second_rn_bezout_divisor_firstproduct))) + (((ge_first_in_bezout_divisor_firstproduct) * (ge_second_rp_bezout_divisor_firstproduct))))))) + ge_balance_positive_bezout_divisor_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_bezout_divisor_second. (exists ge_first_rp_bezout_divisor_secondproduct ge_first_rn_bezout_divisor_secondproduct ge_first_ip_bezout_divisor_secondproduct ge_first_in_bezout_divisor_secondproduct ge_second_rp_bezout_divisor_secondproduct ge_second_rn_bezout_divisor_secondproduct ge_second_ip_bezout_divisor_secondproduct ge_second_in_bezout_divisor_secondproduct. ((exists ge_representation_real_code_bezout_divisor_secondproductfirst ge_representation_imaginary_code_bezout_divisor_secondproductfirst. (((d) = ((ge_representation_real_code_bezout_divisor_secondproductfirst) + (ge_representation_imaginary_code_bezout_divisor_secondproductfirst)) * S ((ge_representation_real_code_bezout_divisor_secondproductfirst) + (ge_representation_imaginary_code_bezout_divisor_secondproductfirst)) + ((ge_representation_imaginary_code_bezout_divisor_secondproductfirst) + (ge_representation_imaginary_code_bezout_divisor_secondproductfirst))) /\ ((exists ge_balance_positive_bezout_divisor_secondproductfirstreal ge_balance_negative_bezout_divisor_secondproductfirstreal. (((((ge_representation_real_code_bezout_divisor_secondproductfirst) = 2 * (ge_balance_positive_bezout_divisor_secondproductfirstreal) /\ (ge_balance_negative_bezout_divisor_secondproductfirstreal) = 0) \/ exists ge_signed_half_bezout_divisor_secondproductfirstrealdecode. (((ge_representation_real_code_bezout_divisor_secondproductfirst) = 2 * ge_signed_half_bezout_divisor_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_secondproductfirstreal) = 0) /\ (ge_balance_negative_bezout_divisor_secondproductfirstreal) = S ge_signed_half_bezout_divisor_secondproductfirstrealdecode))) /\ ((ge_first_rp_bezout_divisor_secondproduct) + ge_balance_negative_bezout_divisor_secondproductfirstreal = (ge_first_rn_bezout_divisor_secondproduct) + ge_balance_positive_bezout_divisor_secondproductfirstreal))) /\ (exists ge_balance_positive_bezout_divisor_secondproductfirstimaginary ge_balance_negative_bezout_divisor_secondproductfirstimaginary. (((((ge_representation_imaginary_code_bezout_divisor_secondproductfirst) = 2 * (ge_balance_positive_bezout_divisor_secondproductfirstimaginary) /\ (ge_balance_negative_bezout_divisor_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_secondproductfirst) = 2 * ge_signed_half_bezout_divisor_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_secondproductfirstimaginary) = S ge_signed_half_bezout_divisor_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_bezout_divisor_secondproduct) + ge_balance_negative_bezout_divisor_secondproductfirstimaginary = (ge_first_in_bezout_divisor_secondproduct) + ge_balance_positive_bezout_divisor_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_divisor_secondproductsecond ge_representation_imaginary_code_bezout_divisor_secondproductsecond. (((gr_quotient_bezout_divisor_second) = ((ge_representation_real_code_bezout_divisor_secondproductsecond) + (ge_representation_imaginary_code_bezout_divisor_secondproductsecond)) * S ((ge_representation_real_code_bezout_divisor_secondproductsecond) + (ge_representation_imaginary_code_bezout_divisor_secondproductsecond)) + ((ge_representation_imaginary_code_bezout_divisor_secondproductsecond) + (ge_representation_imaginary_code_bezout_divisor_secondproductsecond))) /\ ((exists ge_balance_positive_bezout_divisor_secondproductsecondreal ge_balance_negative_bezout_divisor_secondproductsecondreal. (((((ge_representation_real_code_bezout_divisor_secondproductsecond) = 2 * (ge_balance_positive_bezout_divisor_secondproductsecondreal) /\ (ge_balance_negative_bezout_divisor_secondproductsecondreal) = 0) \/ exists ge_signed_half_bezout_divisor_secondproductsecondrealdecode. (((ge_representation_real_code_bezout_divisor_secondproductsecond) = 2 * ge_signed_half_bezout_divisor_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_secondproductsecondreal) = 0) /\ (ge_balance_negative_bezout_divisor_secondproductsecondreal) = S ge_signed_half_bezout_divisor_secondproductsecondrealdecode))) /\ ((ge_second_rp_bezout_divisor_secondproduct) + ge_balance_negative_bezout_divisor_secondproductsecondreal = (ge_second_rn_bezout_divisor_secondproduct) + ge_balance_positive_bezout_divisor_secondproductsecondreal))) /\ (exists ge_balance_positive_bezout_divisor_secondproductsecondimaginary ge_balance_negative_bezout_divisor_secondproductsecondimaginary. (((((ge_representation_imaginary_code_bezout_divisor_secondproductsecond) = 2 * (ge_balance_positive_bezout_divisor_secondproductsecondimaginary) /\ (ge_balance_negative_bezout_divisor_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_secondproductsecond) = 2 * ge_signed_half_bezout_divisor_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_secondproductsecondimaginary) = S ge_signed_half_bezout_divisor_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_bezout_divisor_secondproduct) + ge_balance_negative_bezout_divisor_secondproductsecondimaginary = (ge_second_in_bezout_divisor_secondproduct) + ge_balance_positive_bezout_divisor_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_divisor_secondproductoutput ge_representation_imaginary_code_bezout_divisor_secondproductoutput. (((b) = ((ge_representation_real_code_bezout_divisor_secondproductoutput) + (ge_representation_imaginary_code_bezout_divisor_secondproductoutput)) * S ((ge_representation_real_code_bezout_divisor_secondproductoutput) + (ge_representation_imaginary_code_bezout_divisor_secondproductoutput)) + ((ge_representation_imaginary_code_bezout_divisor_secondproductoutput) + (ge_representation_imaginary_code_bezout_divisor_secondproductoutput))) /\ ((exists ge_balance_positive_bezout_divisor_secondproductoutputreal ge_balance_negative_bezout_divisor_secondproductoutputreal. (((((ge_representation_real_code_bezout_divisor_secondproductoutput) = 2 * (ge_balance_positive_bezout_divisor_secondproductoutputreal) /\ (ge_balance_negative_bezout_divisor_secondproductoutputreal) = 0) \/ exists ge_signed_half_bezout_divisor_secondproductoutputrealdecode. (((ge_representation_real_code_bezout_divisor_secondproductoutput) = 2 * ge_signed_half_bezout_divisor_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_secondproductoutputreal) = 0) /\ (ge_balance_negative_bezout_divisor_secondproductoutputreal) = S ge_signed_half_bezout_divisor_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_divisor_secondproduct) * (ge_second_rp_bezout_divisor_secondproduct))) + (((ge_first_rn_bezout_divisor_secondproduct) * (ge_second_rn_bezout_divisor_secondproduct))))) + (((((ge_first_ip_bezout_divisor_secondproduct) * (ge_second_in_bezout_divisor_secondproduct))) + (((ge_first_in_bezout_divisor_secondproduct) * (ge_second_ip_bezout_divisor_secondproduct))))))) + ge_balance_negative_bezout_divisor_secondproductoutputreal = (((((((ge_first_rp_bezout_divisor_secondproduct) * (ge_second_rn_bezout_divisor_secondproduct))) + (((ge_first_rn_bezout_divisor_secondproduct) * (ge_second_rp_bezout_divisor_secondproduct))))) + (((((ge_first_ip_bezout_divisor_secondproduct) * (ge_second_ip_bezout_divisor_secondproduct))) + (((ge_first_in_bezout_divisor_secondproduct) * (ge_second_in_bezout_divisor_secondproduct))))))) + ge_balance_positive_bezout_divisor_secondproductoutputreal))) /\ (exists ge_balance_positive_bezout_divisor_secondproductoutputimaginary ge_balance_negative_bezout_divisor_secondproductoutputimaginary. (((((ge_representation_imaginary_code_bezout_divisor_secondproductoutput) = 2 * (ge_balance_positive_bezout_divisor_secondproductoutputimaginary) /\ (ge_balance_negative_bezout_divisor_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_secondproductoutput) = 2 * ge_signed_half_bezout_divisor_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_secondproductoutputimaginary) = S ge_signed_half_bezout_divisor_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_divisor_secondproduct) * (ge_second_ip_bezout_divisor_secondproduct))) + (((ge_first_rn_bezout_divisor_secondproduct) * (ge_second_in_bezout_divisor_secondproduct))))) + (((((ge_first_ip_bezout_divisor_secondproduct) * (ge_second_rp_bezout_divisor_secondproduct))) + (((ge_first_in_bezout_divisor_secondproduct) * (ge_second_rn_bezout_divisor_secondproduct))))))) + ge_balance_negative_bezout_divisor_secondproductoutputimaginary = (((((((ge_first_rp_bezout_divisor_secondproduct) * (ge_second_in_bezout_divisor_secondproduct))) + (((ge_first_rn_bezout_divisor_secondproduct) * (ge_second_ip_bezout_divisor_secondproduct))))) + (((((ge_first_ip_bezout_divisor_secondproduct) * (ge_second_rn_bezout_divisor_secondproduct))) + (((ge_first_in_bezout_divisor_secondproduct) * (ge_second_rp_bezout_divisor_secondproduct))))))) + ge_balance_positive_bezout_divisor_secondproductoutputimaginary)))))))))) -> (exists gr_first_product_bezout_divisor_equation gr_second_product_bezout_divisor_equation. ((exists ge_first_rp_bezout_divisor_equationfirst ge_first_rn_bezout_divisor_equationfirst ge_first_ip_bezout_divisor_equationfirst ge_first_in_bezout_divisor_equationfirst ge_second_rp_bezout_divisor_equationfirst ge_second_rn_bezout_divisor_equationfirst ge_second_ip_bezout_divisor_equationfirst ge_second_in_bezout_divisor_equationfirst. ((exists ge_representation_real_code_bezout_divisor_equationfirstfirst ge_representation_imaginary_code_bezout_divisor_equationfirstfirst. (((a) = ((ge_representation_real_code_bezout_divisor_equationfirstfirst) + (ge_representation_imaginary_code_bezout_divisor_equationfirstfirst)) * S ((ge_representation_real_code_bezout_divisor_equationfirstfirst) + (ge_representation_imaginary_code_bezout_divisor_equationfirstfirst)) + ((ge_representation_imaginary_code_bezout_divisor_equationfirstfirst) + (ge_representation_imaginary_code_bezout_divisor_equationfirstfirst))) /\ ((exists ge_balance_positive_bezout_divisor_equationfirstfirstreal ge_balance_negative_bezout_divisor_equationfirstfirstreal. (((((ge_representation_real_code_bezout_divisor_equationfirstfirst) = 2 * (ge_balance_positive_bezout_divisor_equationfirstfirstreal) /\ (ge_balance_negative_bezout_divisor_equationfirstfirstreal) = 0) \/ exists ge_signed_half_bezout_divisor_equationfirstfirstrealdecode. (((ge_representation_real_code_bezout_divisor_equationfirstfirst) = 2 * ge_signed_half_bezout_divisor_equationfirstfirstrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_equationfirstfirstreal) = 0) /\ (ge_balance_negative_bezout_divisor_equationfirstfirstreal) = S ge_signed_half_bezout_divisor_equationfirstfirstrealdecode))) /\ ((ge_first_rp_bezout_divisor_equationfirst) + ge_balance_negative_bezout_divisor_equationfirstfirstreal = (ge_first_rn_bezout_divisor_equationfirst) + ge_balance_positive_bezout_divisor_equationfirstfirstreal))) /\ (exists ge_balance_positive_bezout_divisor_equationfirstfirstimaginary ge_balance_negative_bezout_divisor_equationfirstfirstimaginary. (((((ge_representation_imaginary_code_bezout_divisor_equationfirstfirst) = 2 * (ge_balance_positive_bezout_divisor_equationfirstfirstimaginary) /\ (ge_balance_negative_bezout_divisor_equationfirstfirstimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_equationfirstfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_equationfirstfirst) = 2 * ge_signed_half_bezout_divisor_equationfirstfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_equationfirstfirstimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_equationfirstfirstimaginary) = S ge_signed_half_bezout_divisor_equationfirstfirstimaginarydecode))) /\ ((ge_first_ip_bezout_divisor_equationfirst) + ge_balance_negative_bezout_divisor_equationfirstfirstimaginary = (ge_first_in_bezout_divisor_equationfirst) + ge_balance_positive_bezout_divisor_equationfirstfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_divisor_equationfirstsecond ge_representation_imaginary_code_bezout_divisor_equationfirstsecond. (((u) = ((ge_representation_real_code_bezout_divisor_equationfirstsecond) + (ge_representation_imaginary_code_bezout_divisor_equationfirstsecond)) * S ((ge_representation_real_code_bezout_divisor_equationfirstsecond) + (ge_representation_imaginary_code_bezout_divisor_equationfirstsecond)) + ((ge_representation_imaginary_code_bezout_divisor_equationfirstsecond) + (ge_representation_imaginary_code_bezout_divisor_equationfirstsecond))) /\ ((exists ge_balance_positive_bezout_divisor_equationfirstsecondreal ge_balance_negative_bezout_divisor_equationfirstsecondreal. (((((ge_representation_real_code_bezout_divisor_equationfirstsecond) = 2 * (ge_balance_positive_bezout_divisor_equationfirstsecondreal) /\ (ge_balance_negative_bezout_divisor_equationfirstsecondreal) = 0) \/ exists ge_signed_half_bezout_divisor_equationfirstsecondrealdecode. (((ge_representation_real_code_bezout_divisor_equationfirstsecond) = 2 * ge_signed_half_bezout_divisor_equationfirstsecondrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_equationfirstsecondreal) = 0) /\ (ge_balance_negative_bezout_divisor_equationfirstsecondreal) = S ge_signed_half_bezout_divisor_equationfirstsecondrealdecode))) /\ ((ge_second_rp_bezout_divisor_equationfirst) + ge_balance_negative_bezout_divisor_equationfirstsecondreal = (ge_second_rn_bezout_divisor_equationfirst) + ge_balance_positive_bezout_divisor_equationfirstsecondreal))) /\ (exists ge_balance_positive_bezout_divisor_equationfirstsecondimaginary ge_balance_negative_bezout_divisor_equationfirstsecondimaginary. (((((ge_representation_imaginary_code_bezout_divisor_equationfirstsecond) = 2 * (ge_balance_positive_bezout_divisor_equationfirstsecondimaginary) /\ (ge_balance_negative_bezout_divisor_equationfirstsecondimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_equationfirstsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_equationfirstsecond) = 2 * ge_signed_half_bezout_divisor_equationfirstsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_equationfirstsecondimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_equationfirstsecondimaginary) = S ge_signed_half_bezout_divisor_equationfirstsecondimaginarydecode))) /\ ((ge_second_ip_bezout_divisor_equationfirst) + ge_balance_negative_bezout_divisor_equationfirstsecondimaginary = (ge_second_in_bezout_divisor_equationfirst) + ge_balance_positive_bezout_divisor_equationfirstsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_divisor_equationfirstoutput ge_representation_imaginary_code_bezout_divisor_equationfirstoutput. (((gr_first_product_bezout_divisor_equation) = ((ge_representation_real_code_bezout_divisor_equationfirstoutput) + (ge_representation_imaginary_code_bezout_divisor_equationfirstoutput)) * S ((ge_representation_real_code_bezout_divisor_equationfirstoutput) + (ge_representation_imaginary_code_bezout_divisor_equationfirstoutput)) + ((ge_representation_imaginary_code_bezout_divisor_equationfirstoutput) + (ge_representation_imaginary_code_bezout_divisor_equationfirstoutput))) /\ ((exists ge_balance_positive_bezout_divisor_equationfirstoutputreal ge_balance_negative_bezout_divisor_equationfirstoutputreal. (((((ge_representation_real_code_bezout_divisor_equationfirstoutput) = 2 * (ge_balance_positive_bezout_divisor_equationfirstoutputreal) /\ (ge_balance_negative_bezout_divisor_equationfirstoutputreal) = 0) \/ exists ge_signed_half_bezout_divisor_equationfirstoutputrealdecode. (((ge_representation_real_code_bezout_divisor_equationfirstoutput) = 2 * ge_signed_half_bezout_divisor_equationfirstoutputrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_equationfirstoutputreal) = 0) /\ (ge_balance_negative_bezout_divisor_equationfirstoutputreal) = S ge_signed_half_bezout_divisor_equationfirstoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_divisor_equationfirst) * (ge_second_rp_bezout_divisor_equationfirst))) + (((ge_first_rn_bezout_divisor_equationfirst) * (ge_second_rn_bezout_divisor_equationfirst))))) + (((((ge_first_ip_bezout_divisor_equationfirst) * (ge_second_in_bezout_divisor_equationfirst))) + (((ge_first_in_bezout_divisor_equationfirst) * (ge_second_ip_bezout_divisor_equationfirst))))))) + ge_balance_negative_bezout_divisor_equationfirstoutputreal = (((((((ge_first_rp_bezout_divisor_equationfirst) * (ge_second_rn_bezout_divisor_equationfirst))) + (((ge_first_rn_bezout_divisor_equationfirst) * (ge_second_rp_bezout_divisor_equationfirst))))) + (((((ge_first_ip_bezout_divisor_equationfirst) * (ge_second_ip_bezout_divisor_equationfirst))) + (((ge_first_in_bezout_divisor_equationfirst) * (ge_second_in_bezout_divisor_equationfirst))))))) + ge_balance_positive_bezout_divisor_equationfirstoutputreal))) /\ (exists ge_balance_positive_bezout_divisor_equationfirstoutputimaginary ge_balance_negative_bezout_divisor_equationfirstoutputimaginary. (((((ge_representation_imaginary_code_bezout_divisor_equationfirstoutput) = 2 * (ge_balance_positive_bezout_divisor_equationfirstoutputimaginary) /\ (ge_balance_negative_bezout_divisor_equationfirstoutputimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_equationfirstoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_equationfirstoutput) = 2 * ge_signed_half_bezout_divisor_equationfirstoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_equationfirstoutputimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_equationfirstoutputimaginary) = S ge_signed_half_bezout_divisor_equationfirstoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_divisor_equationfirst) * (ge_second_ip_bezout_divisor_equationfirst))) + (((ge_first_rn_bezout_divisor_equationfirst) * (ge_second_in_bezout_divisor_equationfirst))))) + (((((ge_first_ip_bezout_divisor_equationfirst) * (ge_second_rp_bezout_divisor_equationfirst))) + (((ge_first_in_bezout_divisor_equationfirst) * (ge_second_rn_bezout_divisor_equationfirst))))))) + ge_balance_negative_bezout_divisor_equationfirstoutputimaginary = (((((((ge_first_rp_bezout_divisor_equationfirst) * (ge_second_in_bezout_divisor_equationfirst))) + (((ge_first_rn_bezout_divisor_equationfirst) * (ge_second_ip_bezout_divisor_equationfirst))))) + (((((ge_first_ip_bezout_divisor_equationfirst) * (ge_second_rn_bezout_divisor_equationfirst))) + (((ge_first_in_bezout_divisor_equationfirst) * (ge_second_rp_bezout_divisor_equationfirst))))))) + ge_balance_positive_bezout_divisor_equationfirstoutputimaginary))))))))) /\ ((exists ge_first_rp_bezout_divisor_equationsecond ge_first_rn_bezout_divisor_equationsecond ge_first_ip_bezout_divisor_equationsecond ge_first_in_bezout_divisor_equationsecond ge_second_rp_bezout_divisor_equationsecond ge_second_rn_bezout_divisor_equationsecond ge_second_ip_bezout_divisor_equationsecond ge_second_in_bezout_divisor_equationsecond. ((exists ge_representation_real_code_bezout_divisor_equationsecondfirst ge_representation_imaginary_code_bezout_divisor_equationsecondfirst. (((b) = ((ge_representation_real_code_bezout_divisor_equationsecondfirst) + (ge_representation_imaginary_code_bezout_divisor_equationsecondfirst)) * S ((ge_representation_real_code_bezout_divisor_equationsecondfirst) + (ge_representation_imaginary_code_bezout_divisor_equationsecondfirst)) + ((ge_representation_imaginary_code_bezout_divisor_equationsecondfirst) + (ge_representation_imaginary_code_bezout_divisor_equationsecondfirst))) /\ ((exists ge_balance_positive_bezout_divisor_equationsecondfirstreal ge_balance_negative_bezout_divisor_equationsecondfirstreal. (((((ge_representation_real_code_bezout_divisor_equationsecondfirst) = 2 * (ge_balance_positive_bezout_divisor_equationsecondfirstreal) /\ (ge_balance_negative_bezout_divisor_equationsecondfirstreal) = 0) \/ exists ge_signed_half_bezout_divisor_equationsecondfirstrealdecode. (((ge_representation_real_code_bezout_divisor_equationsecondfirst) = 2 * ge_signed_half_bezout_divisor_equationsecondfirstrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsecondfirstreal) = 0) /\ (ge_balance_negative_bezout_divisor_equationsecondfirstreal) = S ge_signed_half_bezout_divisor_equationsecondfirstrealdecode))) /\ ((ge_first_rp_bezout_divisor_equationsecond) + ge_balance_negative_bezout_divisor_equationsecondfirstreal = (ge_first_rn_bezout_divisor_equationsecond) + ge_balance_positive_bezout_divisor_equationsecondfirstreal))) /\ (exists ge_balance_positive_bezout_divisor_equationsecondfirstimaginary ge_balance_negative_bezout_divisor_equationsecondfirstimaginary. (((((ge_representation_imaginary_code_bezout_divisor_equationsecondfirst) = 2 * (ge_balance_positive_bezout_divisor_equationsecondfirstimaginary) /\ (ge_balance_negative_bezout_divisor_equationsecondfirstimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_equationsecondfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_equationsecondfirst) = 2 * ge_signed_half_bezout_divisor_equationsecondfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsecondfirstimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_equationsecondfirstimaginary) = S ge_signed_half_bezout_divisor_equationsecondfirstimaginarydecode))) /\ ((ge_first_ip_bezout_divisor_equationsecond) + ge_balance_negative_bezout_divisor_equationsecondfirstimaginary = (ge_first_in_bezout_divisor_equationsecond) + ge_balance_positive_bezout_divisor_equationsecondfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_divisor_equationsecondsecond ge_representation_imaginary_code_bezout_divisor_equationsecondsecond. (((v) = ((ge_representation_real_code_bezout_divisor_equationsecondsecond) + (ge_representation_imaginary_code_bezout_divisor_equationsecondsecond)) * S ((ge_representation_real_code_bezout_divisor_equationsecondsecond) + (ge_representation_imaginary_code_bezout_divisor_equationsecondsecond)) + ((ge_representation_imaginary_code_bezout_divisor_equationsecondsecond) + (ge_representation_imaginary_code_bezout_divisor_equationsecondsecond))) /\ ((exists ge_balance_positive_bezout_divisor_equationsecondsecondreal ge_balance_negative_bezout_divisor_equationsecondsecondreal. (((((ge_representation_real_code_bezout_divisor_equationsecondsecond) = 2 * (ge_balance_positive_bezout_divisor_equationsecondsecondreal) /\ (ge_balance_negative_bezout_divisor_equationsecondsecondreal) = 0) \/ exists ge_signed_half_bezout_divisor_equationsecondsecondrealdecode. (((ge_representation_real_code_bezout_divisor_equationsecondsecond) = 2 * ge_signed_half_bezout_divisor_equationsecondsecondrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsecondsecondreal) = 0) /\ (ge_balance_negative_bezout_divisor_equationsecondsecondreal) = S ge_signed_half_bezout_divisor_equationsecondsecondrealdecode))) /\ ((ge_second_rp_bezout_divisor_equationsecond) + ge_balance_negative_bezout_divisor_equationsecondsecondreal = (ge_second_rn_bezout_divisor_equationsecond) + ge_balance_positive_bezout_divisor_equationsecondsecondreal))) /\ (exists ge_balance_positive_bezout_divisor_equationsecondsecondimaginary ge_balance_negative_bezout_divisor_equationsecondsecondimaginary. (((((ge_representation_imaginary_code_bezout_divisor_equationsecondsecond) = 2 * (ge_balance_positive_bezout_divisor_equationsecondsecondimaginary) /\ (ge_balance_negative_bezout_divisor_equationsecondsecondimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_equationsecondsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_equationsecondsecond) = 2 * ge_signed_half_bezout_divisor_equationsecondsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsecondsecondimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_equationsecondsecondimaginary) = S ge_signed_half_bezout_divisor_equationsecondsecondimaginarydecode))) /\ ((ge_second_ip_bezout_divisor_equationsecond) + ge_balance_negative_bezout_divisor_equationsecondsecondimaginary = (ge_second_in_bezout_divisor_equationsecond) + ge_balance_positive_bezout_divisor_equationsecondsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_divisor_equationsecondoutput ge_representation_imaginary_code_bezout_divisor_equationsecondoutput. (((gr_second_product_bezout_divisor_equation) = ((ge_representation_real_code_bezout_divisor_equationsecondoutput) + (ge_representation_imaginary_code_bezout_divisor_equationsecondoutput)) * S ((ge_representation_real_code_bezout_divisor_equationsecondoutput) + (ge_representation_imaginary_code_bezout_divisor_equationsecondoutput)) + ((ge_representation_imaginary_code_bezout_divisor_equationsecondoutput) + (ge_representation_imaginary_code_bezout_divisor_equationsecondoutput))) /\ ((exists ge_balance_positive_bezout_divisor_equationsecondoutputreal ge_balance_negative_bezout_divisor_equationsecondoutputreal. (((((ge_representation_real_code_bezout_divisor_equationsecondoutput) = 2 * (ge_balance_positive_bezout_divisor_equationsecondoutputreal) /\ (ge_balance_negative_bezout_divisor_equationsecondoutputreal) = 0) \/ exists ge_signed_half_bezout_divisor_equationsecondoutputrealdecode. (((ge_representation_real_code_bezout_divisor_equationsecondoutput) = 2 * ge_signed_half_bezout_divisor_equationsecondoutputrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsecondoutputreal) = 0) /\ (ge_balance_negative_bezout_divisor_equationsecondoutputreal) = S ge_signed_half_bezout_divisor_equationsecondoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_divisor_equationsecond) * (ge_second_rp_bezout_divisor_equationsecond))) + (((ge_first_rn_bezout_divisor_equationsecond) * (ge_second_rn_bezout_divisor_equationsecond))))) + (((((ge_first_ip_bezout_divisor_equationsecond) * (ge_second_in_bezout_divisor_equationsecond))) + (((ge_first_in_bezout_divisor_equationsecond) * (ge_second_ip_bezout_divisor_equationsecond))))))) + ge_balance_negative_bezout_divisor_equationsecondoutputreal = (((((((ge_first_rp_bezout_divisor_equationsecond) * (ge_second_rn_bezout_divisor_equationsecond))) + (((ge_first_rn_bezout_divisor_equationsecond) * (ge_second_rp_bezout_divisor_equationsecond))))) + (((((ge_first_ip_bezout_divisor_equationsecond) * (ge_second_ip_bezout_divisor_equationsecond))) + (((ge_first_in_bezout_divisor_equationsecond) * (ge_second_in_bezout_divisor_equationsecond))))))) + ge_balance_positive_bezout_divisor_equationsecondoutputreal))) /\ (exists ge_balance_positive_bezout_divisor_equationsecondoutputimaginary ge_balance_negative_bezout_divisor_equationsecondoutputimaginary. (((((ge_representation_imaginary_code_bezout_divisor_equationsecondoutput) = 2 * (ge_balance_positive_bezout_divisor_equationsecondoutputimaginary) /\ (ge_balance_negative_bezout_divisor_equationsecondoutputimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_equationsecondoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_equationsecondoutput) = 2 * ge_signed_half_bezout_divisor_equationsecondoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsecondoutputimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_equationsecondoutputimaginary) = S ge_signed_half_bezout_divisor_equationsecondoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_divisor_equationsecond) * (ge_second_ip_bezout_divisor_equationsecond))) + (((ge_first_rn_bezout_divisor_equationsecond) * (ge_second_in_bezout_divisor_equationsecond))))) + (((((ge_first_ip_bezout_divisor_equationsecond) * (ge_second_rp_bezout_divisor_equationsecond))) + (((ge_first_in_bezout_divisor_equationsecond) * (ge_second_rn_bezout_divisor_equationsecond))))))) + ge_balance_negative_bezout_divisor_equationsecondoutputimaginary = (((((((ge_first_rp_bezout_divisor_equationsecond) * (ge_second_in_bezout_divisor_equationsecond))) + (((ge_first_rn_bezout_divisor_equationsecond) * (ge_second_ip_bezout_divisor_equationsecond))))) + (((((ge_first_ip_bezout_divisor_equationsecond) * (ge_second_rn_bezout_divisor_equationsecond))) + (((ge_first_in_bezout_divisor_equationsecond) * (ge_second_rp_bezout_divisor_equationsecond))))))) + ge_balance_positive_bezout_divisor_equationsecondoutputimaginary))))))))) /\ (exists ge_first_rp_bezout_divisor_equationsum ge_first_rn_bezout_divisor_equationsum ge_first_ip_bezout_divisor_equationsum ge_first_in_bezout_divisor_equationsum ge_second_rp_bezout_divisor_equationsum ge_second_rn_bezout_divisor_equationsum ge_second_ip_bezout_divisor_equationsum ge_second_in_bezout_divisor_equationsum. ((exists ge_representation_real_code_bezout_divisor_equationsumfirst ge_representation_imaginary_code_bezout_divisor_equationsumfirst. (((gr_first_product_bezout_divisor_equation) = ((ge_representation_real_code_bezout_divisor_equationsumfirst) + (ge_representation_imaginary_code_bezout_divisor_equationsumfirst)) * S ((ge_representation_real_code_bezout_divisor_equationsumfirst) + (ge_representation_imaginary_code_bezout_divisor_equationsumfirst)) + ((ge_representation_imaginary_code_bezout_divisor_equationsumfirst) + (ge_representation_imaginary_code_bezout_divisor_equationsumfirst))) /\ ((exists ge_balance_positive_bezout_divisor_equationsumfirstreal ge_balance_negative_bezout_divisor_equationsumfirstreal. (((((ge_representation_real_code_bezout_divisor_equationsumfirst) = 2 * (ge_balance_positive_bezout_divisor_equationsumfirstreal) /\ (ge_balance_negative_bezout_divisor_equationsumfirstreal) = 0) \/ exists ge_signed_half_bezout_divisor_equationsumfirstrealdecode. (((ge_representation_real_code_bezout_divisor_equationsumfirst) = 2 * ge_signed_half_bezout_divisor_equationsumfirstrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsumfirstreal) = 0) /\ (ge_balance_negative_bezout_divisor_equationsumfirstreal) = S ge_signed_half_bezout_divisor_equationsumfirstrealdecode))) /\ ((ge_first_rp_bezout_divisor_equationsum) + ge_balance_negative_bezout_divisor_equationsumfirstreal = (ge_first_rn_bezout_divisor_equationsum) + ge_balance_positive_bezout_divisor_equationsumfirstreal))) /\ (exists ge_balance_positive_bezout_divisor_equationsumfirstimaginary ge_balance_negative_bezout_divisor_equationsumfirstimaginary. (((((ge_representation_imaginary_code_bezout_divisor_equationsumfirst) = 2 * (ge_balance_positive_bezout_divisor_equationsumfirstimaginary) /\ (ge_balance_negative_bezout_divisor_equationsumfirstimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_equationsumfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_equationsumfirst) = 2 * ge_signed_half_bezout_divisor_equationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsumfirstimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_equationsumfirstimaginary) = S ge_signed_half_bezout_divisor_equationsumfirstimaginarydecode))) /\ ((ge_first_ip_bezout_divisor_equationsum) + ge_balance_negative_bezout_divisor_equationsumfirstimaginary = (ge_first_in_bezout_divisor_equationsum) + ge_balance_positive_bezout_divisor_equationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_divisor_equationsumsecond ge_representation_imaginary_code_bezout_divisor_equationsumsecond. (((gr_second_product_bezout_divisor_equation) = ((ge_representation_real_code_bezout_divisor_equationsumsecond) + (ge_representation_imaginary_code_bezout_divisor_equationsumsecond)) * S ((ge_representation_real_code_bezout_divisor_equationsumsecond) + (ge_representation_imaginary_code_bezout_divisor_equationsumsecond)) + ((ge_representation_imaginary_code_bezout_divisor_equationsumsecond) + (ge_representation_imaginary_code_bezout_divisor_equationsumsecond))) /\ ((exists ge_balance_positive_bezout_divisor_equationsumsecondreal ge_balance_negative_bezout_divisor_equationsumsecondreal. (((((ge_representation_real_code_bezout_divisor_equationsumsecond) = 2 * (ge_balance_positive_bezout_divisor_equationsumsecondreal) /\ (ge_balance_negative_bezout_divisor_equationsumsecondreal) = 0) \/ exists ge_signed_half_bezout_divisor_equationsumsecondrealdecode. (((ge_representation_real_code_bezout_divisor_equationsumsecond) = 2 * ge_signed_half_bezout_divisor_equationsumsecondrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsumsecondreal) = 0) /\ (ge_balance_negative_bezout_divisor_equationsumsecondreal) = S ge_signed_half_bezout_divisor_equationsumsecondrealdecode))) /\ ((ge_second_rp_bezout_divisor_equationsum) + ge_balance_negative_bezout_divisor_equationsumsecondreal = (ge_second_rn_bezout_divisor_equationsum) + ge_balance_positive_bezout_divisor_equationsumsecondreal))) /\ (exists ge_balance_positive_bezout_divisor_equationsumsecondimaginary ge_balance_negative_bezout_divisor_equationsumsecondimaginary. (((((ge_representation_imaginary_code_bezout_divisor_equationsumsecond) = 2 * (ge_balance_positive_bezout_divisor_equationsumsecondimaginary) /\ (ge_balance_negative_bezout_divisor_equationsumsecondimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_equationsumsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_equationsumsecond) = 2 * ge_signed_half_bezout_divisor_equationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsumsecondimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_equationsumsecondimaginary) = S ge_signed_half_bezout_divisor_equationsumsecondimaginarydecode))) /\ ((ge_second_ip_bezout_divisor_equationsum) + ge_balance_negative_bezout_divisor_equationsumsecondimaginary = (ge_second_in_bezout_divisor_equationsum) + ge_balance_positive_bezout_divisor_equationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_divisor_equationsumoutput ge_representation_imaginary_code_bezout_divisor_equationsumoutput. (((g) = ((ge_representation_real_code_bezout_divisor_equationsumoutput) + (ge_representation_imaginary_code_bezout_divisor_equationsumoutput)) * S ((ge_representation_real_code_bezout_divisor_equationsumoutput) + (ge_representation_imaginary_code_bezout_divisor_equationsumoutput)) + ((ge_representation_imaginary_code_bezout_divisor_equationsumoutput) + (ge_representation_imaginary_code_bezout_divisor_equationsumoutput))) /\ ((exists ge_balance_positive_bezout_divisor_equationsumoutputreal ge_balance_negative_bezout_divisor_equationsumoutputreal. (((((ge_representation_real_code_bezout_divisor_equationsumoutput) = 2 * (ge_balance_positive_bezout_divisor_equationsumoutputreal) /\ (ge_balance_negative_bezout_divisor_equationsumoutputreal) = 0) \/ exists ge_signed_half_bezout_divisor_equationsumoutputrealdecode. (((ge_representation_real_code_bezout_divisor_equationsumoutput) = 2 * ge_signed_half_bezout_divisor_equationsumoutputrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsumoutputreal) = 0) /\ (ge_balance_negative_bezout_divisor_equationsumoutputreal) = S ge_signed_half_bezout_divisor_equationsumoutputrealdecode))) /\ ((((ge_first_rp_bezout_divisor_equationsum) + (ge_second_rp_bezout_divisor_equationsum))) + ge_balance_negative_bezout_divisor_equationsumoutputreal = (((ge_first_rn_bezout_divisor_equationsum) + (ge_second_rn_bezout_divisor_equationsum))) + ge_balance_positive_bezout_divisor_equationsumoutputreal))) /\ (exists ge_balance_positive_bezout_divisor_equationsumoutputimaginary ge_balance_negative_bezout_divisor_equationsumoutputimaginary. (((((ge_representation_imaginary_code_bezout_divisor_equationsumoutput) = 2 * (ge_balance_positive_bezout_divisor_equationsumoutputimaginary) /\ (ge_balance_negative_bezout_divisor_equationsumoutputimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_equationsumoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_equationsumoutput) = 2 * ge_signed_half_bezout_divisor_equationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_equationsumoutputimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_equationsumoutputimaginary) = S ge_signed_half_bezout_divisor_equationsumoutputimaginarydecode))) /\ ((((ge_first_ip_bezout_divisor_equationsum) + (ge_second_ip_bezout_divisor_equationsum))) + ge_balance_negative_bezout_divisor_equationsumoutputimaginary = (((ge_first_in_bezout_divisor_equationsum) + (ge_second_in_bezout_divisor_equationsum))) + ge_balance_positive_bezout_divisor_equationsumoutputimaginary)))))))))))) -> (exists gr_quotient_bezout_divisor_result. (exists ge_first_rp_bezout_divisor_resultproduct ge_first_rn_bezout_divisor_resultproduct ge_first_ip_bezout_divisor_resultproduct ge_first_in_bezout_divisor_resultproduct ge_second_rp_bezout_divisor_resultproduct ge_second_rn_bezout_divisor_resultproduct ge_second_ip_bezout_divisor_resultproduct ge_second_in_bezout_divisor_resultproduct. ((exists ge_representation_real_code_bezout_divisor_resultproductfirst ge_representation_imaginary_code_bezout_divisor_resultproductfirst. (((d) = ((ge_representation_real_code_bezout_divisor_resultproductfirst) + (ge_representation_imaginary_code_bezout_divisor_resultproductfirst)) * S ((ge_representation_real_code_bezout_divisor_resultproductfirst) + (ge_representation_imaginary_code_bezout_divisor_resultproductfirst)) + ((ge_representation_imaginary_code_bezout_divisor_resultproductfirst) + (ge_representation_imaginary_code_bezout_divisor_resultproductfirst))) /\ ((exists ge_balance_positive_bezout_divisor_resultproductfirstreal ge_balance_negative_bezout_divisor_resultproductfirstreal. (((((ge_representation_real_code_bezout_divisor_resultproductfirst) = 2 * (ge_balance_positive_bezout_divisor_resultproductfirstreal) /\ (ge_balance_negative_bezout_divisor_resultproductfirstreal) = 0) \/ exists ge_signed_half_bezout_divisor_resultproductfirstrealdecode. (((ge_representation_real_code_bezout_divisor_resultproductfirst) = 2 * ge_signed_half_bezout_divisor_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_resultproductfirstreal) = 0) /\ (ge_balance_negative_bezout_divisor_resultproductfirstreal) = S ge_signed_half_bezout_divisor_resultproductfirstrealdecode))) /\ ((ge_first_rp_bezout_divisor_resultproduct) + ge_balance_negative_bezout_divisor_resultproductfirstreal = (ge_first_rn_bezout_divisor_resultproduct) + ge_balance_positive_bezout_divisor_resultproductfirstreal))) /\ (exists ge_balance_positive_bezout_divisor_resultproductfirstimaginary ge_balance_negative_bezout_divisor_resultproductfirstimaginary. (((((ge_representation_imaginary_code_bezout_divisor_resultproductfirst) = 2 * (ge_balance_positive_bezout_divisor_resultproductfirstimaginary) /\ (ge_balance_negative_bezout_divisor_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_resultproductfirst) = 2 * ge_signed_half_bezout_divisor_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_resultproductfirstimaginary) = S ge_signed_half_bezout_divisor_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_bezout_divisor_resultproduct) + ge_balance_negative_bezout_divisor_resultproductfirstimaginary = (ge_first_in_bezout_divisor_resultproduct) + ge_balance_positive_bezout_divisor_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_divisor_resultproductsecond ge_representation_imaginary_code_bezout_divisor_resultproductsecond. (((gr_quotient_bezout_divisor_result) = ((ge_representation_real_code_bezout_divisor_resultproductsecond) + (ge_representation_imaginary_code_bezout_divisor_resultproductsecond)) * S ((ge_representation_real_code_bezout_divisor_resultproductsecond) + (ge_representation_imaginary_code_bezout_divisor_resultproductsecond)) + ((ge_representation_imaginary_code_bezout_divisor_resultproductsecond) + (ge_representation_imaginary_code_bezout_divisor_resultproductsecond))) /\ ((exists ge_balance_positive_bezout_divisor_resultproductsecondreal ge_balance_negative_bezout_divisor_resultproductsecondreal. (((((ge_representation_real_code_bezout_divisor_resultproductsecond) = 2 * (ge_balance_positive_bezout_divisor_resultproductsecondreal) /\ (ge_balance_negative_bezout_divisor_resultproductsecondreal) = 0) \/ exists ge_signed_half_bezout_divisor_resultproductsecondrealdecode. (((ge_representation_real_code_bezout_divisor_resultproductsecond) = 2 * ge_signed_half_bezout_divisor_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_resultproductsecondreal) = 0) /\ (ge_balance_negative_bezout_divisor_resultproductsecondreal) = S ge_signed_half_bezout_divisor_resultproductsecondrealdecode))) /\ ((ge_second_rp_bezout_divisor_resultproduct) + ge_balance_negative_bezout_divisor_resultproductsecondreal = (ge_second_rn_bezout_divisor_resultproduct) + ge_balance_positive_bezout_divisor_resultproductsecondreal))) /\ (exists ge_balance_positive_bezout_divisor_resultproductsecondimaginary ge_balance_negative_bezout_divisor_resultproductsecondimaginary. (((((ge_representation_imaginary_code_bezout_divisor_resultproductsecond) = 2 * (ge_balance_positive_bezout_divisor_resultproductsecondimaginary) /\ (ge_balance_negative_bezout_divisor_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_resultproductsecond) = 2 * ge_signed_half_bezout_divisor_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_resultproductsecondimaginary) = S ge_signed_half_bezout_divisor_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_bezout_divisor_resultproduct) + ge_balance_negative_bezout_divisor_resultproductsecondimaginary = (ge_second_in_bezout_divisor_resultproduct) + ge_balance_positive_bezout_divisor_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_divisor_resultproductoutput ge_representation_imaginary_code_bezout_divisor_resultproductoutput. (((g) = ((ge_representation_real_code_bezout_divisor_resultproductoutput) + (ge_representation_imaginary_code_bezout_divisor_resultproductoutput)) * S ((ge_representation_real_code_bezout_divisor_resultproductoutput) + (ge_representation_imaginary_code_bezout_divisor_resultproductoutput)) + ((ge_representation_imaginary_code_bezout_divisor_resultproductoutput) + (ge_representation_imaginary_code_bezout_divisor_resultproductoutput))) /\ ((exists ge_balance_positive_bezout_divisor_resultproductoutputreal ge_balance_negative_bezout_divisor_resultproductoutputreal. (((((ge_representation_real_code_bezout_divisor_resultproductoutput) = 2 * (ge_balance_positive_bezout_divisor_resultproductoutputreal) /\ (ge_balance_negative_bezout_divisor_resultproductoutputreal) = 0) \/ exists ge_signed_half_bezout_divisor_resultproductoutputrealdecode. (((ge_representation_real_code_bezout_divisor_resultproductoutput) = 2 * ge_signed_half_bezout_divisor_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_bezout_divisor_resultproductoutputreal) = 0) /\ (ge_balance_negative_bezout_divisor_resultproductoutputreal) = S ge_signed_half_bezout_divisor_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_divisor_resultproduct) * (ge_second_rp_bezout_divisor_resultproduct))) + (((ge_first_rn_bezout_divisor_resultproduct) * (ge_second_rn_bezout_divisor_resultproduct))))) + (((((ge_first_ip_bezout_divisor_resultproduct) * (ge_second_in_bezout_divisor_resultproduct))) + (((ge_first_in_bezout_divisor_resultproduct) * (ge_second_ip_bezout_divisor_resultproduct))))))) + ge_balance_negative_bezout_divisor_resultproductoutputreal = (((((((ge_first_rp_bezout_divisor_resultproduct) * (ge_second_rn_bezout_divisor_resultproduct))) + (((ge_first_rn_bezout_divisor_resultproduct) * (ge_second_rp_bezout_divisor_resultproduct))))) + (((((ge_first_ip_bezout_divisor_resultproduct) * (ge_second_ip_bezout_divisor_resultproduct))) + (((ge_first_in_bezout_divisor_resultproduct) * (ge_second_in_bezout_divisor_resultproduct))))))) + ge_balance_positive_bezout_divisor_resultproductoutputreal))) /\ (exists ge_balance_positive_bezout_divisor_resultproductoutputimaginary ge_balance_negative_bezout_divisor_resultproductoutputimaginary. (((((ge_representation_imaginary_code_bezout_divisor_resultproductoutput) = 2 * (ge_balance_positive_bezout_divisor_resultproductoutputimaginary) /\ (ge_balance_negative_bezout_divisor_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_bezout_divisor_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_divisor_resultproductoutput) = 2 * ge_signed_half_bezout_divisor_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_divisor_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_bezout_divisor_resultproductoutputimaginary) = S ge_signed_half_bezout_divisor_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_divisor_resultproduct) * (ge_second_ip_bezout_divisor_resultproduct))) + (((ge_first_rn_bezout_divisor_resultproduct) * (ge_second_in_bezout_divisor_resultproduct))))) + (((((ge_first_ip_bezout_divisor_resultproduct) * (ge_second_rp_bezout_divisor_resultproduct))) + (((ge_first_in_bezout_divisor_resultproduct) * (ge_second_rn_bezout_divisor_resultproduct))))))) + ge_balance_negative_bezout_divisor_resultproductoutputimaginary = (((((((ge_first_rp_bezout_divisor_resultproduct) * (ge_second_in_bezout_divisor_resultproduct))) + (((ge_first_rn_bezout_divisor_resultproduct) * (ge_second_ip_bezout_divisor_resultproduct))))) + (((((ge_first_ip_bezout_divisor_resultproduct) * (ge_second_rn_bezout_divisor_resultproduct))) + (((ge_first_in_bezout_divisor_resultproduct) * (ge_second_rp_bezout_divisor_resultproduct))))))) + ge_balance_positive_bezout_divisor_resultproductoutputimaginary))))))))))