gaussian_gcd_bezout_exists

Exact expanded first-order arithmetic statement

forall a b. (exists ge_real_positive_gcd_exists_first ge_real_negative_gcd_exists_first ge_imaginary_positive_gcd_exists_first ge_imaginary_negative_gcd_exists_first. (exists ge_real_code_gcd_exists_firstdecode ge_imaginary_code_gcd_exists_firstdecode. (((a) = ((ge_real_code_gcd_exists_firstdecode) + (ge_imaginary_code_gcd_exists_firstdecode)) * S ((ge_real_code_gcd_exists_firstdecode) + (ge_imaginary_code_gcd_exists_firstdecode)) + ((ge_imaginary_code_gcd_exists_firstdecode) + (ge_imaginary_code_gcd_exists_firstdecode))) /\ (((((ge_real_code_gcd_exists_firstdecode) = 2 * (ge_real_positive_gcd_exists_first) /\ (ge_real_negative_gcd_exists_first) = 0) \/ exists ge_signed_half_ge_gcd_exists_firstdecode_real. (((ge_real_code_gcd_exists_firstdecode) = 2 * ge_signed_half_ge_gcd_exists_firstdecode_real + 1 /\ (ge_real_positive_gcd_exists_first) = 0) /\ (ge_real_negative_gcd_exists_first) = S ge_signed_half_ge_gcd_exists_firstdecode_real))) /\ ((((ge_imaginary_code_gcd_exists_firstdecode) = 2 * (ge_imaginary_positive_gcd_exists_first) /\ (ge_imaginary_negative_gcd_exists_first) = 0) \/ exists ge_signed_half_ge_gcd_exists_firstdecode_imaginary. (((ge_imaginary_code_gcd_exists_firstdecode) = 2 * ge_signed_half_ge_gcd_exists_firstdecode_imaginary + 1 /\ (ge_imaginary_positive_gcd_exists_first) = 0) /\ (ge_imaginary_negative_gcd_exists_first) = S ge_signed_half_ge_gcd_exists_firstdecode_imaginary))))))) -> (exists ge_real_positive_gcd_exists_second ge_real_negative_gcd_exists_second ge_imaginary_positive_gcd_exists_second ge_imaginary_negative_gcd_exists_second. (exists ge_real_code_gcd_exists_seconddecode ge_imaginary_code_gcd_exists_seconddecode. (((b) = ((ge_real_code_gcd_exists_seconddecode) + (ge_imaginary_code_gcd_exists_seconddecode)) * S ((ge_real_code_gcd_exists_seconddecode) + (ge_imaginary_code_gcd_exists_seconddecode)) + ((ge_imaginary_code_gcd_exists_seconddecode) + (ge_imaginary_code_gcd_exists_seconddecode))) /\ (((((ge_real_code_gcd_exists_seconddecode) = 2 * (ge_real_positive_gcd_exists_second) /\ (ge_real_negative_gcd_exists_second) = 0) \/ exists ge_signed_half_ge_gcd_exists_seconddecode_real. (((ge_real_code_gcd_exists_seconddecode) = 2 * ge_signed_half_ge_gcd_exists_seconddecode_real + 1 /\ (ge_real_positive_gcd_exists_second) = 0) /\ (ge_real_negative_gcd_exists_second) = S ge_signed_half_ge_gcd_exists_seconddecode_real))) /\ ((((ge_imaginary_code_gcd_exists_seconddecode) = 2 * (ge_imaginary_positive_gcd_exists_second) /\ (ge_imaginary_negative_gcd_exists_second) = 0) \/ exists ge_signed_half_ge_gcd_exists_seconddecode_imaginary. (((ge_imaginary_code_gcd_exists_seconddecode) = 2 * ge_signed_half_ge_gcd_exists_seconddecode_imaginary + 1 /\ (ge_imaginary_positive_gcd_exists_second) = 0) /\ (ge_imaginary_negative_gcd_exists_second) = S ge_signed_half_ge_gcd_exists_seconddecode_imaginary))))))) -> (exists gr_gcd_gcd_exists_result gr_first_coefficient_gcd_exists_result gr_second_coefficient_gcd_exists_result. ((((exists gr_quotient_gcd_exists_resultgcdfirst. (exists ge_first_rp_gcd_exists_resultgcdfirstproduct ge_first_rn_gcd_exists_resultgcdfirstproduct ge_first_ip_gcd_exists_resultgcdfirstproduct ge_first_in_gcd_exists_resultgcdfirstproduct ge_second_rp_gcd_exists_resultgcdfirstproduct ge_second_rn_gcd_exists_resultgcdfirstproduct ge_second_ip_gcd_exists_resultgcdfirstproduct ge_second_in_gcd_exists_resultgcdfirstproduct. ((exists ge_representation_real_code_gcd_exists_resultgcdfirstproductfirst ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductfirst. (((gr_gcd_gcd_exists_result) = ((ge_representation_real_code_gcd_exists_resultgcdfirstproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductfirst)) * S ((ge_representation_real_code_gcd_exists_resultgcdfirstproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductfirst)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductfirst))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdfirstproductfirstreal ge_balance_negative_gcd_exists_resultgcdfirstproductfirstreal. (((((ge_representation_real_code_gcd_exists_resultgcdfirstproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdfirstproductfirstreal) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdfirstproductfirstrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdfirstproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdfirstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdfirstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductfirstreal) = S ge_signed_half_gcd_exists_resultgcdfirstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_exists_resultgcdfirstproduct) + ge_balance_negative_gcd_exists_resultgcdfirstproductfirstreal = (ge_first_rn_gcd_exists_resultgcdfirstproduct) + ge_balance_positive_gcd_exists_resultgcdfirstproductfirstreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdfirstproductfirstimaginary ge_balance_negative_gcd_exists_resultgcdfirstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdfirstproductfirstimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdfirstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdfirstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdfirstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductfirstimaginary) = S ge_signed_half_gcd_exists_resultgcdfirstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_exists_resultgcdfirstproduct) + ge_balance_negative_gcd_exists_resultgcdfirstproductfirstimaginary = (ge_first_in_gcd_exists_resultgcdfirstproduct) + ge_balance_positive_gcd_exists_resultgcdfirstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_exists_resultgcdfirstproductsecond ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductsecond. (((gr_quotient_gcd_exists_resultgcdfirst) = ((ge_representation_real_code_gcd_exists_resultgcdfirstproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductsecond)) * S ((ge_representation_real_code_gcd_exists_resultgcdfirstproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductsecond)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductsecond))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdfirstproductsecondreal ge_balance_negative_gcd_exists_resultgcdfirstproductsecondreal. (((((ge_representation_real_code_gcd_exists_resultgcdfirstproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdfirstproductsecondreal) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdfirstproductsecondrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdfirstproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdfirstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdfirstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductsecondreal) = S ge_signed_half_gcd_exists_resultgcdfirstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_exists_resultgcdfirstproduct) + ge_balance_negative_gcd_exists_resultgcdfirstproductsecondreal = (ge_second_rn_gcd_exists_resultgcdfirstproduct) + ge_balance_positive_gcd_exists_resultgcdfirstproductsecondreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdfirstproductsecondimaginary ge_balance_negative_gcd_exists_resultgcdfirstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdfirstproductsecondimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdfirstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdfirstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdfirstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductsecondimaginary) = S ge_signed_half_gcd_exists_resultgcdfirstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_exists_resultgcdfirstproduct) + ge_balance_negative_gcd_exists_resultgcdfirstproductsecondimaginary = (ge_second_in_gcd_exists_resultgcdfirstproduct) + ge_balance_positive_gcd_exists_resultgcdfirstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_exists_resultgcdfirstproductoutput ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductoutput. (((a) = ((ge_representation_real_code_gcd_exists_resultgcdfirstproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductoutput)) * S ((ge_representation_real_code_gcd_exists_resultgcdfirstproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductoutput)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductoutput))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdfirstproductoutputreal ge_balance_negative_gcd_exists_resultgcdfirstproductoutputreal. (((((ge_representation_real_code_gcd_exists_resultgcdfirstproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdfirstproductoutputreal) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdfirstproductoutputrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdfirstproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdfirstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdfirstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductoutputreal) = S ge_signed_half_gcd_exists_resultgcdfirstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdfirstproduct) * (ge_second_rp_gcd_exists_resultgcdfirstproduct))) + (((ge_first_rn_gcd_exists_resultgcdfirstproduct) * (ge_second_rn_gcd_exists_resultgcdfirstproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdfirstproduct) * (ge_second_in_gcd_exists_resultgcdfirstproduct))) + (((ge_first_in_gcd_exists_resultgcdfirstproduct) * (ge_second_ip_gcd_exists_resultgcdfirstproduct))))))) + ge_balance_negative_gcd_exists_resultgcdfirstproductoutputreal = (((((((ge_first_rp_gcd_exists_resultgcdfirstproduct) * (ge_second_rn_gcd_exists_resultgcdfirstproduct))) + (((ge_first_rn_gcd_exists_resultgcdfirstproduct) * (ge_second_rp_gcd_exists_resultgcdfirstproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdfirstproduct) * (ge_second_ip_gcd_exists_resultgcdfirstproduct))) + (((ge_first_in_gcd_exists_resultgcdfirstproduct) * (ge_second_in_gcd_exists_resultgcdfirstproduct))))))) + ge_balance_positive_gcd_exists_resultgcdfirstproductoutputreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdfirstproductoutputimaginary ge_balance_negative_gcd_exists_resultgcdfirstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdfirstproductoutputimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdfirstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdfirstproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdfirstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdfirstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdfirstproductoutputimaginary) = S ge_signed_half_gcd_exists_resultgcdfirstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdfirstproduct) * (ge_second_ip_gcd_exists_resultgcdfirstproduct))) + (((ge_first_rn_gcd_exists_resultgcdfirstproduct) * (ge_second_in_gcd_exists_resultgcdfirstproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdfirstproduct) * (ge_second_rp_gcd_exists_resultgcdfirstproduct))) + (((ge_first_in_gcd_exists_resultgcdfirstproduct) * (ge_second_rn_gcd_exists_resultgcdfirstproduct))))))) + ge_balance_negative_gcd_exists_resultgcdfirstproductoutputimaginary = (((((((ge_first_rp_gcd_exists_resultgcdfirstproduct) * (ge_second_in_gcd_exists_resultgcdfirstproduct))) + (((ge_first_rn_gcd_exists_resultgcdfirstproduct) * (ge_second_ip_gcd_exists_resultgcdfirstproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdfirstproduct) * (ge_second_rn_gcd_exists_resultgcdfirstproduct))) + (((ge_first_in_gcd_exists_resultgcdfirstproduct) * (ge_second_rp_gcd_exists_resultgcdfirstproduct))))))) + ge_balance_positive_gcd_exists_resultgcdfirstproductoutputimaginary)))))))))) /\ ((exists gr_quotient_gcd_exists_resultgcdsecond. (exists ge_first_rp_gcd_exists_resultgcdsecondproduct ge_first_rn_gcd_exists_resultgcdsecondproduct ge_first_ip_gcd_exists_resultgcdsecondproduct ge_first_in_gcd_exists_resultgcdsecondproduct ge_second_rp_gcd_exists_resultgcdsecondproduct ge_second_rn_gcd_exists_resultgcdsecondproduct ge_second_ip_gcd_exists_resultgcdsecondproduct ge_second_in_gcd_exists_resultgcdsecondproduct. ((exists ge_representation_real_code_gcd_exists_resultgcdsecondproductfirst ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductfirst. (((gr_gcd_gcd_exists_result) = ((ge_representation_real_code_gcd_exists_resultgcdsecondproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductfirst)) * S ((ge_representation_real_code_gcd_exists_resultgcdsecondproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductfirst)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductfirst))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdsecondproductfirstreal ge_balance_negative_gcd_exists_resultgcdsecondproductfirstreal. (((((ge_representation_real_code_gcd_exists_resultgcdsecondproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdsecondproductfirstreal) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdsecondproductfirstrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdsecondproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdsecondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdsecondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductfirstreal) = S ge_signed_half_gcd_exists_resultgcdsecondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_exists_resultgcdsecondproduct) + ge_balance_negative_gcd_exists_resultgcdsecondproductfirstreal = (ge_first_rn_gcd_exists_resultgcdsecondproduct) + ge_balance_positive_gcd_exists_resultgcdsecondproductfirstreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdsecondproductfirstimaginary ge_balance_negative_gcd_exists_resultgcdsecondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdsecondproductfirstimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdsecondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdsecondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdsecondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductfirstimaginary) = S ge_signed_half_gcd_exists_resultgcdsecondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_exists_resultgcdsecondproduct) + ge_balance_negative_gcd_exists_resultgcdsecondproductfirstimaginary = (ge_first_in_gcd_exists_resultgcdsecondproduct) + ge_balance_positive_gcd_exists_resultgcdsecondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_exists_resultgcdsecondproductsecond ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductsecond. (((gr_quotient_gcd_exists_resultgcdsecond) = ((ge_representation_real_code_gcd_exists_resultgcdsecondproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductsecond)) * S ((ge_representation_real_code_gcd_exists_resultgcdsecondproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductsecond)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductsecond))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdsecondproductsecondreal ge_balance_negative_gcd_exists_resultgcdsecondproductsecondreal. (((((ge_representation_real_code_gcd_exists_resultgcdsecondproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdsecondproductsecondreal) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdsecondproductsecondrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdsecondproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdsecondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdsecondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductsecondreal) = S ge_signed_half_gcd_exists_resultgcdsecondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_exists_resultgcdsecondproduct) + ge_balance_negative_gcd_exists_resultgcdsecondproductsecondreal = (ge_second_rn_gcd_exists_resultgcdsecondproduct) + ge_balance_positive_gcd_exists_resultgcdsecondproductsecondreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdsecondproductsecondimaginary ge_balance_negative_gcd_exists_resultgcdsecondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdsecondproductsecondimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdsecondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdsecondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdsecondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductsecondimaginary) = S ge_signed_half_gcd_exists_resultgcdsecondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_exists_resultgcdsecondproduct) + ge_balance_negative_gcd_exists_resultgcdsecondproductsecondimaginary = (ge_second_in_gcd_exists_resultgcdsecondproduct) + ge_balance_positive_gcd_exists_resultgcdsecondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_exists_resultgcdsecondproductoutput ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductoutput. (((b) = ((ge_representation_real_code_gcd_exists_resultgcdsecondproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductoutput)) * S ((ge_representation_real_code_gcd_exists_resultgcdsecondproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductoutput)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductoutput))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdsecondproductoutputreal ge_balance_negative_gcd_exists_resultgcdsecondproductoutputreal. (((((ge_representation_real_code_gcd_exists_resultgcdsecondproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdsecondproductoutputreal) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdsecondproductoutputrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdsecondproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdsecondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdsecondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductoutputreal) = S ge_signed_half_gcd_exists_resultgcdsecondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdsecondproduct) * (ge_second_rp_gcd_exists_resultgcdsecondproduct))) + (((ge_first_rn_gcd_exists_resultgcdsecondproduct) * (ge_second_rn_gcd_exists_resultgcdsecondproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdsecondproduct) * (ge_second_in_gcd_exists_resultgcdsecondproduct))) + (((ge_first_in_gcd_exists_resultgcdsecondproduct) * (ge_second_ip_gcd_exists_resultgcdsecondproduct))))))) + ge_balance_negative_gcd_exists_resultgcdsecondproductoutputreal = (((((((ge_first_rp_gcd_exists_resultgcdsecondproduct) * (ge_second_rn_gcd_exists_resultgcdsecondproduct))) + (((ge_first_rn_gcd_exists_resultgcdsecondproduct) * (ge_second_rp_gcd_exists_resultgcdsecondproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdsecondproduct) * (ge_second_ip_gcd_exists_resultgcdsecondproduct))) + (((ge_first_in_gcd_exists_resultgcdsecondproduct) * (ge_second_in_gcd_exists_resultgcdsecondproduct))))))) + ge_balance_positive_gcd_exists_resultgcdsecondproductoutputreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdsecondproductoutputimaginary ge_balance_negative_gcd_exists_resultgcdsecondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdsecondproductoutputimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdsecondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdsecondproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdsecondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdsecondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdsecondproductoutputimaginary) = S ge_signed_half_gcd_exists_resultgcdsecondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdsecondproduct) * (ge_second_ip_gcd_exists_resultgcdsecondproduct))) + (((ge_first_rn_gcd_exists_resultgcdsecondproduct) * (ge_second_in_gcd_exists_resultgcdsecondproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdsecondproduct) * (ge_second_rp_gcd_exists_resultgcdsecondproduct))) + (((ge_first_in_gcd_exists_resultgcdsecondproduct) * (ge_second_rn_gcd_exists_resultgcdsecondproduct))))))) + ge_balance_negative_gcd_exists_resultgcdsecondproductoutputimaginary = (((((((ge_first_rp_gcd_exists_resultgcdsecondproduct) * (ge_second_in_gcd_exists_resultgcdsecondproduct))) + (((ge_first_rn_gcd_exists_resultgcdsecondproduct) * (ge_second_ip_gcd_exists_resultgcdsecondproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdsecondproduct) * (ge_second_rn_gcd_exists_resultgcdsecondproduct))) + (((ge_first_in_gcd_exists_resultgcdsecondproduct) * (ge_second_rp_gcd_exists_resultgcdsecondproduct))))))) + ge_balance_positive_gcd_exists_resultgcdsecondproductoutputimaginary)))))))))) /\ (forall gr_common_divisor_gcd_exists_resultgcd. (exists gr_quotient_gcd_exists_resultgcdcommon_first. (exists ge_first_rp_gcd_exists_resultgcdcommon_firstproduct ge_first_rn_gcd_exists_resultgcdcommon_firstproduct ge_first_ip_gcd_exists_resultgcdcommon_firstproduct ge_first_in_gcd_exists_resultgcdcommon_firstproduct ge_second_rp_gcd_exists_resultgcdcommon_firstproduct ge_second_rn_gcd_exists_resultgcdcommon_firstproduct ge_second_ip_gcd_exists_resultgcdcommon_firstproduct ge_second_in_gcd_exists_resultgcdcommon_firstproduct. ((exists ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductfirst ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductfirst. (((gr_common_divisor_gcd_exists_resultgcd) = ((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductfirst)) * S ((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductfirst)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductfirst))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdcommon_firstproductfirstreal ge_balance_negative_gcd_exists_resultgcdcommon_firstproductfirstreal. (((((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductfirstreal) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_firstproductfirstrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductfirstreal) = S ge_signed_half_gcd_exists_resultgcdcommon_firstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_exists_resultgcdcommon_firstproduct) + ge_balance_negative_gcd_exists_resultgcdcommon_firstproductfirstreal = (ge_first_rn_gcd_exists_resultgcdcommon_firstproduct) + ge_balance_positive_gcd_exists_resultgcdcommon_firstproductfirstreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdcommon_firstproductfirstimaginary ge_balance_negative_gcd_exists_resultgcdcommon_firstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductfirstimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductfirstimaginary) = S ge_signed_half_gcd_exists_resultgcdcommon_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_exists_resultgcdcommon_firstproduct) + ge_balance_negative_gcd_exists_resultgcdcommon_firstproductfirstimaginary = (ge_first_in_gcd_exists_resultgcdcommon_firstproduct) + ge_balance_positive_gcd_exists_resultgcdcommon_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductsecond ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductsecond. (((gr_quotient_gcd_exists_resultgcdcommon_first) = ((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductsecond)) * S ((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductsecond)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductsecond))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdcommon_firstproductsecondreal ge_balance_negative_gcd_exists_resultgcdcommon_firstproductsecondreal. (((((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductsecondreal) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_firstproductsecondrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductsecondreal) = S ge_signed_half_gcd_exists_resultgcdcommon_firstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_exists_resultgcdcommon_firstproduct) + ge_balance_negative_gcd_exists_resultgcdcommon_firstproductsecondreal = (ge_second_rn_gcd_exists_resultgcdcommon_firstproduct) + ge_balance_positive_gcd_exists_resultgcdcommon_firstproductsecondreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdcommon_firstproductsecondimaginary ge_balance_negative_gcd_exists_resultgcdcommon_firstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductsecondimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductsecondimaginary) = S ge_signed_half_gcd_exists_resultgcdcommon_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_exists_resultgcdcommon_firstproduct) + ge_balance_negative_gcd_exists_resultgcdcommon_firstproductsecondimaginary = (ge_second_in_gcd_exists_resultgcdcommon_firstproduct) + ge_balance_positive_gcd_exists_resultgcdcommon_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductoutput ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductoutput. (((a) = ((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductoutput)) * S ((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductoutput)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductoutput))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdcommon_firstproductoutputreal ge_balance_negative_gcd_exists_resultgcdcommon_firstproductoutputreal. (((((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductoutputreal) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_firstproductoutputrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdcommon_firstproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductoutputreal) = S ge_signed_half_gcd_exists_resultgcdcommon_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_rp_gcd_exists_resultgcdcommon_firstproduct))) + (((ge_first_rn_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_rn_gcd_exists_resultgcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_in_gcd_exists_resultgcdcommon_firstproduct))) + (((ge_first_in_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_ip_gcd_exists_resultgcdcommon_firstproduct))))))) + ge_balance_negative_gcd_exists_resultgcdcommon_firstproductoutputreal = (((((((ge_first_rp_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_rn_gcd_exists_resultgcdcommon_firstproduct))) + (((ge_first_rn_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_rp_gcd_exists_resultgcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_ip_gcd_exists_resultgcdcommon_firstproduct))) + (((ge_first_in_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_in_gcd_exists_resultgcdcommon_firstproduct))))))) + ge_balance_positive_gcd_exists_resultgcdcommon_firstproductoutputreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdcommon_firstproductoutputimaginary ge_balance_negative_gcd_exists_resultgcdcommon_firstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductoutputimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_firstproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_firstproductoutputimaginary) = S ge_signed_half_gcd_exists_resultgcdcommon_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_ip_gcd_exists_resultgcdcommon_firstproduct))) + (((ge_first_rn_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_in_gcd_exists_resultgcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_rp_gcd_exists_resultgcdcommon_firstproduct))) + (((ge_first_in_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_rn_gcd_exists_resultgcdcommon_firstproduct))))))) + ge_balance_negative_gcd_exists_resultgcdcommon_firstproductoutputimaginary = (((((((ge_first_rp_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_in_gcd_exists_resultgcdcommon_firstproduct))) + (((ge_first_rn_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_ip_gcd_exists_resultgcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_rn_gcd_exists_resultgcdcommon_firstproduct))) + (((ge_first_in_gcd_exists_resultgcdcommon_firstproduct) * (ge_second_rp_gcd_exists_resultgcdcommon_firstproduct))))))) + ge_balance_positive_gcd_exists_resultgcdcommon_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_exists_resultgcdcommon_second. (exists ge_first_rp_gcd_exists_resultgcdcommon_secondproduct ge_first_rn_gcd_exists_resultgcdcommon_secondproduct ge_first_ip_gcd_exists_resultgcdcommon_secondproduct ge_first_in_gcd_exists_resultgcdcommon_secondproduct ge_second_rp_gcd_exists_resultgcdcommon_secondproduct ge_second_rn_gcd_exists_resultgcdcommon_secondproduct ge_second_ip_gcd_exists_resultgcdcommon_secondproduct ge_second_in_gcd_exists_resultgcdcommon_secondproduct. ((exists ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductfirst ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductfirst. (((gr_common_divisor_gcd_exists_resultgcd) = ((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductfirst)) * S ((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductfirst)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductfirst))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdcommon_secondproductfirstreal ge_balance_negative_gcd_exists_resultgcdcommon_secondproductfirstreal. (((((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductfirstreal) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_secondproductfirstrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductfirstreal) = S ge_signed_half_gcd_exists_resultgcdcommon_secondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_exists_resultgcdcommon_secondproduct) + ge_balance_negative_gcd_exists_resultgcdcommon_secondproductfirstreal = (ge_first_rn_gcd_exists_resultgcdcommon_secondproduct) + ge_balance_positive_gcd_exists_resultgcdcommon_secondproductfirstreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdcommon_secondproductfirstimaginary ge_balance_negative_gcd_exists_resultgcdcommon_secondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductfirstimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductfirstimaginary) = S ge_signed_half_gcd_exists_resultgcdcommon_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_exists_resultgcdcommon_secondproduct) + ge_balance_negative_gcd_exists_resultgcdcommon_secondproductfirstimaginary = (ge_first_in_gcd_exists_resultgcdcommon_secondproduct) + ge_balance_positive_gcd_exists_resultgcdcommon_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductsecond ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductsecond. (((gr_quotient_gcd_exists_resultgcdcommon_second) = ((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductsecond)) * S ((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductsecond)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductsecond))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdcommon_secondproductsecondreal ge_balance_negative_gcd_exists_resultgcdcommon_secondproductsecondreal. (((((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductsecondreal) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_secondproductsecondrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductsecondreal) = S ge_signed_half_gcd_exists_resultgcdcommon_secondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_exists_resultgcdcommon_secondproduct) + ge_balance_negative_gcd_exists_resultgcdcommon_secondproductsecondreal = (ge_second_rn_gcd_exists_resultgcdcommon_secondproduct) + ge_balance_positive_gcd_exists_resultgcdcommon_secondproductsecondreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdcommon_secondproductsecondimaginary ge_balance_negative_gcd_exists_resultgcdcommon_secondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductsecondimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductsecondimaginary) = S ge_signed_half_gcd_exists_resultgcdcommon_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_exists_resultgcdcommon_secondproduct) + ge_balance_negative_gcd_exists_resultgcdcommon_secondproductsecondimaginary = (ge_second_in_gcd_exists_resultgcdcommon_secondproduct) + ge_balance_positive_gcd_exists_resultgcdcommon_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductoutput ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductoutput. (((b) = ((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductoutput)) * S ((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductoutput)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductoutput))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdcommon_secondproductoutputreal ge_balance_negative_gcd_exists_resultgcdcommon_secondproductoutputreal. (((((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductoutputreal) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_secondproductoutputrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdcommon_secondproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductoutputreal) = S ge_signed_half_gcd_exists_resultgcdcommon_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_rp_gcd_exists_resultgcdcommon_secondproduct))) + (((ge_first_rn_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_rn_gcd_exists_resultgcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_in_gcd_exists_resultgcdcommon_secondproduct))) + (((ge_first_in_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_ip_gcd_exists_resultgcdcommon_secondproduct))))))) + ge_balance_negative_gcd_exists_resultgcdcommon_secondproductoutputreal = (((((((ge_first_rp_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_rn_gcd_exists_resultgcdcommon_secondproduct))) + (((ge_first_rn_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_rp_gcd_exists_resultgcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_ip_gcd_exists_resultgcdcommon_secondproduct))) + (((ge_first_in_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_in_gcd_exists_resultgcdcommon_secondproduct))))))) + ge_balance_positive_gcd_exists_resultgcdcommon_secondproductoutputreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdcommon_secondproductoutputimaginary ge_balance_negative_gcd_exists_resultgcdcommon_secondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductoutputimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdcommon_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdcommon_secondproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdcommon_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdcommon_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdcommon_secondproductoutputimaginary) = S ge_signed_half_gcd_exists_resultgcdcommon_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_ip_gcd_exists_resultgcdcommon_secondproduct))) + (((ge_first_rn_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_in_gcd_exists_resultgcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_rp_gcd_exists_resultgcdcommon_secondproduct))) + (((ge_first_in_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_rn_gcd_exists_resultgcdcommon_secondproduct))))))) + ge_balance_negative_gcd_exists_resultgcdcommon_secondproductoutputimaginary = (((((((ge_first_rp_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_in_gcd_exists_resultgcdcommon_secondproduct))) + (((ge_first_rn_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_ip_gcd_exists_resultgcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_rn_gcd_exists_resultgcdcommon_secondproduct))) + (((ge_first_in_gcd_exists_resultgcdcommon_secondproduct) * (ge_second_rp_gcd_exists_resultgcdcommon_secondproduct))))))) + ge_balance_positive_gcd_exists_resultgcdcommon_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_exists_resultgcdgreatest. (exists ge_first_rp_gcd_exists_resultgcdgreatestproduct ge_first_rn_gcd_exists_resultgcdgreatestproduct ge_first_ip_gcd_exists_resultgcdgreatestproduct ge_first_in_gcd_exists_resultgcdgreatestproduct ge_second_rp_gcd_exists_resultgcdgreatestproduct ge_second_rn_gcd_exists_resultgcdgreatestproduct ge_second_ip_gcd_exists_resultgcdgreatestproduct ge_second_in_gcd_exists_resultgcdgreatestproduct. ((exists ge_representation_real_code_gcd_exists_resultgcdgreatestproductfirst ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductfirst. (((gr_common_divisor_gcd_exists_resultgcd) = ((ge_representation_real_code_gcd_exists_resultgcdgreatestproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductfirst)) * S ((ge_representation_real_code_gcd_exists_resultgcdgreatestproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductfirst)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductfirst) + (ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductfirst))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdgreatestproductfirstreal ge_balance_negative_gcd_exists_resultgcdgreatestproductfirstreal. (((((ge_representation_real_code_gcd_exists_resultgcdgreatestproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdgreatestproductfirstreal) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductfirstreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdgreatestproductfirstrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdgreatestproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdgreatestproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdgreatestproductfirstreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductfirstreal) = S ge_signed_half_gcd_exists_resultgcdgreatestproductfirstrealdecode))) /\ ((ge_first_rp_gcd_exists_resultgcdgreatestproduct) + ge_balance_negative_gcd_exists_resultgcdgreatestproductfirstreal = (ge_first_rn_gcd_exists_resultgcdgreatestproduct) + ge_balance_positive_gcd_exists_resultgcdgreatestproductfirstreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdgreatestproductfirstimaginary ge_balance_negative_gcd_exists_resultgcdgreatestproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductfirst) = 2 * (ge_balance_positive_gcd_exists_resultgcdgreatestproductfirstimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdgreatestproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductfirst) = 2 * ge_signed_half_gcd_exists_resultgcdgreatestproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdgreatestproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductfirstimaginary) = S ge_signed_half_gcd_exists_resultgcdgreatestproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_exists_resultgcdgreatestproduct) + ge_balance_negative_gcd_exists_resultgcdgreatestproductfirstimaginary = (ge_first_in_gcd_exists_resultgcdgreatestproduct) + ge_balance_positive_gcd_exists_resultgcdgreatestproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_exists_resultgcdgreatestproductsecond ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductsecond. (((gr_quotient_gcd_exists_resultgcdgreatest) = ((ge_representation_real_code_gcd_exists_resultgcdgreatestproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductsecond)) * S ((ge_representation_real_code_gcd_exists_resultgcdgreatestproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductsecond)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductsecond) + (ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductsecond))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdgreatestproductsecondreal ge_balance_negative_gcd_exists_resultgcdgreatestproductsecondreal. (((((ge_representation_real_code_gcd_exists_resultgcdgreatestproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdgreatestproductsecondreal) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductsecondreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdgreatestproductsecondrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdgreatestproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdgreatestproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdgreatestproductsecondreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductsecondreal) = S ge_signed_half_gcd_exists_resultgcdgreatestproductsecondrealdecode))) /\ ((ge_second_rp_gcd_exists_resultgcdgreatestproduct) + ge_balance_negative_gcd_exists_resultgcdgreatestproductsecondreal = (ge_second_rn_gcd_exists_resultgcdgreatestproduct) + ge_balance_positive_gcd_exists_resultgcdgreatestproductsecondreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdgreatestproductsecondimaginary ge_balance_negative_gcd_exists_resultgcdgreatestproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductsecond) = 2 * (ge_balance_positive_gcd_exists_resultgcdgreatestproductsecondimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdgreatestproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductsecond) = 2 * ge_signed_half_gcd_exists_resultgcdgreatestproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdgreatestproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductsecondimaginary) = S ge_signed_half_gcd_exists_resultgcdgreatestproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_exists_resultgcdgreatestproduct) + ge_balance_negative_gcd_exists_resultgcdgreatestproductsecondimaginary = (ge_second_in_gcd_exists_resultgcdgreatestproduct) + ge_balance_positive_gcd_exists_resultgcdgreatestproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_exists_resultgcdgreatestproductoutput ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductoutput. (((gr_gcd_gcd_exists_result) = ((ge_representation_real_code_gcd_exists_resultgcdgreatestproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductoutput)) * S ((ge_representation_real_code_gcd_exists_resultgcdgreatestproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductoutput)) + ((ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductoutput) + (ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductoutput))) /\ ((exists ge_balance_positive_gcd_exists_resultgcdgreatestproductoutputreal ge_balance_negative_gcd_exists_resultgcdgreatestproductoutputreal. (((((ge_representation_real_code_gcd_exists_resultgcdgreatestproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdgreatestproductoutputreal) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductoutputreal) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdgreatestproductoutputrealdecode. (((ge_representation_real_code_gcd_exists_resultgcdgreatestproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdgreatestproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdgreatestproductoutputreal) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductoutputreal) = S ge_signed_half_gcd_exists_resultgcdgreatestproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdgreatestproduct) * (ge_second_rp_gcd_exists_resultgcdgreatestproduct))) + (((ge_first_rn_gcd_exists_resultgcdgreatestproduct) * (ge_second_rn_gcd_exists_resultgcdgreatestproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdgreatestproduct) * (ge_second_in_gcd_exists_resultgcdgreatestproduct))) + (((ge_first_in_gcd_exists_resultgcdgreatestproduct) * (ge_second_ip_gcd_exists_resultgcdgreatestproduct))))))) + ge_balance_negative_gcd_exists_resultgcdgreatestproductoutputreal = (((((((ge_first_rp_gcd_exists_resultgcdgreatestproduct) * (ge_second_rn_gcd_exists_resultgcdgreatestproduct))) + (((ge_first_rn_gcd_exists_resultgcdgreatestproduct) * (ge_second_rp_gcd_exists_resultgcdgreatestproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdgreatestproduct) * (ge_second_ip_gcd_exists_resultgcdgreatestproduct))) + (((ge_first_in_gcd_exists_resultgcdgreatestproduct) * (ge_second_in_gcd_exists_resultgcdgreatestproduct))))))) + ge_balance_positive_gcd_exists_resultgcdgreatestproductoutputreal))) /\ (exists ge_balance_positive_gcd_exists_resultgcdgreatestproductoutputimaginary ge_balance_negative_gcd_exists_resultgcdgreatestproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductoutput) = 2 * (ge_balance_positive_gcd_exists_resultgcdgreatestproductoutputimaginary) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultgcdgreatestproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultgcdgreatestproductoutput) = 2 * ge_signed_half_gcd_exists_resultgcdgreatestproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultgcdgreatestproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultgcdgreatestproductoutputimaginary) = S ge_signed_half_gcd_exists_resultgcdgreatestproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_exists_resultgcdgreatestproduct) * (ge_second_ip_gcd_exists_resultgcdgreatestproduct))) + (((ge_first_rn_gcd_exists_resultgcdgreatestproduct) * (ge_second_in_gcd_exists_resultgcdgreatestproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdgreatestproduct) * (ge_second_rp_gcd_exists_resultgcdgreatestproduct))) + (((ge_first_in_gcd_exists_resultgcdgreatestproduct) * (ge_second_rn_gcd_exists_resultgcdgreatestproduct))))))) + ge_balance_negative_gcd_exists_resultgcdgreatestproductoutputimaginary = (((((((ge_first_rp_gcd_exists_resultgcdgreatestproduct) * (ge_second_in_gcd_exists_resultgcdgreatestproduct))) + (((ge_first_rn_gcd_exists_resultgcdgreatestproduct) * (ge_second_ip_gcd_exists_resultgcdgreatestproduct))))) + (((((ge_first_ip_gcd_exists_resultgcdgreatestproduct) * (ge_second_rn_gcd_exists_resultgcdgreatestproduct))) + (((ge_first_in_gcd_exists_resultgcdgreatestproduct) * (ge_second_rp_gcd_exists_resultgcdgreatestproduct))))))) + ge_balance_positive_gcd_exists_resultgcdgreatestproductoutputimaginary)))))))))))))) /\ (exists gr_first_product_gcd_exists_resultbezout gr_second_product_gcd_exists_resultbezout. ((exists ge_first_rp_gcd_exists_resultbezoutfirst ge_first_rn_gcd_exists_resultbezoutfirst ge_first_ip_gcd_exists_resultbezoutfirst ge_first_in_gcd_exists_resultbezoutfirst ge_second_rp_gcd_exists_resultbezoutfirst ge_second_rn_gcd_exists_resultbezoutfirst ge_second_ip_gcd_exists_resultbezoutfirst ge_second_in_gcd_exists_resultbezoutfirst. ((exists ge_representation_real_code_gcd_exists_resultbezoutfirstfirst ge_representation_imaginary_code_gcd_exists_resultbezoutfirstfirst. (((a) = ((ge_representation_real_code_gcd_exists_resultbezoutfirstfirst) + (ge_representation_imaginary_code_gcd_exists_resultbezoutfirstfirst)) * S ((ge_representation_real_code_gcd_exists_resultbezoutfirstfirst) + (ge_representation_imaginary_code_gcd_exists_resultbezoutfirstfirst)) + ((ge_representation_imaginary_code_gcd_exists_resultbezoutfirstfirst) + (ge_representation_imaginary_code_gcd_exists_resultbezoutfirstfirst))) /\ ((exists ge_balance_positive_gcd_exists_resultbezoutfirstfirstreal ge_balance_negative_gcd_exists_resultbezoutfirstfirstreal. (((((ge_representation_real_code_gcd_exists_resultbezoutfirstfirst) = 2 * (ge_balance_positive_gcd_exists_resultbezoutfirstfirstreal) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstfirstreal) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutfirstfirstrealdecode. (((ge_representation_real_code_gcd_exists_resultbezoutfirstfirst) = 2 * ge_signed_half_gcd_exists_resultbezoutfirstfirstrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutfirstfirstreal) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstfirstreal) = S ge_signed_half_gcd_exists_resultbezoutfirstfirstrealdecode))) /\ ((ge_first_rp_gcd_exists_resultbezoutfirst) + ge_balance_negative_gcd_exists_resultbezoutfirstfirstreal = (ge_first_rn_gcd_exists_resultbezoutfirst) + ge_balance_positive_gcd_exists_resultbezoutfirstfirstreal))) /\ (exists ge_balance_positive_gcd_exists_resultbezoutfirstfirstimaginary ge_balance_negative_gcd_exists_resultbezoutfirstfirstimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultbezoutfirstfirst) = 2 * (ge_balance_positive_gcd_exists_resultbezoutfirstfirstimaginary) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstfirstimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutfirstfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultbezoutfirstfirst) = 2 * ge_signed_half_gcd_exists_resultbezoutfirstfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutfirstfirstimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstfirstimaginary) = S ge_signed_half_gcd_exists_resultbezoutfirstfirstimaginarydecode))) /\ ((ge_first_ip_gcd_exists_resultbezoutfirst) + ge_balance_negative_gcd_exists_resultbezoutfirstfirstimaginary = (ge_first_in_gcd_exists_resultbezoutfirst) + ge_balance_positive_gcd_exists_resultbezoutfirstfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_exists_resultbezoutfirstsecond ge_representation_imaginary_code_gcd_exists_resultbezoutfirstsecond. (((gr_first_coefficient_gcd_exists_result) = ((ge_representation_real_code_gcd_exists_resultbezoutfirstsecond) + (ge_representation_imaginary_code_gcd_exists_resultbezoutfirstsecond)) * S ((ge_representation_real_code_gcd_exists_resultbezoutfirstsecond) + (ge_representation_imaginary_code_gcd_exists_resultbezoutfirstsecond)) + ((ge_representation_imaginary_code_gcd_exists_resultbezoutfirstsecond) + (ge_representation_imaginary_code_gcd_exists_resultbezoutfirstsecond))) /\ ((exists ge_balance_positive_gcd_exists_resultbezoutfirstsecondreal ge_balance_negative_gcd_exists_resultbezoutfirstsecondreal. (((((ge_representation_real_code_gcd_exists_resultbezoutfirstsecond) = 2 * (ge_balance_positive_gcd_exists_resultbezoutfirstsecondreal) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstsecondreal) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutfirstsecondrealdecode. (((ge_representation_real_code_gcd_exists_resultbezoutfirstsecond) = 2 * ge_signed_half_gcd_exists_resultbezoutfirstsecondrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutfirstsecondreal) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstsecondreal) = S ge_signed_half_gcd_exists_resultbezoutfirstsecondrealdecode))) /\ ((ge_second_rp_gcd_exists_resultbezoutfirst) + ge_balance_negative_gcd_exists_resultbezoutfirstsecondreal = (ge_second_rn_gcd_exists_resultbezoutfirst) + ge_balance_positive_gcd_exists_resultbezoutfirstsecondreal))) /\ (exists ge_balance_positive_gcd_exists_resultbezoutfirstsecondimaginary ge_balance_negative_gcd_exists_resultbezoutfirstsecondimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultbezoutfirstsecond) = 2 * (ge_balance_positive_gcd_exists_resultbezoutfirstsecondimaginary) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstsecondimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutfirstsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultbezoutfirstsecond) = 2 * ge_signed_half_gcd_exists_resultbezoutfirstsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutfirstsecondimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstsecondimaginary) = S ge_signed_half_gcd_exists_resultbezoutfirstsecondimaginarydecode))) /\ ((ge_second_ip_gcd_exists_resultbezoutfirst) + ge_balance_negative_gcd_exists_resultbezoutfirstsecondimaginary = (ge_second_in_gcd_exists_resultbezoutfirst) + ge_balance_positive_gcd_exists_resultbezoutfirstsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_exists_resultbezoutfirstoutput ge_representation_imaginary_code_gcd_exists_resultbezoutfirstoutput. (((gr_first_product_gcd_exists_resultbezout) = ((ge_representation_real_code_gcd_exists_resultbezoutfirstoutput) + (ge_representation_imaginary_code_gcd_exists_resultbezoutfirstoutput)) * S ((ge_representation_real_code_gcd_exists_resultbezoutfirstoutput) + (ge_representation_imaginary_code_gcd_exists_resultbezoutfirstoutput)) + ((ge_representation_imaginary_code_gcd_exists_resultbezoutfirstoutput) + (ge_representation_imaginary_code_gcd_exists_resultbezoutfirstoutput))) /\ ((exists ge_balance_positive_gcd_exists_resultbezoutfirstoutputreal ge_balance_negative_gcd_exists_resultbezoutfirstoutputreal. (((((ge_representation_real_code_gcd_exists_resultbezoutfirstoutput) = 2 * (ge_balance_positive_gcd_exists_resultbezoutfirstoutputreal) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstoutputreal) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutfirstoutputrealdecode. (((ge_representation_real_code_gcd_exists_resultbezoutfirstoutput) = 2 * ge_signed_half_gcd_exists_resultbezoutfirstoutputrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutfirstoutputreal) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstoutputreal) = S ge_signed_half_gcd_exists_resultbezoutfirstoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_exists_resultbezoutfirst) * (ge_second_rp_gcd_exists_resultbezoutfirst))) + (((ge_first_rn_gcd_exists_resultbezoutfirst) * (ge_second_rn_gcd_exists_resultbezoutfirst))))) + (((((ge_first_ip_gcd_exists_resultbezoutfirst) * (ge_second_in_gcd_exists_resultbezoutfirst))) + (((ge_first_in_gcd_exists_resultbezoutfirst) * (ge_second_ip_gcd_exists_resultbezoutfirst))))))) + ge_balance_negative_gcd_exists_resultbezoutfirstoutputreal = (((((((ge_first_rp_gcd_exists_resultbezoutfirst) * (ge_second_rn_gcd_exists_resultbezoutfirst))) + (((ge_first_rn_gcd_exists_resultbezoutfirst) * (ge_second_rp_gcd_exists_resultbezoutfirst))))) + (((((ge_first_ip_gcd_exists_resultbezoutfirst) * (ge_second_ip_gcd_exists_resultbezoutfirst))) + (((ge_first_in_gcd_exists_resultbezoutfirst) * (ge_second_in_gcd_exists_resultbezoutfirst))))))) + ge_balance_positive_gcd_exists_resultbezoutfirstoutputreal))) /\ (exists ge_balance_positive_gcd_exists_resultbezoutfirstoutputimaginary ge_balance_negative_gcd_exists_resultbezoutfirstoutputimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultbezoutfirstoutput) = 2 * (ge_balance_positive_gcd_exists_resultbezoutfirstoutputimaginary) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstoutputimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutfirstoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultbezoutfirstoutput) = 2 * ge_signed_half_gcd_exists_resultbezoutfirstoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutfirstoutputimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutfirstoutputimaginary) = S ge_signed_half_gcd_exists_resultbezoutfirstoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_exists_resultbezoutfirst) * (ge_second_ip_gcd_exists_resultbezoutfirst))) + (((ge_first_rn_gcd_exists_resultbezoutfirst) * (ge_second_in_gcd_exists_resultbezoutfirst))))) + (((((ge_first_ip_gcd_exists_resultbezoutfirst) * (ge_second_rp_gcd_exists_resultbezoutfirst))) + (((ge_first_in_gcd_exists_resultbezoutfirst) * (ge_second_rn_gcd_exists_resultbezoutfirst))))))) + ge_balance_negative_gcd_exists_resultbezoutfirstoutputimaginary = (((((((ge_first_rp_gcd_exists_resultbezoutfirst) * (ge_second_in_gcd_exists_resultbezoutfirst))) + (((ge_first_rn_gcd_exists_resultbezoutfirst) * (ge_second_ip_gcd_exists_resultbezoutfirst))))) + (((((ge_first_ip_gcd_exists_resultbezoutfirst) * (ge_second_rn_gcd_exists_resultbezoutfirst))) + (((ge_first_in_gcd_exists_resultbezoutfirst) * (ge_second_rp_gcd_exists_resultbezoutfirst))))))) + ge_balance_positive_gcd_exists_resultbezoutfirstoutputimaginary))))))))) /\ ((exists ge_first_rp_gcd_exists_resultbezoutsecond ge_first_rn_gcd_exists_resultbezoutsecond ge_first_ip_gcd_exists_resultbezoutsecond ge_first_in_gcd_exists_resultbezoutsecond ge_second_rp_gcd_exists_resultbezoutsecond ge_second_rn_gcd_exists_resultbezoutsecond ge_second_ip_gcd_exists_resultbezoutsecond ge_second_in_gcd_exists_resultbezoutsecond. ((exists ge_representation_real_code_gcd_exists_resultbezoutsecondfirst ge_representation_imaginary_code_gcd_exists_resultbezoutsecondfirst. (((b) = ((ge_representation_real_code_gcd_exists_resultbezoutsecondfirst) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsecondfirst)) * S ((ge_representation_real_code_gcd_exists_resultbezoutsecondfirst) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsecondfirst)) + ((ge_representation_imaginary_code_gcd_exists_resultbezoutsecondfirst) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsecondfirst))) /\ ((exists ge_balance_positive_gcd_exists_resultbezoutsecondfirstreal ge_balance_negative_gcd_exists_resultbezoutsecondfirstreal. (((((ge_representation_real_code_gcd_exists_resultbezoutsecondfirst) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsecondfirstreal) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondfirstreal) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsecondfirstrealdecode. (((ge_representation_real_code_gcd_exists_resultbezoutsecondfirst) = 2 * ge_signed_half_gcd_exists_resultbezoutsecondfirstrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsecondfirstreal) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondfirstreal) = S ge_signed_half_gcd_exists_resultbezoutsecondfirstrealdecode))) /\ ((ge_first_rp_gcd_exists_resultbezoutsecond) + ge_balance_negative_gcd_exists_resultbezoutsecondfirstreal = (ge_first_rn_gcd_exists_resultbezoutsecond) + ge_balance_positive_gcd_exists_resultbezoutsecondfirstreal))) /\ (exists ge_balance_positive_gcd_exists_resultbezoutsecondfirstimaginary ge_balance_negative_gcd_exists_resultbezoutsecondfirstimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultbezoutsecondfirst) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsecondfirstimaginary) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondfirstimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsecondfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultbezoutsecondfirst) = 2 * ge_signed_half_gcd_exists_resultbezoutsecondfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsecondfirstimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondfirstimaginary) = S ge_signed_half_gcd_exists_resultbezoutsecondfirstimaginarydecode))) /\ ((ge_first_ip_gcd_exists_resultbezoutsecond) + ge_balance_negative_gcd_exists_resultbezoutsecondfirstimaginary = (ge_first_in_gcd_exists_resultbezoutsecond) + ge_balance_positive_gcd_exists_resultbezoutsecondfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_exists_resultbezoutsecondsecond ge_representation_imaginary_code_gcd_exists_resultbezoutsecondsecond. (((gr_second_coefficient_gcd_exists_result) = ((ge_representation_real_code_gcd_exists_resultbezoutsecondsecond) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsecondsecond)) * S ((ge_representation_real_code_gcd_exists_resultbezoutsecondsecond) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsecondsecond)) + ((ge_representation_imaginary_code_gcd_exists_resultbezoutsecondsecond) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsecondsecond))) /\ ((exists ge_balance_positive_gcd_exists_resultbezoutsecondsecondreal ge_balance_negative_gcd_exists_resultbezoutsecondsecondreal. (((((ge_representation_real_code_gcd_exists_resultbezoutsecondsecond) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsecondsecondreal) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondsecondreal) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsecondsecondrealdecode. (((ge_representation_real_code_gcd_exists_resultbezoutsecondsecond) = 2 * ge_signed_half_gcd_exists_resultbezoutsecondsecondrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsecondsecondreal) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondsecondreal) = S ge_signed_half_gcd_exists_resultbezoutsecondsecondrealdecode))) /\ ((ge_second_rp_gcd_exists_resultbezoutsecond) + ge_balance_negative_gcd_exists_resultbezoutsecondsecondreal = (ge_second_rn_gcd_exists_resultbezoutsecond) + ge_balance_positive_gcd_exists_resultbezoutsecondsecondreal))) /\ (exists ge_balance_positive_gcd_exists_resultbezoutsecondsecondimaginary ge_balance_negative_gcd_exists_resultbezoutsecondsecondimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultbezoutsecondsecond) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsecondsecondimaginary) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondsecondimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsecondsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultbezoutsecondsecond) = 2 * ge_signed_half_gcd_exists_resultbezoutsecondsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsecondsecondimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondsecondimaginary) = S ge_signed_half_gcd_exists_resultbezoutsecondsecondimaginarydecode))) /\ ((ge_second_ip_gcd_exists_resultbezoutsecond) + ge_balance_negative_gcd_exists_resultbezoutsecondsecondimaginary = (ge_second_in_gcd_exists_resultbezoutsecond) + ge_balance_positive_gcd_exists_resultbezoutsecondsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_exists_resultbezoutsecondoutput ge_representation_imaginary_code_gcd_exists_resultbezoutsecondoutput. (((gr_second_product_gcd_exists_resultbezout) = ((ge_representation_real_code_gcd_exists_resultbezoutsecondoutput) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsecondoutput)) * S ((ge_representation_real_code_gcd_exists_resultbezoutsecondoutput) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsecondoutput)) + ((ge_representation_imaginary_code_gcd_exists_resultbezoutsecondoutput) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsecondoutput))) /\ ((exists ge_balance_positive_gcd_exists_resultbezoutsecondoutputreal ge_balance_negative_gcd_exists_resultbezoutsecondoutputreal. (((((ge_representation_real_code_gcd_exists_resultbezoutsecondoutput) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsecondoutputreal) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondoutputreal) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsecondoutputrealdecode. (((ge_representation_real_code_gcd_exists_resultbezoutsecondoutput) = 2 * ge_signed_half_gcd_exists_resultbezoutsecondoutputrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsecondoutputreal) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondoutputreal) = S ge_signed_half_gcd_exists_resultbezoutsecondoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_exists_resultbezoutsecond) * (ge_second_rp_gcd_exists_resultbezoutsecond))) + (((ge_first_rn_gcd_exists_resultbezoutsecond) * (ge_second_rn_gcd_exists_resultbezoutsecond))))) + (((((ge_first_ip_gcd_exists_resultbezoutsecond) * (ge_second_in_gcd_exists_resultbezoutsecond))) + (((ge_first_in_gcd_exists_resultbezoutsecond) * (ge_second_ip_gcd_exists_resultbezoutsecond))))))) + ge_balance_negative_gcd_exists_resultbezoutsecondoutputreal = (((((((ge_first_rp_gcd_exists_resultbezoutsecond) * (ge_second_rn_gcd_exists_resultbezoutsecond))) + (((ge_first_rn_gcd_exists_resultbezoutsecond) * (ge_second_rp_gcd_exists_resultbezoutsecond))))) + (((((ge_first_ip_gcd_exists_resultbezoutsecond) * (ge_second_ip_gcd_exists_resultbezoutsecond))) + (((ge_first_in_gcd_exists_resultbezoutsecond) * (ge_second_in_gcd_exists_resultbezoutsecond))))))) + ge_balance_positive_gcd_exists_resultbezoutsecondoutputreal))) /\ (exists ge_balance_positive_gcd_exists_resultbezoutsecondoutputimaginary ge_balance_negative_gcd_exists_resultbezoutsecondoutputimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultbezoutsecondoutput) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsecondoutputimaginary) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondoutputimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsecondoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultbezoutsecondoutput) = 2 * ge_signed_half_gcd_exists_resultbezoutsecondoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsecondoutputimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsecondoutputimaginary) = S ge_signed_half_gcd_exists_resultbezoutsecondoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_exists_resultbezoutsecond) * (ge_second_ip_gcd_exists_resultbezoutsecond))) + (((ge_first_rn_gcd_exists_resultbezoutsecond) * (ge_second_in_gcd_exists_resultbezoutsecond))))) + (((((ge_first_ip_gcd_exists_resultbezoutsecond) * (ge_second_rp_gcd_exists_resultbezoutsecond))) + (((ge_first_in_gcd_exists_resultbezoutsecond) * (ge_second_rn_gcd_exists_resultbezoutsecond))))))) + ge_balance_negative_gcd_exists_resultbezoutsecondoutputimaginary = (((((((ge_first_rp_gcd_exists_resultbezoutsecond) * (ge_second_in_gcd_exists_resultbezoutsecond))) + (((ge_first_rn_gcd_exists_resultbezoutsecond) * (ge_second_ip_gcd_exists_resultbezoutsecond))))) + (((((ge_first_ip_gcd_exists_resultbezoutsecond) * (ge_second_rn_gcd_exists_resultbezoutsecond))) + (((ge_first_in_gcd_exists_resultbezoutsecond) * (ge_second_rp_gcd_exists_resultbezoutsecond))))))) + ge_balance_positive_gcd_exists_resultbezoutsecondoutputimaginary))))))))) /\ (exists ge_first_rp_gcd_exists_resultbezoutsum ge_first_rn_gcd_exists_resultbezoutsum ge_first_ip_gcd_exists_resultbezoutsum ge_first_in_gcd_exists_resultbezoutsum ge_second_rp_gcd_exists_resultbezoutsum ge_second_rn_gcd_exists_resultbezoutsum ge_second_ip_gcd_exists_resultbezoutsum ge_second_in_gcd_exists_resultbezoutsum. ((exists ge_representation_real_code_gcd_exists_resultbezoutsumfirst ge_representation_imaginary_code_gcd_exists_resultbezoutsumfirst. (((gr_first_product_gcd_exists_resultbezout) = ((ge_representation_real_code_gcd_exists_resultbezoutsumfirst) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsumfirst)) * S ((ge_representation_real_code_gcd_exists_resultbezoutsumfirst) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsumfirst)) + ((ge_representation_imaginary_code_gcd_exists_resultbezoutsumfirst) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsumfirst))) /\ ((exists ge_balance_positive_gcd_exists_resultbezoutsumfirstreal ge_balance_negative_gcd_exists_resultbezoutsumfirstreal. (((((ge_representation_real_code_gcd_exists_resultbezoutsumfirst) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsumfirstreal) /\ (ge_balance_negative_gcd_exists_resultbezoutsumfirstreal) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsumfirstrealdecode. (((ge_representation_real_code_gcd_exists_resultbezoutsumfirst) = 2 * ge_signed_half_gcd_exists_resultbezoutsumfirstrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsumfirstreal) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsumfirstreal) = S ge_signed_half_gcd_exists_resultbezoutsumfirstrealdecode))) /\ ((ge_first_rp_gcd_exists_resultbezoutsum) + ge_balance_negative_gcd_exists_resultbezoutsumfirstreal = (ge_first_rn_gcd_exists_resultbezoutsum) + ge_balance_positive_gcd_exists_resultbezoutsumfirstreal))) /\ (exists ge_balance_positive_gcd_exists_resultbezoutsumfirstimaginary ge_balance_negative_gcd_exists_resultbezoutsumfirstimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultbezoutsumfirst) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsumfirstimaginary) /\ (ge_balance_negative_gcd_exists_resultbezoutsumfirstimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsumfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultbezoutsumfirst) = 2 * ge_signed_half_gcd_exists_resultbezoutsumfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsumfirstimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsumfirstimaginary) = S ge_signed_half_gcd_exists_resultbezoutsumfirstimaginarydecode))) /\ ((ge_first_ip_gcd_exists_resultbezoutsum) + ge_balance_negative_gcd_exists_resultbezoutsumfirstimaginary = (ge_first_in_gcd_exists_resultbezoutsum) + ge_balance_positive_gcd_exists_resultbezoutsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_exists_resultbezoutsumsecond ge_representation_imaginary_code_gcd_exists_resultbezoutsumsecond. (((gr_second_product_gcd_exists_resultbezout) = ((ge_representation_real_code_gcd_exists_resultbezoutsumsecond) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsumsecond)) * S ((ge_representation_real_code_gcd_exists_resultbezoutsumsecond) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsumsecond)) + ((ge_representation_imaginary_code_gcd_exists_resultbezoutsumsecond) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsumsecond))) /\ ((exists ge_balance_positive_gcd_exists_resultbezoutsumsecondreal ge_balance_negative_gcd_exists_resultbezoutsumsecondreal. (((((ge_representation_real_code_gcd_exists_resultbezoutsumsecond) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsumsecondreal) /\ (ge_balance_negative_gcd_exists_resultbezoutsumsecondreal) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsumsecondrealdecode. (((ge_representation_real_code_gcd_exists_resultbezoutsumsecond) = 2 * ge_signed_half_gcd_exists_resultbezoutsumsecondrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsumsecondreal) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsumsecondreal) = S ge_signed_half_gcd_exists_resultbezoutsumsecondrealdecode))) /\ ((ge_second_rp_gcd_exists_resultbezoutsum) + ge_balance_negative_gcd_exists_resultbezoutsumsecondreal = (ge_second_rn_gcd_exists_resultbezoutsum) + ge_balance_positive_gcd_exists_resultbezoutsumsecondreal))) /\ (exists ge_balance_positive_gcd_exists_resultbezoutsumsecondimaginary ge_balance_negative_gcd_exists_resultbezoutsumsecondimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultbezoutsumsecond) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsumsecondimaginary) /\ (ge_balance_negative_gcd_exists_resultbezoutsumsecondimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsumsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultbezoutsumsecond) = 2 * ge_signed_half_gcd_exists_resultbezoutsumsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsumsecondimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsumsecondimaginary) = S ge_signed_half_gcd_exists_resultbezoutsumsecondimaginarydecode))) /\ ((ge_second_ip_gcd_exists_resultbezoutsum) + ge_balance_negative_gcd_exists_resultbezoutsumsecondimaginary = (ge_second_in_gcd_exists_resultbezoutsum) + ge_balance_positive_gcd_exists_resultbezoutsumsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_exists_resultbezoutsumoutput ge_representation_imaginary_code_gcd_exists_resultbezoutsumoutput. (((gr_gcd_gcd_exists_result) = ((ge_representation_real_code_gcd_exists_resultbezoutsumoutput) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsumoutput)) * S ((ge_representation_real_code_gcd_exists_resultbezoutsumoutput) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsumoutput)) + ((ge_representation_imaginary_code_gcd_exists_resultbezoutsumoutput) + (ge_representation_imaginary_code_gcd_exists_resultbezoutsumoutput))) /\ ((exists ge_balance_positive_gcd_exists_resultbezoutsumoutputreal ge_balance_negative_gcd_exists_resultbezoutsumoutputreal. (((((ge_representation_real_code_gcd_exists_resultbezoutsumoutput) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsumoutputreal) /\ (ge_balance_negative_gcd_exists_resultbezoutsumoutputreal) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsumoutputrealdecode. (((ge_representation_real_code_gcd_exists_resultbezoutsumoutput) = 2 * ge_signed_half_gcd_exists_resultbezoutsumoutputrealdecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsumoutputreal) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsumoutputreal) = S ge_signed_half_gcd_exists_resultbezoutsumoutputrealdecode))) /\ ((((ge_first_rp_gcd_exists_resultbezoutsum) + (ge_second_rp_gcd_exists_resultbezoutsum))) + ge_balance_negative_gcd_exists_resultbezoutsumoutputreal = (((ge_first_rn_gcd_exists_resultbezoutsum) + (ge_second_rn_gcd_exists_resultbezoutsum))) + ge_balance_positive_gcd_exists_resultbezoutsumoutputreal))) /\ (exists ge_balance_positive_gcd_exists_resultbezoutsumoutputimaginary ge_balance_negative_gcd_exists_resultbezoutsumoutputimaginary. (((((ge_representation_imaginary_code_gcd_exists_resultbezoutsumoutput) = 2 * (ge_balance_positive_gcd_exists_resultbezoutsumoutputimaginary) /\ (ge_balance_negative_gcd_exists_resultbezoutsumoutputimaginary) = 0) \/ exists ge_signed_half_gcd_exists_resultbezoutsumoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_exists_resultbezoutsumoutput) = 2 * ge_signed_half_gcd_exists_resultbezoutsumoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_exists_resultbezoutsumoutputimaginary) = 0) /\ (ge_balance_negative_gcd_exists_resultbezoutsumoutputimaginary) = S ge_signed_half_gcd_exists_resultbezoutsumoutputimaginarydecode))) /\ ((((ge_first_ip_gcd_exists_resultbezoutsum) + (ge_second_ip_gcd_exists_resultbezoutsum))) + ge_balance_negative_gcd_exists_resultbezoutsumoutputimaginary = (((ge_first_in_gcd_exists_resultbezoutsum) + (ge_second_in_gcd_exists_resultbezoutsum))) + ge_balance_positive_gcd_exists_resultbezoutsumoutputimaginary))))))))))))))