gaussian_bezout_euclidean_backward

Exact expanded first-order arithmetic statement

forall g a b q r u v. (exists ge_division_product_bezout_euclidean_equation. ((exists ge_first_rp_bezout_euclidean_equationproduct ge_first_rn_bezout_euclidean_equationproduct ge_first_ip_bezout_euclidean_equationproduct ge_first_in_bezout_euclidean_equationproduct ge_second_rp_bezout_euclidean_equationproduct ge_second_rn_bezout_euclidean_equationproduct ge_second_ip_bezout_euclidean_equationproduct ge_second_in_bezout_euclidean_equationproduct. ((exists ge_representation_real_code_bezout_euclidean_equationproductfirst ge_representation_imaginary_code_bezout_euclidean_equationproductfirst. (((b) = ((ge_representation_real_code_bezout_euclidean_equationproductfirst) + (ge_representation_imaginary_code_bezout_euclidean_equationproductfirst)) * S ((ge_representation_real_code_bezout_euclidean_equationproductfirst) + (ge_representation_imaginary_code_bezout_euclidean_equationproductfirst)) + ((ge_representation_imaginary_code_bezout_euclidean_equationproductfirst) + (ge_representation_imaginary_code_bezout_euclidean_equationproductfirst))) /\ ((exists ge_balance_positive_bezout_euclidean_equationproductfirstreal ge_balance_negative_bezout_euclidean_equationproductfirstreal. (((((ge_representation_real_code_bezout_euclidean_equationproductfirst) = 2 * (ge_balance_positive_bezout_euclidean_equationproductfirstreal) /\ (ge_balance_negative_bezout_euclidean_equationproductfirstreal) = 0) \/ exists ge_signed_half_bezout_euclidean_equationproductfirstrealdecode. (((ge_representation_real_code_bezout_euclidean_equationproductfirst) = 2 * ge_signed_half_bezout_euclidean_equationproductfirstrealdecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationproductfirstreal) = 0) /\ (ge_balance_negative_bezout_euclidean_equationproductfirstreal) = S ge_signed_half_bezout_euclidean_equationproductfirstrealdecode))) /\ ((ge_first_rp_bezout_euclidean_equationproduct) + ge_balance_negative_bezout_euclidean_equationproductfirstreal = (ge_first_rn_bezout_euclidean_equationproduct) + ge_balance_positive_bezout_euclidean_equationproductfirstreal))) /\ (exists ge_balance_positive_bezout_euclidean_equationproductfirstimaginary ge_balance_negative_bezout_euclidean_equationproductfirstimaginary. (((((ge_representation_imaginary_code_bezout_euclidean_equationproductfirst) = 2 * (ge_balance_positive_bezout_euclidean_equationproductfirstimaginary) /\ (ge_balance_negative_bezout_euclidean_equationproductfirstimaginary) = 0) \/ exists ge_signed_half_bezout_euclidean_equationproductfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_euclidean_equationproductfirst) = 2 * ge_signed_half_bezout_euclidean_equationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationproductfirstimaginary) = 0) /\ (ge_balance_negative_bezout_euclidean_equationproductfirstimaginary) = S ge_signed_half_bezout_euclidean_equationproductfirstimaginarydecode))) /\ ((ge_first_ip_bezout_euclidean_equationproduct) + ge_balance_negative_bezout_euclidean_equationproductfirstimaginary = (ge_first_in_bezout_euclidean_equationproduct) + ge_balance_positive_bezout_euclidean_equationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_euclidean_equationproductsecond ge_representation_imaginary_code_bezout_euclidean_equationproductsecond. (((q) = ((ge_representation_real_code_bezout_euclidean_equationproductsecond) + (ge_representation_imaginary_code_bezout_euclidean_equationproductsecond)) * S ((ge_representation_real_code_bezout_euclidean_equationproductsecond) + (ge_representation_imaginary_code_bezout_euclidean_equationproductsecond)) + ((ge_representation_imaginary_code_bezout_euclidean_equationproductsecond) + (ge_representation_imaginary_code_bezout_euclidean_equationproductsecond))) /\ ((exists ge_balance_positive_bezout_euclidean_equationproductsecondreal ge_balance_negative_bezout_euclidean_equationproductsecondreal. (((((ge_representation_real_code_bezout_euclidean_equationproductsecond) = 2 * (ge_balance_positive_bezout_euclidean_equationproductsecondreal) /\ (ge_balance_negative_bezout_euclidean_equationproductsecondreal) = 0) \/ exists ge_signed_half_bezout_euclidean_equationproductsecondrealdecode. (((ge_representation_real_code_bezout_euclidean_equationproductsecond) = 2 * ge_signed_half_bezout_euclidean_equationproductsecondrealdecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationproductsecondreal) = 0) /\ (ge_balance_negative_bezout_euclidean_equationproductsecondreal) = S ge_signed_half_bezout_euclidean_equationproductsecondrealdecode))) /\ ((ge_second_rp_bezout_euclidean_equationproduct) + ge_balance_negative_bezout_euclidean_equationproductsecondreal = (ge_second_rn_bezout_euclidean_equationproduct) + ge_balance_positive_bezout_euclidean_equationproductsecondreal))) /\ (exists ge_balance_positive_bezout_euclidean_equationproductsecondimaginary ge_balance_negative_bezout_euclidean_equationproductsecondimaginary. (((((ge_representation_imaginary_code_bezout_euclidean_equationproductsecond) = 2 * (ge_balance_positive_bezout_euclidean_equationproductsecondimaginary) /\ (ge_balance_negative_bezout_euclidean_equationproductsecondimaginary) = 0) \/ exists ge_signed_half_bezout_euclidean_equationproductsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_euclidean_equationproductsecond) = 2 * ge_signed_half_bezout_euclidean_equationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationproductsecondimaginary) = 0) /\ (ge_balance_negative_bezout_euclidean_equationproductsecondimaginary) = S ge_signed_half_bezout_euclidean_equationproductsecondimaginarydecode))) /\ ((ge_second_ip_bezout_euclidean_equationproduct) + ge_balance_negative_bezout_euclidean_equationproductsecondimaginary = (ge_second_in_bezout_euclidean_equationproduct) + ge_balance_positive_bezout_euclidean_equationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_euclidean_equationproductoutput ge_representation_imaginary_code_bezout_euclidean_equationproductoutput. (((ge_division_product_bezout_euclidean_equation) = ((ge_representation_real_code_bezout_euclidean_equationproductoutput) + (ge_representation_imaginary_code_bezout_euclidean_equationproductoutput)) * S ((ge_representation_real_code_bezout_euclidean_equationproductoutput) + (ge_representation_imaginary_code_bezout_euclidean_equationproductoutput)) + ((ge_representation_imaginary_code_bezout_euclidean_equationproductoutput) + (ge_representation_imaginary_code_bezout_euclidean_equationproductoutput))) /\ ((exists ge_balance_positive_bezout_euclidean_equationproductoutputreal ge_balance_negative_bezout_euclidean_equationproductoutputreal. (((((ge_representation_real_code_bezout_euclidean_equationproductoutput) = 2 * (ge_balance_positive_bezout_euclidean_equationproductoutputreal) /\ (ge_balance_negative_bezout_euclidean_equationproductoutputreal) = 0) \/ exists ge_signed_half_bezout_euclidean_equationproductoutputrealdecode. (((ge_representation_real_code_bezout_euclidean_equationproductoutput) = 2 * ge_signed_half_bezout_euclidean_equationproductoutputrealdecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationproductoutputreal) = 0) /\ (ge_balance_negative_bezout_euclidean_equationproductoutputreal) = S ge_signed_half_bezout_euclidean_equationproductoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_euclidean_equationproduct) * (ge_second_rp_bezout_euclidean_equationproduct))) + (((ge_first_rn_bezout_euclidean_equationproduct) * (ge_second_rn_bezout_euclidean_equationproduct))))) + (((((ge_first_ip_bezout_euclidean_equationproduct) * (ge_second_in_bezout_euclidean_equationproduct))) + (((ge_first_in_bezout_euclidean_equationproduct) * (ge_second_ip_bezout_euclidean_equationproduct))))))) + ge_balance_negative_bezout_euclidean_equationproductoutputreal = (((((((ge_first_rp_bezout_euclidean_equationproduct) * (ge_second_rn_bezout_euclidean_equationproduct))) + (((ge_first_rn_bezout_euclidean_equationproduct) * (ge_second_rp_bezout_euclidean_equationproduct))))) + (((((ge_first_ip_bezout_euclidean_equationproduct) * (ge_second_ip_bezout_euclidean_equationproduct))) + (((ge_first_in_bezout_euclidean_equationproduct) * (ge_second_in_bezout_euclidean_equationproduct))))))) + ge_balance_positive_bezout_euclidean_equationproductoutputreal))) /\ (exists ge_balance_positive_bezout_euclidean_equationproductoutputimaginary ge_balance_negative_bezout_euclidean_equationproductoutputimaginary. (((((ge_representation_imaginary_code_bezout_euclidean_equationproductoutput) = 2 * (ge_balance_positive_bezout_euclidean_equationproductoutputimaginary) /\ (ge_balance_negative_bezout_euclidean_equationproductoutputimaginary) = 0) \/ exists ge_signed_half_bezout_euclidean_equationproductoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_euclidean_equationproductoutput) = 2 * ge_signed_half_bezout_euclidean_equationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationproductoutputimaginary) = 0) /\ (ge_balance_negative_bezout_euclidean_equationproductoutputimaginary) = S ge_signed_half_bezout_euclidean_equationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_euclidean_equationproduct) * (ge_second_ip_bezout_euclidean_equationproduct))) + (((ge_first_rn_bezout_euclidean_equationproduct) * (ge_second_in_bezout_euclidean_equationproduct))))) + (((((ge_first_ip_bezout_euclidean_equationproduct) * (ge_second_rp_bezout_euclidean_equationproduct))) + (((ge_first_in_bezout_euclidean_equationproduct) * (ge_second_rn_bezout_euclidean_equationproduct))))))) + ge_balance_negative_bezout_euclidean_equationproductoutputimaginary = (((((((ge_first_rp_bezout_euclidean_equationproduct) * (ge_second_in_bezout_euclidean_equationproduct))) + (((ge_first_rn_bezout_euclidean_equationproduct) * (ge_second_ip_bezout_euclidean_equationproduct))))) + (((((ge_first_ip_bezout_euclidean_equationproduct) * (ge_second_rn_bezout_euclidean_equationproduct))) + (((ge_first_in_bezout_euclidean_equationproduct) * (ge_second_rp_bezout_euclidean_equationproduct))))))) + ge_balance_positive_bezout_euclidean_equationproductoutputimaginary))))))))) /\ (exists ge_first_rp_bezout_euclidean_equationsum ge_first_rn_bezout_euclidean_equationsum ge_first_ip_bezout_euclidean_equationsum ge_first_in_bezout_euclidean_equationsum ge_second_rp_bezout_euclidean_equationsum ge_second_rn_bezout_euclidean_equationsum ge_second_ip_bezout_euclidean_equationsum ge_second_in_bezout_euclidean_equationsum. ((exists ge_representation_real_code_bezout_euclidean_equationsumfirst ge_representation_imaginary_code_bezout_euclidean_equationsumfirst. (((ge_division_product_bezout_euclidean_equation) = ((ge_representation_real_code_bezout_euclidean_equationsumfirst) + (ge_representation_imaginary_code_bezout_euclidean_equationsumfirst)) * S ((ge_representation_real_code_bezout_euclidean_equationsumfirst) + (ge_representation_imaginary_code_bezout_euclidean_equationsumfirst)) + ((ge_representation_imaginary_code_bezout_euclidean_equationsumfirst) + (ge_representation_imaginary_code_bezout_euclidean_equationsumfirst))) /\ ((exists ge_balance_positive_bezout_euclidean_equationsumfirstreal ge_balance_negative_bezout_euclidean_equationsumfirstreal. (((((ge_representation_real_code_bezout_euclidean_equationsumfirst) = 2 * (ge_balance_positive_bezout_euclidean_equationsumfirstreal) /\ (ge_balance_negative_bezout_euclidean_equationsumfirstreal) = 0) \/ exists ge_signed_half_bezout_euclidean_equationsumfirstrealdecode. (((ge_representation_real_code_bezout_euclidean_equationsumfirst) = 2 * ge_signed_half_bezout_euclidean_equationsumfirstrealdecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationsumfirstreal) = 0) /\ (ge_balance_negative_bezout_euclidean_equationsumfirstreal) = S ge_signed_half_bezout_euclidean_equationsumfirstrealdecode))) /\ ((ge_first_rp_bezout_euclidean_equationsum) + ge_balance_negative_bezout_euclidean_equationsumfirstreal = (ge_first_rn_bezout_euclidean_equationsum) + ge_balance_positive_bezout_euclidean_equationsumfirstreal))) /\ (exists ge_balance_positive_bezout_euclidean_equationsumfirstimaginary ge_balance_negative_bezout_euclidean_equationsumfirstimaginary. (((((ge_representation_imaginary_code_bezout_euclidean_equationsumfirst) = 2 * (ge_balance_positive_bezout_euclidean_equationsumfirstimaginary) /\ (ge_balance_negative_bezout_euclidean_equationsumfirstimaginary) = 0) \/ exists ge_signed_half_bezout_euclidean_equationsumfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_euclidean_equationsumfirst) = 2 * ge_signed_half_bezout_euclidean_equationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationsumfirstimaginary) = 0) /\ (ge_balance_negative_bezout_euclidean_equationsumfirstimaginary) = S ge_signed_half_bezout_euclidean_equationsumfirstimaginarydecode))) /\ ((ge_first_ip_bezout_euclidean_equationsum) + ge_balance_negative_bezout_euclidean_equationsumfirstimaginary = (ge_first_in_bezout_euclidean_equationsum) + ge_balance_positive_bezout_euclidean_equationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_euclidean_equationsumsecond ge_representation_imaginary_code_bezout_euclidean_equationsumsecond. (((r) = ((ge_representation_real_code_bezout_euclidean_equationsumsecond) + (ge_representation_imaginary_code_bezout_euclidean_equationsumsecond)) * S ((ge_representation_real_code_bezout_euclidean_equationsumsecond) + (ge_representation_imaginary_code_bezout_euclidean_equationsumsecond)) + ((ge_representation_imaginary_code_bezout_euclidean_equationsumsecond) + (ge_representation_imaginary_code_bezout_euclidean_equationsumsecond))) /\ ((exists ge_balance_positive_bezout_euclidean_equationsumsecondreal ge_balance_negative_bezout_euclidean_equationsumsecondreal. (((((ge_representation_real_code_bezout_euclidean_equationsumsecond) = 2 * (ge_balance_positive_bezout_euclidean_equationsumsecondreal) /\ (ge_balance_negative_bezout_euclidean_equationsumsecondreal) = 0) \/ exists ge_signed_half_bezout_euclidean_equationsumsecondrealdecode. (((ge_representation_real_code_bezout_euclidean_equationsumsecond) = 2 * ge_signed_half_bezout_euclidean_equationsumsecondrealdecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationsumsecondreal) = 0) /\ (ge_balance_negative_bezout_euclidean_equationsumsecondreal) = S ge_signed_half_bezout_euclidean_equationsumsecondrealdecode))) /\ ((ge_second_rp_bezout_euclidean_equationsum) + ge_balance_negative_bezout_euclidean_equationsumsecondreal = (ge_second_rn_bezout_euclidean_equationsum) + ge_balance_positive_bezout_euclidean_equationsumsecondreal))) /\ (exists ge_balance_positive_bezout_euclidean_equationsumsecondimaginary ge_balance_negative_bezout_euclidean_equationsumsecondimaginary. (((((ge_representation_imaginary_code_bezout_euclidean_equationsumsecond) = 2 * (ge_balance_positive_bezout_euclidean_equationsumsecondimaginary) /\ (ge_balance_negative_bezout_euclidean_equationsumsecondimaginary) = 0) \/ exists ge_signed_half_bezout_euclidean_equationsumsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_euclidean_equationsumsecond) = 2 * ge_signed_half_bezout_euclidean_equationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationsumsecondimaginary) = 0) /\ (ge_balance_negative_bezout_euclidean_equationsumsecondimaginary) = S ge_signed_half_bezout_euclidean_equationsumsecondimaginarydecode))) /\ ((ge_second_ip_bezout_euclidean_equationsum) + ge_balance_negative_bezout_euclidean_equationsumsecondimaginary = (ge_second_in_bezout_euclidean_equationsum) + ge_balance_positive_bezout_euclidean_equationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_euclidean_equationsumoutput ge_representation_imaginary_code_bezout_euclidean_equationsumoutput. (((a) = ((ge_representation_real_code_bezout_euclidean_equationsumoutput) + (ge_representation_imaginary_code_bezout_euclidean_equationsumoutput)) * S ((ge_representation_real_code_bezout_euclidean_equationsumoutput) + (ge_representation_imaginary_code_bezout_euclidean_equationsumoutput)) + ((ge_representation_imaginary_code_bezout_euclidean_equationsumoutput) + (ge_representation_imaginary_code_bezout_euclidean_equationsumoutput))) /\ ((exists ge_balance_positive_bezout_euclidean_equationsumoutputreal ge_balance_negative_bezout_euclidean_equationsumoutputreal. (((((ge_representation_real_code_bezout_euclidean_equationsumoutput) = 2 * (ge_balance_positive_bezout_euclidean_equationsumoutputreal) /\ (ge_balance_negative_bezout_euclidean_equationsumoutputreal) = 0) \/ exists ge_signed_half_bezout_euclidean_equationsumoutputrealdecode. (((ge_representation_real_code_bezout_euclidean_equationsumoutput) = 2 * ge_signed_half_bezout_euclidean_equationsumoutputrealdecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationsumoutputreal) = 0) /\ (ge_balance_negative_bezout_euclidean_equationsumoutputreal) = S ge_signed_half_bezout_euclidean_equationsumoutputrealdecode))) /\ ((((ge_first_rp_bezout_euclidean_equationsum) + (ge_second_rp_bezout_euclidean_equationsum))) + ge_balance_negative_bezout_euclidean_equationsumoutputreal = (((ge_first_rn_bezout_euclidean_equationsum) + (ge_second_rn_bezout_euclidean_equationsum))) + ge_balance_positive_bezout_euclidean_equationsumoutputreal))) /\ (exists ge_balance_positive_bezout_euclidean_equationsumoutputimaginary ge_balance_negative_bezout_euclidean_equationsumoutputimaginary. (((((ge_representation_imaginary_code_bezout_euclidean_equationsumoutput) = 2 * (ge_balance_positive_bezout_euclidean_equationsumoutputimaginary) /\ (ge_balance_negative_bezout_euclidean_equationsumoutputimaginary) = 0) \/ exists ge_signed_half_bezout_euclidean_equationsumoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_euclidean_equationsumoutput) = 2 * ge_signed_half_bezout_euclidean_equationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_euclidean_equationsumoutputimaginary) = 0) /\ (ge_balance_negative_bezout_euclidean_equationsumoutputimaginary) = S ge_signed_half_bezout_euclidean_equationsumoutputimaginarydecode))) /\ ((((ge_first_ip_bezout_euclidean_equationsum) + (ge_second_ip_bezout_euclidean_equationsum))) + ge_balance_negative_bezout_euclidean_equationsumoutputimaginary = (((ge_first_in_bezout_euclidean_equationsum) + (ge_second_in_bezout_euclidean_equationsum))) + ge_balance_positive_bezout_euclidean_equationsumoutputimaginary))))))))))) -> (exists gr_first_product_bezout_remainder gr_second_product_bezout_remainder. ((exists ge_first_rp_bezout_remainderfirst ge_first_rn_bezout_remainderfirst ge_first_ip_bezout_remainderfirst ge_first_in_bezout_remainderfirst ge_second_rp_bezout_remainderfirst ge_second_rn_bezout_remainderfirst ge_second_ip_bezout_remainderfirst ge_second_in_bezout_remainderfirst. ((exists ge_representation_real_code_bezout_remainderfirstfirst ge_representation_imaginary_code_bezout_remainderfirstfirst. (((b) = ((ge_representation_real_code_bezout_remainderfirstfirst) + (ge_representation_imaginary_code_bezout_remainderfirstfirst)) * S ((ge_representation_real_code_bezout_remainderfirstfirst) + (ge_representation_imaginary_code_bezout_remainderfirstfirst)) + ((ge_representation_imaginary_code_bezout_remainderfirstfirst) + (ge_representation_imaginary_code_bezout_remainderfirstfirst))) /\ ((exists ge_balance_positive_bezout_remainderfirstfirstreal ge_balance_negative_bezout_remainderfirstfirstreal. (((((ge_representation_real_code_bezout_remainderfirstfirst) = 2 * (ge_balance_positive_bezout_remainderfirstfirstreal) /\ (ge_balance_negative_bezout_remainderfirstfirstreal) = 0) \/ exists ge_signed_half_bezout_remainderfirstfirstrealdecode. (((ge_representation_real_code_bezout_remainderfirstfirst) = 2 * ge_signed_half_bezout_remainderfirstfirstrealdecode + 1 /\ (ge_balance_positive_bezout_remainderfirstfirstreal) = 0) /\ (ge_balance_negative_bezout_remainderfirstfirstreal) = S ge_signed_half_bezout_remainderfirstfirstrealdecode))) /\ ((ge_first_rp_bezout_remainderfirst) + ge_balance_negative_bezout_remainderfirstfirstreal = (ge_first_rn_bezout_remainderfirst) + ge_balance_positive_bezout_remainderfirstfirstreal))) /\ (exists ge_balance_positive_bezout_remainderfirstfirstimaginary ge_balance_negative_bezout_remainderfirstfirstimaginary. (((((ge_representation_imaginary_code_bezout_remainderfirstfirst) = 2 * (ge_balance_positive_bezout_remainderfirstfirstimaginary) /\ (ge_balance_negative_bezout_remainderfirstfirstimaginary) = 0) \/ exists ge_signed_half_bezout_remainderfirstfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_remainderfirstfirst) = 2 * ge_signed_half_bezout_remainderfirstfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_remainderfirstfirstimaginary) = 0) /\ (ge_balance_negative_bezout_remainderfirstfirstimaginary) = S ge_signed_half_bezout_remainderfirstfirstimaginarydecode))) /\ ((ge_first_ip_bezout_remainderfirst) + ge_balance_negative_bezout_remainderfirstfirstimaginary = (ge_first_in_bezout_remainderfirst) + ge_balance_positive_bezout_remainderfirstfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_remainderfirstsecond ge_representation_imaginary_code_bezout_remainderfirstsecond. (((u) = ((ge_representation_real_code_bezout_remainderfirstsecond) + (ge_representation_imaginary_code_bezout_remainderfirstsecond)) * S ((ge_representation_real_code_bezout_remainderfirstsecond) + (ge_representation_imaginary_code_bezout_remainderfirstsecond)) + ((ge_representation_imaginary_code_bezout_remainderfirstsecond) + (ge_representation_imaginary_code_bezout_remainderfirstsecond))) /\ ((exists ge_balance_positive_bezout_remainderfirstsecondreal ge_balance_negative_bezout_remainderfirstsecondreal. (((((ge_representation_real_code_bezout_remainderfirstsecond) = 2 * (ge_balance_positive_bezout_remainderfirstsecondreal) /\ (ge_balance_negative_bezout_remainderfirstsecondreal) = 0) \/ exists ge_signed_half_bezout_remainderfirstsecondrealdecode. (((ge_representation_real_code_bezout_remainderfirstsecond) = 2 * ge_signed_half_bezout_remainderfirstsecondrealdecode + 1 /\ (ge_balance_positive_bezout_remainderfirstsecondreal) = 0) /\ (ge_balance_negative_bezout_remainderfirstsecondreal) = S ge_signed_half_bezout_remainderfirstsecondrealdecode))) /\ ((ge_second_rp_bezout_remainderfirst) + ge_balance_negative_bezout_remainderfirstsecondreal = (ge_second_rn_bezout_remainderfirst) + ge_balance_positive_bezout_remainderfirstsecondreal))) /\ (exists ge_balance_positive_bezout_remainderfirstsecondimaginary ge_balance_negative_bezout_remainderfirstsecondimaginary. (((((ge_representation_imaginary_code_bezout_remainderfirstsecond) = 2 * (ge_balance_positive_bezout_remainderfirstsecondimaginary) /\ (ge_balance_negative_bezout_remainderfirstsecondimaginary) = 0) \/ exists ge_signed_half_bezout_remainderfirstsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_remainderfirstsecond) = 2 * ge_signed_half_bezout_remainderfirstsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_remainderfirstsecondimaginary) = 0) /\ (ge_balance_negative_bezout_remainderfirstsecondimaginary) = S ge_signed_half_bezout_remainderfirstsecondimaginarydecode))) /\ ((ge_second_ip_bezout_remainderfirst) + ge_balance_negative_bezout_remainderfirstsecondimaginary = (ge_second_in_bezout_remainderfirst) + ge_balance_positive_bezout_remainderfirstsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_remainderfirstoutput ge_representation_imaginary_code_bezout_remainderfirstoutput. (((gr_first_product_bezout_remainder) = ((ge_representation_real_code_bezout_remainderfirstoutput) + (ge_representation_imaginary_code_bezout_remainderfirstoutput)) * S ((ge_representation_real_code_bezout_remainderfirstoutput) + (ge_representation_imaginary_code_bezout_remainderfirstoutput)) + ((ge_representation_imaginary_code_bezout_remainderfirstoutput) + (ge_representation_imaginary_code_bezout_remainderfirstoutput))) /\ ((exists ge_balance_positive_bezout_remainderfirstoutputreal ge_balance_negative_bezout_remainderfirstoutputreal. (((((ge_representation_real_code_bezout_remainderfirstoutput) = 2 * (ge_balance_positive_bezout_remainderfirstoutputreal) /\ (ge_balance_negative_bezout_remainderfirstoutputreal) = 0) \/ exists ge_signed_half_bezout_remainderfirstoutputrealdecode. (((ge_representation_real_code_bezout_remainderfirstoutput) = 2 * ge_signed_half_bezout_remainderfirstoutputrealdecode + 1 /\ (ge_balance_positive_bezout_remainderfirstoutputreal) = 0) /\ (ge_balance_negative_bezout_remainderfirstoutputreal) = S ge_signed_half_bezout_remainderfirstoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_remainderfirst) * (ge_second_rp_bezout_remainderfirst))) + (((ge_first_rn_bezout_remainderfirst) * (ge_second_rn_bezout_remainderfirst))))) + (((((ge_first_ip_bezout_remainderfirst) * (ge_second_in_bezout_remainderfirst))) + (((ge_first_in_bezout_remainderfirst) * (ge_second_ip_bezout_remainderfirst))))))) + ge_balance_negative_bezout_remainderfirstoutputreal = (((((((ge_first_rp_bezout_remainderfirst) * (ge_second_rn_bezout_remainderfirst))) + (((ge_first_rn_bezout_remainderfirst) * (ge_second_rp_bezout_remainderfirst))))) + (((((ge_first_ip_bezout_remainderfirst) * (ge_second_ip_bezout_remainderfirst))) + (((ge_first_in_bezout_remainderfirst) * (ge_second_in_bezout_remainderfirst))))))) + ge_balance_positive_bezout_remainderfirstoutputreal))) /\ (exists ge_balance_positive_bezout_remainderfirstoutputimaginary ge_balance_negative_bezout_remainderfirstoutputimaginary. (((((ge_representation_imaginary_code_bezout_remainderfirstoutput) = 2 * (ge_balance_positive_bezout_remainderfirstoutputimaginary) /\ (ge_balance_negative_bezout_remainderfirstoutputimaginary) = 0) \/ exists ge_signed_half_bezout_remainderfirstoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_remainderfirstoutput) = 2 * ge_signed_half_bezout_remainderfirstoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_remainderfirstoutputimaginary) = 0) /\ (ge_balance_negative_bezout_remainderfirstoutputimaginary) = S ge_signed_half_bezout_remainderfirstoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_remainderfirst) * (ge_second_ip_bezout_remainderfirst))) + (((ge_first_rn_bezout_remainderfirst) * (ge_second_in_bezout_remainderfirst))))) + (((((ge_first_ip_bezout_remainderfirst) * (ge_second_rp_bezout_remainderfirst))) + (((ge_first_in_bezout_remainderfirst) * (ge_second_rn_bezout_remainderfirst))))))) + ge_balance_negative_bezout_remainderfirstoutputimaginary = (((((((ge_first_rp_bezout_remainderfirst) * (ge_second_in_bezout_remainderfirst))) + (((ge_first_rn_bezout_remainderfirst) * (ge_second_ip_bezout_remainderfirst))))) + (((((ge_first_ip_bezout_remainderfirst) * (ge_second_rn_bezout_remainderfirst))) + (((ge_first_in_bezout_remainderfirst) * (ge_second_rp_bezout_remainderfirst))))))) + ge_balance_positive_bezout_remainderfirstoutputimaginary))))))))) /\ ((exists ge_first_rp_bezout_remaindersecond ge_first_rn_bezout_remaindersecond ge_first_ip_bezout_remaindersecond ge_first_in_bezout_remaindersecond ge_second_rp_bezout_remaindersecond ge_second_rn_bezout_remaindersecond ge_second_ip_bezout_remaindersecond ge_second_in_bezout_remaindersecond. ((exists ge_representation_real_code_bezout_remaindersecondfirst ge_representation_imaginary_code_bezout_remaindersecondfirst. (((r) = ((ge_representation_real_code_bezout_remaindersecondfirst) + (ge_representation_imaginary_code_bezout_remaindersecondfirst)) * S ((ge_representation_real_code_bezout_remaindersecondfirst) + (ge_representation_imaginary_code_bezout_remaindersecondfirst)) + ((ge_representation_imaginary_code_bezout_remaindersecondfirst) + (ge_representation_imaginary_code_bezout_remaindersecondfirst))) /\ ((exists ge_balance_positive_bezout_remaindersecondfirstreal ge_balance_negative_bezout_remaindersecondfirstreal. (((((ge_representation_real_code_bezout_remaindersecondfirst) = 2 * (ge_balance_positive_bezout_remaindersecondfirstreal) /\ (ge_balance_negative_bezout_remaindersecondfirstreal) = 0) \/ exists ge_signed_half_bezout_remaindersecondfirstrealdecode. (((ge_representation_real_code_bezout_remaindersecondfirst) = 2 * ge_signed_half_bezout_remaindersecondfirstrealdecode + 1 /\ (ge_balance_positive_bezout_remaindersecondfirstreal) = 0) /\ (ge_balance_negative_bezout_remaindersecondfirstreal) = S ge_signed_half_bezout_remaindersecondfirstrealdecode))) /\ ((ge_first_rp_bezout_remaindersecond) + ge_balance_negative_bezout_remaindersecondfirstreal = (ge_first_rn_bezout_remaindersecond) + ge_balance_positive_bezout_remaindersecondfirstreal))) /\ (exists ge_balance_positive_bezout_remaindersecondfirstimaginary ge_balance_negative_bezout_remaindersecondfirstimaginary. (((((ge_representation_imaginary_code_bezout_remaindersecondfirst) = 2 * (ge_balance_positive_bezout_remaindersecondfirstimaginary) /\ (ge_balance_negative_bezout_remaindersecondfirstimaginary) = 0) \/ exists ge_signed_half_bezout_remaindersecondfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_remaindersecondfirst) = 2 * ge_signed_half_bezout_remaindersecondfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_remaindersecondfirstimaginary) = 0) /\ (ge_balance_negative_bezout_remaindersecondfirstimaginary) = S ge_signed_half_bezout_remaindersecondfirstimaginarydecode))) /\ ((ge_first_ip_bezout_remaindersecond) + ge_balance_negative_bezout_remaindersecondfirstimaginary = (ge_first_in_bezout_remaindersecond) + ge_balance_positive_bezout_remaindersecondfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_remaindersecondsecond ge_representation_imaginary_code_bezout_remaindersecondsecond. (((v) = ((ge_representation_real_code_bezout_remaindersecondsecond) + (ge_representation_imaginary_code_bezout_remaindersecondsecond)) * S ((ge_representation_real_code_bezout_remaindersecondsecond) + (ge_representation_imaginary_code_bezout_remaindersecondsecond)) + ((ge_representation_imaginary_code_bezout_remaindersecondsecond) + (ge_representation_imaginary_code_bezout_remaindersecondsecond))) /\ ((exists ge_balance_positive_bezout_remaindersecondsecondreal ge_balance_negative_bezout_remaindersecondsecondreal. (((((ge_representation_real_code_bezout_remaindersecondsecond) = 2 * (ge_balance_positive_bezout_remaindersecondsecondreal) /\ (ge_balance_negative_bezout_remaindersecondsecondreal) = 0) \/ exists ge_signed_half_bezout_remaindersecondsecondrealdecode. (((ge_representation_real_code_bezout_remaindersecondsecond) = 2 * ge_signed_half_bezout_remaindersecondsecondrealdecode + 1 /\ (ge_balance_positive_bezout_remaindersecondsecondreal) = 0) /\ (ge_balance_negative_bezout_remaindersecondsecondreal) = S ge_signed_half_bezout_remaindersecondsecondrealdecode))) /\ ((ge_second_rp_bezout_remaindersecond) + ge_balance_negative_bezout_remaindersecondsecondreal = (ge_second_rn_bezout_remaindersecond) + ge_balance_positive_bezout_remaindersecondsecondreal))) /\ (exists ge_balance_positive_bezout_remaindersecondsecondimaginary ge_balance_negative_bezout_remaindersecondsecondimaginary. (((((ge_representation_imaginary_code_bezout_remaindersecondsecond) = 2 * (ge_balance_positive_bezout_remaindersecondsecondimaginary) /\ (ge_balance_negative_bezout_remaindersecondsecondimaginary) = 0) \/ exists ge_signed_half_bezout_remaindersecondsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_remaindersecondsecond) = 2 * ge_signed_half_bezout_remaindersecondsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_remaindersecondsecondimaginary) = 0) /\ (ge_balance_negative_bezout_remaindersecondsecondimaginary) = S ge_signed_half_bezout_remaindersecondsecondimaginarydecode))) /\ ((ge_second_ip_bezout_remaindersecond) + ge_balance_negative_bezout_remaindersecondsecondimaginary = (ge_second_in_bezout_remaindersecond) + ge_balance_positive_bezout_remaindersecondsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_remaindersecondoutput ge_representation_imaginary_code_bezout_remaindersecondoutput. (((gr_second_product_bezout_remainder) = ((ge_representation_real_code_bezout_remaindersecondoutput) + (ge_representation_imaginary_code_bezout_remaindersecondoutput)) * S ((ge_representation_real_code_bezout_remaindersecondoutput) + (ge_representation_imaginary_code_bezout_remaindersecondoutput)) + ((ge_representation_imaginary_code_bezout_remaindersecondoutput) + (ge_representation_imaginary_code_bezout_remaindersecondoutput))) /\ ((exists ge_balance_positive_bezout_remaindersecondoutputreal ge_balance_negative_bezout_remaindersecondoutputreal. (((((ge_representation_real_code_bezout_remaindersecondoutput) = 2 * (ge_balance_positive_bezout_remaindersecondoutputreal) /\ (ge_balance_negative_bezout_remaindersecondoutputreal) = 0) \/ exists ge_signed_half_bezout_remaindersecondoutputrealdecode. (((ge_representation_real_code_bezout_remaindersecondoutput) = 2 * ge_signed_half_bezout_remaindersecondoutputrealdecode + 1 /\ (ge_balance_positive_bezout_remaindersecondoutputreal) = 0) /\ (ge_balance_negative_bezout_remaindersecondoutputreal) = S ge_signed_half_bezout_remaindersecondoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_remaindersecond) * (ge_second_rp_bezout_remaindersecond))) + (((ge_first_rn_bezout_remaindersecond) * (ge_second_rn_bezout_remaindersecond))))) + (((((ge_first_ip_bezout_remaindersecond) * (ge_second_in_bezout_remaindersecond))) + (((ge_first_in_bezout_remaindersecond) * (ge_second_ip_bezout_remaindersecond))))))) + ge_balance_negative_bezout_remaindersecondoutputreal = (((((((ge_first_rp_bezout_remaindersecond) * (ge_second_rn_bezout_remaindersecond))) + (((ge_first_rn_bezout_remaindersecond) * (ge_second_rp_bezout_remaindersecond))))) + (((((ge_first_ip_bezout_remaindersecond) * (ge_second_ip_bezout_remaindersecond))) + (((ge_first_in_bezout_remaindersecond) * (ge_second_in_bezout_remaindersecond))))))) + ge_balance_positive_bezout_remaindersecondoutputreal))) /\ (exists ge_balance_positive_bezout_remaindersecondoutputimaginary ge_balance_negative_bezout_remaindersecondoutputimaginary. (((((ge_representation_imaginary_code_bezout_remaindersecondoutput) = 2 * (ge_balance_positive_bezout_remaindersecondoutputimaginary) /\ (ge_balance_negative_bezout_remaindersecondoutputimaginary) = 0) \/ exists ge_signed_half_bezout_remaindersecondoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_remaindersecondoutput) = 2 * ge_signed_half_bezout_remaindersecondoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_remaindersecondoutputimaginary) = 0) /\ (ge_balance_negative_bezout_remaindersecondoutputimaginary) = S ge_signed_half_bezout_remaindersecondoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_remaindersecond) * (ge_second_ip_bezout_remaindersecond))) + (((ge_first_rn_bezout_remaindersecond) * (ge_second_in_bezout_remaindersecond))))) + (((((ge_first_ip_bezout_remaindersecond) * (ge_second_rp_bezout_remaindersecond))) + (((ge_first_in_bezout_remaindersecond) * (ge_second_rn_bezout_remaindersecond))))))) + ge_balance_negative_bezout_remaindersecondoutputimaginary = (((((((ge_first_rp_bezout_remaindersecond) * (ge_second_in_bezout_remaindersecond))) + (((ge_first_rn_bezout_remaindersecond) * (ge_second_ip_bezout_remaindersecond))))) + (((((ge_first_ip_bezout_remaindersecond) * (ge_second_rn_bezout_remaindersecond))) + (((ge_first_in_bezout_remaindersecond) * (ge_second_rp_bezout_remaindersecond))))))) + ge_balance_positive_bezout_remaindersecondoutputimaginary))))))))) /\ (exists ge_first_rp_bezout_remaindersum ge_first_rn_bezout_remaindersum ge_first_ip_bezout_remaindersum ge_first_in_bezout_remaindersum ge_second_rp_bezout_remaindersum ge_second_rn_bezout_remaindersum ge_second_ip_bezout_remaindersum ge_second_in_bezout_remaindersum. ((exists ge_representation_real_code_bezout_remaindersumfirst ge_representation_imaginary_code_bezout_remaindersumfirst. (((gr_first_product_bezout_remainder) = ((ge_representation_real_code_bezout_remaindersumfirst) + (ge_representation_imaginary_code_bezout_remaindersumfirst)) * S ((ge_representation_real_code_bezout_remaindersumfirst) + (ge_representation_imaginary_code_bezout_remaindersumfirst)) + ((ge_representation_imaginary_code_bezout_remaindersumfirst) + (ge_representation_imaginary_code_bezout_remaindersumfirst))) /\ ((exists ge_balance_positive_bezout_remaindersumfirstreal ge_balance_negative_bezout_remaindersumfirstreal. (((((ge_representation_real_code_bezout_remaindersumfirst) = 2 * (ge_balance_positive_bezout_remaindersumfirstreal) /\ (ge_balance_negative_bezout_remaindersumfirstreal) = 0) \/ exists ge_signed_half_bezout_remaindersumfirstrealdecode. (((ge_representation_real_code_bezout_remaindersumfirst) = 2 * ge_signed_half_bezout_remaindersumfirstrealdecode + 1 /\ (ge_balance_positive_bezout_remaindersumfirstreal) = 0) /\ (ge_balance_negative_bezout_remaindersumfirstreal) = S ge_signed_half_bezout_remaindersumfirstrealdecode))) /\ ((ge_first_rp_bezout_remaindersum) + ge_balance_negative_bezout_remaindersumfirstreal = (ge_first_rn_bezout_remaindersum) + ge_balance_positive_bezout_remaindersumfirstreal))) /\ (exists ge_balance_positive_bezout_remaindersumfirstimaginary ge_balance_negative_bezout_remaindersumfirstimaginary. (((((ge_representation_imaginary_code_bezout_remaindersumfirst) = 2 * (ge_balance_positive_bezout_remaindersumfirstimaginary) /\ (ge_balance_negative_bezout_remaindersumfirstimaginary) = 0) \/ exists ge_signed_half_bezout_remaindersumfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_remaindersumfirst) = 2 * ge_signed_half_bezout_remaindersumfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_remaindersumfirstimaginary) = 0) /\ (ge_balance_negative_bezout_remaindersumfirstimaginary) = S ge_signed_half_bezout_remaindersumfirstimaginarydecode))) /\ ((ge_first_ip_bezout_remaindersum) + ge_balance_negative_bezout_remaindersumfirstimaginary = (ge_first_in_bezout_remaindersum) + ge_balance_positive_bezout_remaindersumfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_remaindersumsecond ge_representation_imaginary_code_bezout_remaindersumsecond. (((gr_second_product_bezout_remainder) = ((ge_representation_real_code_bezout_remaindersumsecond) + (ge_representation_imaginary_code_bezout_remaindersumsecond)) * S ((ge_representation_real_code_bezout_remaindersumsecond) + (ge_representation_imaginary_code_bezout_remaindersumsecond)) + ((ge_representation_imaginary_code_bezout_remaindersumsecond) + (ge_representation_imaginary_code_bezout_remaindersumsecond))) /\ ((exists ge_balance_positive_bezout_remaindersumsecondreal ge_balance_negative_bezout_remaindersumsecondreal. (((((ge_representation_real_code_bezout_remaindersumsecond) = 2 * (ge_balance_positive_bezout_remaindersumsecondreal) /\ (ge_balance_negative_bezout_remaindersumsecondreal) = 0) \/ exists ge_signed_half_bezout_remaindersumsecondrealdecode. (((ge_representation_real_code_bezout_remaindersumsecond) = 2 * ge_signed_half_bezout_remaindersumsecondrealdecode + 1 /\ (ge_balance_positive_bezout_remaindersumsecondreal) = 0) /\ (ge_balance_negative_bezout_remaindersumsecondreal) = S ge_signed_half_bezout_remaindersumsecondrealdecode))) /\ ((ge_second_rp_bezout_remaindersum) + ge_balance_negative_bezout_remaindersumsecondreal = (ge_second_rn_bezout_remaindersum) + ge_balance_positive_bezout_remaindersumsecondreal))) /\ (exists ge_balance_positive_bezout_remaindersumsecondimaginary ge_balance_negative_bezout_remaindersumsecondimaginary. (((((ge_representation_imaginary_code_bezout_remaindersumsecond) = 2 * (ge_balance_positive_bezout_remaindersumsecondimaginary) /\ (ge_balance_negative_bezout_remaindersumsecondimaginary) = 0) \/ exists ge_signed_half_bezout_remaindersumsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_remaindersumsecond) = 2 * ge_signed_half_bezout_remaindersumsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_remaindersumsecondimaginary) = 0) /\ (ge_balance_negative_bezout_remaindersumsecondimaginary) = S ge_signed_half_bezout_remaindersumsecondimaginarydecode))) /\ ((ge_second_ip_bezout_remaindersum) + ge_balance_negative_bezout_remaindersumsecondimaginary = (ge_second_in_bezout_remaindersum) + ge_balance_positive_bezout_remaindersumsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_remaindersumoutput ge_representation_imaginary_code_bezout_remaindersumoutput. (((g) = ((ge_representation_real_code_bezout_remaindersumoutput) + (ge_representation_imaginary_code_bezout_remaindersumoutput)) * S ((ge_representation_real_code_bezout_remaindersumoutput) + (ge_representation_imaginary_code_bezout_remaindersumoutput)) + ((ge_representation_imaginary_code_bezout_remaindersumoutput) + (ge_representation_imaginary_code_bezout_remaindersumoutput))) /\ ((exists ge_balance_positive_bezout_remaindersumoutputreal ge_balance_negative_bezout_remaindersumoutputreal. (((((ge_representation_real_code_bezout_remaindersumoutput) = 2 * (ge_balance_positive_bezout_remaindersumoutputreal) /\ (ge_balance_negative_bezout_remaindersumoutputreal) = 0) \/ exists ge_signed_half_bezout_remaindersumoutputrealdecode. (((ge_representation_real_code_bezout_remaindersumoutput) = 2 * ge_signed_half_bezout_remaindersumoutputrealdecode + 1 /\ (ge_balance_positive_bezout_remaindersumoutputreal) = 0) /\ (ge_balance_negative_bezout_remaindersumoutputreal) = S ge_signed_half_bezout_remaindersumoutputrealdecode))) /\ ((((ge_first_rp_bezout_remaindersum) + (ge_second_rp_bezout_remaindersum))) + ge_balance_negative_bezout_remaindersumoutputreal = (((ge_first_rn_bezout_remaindersum) + (ge_second_rn_bezout_remaindersum))) + ge_balance_positive_bezout_remaindersumoutputreal))) /\ (exists ge_balance_positive_bezout_remaindersumoutputimaginary ge_balance_negative_bezout_remaindersumoutputimaginary. (((((ge_representation_imaginary_code_bezout_remaindersumoutput) = 2 * (ge_balance_positive_bezout_remaindersumoutputimaginary) /\ (ge_balance_negative_bezout_remaindersumoutputimaginary) = 0) \/ exists ge_signed_half_bezout_remaindersumoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_remaindersumoutput) = 2 * ge_signed_half_bezout_remaindersumoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_remaindersumoutputimaginary) = 0) /\ (ge_balance_negative_bezout_remaindersumoutputimaginary) = S ge_signed_half_bezout_remaindersumoutputimaginarydecode))) /\ ((((ge_first_ip_bezout_remaindersum) + (ge_second_ip_bezout_remaindersum))) + ge_balance_negative_bezout_remaindersumoutputimaginary = (((ge_first_in_bezout_remaindersum) + (ge_second_in_bezout_remaindersum))) + ge_balance_positive_bezout_remaindersumoutputimaginary)))))))))))) -> exists w. (exists gr_first_product_bezout_dividend gr_second_product_bezout_dividend. ((exists ge_first_rp_bezout_dividendfirst ge_first_rn_bezout_dividendfirst ge_first_ip_bezout_dividendfirst ge_first_in_bezout_dividendfirst ge_second_rp_bezout_dividendfirst ge_second_rn_bezout_dividendfirst ge_second_ip_bezout_dividendfirst ge_second_in_bezout_dividendfirst. ((exists ge_representation_real_code_bezout_dividendfirstfirst ge_representation_imaginary_code_bezout_dividendfirstfirst. (((a) = ((ge_representation_real_code_bezout_dividendfirstfirst) + (ge_representation_imaginary_code_bezout_dividendfirstfirst)) * S ((ge_representation_real_code_bezout_dividendfirstfirst) + (ge_representation_imaginary_code_bezout_dividendfirstfirst)) + ((ge_representation_imaginary_code_bezout_dividendfirstfirst) + (ge_representation_imaginary_code_bezout_dividendfirstfirst))) /\ ((exists ge_balance_positive_bezout_dividendfirstfirstreal ge_balance_negative_bezout_dividendfirstfirstreal. (((((ge_representation_real_code_bezout_dividendfirstfirst) = 2 * (ge_balance_positive_bezout_dividendfirstfirstreal) /\ (ge_balance_negative_bezout_dividendfirstfirstreal) = 0) \/ exists ge_signed_half_bezout_dividendfirstfirstrealdecode. (((ge_representation_real_code_bezout_dividendfirstfirst) = 2 * ge_signed_half_bezout_dividendfirstfirstrealdecode + 1 /\ (ge_balance_positive_bezout_dividendfirstfirstreal) = 0) /\ (ge_balance_negative_bezout_dividendfirstfirstreal) = S ge_signed_half_bezout_dividendfirstfirstrealdecode))) /\ ((ge_first_rp_bezout_dividendfirst) + ge_balance_negative_bezout_dividendfirstfirstreal = (ge_first_rn_bezout_dividendfirst) + ge_balance_positive_bezout_dividendfirstfirstreal))) /\ (exists ge_balance_positive_bezout_dividendfirstfirstimaginary ge_balance_negative_bezout_dividendfirstfirstimaginary. (((((ge_representation_imaginary_code_bezout_dividendfirstfirst) = 2 * (ge_balance_positive_bezout_dividendfirstfirstimaginary) /\ (ge_balance_negative_bezout_dividendfirstfirstimaginary) = 0) \/ exists ge_signed_half_bezout_dividendfirstfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_dividendfirstfirst) = 2 * ge_signed_half_bezout_dividendfirstfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_dividendfirstfirstimaginary) = 0) /\ (ge_balance_negative_bezout_dividendfirstfirstimaginary) = S ge_signed_half_bezout_dividendfirstfirstimaginarydecode))) /\ ((ge_first_ip_bezout_dividendfirst) + ge_balance_negative_bezout_dividendfirstfirstimaginary = (ge_first_in_bezout_dividendfirst) + ge_balance_positive_bezout_dividendfirstfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_dividendfirstsecond ge_representation_imaginary_code_bezout_dividendfirstsecond. (((v) = ((ge_representation_real_code_bezout_dividendfirstsecond) + (ge_representation_imaginary_code_bezout_dividendfirstsecond)) * S ((ge_representation_real_code_bezout_dividendfirstsecond) + (ge_representation_imaginary_code_bezout_dividendfirstsecond)) + ((ge_representation_imaginary_code_bezout_dividendfirstsecond) + (ge_representation_imaginary_code_bezout_dividendfirstsecond))) /\ ((exists ge_balance_positive_bezout_dividendfirstsecondreal ge_balance_negative_bezout_dividendfirstsecondreal. (((((ge_representation_real_code_bezout_dividendfirstsecond) = 2 * (ge_balance_positive_bezout_dividendfirstsecondreal) /\ (ge_balance_negative_bezout_dividendfirstsecondreal) = 0) \/ exists ge_signed_half_bezout_dividendfirstsecondrealdecode. (((ge_representation_real_code_bezout_dividendfirstsecond) = 2 * ge_signed_half_bezout_dividendfirstsecondrealdecode + 1 /\ (ge_balance_positive_bezout_dividendfirstsecondreal) = 0) /\ (ge_balance_negative_bezout_dividendfirstsecondreal) = S ge_signed_half_bezout_dividendfirstsecondrealdecode))) /\ ((ge_second_rp_bezout_dividendfirst) + ge_balance_negative_bezout_dividendfirstsecondreal = (ge_second_rn_bezout_dividendfirst) + ge_balance_positive_bezout_dividendfirstsecondreal))) /\ (exists ge_balance_positive_bezout_dividendfirstsecondimaginary ge_balance_negative_bezout_dividendfirstsecondimaginary. (((((ge_representation_imaginary_code_bezout_dividendfirstsecond) = 2 * (ge_balance_positive_bezout_dividendfirstsecondimaginary) /\ (ge_balance_negative_bezout_dividendfirstsecondimaginary) = 0) \/ exists ge_signed_half_bezout_dividendfirstsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_dividendfirstsecond) = 2 * ge_signed_half_bezout_dividendfirstsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_dividendfirstsecondimaginary) = 0) /\ (ge_balance_negative_bezout_dividendfirstsecondimaginary) = S ge_signed_half_bezout_dividendfirstsecondimaginarydecode))) /\ ((ge_second_ip_bezout_dividendfirst) + ge_balance_negative_bezout_dividendfirstsecondimaginary = (ge_second_in_bezout_dividendfirst) + ge_balance_positive_bezout_dividendfirstsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_dividendfirstoutput ge_representation_imaginary_code_bezout_dividendfirstoutput. (((gr_first_product_bezout_dividend) = ((ge_representation_real_code_bezout_dividendfirstoutput) + (ge_representation_imaginary_code_bezout_dividendfirstoutput)) * S ((ge_representation_real_code_bezout_dividendfirstoutput) + (ge_representation_imaginary_code_bezout_dividendfirstoutput)) + ((ge_representation_imaginary_code_bezout_dividendfirstoutput) + (ge_representation_imaginary_code_bezout_dividendfirstoutput))) /\ ((exists ge_balance_positive_bezout_dividendfirstoutputreal ge_balance_negative_bezout_dividendfirstoutputreal. (((((ge_representation_real_code_bezout_dividendfirstoutput) = 2 * (ge_balance_positive_bezout_dividendfirstoutputreal) /\ (ge_balance_negative_bezout_dividendfirstoutputreal) = 0) \/ exists ge_signed_half_bezout_dividendfirstoutputrealdecode. (((ge_representation_real_code_bezout_dividendfirstoutput) = 2 * ge_signed_half_bezout_dividendfirstoutputrealdecode + 1 /\ (ge_balance_positive_bezout_dividendfirstoutputreal) = 0) /\ (ge_balance_negative_bezout_dividendfirstoutputreal) = S ge_signed_half_bezout_dividendfirstoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_dividendfirst) * (ge_second_rp_bezout_dividendfirst))) + (((ge_first_rn_bezout_dividendfirst) * (ge_second_rn_bezout_dividendfirst))))) + (((((ge_first_ip_bezout_dividendfirst) * (ge_second_in_bezout_dividendfirst))) + (((ge_first_in_bezout_dividendfirst) * (ge_second_ip_bezout_dividendfirst))))))) + ge_balance_negative_bezout_dividendfirstoutputreal = (((((((ge_first_rp_bezout_dividendfirst) * (ge_second_rn_bezout_dividendfirst))) + (((ge_first_rn_bezout_dividendfirst) * (ge_second_rp_bezout_dividendfirst))))) + (((((ge_first_ip_bezout_dividendfirst) * (ge_second_ip_bezout_dividendfirst))) + (((ge_first_in_bezout_dividendfirst) * (ge_second_in_bezout_dividendfirst))))))) + ge_balance_positive_bezout_dividendfirstoutputreal))) /\ (exists ge_balance_positive_bezout_dividendfirstoutputimaginary ge_balance_negative_bezout_dividendfirstoutputimaginary. (((((ge_representation_imaginary_code_bezout_dividendfirstoutput) = 2 * (ge_balance_positive_bezout_dividendfirstoutputimaginary) /\ (ge_balance_negative_bezout_dividendfirstoutputimaginary) = 0) \/ exists ge_signed_half_bezout_dividendfirstoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_dividendfirstoutput) = 2 * ge_signed_half_bezout_dividendfirstoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_dividendfirstoutputimaginary) = 0) /\ (ge_balance_negative_bezout_dividendfirstoutputimaginary) = S ge_signed_half_bezout_dividendfirstoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_dividendfirst) * (ge_second_ip_bezout_dividendfirst))) + (((ge_first_rn_bezout_dividendfirst) * (ge_second_in_bezout_dividendfirst))))) + (((((ge_first_ip_bezout_dividendfirst) * (ge_second_rp_bezout_dividendfirst))) + (((ge_first_in_bezout_dividendfirst) * (ge_second_rn_bezout_dividendfirst))))))) + ge_balance_negative_bezout_dividendfirstoutputimaginary = (((((((ge_first_rp_bezout_dividendfirst) * (ge_second_in_bezout_dividendfirst))) + (((ge_first_rn_bezout_dividendfirst) * (ge_second_ip_bezout_dividendfirst))))) + (((((ge_first_ip_bezout_dividendfirst) * (ge_second_rn_bezout_dividendfirst))) + (((ge_first_in_bezout_dividendfirst) * (ge_second_rp_bezout_dividendfirst))))))) + ge_balance_positive_bezout_dividendfirstoutputimaginary))))))))) /\ ((exists ge_first_rp_bezout_dividendsecond ge_first_rn_bezout_dividendsecond ge_first_ip_bezout_dividendsecond ge_first_in_bezout_dividendsecond ge_second_rp_bezout_dividendsecond ge_second_rn_bezout_dividendsecond ge_second_ip_bezout_dividendsecond ge_second_in_bezout_dividendsecond. ((exists ge_representation_real_code_bezout_dividendsecondfirst ge_representation_imaginary_code_bezout_dividendsecondfirst. (((b) = ((ge_representation_real_code_bezout_dividendsecondfirst) + (ge_representation_imaginary_code_bezout_dividendsecondfirst)) * S ((ge_representation_real_code_bezout_dividendsecondfirst) + (ge_representation_imaginary_code_bezout_dividendsecondfirst)) + ((ge_representation_imaginary_code_bezout_dividendsecondfirst) + (ge_representation_imaginary_code_bezout_dividendsecondfirst))) /\ ((exists ge_balance_positive_bezout_dividendsecondfirstreal ge_balance_negative_bezout_dividendsecondfirstreal. (((((ge_representation_real_code_bezout_dividendsecondfirst) = 2 * (ge_balance_positive_bezout_dividendsecondfirstreal) /\ (ge_balance_negative_bezout_dividendsecondfirstreal) = 0) \/ exists ge_signed_half_bezout_dividendsecondfirstrealdecode. (((ge_representation_real_code_bezout_dividendsecondfirst) = 2 * ge_signed_half_bezout_dividendsecondfirstrealdecode + 1 /\ (ge_balance_positive_bezout_dividendsecondfirstreal) = 0) /\ (ge_balance_negative_bezout_dividendsecondfirstreal) = S ge_signed_half_bezout_dividendsecondfirstrealdecode))) /\ ((ge_first_rp_bezout_dividendsecond) + ge_balance_negative_bezout_dividendsecondfirstreal = (ge_first_rn_bezout_dividendsecond) + ge_balance_positive_bezout_dividendsecondfirstreal))) /\ (exists ge_balance_positive_bezout_dividendsecondfirstimaginary ge_balance_negative_bezout_dividendsecondfirstimaginary. (((((ge_representation_imaginary_code_bezout_dividendsecondfirst) = 2 * (ge_balance_positive_bezout_dividendsecondfirstimaginary) /\ (ge_balance_negative_bezout_dividendsecondfirstimaginary) = 0) \/ exists ge_signed_half_bezout_dividendsecondfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_dividendsecondfirst) = 2 * ge_signed_half_bezout_dividendsecondfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_dividendsecondfirstimaginary) = 0) /\ (ge_balance_negative_bezout_dividendsecondfirstimaginary) = S ge_signed_half_bezout_dividendsecondfirstimaginarydecode))) /\ ((ge_first_ip_bezout_dividendsecond) + ge_balance_negative_bezout_dividendsecondfirstimaginary = (ge_first_in_bezout_dividendsecond) + ge_balance_positive_bezout_dividendsecondfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_dividendsecondsecond ge_representation_imaginary_code_bezout_dividendsecondsecond. (((w) = ((ge_representation_real_code_bezout_dividendsecondsecond) + (ge_representation_imaginary_code_bezout_dividendsecondsecond)) * S ((ge_representation_real_code_bezout_dividendsecondsecond) + (ge_representation_imaginary_code_bezout_dividendsecondsecond)) + ((ge_representation_imaginary_code_bezout_dividendsecondsecond) + (ge_representation_imaginary_code_bezout_dividendsecondsecond))) /\ ((exists ge_balance_positive_bezout_dividendsecondsecondreal ge_balance_negative_bezout_dividendsecondsecondreal. (((((ge_representation_real_code_bezout_dividendsecondsecond) = 2 * (ge_balance_positive_bezout_dividendsecondsecondreal) /\ (ge_balance_negative_bezout_dividendsecondsecondreal) = 0) \/ exists ge_signed_half_bezout_dividendsecondsecondrealdecode. (((ge_representation_real_code_bezout_dividendsecondsecond) = 2 * ge_signed_half_bezout_dividendsecondsecondrealdecode + 1 /\ (ge_balance_positive_bezout_dividendsecondsecondreal) = 0) /\ (ge_balance_negative_bezout_dividendsecondsecondreal) = S ge_signed_half_bezout_dividendsecondsecondrealdecode))) /\ ((ge_second_rp_bezout_dividendsecond) + ge_balance_negative_bezout_dividendsecondsecondreal = (ge_second_rn_bezout_dividendsecond) + ge_balance_positive_bezout_dividendsecondsecondreal))) /\ (exists ge_balance_positive_bezout_dividendsecondsecondimaginary ge_balance_negative_bezout_dividendsecondsecondimaginary. (((((ge_representation_imaginary_code_bezout_dividendsecondsecond) = 2 * (ge_balance_positive_bezout_dividendsecondsecondimaginary) /\ (ge_balance_negative_bezout_dividendsecondsecondimaginary) = 0) \/ exists ge_signed_half_bezout_dividendsecondsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_dividendsecondsecond) = 2 * ge_signed_half_bezout_dividendsecondsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_dividendsecondsecondimaginary) = 0) /\ (ge_balance_negative_bezout_dividendsecondsecondimaginary) = S ge_signed_half_bezout_dividendsecondsecondimaginarydecode))) /\ ((ge_second_ip_bezout_dividendsecond) + ge_balance_negative_bezout_dividendsecondsecondimaginary = (ge_second_in_bezout_dividendsecond) + ge_balance_positive_bezout_dividendsecondsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_dividendsecondoutput ge_representation_imaginary_code_bezout_dividendsecondoutput. (((gr_second_product_bezout_dividend) = ((ge_representation_real_code_bezout_dividendsecondoutput) + (ge_representation_imaginary_code_bezout_dividendsecondoutput)) * S ((ge_representation_real_code_bezout_dividendsecondoutput) + (ge_representation_imaginary_code_bezout_dividendsecondoutput)) + ((ge_representation_imaginary_code_bezout_dividendsecondoutput) + (ge_representation_imaginary_code_bezout_dividendsecondoutput))) /\ ((exists ge_balance_positive_bezout_dividendsecondoutputreal ge_balance_negative_bezout_dividendsecondoutputreal. (((((ge_representation_real_code_bezout_dividendsecondoutput) = 2 * (ge_balance_positive_bezout_dividendsecondoutputreal) /\ (ge_balance_negative_bezout_dividendsecondoutputreal) = 0) \/ exists ge_signed_half_bezout_dividendsecondoutputrealdecode. (((ge_representation_real_code_bezout_dividendsecondoutput) = 2 * ge_signed_half_bezout_dividendsecondoutputrealdecode + 1 /\ (ge_balance_positive_bezout_dividendsecondoutputreal) = 0) /\ (ge_balance_negative_bezout_dividendsecondoutputreal) = S ge_signed_half_bezout_dividendsecondoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_dividendsecond) * (ge_second_rp_bezout_dividendsecond))) + (((ge_first_rn_bezout_dividendsecond) * (ge_second_rn_bezout_dividendsecond))))) + (((((ge_first_ip_bezout_dividendsecond) * (ge_second_in_bezout_dividendsecond))) + (((ge_first_in_bezout_dividendsecond) * (ge_second_ip_bezout_dividendsecond))))))) + ge_balance_negative_bezout_dividendsecondoutputreal = (((((((ge_first_rp_bezout_dividendsecond) * (ge_second_rn_bezout_dividendsecond))) + (((ge_first_rn_bezout_dividendsecond) * (ge_second_rp_bezout_dividendsecond))))) + (((((ge_first_ip_bezout_dividendsecond) * (ge_second_ip_bezout_dividendsecond))) + (((ge_first_in_bezout_dividendsecond) * (ge_second_in_bezout_dividendsecond))))))) + ge_balance_positive_bezout_dividendsecondoutputreal))) /\ (exists ge_balance_positive_bezout_dividendsecondoutputimaginary ge_balance_negative_bezout_dividendsecondoutputimaginary. (((((ge_representation_imaginary_code_bezout_dividendsecondoutput) = 2 * (ge_balance_positive_bezout_dividendsecondoutputimaginary) /\ (ge_balance_negative_bezout_dividendsecondoutputimaginary) = 0) \/ exists ge_signed_half_bezout_dividendsecondoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_dividendsecondoutput) = 2 * ge_signed_half_bezout_dividendsecondoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_dividendsecondoutputimaginary) = 0) /\ (ge_balance_negative_bezout_dividendsecondoutputimaginary) = S ge_signed_half_bezout_dividendsecondoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_dividendsecond) * (ge_second_ip_bezout_dividendsecond))) + (((ge_first_rn_bezout_dividendsecond) * (ge_second_in_bezout_dividendsecond))))) + (((((ge_first_ip_bezout_dividendsecond) * (ge_second_rp_bezout_dividendsecond))) + (((ge_first_in_bezout_dividendsecond) * (ge_second_rn_bezout_dividendsecond))))))) + ge_balance_negative_bezout_dividendsecondoutputimaginary = (((((((ge_first_rp_bezout_dividendsecond) * (ge_second_in_bezout_dividendsecond))) + (((ge_first_rn_bezout_dividendsecond) * (ge_second_ip_bezout_dividendsecond))))) + (((((ge_first_ip_bezout_dividendsecond) * (ge_second_rn_bezout_dividendsecond))) + (((ge_first_in_bezout_dividendsecond) * (ge_second_rp_bezout_dividendsecond))))))) + ge_balance_positive_bezout_dividendsecondoutputimaginary))))))))) /\ (exists ge_first_rp_bezout_dividendsum ge_first_rn_bezout_dividendsum ge_first_ip_bezout_dividendsum ge_first_in_bezout_dividendsum ge_second_rp_bezout_dividendsum ge_second_rn_bezout_dividendsum ge_second_ip_bezout_dividendsum ge_second_in_bezout_dividendsum. ((exists ge_representation_real_code_bezout_dividendsumfirst ge_representation_imaginary_code_bezout_dividendsumfirst. (((gr_first_product_bezout_dividend) = ((ge_representation_real_code_bezout_dividendsumfirst) + (ge_representation_imaginary_code_bezout_dividendsumfirst)) * S ((ge_representation_real_code_bezout_dividendsumfirst) + (ge_representation_imaginary_code_bezout_dividendsumfirst)) + ((ge_representation_imaginary_code_bezout_dividendsumfirst) + (ge_representation_imaginary_code_bezout_dividendsumfirst))) /\ ((exists ge_balance_positive_bezout_dividendsumfirstreal ge_balance_negative_bezout_dividendsumfirstreal. (((((ge_representation_real_code_bezout_dividendsumfirst) = 2 * (ge_balance_positive_bezout_dividendsumfirstreal) /\ (ge_balance_negative_bezout_dividendsumfirstreal) = 0) \/ exists ge_signed_half_bezout_dividendsumfirstrealdecode. (((ge_representation_real_code_bezout_dividendsumfirst) = 2 * ge_signed_half_bezout_dividendsumfirstrealdecode + 1 /\ (ge_balance_positive_bezout_dividendsumfirstreal) = 0) /\ (ge_balance_negative_bezout_dividendsumfirstreal) = S ge_signed_half_bezout_dividendsumfirstrealdecode))) /\ ((ge_first_rp_bezout_dividendsum) + ge_balance_negative_bezout_dividendsumfirstreal = (ge_first_rn_bezout_dividendsum) + ge_balance_positive_bezout_dividendsumfirstreal))) /\ (exists ge_balance_positive_bezout_dividendsumfirstimaginary ge_balance_negative_bezout_dividendsumfirstimaginary. (((((ge_representation_imaginary_code_bezout_dividendsumfirst) = 2 * (ge_balance_positive_bezout_dividendsumfirstimaginary) /\ (ge_balance_negative_bezout_dividendsumfirstimaginary) = 0) \/ exists ge_signed_half_bezout_dividendsumfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_dividendsumfirst) = 2 * ge_signed_half_bezout_dividendsumfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_dividendsumfirstimaginary) = 0) /\ (ge_balance_negative_bezout_dividendsumfirstimaginary) = S ge_signed_half_bezout_dividendsumfirstimaginarydecode))) /\ ((ge_first_ip_bezout_dividendsum) + ge_balance_negative_bezout_dividendsumfirstimaginary = (ge_first_in_bezout_dividendsum) + ge_balance_positive_bezout_dividendsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_dividendsumsecond ge_representation_imaginary_code_bezout_dividendsumsecond. (((gr_second_product_bezout_dividend) = ((ge_representation_real_code_bezout_dividendsumsecond) + (ge_representation_imaginary_code_bezout_dividendsumsecond)) * S ((ge_representation_real_code_bezout_dividendsumsecond) + (ge_representation_imaginary_code_bezout_dividendsumsecond)) + ((ge_representation_imaginary_code_bezout_dividendsumsecond) + (ge_representation_imaginary_code_bezout_dividendsumsecond))) /\ ((exists ge_balance_positive_bezout_dividendsumsecondreal ge_balance_negative_bezout_dividendsumsecondreal. (((((ge_representation_real_code_bezout_dividendsumsecond) = 2 * (ge_balance_positive_bezout_dividendsumsecondreal) /\ (ge_balance_negative_bezout_dividendsumsecondreal) = 0) \/ exists ge_signed_half_bezout_dividendsumsecondrealdecode. (((ge_representation_real_code_bezout_dividendsumsecond) = 2 * ge_signed_half_bezout_dividendsumsecondrealdecode + 1 /\ (ge_balance_positive_bezout_dividendsumsecondreal) = 0) /\ (ge_balance_negative_bezout_dividendsumsecondreal) = S ge_signed_half_bezout_dividendsumsecondrealdecode))) /\ ((ge_second_rp_bezout_dividendsum) + ge_balance_negative_bezout_dividendsumsecondreal = (ge_second_rn_bezout_dividendsum) + ge_balance_positive_bezout_dividendsumsecondreal))) /\ (exists ge_balance_positive_bezout_dividendsumsecondimaginary ge_balance_negative_bezout_dividendsumsecondimaginary. (((((ge_representation_imaginary_code_bezout_dividendsumsecond) = 2 * (ge_balance_positive_bezout_dividendsumsecondimaginary) /\ (ge_balance_negative_bezout_dividendsumsecondimaginary) = 0) \/ exists ge_signed_half_bezout_dividendsumsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_dividendsumsecond) = 2 * ge_signed_half_bezout_dividendsumsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_dividendsumsecondimaginary) = 0) /\ (ge_balance_negative_bezout_dividendsumsecondimaginary) = S ge_signed_half_bezout_dividendsumsecondimaginarydecode))) /\ ((ge_second_ip_bezout_dividendsum) + ge_balance_negative_bezout_dividendsumsecondimaginary = (ge_second_in_bezout_dividendsum) + ge_balance_positive_bezout_dividendsumsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_dividendsumoutput ge_representation_imaginary_code_bezout_dividendsumoutput. (((g) = ((ge_representation_real_code_bezout_dividendsumoutput) + (ge_representation_imaginary_code_bezout_dividendsumoutput)) * S ((ge_representation_real_code_bezout_dividendsumoutput) + (ge_representation_imaginary_code_bezout_dividendsumoutput)) + ((ge_representation_imaginary_code_bezout_dividendsumoutput) + (ge_representation_imaginary_code_bezout_dividendsumoutput))) /\ ((exists ge_balance_positive_bezout_dividendsumoutputreal ge_balance_negative_bezout_dividendsumoutputreal. (((((ge_representation_real_code_bezout_dividendsumoutput) = 2 * (ge_balance_positive_bezout_dividendsumoutputreal) /\ (ge_balance_negative_bezout_dividendsumoutputreal) = 0) \/ exists ge_signed_half_bezout_dividendsumoutputrealdecode. (((ge_representation_real_code_bezout_dividendsumoutput) = 2 * ge_signed_half_bezout_dividendsumoutputrealdecode + 1 /\ (ge_balance_positive_bezout_dividendsumoutputreal) = 0) /\ (ge_balance_negative_bezout_dividendsumoutputreal) = S ge_signed_half_bezout_dividendsumoutputrealdecode))) /\ ((((ge_first_rp_bezout_dividendsum) + (ge_second_rp_bezout_dividendsum))) + ge_balance_negative_bezout_dividendsumoutputreal = (((ge_first_rn_bezout_dividendsum) + (ge_second_rn_bezout_dividendsum))) + ge_balance_positive_bezout_dividendsumoutputreal))) /\ (exists ge_balance_positive_bezout_dividendsumoutputimaginary ge_balance_negative_bezout_dividendsumoutputimaginary. (((((ge_representation_imaginary_code_bezout_dividendsumoutput) = 2 * (ge_balance_positive_bezout_dividendsumoutputimaginary) /\ (ge_balance_negative_bezout_dividendsumoutputimaginary) = 0) \/ exists ge_signed_half_bezout_dividendsumoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_dividendsumoutput) = 2 * ge_signed_half_bezout_dividendsumoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_dividendsumoutputimaginary) = 0) /\ (ge_balance_negative_bezout_dividendsumoutputimaginary) = S ge_signed_half_bezout_dividendsumoutputimaginarydecode))) /\ ((((ge_first_ip_bezout_dividendsum) + (ge_second_ip_bezout_dividendsum))) + ge_balance_negative_bezout_dividendsumoutputimaginary = (((ge_first_in_bezout_dividendsum) + (ge_second_in_bezout_dividendsum))) + ge_balance_positive_bezout_dividendsumoutputimaginary))))))))))))