gaussian_gcd_bezout_bounded_exists

Exact expanded first-order arithmetic statement

forall k a b N. (exists ge_real_positive_gcd_bounded_first ge_real_negative_gcd_bounded_first ge_imaginary_positive_gcd_bounded_first ge_imaginary_negative_gcd_bounded_first. (exists ge_real_code_gcd_bounded_firstdecode ge_imaginary_code_gcd_bounded_firstdecode. (((a) = ((ge_real_code_gcd_bounded_firstdecode) + (ge_imaginary_code_gcd_bounded_firstdecode)) * S ((ge_real_code_gcd_bounded_firstdecode) + (ge_imaginary_code_gcd_bounded_firstdecode)) + ((ge_imaginary_code_gcd_bounded_firstdecode) + (ge_imaginary_code_gcd_bounded_firstdecode))) /\ (((((ge_real_code_gcd_bounded_firstdecode) = 2 * (ge_real_positive_gcd_bounded_first) /\ (ge_real_negative_gcd_bounded_first) = 0) \/ exists ge_signed_half_ge_gcd_bounded_firstdecode_real. (((ge_real_code_gcd_bounded_firstdecode) = 2 * ge_signed_half_ge_gcd_bounded_firstdecode_real + 1 /\ (ge_real_positive_gcd_bounded_first) = 0) /\ (ge_real_negative_gcd_bounded_first) = S ge_signed_half_ge_gcd_bounded_firstdecode_real))) /\ ((((ge_imaginary_code_gcd_bounded_firstdecode) = 2 * (ge_imaginary_positive_gcd_bounded_first) /\ (ge_imaginary_negative_gcd_bounded_first) = 0) \/ exists ge_signed_half_ge_gcd_bounded_firstdecode_imaginary. (((ge_imaginary_code_gcd_bounded_firstdecode) = 2 * ge_signed_half_ge_gcd_bounded_firstdecode_imaginary + 1 /\ (ge_imaginary_positive_gcd_bounded_first) = 0) /\ (ge_imaginary_negative_gcd_bounded_first) = S ge_signed_half_ge_gcd_bounded_firstdecode_imaginary))))))) -> (exists ge_real_positive_gcd_bounded_second ge_real_negative_gcd_bounded_second ge_imaginary_positive_gcd_bounded_second ge_imaginary_negative_gcd_bounded_second. (exists ge_real_code_gcd_bounded_seconddecode ge_imaginary_code_gcd_bounded_seconddecode. (((b) = ((ge_real_code_gcd_bounded_seconddecode) + (ge_imaginary_code_gcd_bounded_seconddecode)) * S ((ge_real_code_gcd_bounded_seconddecode) + (ge_imaginary_code_gcd_bounded_seconddecode)) + ((ge_imaginary_code_gcd_bounded_seconddecode) + (ge_imaginary_code_gcd_bounded_seconddecode))) /\ (((((ge_real_code_gcd_bounded_seconddecode) = 2 * (ge_real_positive_gcd_bounded_second) /\ (ge_real_negative_gcd_bounded_second) = 0) \/ exists ge_signed_half_ge_gcd_bounded_seconddecode_real. (((ge_real_code_gcd_bounded_seconddecode) = 2 * ge_signed_half_ge_gcd_bounded_seconddecode_real + 1 /\ (ge_real_positive_gcd_bounded_second) = 0) /\ (ge_real_negative_gcd_bounded_second) = S ge_signed_half_ge_gcd_bounded_seconddecode_real))) /\ ((((ge_imaginary_code_gcd_bounded_seconddecode) = 2 * (ge_imaginary_positive_gcd_bounded_second) /\ (ge_imaginary_negative_gcd_bounded_second) = 0) \/ exists ge_signed_half_ge_gcd_bounded_seconddecode_imaginary. (((ge_imaginary_code_gcd_bounded_seconddecode) = 2 * ge_signed_half_ge_gcd_bounded_seconddecode_imaginary + 1 /\ (ge_imaginary_positive_gcd_bounded_second) = 0) /\ (ge_imaginary_negative_gcd_bounded_second) = S ge_signed_half_ge_gcd_bounded_seconddecode_imaginary))))))) -> (exists ge_norm_rp_gcd_bounded_norm ge_norm_rn_gcd_bounded_norm ge_norm_ip_gcd_bounded_norm ge_norm_in_gcd_bounded_norm. ((exists ge_representation_real_code_gcd_bounded_normrepresentation ge_representation_imaginary_code_gcd_bounded_normrepresentation. (((b) = ((ge_representation_real_code_gcd_bounded_normrepresentation) + (ge_representation_imaginary_code_gcd_bounded_normrepresentation)) * S ((ge_representation_real_code_gcd_bounded_normrepresentation) + (ge_representation_imaginary_code_gcd_bounded_normrepresentation)) + ((ge_representation_imaginary_code_gcd_bounded_normrepresentation) + (ge_representation_imaginary_code_gcd_bounded_normrepresentation))) /\ ((exists ge_balance_positive_gcd_bounded_normrepresentationreal ge_balance_negative_gcd_bounded_normrepresentationreal. (((((ge_representation_real_code_gcd_bounded_normrepresentation) = 2 * (ge_balance_positive_gcd_bounded_normrepresentationreal) /\ (ge_balance_negative_gcd_bounded_normrepresentationreal) = 0) \/ exists ge_signed_half_gcd_bounded_normrepresentationrealdecode. (((ge_representation_real_code_gcd_bounded_normrepresentation) = 2 * ge_signed_half_gcd_bounded_normrepresentationrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_normrepresentationreal) = 0) /\ (ge_balance_negative_gcd_bounded_normrepresentationreal) = S ge_signed_half_gcd_bounded_normrepresentationrealdecode))) /\ ((ge_norm_rp_gcd_bounded_norm) + ge_balance_negative_gcd_bounded_normrepresentationreal = (ge_norm_rn_gcd_bounded_norm) + ge_balance_positive_gcd_bounded_normrepresentationreal))) /\ (exists ge_balance_positive_gcd_bounded_normrepresentationimaginary ge_balance_negative_gcd_bounded_normrepresentationimaginary. (((((ge_representation_imaginary_code_gcd_bounded_normrepresentation) = 2 * (ge_balance_positive_gcd_bounded_normrepresentationimaginary) /\ (ge_balance_negative_gcd_bounded_normrepresentationimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_normrepresentation) = 2 * ge_signed_half_gcd_bounded_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_normrepresentationimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_normrepresentationimaginary) = S ge_signed_half_gcd_bounded_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_gcd_bounded_norm) + ge_balance_negative_gcd_bounded_normrepresentationimaginary = (ge_norm_in_gcd_bounded_norm) + ge_balance_positive_gcd_bounded_normrepresentationimaginary)))))) /\ (exists ge_real_square_gcd_bounded_normsquare ge_imaginary_square_gcd_bounded_normsquare. ((((((ge_norm_rp_gcd_bounded_norm) * (ge_norm_rp_gcd_bounded_norm))) + (((ge_norm_rn_gcd_bounded_norm) * (ge_norm_rn_gcd_bounded_norm)))) = ((ge_real_square_gcd_bounded_normsquare) + (((((ge_norm_rp_gcd_bounded_norm) * (ge_norm_rn_gcd_bounded_norm))) + (((ge_norm_rn_gcd_bounded_norm) * (ge_norm_rp_gcd_bounded_norm))))))) /\ ((((((ge_norm_ip_gcd_bounded_norm) * (ge_norm_ip_gcd_bounded_norm))) + (((ge_norm_in_gcd_bounded_norm) * (ge_norm_in_gcd_bounded_norm)))) = ((ge_imaginary_square_gcd_bounded_normsquare) + (((((ge_norm_ip_gcd_bounded_norm) * (ge_norm_in_gcd_bounded_norm))) + (((ge_norm_in_gcd_bounded_norm) * (ge_norm_ip_gcd_bounded_norm))))))) /\ ((N) = ge_real_square_gcd_bounded_normsquare + ge_imaginary_square_gcd_bounded_normsquare)))))) -> (exists ge_gap_gcd_bounded_bound. ge_gap_gcd_bounded_bound + (N) = (k)) -> (exists gr_gcd_gcd_bounded_result gr_first_coefficient_gcd_bounded_result gr_second_coefficient_gcd_bounded_result. ((((exists gr_quotient_gcd_bounded_resultgcdfirst. (exists ge_first_rp_gcd_bounded_resultgcdfirstproduct ge_first_rn_gcd_bounded_resultgcdfirstproduct ge_first_ip_gcd_bounded_resultgcdfirstproduct ge_first_in_gcd_bounded_resultgcdfirstproduct ge_second_rp_gcd_bounded_resultgcdfirstproduct ge_second_rn_gcd_bounded_resultgcdfirstproduct ge_second_ip_gcd_bounded_resultgcdfirstproduct ge_second_in_gcd_bounded_resultgcdfirstproduct. ((exists ge_representation_real_code_gcd_bounded_resultgcdfirstproductfirst ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductfirst. (((gr_gcd_gcd_bounded_result) = ((ge_representation_real_code_gcd_bounded_resultgcdfirstproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductfirst)) * S ((ge_representation_real_code_gcd_bounded_resultgcdfirstproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductfirst)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductfirst))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdfirstproductfirstreal ge_balance_negative_gcd_bounded_resultgcdfirstproductfirstreal. (((((ge_representation_real_code_gcd_bounded_resultgcdfirstproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdfirstproductfirstreal) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdfirstproductfirstrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdfirstproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdfirstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdfirstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductfirstreal) = S ge_signed_half_gcd_bounded_resultgcdfirstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_bounded_resultgcdfirstproduct) + ge_balance_negative_gcd_bounded_resultgcdfirstproductfirstreal = (ge_first_rn_gcd_bounded_resultgcdfirstproduct) + ge_balance_positive_gcd_bounded_resultgcdfirstproductfirstreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdfirstproductfirstimaginary ge_balance_negative_gcd_bounded_resultgcdfirstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdfirstproductfirstimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdfirstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdfirstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdfirstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductfirstimaginary) = S ge_signed_half_gcd_bounded_resultgcdfirstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_bounded_resultgcdfirstproduct) + ge_balance_negative_gcd_bounded_resultgcdfirstproductfirstimaginary = (ge_first_in_gcd_bounded_resultgcdfirstproduct) + ge_balance_positive_gcd_bounded_resultgcdfirstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_bounded_resultgcdfirstproductsecond ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductsecond. (((gr_quotient_gcd_bounded_resultgcdfirst) = ((ge_representation_real_code_gcd_bounded_resultgcdfirstproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductsecond)) * S ((ge_representation_real_code_gcd_bounded_resultgcdfirstproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductsecond)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductsecond))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdfirstproductsecondreal ge_balance_negative_gcd_bounded_resultgcdfirstproductsecondreal. (((((ge_representation_real_code_gcd_bounded_resultgcdfirstproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdfirstproductsecondreal) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdfirstproductsecondrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdfirstproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdfirstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdfirstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductsecondreal) = S ge_signed_half_gcd_bounded_resultgcdfirstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_bounded_resultgcdfirstproduct) + ge_balance_negative_gcd_bounded_resultgcdfirstproductsecondreal = (ge_second_rn_gcd_bounded_resultgcdfirstproduct) + ge_balance_positive_gcd_bounded_resultgcdfirstproductsecondreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdfirstproductsecondimaginary ge_balance_negative_gcd_bounded_resultgcdfirstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdfirstproductsecondimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdfirstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdfirstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdfirstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductsecondimaginary) = S ge_signed_half_gcd_bounded_resultgcdfirstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_bounded_resultgcdfirstproduct) + ge_balance_negative_gcd_bounded_resultgcdfirstproductsecondimaginary = (ge_second_in_gcd_bounded_resultgcdfirstproduct) + ge_balance_positive_gcd_bounded_resultgcdfirstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_bounded_resultgcdfirstproductoutput ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductoutput. (((a) = ((ge_representation_real_code_gcd_bounded_resultgcdfirstproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductoutput)) * S ((ge_representation_real_code_gcd_bounded_resultgcdfirstproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductoutput)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductoutput))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdfirstproductoutputreal ge_balance_negative_gcd_bounded_resultgcdfirstproductoutputreal. (((((ge_representation_real_code_gcd_bounded_resultgcdfirstproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdfirstproductoutputreal) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdfirstproductoutputrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdfirstproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdfirstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdfirstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductoutputreal) = S ge_signed_half_gcd_bounded_resultgcdfirstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdfirstproduct) * (ge_second_rp_gcd_bounded_resultgcdfirstproduct))) + (((ge_first_rn_gcd_bounded_resultgcdfirstproduct) * (ge_second_rn_gcd_bounded_resultgcdfirstproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdfirstproduct) * (ge_second_in_gcd_bounded_resultgcdfirstproduct))) + (((ge_first_in_gcd_bounded_resultgcdfirstproduct) * (ge_second_ip_gcd_bounded_resultgcdfirstproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdfirstproductoutputreal = (((((((ge_first_rp_gcd_bounded_resultgcdfirstproduct) * (ge_second_rn_gcd_bounded_resultgcdfirstproduct))) + (((ge_first_rn_gcd_bounded_resultgcdfirstproduct) * (ge_second_rp_gcd_bounded_resultgcdfirstproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdfirstproduct) * (ge_second_ip_gcd_bounded_resultgcdfirstproduct))) + (((ge_first_in_gcd_bounded_resultgcdfirstproduct) * (ge_second_in_gcd_bounded_resultgcdfirstproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdfirstproductoutputreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdfirstproductoutputimaginary ge_balance_negative_gcd_bounded_resultgcdfirstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdfirstproductoutputimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdfirstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdfirstproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdfirstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdfirstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdfirstproductoutputimaginary) = S ge_signed_half_gcd_bounded_resultgcdfirstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdfirstproduct) * (ge_second_ip_gcd_bounded_resultgcdfirstproduct))) + (((ge_first_rn_gcd_bounded_resultgcdfirstproduct) * (ge_second_in_gcd_bounded_resultgcdfirstproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdfirstproduct) * (ge_second_rp_gcd_bounded_resultgcdfirstproduct))) + (((ge_first_in_gcd_bounded_resultgcdfirstproduct) * (ge_second_rn_gcd_bounded_resultgcdfirstproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdfirstproductoutputimaginary = (((((((ge_first_rp_gcd_bounded_resultgcdfirstproduct) * (ge_second_in_gcd_bounded_resultgcdfirstproduct))) + (((ge_first_rn_gcd_bounded_resultgcdfirstproduct) * (ge_second_ip_gcd_bounded_resultgcdfirstproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdfirstproduct) * (ge_second_rn_gcd_bounded_resultgcdfirstproduct))) + (((ge_first_in_gcd_bounded_resultgcdfirstproduct) * (ge_second_rp_gcd_bounded_resultgcdfirstproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdfirstproductoutputimaginary)))))))))) /\ ((exists gr_quotient_gcd_bounded_resultgcdsecond. (exists ge_first_rp_gcd_bounded_resultgcdsecondproduct ge_first_rn_gcd_bounded_resultgcdsecondproduct ge_first_ip_gcd_bounded_resultgcdsecondproduct ge_first_in_gcd_bounded_resultgcdsecondproduct ge_second_rp_gcd_bounded_resultgcdsecondproduct ge_second_rn_gcd_bounded_resultgcdsecondproduct ge_second_ip_gcd_bounded_resultgcdsecondproduct ge_second_in_gcd_bounded_resultgcdsecondproduct. ((exists ge_representation_real_code_gcd_bounded_resultgcdsecondproductfirst ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductfirst. (((gr_gcd_gcd_bounded_result) = ((ge_representation_real_code_gcd_bounded_resultgcdsecondproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductfirst)) * S ((ge_representation_real_code_gcd_bounded_resultgcdsecondproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductfirst)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductfirst))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdsecondproductfirstreal ge_balance_negative_gcd_bounded_resultgcdsecondproductfirstreal. (((((ge_representation_real_code_gcd_bounded_resultgcdsecondproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdsecondproductfirstreal) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdsecondproductfirstrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdsecondproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdsecondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdsecondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductfirstreal) = S ge_signed_half_gcd_bounded_resultgcdsecondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_bounded_resultgcdsecondproduct) + ge_balance_negative_gcd_bounded_resultgcdsecondproductfirstreal = (ge_first_rn_gcd_bounded_resultgcdsecondproduct) + ge_balance_positive_gcd_bounded_resultgcdsecondproductfirstreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdsecondproductfirstimaginary ge_balance_negative_gcd_bounded_resultgcdsecondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdsecondproductfirstimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdsecondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdsecondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdsecondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductfirstimaginary) = S ge_signed_half_gcd_bounded_resultgcdsecondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_bounded_resultgcdsecondproduct) + ge_balance_negative_gcd_bounded_resultgcdsecondproductfirstimaginary = (ge_first_in_gcd_bounded_resultgcdsecondproduct) + ge_balance_positive_gcd_bounded_resultgcdsecondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_bounded_resultgcdsecondproductsecond ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductsecond. (((gr_quotient_gcd_bounded_resultgcdsecond) = ((ge_representation_real_code_gcd_bounded_resultgcdsecondproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductsecond)) * S ((ge_representation_real_code_gcd_bounded_resultgcdsecondproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductsecond)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductsecond))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdsecondproductsecondreal ge_balance_negative_gcd_bounded_resultgcdsecondproductsecondreal. (((((ge_representation_real_code_gcd_bounded_resultgcdsecondproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdsecondproductsecondreal) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdsecondproductsecondrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdsecondproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdsecondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdsecondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductsecondreal) = S ge_signed_half_gcd_bounded_resultgcdsecondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_bounded_resultgcdsecondproduct) + ge_balance_negative_gcd_bounded_resultgcdsecondproductsecondreal = (ge_second_rn_gcd_bounded_resultgcdsecondproduct) + ge_balance_positive_gcd_bounded_resultgcdsecondproductsecondreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdsecondproductsecondimaginary ge_balance_negative_gcd_bounded_resultgcdsecondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdsecondproductsecondimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdsecondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdsecondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdsecondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductsecondimaginary) = S ge_signed_half_gcd_bounded_resultgcdsecondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_bounded_resultgcdsecondproduct) + ge_balance_negative_gcd_bounded_resultgcdsecondproductsecondimaginary = (ge_second_in_gcd_bounded_resultgcdsecondproduct) + ge_balance_positive_gcd_bounded_resultgcdsecondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_bounded_resultgcdsecondproductoutput ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductoutput. (((b) = ((ge_representation_real_code_gcd_bounded_resultgcdsecondproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductoutput)) * S ((ge_representation_real_code_gcd_bounded_resultgcdsecondproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductoutput)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductoutput))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdsecondproductoutputreal ge_balance_negative_gcd_bounded_resultgcdsecondproductoutputreal. (((((ge_representation_real_code_gcd_bounded_resultgcdsecondproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdsecondproductoutputreal) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdsecondproductoutputrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdsecondproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdsecondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdsecondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductoutputreal) = S ge_signed_half_gcd_bounded_resultgcdsecondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdsecondproduct) * (ge_second_rp_gcd_bounded_resultgcdsecondproduct))) + (((ge_first_rn_gcd_bounded_resultgcdsecondproduct) * (ge_second_rn_gcd_bounded_resultgcdsecondproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdsecondproduct) * (ge_second_in_gcd_bounded_resultgcdsecondproduct))) + (((ge_first_in_gcd_bounded_resultgcdsecondproduct) * (ge_second_ip_gcd_bounded_resultgcdsecondproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdsecondproductoutputreal = (((((((ge_first_rp_gcd_bounded_resultgcdsecondproduct) * (ge_second_rn_gcd_bounded_resultgcdsecondproduct))) + (((ge_first_rn_gcd_bounded_resultgcdsecondproduct) * (ge_second_rp_gcd_bounded_resultgcdsecondproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdsecondproduct) * (ge_second_ip_gcd_bounded_resultgcdsecondproduct))) + (((ge_first_in_gcd_bounded_resultgcdsecondproduct) * (ge_second_in_gcd_bounded_resultgcdsecondproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdsecondproductoutputreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdsecondproductoutputimaginary ge_balance_negative_gcd_bounded_resultgcdsecondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdsecondproductoutputimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdsecondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdsecondproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdsecondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdsecondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdsecondproductoutputimaginary) = S ge_signed_half_gcd_bounded_resultgcdsecondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdsecondproduct) * (ge_second_ip_gcd_bounded_resultgcdsecondproduct))) + (((ge_first_rn_gcd_bounded_resultgcdsecondproduct) * (ge_second_in_gcd_bounded_resultgcdsecondproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdsecondproduct) * (ge_second_rp_gcd_bounded_resultgcdsecondproduct))) + (((ge_first_in_gcd_bounded_resultgcdsecondproduct) * (ge_second_rn_gcd_bounded_resultgcdsecondproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdsecondproductoutputimaginary = (((((((ge_first_rp_gcd_bounded_resultgcdsecondproduct) * (ge_second_in_gcd_bounded_resultgcdsecondproduct))) + (((ge_first_rn_gcd_bounded_resultgcdsecondproduct) * (ge_second_ip_gcd_bounded_resultgcdsecondproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdsecondproduct) * (ge_second_rn_gcd_bounded_resultgcdsecondproduct))) + (((ge_first_in_gcd_bounded_resultgcdsecondproduct) * (ge_second_rp_gcd_bounded_resultgcdsecondproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdsecondproductoutputimaginary)))))))))) /\ (forall gr_common_divisor_gcd_bounded_resultgcd. (exists gr_quotient_gcd_bounded_resultgcdcommon_first. (exists ge_first_rp_gcd_bounded_resultgcdcommon_firstproduct ge_first_rn_gcd_bounded_resultgcdcommon_firstproduct ge_first_ip_gcd_bounded_resultgcdcommon_firstproduct ge_first_in_gcd_bounded_resultgcdcommon_firstproduct ge_second_rp_gcd_bounded_resultgcdcommon_firstproduct ge_second_rn_gcd_bounded_resultgcdcommon_firstproduct ge_second_ip_gcd_bounded_resultgcdcommon_firstproduct ge_second_in_gcd_bounded_resultgcdcommon_firstproduct. ((exists ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductfirst ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductfirst. (((gr_common_divisor_gcd_bounded_resultgcd) = ((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductfirst)) * S ((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductfirst)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductfirst))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductfirstreal ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductfirstreal. (((((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductfirstreal) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_firstproductfirstrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductfirstreal) = S ge_signed_half_gcd_bounded_resultgcdcommon_firstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_bounded_resultgcdcommon_firstproduct) + ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductfirstreal = (ge_first_rn_gcd_bounded_resultgcdcommon_firstproduct) + ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductfirstreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductfirstimaginary ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductfirstimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductfirstimaginary) = S ge_signed_half_gcd_bounded_resultgcdcommon_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_bounded_resultgcdcommon_firstproduct) + ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductfirstimaginary = (ge_first_in_gcd_bounded_resultgcdcommon_firstproduct) + ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductsecond ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductsecond. (((gr_quotient_gcd_bounded_resultgcdcommon_first) = ((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductsecond)) * S ((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductsecond)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductsecond))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductsecondreal ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductsecondreal. (((((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductsecondreal) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_firstproductsecondrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductsecondreal) = S ge_signed_half_gcd_bounded_resultgcdcommon_firstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_bounded_resultgcdcommon_firstproduct) + ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductsecondreal = (ge_second_rn_gcd_bounded_resultgcdcommon_firstproduct) + ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductsecondreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductsecondimaginary ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductsecondimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductsecondimaginary) = S ge_signed_half_gcd_bounded_resultgcdcommon_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_bounded_resultgcdcommon_firstproduct) + ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductsecondimaginary = (ge_second_in_gcd_bounded_resultgcdcommon_firstproduct) + ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductoutput ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductoutput. (((a) = ((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductoutput)) * S ((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductoutput)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductoutput))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductoutputreal ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductoutputreal. (((((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductoutputreal) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_firstproductoutputrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdcommon_firstproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductoutputreal) = S ge_signed_half_gcd_bounded_resultgcdcommon_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_rp_gcd_bounded_resultgcdcommon_firstproduct))) + (((ge_first_rn_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_rn_gcd_bounded_resultgcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_in_gcd_bounded_resultgcdcommon_firstproduct))) + (((ge_first_in_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_ip_gcd_bounded_resultgcdcommon_firstproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductoutputreal = (((((((ge_first_rp_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_rn_gcd_bounded_resultgcdcommon_firstproduct))) + (((ge_first_rn_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_rp_gcd_bounded_resultgcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_ip_gcd_bounded_resultgcdcommon_firstproduct))) + (((ge_first_in_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_in_gcd_bounded_resultgcdcommon_firstproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductoutputreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductoutputimaginary ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductoutputimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_firstproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductoutputimaginary) = S ge_signed_half_gcd_bounded_resultgcdcommon_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_ip_gcd_bounded_resultgcdcommon_firstproduct))) + (((ge_first_rn_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_in_gcd_bounded_resultgcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_rp_gcd_bounded_resultgcdcommon_firstproduct))) + (((ge_first_in_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_rn_gcd_bounded_resultgcdcommon_firstproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdcommon_firstproductoutputimaginary = (((((((ge_first_rp_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_in_gcd_bounded_resultgcdcommon_firstproduct))) + (((ge_first_rn_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_ip_gcd_bounded_resultgcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_rn_gcd_bounded_resultgcdcommon_firstproduct))) + (((ge_first_in_gcd_bounded_resultgcdcommon_firstproduct) * (ge_second_rp_gcd_bounded_resultgcdcommon_firstproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdcommon_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_bounded_resultgcdcommon_second. (exists ge_first_rp_gcd_bounded_resultgcdcommon_secondproduct ge_first_rn_gcd_bounded_resultgcdcommon_secondproduct ge_first_ip_gcd_bounded_resultgcdcommon_secondproduct ge_first_in_gcd_bounded_resultgcdcommon_secondproduct ge_second_rp_gcd_bounded_resultgcdcommon_secondproduct ge_second_rn_gcd_bounded_resultgcdcommon_secondproduct ge_second_ip_gcd_bounded_resultgcdcommon_secondproduct ge_second_in_gcd_bounded_resultgcdcommon_secondproduct. ((exists ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductfirst ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductfirst. (((gr_common_divisor_gcd_bounded_resultgcd) = ((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductfirst)) * S ((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductfirst)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductfirst))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductfirstreal ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductfirstreal. (((((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductfirstreal) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_secondproductfirstrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductfirstreal) = S ge_signed_half_gcd_bounded_resultgcdcommon_secondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_bounded_resultgcdcommon_secondproduct) + ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductfirstreal = (ge_first_rn_gcd_bounded_resultgcdcommon_secondproduct) + ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductfirstreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductfirstimaginary ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductfirstimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductfirstimaginary) = S ge_signed_half_gcd_bounded_resultgcdcommon_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_bounded_resultgcdcommon_secondproduct) + ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductfirstimaginary = (ge_first_in_gcd_bounded_resultgcdcommon_secondproduct) + ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductsecond ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductsecond. (((gr_quotient_gcd_bounded_resultgcdcommon_second) = ((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductsecond)) * S ((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductsecond)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductsecond))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductsecondreal ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductsecondreal. (((((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductsecondreal) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_secondproductsecondrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductsecondreal) = S ge_signed_half_gcd_bounded_resultgcdcommon_secondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_bounded_resultgcdcommon_secondproduct) + ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductsecondreal = (ge_second_rn_gcd_bounded_resultgcdcommon_secondproduct) + ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductsecondreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductsecondimaginary ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductsecondimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductsecondimaginary) = S ge_signed_half_gcd_bounded_resultgcdcommon_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_bounded_resultgcdcommon_secondproduct) + ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductsecondimaginary = (ge_second_in_gcd_bounded_resultgcdcommon_secondproduct) + ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductoutput ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductoutput. (((b) = ((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductoutput)) * S ((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductoutput)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductoutput))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductoutputreal ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductoutputreal. (((((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductoutputreal) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_secondproductoutputrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdcommon_secondproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductoutputreal) = S ge_signed_half_gcd_bounded_resultgcdcommon_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_rp_gcd_bounded_resultgcdcommon_secondproduct))) + (((ge_first_rn_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_rn_gcd_bounded_resultgcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_in_gcd_bounded_resultgcdcommon_secondproduct))) + (((ge_first_in_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_ip_gcd_bounded_resultgcdcommon_secondproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductoutputreal = (((((((ge_first_rp_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_rn_gcd_bounded_resultgcdcommon_secondproduct))) + (((ge_first_rn_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_rp_gcd_bounded_resultgcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_ip_gcd_bounded_resultgcdcommon_secondproduct))) + (((ge_first_in_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_in_gcd_bounded_resultgcdcommon_secondproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductoutputreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductoutputimaginary ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductoutputimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdcommon_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdcommon_secondproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdcommon_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductoutputimaginary) = S ge_signed_half_gcd_bounded_resultgcdcommon_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_ip_gcd_bounded_resultgcdcommon_secondproduct))) + (((ge_first_rn_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_in_gcd_bounded_resultgcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_rp_gcd_bounded_resultgcdcommon_secondproduct))) + (((ge_first_in_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_rn_gcd_bounded_resultgcdcommon_secondproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdcommon_secondproductoutputimaginary = (((((((ge_first_rp_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_in_gcd_bounded_resultgcdcommon_secondproduct))) + (((ge_first_rn_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_ip_gcd_bounded_resultgcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_rn_gcd_bounded_resultgcdcommon_secondproduct))) + (((ge_first_in_gcd_bounded_resultgcdcommon_secondproduct) * (ge_second_rp_gcd_bounded_resultgcdcommon_secondproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdcommon_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_bounded_resultgcdgreatest. (exists ge_first_rp_gcd_bounded_resultgcdgreatestproduct ge_first_rn_gcd_bounded_resultgcdgreatestproduct ge_first_ip_gcd_bounded_resultgcdgreatestproduct ge_first_in_gcd_bounded_resultgcdgreatestproduct ge_second_rp_gcd_bounded_resultgcdgreatestproduct ge_second_rn_gcd_bounded_resultgcdgreatestproduct ge_second_ip_gcd_bounded_resultgcdgreatestproduct ge_second_in_gcd_bounded_resultgcdgreatestproduct. ((exists ge_representation_real_code_gcd_bounded_resultgcdgreatestproductfirst ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductfirst. (((gr_common_divisor_gcd_bounded_resultgcd) = ((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductfirst)) * S ((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductfirst)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductfirst) + (ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductfirst))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdgreatestproductfirstreal ge_balance_negative_gcd_bounded_resultgcdgreatestproductfirstreal. (((((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdgreatestproductfirstreal) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductfirstreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdgreatestproductfirstrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdgreatestproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdgreatestproductfirstreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductfirstreal) = S ge_signed_half_gcd_bounded_resultgcdgreatestproductfirstrealdecode))) /\ ((ge_first_rp_gcd_bounded_resultgcdgreatestproduct) + ge_balance_negative_gcd_bounded_resultgcdgreatestproductfirstreal = (ge_first_rn_gcd_bounded_resultgcdgreatestproduct) + ge_balance_positive_gcd_bounded_resultgcdgreatestproductfirstreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdgreatestproductfirstimaginary ge_balance_negative_gcd_bounded_resultgcdgreatestproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductfirst) = 2 * (ge_balance_positive_gcd_bounded_resultgcdgreatestproductfirstimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdgreatestproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductfirst) = 2 * ge_signed_half_gcd_bounded_resultgcdgreatestproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdgreatestproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductfirstimaginary) = S ge_signed_half_gcd_bounded_resultgcdgreatestproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_bounded_resultgcdgreatestproduct) + ge_balance_negative_gcd_bounded_resultgcdgreatestproductfirstimaginary = (ge_first_in_gcd_bounded_resultgcdgreatestproduct) + ge_balance_positive_gcd_bounded_resultgcdgreatestproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_bounded_resultgcdgreatestproductsecond ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductsecond. (((gr_quotient_gcd_bounded_resultgcdgreatest) = ((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductsecond)) * S ((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductsecond)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductsecond) + (ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductsecond))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdgreatestproductsecondreal ge_balance_negative_gcd_bounded_resultgcdgreatestproductsecondreal. (((((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdgreatestproductsecondreal) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductsecondreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdgreatestproductsecondrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdgreatestproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdgreatestproductsecondreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductsecondreal) = S ge_signed_half_gcd_bounded_resultgcdgreatestproductsecondrealdecode))) /\ ((ge_second_rp_gcd_bounded_resultgcdgreatestproduct) + ge_balance_negative_gcd_bounded_resultgcdgreatestproductsecondreal = (ge_second_rn_gcd_bounded_resultgcdgreatestproduct) + ge_balance_positive_gcd_bounded_resultgcdgreatestproductsecondreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdgreatestproductsecondimaginary ge_balance_negative_gcd_bounded_resultgcdgreatestproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductsecond) = 2 * (ge_balance_positive_gcd_bounded_resultgcdgreatestproductsecondimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdgreatestproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductsecond) = 2 * ge_signed_half_gcd_bounded_resultgcdgreatestproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdgreatestproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductsecondimaginary) = S ge_signed_half_gcd_bounded_resultgcdgreatestproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_bounded_resultgcdgreatestproduct) + ge_balance_negative_gcd_bounded_resultgcdgreatestproductsecondimaginary = (ge_second_in_gcd_bounded_resultgcdgreatestproduct) + ge_balance_positive_gcd_bounded_resultgcdgreatestproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_bounded_resultgcdgreatestproductoutput ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductoutput. (((gr_gcd_gcd_bounded_result) = ((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductoutput)) * S ((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductoutput)) + ((ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductoutput) + (ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductoutput))) /\ ((exists ge_balance_positive_gcd_bounded_resultgcdgreatestproductoutputreal ge_balance_negative_gcd_bounded_resultgcdgreatestproductoutputreal. (((((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdgreatestproductoutputreal) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductoutputreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdgreatestproductoutputrealdecode. (((ge_representation_real_code_gcd_bounded_resultgcdgreatestproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdgreatestproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdgreatestproductoutputreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductoutputreal) = S ge_signed_half_gcd_bounded_resultgcdgreatestproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdgreatestproduct) * (ge_second_rp_gcd_bounded_resultgcdgreatestproduct))) + (((ge_first_rn_gcd_bounded_resultgcdgreatestproduct) * (ge_second_rn_gcd_bounded_resultgcdgreatestproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdgreatestproduct) * (ge_second_in_gcd_bounded_resultgcdgreatestproduct))) + (((ge_first_in_gcd_bounded_resultgcdgreatestproduct) * (ge_second_ip_gcd_bounded_resultgcdgreatestproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdgreatestproductoutputreal = (((((((ge_first_rp_gcd_bounded_resultgcdgreatestproduct) * (ge_second_rn_gcd_bounded_resultgcdgreatestproduct))) + (((ge_first_rn_gcd_bounded_resultgcdgreatestproduct) * (ge_second_rp_gcd_bounded_resultgcdgreatestproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdgreatestproduct) * (ge_second_ip_gcd_bounded_resultgcdgreatestproduct))) + (((ge_first_in_gcd_bounded_resultgcdgreatestproduct) * (ge_second_in_gcd_bounded_resultgcdgreatestproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdgreatestproductoutputreal))) /\ (exists ge_balance_positive_gcd_bounded_resultgcdgreatestproductoutputimaginary ge_balance_negative_gcd_bounded_resultgcdgreatestproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductoutput) = 2 * (ge_balance_positive_gcd_bounded_resultgcdgreatestproductoutputimaginary) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultgcdgreatestproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultgcdgreatestproductoutput) = 2 * ge_signed_half_gcd_bounded_resultgcdgreatestproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultgcdgreatestproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultgcdgreatestproductoutputimaginary) = S ge_signed_half_gcd_bounded_resultgcdgreatestproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultgcdgreatestproduct) * (ge_second_ip_gcd_bounded_resultgcdgreatestproduct))) + (((ge_first_rn_gcd_bounded_resultgcdgreatestproduct) * (ge_second_in_gcd_bounded_resultgcdgreatestproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdgreatestproduct) * (ge_second_rp_gcd_bounded_resultgcdgreatestproduct))) + (((ge_first_in_gcd_bounded_resultgcdgreatestproduct) * (ge_second_rn_gcd_bounded_resultgcdgreatestproduct))))))) + ge_balance_negative_gcd_bounded_resultgcdgreatestproductoutputimaginary = (((((((ge_first_rp_gcd_bounded_resultgcdgreatestproduct) * (ge_second_in_gcd_bounded_resultgcdgreatestproduct))) + (((ge_first_rn_gcd_bounded_resultgcdgreatestproduct) * (ge_second_ip_gcd_bounded_resultgcdgreatestproduct))))) + (((((ge_first_ip_gcd_bounded_resultgcdgreatestproduct) * (ge_second_rn_gcd_bounded_resultgcdgreatestproduct))) + (((ge_first_in_gcd_bounded_resultgcdgreatestproduct) * (ge_second_rp_gcd_bounded_resultgcdgreatestproduct))))))) + ge_balance_positive_gcd_bounded_resultgcdgreatestproductoutputimaginary)))))))))))))) /\ (exists gr_first_product_gcd_bounded_resultbezout gr_second_product_gcd_bounded_resultbezout. ((exists ge_first_rp_gcd_bounded_resultbezoutfirst ge_first_rn_gcd_bounded_resultbezoutfirst ge_first_ip_gcd_bounded_resultbezoutfirst ge_first_in_gcd_bounded_resultbezoutfirst ge_second_rp_gcd_bounded_resultbezoutfirst ge_second_rn_gcd_bounded_resultbezoutfirst ge_second_ip_gcd_bounded_resultbezoutfirst ge_second_in_gcd_bounded_resultbezoutfirst. ((exists ge_representation_real_code_gcd_bounded_resultbezoutfirstfirst ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstfirst. (((a) = ((ge_representation_real_code_gcd_bounded_resultbezoutfirstfirst) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstfirst)) * S ((ge_representation_real_code_gcd_bounded_resultbezoutfirstfirst) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstfirst)) + ((ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstfirst) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstfirst))) /\ ((exists ge_balance_positive_gcd_bounded_resultbezoutfirstfirstreal ge_balance_negative_gcd_bounded_resultbezoutfirstfirstreal. (((((ge_representation_real_code_gcd_bounded_resultbezoutfirstfirst) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutfirstfirstreal) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstfirstreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutfirstfirstrealdecode. (((ge_representation_real_code_gcd_bounded_resultbezoutfirstfirst) = 2 * ge_signed_half_gcd_bounded_resultbezoutfirstfirstrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutfirstfirstreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstfirstreal) = S ge_signed_half_gcd_bounded_resultbezoutfirstfirstrealdecode))) /\ ((ge_first_rp_gcd_bounded_resultbezoutfirst) + ge_balance_negative_gcd_bounded_resultbezoutfirstfirstreal = (ge_first_rn_gcd_bounded_resultbezoutfirst) + ge_balance_positive_gcd_bounded_resultbezoutfirstfirstreal))) /\ (exists ge_balance_positive_gcd_bounded_resultbezoutfirstfirstimaginary ge_balance_negative_gcd_bounded_resultbezoutfirstfirstimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstfirst) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutfirstfirstimaginary) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstfirstimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutfirstfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstfirst) = 2 * ge_signed_half_gcd_bounded_resultbezoutfirstfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutfirstfirstimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstfirstimaginary) = S ge_signed_half_gcd_bounded_resultbezoutfirstfirstimaginarydecode))) /\ ((ge_first_ip_gcd_bounded_resultbezoutfirst) + ge_balance_negative_gcd_bounded_resultbezoutfirstfirstimaginary = (ge_first_in_gcd_bounded_resultbezoutfirst) + ge_balance_positive_gcd_bounded_resultbezoutfirstfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_bounded_resultbezoutfirstsecond ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstsecond. (((gr_first_coefficient_gcd_bounded_result) = ((ge_representation_real_code_gcd_bounded_resultbezoutfirstsecond) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstsecond)) * S ((ge_representation_real_code_gcd_bounded_resultbezoutfirstsecond) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstsecond)) + ((ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstsecond) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstsecond))) /\ ((exists ge_balance_positive_gcd_bounded_resultbezoutfirstsecondreal ge_balance_negative_gcd_bounded_resultbezoutfirstsecondreal. (((((ge_representation_real_code_gcd_bounded_resultbezoutfirstsecond) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutfirstsecondreal) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstsecondreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutfirstsecondrealdecode. (((ge_representation_real_code_gcd_bounded_resultbezoutfirstsecond) = 2 * ge_signed_half_gcd_bounded_resultbezoutfirstsecondrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutfirstsecondreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstsecondreal) = S ge_signed_half_gcd_bounded_resultbezoutfirstsecondrealdecode))) /\ ((ge_second_rp_gcd_bounded_resultbezoutfirst) + ge_balance_negative_gcd_bounded_resultbezoutfirstsecondreal = (ge_second_rn_gcd_bounded_resultbezoutfirst) + ge_balance_positive_gcd_bounded_resultbezoutfirstsecondreal))) /\ (exists ge_balance_positive_gcd_bounded_resultbezoutfirstsecondimaginary ge_balance_negative_gcd_bounded_resultbezoutfirstsecondimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstsecond) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutfirstsecondimaginary) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstsecondimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutfirstsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstsecond) = 2 * ge_signed_half_gcd_bounded_resultbezoutfirstsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutfirstsecondimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstsecondimaginary) = S ge_signed_half_gcd_bounded_resultbezoutfirstsecondimaginarydecode))) /\ ((ge_second_ip_gcd_bounded_resultbezoutfirst) + ge_balance_negative_gcd_bounded_resultbezoutfirstsecondimaginary = (ge_second_in_gcd_bounded_resultbezoutfirst) + ge_balance_positive_gcd_bounded_resultbezoutfirstsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_bounded_resultbezoutfirstoutput ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstoutput. (((gr_first_product_gcd_bounded_resultbezout) = ((ge_representation_real_code_gcd_bounded_resultbezoutfirstoutput) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstoutput)) * S ((ge_representation_real_code_gcd_bounded_resultbezoutfirstoutput) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstoutput)) + ((ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstoutput) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstoutput))) /\ ((exists ge_balance_positive_gcd_bounded_resultbezoutfirstoutputreal ge_balance_negative_gcd_bounded_resultbezoutfirstoutputreal. (((((ge_representation_real_code_gcd_bounded_resultbezoutfirstoutput) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutfirstoutputreal) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstoutputreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutfirstoutputrealdecode. (((ge_representation_real_code_gcd_bounded_resultbezoutfirstoutput) = 2 * ge_signed_half_gcd_bounded_resultbezoutfirstoutputrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutfirstoutputreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstoutputreal) = S ge_signed_half_gcd_bounded_resultbezoutfirstoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultbezoutfirst) * (ge_second_rp_gcd_bounded_resultbezoutfirst))) + (((ge_first_rn_gcd_bounded_resultbezoutfirst) * (ge_second_rn_gcd_bounded_resultbezoutfirst))))) + (((((ge_first_ip_gcd_bounded_resultbezoutfirst) * (ge_second_in_gcd_bounded_resultbezoutfirst))) + (((ge_first_in_gcd_bounded_resultbezoutfirst) * (ge_second_ip_gcd_bounded_resultbezoutfirst))))))) + ge_balance_negative_gcd_bounded_resultbezoutfirstoutputreal = (((((((ge_first_rp_gcd_bounded_resultbezoutfirst) * (ge_second_rn_gcd_bounded_resultbezoutfirst))) + (((ge_first_rn_gcd_bounded_resultbezoutfirst) * (ge_second_rp_gcd_bounded_resultbezoutfirst))))) + (((((ge_first_ip_gcd_bounded_resultbezoutfirst) * (ge_second_ip_gcd_bounded_resultbezoutfirst))) + (((ge_first_in_gcd_bounded_resultbezoutfirst) * (ge_second_in_gcd_bounded_resultbezoutfirst))))))) + ge_balance_positive_gcd_bounded_resultbezoutfirstoutputreal))) /\ (exists ge_balance_positive_gcd_bounded_resultbezoutfirstoutputimaginary ge_balance_negative_gcd_bounded_resultbezoutfirstoutputimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstoutput) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutfirstoutputimaginary) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstoutputimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutfirstoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultbezoutfirstoutput) = 2 * ge_signed_half_gcd_bounded_resultbezoutfirstoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutfirstoutputimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutfirstoutputimaginary) = S ge_signed_half_gcd_bounded_resultbezoutfirstoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultbezoutfirst) * (ge_second_ip_gcd_bounded_resultbezoutfirst))) + (((ge_first_rn_gcd_bounded_resultbezoutfirst) * (ge_second_in_gcd_bounded_resultbezoutfirst))))) + (((((ge_first_ip_gcd_bounded_resultbezoutfirst) * (ge_second_rp_gcd_bounded_resultbezoutfirst))) + (((ge_first_in_gcd_bounded_resultbezoutfirst) * (ge_second_rn_gcd_bounded_resultbezoutfirst))))))) + ge_balance_negative_gcd_bounded_resultbezoutfirstoutputimaginary = (((((((ge_first_rp_gcd_bounded_resultbezoutfirst) * (ge_second_in_gcd_bounded_resultbezoutfirst))) + (((ge_first_rn_gcd_bounded_resultbezoutfirst) * (ge_second_ip_gcd_bounded_resultbezoutfirst))))) + (((((ge_first_ip_gcd_bounded_resultbezoutfirst) * (ge_second_rn_gcd_bounded_resultbezoutfirst))) + (((ge_first_in_gcd_bounded_resultbezoutfirst) * (ge_second_rp_gcd_bounded_resultbezoutfirst))))))) + ge_balance_positive_gcd_bounded_resultbezoutfirstoutputimaginary))))))))) /\ ((exists ge_first_rp_gcd_bounded_resultbezoutsecond ge_first_rn_gcd_bounded_resultbezoutsecond ge_first_ip_gcd_bounded_resultbezoutsecond ge_first_in_gcd_bounded_resultbezoutsecond ge_second_rp_gcd_bounded_resultbezoutsecond ge_second_rn_gcd_bounded_resultbezoutsecond ge_second_ip_gcd_bounded_resultbezoutsecond ge_second_in_gcd_bounded_resultbezoutsecond. ((exists ge_representation_real_code_gcd_bounded_resultbezoutsecondfirst ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondfirst. (((b) = ((ge_representation_real_code_gcd_bounded_resultbezoutsecondfirst) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondfirst)) * S ((ge_representation_real_code_gcd_bounded_resultbezoutsecondfirst) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondfirst)) + ((ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondfirst) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondfirst))) /\ ((exists ge_balance_positive_gcd_bounded_resultbezoutsecondfirstreal ge_balance_negative_gcd_bounded_resultbezoutsecondfirstreal. (((((ge_representation_real_code_gcd_bounded_resultbezoutsecondfirst) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsecondfirstreal) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondfirstreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsecondfirstrealdecode. (((ge_representation_real_code_gcd_bounded_resultbezoutsecondfirst) = 2 * ge_signed_half_gcd_bounded_resultbezoutsecondfirstrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsecondfirstreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondfirstreal) = S ge_signed_half_gcd_bounded_resultbezoutsecondfirstrealdecode))) /\ ((ge_first_rp_gcd_bounded_resultbezoutsecond) + ge_balance_negative_gcd_bounded_resultbezoutsecondfirstreal = (ge_first_rn_gcd_bounded_resultbezoutsecond) + ge_balance_positive_gcd_bounded_resultbezoutsecondfirstreal))) /\ (exists ge_balance_positive_gcd_bounded_resultbezoutsecondfirstimaginary ge_balance_negative_gcd_bounded_resultbezoutsecondfirstimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondfirst) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsecondfirstimaginary) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondfirstimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsecondfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondfirst) = 2 * ge_signed_half_gcd_bounded_resultbezoutsecondfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsecondfirstimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondfirstimaginary) = S ge_signed_half_gcd_bounded_resultbezoutsecondfirstimaginarydecode))) /\ ((ge_first_ip_gcd_bounded_resultbezoutsecond) + ge_balance_negative_gcd_bounded_resultbezoutsecondfirstimaginary = (ge_first_in_gcd_bounded_resultbezoutsecond) + ge_balance_positive_gcd_bounded_resultbezoutsecondfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_bounded_resultbezoutsecondsecond ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondsecond. (((gr_second_coefficient_gcd_bounded_result) = ((ge_representation_real_code_gcd_bounded_resultbezoutsecondsecond) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondsecond)) * S ((ge_representation_real_code_gcd_bounded_resultbezoutsecondsecond) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondsecond)) + ((ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondsecond) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondsecond))) /\ ((exists ge_balance_positive_gcd_bounded_resultbezoutsecondsecondreal ge_balance_negative_gcd_bounded_resultbezoutsecondsecondreal. (((((ge_representation_real_code_gcd_bounded_resultbezoutsecondsecond) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsecondsecondreal) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondsecondreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsecondsecondrealdecode. (((ge_representation_real_code_gcd_bounded_resultbezoutsecondsecond) = 2 * ge_signed_half_gcd_bounded_resultbezoutsecondsecondrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsecondsecondreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondsecondreal) = S ge_signed_half_gcd_bounded_resultbezoutsecondsecondrealdecode))) /\ ((ge_second_rp_gcd_bounded_resultbezoutsecond) + ge_balance_negative_gcd_bounded_resultbezoutsecondsecondreal = (ge_second_rn_gcd_bounded_resultbezoutsecond) + ge_balance_positive_gcd_bounded_resultbezoutsecondsecondreal))) /\ (exists ge_balance_positive_gcd_bounded_resultbezoutsecondsecondimaginary ge_balance_negative_gcd_bounded_resultbezoutsecondsecondimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondsecond) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsecondsecondimaginary) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondsecondimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsecondsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondsecond) = 2 * ge_signed_half_gcd_bounded_resultbezoutsecondsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsecondsecondimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondsecondimaginary) = S ge_signed_half_gcd_bounded_resultbezoutsecondsecondimaginarydecode))) /\ ((ge_second_ip_gcd_bounded_resultbezoutsecond) + ge_balance_negative_gcd_bounded_resultbezoutsecondsecondimaginary = (ge_second_in_gcd_bounded_resultbezoutsecond) + ge_balance_positive_gcd_bounded_resultbezoutsecondsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_bounded_resultbezoutsecondoutput ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondoutput. (((gr_second_product_gcd_bounded_resultbezout) = ((ge_representation_real_code_gcd_bounded_resultbezoutsecondoutput) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondoutput)) * S ((ge_representation_real_code_gcd_bounded_resultbezoutsecondoutput) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondoutput)) + ((ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondoutput) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondoutput))) /\ ((exists ge_balance_positive_gcd_bounded_resultbezoutsecondoutputreal ge_balance_negative_gcd_bounded_resultbezoutsecondoutputreal. (((((ge_representation_real_code_gcd_bounded_resultbezoutsecondoutput) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsecondoutputreal) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondoutputreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsecondoutputrealdecode. (((ge_representation_real_code_gcd_bounded_resultbezoutsecondoutput) = 2 * ge_signed_half_gcd_bounded_resultbezoutsecondoutputrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsecondoutputreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondoutputreal) = S ge_signed_half_gcd_bounded_resultbezoutsecondoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultbezoutsecond) * (ge_second_rp_gcd_bounded_resultbezoutsecond))) + (((ge_first_rn_gcd_bounded_resultbezoutsecond) * (ge_second_rn_gcd_bounded_resultbezoutsecond))))) + (((((ge_first_ip_gcd_bounded_resultbezoutsecond) * (ge_second_in_gcd_bounded_resultbezoutsecond))) + (((ge_first_in_gcd_bounded_resultbezoutsecond) * (ge_second_ip_gcd_bounded_resultbezoutsecond))))))) + ge_balance_negative_gcd_bounded_resultbezoutsecondoutputreal = (((((((ge_first_rp_gcd_bounded_resultbezoutsecond) * (ge_second_rn_gcd_bounded_resultbezoutsecond))) + (((ge_first_rn_gcd_bounded_resultbezoutsecond) * (ge_second_rp_gcd_bounded_resultbezoutsecond))))) + (((((ge_first_ip_gcd_bounded_resultbezoutsecond) * (ge_second_ip_gcd_bounded_resultbezoutsecond))) + (((ge_first_in_gcd_bounded_resultbezoutsecond) * (ge_second_in_gcd_bounded_resultbezoutsecond))))))) + ge_balance_positive_gcd_bounded_resultbezoutsecondoutputreal))) /\ (exists ge_balance_positive_gcd_bounded_resultbezoutsecondoutputimaginary ge_balance_negative_gcd_bounded_resultbezoutsecondoutputimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondoutput) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsecondoutputimaginary) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondoutputimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsecondoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultbezoutsecondoutput) = 2 * ge_signed_half_gcd_bounded_resultbezoutsecondoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsecondoutputimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsecondoutputimaginary) = S ge_signed_half_gcd_bounded_resultbezoutsecondoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_bounded_resultbezoutsecond) * (ge_second_ip_gcd_bounded_resultbezoutsecond))) + (((ge_first_rn_gcd_bounded_resultbezoutsecond) * (ge_second_in_gcd_bounded_resultbezoutsecond))))) + (((((ge_first_ip_gcd_bounded_resultbezoutsecond) * (ge_second_rp_gcd_bounded_resultbezoutsecond))) + (((ge_first_in_gcd_bounded_resultbezoutsecond) * (ge_second_rn_gcd_bounded_resultbezoutsecond))))))) + ge_balance_negative_gcd_bounded_resultbezoutsecondoutputimaginary = (((((((ge_first_rp_gcd_bounded_resultbezoutsecond) * (ge_second_in_gcd_bounded_resultbezoutsecond))) + (((ge_first_rn_gcd_bounded_resultbezoutsecond) * (ge_second_ip_gcd_bounded_resultbezoutsecond))))) + (((((ge_first_ip_gcd_bounded_resultbezoutsecond) * (ge_second_rn_gcd_bounded_resultbezoutsecond))) + (((ge_first_in_gcd_bounded_resultbezoutsecond) * (ge_second_rp_gcd_bounded_resultbezoutsecond))))))) + ge_balance_positive_gcd_bounded_resultbezoutsecondoutputimaginary))))))))) /\ (exists ge_first_rp_gcd_bounded_resultbezoutsum ge_first_rn_gcd_bounded_resultbezoutsum ge_first_ip_gcd_bounded_resultbezoutsum ge_first_in_gcd_bounded_resultbezoutsum ge_second_rp_gcd_bounded_resultbezoutsum ge_second_rn_gcd_bounded_resultbezoutsum ge_second_ip_gcd_bounded_resultbezoutsum ge_second_in_gcd_bounded_resultbezoutsum. ((exists ge_representation_real_code_gcd_bounded_resultbezoutsumfirst ge_representation_imaginary_code_gcd_bounded_resultbezoutsumfirst. (((gr_first_product_gcd_bounded_resultbezout) = ((ge_representation_real_code_gcd_bounded_resultbezoutsumfirst) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsumfirst)) * S ((ge_representation_real_code_gcd_bounded_resultbezoutsumfirst) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsumfirst)) + ((ge_representation_imaginary_code_gcd_bounded_resultbezoutsumfirst) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsumfirst))) /\ ((exists ge_balance_positive_gcd_bounded_resultbezoutsumfirstreal ge_balance_negative_gcd_bounded_resultbezoutsumfirstreal. (((((ge_representation_real_code_gcd_bounded_resultbezoutsumfirst) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsumfirstreal) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumfirstreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsumfirstrealdecode. (((ge_representation_real_code_gcd_bounded_resultbezoutsumfirst) = 2 * ge_signed_half_gcd_bounded_resultbezoutsumfirstrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsumfirstreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumfirstreal) = S ge_signed_half_gcd_bounded_resultbezoutsumfirstrealdecode))) /\ ((ge_first_rp_gcd_bounded_resultbezoutsum) + ge_balance_negative_gcd_bounded_resultbezoutsumfirstreal = (ge_first_rn_gcd_bounded_resultbezoutsum) + ge_balance_positive_gcd_bounded_resultbezoutsumfirstreal))) /\ (exists ge_balance_positive_gcd_bounded_resultbezoutsumfirstimaginary ge_balance_negative_gcd_bounded_resultbezoutsumfirstimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultbezoutsumfirst) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsumfirstimaginary) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumfirstimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsumfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultbezoutsumfirst) = 2 * ge_signed_half_gcd_bounded_resultbezoutsumfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsumfirstimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumfirstimaginary) = S ge_signed_half_gcd_bounded_resultbezoutsumfirstimaginarydecode))) /\ ((ge_first_ip_gcd_bounded_resultbezoutsum) + ge_balance_negative_gcd_bounded_resultbezoutsumfirstimaginary = (ge_first_in_gcd_bounded_resultbezoutsum) + ge_balance_positive_gcd_bounded_resultbezoutsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_bounded_resultbezoutsumsecond ge_representation_imaginary_code_gcd_bounded_resultbezoutsumsecond. (((gr_second_product_gcd_bounded_resultbezout) = ((ge_representation_real_code_gcd_bounded_resultbezoutsumsecond) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsumsecond)) * S ((ge_representation_real_code_gcd_bounded_resultbezoutsumsecond) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsumsecond)) + ((ge_representation_imaginary_code_gcd_bounded_resultbezoutsumsecond) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsumsecond))) /\ ((exists ge_balance_positive_gcd_bounded_resultbezoutsumsecondreal ge_balance_negative_gcd_bounded_resultbezoutsumsecondreal. (((((ge_representation_real_code_gcd_bounded_resultbezoutsumsecond) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsumsecondreal) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumsecondreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsumsecondrealdecode. (((ge_representation_real_code_gcd_bounded_resultbezoutsumsecond) = 2 * ge_signed_half_gcd_bounded_resultbezoutsumsecondrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsumsecondreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumsecondreal) = S ge_signed_half_gcd_bounded_resultbezoutsumsecondrealdecode))) /\ ((ge_second_rp_gcd_bounded_resultbezoutsum) + ge_balance_negative_gcd_bounded_resultbezoutsumsecondreal = (ge_second_rn_gcd_bounded_resultbezoutsum) + ge_balance_positive_gcd_bounded_resultbezoutsumsecondreal))) /\ (exists ge_balance_positive_gcd_bounded_resultbezoutsumsecondimaginary ge_balance_negative_gcd_bounded_resultbezoutsumsecondimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultbezoutsumsecond) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsumsecondimaginary) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumsecondimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsumsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultbezoutsumsecond) = 2 * ge_signed_half_gcd_bounded_resultbezoutsumsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsumsecondimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumsecondimaginary) = S ge_signed_half_gcd_bounded_resultbezoutsumsecondimaginarydecode))) /\ ((ge_second_ip_gcd_bounded_resultbezoutsum) + ge_balance_negative_gcd_bounded_resultbezoutsumsecondimaginary = (ge_second_in_gcd_bounded_resultbezoutsum) + ge_balance_positive_gcd_bounded_resultbezoutsumsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_bounded_resultbezoutsumoutput ge_representation_imaginary_code_gcd_bounded_resultbezoutsumoutput. (((gr_gcd_gcd_bounded_result) = ((ge_representation_real_code_gcd_bounded_resultbezoutsumoutput) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsumoutput)) * S ((ge_representation_real_code_gcd_bounded_resultbezoutsumoutput) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsumoutput)) + ((ge_representation_imaginary_code_gcd_bounded_resultbezoutsumoutput) + (ge_representation_imaginary_code_gcd_bounded_resultbezoutsumoutput))) /\ ((exists ge_balance_positive_gcd_bounded_resultbezoutsumoutputreal ge_balance_negative_gcd_bounded_resultbezoutsumoutputreal. (((((ge_representation_real_code_gcd_bounded_resultbezoutsumoutput) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsumoutputreal) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumoutputreal) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsumoutputrealdecode. (((ge_representation_real_code_gcd_bounded_resultbezoutsumoutput) = 2 * ge_signed_half_gcd_bounded_resultbezoutsumoutputrealdecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsumoutputreal) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumoutputreal) = S ge_signed_half_gcd_bounded_resultbezoutsumoutputrealdecode))) /\ ((((ge_first_rp_gcd_bounded_resultbezoutsum) + (ge_second_rp_gcd_bounded_resultbezoutsum))) + ge_balance_negative_gcd_bounded_resultbezoutsumoutputreal = (((ge_first_rn_gcd_bounded_resultbezoutsum) + (ge_second_rn_gcd_bounded_resultbezoutsum))) + ge_balance_positive_gcd_bounded_resultbezoutsumoutputreal))) /\ (exists ge_balance_positive_gcd_bounded_resultbezoutsumoutputimaginary ge_balance_negative_gcd_bounded_resultbezoutsumoutputimaginary. (((((ge_representation_imaginary_code_gcd_bounded_resultbezoutsumoutput) = 2 * (ge_balance_positive_gcd_bounded_resultbezoutsumoutputimaginary) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumoutputimaginary) = 0) \/ exists ge_signed_half_gcd_bounded_resultbezoutsumoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_bounded_resultbezoutsumoutput) = 2 * ge_signed_half_gcd_bounded_resultbezoutsumoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_bounded_resultbezoutsumoutputimaginary) = 0) /\ (ge_balance_negative_gcd_bounded_resultbezoutsumoutputimaginary) = S ge_signed_half_gcd_bounded_resultbezoutsumoutputimaginarydecode))) /\ ((((ge_first_ip_gcd_bounded_resultbezoutsum) + (ge_second_ip_gcd_bounded_resultbezoutsum))) + ge_balance_negative_gcd_bounded_resultbezoutsumoutputimaginary = (((ge_first_in_gcd_bounded_resultbezoutsum) + (ge_second_in_gcd_bounded_resultbezoutsum))) + ge_balance_positive_gcd_bounded_resultbezoutsumoutputimaginary))))))))))))))