gaussian_bezout_unit_divisor_cancel

Exact expanded first-order arithmetic statement

forall p a b c g u v. (exists ge_first_rp_gauss_given_product ge_first_rn_gauss_given_product ge_first_ip_gauss_given_product ge_first_in_gauss_given_product ge_second_rp_gauss_given_product ge_second_rn_gauss_given_product ge_second_ip_gauss_given_product ge_second_in_gauss_given_product. ((exists ge_representation_real_code_gauss_given_productfirst ge_representation_imaginary_code_gauss_given_productfirst. (((a) = ((ge_representation_real_code_gauss_given_productfirst) + (ge_representation_imaginary_code_gauss_given_productfirst)) * S ((ge_representation_real_code_gauss_given_productfirst) + (ge_representation_imaginary_code_gauss_given_productfirst)) + ((ge_representation_imaginary_code_gauss_given_productfirst) + (ge_representation_imaginary_code_gauss_given_productfirst))) /\ ((exists ge_balance_positive_gauss_given_productfirstreal ge_balance_negative_gauss_given_productfirstreal. (((((ge_representation_real_code_gauss_given_productfirst) = 2 * (ge_balance_positive_gauss_given_productfirstreal) /\ (ge_balance_negative_gauss_given_productfirstreal) = 0) \/ exists ge_signed_half_gauss_given_productfirstrealdecode. (((ge_representation_real_code_gauss_given_productfirst) = 2 * ge_signed_half_gauss_given_productfirstrealdecode + 1 /\ (ge_balance_positive_gauss_given_productfirstreal) = 0) /\ (ge_balance_negative_gauss_given_productfirstreal) = S ge_signed_half_gauss_given_productfirstrealdecode))) /\ ((ge_first_rp_gauss_given_product) + ge_balance_negative_gauss_given_productfirstreal = (ge_first_rn_gauss_given_product) + ge_balance_positive_gauss_given_productfirstreal))) /\ (exists ge_balance_positive_gauss_given_productfirstimaginary ge_balance_negative_gauss_given_productfirstimaginary. (((((ge_representation_imaginary_code_gauss_given_productfirst) = 2 * (ge_balance_positive_gauss_given_productfirstimaginary) /\ (ge_balance_negative_gauss_given_productfirstimaginary) = 0) \/ exists ge_signed_half_gauss_given_productfirstimaginarydecode. (((ge_representation_imaginary_code_gauss_given_productfirst) = 2 * ge_signed_half_gauss_given_productfirstimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_productfirstimaginary) = 0) /\ (ge_balance_negative_gauss_given_productfirstimaginary) = S ge_signed_half_gauss_given_productfirstimaginarydecode))) /\ ((ge_first_ip_gauss_given_product) + ge_balance_negative_gauss_given_productfirstimaginary = (ge_first_in_gauss_given_product) + ge_balance_positive_gauss_given_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_gauss_given_productsecond ge_representation_imaginary_code_gauss_given_productsecond. (((b) = ((ge_representation_real_code_gauss_given_productsecond) + (ge_representation_imaginary_code_gauss_given_productsecond)) * S ((ge_representation_real_code_gauss_given_productsecond) + (ge_representation_imaginary_code_gauss_given_productsecond)) + ((ge_representation_imaginary_code_gauss_given_productsecond) + (ge_representation_imaginary_code_gauss_given_productsecond))) /\ ((exists ge_balance_positive_gauss_given_productsecondreal ge_balance_negative_gauss_given_productsecondreal. (((((ge_representation_real_code_gauss_given_productsecond) = 2 * (ge_balance_positive_gauss_given_productsecondreal) /\ (ge_balance_negative_gauss_given_productsecondreal) = 0) \/ exists ge_signed_half_gauss_given_productsecondrealdecode. (((ge_representation_real_code_gauss_given_productsecond) = 2 * ge_signed_half_gauss_given_productsecondrealdecode + 1 /\ (ge_balance_positive_gauss_given_productsecondreal) = 0) /\ (ge_balance_negative_gauss_given_productsecondreal) = S ge_signed_half_gauss_given_productsecondrealdecode))) /\ ((ge_second_rp_gauss_given_product) + ge_balance_negative_gauss_given_productsecondreal = (ge_second_rn_gauss_given_product) + ge_balance_positive_gauss_given_productsecondreal))) /\ (exists ge_balance_positive_gauss_given_productsecondimaginary ge_balance_negative_gauss_given_productsecondimaginary. (((((ge_representation_imaginary_code_gauss_given_productsecond) = 2 * (ge_balance_positive_gauss_given_productsecondimaginary) /\ (ge_balance_negative_gauss_given_productsecondimaginary) = 0) \/ exists ge_signed_half_gauss_given_productsecondimaginarydecode. (((ge_representation_imaginary_code_gauss_given_productsecond) = 2 * ge_signed_half_gauss_given_productsecondimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_productsecondimaginary) = 0) /\ (ge_balance_negative_gauss_given_productsecondimaginary) = S ge_signed_half_gauss_given_productsecondimaginarydecode))) /\ ((ge_second_ip_gauss_given_product) + ge_balance_negative_gauss_given_productsecondimaginary = (ge_second_in_gauss_given_product) + ge_balance_positive_gauss_given_productsecondimaginary)))))) /\ (exists ge_representation_real_code_gauss_given_productoutput ge_representation_imaginary_code_gauss_given_productoutput. (((c) = ((ge_representation_real_code_gauss_given_productoutput) + (ge_representation_imaginary_code_gauss_given_productoutput)) * S ((ge_representation_real_code_gauss_given_productoutput) + (ge_representation_imaginary_code_gauss_given_productoutput)) + ((ge_representation_imaginary_code_gauss_given_productoutput) + (ge_representation_imaginary_code_gauss_given_productoutput))) /\ ((exists ge_balance_positive_gauss_given_productoutputreal ge_balance_negative_gauss_given_productoutputreal. (((((ge_representation_real_code_gauss_given_productoutput) = 2 * (ge_balance_positive_gauss_given_productoutputreal) /\ (ge_balance_negative_gauss_given_productoutputreal) = 0) \/ exists ge_signed_half_gauss_given_productoutputrealdecode. (((ge_representation_real_code_gauss_given_productoutput) = 2 * ge_signed_half_gauss_given_productoutputrealdecode + 1 /\ (ge_balance_positive_gauss_given_productoutputreal) = 0) /\ (ge_balance_negative_gauss_given_productoutputreal) = S ge_signed_half_gauss_given_productoutputrealdecode))) /\ ((((((((ge_first_rp_gauss_given_product) * (ge_second_rp_gauss_given_product))) + (((ge_first_rn_gauss_given_product) * (ge_second_rn_gauss_given_product))))) + (((((ge_first_ip_gauss_given_product) * (ge_second_in_gauss_given_product))) + (((ge_first_in_gauss_given_product) * (ge_second_ip_gauss_given_product))))))) + ge_balance_negative_gauss_given_productoutputreal = (((((((ge_first_rp_gauss_given_product) * (ge_second_rn_gauss_given_product))) + (((ge_first_rn_gauss_given_product) * (ge_second_rp_gauss_given_product))))) + (((((ge_first_ip_gauss_given_product) * (ge_second_ip_gauss_given_product))) + (((ge_first_in_gauss_given_product) * (ge_second_in_gauss_given_product))))))) + ge_balance_positive_gauss_given_productoutputreal))) /\ (exists ge_balance_positive_gauss_given_productoutputimaginary ge_balance_negative_gauss_given_productoutputimaginary. (((((ge_representation_imaginary_code_gauss_given_productoutput) = 2 * (ge_balance_positive_gauss_given_productoutputimaginary) /\ (ge_balance_negative_gauss_given_productoutputimaginary) = 0) \/ exists ge_signed_half_gauss_given_productoutputimaginarydecode. (((ge_representation_imaginary_code_gauss_given_productoutput) = 2 * ge_signed_half_gauss_given_productoutputimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_productoutputimaginary) = 0) /\ (ge_balance_negative_gauss_given_productoutputimaginary) = S ge_signed_half_gauss_given_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_gauss_given_product) * (ge_second_ip_gauss_given_product))) + (((ge_first_rn_gauss_given_product) * (ge_second_in_gauss_given_product))))) + (((((ge_first_ip_gauss_given_product) * (ge_second_rp_gauss_given_product))) + (((ge_first_in_gauss_given_product) * (ge_second_rn_gauss_given_product))))))) + ge_balance_negative_gauss_given_productoutputimaginary = (((((((ge_first_rp_gauss_given_product) * (ge_second_in_gauss_given_product))) + (((ge_first_rn_gauss_given_product) * (ge_second_ip_gauss_given_product))))) + (((((ge_first_ip_gauss_given_product) * (ge_second_rn_gauss_given_product))) + (((ge_first_in_gauss_given_product) * (ge_second_rp_gauss_given_product))))))) + ge_balance_positive_gauss_given_productoutputimaginary))))))))) -> (exists gr_quotient_gauss_given_divisor. (exists ge_first_rp_gauss_given_divisorproduct ge_first_rn_gauss_given_divisorproduct ge_first_ip_gauss_given_divisorproduct ge_first_in_gauss_given_divisorproduct ge_second_rp_gauss_given_divisorproduct ge_second_rn_gauss_given_divisorproduct ge_second_ip_gauss_given_divisorproduct ge_second_in_gauss_given_divisorproduct. ((exists ge_representation_real_code_gauss_given_divisorproductfirst ge_representation_imaginary_code_gauss_given_divisorproductfirst. (((p) = ((ge_representation_real_code_gauss_given_divisorproductfirst) + (ge_representation_imaginary_code_gauss_given_divisorproductfirst)) * S ((ge_representation_real_code_gauss_given_divisorproductfirst) + (ge_representation_imaginary_code_gauss_given_divisorproductfirst)) + ((ge_representation_imaginary_code_gauss_given_divisorproductfirst) + (ge_representation_imaginary_code_gauss_given_divisorproductfirst))) /\ ((exists ge_balance_positive_gauss_given_divisorproductfirstreal ge_balance_negative_gauss_given_divisorproductfirstreal. (((((ge_representation_real_code_gauss_given_divisorproductfirst) = 2 * (ge_balance_positive_gauss_given_divisorproductfirstreal) /\ (ge_balance_negative_gauss_given_divisorproductfirstreal) = 0) \/ exists ge_signed_half_gauss_given_divisorproductfirstrealdecode. (((ge_representation_real_code_gauss_given_divisorproductfirst) = 2 * ge_signed_half_gauss_given_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gauss_given_divisorproductfirstreal) = 0) /\ (ge_balance_negative_gauss_given_divisorproductfirstreal) = S ge_signed_half_gauss_given_divisorproductfirstrealdecode))) /\ ((ge_first_rp_gauss_given_divisorproduct) + ge_balance_negative_gauss_given_divisorproductfirstreal = (ge_first_rn_gauss_given_divisorproduct) + ge_balance_positive_gauss_given_divisorproductfirstreal))) /\ (exists ge_balance_positive_gauss_given_divisorproductfirstimaginary ge_balance_negative_gauss_given_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_gauss_given_divisorproductfirst) = 2 * (ge_balance_positive_gauss_given_divisorproductfirstimaginary) /\ (ge_balance_negative_gauss_given_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gauss_given_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gauss_given_divisorproductfirst) = 2 * ge_signed_half_gauss_given_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gauss_given_divisorproductfirstimaginary) = S ge_signed_half_gauss_given_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gauss_given_divisorproduct) + ge_balance_negative_gauss_given_divisorproductfirstimaginary = (ge_first_in_gauss_given_divisorproduct) + ge_balance_positive_gauss_given_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gauss_given_divisorproductsecond ge_representation_imaginary_code_gauss_given_divisorproductsecond. (((gr_quotient_gauss_given_divisor) = ((ge_representation_real_code_gauss_given_divisorproductsecond) + (ge_representation_imaginary_code_gauss_given_divisorproductsecond)) * S ((ge_representation_real_code_gauss_given_divisorproductsecond) + (ge_representation_imaginary_code_gauss_given_divisorproductsecond)) + ((ge_representation_imaginary_code_gauss_given_divisorproductsecond) + (ge_representation_imaginary_code_gauss_given_divisorproductsecond))) /\ ((exists ge_balance_positive_gauss_given_divisorproductsecondreal ge_balance_negative_gauss_given_divisorproductsecondreal. (((((ge_representation_real_code_gauss_given_divisorproductsecond) = 2 * (ge_balance_positive_gauss_given_divisorproductsecondreal) /\ (ge_balance_negative_gauss_given_divisorproductsecondreal) = 0) \/ exists ge_signed_half_gauss_given_divisorproductsecondrealdecode. (((ge_representation_real_code_gauss_given_divisorproductsecond) = 2 * ge_signed_half_gauss_given_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gauss_given_divisorproductsecondreal) = 0) /\ (ge_balance_negative_gauss_given_divisorproductsecondreal) = S ge_signed_half_gauss_given_divisorproductsecondrealdecode))) /\ ((ge_second_rp_gauss_given_divisorproduct) + ge_balance_negative_gauss_given_divisorproductsecondreal = (ge_second_rn_gauss_given_divisorproduct) + ge_balance_positive_gauss_given_divisorproductsecondreal))) /\ (exists ge_balance_positive_gauss_given_divisorproductsecondimaginary ge_balance_negative_gauss_given_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_gauss_given_divisorproductsecond) = 2 * (ge_balance_positive_gauss_given_divisorproductsecondimaginary) /\ (ge_balance_negative_gauss_given_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gauss_given_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gauss_given_divisorproductsecond) = 2 * ge_signed_half_gauss_given_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gauss_given_divisorproductsecondimaginary) = S ge_signed_half_gauss_given_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gauss_given_divisorproduct) + ge_balance_negative_gauss_given_divisorproductsecondimaginary = (ge_second_in_gauss_given_divisorproduct) + ge_balance_positive_gauss_given_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gauss_given_divisorproductoutput ge_representation_imaginary_code_gauss_given_divisorproductoutput. (((c) = ((ge_representation_real_code_gauss_given_divisorproductoutput) + (ge_representation_imaginary_code_gauss_given_divisorproductoutput)) * S ((ge_representation_real_code_gauss_given_divisorproductoutput) + (ge_representation_imaginary_code_gauss_given_divisorproductoutput)) + ((ge_representation_imaginary_code_gauss_given_divisorproductoutput) + (ge_representation_imaginary_code_gauss_given_divisorproductoutput))) /\ ((exists ge_balance_positive_gauss_given_divisorproductoutputreal ge_balance_negative_gauss_given_divisorproductoutputreal. (((((ge_representation_real_code_gauss_given_divisorproductoutput) = 2 * (ge_balance_positive_gauss_given_divisorproductoutputreal) /\ (ge_balance_negative_gauss_given_divisorproductoutputreal) = 0) \/ exists ge_signed_half_gauss_given_divisorproductoutputrealdecode. (((ge_representation_real_code_gauss_given_divisorproductoutput) = 2 * ge_signed_half_gauss_given_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gauss_given_divisorproductoutputreal) = 0) /\ (ge_balance_negative_gauss_given_divisorproductoutputreal) = S ge_signed_half_gauss_given_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gauss_given_divisorproduct) * (ge_second_rp_gauss_given_divisorproduct))) + (((ge_first_rn_gauss_given_divisorproduct) * (ge_second_rn_gauss_given_divisorproduct))))) + (((((ge_first_ip_gauss_given_divisorproduct) * (ge_second_in_gauss_given_divisorproduct))) + (((ge_first_in_gauss_given_divisorproduct) * (ge_second_ip_gauss_given_divisorproduct))))))) + ge_balance_negative_gauss_given_divisorproductoutputreal = (((((((ge_first_rp_gauss_given_divisorproduct) * (ge_second_rn_gauss_given_divisorproduct))) + (((ge_first_rn_gauss_given_divisorproduct) * (ge_second_rp_gauss_given_divisorproduct))))) + (((((ge_first_ip_gauss_given_divisorproduct) * (ge_second_ip_gauss_given_divisorproduct))) + (((ge_first_in_gauss_given_divisorproduct) * (ge_second_in_gauss_given_divisorproduct))))))) + ge_balance_positive_gauss_given_divisorproductoutputreal))) /\ (exists ge_balance_positive_gauss_given_divisorproductoutputimaginary ge_balance_negative_gauss_given_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_gauss_given_divisorproductoutput) = 2 * (ge_balance_positive_gauss_given_divisorproductoutputimaginary) /\ (ge_balance_negative_gauss_given_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gauss_given_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gauss_given_divisorproductoutput) = 2 * ge_signed_half_gauss_given_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gauss_given_divisorproductoutputimaginary) = S ge_signed_half_gauss_given_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gauss_given_divisorproduct) * (ge_second_ip_gauss_given_divisorproduct))) + (((ge_first_rn_gauss_given_divisorproduct) * (ge_second_in_gauss_given_divisorproduct))))) + (((((ge_first_ip_gauss_given_divisorproduct) * (ge_second_rp_gauss_given_divisorproduct))) + (((ge_first_in_gauss_given_divisorproduct) * (ge_second_rn_gauss_given_divisorproduct))))))) + ge_balance_negative_gauss_given_divisorproductoutputimaginary = (((((((ge_first_rp_gauss_given_divisorproduct) * (ge_second_in_gauss_given_divisorproduct))) + (((ge_first_rn_gauss_given_divisorproduct) * (ge_second_ip_gauss_given_divisorproduct))))) + (((((ge_first_ip_gauss_given_divisorproduct) * (ge_second_rn_gauss_given_divisorproduct))) + (((ge_first_in_gauss_given_divisorproduct) * (ge_second_rp_gauss_given_divisorproduct))))))) + ge_balance_positive_gauss_given_divisorproductoutputimaginary)))))))))) -> (exists gr_first_product_gauss_given_bezout gr_second_product_gauss_given_bezout. ((exists ge_first_rp_gauss_given_bezoutfirst ge_first_rn_gauss_given_bezoutfirst ge_first_ip_gauss_given_bezoutfirst ge_first_in_gauss_given_bezoutfirst ge_second_rp_gauss_given_bezoutfirst ge_second_rn_gauss_given_bezoutfirst ge_second_ip_gauss_given_bezoutfirst ge_second_in_gauss_given_bezoutfirst. ((exists ge_representation_real_code_gauss_given_bezoutfirstfirst ge_representation_imaginary_code_gauss_given_bezoutfirstfirst. (((p) = ((ge_representation_real_code_gauss_given_bezoutfirstfirst) + (ge_representation_imaginary_code_gauss_given_bezoutfirstfirst)) * S ((ge_representation_real_code_gauss_given_bezoutfirstfirst) + (ge_representation_imaginary_code_gauss_given_bezoutfirstfirst)) + ((ge_representation_imaginary_code_gauss_given_bezoutfirstfirst) + (ge_representation_imaginary_code_gauss_given_bezoutfirstfirst))) /\ ((exists ge_balance_positive_gauss_given_bezoutfirstfirstreal ge_balance_negative_gauss_given_bezoutfirstfirstreal. (((((ge_representation_real_code_gauss_given_bezoutfirstfirst) = 2 * (ge_balance_positive_gauss_given_bezoutfirstfirstreal) /\ (ge_balance_negative_gauss_given_bezoutfirstfirstreal) = 0) \/ exists ge_signed_half_gauss_given_bezoutfirstfirstrealdecode. (((ge_representation_real_code_gauss_given_bezoutfirstfirst) = 2 * ge_signed_half_gauss_given_bezoutfirstfirstrealdecode + 1 /\ (ge_balance_positive_gauss_given_bezoutfirstfirstreal) = 0) /\ (ge_balance_negative_gauss_given_bezoutfirstfirstreal) = S ge_signed_half_gauss_given_bezoutfirstfirstrealdecode))) /\ ((ge_first_rp_gauss_given_bezoutfirst) + ge_balance_negative_gauss_given_bezoutfirstfirstreal = (ge_first_rn_gauss_given_bezoutfirst) + ge_balance_positive_gauss_given_bezoutfirstfirstreal))) /\ (exists ge_balance_positive_gauss_given_bezoutfirstfirstimaginary ge_balance_negative_gauss_given_bezoutfirstfirstimaginary. (((((ge_representation_imaginary_code_gauss_given_bezoutfirstfirst) = 2 * (ge_balance_positive_gauss_given_bezoutfirstfirstimaginary) /\ (ge_balance_negative_gauss_given_bezoutfirstfirstimaginary) = 0) \/ exists ge_signed_half_gauss_given_bezoutfirstfirstimaginarydecode. (((ge_representation_imaginary_code_gauss_given_bezoutfirstfirst) = 2 * ge_signed_half_gauss_given_bezoutfirstfirstimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_bezoutfirstfirstimaginary) = 0) /\ (ge_balance_negative_gauss_given_bezoutfirstfirstimaginary) = S ge_signed_half_gauss_given_bezoutfirstfirstimaginarydecode))) /\ ((ge_first_ip_gauss_given_bezoutfirst) + ge_balance_negative_gauss_given_bezoutfirstfirstimaginary = (ge_first_in_gauss_given_bezoutfirst) + ge_balance_positive_gauss_given_bezoutfirstfirstimaginary)))))) /\ ((exists ge_representation_real_code_gauss_given_bezoutfirstsecond ge_representation_imaginary_code_gauss_given_bezoutfirstsecond. (((u) = ((ge_representation_real_code_gauss_given_bezoutfirstsecond) + (ge_representation_imaginary_code_gauss_given_bezoutfirstsecond)) * S ((ge_representation_real_code_gauss_given_bezoutfirstsecond) + (ge_representation_imaginary_code_gauss_given_bezoutfirstsecond)) + ((ge_representation_imaginary_code_gauss_given_bezoutfirstsecond) + (ge_representation_imaginary_code_gauss_given_bezoutfirstsecond))) /\ ((exists ge_balance_positive_gauss_given_bezoutfirstsecondreal ge_balance_negative_gauss_given_bezoutfirstsecondreal. (((((ge_representation_real_code_gauss_given_bezoutfirstsecond) = 2 * (ge_balance_positive_gauss_given_bezoutfirstsecondreal) /\ (ge_balance_negative_gauss_given_bezoutfirstsecondreal) = 0) \/ exists ge_signed_half_gauss_given_bezoutfirstsecondrealdecode. (((ge_representation_real_code_gauss_given_bezoutfirstsecond) = 2 * ge_signed_half_gauss_given_bezoutfirstsecondrealdecode + 1 /\ (ge_balance_positive_gauss_given_bezoutfirstsecondreal) = 0) /\ (ge_balance_negative_gauss_given_bezoutfirstsecondreal) = S ge_signed_half_gauss_given_bezoutfirstsecondrealdecode))) /\ ((ge_second_rp_gauss_given_bezoutfirst) + ge_balance_negative_gauss_given_bezoutfirstsecondreal = (ge_second_rn_gauss_given_bezoutfirst) + ge_balance_positive_gauss_given_bezoutfirstsecondreal))) /\ (exists ge_balance_positive_gauss_given_bezoutfirstsecondimaginary ge_balance_negative_gauss_given_bezoutfirstsecondimaginary. (((((ge_representation_imaginary_code_gauss_given_bezoutfirstsecond) = 2 * (ge_balance_positive_gauss_given_bezoutfirstsecondimaginary) /\ (ge_balance_negative_gauss_given_bezoutfirstsecondimaginary) = 0) \/ exists ge_signed_half_gauss_given_bezoutfirstsecondimaginarydecode. (((ge_representation_imaginary_code_gauss_given_bezoutfirstsecond) = 2 * ge_signed_half_gauss_given_bezoutfirstsecondimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_bezoutfirstsecondimaginary) = 0) /\ (ge_balance_negative_gauss_given_bezoutfirstsecondimaginary) = S ge_signed_half_gauss_given_bezoutfirstsecondimaginarydecode))) /\ ((ge_second_ip_gauss_given_bezoutfirst) + ge_balance_negative_gauss_given_bezoutfirstsecondimaginary = (ge_second_in_gauss_given_bezoutfirst) + ge_balance_positive_gauss_given_bezoutfirstsecondimaginary)))))) /\ (exists ge_representation_real_code_gauss_given_bezoutfirstoutput ge_representation_imaginary_code_gauss_given_bezoutfirstoutput. (((gr_first_product_gauss_given_bezout) = ((ge_representation_real_code_gauss_given_bezoutfirstoutput) + (ge_representation_imaginary_code_gauss_given_bezoutfirstoutput)) * S ((ge_representation_real_code_gauss_given_bezoutfirstoutput) + (ge_representation_imaginary_code_gauss_given_bezoutfirstoutput)) + ((ge_representation_imaginary_code_gauss_given_bezoutfirstoutput) + (ge_representation_imaginary_code_gauss_given_bezoutfirstoutput))) /\ ((exists ge_balance_positive_gauss_given_bezoutfirstoutputreal ge_balance_negative_gauss_given_bezoutfirstoutputreal. (((((ge_representation_real_code_gauss_given_bezoutfirstoutput) = 2 * (ge_balance_positive_gauss_given_bezoutfirstoutputreal) /\ (ge_balance_negative_gauss_given_bezoutfirstoutputreal) = 0) \/ exists ge_signed_half_gauss_given_bezoutfirstoutputrealdecode. (((ge_representation_real_code_gauss_given_bezoutfirstoutput) = 2 * ge_signed_half_gauss_given_bezoutfirstoutputrealdecode + 1 /\ (ge_balance_positive_gauss_given_bezoutfirstoutputreal) = 0) /\ (ge_balance_negative_gauss_given_bezoutfirstoutputreal) = S ge_signed_half_gauss_given_bezoutfirstoutputrealdecode))) /\ ((((((((ge_first_rp_gauss_given_bezoutfirst) * (ge_second_rp_gauss_given_bezoutfirst))) + (((ge_first_rn_gauss_given_bezoutfirst) * (ge_second_rn_gauss_given_bezoutfirst))))) + (((((ge_first_ip_gauss_given_bezoutfirst) * (ge_second_in_gauss_given_bezoutfirst))) + (((ge_first_in_gauss_given_bezoutfirst) * (ge_second_ip_gauss_given_bezoutfirst))))))) + ge_balance_negative_gauss_given_bezoutfirstoutputreal = (((((((ge_first_rp_gauss_given_bezoutfirst) * (ge_second_rn_gauss_given_bezoutfirst))) + (((ge_first_rn_gauss_given_bezoutfirst) * (ge_second_rp_gauss_given_bezoutfirst))))) + (((((ge_first_ip_gauss_given_bezoutfirst) * (ge_second_ip_gauss_given_bezoutfirst))) + (((ge_first_in_gauss_given_bezoutfirst) * (ge_second_in_gauss_given_bezoutfirst))))))) + ge_balance_positive_gauss_given_bezoutfirstoutputreal))) /\ (exists ge_balance_positive_gauss_given_bezoutfirstoutputimaginary ge_balance_negative_gauss_given_bezoutfirstoutputimaginary. (((((ge_representation_imaginary_code_gauss_given_bezoutfirstoutput) = 2 * (ge_balance_positive_gauss_given_bezoutfirstoutputimaginary) /\ (ge_balance_negative_gauss_given_bezoutfirstoutputimaginary) = 0) \/ exists ge_signed_half_gauss_given_bezoutfirstoutputimaginarydecode. (((ge_representation_imaginary_code_gauss_given_bezoutfirstoutput) = 2 * ge_signed_half_gauss_given_bezoutfirstoutputimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_bezoutfirstoutputimaginary) = 0) /\ (ge_balance_negative_gauss_given_bezoutfirstoutputimaginary) = S ge_signed_half_gauss_given_bezoutfirstoutputimaginarydecode))) /\ ((((((((ge_first_rp_gauss_given_bezoutfirst) * (ge_second_ip_gauss_given_bezoutfirst))) + (((ge_first_rn_gauss_given_bezoutfirst) * (ge_second_in_gauss_given_bezoutfirst))))) + (((((ge_first_ip_gauss_given_bezoutfirst) * (ge_second_rp_gauss_given_bezoutfirst))) + (((ge_first_in_gauss_given_bezoutfirst) * (ge_second_rn_gauss_given_bezoutfirst))))))) + ge_balance_negative_gauss_given_bezoutfirstoutputimaginary = (((((((ge_first_rp_gauss_given_bezoutfirst) * (ge_second_in_gauss_given_bezoutfirst))) + (((ge_first_rn_gauss_given_bezoutfirst) * (ge_second_ip_gauss_given_bezoutfirst))))) + (((((ge_first_ip_gauss_given_bezoutfirst) * (ge_second_rn_gauss_given_bezoutfirst))) + (((ge_first_in_gauss_given_bezoutfirst) * (ge_second_rp_gauss_given_bezoutfirst))))))) + ge_balance_positive_gauss_given_bezoutfirstoutputimaginary))))))))) /\ ((exists ge_first_rp_gauss_given_bezoutsecond ge_first_rn_gauss_given_bezoutsecond ge_first_ip_gauss_given_bezoutsecond ge_first_in_gauss_given_bezoutsecond ge_second_rp_gauss_given_bezoutsecond ge_second_rn_gauss_given_bezoutsecond ge_second_ip_gauss_given_bezoutsecond ge_second_in_gauss_given_bezoutsecond. ((exists ge_representation_real_code_gauss_given_bezoutsecondfirst ge_representation_imaginary_code_gauss_given_bezoutsecondfirst. (((a) = ((ge_representation_real_code_gauss_given_bezoutsecondfirst) + (ge_representation_imaginary_code_gauss_given_bezoutsecondfirst)) * S ((ge_representation_real_code_gauss_given_bezoutsecondfirst) + (ge_representation_imaginary_code_gauss_given_bezoutsecondfirst)) + ((ge_representation_imaginary_code_gauss_given_bezoutsecondfirst) + (ge_representation_imaginary_code_gauss_given_bezoutsecondfirst))) /\ ((exists ge_balance_positive_gauss_given_bezoutsecondfirstreal ge_balance_negative_gauss_given_bezoutsecondfirstreal. (((((ge_representation_real_code_gauss_given_bezoutsecondfirst) = 2 * (ge_balance_positive_gauss_given_bezoutsecondfirstreal) /\ (ge_balance_negative_gauss_given_bezoutsecondfirstreal) = 0) \/ exists ge_signed_half_gauss_given_bezoutsecondfirstrealdecode. (((ge_representation_real_code_gauss_given_bezoutsecondfirst) = 2 * ge_signed_half_gauss_given_bezoutsecondfirstrealdecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsecondfirstreal) = 0) /\ (ge_balance_negative_gauss_given_bezoutsecondfirstreal) = S ge_signed_half_gauss_given_bezoutsecondfirstrealdecode))) /\ ((ge_first_rp_gauss_given_bezoutsecond) + ge_balance_negative_gauss_given_bezoutsecondfirstreal = (ge_first_rn_gauss_given_bezoutsecond) + ge_balance_positive_gauss_given_bezoutsecondfirstreal))) /\ (exists ge_balance_positive_gauss_given_bezoutsecondfirstimaginary ge_balance_negative_gauss_given_bezoutsecondfirstimaginary. (((((ge_representation_imaginary_code_gauss_given_bezoutsecondfirst) = 2 * (ge_balance_positive_gauss_given_bezoutsecondfirstimaginary) /\ (ge_balance_negative_gauss_given_bezoutsecondfirstimaginary) = 0) \/ exists ge_signed_half_gauss_given_bezoutsecondfirstimaginarydecode. (((ge_representation_imaginary_code_gauss_given_bezoutsecondfirst) = 2 * ge_signed_half_gauss_given_bezoutsecondfirstimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsecondfirstimaginary) = 0) /\ (ge_balance_negative_gauss_given_bezoutsecondfirstimaginary) = S ge_signed_half_gauss_given_bezoutsecondfirstimaginarydecode))) /\ ((ge_first_ip_gauss_given_bezoutsecond) + ge_balance_negative_gauss_given_bezoutsecondfirstimaginary = (ge_first_in_gauss_given_bezoutsecond) + ge_balance_positive_gauss_given_bezoutsecondfirstimaginary)))))) /\ ((exists ge_representation_real_code_gauss_given_bezoutsecondsecond ge_representation_imaginary_code_gauss_given_bezoutsecondsecond. (((v) = ((ge_representation_real_code_gauss_given_bezoutsecondsecond) + (ge_representation_imaginary_code_gauss_given_bezoutsecondsecond)) * S ((ge_representation_real_code_gauss_given_bezoutsecondsecond) + (ge_representation_imaginary_code_gauss_given_bezoutsecondsecond)) + ((ge_representation_imaginary_code_gauss_given_bezoutsecondsecond) + (ge_representation_imaginary_code_gauss_given_bezoutsecondsecond))) /\ ((exists ge_balance_positive_gauss_given_bezoutsecondsecondreal ge_balance_negative_gauss_given_bezoutsecondsecondreal. (((((ge_representation_real_code_gauss_given_bezoutsecondsecond) = 2 * (ge_balance_positive_gauss_given_bezoutsecondsecondreal) /\ (ge_balance_negative_gauss_given_bezoutsecondsecondreal) = 0) \/ exists ge_signed_half_gauss_given_bezoutsecondsecondrealdecode. (((ge_representation_real_code_gauss_given_bezoutsecondsecond) = 2 * ge_signed_half_gauss_given_bezoutsecondsecondrealdecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsecondsecondreal) = 0) /\ (ge_balance_negative_gauss_given_bezoutsecondsecondreal) = S ge_signed_half_gauss_given_bezoutsecondsecondrealdecode))) /\ ((ge_second_rp_gauss_given_bezoutsecond) + ge_balance_negative_gauss_given_bezoutsecondsecondreal = (ge_second_rn_gauss_given_bezoutsecond) + ge_balance_positive_gauss_given_bezoutsecondsecondreal))) /\ (exists ge_balance_positive_gauss_given_bezoutsecondsecondimaginary ge_balance_negative_gauss_given_bezoutsecondsecondimaginary. (((((ge_representation_imaginary_code_gauss_given_bezoutsecondsecond) = 2 * (ge_balance_positive_gauss_given_bezoutsecondsecondimaginary) /\ (ge_balance_negative_gauss_given_bezoutsecondsecondimaginary) = 0) \/ exists ge_signed_half_gauss_given_bezoutsecondsecondimaginarydecode. (((ge_representation_imaginary_code_gauss_given_bezoutsecondsecond) = 2 * ge_signed_half_gauss_given_bezoutsecondsecondimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsecondsecondimaginary) = 0) /\ (ge_balance_negative_gauss_given_bezoutsecondsecondimaginary) = S ge_signed_half_gauss_given_bezoutsecondsecondimaginarydecode))) /\ ((ge_second_ip_gauss_given_bezoutsecond) + ge_balance_negative_gauss_given_bezoutsecondsecondimaginary = (ge_second_in_gauss_given_bezoutsecond) + ge_balance_positive_gauss_given_bezoutsecondsecondimaginary)))))) /\ (exists ge_representation_real_code_gauss_given_bezoutsecondoutput ge_representation_imaginary_code_gauss_given_bezoutsecondoutput. (((gr_second_product_gauss_given_bezout) = ((ge_representation_real_code_gauss_given_bezoutsecondoutput) + (ge_representation_imaginary_code_gauss_given_bezoutsecondoutput)) * S ((ge_representation_real_code_gauss_given_bezoutsecondoutput) + (ge_representation_imaginary_code_gauss_given_bezoutsecondoutput)) + ((ge_representation_imaginary_code_gauss_given_bezoutsecondoutput) + (ge_representation_imaginary_code_gauss_given_bezoutsecondoutput))) /\ ((exists ge_balance_positive_gauss_given_bezoutsecondoutputreal ge_balance_negative_gauss_given_bezoutsecondoutputreal. (((((ge_representation_real_code_gauss_given_bezoutsecondoutput) = 2 * (ge_balance_positive_gauss_given_bezoutsecondoutputreal) /\ (ge_balance_negative_gauss_given_bezoutsecondoutputreal) = 0) \/ exists ge_signed_half_gauss_given_bezoutsecondoutputrealdecode. (((ge_representation_real_code_gauss_given_bezoutsecondoutput) = 2 * ge_signed_half_gauss_given_bezoutsecondoutputrealdecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsecondoutputreal) = 0) /\ (ge_balance_negative_gauss_given_bezoutsecondoutputreal) = S ge_signed_half_gauss_given_bezoutsecondoutputrealdecode))) /\ ((((((((ge_first_rp_gauss_given_bezoutsecond) * (ge_second_rp_gauss_given_bezoutsecond))) + (((ge_first_rn_gauss_given_bezoutsecond) * (ge_second_rn_gauss_given_bezoutsecond))))) + (((((ge_first_ip_gauss_given_bezoutsecond) * (ge_second_in_gauss_given_bezoutsecond))) + (((ge_first_in_gauss_given_bezoutsecond) * (ge_second_ip_gauss_given_bezoutsecond))))))) + ge_balance_negative_gauss_given_bezoutsecondoutputreal = (((((((ge_first_rp_gauss_given_bezoutsecond) * (ge_second_rn_gauss_given_bezoutsecond))) + (((ge_first_rn_gauss_given_bezoutsecond) * (ge_second_rp_gauss_given_bezoutsecond))))) + (((((ge_first_ip_gauss_given_bezoutsecond) * (ge_second_ip_gauss_given_bezoutsecond))) + (((ge_first_in_gauss_given_bezoutsecond) * (ge_second_in_gauss_given_bezoutsecond))))))) + ge_balance_positive_gauss_given_bezoutsecondoutputreal))) /\ (exists ge_balance_positive_gauss_given_bezoutsecondoutputimaginary ge_balance_negative_gauss_given_bezoutsecondoutputimaginary. (((((ge_representation_imaginary_code_gauss_given_bezoutsecondoutput) = 2 * (ge_balance_positive_gauss_given_bezoutsecondoutputimaginary) /\ (ge_balance_negative_gauss_given_bezoutsecondoutputimaginary) = 0) \/ exists ge_signed_half_gauss_given_bezoutsecondoutputimaginarydecode. (((ge_representation_imaginary_code_gauss_given_bezoutsecondoutput) = 2 * ge_signed_half_gauss_given_bezoutsecondoutputimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsecondoutputimaginary) = 0) /\ (ge_balance_negative_gauss_given_bezoutsecondoutputimaginary) = S ge_signed_half_gauss_given_bezoutsecondoutputimaginarydecode))) /\ ((((((((ge_first_rp_gauss_given_bezoutsecond) * (ge_second_ip_gauss_given_bezoutsecond))) + (((ge_first_rn_gauss_given_bezoutsecond) * (ge_second_in_gauss_given_bezoutsecond))))) + (((((ge_first_ip_gauss_given_bezoutsecond) * (ge_second_rp_gauss_given_bezoutsecond))) + (((ge_first_in_gauss_given_bezoutsecond) * (ge_second_rn_gauss_given_bezoutsecond))))))) + ge_balance_negative_gauss_given_bezoutsecondoutputimaginary = (((((((ge_first_rp_gauss_given_bezoutsecond) * (ge_second_in_gauss_given_bezoutsecond))) + (((ge_first_rn_gauss_given_bezoutsecond) * (ge_second_ip_gauss_given_bezoutsecond))))) + (((((ge_first_ip_gauss_given_bezoutsecond) * (ge_second_rn_gauss_given_bezoutsecond))) + (((ge_first_in_gauss_given_bezoutsecond) * (ge_second_rp_gauss_given_bezoutsecond))))))) + ge_balance_positive_gauss_given_bezoutsecondoutputimaginary))))))))) /\ (exists ge_first_rp_gauss_given_bezoutsum ge_first_rn_gauss_given_bezoutsum ge_first_ip_gauss_given_bezoutsum ge_first_in_gauss_given_bezoutsum ge_second_rp_gauss_given_bezoutsum ge_second_rn_gauss_given_bezoutsum ge_second_ip_gauss_given_bezoutsum ge_second_in_gauss_given_bezoutsum. ((exists ge_representation_real_code_gauss_given_bezoutsumfirst ge_representation_imaginary_code_gauss_given_bezoutsumfirst. (((gr_first_product_gauss_given_bezout) = ((ge_representation_real_code_gauss_given_bezoutsumfirst) + (ge_representation_imaginary_code_gauss_given_bezoutsumfirst)) * S ((ge_representation_real_code_gauss_given_bezoutsumfirst) + (ge_representation_imaginary_code_gauss_given_bezoutsumfirst)) + ((ge_representation_imaginary_code_gauss_given_bezoutsumfirst) + (ge_representation_imaginary_code_gauss_given_bezoutsumfirst))) /\ ((exists ge_balance_positive_gauss_given_bezoutsumfirstreal ge_balance_negative_gauss_given_bezoutsumfirstreal. (((((ge_representation_real_code_gauss_given_bezoutsumfirst) = 2 * (ge_balance_positive_gauss_given_bezoutsumfirstreal) /\ (ge_balance_negative_gauss_given_bezoutsumfirstreal) = 0) \/ exists ge_signed_half_gauss_given_bezoutsumfirstrealdecode. (((ge_representation_real_code_gauss_given_bezoutsumfirst) = 2 * ge_signed_half_gauss_given_bezoutsumfirstrealdecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsumfirstreal) = 0) /\ (ge_balance_negative_gauss_given_bezoutsumfirstreal) = S ge_signed_half_gauss_given_bezoutsumfirstrealdecode))) /\ ((ge_first_rp_gauss_given_bezoutsum) + ge_balance_negative_gauss_given_bezoutsumfirstreal = (ge_first_rn_gauss_given_bezoutsum) + ge_balance_positive_gauss_given_bezoutsumfirstreal))) /\ (exists ge_balance_positive_gauss_given_bezoutsumfirstimaginary ge_balance_negative_gauss_given_bezoutsumfirstimaginary. (((((ge_representation_imaginary_code_gauss_given_bezoutsumfirst) = 2 * (ge_balance_positive_gauss_given_bezoutsumfirstimaginary) /\ (ge_balance_negative_gauss_given_bezoutsumfirstimaginary) = 0) \/ exists ge_signed_half_gauss_given_bezoutsumfirstimaginarydecode. (((ge_representation_imaginary_code_gauss_given_bezoutsumfirst) = 2 * ge_signed_half_gauss_given_bezoutsumfirstimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsumfirstimaginary) = 0) /\ (ge_balance_negative_gauss_given_bezoutsumfirstimaginary) = S ge_signed_half_gauss_given_bezoutsumfirstimaginarydecode))) /\ ((ge_first_ip_gauss_given_bezoutsum) + ge_balance_negative_gauss_given_bezoutsumfirstimaginary = (ge_first_in_gauss_given_bezoutsum) + ge_balance_positive_gauss_given_bezoutsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_gauss_given_bezoutsumsecond ge_representation_imaginary_code_gauss_given_bezoutsumsecond. (((gr_second_product_gauss_given_bezout) = ((ge_representation_real_code_gauss_given_bezoutsumsecond) + (ge_representation_imaginary_code_gauss_given_bezoutsumsecond)) * S ((ge_representation_real_code_gauss_given_bezoutsumsecond) + (ge_representation_imaginary_code_gauss_given_bezoutsumsecond)) + ((ge_representation_imaginary_code_gauss_given_bezoutsumsecond) + (ge_representation_imaginary_code_gauss_given_bezoutsumsecond))) /\ ((exists ge_balance_positive_gauss_given_bezoutsumsecondreal ge_balance_negative_gauss_given_bezoutsumsecondreal. (((((ge_representation_real_code_gauss_given_bezoutsumsecond) = 2 * (ge_balance_positive_gauss_given_bezoutsumsecondreal) /\ (ge_balance_negative_gauss_given_bezoutsumsecondreal) = 0) \/ exists ge_signed_half_gauss_given_bezoutsumsecondrealdecode. (((ge_representation_real_code_gauss_given_bezoutsumsecond) = 2 * ge_signed_half_gauss_given_bezoutsumsecondrealdecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsumsecondreal) = 0) /\ (ge_balance_negative_gauss_given_bezoutsumsecondreal) = S ge_signed_half_gauss_given_bezoutsumsecondrealdecode))) /\ ((ge_second_rp_gauss_given_bezoutsum) + ge_balance_negative_gauss_given_bezoutsumsecondreal = (ge_second_rn_gauss_given_bezoutsum) + ge_balance_positive_gauss_given_bezoutsumsecondreal))) /\ (exists ge_balance_positive_gauss_given_bezoutsumsecondimaginary ge_balance_negative_gauss_given_bezoutsumsecondimaginary. (((((ge_representation_imaginary_code_gauss_given_bezoutsumsecond) = 2 * (ge_balance_positive_gauss_given_bezoutsumsecondimaginary) /\ (ge_balance_negative_gauss_given_bezoutsumsecondimaginary) = 0) \/ exists ge_signed_half_gauss_given_bezoutsumsecondimaginarydecode. (((ge_representation_imaginary_code_gauss_given_bezoutsumsecond) = 2 * ge_signed_half_gauss_given_bezoutsumsecondimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsumsecondimaginary) = 0) /\ (ge_balance_negative_gauss_given_bezoutsumsecondimaginary) = S ge_signed_half_gauss_given_bezoutsumsecondimaginarydecode))) /\ ((ge_second_ip_gauss_given_bezoutsum) + ge_balance_negative_gauss_given_bezoutsumsecondimaginary = (ge_second_in_gauss_given_bezoutsum) + ge_balance_positive_gauss_given_bezoutsumsecondimaginary)))))) /\ (exists ge_representation_real_code_gauss_given_bezoutsumoutput ge_representation_imaginary_code_gauss_given_bezoutsumoutput. (((g) = ((ge_representation_real_code_gauss_given_bezoutsumoutput) + (ge_representation_imaginary_code_gauss_given_bezoutsumoutput)) * S ((ge_representation_real_code_gauss_given_bezoutsumoutput) + (ge_representation_imaginary_code_gauss_given_bezoutsumoutput)) + ((ge_representation_imaginary_code_gauss_given_bezoutsumoutput) + (ge_representation_imaginary_code_gauss_given_bezoutsumoutput))) /\ ((exists ge_balance_positive_gauss_given_bezoutsumoutputreal ge_balance_negative_gauss_given_bezoutsumoutputreal. (((((ge_representation_real_code_gauss_given_bezoutsumoutput) = 2 * (ge_balance_positive_gauss_given_bezoutsumoutputreal) /\ (ge_balance_negative_gauss_given_bezoutsumoutputreal) = 0) \/ exists ge_signed_half_gauss_given_bezoutsumoutputrealdecode. (((ge_representation_real_code_gauss_given_bezoutsumoutput) = 2 * ge_signed_half_gauss_given_bezoutsumoutputrealdecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsumoutputreal) = 0) /\ (ge_balance_negative_gauss_given_bezoutsumoutputreal) = S ge_signed_half_gauss_given_bezoutsumoutputrealdecode))) /\ ((((ge_first_rp_gauss_given_bezoutsum) + (ge_second_rp_gauss_given_bezoutsum))) + ge_balance_negative_gauss_given_bezoutsumoutputreal = (((ge_first_rn_gauss_given_bezoutsum) + (ge_second_rn_gauss_given_bezoutsum))) + ge_balance_positive_gauss_given_bezoutsumoutputreal))) /\ (exists ge_balance_positive_gauss_given_bezoutsumoutputimaginary ge_balance_negative_gauss_given_bezoutsumoutputimaginary. (((((ge_representation_imaginary_code_gauss_given_bezoutsumoutput) = 2 * (ge_balance_positive_gauss_given_bezoutsumoutputimaginary) /\ (ge_balance_negative_gauss_given_bezoutsumoutputimaginary) = 0) \/ exists ge_signed_half_gauss_given_bezoutsumoutputimaginarydecode. (((ge_representation_imaginary_code_gauss_given_bezoutsumoutput) = 2 * ge_signed_half_gauss_given_bezoutsumoutputimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_bezoutsumoutputimaginary) = 0) /\ (ge_balance_negative_gauss_given_bezoutsumoutputimaginary) = S ge_signed_half_gauss_given_bezoutsumoutputimaginarydecode))) /\ ((((ge_first_ip_gauss_given_bezoutsum) + (ge_second_ip_gauss_given_bezoutsum))) + ge_balance_negative_gauss_given_bezoutsumoutputimaginary = (((ge_first_in_gauss_given_bezoutsum) + (ge_second_in_gauss_given_bezoutsum))) + ge_balance_positive_gauss_given_bezoutsumoutputimaginary)))))))))))) -> (exists gr_inverse_gauss_given_unit. (exists ge_first_rp_gauss_given_unitidentity ge_first_rn_gauss_given_unitidentity ge_first_ip_gauss_given_unitidentity ge_first_in_gauss_given_unitidentity ge_second_rp_gauss_given_unitidentity ge_second_rn_gauss_given_unitidentity ge_second_ip_gauss_given_unitidentity ge_second_in_gauss_given_unitidentity. ((exists ge_representation_real_code_gauss_given_unitidentityfirst ge_representation_imaginary_code_gauss_given_unitidentityfirst. (((g) = ((ge_representation_real_code_gauss_given_unitidentityfirst) + (ge_representation_imaginary_code_gauss_given_unitidentityfirst)) * S ((ge_representation_real_code_gauss_given_unitidentityfirst) + (ge_representation_imaginary_code_gauss_given_unitidentityfirst)) + ((ge_representation_imaginary_code_gauss_given_unitidentityfirst) + (ge_representation_imaginary_code_gauss_given_unitidentityfirst))) /\ ((exists ge_balance_positive_gauss_given_unitidentityfirstreal ge_balance_negative_gauss_given_unitidentityfirstreal. (((((ge_representation_real_code_gauss_given_unitidentityfirst) = 2 * (ge_balance_positive_gauss_given_unitidentityfirstreal) /\ (ge_balance_negative_gauss_given_unitidentityfirstreal) = 0) \/ exists ge_signed_half_gauss_given_unitidentityfirstrealdecode. (((ge_representation_real_code_gauss_given_unitidentityfirst) = 2 * ge_signed_half_gauss_given_unitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gauss_given_unitidentityfirstreal) = 0) /\ (ge_balance_negative_gauss_given_unitidentityfirstreal) = S ge_signed_half_gauss_given_unitidentityfirstrealdecode))) /\ ((ge_first_rp_gauss_given_unitidentity) + ge_balance_negative_gauss_given_unitidentityfirstreal = (ge_first_rn_gauss_given_unitidentity) + ge_balance_positive_gauss_given_unitidentityfirstreal))) /\ (exists ge_balance_positive_gauss_given_unitidentityfirstimaginary ge_balance_negative_gauss_given_unitidentityfirstimaginary. (((((ge_representation_imaginary_code_gauss_given_unitidentityfirst) = 2 * (ge_balance_positive_gauss_given_unitidentityfirstimaginary) /\ (ge_balance_negative_gauss_given_unitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gauss_given_unitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gauss_given_unitidentityfirst) = 2 * ge_signed_half_gauss_given_unitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_unitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gauss_given_unitidentityfirstimaginary) = S ge_signed_half_gauss_given_unitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gauss_given_unitidentity) + ge_balance_negative_gauss_given_unitidentityfirstimaginary = (ge_first_in_gauss_given_unitidentity) + ge_balance_positive_gauss_given_unitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gauss_given_unitidentitysecond ge_representation_imaginary_code_gauss_given_unitidentitysecond. (((gr_inverse_gauss_given_unit) = ((ge_representation_real_code_gauss_given_unitidentitysecond) + (ge_representation_imaginary_code_gauss_given_unitidentitysecond)) * S ((ge_representation_real_code_gauss_given_unitidentitysecond) + (ge_representation_imaginary_code_gauss_given_unitidentitysecond)) + ((ge_representation_imaginary_code_gauss_given_unitidentitysecond) + (ge_representation_imaginary_code_gauss_given_unitidentitysecond))) /\ ((exists ge_balance_positive_gauss_given_unitidentitysecondreal ge_balance_negative_gauss_given_unitidentitysecondreal. (((((ge_representation_real_code_gauss_given_unitidentitysecond) = 2 * (ge_balance_positive_gauss_given_unitidentitysecondreal) /\ (ge_balance_negative_gauss_given_unitidentitysecondreal) = 0) \/ exists ge_signed_half_gauss_given_unitidentitysecondrealdecode. (((ge_representation_real_code_gauss_given_unitidentitysecond) = 2 * ge_signed_half_gauss_given_unitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gauss_given_unitidentitysecondreal) = 0) /\ (ge_balance_negative_gauss_given_unitidentitysecondreal) = S ge_signed_half_gauss_given_unitidentitysecondrealdecode))) /\ ((ge_second_rp_gauss_given_unitidentity) + ge_balance_negative_gauss_given_unitidentitysecondreal = (ge_second_rn_gauss_given_unitidentity) + ge_balance_positive_gauss_given_unitidentitysecondreal))) /\ (exists ge_balance_positive_gauss_given_unitidentitysecondimaginary ge_balance_negative_gauss_given_unitidentitysecondimaginary. (((((ge_representation_imaginary_code_gauss_given_unitidentitysecond) = 2 * (ge_balance_positive_gauss_given_unitidentitysecondimaginary) /\ (ge_balance_negative_gauss_given_unitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gauss_given_unitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gauss_given_unitidentitysecond) = 2 * ge_signed_half_gauss_given_unitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_unitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gauss_given_unitidentitysecondimaginary) = S ge_signed_half_gauss_given_unitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gauss_given_unitidentity) + ge_balance_negative_gauss_given_unitidentitysecondimaginary = (ge_second_in_gauss_given_unitidentity) + ge_balance_positive_gauss_given_unitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gauss_given_unitidentityoutput ge_representation_imaginary_code_gauss_given_unitidentityoutput. (((6) = ((ge_representation_real_code_gauss_given_unitidentityoutput) + (ge_representation_imaginary_code_gauss_given_unitidentityoutput)) * S ((ge_representation_real_code_gauss_given_unitidentityoutput) + (ge_representation_imaginary_code_gauss_given_unitidentityoutput)) + ((ge_representation_imaginary_code_gauss_given_unitidentityoutput) + (ge_representation_imaginary_code_gauss_given_unitidentityoutput))) /\ ((exists ge_balance_positive_gauss_given_unitidentityoutputreal ge_balance_negative_gauss_given_unitidentityoutputreal. (((((ge_representation_real_code_gauss_given_unitidentityoutput) = 2 * (ge_balance_positive_gauss_given_unitidentityoutputreal) /\ (ge_balance_negative_gauss_given_unitidentityoutputreal) = 0) \/ exists ge_signed_half_gauss_given_unitidentityoutputrealdecode. (((ge_representation_real_code_gauss_given_unitidentityoutput) = 2 * ge_signed_half_gauss_given_unitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gauss_given_unitidentityoutputreal) = 0) /\ (ge_balance_negative_gauss_given_unitidentityoutputreal) = S ge_signed_half_gauss_given_unitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gauss_given_unitidentity) * (ge_second_rp_gauss_given_unitidentity))) + (((ge_first_rn_gauss_given_unitidentity) * (ge_second_rn_gauss_given_unitidentity))))) + (((((ge_first_ip_gauss_given_unitidentity) * (ge_second_in_gauss_given_unitidentity))) + (((ge_first_in_gauss_given_unitidentity) * (ge_second_ip_gauss_given_unitidentity))))))) + ge_balance_negative_gauss_given_unitidentityoutputreal = (((((((ge_first_rp_gauss_given_unitidentity) * (ge_second_rn_gauss_given_unitidentity))) + (((ge_first_rn_gauss_given_unitidentity) * (ge_second_rp_gauss_given_unitidentity))))) + (((((ge_first_ip_gauss_given_unitidentity) * (ge_second_ip_gauss_given_unitidentity))) + (((ge_first_in_gauss_given_unitidentity) * (ge_second_in_gauss_given_unitidentity))))))) + ge_balance_positive_gauss_given_unitidentityoutputreal))) /\ (exists ge_balance_positive_gauss_given_unitidentityoutputimaginary ge_balance_negative_gauss_given_unitidentityoutputimaginary. (((((ge_representation_imaginary_code_gauss_given_unitidentityoutput) = 2 * (ge_balance_positive_gauss_given_unitidentityoutputimaginary) /\ (ge_balance_negative_gauss_given_unitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gauss_given_unitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gauss_given_unitidentityoutput) = 2 * ge_signed_half_gauss_given_unitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gauss_given_unitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gauss_given_unitidentityoutputimaginary) = S ge_signed_half_gauss_given_unitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gauss_given_unitidentity) * (ge_second_ip_gauss_given_unitidentity))) + (((ge_first_rn_gauss_given_unitidentity) * (ge_second_in_gauss_given_unitidentity))))) + (((((ge_first_ip_gauss_given_unitidentity) * (ge_second_rp_gauss_given_unitidentity))) + (((ge_first_in_gauss_given_unitidentity) * (ge_second_rn_gauss_given_unitidentity))))))) + ge_balance_negative_gauss_given_unitidentityoutputimaginary = (((((((ge_first_rp_gauss_given_unitidentity) * (ge_second_in_gauss_given_unitidentity))) + (((ge_first_rn_gauss_given_unitidentity) * (ge_second_ip_gauss_given_unitidentity))))) + (((((ge_first_ip_gauss_given_unitidentity) * (ge_second_rn_gauss_given_unitidentity))) + (((ge_first_in_gauss_given_unitidentity) * (ge_second_rp_gauss_given_unitidentity))))))) + ge_balance_positive_gauss_given_unitidentityoutputimaginary)))))))))) -> (exists gr_quotient_gauss_result. (exists ge_first_rp_gauss_resultproduct ge_first_rn_gauss_resultproduct ge_first_ip_gauss_resultproduct ge_first_in_gauss_resultproduct ge_second_rp_gauss_resultproduct ge_second_rn_gauss_resultproduct ge_second_ip_gauss_resultproduct ge_second_in_gauss_resultproduct. ((exists ge_representation_real_code_gauss_resultproductfirst ge_representation_imaginary_code_gauss_resultproductfirst. (((p) = ((ge_representation_real_code_gauss_resultproductfirst) + (ge_representation_imaginary_code_gauss_resultproductfirst)) * S ((ge_representation_real_code_gauss_resultproductfirst) + (ge_representation_imaginary_code_gauss_resultproductfirst)) + ((ge_representation_imaginary_code_gauss_resultproductfirst) + (ge_representation_imaginary_code_gauss_resultproductfirst))) /\ ((exists ge_balance_positive_gauss_resultproductfirstreal ge_balance_negative_gauss_resultproductfirstreal. (((((ge_representation_real_code_gauss_resultproductfirst) = 2 * (ge_balance_positive_gauss_resultproductfirstreal) /\ (ge_balance_negative_gauss_resultproductfirstreal) = 0) \/ exists ge_signed_half_gauss_resultproductfirstrealdecode. (((ge_representation_real_code_gauss_resultproductfirst) = 2 * ge_signed_half_gauss_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_gauss_resultproductfirstreal) = 0) /\ (ge_balance_negative_gauss_resultproductfirstreal) = S ge_signed_half_gauss_resultproductfirstrealdecode))) /\ ((ge_first_rp_gauss_resultproduct) + ge_balance_negative_gauss_resultproductfirstreal = (ge_first_rn_gauss_resultproduct) + ge_balance_positive_gauss_resultproductfirstreal))) /\ (exists ge_balance_positive_gauss_resultproductfirstimaginary ge_balance_negative_gauss_resultproductfirstimaginary. (((((ge_representation_imaginary_code_gauss_resultproductfirst) = 2 * (ge_balance_positive_gauss_resultproductfirstimaginary) /\ (ge_balance_negative_gauss_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_gauss_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_gauss_resultproductfirst) = 2 * ge_signed_half_gauss_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gauss_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_gauss_resultproductfirstimaginary) = S ge_signed_half_gauss_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_gauss_resultproduct) + ge_balance_negative_gauss_resultproductfirstimaginary = (ge_first_in_gauss_resultproduct) + ge_balance_positive_gauss_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gauss_resultproductsecond ge_representation_imaginary_code_gauss_resultproductsecond. (((gr_quotient_gauss_result) = ((ge_representation_real_code_gauss_resultproductsecond) + (ge_representation_imaginary_code_gauss_resultproductsecond)) * S ((ge_representation_real_code_gauss_resultproductsecond) + (ge_representation_imaginary_code_gauss_resultproductsecond)) + ((ge_representation_imaginary_code_gauss_resultproductsecond) + (ge_representation_imaginary_code_gauss_resultproductsecond))) /\ ((exists ge_balance_positive_gauss_resultproductsecondreal ge_balance_negative_gauss_resultproductsecondreal. (((((ge_representation_real_code_gauss_resultproductsecond) = 2 * (ge_balance_positive_gauss_resultproductsecondreal) /\ (ge_balance_negative_gauss_resultproductsecondreal) = 0) \/ exists ge_signed_half_gauss_resultproductsecondrealdecode. (((ge_representation_real_code_gauss_resultproductsecond) = 2 * ge_signed_half_gauss_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_gauss_resultproductsecondreal) = 0) /\ (ge_balance_negative_gauss_resultproductsecondreal) = S ge_signed_half_gauss_resultproductsecondrealdecode))) /\ ((ge_second_rp_gauss_resultproduct) + ge_balance_negative_gauss_resultproductsecondreal = (ge_second_rn_gauss_resultproduct) + ge_balance_positive_gauss_resultproductsecondreal))) /\ (exists ge_balance_positive_gauss_resultproductsecondimaginary ge_balance_negative_gauss_resultproductsecondimaginary. (((((ge_representation_imaginary_code_gauss_resultproductsecond) = 2 * (ge_balance_positive_gauss_resultproductsecondimaginary) /\ (ge_balance_negative_gauss_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_gauss_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_gauss_resultproductsecond) = 2 * ge_signed_half_gauss_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gauss_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_gauss_resultproductsecondimaginary) = S ge_signed_half_gauss_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_gauss_resultproduct) + ge_balance_negative_gauss_resultproductsecondimaginary = (ge_second_in_gauss_resultproduct) + ge_balance_positive_gauss_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gauss_resultproductoutput ge_representation_imaginary_code_gauss_resultproductoutput. (((b) = ((ge_representation_real_code_gauss_resultproductoutput) + (ge_representation_imaginary_code_gauss_resultproductoutput)) * S ((ge_representation_real_code_gauss_resultproductoutput) + (ge_representation_imaginary_code_gauss_resultproductoutput)) + ((ge_representation_imaginary_code_gauss_resultproductoutput) + (ge_representation_imaginary_code_gauss_resultproductoutput))) /\ ((exists ge_balance_positive_gauss_resultproductoutputreal ge_balance_negative_gauss_resultproductoutputreal. (((((ge_representation_real_code_gauss_resultproductoutput) = 2 * (ge_balance_positive_gauss_resultproductoutputreal) /\ (ge_balance_negative_gauss_resultproductoutputreal) = 0) \/ exists ge_signed_half_gauss_resultproductoutputrealdecode. (((ge_representation_real_code_gauss_resultproductoutput) = 2 * ge_signed_half_gauss_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_gauss_resultproductoutputreal) = 0) /\ (ge_balance_negative_gauss_resultproductoutputreal) = S ge_signed_half_gauss_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_gauss_resultproduct) * (ge_second_rp_gauss_resultproduct))) + (((ge_first_rn_gauss_resultproduct) * (ge_second_rn_gauss_resultproduct))))) + (((((ge_first_ip_gauss_resultproduct) * (ge_second_in_gauss_resultproduct))) + (((ge_first_in_gauss_resultproduct) * (ge_second_ip_gauss_resultproduct))))))) + ge_balance_negative_gauss_resultproductoutputreal = (((((((ge_first_rp_gauss_resultproduct) * (ge_second_rn_gauss_resultproduct))) + (((ge_first_rn_gauss_resultproduct) * (ge_second_rp_gauss_resultproduct))))) + (((((ge_first_ip_gauss_resultproduct) * (ge_second_ip_gauss_resultproduct))) + (((ge_first_in_gauss_resultproduct) * (ge_second_in_gauss_resultproduct))))))) + ge_balance_positive_gauss_resultproductoutputreal))) /\ (exists ge_balance_positive_gauss_resultproductoutputimaginary ge_balance_negative_gauss_resultproductoutputimaginary. (((((ge_representation_imaginary_code_gauss_resultproductoutput) = 2 * (ge_balance_positive_gauss_resultproductoutputimaginary) /\ (ge_balance_negative_gauss_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_gauss_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_gauss_resultproductoutput) = 2 * ge_signed_half_gauss_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gauss_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_gauss_resultproductoutputimaginary) = S ge_signed_half_gauss_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gauss_resultproduct) * (ge_second_ip_gauss_resultproduct))) + (((ge_first_rn_gauss_resultproduct) * (ge_second_in_gauss_resultproduct))))) + (((((ge_first_ip_gauss_resultproduct) * (ge_second_rp_gauss_resultproduct))) + (((ge_first_in_gauss_resultproduct) * (ge_second_rn_gauss_resultproduct))))))) + ge_balance_negative_gauss_resultproductoutputimaginary = (((((((ge_first_rp_gauss_resultproduct) * (ge_second_in_gauss_resultproduct))) + (((ge_first_rn_gauss_resultproduct) * (ge_second_ip_gauss_resultproduct))))) + (((((ge_first_ip_gauss_resultproduct) * (ge_second_rn_gauss_resultproduct))) + (((ge_first_in_gauss_resultproduct) * (ge_second_rp_gauss_resultproduct))))))) + ge_balance_positive_gauss_resultproductoutputimaginary))))))))))