gaussian_gcd_bezout_zero_case

Exact expanded first-order arithmetic statement

forall a b. (exists ge_real_positive_gcd_zero_case_first ge_real_negative_gcd_zero_case_first ge_imaginary_positive_gcd_zero_case_first ge_imaginary_negative_gcd_zero_case_first. (exists ge_real_code_gcd_zero_case_firstdecode ge_imaginary_code_gcd_zero_case_firstdecode. (((a) = ((ge_real_code_gcd_zero_case_firstdecode) + (ge_imaginary_code_gcd_zero_case_firstdecode)) * S ((ge_real_code_gcd_zero_case_firstdecode) + (ge_imaginary_code_gcd_zero_case_firstdecode)) + ((ge_imaginary_code_gcd_zero_case_firstdecode) + (ge_imaginary_code_gcd_zero_case_firstdecode))) /\ (((((ge_real_code_gcd_zero_case_firstdecode) = 2 * (ge_real_positive_gcd_zero_case_first) /\ (ge_real_negative_gcd_zero_case_first) = 0) \/ exists ge_signed_half_ge_gcd_zero_case_firstdecode_real. (((ge_real_code_gcd_zero_case_firstdecode) = 2 * ge_signed_half_ge_gcd_zero_case_firstdecode_real + 1 /\ (ge_real_positive_gcd_zero_case_first) = 0) /\ (ge_real_negative_gcd_zero_case_first) = S ge_signed_half_ge_gcd_zero_case_firstdecode_real))) /\ ((((ge_imaginary_code_gcd_zero_case_firstdecode) = 2 * (ge_imaginary_positive_gcd_zero_case_first) /\ (ge_imaginary_negative_gcd_zero_case_first) = 0) \/ exists ge_signed_half_ge_gcd_zero_case_firstdecode_imaginary. (((ge_imaginary_code_gcd_zero_case_firstdecode) = 2 * ge_signed_half_ge_gcd_zero_case_firstdecode_imaginary + 1 /\ (ge_imaginary_positive_gcd_zero_case_first) = 0) /\ (ge_imaginary_negative_gcd_zero_case_first) = S ge_signed_half_ge_gcd_zero_case_firstdecode_imaginary))))))) -> (exists ge_real_positive_gcd_zero_case_second ge_real_negative_gcd_zero_case_second ge_imaginary_positive_gcd_zero_case_second ge_imaginary_negative_gcd_zero_case_second. (exists ge_real_code_gcd_zero_case_seconddecode ge_imaginary_code_gcd_zero_case_seconddecode. (((b) = ((ge_real_code_gcd_zero_case_seconddecode) + (ge_imaginary_code_gcd_zero_case_seconddecode)) * S ((ge_real_code_gcd_zero_case_seconddecode) + (ge_imaginary_code_gcd_zero_case_seconddecode)) + ((ge_imaginary_code_gcd_zero_case_seconddecode) + (ge_imaginary_code_gcd_zero_case_seconddecode))) /\ (((((ge_real_code_gcd_zero_case_seconddecode) = 2 * (ge_real_positive_gcd_zero_case_second) /\ (ge_real_negative_gcd_zero_case_second) = 0) \/ exists ge_signed_half_ge_gcd_zero_case_seconddecode_real. (((ge_real_code_gcd_zero_case_seconddecode) = 2 * ge_signed_half_ge_gcd_zero_case_seconddecode_real + 1 /\ (ge_real_positive_gcd_zero_case_second) = 0) /\ (ge_real_negative_gcd_zero_case_second) = S ge_signed_half_ge_gcd_zero_case_seconddecode_real))) /\ ((((ge_imaginary_code_gcd_zero_case_seconddecode) = 2 * (ge_imaginary_positive_gcd_zero_case_second) /\ (ge_imaginary_negative_gcd_zero_case_second) = 0) \/ exists ge_signed_half_ge_gcd_zero_case_seconddecode_imaginary. (((ge_imaginary_code_gcd_zero_case_seconddecode) = 2 * ge_signed_half_ge_gcd_zero_case_seconddecode_imaginary + 1 /\ (ge_imaginary_positive_gcd_zero_case_second) = 0) /\ (ge_imaginary_negative_gcd_zero_case_second) = S ge_signed_half_ge_gcd_zero_case_seconddecode_imaginary))))))) -> b=0 -> (exists gr_gcd_gcd_zero_case gr_first_coefficient_gcd_zero_case gr_second_coefficient_gcd_zero_case. ((((exists gr_quotient_gcd_zero_casegcdfirst. (exists ge_first_rp_gcd_zero_casegcdfirstproduct ge_first_rn_gcd_zero_casegcdfirstproduct ge_first_ip_gcd_zero_casegcdfirstproduct ge_first_in_gcd_zero_casegcdfirstproduct ge_second_rp_gcd_zero_casegcdfirstproduct ge_second_rn_gcd_zero_casegcdfirstproduct ge_second_ip_gcd_zero_casegcdfirstproduct ge_second_in_gcd_zero_casegcdfirstproduct. ((exists ge_representation_real_code_gcd_zero_casegcdfirstproductfirst ge_representation_imaginary_code_gcd_zero_casegcdfirstproductfirst. (((gr_gcd_gcd_zero_case) = ((ge_representation_real_code_gcd_zero_casegcdfirstproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdfirstproductfirst)) * S ((ge_representation_real_code_gcd_zero_casegcdfirstproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdfirstproductfirst)) + ((ge_representation_imaginary_code_gcd_zero_casegcdfirstproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdfirstproductfirst))) /\ ((exists ge_balance_positive_gcd_zero_casegcdfirstproductfirstreal ge_balance_negative_gcd_zero_casegcdfirstproductfirstreal. (((((ge_representation_real_code_gcd_zero_casegcdfirstproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdfirstproductfirstreal) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdfirstproductfirstrealdecode. (((ge_representation_real_code_gcd_zero_casegcdfirstproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdfirstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdfirstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductfirstreal) = S ge_signed_half_gcd_zero_casegcdfirstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zero_casegcdfirstproduct) + ge_balance_negative_gcd_zero_casegcdfirstproductfirstreal = (ge_first_rn_gcd_zero_casegcdfirstproduct) + ge_balance_positive_gcd_zero_casegcdfirstproductfirstreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdfirstproductfirstimaginary ge_balance_negative_gcd_zero_casegcdfirstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdfirstproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdfirstproductfirstimaginary) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdfirstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdfirstproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdfirstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdfirstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductfirstimaginary) = S ge_signed_half_gcd_zero_casegcdfirstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zero_casegcdfirstproduct) + ge_balance_negative_gcd_zero_casegcdfirstproductfirstimaginary = (ge_first_in_gcd_zero_casegcdfirstproduct) + ge_balance_positive_gcd_zero_casegcdfirstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zero_casegcdfirstproductsecond ge_representation_imaginary_code_gcd_zero_casegcdfirstproductsecond. (((gr_quotient_gcd_zero_casegcdfirst) = ((ge_representation_real_code_gcd_zero_casegcdfirstproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdfirstproductsecond)) * S ((ge_representation_real_code_gcd_zero_casegcdfirstproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdfirstproductsecond)) + ((ge_representation_imaginary_code_gcd_zero_casegcdfirstproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdfirstproductsecond))) /\ ((exists ge_balance_positive_gcd_zero_casegcdfirstproductsecondreal ge_balance_negative_gcd_zero_casegcdfirstproductsecondreal. (((((ge_representation_real_code_gcd_zero_casegcdfirstproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdfirstproductsecondreal) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdfirstproductsecondrealdecode. (((ge_representation_real_code_gcd_zero_casegcdfirstproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdfirstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdfirstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductsecondreal) = S ge_signed_half_gcd_zero_casegcdfirstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zero_casegcdfirstproduct) + ge_balance_negative_gcd_zero_casegcdfirstproductsecondreal = (ge_second_rn_gcd_zero_casegcdfirstproduct) + ge_balance_positive_gcd_zero_casegcdfirstproductsecondreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdfirstproductsecondimaginary ge_balance_negative_gcd_zero_casegcdfirstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdfirstproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdfirstproductsecondimaginary) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdfirstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdfirstproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdfirstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdfirstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductsecondimaginary) = S ge_signed_half_gcd_zero_casegcdfirstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zero_casegcdfirstproduct) + ge_balance_negative_gcd_zero_casegcdfirstproductsecondimaginary = (ge_second_in_gcd_zero_casegcdfirstproduct) + ge_balance_positive_gcd_zero_casegcdfirstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zero_casegcdfirstproductoutput ge_representation_imaginary_code_gcd_zero_casegcdfirstproductoutput. (((a) = ((ge_representation_real_code_gcd_zero_casegcdfirstproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdfirstproductoutput)) * S ((ge_representation_real_code_gcd_zero_casegcdfirstproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdfirstproductoutput)) + ((ge_representation_imaginary_code_gcd_zero_casegcdfirstproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdfirstproductoutput))) /\ ((exists ge_balance_positive_gcd_zero_casegcdfirstproductoutputreal ge_balance_negative_gcd_zero_casegcdfirstproductoutputreal. (((((ge_representation_real_code_gcd_zero_casegcdfirstproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdfirstproductoutputreal) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdfirstproductoutputrealdecode. (((ge_representation_real_code_gcd_zero_casegcdfirstproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdfirstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdfirstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductoutputreal) = S ge_signed_half_gcd_zero_casegcdfirstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdfirstproduct) * (ge_second_rp_gcd_zero_casegcdfirstproduct))) + (((ge_first_rn_gcd_zero_casegcdfirstproduct) * (ge_second_rn_gcd_zero_casegcdfirstproduct))))) + (((((ge_first_ip_gcd_zero_casegcdfirstproduct) * (ge_second_in_gcd_zero_casegcdfirstproduct))) + (((ge_first_in_gcd_zero_casegcdfirstproduct) * (ge_second_ip_gcd_zero_casegcdfirstproduct))))))) + ge_balance_negative_gcd_zero_casegcdfirstproductoutputreal = (((((((ge_first_rp_gcd_zero_casegcdfirstproduct) * (ge_second_rn_gcd_zero_casegcdfirstproduct))) + (((ge_first_rn_gcd_zero_casegcdfirstproduct) * (ge_second_rp_gcd_zero_casegcdfirstproduct))))) + (((((ge_first_ip_gcd_zero_casegcdfirstproduct) * (ge_second_ip_gcd_zero_casegcdfirstproduct))) + (((ge_first_in_gcd_zero_casegcdfirstproduct) * (ge_second_in_gcd_zero_casegcdfirstproduct))))))) + ge_balance_positive_gcd_zero_casegcdfirstproductoutputreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdfirstproductoutputimaginary ge_balance_negative_gcd_zero_casegcdfirstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdfirstproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdfirstproductoutputimaginary) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdfirstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdfirstproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdfirstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdfirstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdfirstproductoutputimaginary) = S ge_signed_half_gcd_zero_casegcdfirstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdfirstproduct) * (ge_second_ip_gcd_zero_casegcdfirstproduct))) + (((ge_first_rn_gcd_zero_casegcdfirstproduct) * (ge_second_in_gcd_zero_casegcdfirstproduct))))) + (((((ge_first_ip_gcd_zero_casegcdfirstproduct) * (ge_second_rp_gcd_zero_casegcdfirstproduct))) + (((ge_first_in_gcd_zero_casegcdfirstproduct) * (ge_second_rn_gcd_zero_casegcdfirstproduct))))))) + ge_balance_negative_gcd_zero_casegcdfirstproductoutputimaginary = (((((((ge_first_rp_gcd_zero_casegcdfirstproduct) * (ge_second_in_gcd_zero_casegcdfirstproduct))) + (((ge_first_rn_gcd_zero_casegcdfirstproduct) * (ge_second_ip_gcd_zero_casegcdfirstproduct))))) + (((((ge_first_ip_gcd_zero_casegcdfirstproduct) * (ge_second_rn_gcd_zero_casegcdfirstproduct))) + (((ge_first_in_gcd_zero_casegcdfirstproduct) * (ge_second_rp_gcd_zero_casegcdfirstproduct))))))) + ge_balance_positive_gcd_zero_casegcdfirstproductoutputimaginary)))))))))) /\ ((exists gr_quotient_gcd_zero_casegcdsecond. (exists ge_first_rp_gcd_zero_casegcdsecondproduct ge_first_rn_gcd_zero_casegcdsecondproduct ge_first_ip_gcd_zero_casegcdsecondproduct ge_first_in_gcd_zero_casegcdsecondproduct ge_second_rp_gcd_zero_casegcdsecondproduct ge_second_rn_gcd_zero_casegcdsecondproduct ge_second_ip_gcd_zero_casegcdsecondproduct ge_second_in_gcd_zero_casegcdsecondproduct. ((exists ge_representation_real_code_gcd_zero_casegcdsecondproductfirst ge_representation_imaginary_code_gcd_zero_casegcdsecondproductfirst. (((gr_gcd_gcd_zero_case) = ((ge_representation_real_code_gcd_zero_casegcdsecondproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdsecondproductfirst)) * S ((ge_representation_real_code_gcd_zero_casegcdsecondproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdsecondproductfirst)) + ((ge_representation_imaginary_code_gcd_zero_casegcdsecondproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdsecondproductfirst))) /\ ((exists ge_balance_positive_gcd_zero_casegcdsecondproductfirstreal ge_balance_negative_gcd_zero_casegcdsecondproductfirstreal. (((((ge_representation_real_code_gcd_zero_casegcdsecondproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdsecondproductfirstreal) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdsecondproductfirstrealdecode. (((ge_representation_real_code_gcd_zero_casegcdsecondproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdsecondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdsecondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductfirstreal) = S ge_signed_half_gcd_zero_casegcdsecondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zero_casegcdsecondproduct) + ge_balance_negative_gcd_zero_casegcdsecondproductfirstreal = (ge_first_rn_gcd_zero_casegcdsecondproduct) + ge_balance_positive_gcd_zero_casegcdsecondproductfirstreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdsecondproductfirstimaginary ge_balance_negative_gcd_zero_casegcdsecondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdsecondproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdsecondproductfirstimaginary) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdsecondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdsecondproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdsecondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdsecondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductfirstimaginary) = S ge_signed_half_gcd_zero_casegcdsecondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zero_casegcdsecondproduct) + ge_balance_negative_gcd_zero_casegcdsecondproductfirstimaginary = (ge_first_in_gcd_zero_casegcdsecondproduct) + ge_balance_positive_gcd_zero_casegcdsecondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zero_casegcdsecondproductsecond ge_representation_imaginary_code_gcd_zero_casegcdsecondproductsecond. (((gr_quotient_gcd_zero_casegcdsecond) = ((ge_representation_real_code_gcd_zero_casegcdsecondproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdsecondproductsecond)) * S ((ge_representation_real_code_gcd_zero_casegcdsecondproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdsecondproductsecond)) + ((ge_representation_imaginary_code_gcd_zero_casegcdsecondproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdsecondproductsecond))) /\ ((exists ge_balance_positive_gcd_zero_casegcdsecondproductsecondreal ge_balance_negative_gcd_zero_casegcdsecondproductsecondreal. (((((ge_representation_real_code_gcd_zero_casegcdsecondproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdsecondproductsecondreal) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdsecondproductsecondrealdecode. (((ge_representation_real_code_gcd_zero_casegcdsecondproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdsecondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdsecondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductsecondreal) = S ge_signed_half_gcd_zero_casegcdsecondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zero_casegcdsecondproduct) + ge_balance_negative_gcd_zero_casegcdsecondproductsecondreal = (ge_second_rn_gcd_zero_casegcdsecondproduct) + ge_balance_positive_gcd_zero_casegcdsecondproductsecondreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdsecondproductsecondimaginary ge_balance_negative_gcd_zero_casegcdsecondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdsecondproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdsecondproductsecondimaginary) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdsecondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdsecondproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdsecondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdsecondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductsecondimaginary) = S ge_signed_half_gcd_zero_casegcdsecondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zero_casegcdsecondproduct) + ge_balance_negative_gcd_zero_casegcdsecondproductsecondimaginary = (ge_second_in_gcd_zero_casegcdsecondproduct) + ge_balance_positive_gcd_zero_casegcdsecondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zero_casegcdsecondproductoutput ge_representation_imaginary_code_gcd_zero_casegcdsecondproductoutput. (((b) = ((ge_representation_real_code_gcd_zero_casegcdsecondproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdsecondproductoutput)) * S ((ge_representation_real_code_gcd_zero_casegcdsecondproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdsecondproductoutput)) + ((ge_representation_imaginary_code_gcd_zero_casegcdsecondproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdsecondproductoutput))) /\ ((exists ge_balance_positive_gcd_zero_casegcdsecondproductoutputreal ge_balance_negative_gcd_zero_casegcdsecondproductoutputreal. (((((ge_representation_real_code_gcd_zero_casegcdsecondproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdsecondproductoutputreal) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdsecondproductoutputrealdecode. (((ge_representation_real_code_gcd_zero_casegcdsecondproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdsecondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdsecondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductoutputreal) = S ge_signed_half_gcd_zero_casegcdsecondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdsecondproduct) * (ge_second_rp_gcd_zero_casegcdsecondproduct))) + (((ge_first_rn_gcd_zero_casegcdsecondproduct) * (ge_second_rn_gcd_zero_casegcdsecondproduct))))) + (((((ge_first_ip_gcd_zero_casegcdsecondproduct) * (ge_second_in_gcd_zero_casegcdsecondproduct))) + (((ge_first_in_gcd_zero_casegcdsecondproduct) * (ge_second_ip_gcd_zero_casegcdsecondproduct))))))) + ge_balance_negative_gcd_zero_casegcdsecondproductoutputreal = (((((((ge_first_rp_gcd_zero_casegcdsecondproduct) * (ge_second_rn_gcd_zero_casegcdsecondproduct))) + (((ge_first_rn_gcd_zero_casegcdsecondproduct) * (ge_second_rp_gcd_zero_casegcdsecondproduct))))) + (((((ge_first_ip_gcd_zero_casegcdsecondproduct) * (ge_second_ip_gcd_zero_casegcdsecondproduct))) + (((ge_first_in_gcd_zero_casegcdsecondproduct) * (ge_second_in_gcd_zero_casegcdsecondproduct))))))) + ge_balance_positive_gcd_zero_casegcdsecondproductoutputreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdsecondproductoutputimaginary ge_balance_negative_gcd_zero_casegcdsecondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdsecondproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdsecondproductoutputimaginary) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdsecondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdsecondproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdsecondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdsecondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdsecondproductoutputimaginary) = S ge_signed_half_gcd_zero_casegcdsecondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdsecondproduct) * (ge_second_ip_gcd_zero_casegcdsecondproduct))) + (((ge_first_rn_gcd_zero_casegcdsecondproduct) * (ge_second_in_gcd_zero_casegcdsecondproduct))))) + (((((ge_first_ip_gcd_zero_casegcdsecondproduct) * (ge_second_rp_gcd_zero_casegcdsecondproduct))) + (((ge_first_in_gcd_zero_casegcdsecondproduct) * (ge_second_rn_gcd_zero_casegcdsecondproduct))))))) + ge_balance_negative_gcd_zero_casegcdsecondproductoutputimaginary = (((((((ge_first_rp_gcd_zero_casegcdsecondproduct) * (ge_second_in_gcd_zero_casegcdsecondproduct))) + (((ge_first_rn_gcd_zero_casegcdsecondproduct) * (ge_second_ip_gcd_zero_casegcdsecondproduct))))) + (((((ge_first_ip_gcd_zero_casegcdsecondproduct) * (ge_second_rn_gcd_zero_casegcdsecondproduct))) + (((ge_first_in_gcd_zero_casegcdsecondproduct) * (ge_second_rp_gcd_zero_casegcdsecondproduct))))))) + ge_balance_positive_gcd_zero_casegcdsecondproductoutputimaginary)))))))))) /\ (forall gr_common_divisor_gcd_zero_casegcd. (exists gr_quotient_gcd_zero_casegcdcommon_first. (exists ge_first_rp_gcd_zero_casegcdcommon_firstproduct ge_first_rn_gcd_zero_casegcdcommon_firstproduct ge_first_ip_gcd_zero_casegcdcommon_firstproduct ge_first_in_gcd_zero_casegcdcommon_firstproduct ge_second_rp_gcd_zero_casegcdcommon_firstproduct ge_second_rn_gcd_zero_casegcdcommon_firstproduct ge_second_ip_gcd_zero_casegcdcommon_firstproduct ge_second_in_gcd_zero_casegcdcommon_firstproduct. ((exists ge_representation_real_code_gcd_zero_casegcdcommon_firstproductfirst ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductfirst. (((gr_common_divisor_gcd_zero_casegcd) = ((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductfirst)) * S ((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductfirst)) + ((ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductfirst))) /\ ((exists ge_balance_positive_gcd_zero_casegcdcommon_firstproductfirstreal ge_balance_negative_gcd_zero_casegcdcommon_firstproductfirstreal. (((((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_firstproductfirstreal) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_firstproductfirstrealdecode. (((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdcommon_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_firstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductfirstreal) = S ge_signed_half_gcd_zero_casegcdcommon_firstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zero_casegcdcommon_firstproduct) + ge_balance_negative_gcd_zero_casegcdcommon_firstproductfirstreal = (ge_first_rn_gcd_zero_casegcdcommon_firstproduct) + ge_balance_positive_gcd_zero_casegcdcommon_firstproductfirstreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdcommon_firstproductfirstimaginary ge_balance_negative_gcd_zero_casegcdcommon_firstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_firstproductfirstimaginary) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdcommon_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductfirstimaginary) = S ge_signed_half_gcd_zero_casegcdcommon_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zero_casegcdcommon_firstproduct) + ge_balance_negative_gcd_zero_casegcdcommon_firstproductfirstimaginary = (ge_first_in_gcd_zero_casegcdcommon_firstproduct) + ge_balance_positive_gcd_zero_casegcdcommon_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zero_casegcdcommon_firstproductsecond ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductsecond. (((gr_quotient_gcd_zero_casegcdcommon_first) = ((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductsecond)) * S ((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductsecond)) + ((ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductsecond))) /\ ((exists ge_balance_positive_gcd_zero_casegcdcommon_firstproductsecondreal ge_balance_negative_gcd_zero_casegcdcommon_firstproductsecondreal. (((((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_firstproductsecondreal) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_firstproductsecondrealdecode. (((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdcommon_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_firstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductsecondreal) = S ge_signed_half_gcd_zero_casegcdcommon_firstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zero_casegcdcommon_firstproduct) + ge_balance_negative_gcd_zero_casegcdcommon_firstproductsecondreal = (ge_second_rn_gcd_zero_casegcdcommon_firstproduct) + ge_balance_positive_gcd_zero_casegcdcommon_firstproductsecondreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdcommon_firstproductsecondimaginary ge_balance_negative_gcd_zero_casegcdcommon_firstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_firstproductsecondimaginary) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdcommon_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductsecondimaginary) = S ge_signed_half_gcd_zero_casegcdcommon_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zero_casegcdcommon_firstproduct) + ge_balance_negative_gcd_zero_casegcdcommon_firstproductsecondimaginary = (ge_second_in_gcd_zero_casegcdcommon_firstproduct) + ge_balance_positive_gcd_zero_casegcdcommon_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zero_casegcdcommon_firstproductoutput ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductoutput. (((a) = ((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductoutput)) * S ((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductoutput)) + ((ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductoutput))) /\ ((exists ge_balance_positive_gcd_zero_casegcdcommon_firstproductoutputreal ge_balance_negative_gcd_zero_casegcdcommon_firstproductoutputreal. (((((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_firstproductoutputreal) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_firstproductoutputrealdecode. (((ge_representation_real_code_gcd_zero_casegcdcommon_firstproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdcommon_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_firstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductoutputreal) = S ge_signed_half_gcd_zero_casegcdcommon_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdcommon_firstproduct) * (ge_second_rp_gcd_zero_casegcdcommon_firstproduct))) + (((ge_first_rn_gcd_zero_casegcdcommon_firstproduct) * (ge_second_rn_gcd_zero_casegcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_zero_casegcdcommon_firstproduct) * (ge_second_in_gcd_zero_casegcdcommon_firstproduct))) + (((ge_first_in_gcd_zero_casegcdcommon_firstproduct) * (ge_second_ip_gcd_zero_casegcdcommon_firstproduct))))))) + ge_balance_negative_gcd_zero_casegcdcommon_firstproductoutputreal = (((((((ge_first_rp_gcd_zero_casegcdcommon_firstproduct) * (ge_second_rn_gcd_zero_casegcdcommon_firstproduct))) + (((ge_first_rn_gcd_zero_casegcdcommon_firstproduct) * (ge_second_rp_gcd_zero_casegcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_zero_casegcdcommon_firstproduct) * (ge_second_ip_gcd_zero_casegcdcommon_firstproduct))) + (((ge_first_in_gcd_zero_casegcdcommon_firstproduct) * (ge_second_in_gcd_zero_casegcdcommon_firstproduct))))))) + ge_balance_positive_gcd_zero_casegcdcommon_firstproductoutputreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdcommon_firstproductoutputimaginary ge_balance_negative_gcd_zero_casegcdcommon_firstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_firstproductoutputimaginary) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdcommon_firstproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdcommon_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_firstproductoutputimaginary) = S ge_signed_half_gcd_zero_casegcdcommon_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdcommon_firstproduct) * (ge_second_ip_gcd_zero_casegcdcommon_firstproduct))) + (((ge_first_rn_gcd_zero_casegcdcommon_firstproduct) * (ge_second_in_gcd_zero_casegcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_zero_casegcdcommon_firstproduct) * (ge_second_rp_gcd_zero_casegcdcommon_firstproduct))) + (((ge_first_in_gcd_zero_casegcdcommon_firstproduct) * (ge_second_rn_gcd_zero_casegcdcommon_firstproduct))))))) + ge_balance_negative_gcd_zero_casegcdcommon_firstproductoutputimaginary = (((((((ge_first_rp_gcd_zero_casegcdcommon_firstproduct) * (ge_second_in_gcd_zero_casegcdcommon_firstproduct))) + (((ge_first_rn_gcd_zero_casegcdcommon_firstproduct) * (ge_second_ip_gcd_zero_casegcdcommon_firstproduct))))) + (((((ge_first_ip_gcd_zero_casegcdcommon_firstproduct) * (ge_second_rn_gcd_zero_casegcdcommon_firstproduct))) + (((ge_first_in_gcd_zero_casegcdcommon_firstproduct) * (ge_second_rp_gcd_zero_casegcdcommon_firstproduct))))))) + ge_balance_positive_gcd_zero_casegcdcommon_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_zero_casegcdcommon_second. (exists ge_first_rp_gcd_zero_casegcdcommon_secondproduct ge_first_rn_gcd_zero_casegcdcommon_secondproduct ge_first_ip_gcd_zero_casegcdcommon_secondproduct ge_first_in_gcd_zero_casegcdcommon_secondproduct ge_second_rp_gcd_zero_casegcdcommon_secondproduct ge_second_rn_gcd_zero_casegcdcommon_secondproduct ge_second_ip_gcd_zero_casegcdcommon_secondproduct ge_second_in_gcd_zero_casegcdcommon_secondproduct. ((exists ge_representation_real_code_gcd_zero_casegcdcommon_secondproductfirst ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductfirst. (((gr_common_divisor_gcd_zero_casegcd) = ((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductfirst)) * S ((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductfirst)) + ((ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductfirst))) /\ ((exists ge_balance_positive_gcd_zero_casegcdcommon_secondproductfirstreal ge_balance_negative_gcd_zero_casegcdcommon_secondproductfirstreal. (((((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_secondproductfirstreal) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_secondproductfirstrealdecode. (((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdcommon_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_secondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductfirstreal) = S ge_signed_half_gcd_zero_casegcdcommon_secondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zero_casegcdcommon_secondproduct) + ge_balance_negative_gcd_zero_casegcdcommon_secondproductfirstreal = (ge_first_rn_gcd_zero_casegcdcommon_secondproduct) + ge_balance_positive_gcd_zero_casegcdcommon_secondproductfirstreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdcommon_secondproductfirstimaginary ge_balance_negative_gcd_zero_casegcdcommon_secondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_secondproductfirstimaginary) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdcommon_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductfirstimaginary) = S ge_signed_half_gcd_zero_casegcdcommon_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zero_casegcdcommon_secondproduct) + ge_balance_negative_gcd_zero_casegcdcommon_secondproductfirstimaginary = (ge_first_in_gcd_zero_casegcdcommon_secondproduct) + ge_balance_positive_gcd_zero_casegcdcommon_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zero_casegcdcommon_secondproductsecond ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductsecond. (((gr_quotient_gcd_zero_casegcdcommon_second) = ((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductsecond)) * S ((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductsecond)) + ((ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductsecond))) /\ ((exists ge_balance_positive_gcd_zero_casegcdcommon_secondproductsecondreal ge_balance_negative_gcd_zero_casegcdcommon_secondproductsecondreal. (((((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_secondproductsecondreal) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_secondproductsecondrealdecode. (((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdcommon_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_secondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductsecondreal) = S ge_signed_half_gcd_zero_casegcdcommon_secondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zero_casegcdcommon_secondproduct) + ge_balance_negative_gcd_zero_casegcdcommon_secondproductsecondreal = (ge_second_rn_gcd_zero_casegcdcommon_secondproduct) + ge_balance_positive_gcd_zero_casegcdcommon_secondproductsecondreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdcommon_secondproductsecondimaginary ge_balance_negative_gcd_zero_casegcdcommon_secondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_secondproductsecondimaginary) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdcommon_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductsecondimaginary) = S ge_signed_half_gcd_zero_casegcdcommon_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zero_casegcdcommon_secondproduct) + ge_balance_negative_gcd_zero_casegcdcommon_secondproductsecondimaginary = (ge_second_in_gcd_zero_casegcdcommon_secondproduct) + ge_balance_positive_gcd_zero_casegcdcommon_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zero_casegcdcommon_secondproductoutput ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductoutput. (((b) = ((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductoutput)) * S ((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductoutput)) + ((ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductoutput))) /\ ((exists ge_balance_positive_gcd_zero_casegcdcommon_secondproductoutputreal ge_balance_negative_gcd_zero_casegcdcommon_secondproductoutputreal. (((((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_secondproductoutputreal) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_secondproductoutputrealdecode. (((ge_representation_real_code_gcd_zero_casegcdcommon_secondproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdcommon_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_secondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductoutputreal) = S ge_signed_half_gcd_zero_casegcdcommon_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdcommon_secondproduct) * (ge_second_rp_gcd_zero_casegcdcommon_secondproduct))) + (((ge_first_rn_gcd_zero_casegcdcommon_secondproduct) * (ge_second_rn_gcd_zero_casegcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_zero_casegcdcommon_secondproduct) * (ge_second_in_gcd_zero_casegcdcommon_secondproduct))) + (((ge_first_in_gcd_zero_casegcdcommon_secondproduct) * (ge_second_ip_gcd_zero_casegcdcommon_secondproduct))))))) + ge_balance_negative_gcd_zero_casegcdcommon_secondproductoutputreal = (((((((ge_first_rp_gcd_zero_casegcdcommon_secondproduct) * (ge_second_rn_gcd_zero_casegcdcommon_secondproduct))) + (((ge_first_rn_gcd_zero_casegcdcommon_secondproduct) * (ge_second_rp_gcd_zero_casegcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_zero_casegcdcommon_secondproduct) * (ge_second_ip_gcd_zero_casegcdcommon_secondproduct))) + (((ge_first_in_gcd_zero_casegcdcommon_secondproduct) * (ge_second_in_gcd_zero_casegcdcommon_secondproduct))))))) + ge_balance_positive_gcd_zero_casegcdcommon_secondproductoutputreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdcommon_secondproductoutputimaginary ge_balance_negative_gcd_zero_casegcdcommon_secondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdcommon_secondproductoutputimaginary) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdcommon_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdcommon_secondproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdcommon_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdcommon_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdcommon_secondproductoutputimaginary) = S ge_signed_half_gcd_zero_casegcdcommon_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdcommon_secondproduct) * (ge_second_ip_gcd_zero_casegcdcommon_secondproduct))) + (((ge_first_rn_gcd_zero_casegcdcommon_secondproduct) * (ge_second_in_gcd_zero_casegcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_zero_casegcdcommon_secondproduct) * (ge_second_rp_gcd_zero_casegcdcommon_secondproduct))) + (((ge_first_in_gcd_zero_casegcdcommon_secondproduct) * (ge_second_rn_gcd_zero_casegcdcommon_secondproduct))))))) + ge_balance_negative_gcd_zero_casegcdcommon_secondproductoutputimaginary = (((((((ge_first_rp_gcd_zero_casegcdcommon_secondproduct) * (ge_second_in_gcd_zero_casegcdcommon_secondproduct))) + (((ge_first_rn_gcd_zero_casegcdcommon_secondproduct) * (ge_second_ip_gcd_zero_casegcdcommon_secondproduct))))) + (((((ge_first_ip_gcd_zero_casegcdcommon_secondproduct) * (ge_second_rn_gcd_zero_casegcdcommon_secondproduct))) + (((ge_first_in_gcd_zero_casegcdcommon_secondproduct) * (ge_second_rp_gcd_zero_casegcdcommon_secondproduct))))))) + ge_balance_positive_gcd_zero_casegcdcommon_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_zero_casegcdgreatest. (exists ge_first_rp_gcd_zero_casegcdgreatestproduct ge_first_rn_gcd_zero_casegcdgreatestproduct ge_first_ip_gcd_zero_casegcdgreatestproduct ge_first_in_gcd_zero_casegcdgreatestproduct ge_second_rp_gcd_zero_casegcdgreatestproduct ge_second_rn_gcd_zero_casegcdgreatestproduct ge_second_ip_gcd_zero_casegcdgreatestproduct ge_second_in_gcd_zero_casegcdgreatestproduct. ((exists ge_representation_real_code_gcd_zero_casegcdgreatestproductfirst ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductfirst. (((gr_common_divisor_gcd_zero_casegcd) = ((ge_representation_real_code_gcd_zero_casegcdgreatestproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductfirst)) * S ((ge_representation_real_code_gcd_zero_casegcdgreatestproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductfirst)) + ((ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductfirst) + (ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductfirst))) /\ ((exists ge_balance_positive_gcd_zero_casegcdgreatestproductfirstreal ge_balance_negative_gcd_zero_casegcdgreatestproductfirstreal. (((((ge_representation_real_code_gcd_zero_casegcdgreatestproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdgreatestproductfirstreal) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdgreatestproductfirstrealdecode. (((ge_representation_real_code_gcd_zero_casegcdgreatestproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdgreatestproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdgreatestproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductfirstreal) = S ge_signed_half_gcd_zero_casegcdgreatestproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zero_casegcdgreatestproduct) + ge_balance_negative_gcd_zero_casegcdgreatestproductfirstreal = (ge_first_rn_gcd_zero_casegcdgreatestproduct) + ge_balance_positive_gcd_zero_casegcdgreatestproductfirstreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdgreatestproductfirstimaginary ge_balance_negative_gcd_zero_casegcdgreatestproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductfirst) = 2 * (ge_balance_positive_gcd_zero_casegcdgreatestproductfirstimaginary) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdgreatestproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductfirst) = 2 * ge_signed_half_gcd_zero_casegcdgreatestproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdgreatestproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductfirstimaginary) = S ge_signed_half_gcd_zero_casegcdgreatestproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zero_casegcdgreatestproduct) + ge_balance_negative_gcd_zero_casegcdgreatestproductfirstimaginary = (ge_first_in_gcd_zero_casegcdgreatestproduct) + ge_balance_positive_gcd_zero_casegcdgreatestproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zero_casegcdgreatestproductsecond ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductsecond. (((gr_quotient_gcd_zero_casegcdgreatest) = ((ge_representation_real_code_gcd_zero_casegcdgreatestproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductsecond)) * S ((ge_representation_real_code_gcd_zero_casegcdgreatestproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductsecond)) + ((ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductsecond) + (ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductsecond))) /\ ((exists ge_balance_positive_gcd_zero_casegcdgreatestproductsecondreal ge_balance_negative_gcd_zero_casegcdgreatestproductsecondreal. (((((ge_representation_real_code_gcd_zero_casegcdgreatestproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdgreatestproductsecondreal) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdgreatestproductsecondrealdecode. (((ge_representation_real_code_gcd_zero_casegcdgreatestproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdgreatestproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdgreatestproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductsecondreal) = S ge_signed_half_gcd_zero_casegcdgreatestproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zero_casegcdgreatestproduct) + ge_balance_negative_gcd_zero_casegcdgreatestproductsecondreal = (ge_second_rn_gcd_zero_casegcdgreatestproduct) + ge_balance_positive_gcd_zero_casegcdgreatestproductsecondreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdgreatestproductsecondimaginary ge_balance_negative_gcd_zero_casegcdgreatestproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductsecond) = 2 * (ge_balance_positive_gcd_zero_casegcdgreatestproductsecondimaginary) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdgreatestproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductsecond) = 2 * ge_signed_half_gcd_zero_casegcdgreatestproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdgreatestproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductsecondimaginary) = S ge_signed_half_gcd_zero_casegcdgreatestproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zero_casegcdgreatestproduct) + ge_balance_negative_gcd_zero_casegcdgreatestproductsecondimaginary = (ge_second_in_gcd_zero_casegcdgreatestproduct) + ge_balance_positive_gcd_zero_casegcdgreatestproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zero_casegcdgreatestproductoutput ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductoutput. (((gr_gcd_gcd_zero_case) = ((ge_representation_real_code_gcd_zero_casegcdgreatestproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductoutput)) * S ((ge_representation_real_code_gcd_zero_casegcdgreatestproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductoutput)) + ((ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductoutput) + (ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductoutput))) /\ ((exists ge_balance_positive_gcd_zero_casegcdgreatestproductoutputreal ge_balance_negative_gcd_zero_casegcdgreatestproductoutputreal. (((((ge_representation_real_code_gcd_zero_casegcdgreatestproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdgreatestproductoutputreal) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zero_casegcdgreatestproductoutputrealdecode. (((ge_representation_real_code_gcd_zero_casegcdgreatestproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdgreatestproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdgreatestproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductoutputreal) = S ge_signed_half_gcd_zero_casegcdgreatestproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdgreatestproduct) * (ge_second_rp_gcd_zero_casegcdgreatestproduct))) + (((ge_first_rn_gcd_zero_casegcdgreatestproduct) * (ge_second_rn_gcd_zero_casegcdgreatestproduct))))) + (((((ge_first_ip_gcd_zero_casegcdgreatestproduct) * (ge_second_in_gcd_zero_casegcdgreatestproduct))) + (((ge_first_in_gcd_zero_casegcdgreatestproduct) * (ge_second_ip_gcd_zero_casegcdgreatestproduct))))))) + ge_balance_negative_gcd_zero_casegcdgreatestproductoutputreal = (((((((ge_first_rp_gcd_zero_casegcdgreatestproduct) * (ge_second_rn_gcd_zero_casegcdgreatestproduct))) + (((ge_first_rn_gcd_zero_casegcdgreatestproduct) * (ge_second_rp_gcd_zero_casegcdgreatestproduct))))) + (((((ge_first_ip_gcd_zero_casegcdgreatestproduct) * (ge_second_ip_gcd_zero_casegcdgreatestproduct))) + (((ge_first_in_gcd_zero_casegcdgreatestproduct) * (ge_second_in_gcd_zero_casegcdgreatestproduct))))))) + ge_balance_positive_gcd_zero_casegcdgreatestproductoutputreal))) /\ (exists ge_balance_positive_gcd_zero_casegcdgreatestproductoutputimaginary ge_balance_negative_gcd_zero_casegcdgreatestproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductoutput) = 2 * (ge_balance_positive_gcd_zero_casegcdgreatestproductoutputimaginary) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casegcdgreatestproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casegcdgreatestproductoutput) = 2 * ge_signed_half_gcd_zero_casegcdgreatestproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casegcdgreatestproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casegcdgreatestproductoutputimaginary) = S ge_signed_half_gcd_zero_casegcdgreatestproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zero_casegcdgreatestproduct) * (ge_second_ip_gcd_zero_casegcdgreatestproduct))) + (((ge_first_rn_gcd_zero_casegcdgreatestproduct) * (ge_second_in_gcd_zero_casegcdgreatestproduct))))) + (((((ge_first_ip_gcd_zero_casegcdgreatestproduct) * (ge_second_rp_gcd_zero_casegcdgreatestproduct))) + (((ge_first_in_gcd_zero_casegcdgreatestproduct) * (ge_second_rn_gcd_zero_casegcdgreatestproduct))))))) + ge_balance_negative_gcd_zero_casegcdgreatestproductoutputimaginary = (((((((ge_first_rp_gcd_zero_casegcdgreatestproduct) * (ge_second_in_gcd_zero_casegcdgreatestproduct))) + (((ge_first_rn_gcd_zero_casegcdgreatestproduct) * (ge_second_ip_gcd_zero_casegcdgreatestproduct))))) + (((((ge_first_ip_gcd_zero_casegcdgreatestproduct) * (ge_second_rn_gcd_zero_casegcdgreatestproduct))) + (((ge_first_in_gcd_zero_casegcdgreatestproduct) * (ge_second_rp_gcd_zero_casegcdgreatestproduct))))))) + ge_balance_positive_gcd_zero_casegcdgreatestproductoutputimaginary)))))))))))))) /\ (exists gr_first_product_gcd_zero_casebezout gr_second_product_gcd_zero_casebezout. ((exists ge_first_rp_gcd_zero_casebezoutfirst ge_first_rn_gcd_zero_casebezoutfirst ge_first_ip_gcd_zero_casebezoutfirst ge_first_in_gcd_zero_casebezoutfirst ge_second_rp_gcd_zero_casebezoutfirst ge_second_rn_gcd_zero_casebezoutfirst ge_second_ip_gcd_zero_casebezoutfirst ge_second_in_gcd_zero_casebezoutfirst. ((exists ge_representation_real_code_gcd_zero_casebezoutfirstfirst ge_representation_imaginary_code_gcd_zero_casebezoutfirstfirst. (((a) = ((ge_representation_real_code_gcd_zero_casebezoutfirstfirst) + (ge_representation_imaginary_code_gcd_zero_casebezoutfirstfirst)) * S ((ge_representation_real_code_gcd_zero_casebezoutfirstfirst) + (ge_representation_imaginary_code_gcd_zero_casebezoutfirstfirst)) + ((ge_representation_imaginary_code_gcd_zero_casebezoutfirstfirst) + (ge_representation_imaginary_code_gcd_zero_casebezoutfirstfirst))) /\ ((exists ge_balance_positive_gcd_zero_casebezoutfirstfirstreal ge_balance_negative_gcd_zero_casebezoutfirstfirstreal. (((((ge_representation_real_code_gcd_zero_casebezoutfirstfirst) = 2 * (ge_balance_positive_gcd_zero_casebezoutfirstfirstreal) /\ (ge_balance_negative_gcd_zero_casebezoutfirstfirstreal) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutfirstfirstrealdecode. (((ge_representation_real_code_gcd_zero_casebezoutfirstfirst) = 2 * ge_signed_half_gcd_zero_casebezoutfirstfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutfirstfirstreal) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutfirstfirstreal) = S ge_signed_half_gcd_zero_casebezoutfirstfirstrealdecode))) /\ ((ge_first_rp_gcd_zero_casebezoutfirst) + ge_balance_negative_gcd_zero_casebezoutfirstfirstreal = (ge_first_rn_gcd_zero_casebezoutfirst) + ge_balance_positive_gcd_zero_casebezoutfirstfirstreal))) /\ (exists ge_balance_positive_gcd_zero_casebezoutfirstfirstimaginary ge_balance_negative_gcd_zero_casebezoutfirstfirstimaginary. (((((ge_representation_imaginary_code_gcd_zero_casebezoutfirstfirst) = 2 * (ge_balance_positive_gcd_zero_casebezoutfirstfirstimaginary) /\ (ge_balance_negative_gcd_zero_casebezoutfirstfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutfirstfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casebezoutfirstfirst) = 2 * ge_signed_half_gcd_zero_casebezoutfirstfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutfirstfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutfirstfirstimaginary) = S ge_signed_half_gcd_zero_casebezoutfirstfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zero_casebezoutfirst) + ge_balance_negative_gcd_zero_casebezoutfirstfirstimaginary = (ge_first_in_gcd_zero_casebezoutfirst) + ge_balance_positive_gcd_zero_casebezoutfirstfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zero_casebezoutfirstsecond ge_representation_imaginary_code_gcd_zero_casebezoutfirstsecond. (((gr_first_coefficient_gcd_zero_case) = ((ge_representation_real_code_gcd_zero_casebezoutfirstsecond) + (ge_representation_imaginary_code_gcd_zero_casebezoutfirstsecond)) * S ((ge_representation_real_code_gcd_zero_casebezoutfirstsecond) + (ge_representation_imaginary_code_gcd_zero_casebezoutfirstsecond)) + ((ge_representation_imaginary_code_gcd_zero_casebezoutfirstsecond) + (ge_representation_imaginary_code_gcd_zero_casebezoutfirstsecond))) /\ ((exists ge_balance_positive_gcd_zero_casebezoutfirstsecondreal ge_balance_negative_gcd_zero_casebezoutfirstsecondreal. (((((ge_representation_real_code_gcd_zero_casebezoutfirstsecond) = 2 * (ge_balance_positive_gcd_zero_casebezoutfirstsecondreal) /\ (ge_balance_negative_gcd_zero_casebezoutfirstsecondreal) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutfirstsecondrealdecode. (((ge_representation_real_code_gcd_zero_casebezoutfirstsecond) = 2 * ge_signed_half_gcd_zero_casebezoutfirstsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutfirstsecondreal) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutfirstsecondreal) = S ge_signed_half_gcd_zero_casebezoutfirstsecondrealdecode))) /\ ((ge_second_rp_gcd_zero_casebezoutfirst) + ge_balance_negative_gcd_zero_casebezoutfirstsecondreal = (ge_second_rn_gcd_zero_casebezoutfirst) + ge_balance_positive_gcd_zero_casebezoutfirstsecondreal))) /\ (exists ge_balance_positive_gcd_zero_casebezoutfirstsecondimaginary ge_balance_negative_gcd_zero_casebezoutfirstsecondimaginary. (((((ge_representation_imaginary_code_gcd_zero_casebezoutfirstsecond) = 2 * (ge_balance_positive_gcd_zero_casebezoutfirstsecondimaginary) /\ (ge_balance_negative_gcd_zero_casebezoutfirstsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutfirstsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casebezoutfirstsecond) = 2 * ge_signed_half_gcd_zero_casebezoutfirstsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutfirstsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutfirstsecondimaginary) = S ge_signed_half_gcd_zero_casebezoutfirstsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zero_casebezoutfirst) + ge_balance_negative_gcd_zero_casebezoutfirstsecondimaginary = (ge_second_in_gcd_zero_casebezoutfirst) + ge_balance_positive_gcd_zero_casebezoutfirstsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zero_casebezoutfirstoutput ge_representation_imaginary_code_gcd_zero_casebezoutfirstoutput. (((gr_first_product_gcd_zero_casebezout) = ((ge_representation_real_code_gcd_zero_casebezoutfirstoutput) + (ge_representation_imaginary_code_gcd_zero_casebezoutfirstoutput)) * S ((ge_representation_real_code_gcd_zero_casebezoutfirstoutput) + (ge_representation_imaginary_code_gcd_zero_casebezoutfirstoutput)) + ((ge_representation_imaginary_code_gcd_zero_casebezoutfirstoutput) + (ge_representation_imaginary_code_gcd_zero_casebezoutfirstoutput))) /\ ((exists ge_balance_positive_gcd_zero_casebezoutfirstoutputreal ge_balance_negative_gcd_zero_casebezoutfirstoutputreal. (((((ge_representation_real_code_gcd_zero_casebezoutfirstoutput) = 2 * (ge_balance_positive_gcd_zero_casebezoutfirstoutputreal) /\ (ge_balance_negative_gcd_zero_casebezoutfirstoutputreal) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutfirstoutputrealdecode. (((ge_representation_real_code_gcd_zero_casebezoutfirstoutput) = 2 * ge_signed_half_gcd_zero_casebezoutfirstoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutfirstoutputreal) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutfirstoutputreal) = S ge_signed_half_gcd_zero_casebezoutfirstoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zero_casebezoutfirst) * (ge_second_rp_gcd_zero_casebezoutfirst))) + (((ge_first_rn_gcd_zero_casebezoutfirst) * (ge_second_rn_gcd_zero_casebezoutfirst))))) + (((((ge_first_ip_gcd_zero_casebezoutfirst) * (ge_second_in_gcd_zero_casebezoutfirst))) + (((ge_first_in_gcd_zero_casebezoutfirst) * (ge_second_ip_gcd_zero_casebezoutfirst))))))) + ge_balance_negative_gcd_zero_casebezoutfirstoutputreal = (((((((ge_first_rp_gcd_zero_casebezoutfirst) * (ge_second_rn_gcd_zero_casebezoutfirst))) + (((ge_first_rn_gcd_zero_casebezoutfirst) * (ge_second_rp_gcd_zero_casebezoutfirst))))) + (((((ge_first_ip_gcd_zero_casebezoutfirst) * (ge_second_ip_gcd_zero_casebezoutfirst))) + (((ge_first_in_gcd_zero_casebezoutfirst) * (ge_second_in_gcd_zero_casebezoutfirst))))))) + ge_balance_positive_gcd_zero_casebezoutfirstoutputreal))) /\ (exists ge_balance_positive_gcd_zero_casebezoutfirstoutputimaginary ge_balance_negative_gcd_zero_casebezoutfirstoutputimaginary. (((((ge_representation_imaginary_code_gcd_zero_casebezoutfirstoutput) = 2 * (ge_balance_positive_gcd_zero_casebezoutfirstoutputimaginary) /\ (ge_balance_negative_gcd_zero_casebezoutfirstoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutfirstoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casebezoutfirstoutput) = 2 * ge_signed_half_gcd_zero_casebezoutfirstoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutfirstoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutfirstoutputimaginary) = S ge_signed_half_gcd_zero_casebezoutfirstoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zero_casebezoutfirst) * (ge_second_ip_gcd_zero_casebezoutfirst))) + (((ge_first_rn_gcd_zero_casebezoutfirst) * (ge_second_in_gcd_zero_casebezoutfirst))))) + (((((ge_first_ip_gcd_zero_casebezoutfirst) * (ge_second_rp_gcd_zero_casebezoutfirst))) + (((ge_first_in_gcd_zero_casebezoutfirst) * (ge_second_rn_gcd_zero_casebezoutfirst))))))) + ge_balance_negative_gcd_zero_casebezoutfirstoutputimaginary = (((((((ge_first_rp_gcd_zero_casebezoutfirst) * (ge_second_in_gcd_zero_casebezoutfirst))) + (((ge_first_rn_gcd_zero_casebezoutfirst) * (ge_second_ip_gcd_zero_casebezoutfirst))))) + (((((ge_first_ip_gcd_zero_casebezoutfirst) * (ge_second_rn_gcd_zero_casebezoutfirst))) + (((ge_first_in_gcd_zero_casebezoutfirst) * (ge_second_rp_gcd_zero_casebezoutfirst))))))) + ge_balance_positive_gcd_zero_casebezoutfirstoutputimaginary))))))))) /\ ((exists ge_first_rp_gcd_zero_casebezoutsecond ge_first_rn_gcd_zero_casebezoutsecond ge_first_ip_gcd_zero_casebezoutsecond ge_first_in_gcd_zero_casebezoutsecond ge_second_rp_gcd_zero_casebezoutsecond ge_second_rn_gcd_zero_casebezoutsecond ge_second_ip_gcd_zero_casebezoutsecond ge_second_in_gcd_zero_casebezoutsecond. ((exists ge_representation_real_code_gcd_zero_casebezoutsecondfirst ge_representation_imaginary_code_gcd_zero_casebezoutsecondfirst. (((b) = ((ge_representation_real_code_gcd_zero_casebezoutsecondfirst) + (ge_representation_imaginary_code_gcd_zero_casebezoutsecondfirst)) * S ((ge_representation_real_code_gcd_zero_casebezoutsecondfirst) + (ge_representation_imaginary_code_gcd_zero_casebezoutsecondfirst)) + ((ge_representation_imaginary_code_gcd_zero_casebezoutsecondfirst) + (ge_representation_imaginary_code_gcd_zero_casebezoutsecondfirst))) /\ ((exists ge_balance_positive_gcd_zero_casebezoutsecondfirstreal ge_balance_negative_gcd_zero_casebezoutsecondfirstreal. (((((ge_representation_real_code_gcd_zero_casebezoutsecondfirst) = 2 * (ge_balance_positive_gcd_zero_casebezoutsecondfirstreal) /\ (ge_balance_negative_gcd_zero_casebezoutsecondfirstreal) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsecondfirstrealdecode. (((ge_representation_real_code_gcd_zero_casebezoutsecondfirst) = 2 * ge_signed_half_gcd_zero_casebezoutsecondfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsecondfirstreal) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsecondfirstreal) = S ge_signed_half_gcd_zero_casebezoutsecondfirstrealdecode))) /\ ((ge_first_rp_gcd_zero_casebezoutsecond) + ge_balance_negative_gcd_zero_casebezoutsecondfirstreal = (ge_first_rn_gcd_zero_casebezoutsecond) + ge_balance_positive_gcd_zero_casebezoutsecondfirstreal))) /\ (exists ge_balance_positive_gcd_zero_casebezoutsecondfirstimaginary ge_balance_negative_gcd_zero_casebezoutsecondfirstimaginary. (((((ge_representation_imaginary_code_gcd_zero_casebezoutsecondfirst) = 2 * (ge_balance_positive_gcd_zero_casebezoutsecondfirstimaginary) /\ (ge_balance_negative_gcd_zero_casebezoutsecondfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsecondfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casebezoutsecondfirst) = 2 * ge_signed_half_gcd_zero_casebezoutsecondfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsecondfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsecondfirstimaginary) = S ge_signed_half_gcd_zero_casebezoutsecondfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zero_casebezoutsecond) + ge_balance_negative_gcd_zero_casebezoutsecondfirstimaginary = (ge_first_in_gcd_zero_casebezoutsecond) + ge_balance_positive_gcd_zero_casebezoutsecondfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zero_casebezoutsecondsecond ge_representation_imaginary_code_gcd_zero_casebezoutsecondsecond. (((gr_second_coefficient_gcd_zero_case) = ((ge_representation_real_code_gcd_zero_casebezoutsecondsecond) + (ge_representation_imaginary_code_gcd_zero_casebezoutsecondsecond)) * S ((ge_representation_real_code_gcd_zero_casebezoutsecondsecond) + (ge_representation_imaginary_code_gcd_zero_casebezoutsecondsecond)) + ((ge_representation_imaginary_code_gcd_zero_casebezoutsecondsecond) + (ge_representation_imaginary_code_gcd_zero_casebezoutsecondsecond))) /\ ((exists ge_balance_positive_gcd_zero_casebezoutsecondsecondreal ge_balance_negative_gcd_zero_casebezoutsecondsecondreal. (((((ge_representation_real_code_gcd_zero_casebezoutsecondsecond) = 2 * (ge_balance_positive_gcd_zero_casebezoutsecondsecondreal) /\ (ge_balance_negative_gcd_zero_casebezoutsecondsecondreal) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsecondsecondrealdecode. (((ge_representation_real_code_gcd_zero_casebezoutsecondsecond) = 2 * ge_signed_half_gcd_zero_casebezoutsecondsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsecondsecondreal) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsecondsecondreal) = S ge_signed_half_gcd_zero_casebezoutsecondsecondrealdecode))) /\ ((ge_second_rp_gcd_zero_casebezoutsecond) + ge_balance_negative_gcd_zero_casebezoutsecondsecondreal = (ge_second_rn_gcd_zero_casebezoutsecond) + ge_balance_positive_gcd_zero_casebezoutsecondsecondreal))) /\ (exists ge_balance_positive_gcd_zero_casebezoutsecondsecondimaginary ge_balance_negative_gcd_zero_casebezoutsecondsecondimaginary. (((((ge_representation_imaginary_code_gcd_zero_casebezoutsecondsecond) = 2 * (ge_balance_positive_gcd_zero_casebezoutsecondsecondimaginary) /\ (ge_balance_negative_gcd_zero_casebezoutsecondsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsecondsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casebezoutsecondsecond) = 2 * ge_signed_half_gcd_zero_casebezoutsecondsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsecondsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsecondsecondimaginary) = S ge_signed_half_gcd_zero_casebezoutsecondsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zero_casebezoutsecond) + ge_balance_negative_gcd_zero_casebezoutsecondsecondimaginary = (ge_second_in_gcd_zero_casebezoutsecond) + ge_balance_positive_gcd_zero_casebezoutsecondsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zero_casebezoutsecondoutput ge_representation_imaginary_code_gcd_zero_casebezoutsecondoutput. (((gr_second_product_gcd_zero_casebezout) = ((ge_representation_real_code_gcd_zero_casebezoutsecondoutput) + (ge_representation_imaginary_code_gcd_zero_casebezoutsecondoutput)) * S ((ge_representation_real_code_gcd_zero_casebezoutsecondoutput) + (ge_representation_imaginary_code_gcd_zero_casebezoutsecondoutput)) + ((ge_representation_imaginary_code_gcd_zero_casebezoutsecondoutput) + (ge_representation_imaginary_code_gcd_zero_casebezoutsecondoutput))) /\ ((exists ge_balance_positive_gcd_zero_casebezoutsecondoutputreal ge_balance_negative_gcd_zero_casebezoutsecondoutputreal. (((((ge_representation_real_code_gcd_zero_casebezoutsecondoutput) = 2 * (ge_balance_positive_gcd_zero_casebezoutsecondoutputreal) /\ (ge_balance_negative_gcd_zero_casebezoutsecondoutputreal) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsecondoutputrealdecode. (((ge_representation_real_code_gcd_zero_casebezoutsecondoutput) = 2 * ge_signed_half_gcd_zero_casebezoutsecondoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsecondoutputreal) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsecondoutputreal) = S ge_signed_half_gcd_zero_casebezoutsecondoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zero_casebezoutsecond) * (ge_second_rp_gcd_zero_casebezoutsecond))) + (((ge_first_rn_gcd_zero_casebezoutsecond) * (ge_second_rn_gcd_zero_casebezoutsecond))))) + (((((ge_first_ip_gcd_zero_casebezoutsecond) * (ge_second_in_gcd_zero_casebezoutsecond))) + (((ge_first_in_gcd_zero_casebezoutsecond) * (ge_second_ip_gcd_zero_casebezoutsecond))))))) + ge_balance_negative_gcd_zero_casebezoutsecondoutputreal = (((((((ge_first_rp_gcd_zero_casebezoutsecond) * (ge_second_rn_gcd_zero_casebezoutsecond))) + (((ge_first_rn_gcd_zero_casebezoutsecond) * (ge_second_rp_gcd_zero_casebezoutsecond))))) + (((((ge_first_ip_gcd_zero_casebezoutsecond) * (ge_second_ip_gcd_zero_casebezoutsecond))) + (((ge_first_in_gcd_zero_casebezoutsecond) * (ge_second_in_gcd_zero_casebezoutsecond))))))) + ge_balance_positive_gcd_zero_casebezoutsecondoutputreal))) /\ (exists ge_balance_positive_gcd_zero_casebezoutsecondoutputimaginary ge_balance_negative_gcd_zero_casebezoutsecondoutputimaginary. (((((ge_representation_imaginary_code_gcd_zero_casebezoutsecondoutput) = 2 * (ge_balance_positive_gcd_zero_casebezoutsecondoutputimaginary) /\ (ge_balance_negative_gcd_zero_casebezoutsecondoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsecondoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casebezoutsecondoutput) = 2 * ge_signed_half_gcd_zero_casebezoutsecondoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsecondoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsecondoutputimaginary) = S ge_signed_half_gcd_zero_casebezoutsecondoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zero_casebezoutsecond) * (ge_second_ip_gcd_zero_casebezoutsecond))) + (((ge_first_rn_gcd_zero_casebezoutsecond) * (ge_second_in_gcd_zero_casebezoutsecond))))) + (((((ge_first_ip_gcd_zero_casebezoutsecond) * (ge_second_rp_gcd_zero_casebezoutsecond))) + (((ge_first_in_gcd_zero_casebezoutsecond) * (ge_second_rn_gcd_zero_casebezoutsecond))))))) + ge_balance_negative_gcd_zero_casebezoutsecondoutputimaginary = (((((((ge_first_rp_gcd_zero_casebezoutsecond) * (ge_second_in_gcd_zero_casebezoutsecond))) + (((ge_first_rn_gcd_zero_casebezoutsecond) * (ge_second_ip_gcd_zero_casebezoutsecond))))) + (((((ge_first_ip_gcd_zero_casebezoutsecond) * (ge_second_rn_gcd_zero_casebezoutsecond))) + (((ge_first_in_gcd_zero_casebezoutsecond) * (ge_second_rp_gcd_zero_casebezoutsecond))))))) + ge_balance_positive_gcd_zero_casebezoutsecondoutputimaginary))))))))) /\ (exists ge_first_rp_gcd_zero_casebezoutsum ge_first_rn_gcd_zero_casebezoutsum ge_first_ip_gcd_zero_casebezoutsum ge_first_in_gcd_zero_casebezoutsum ge_second_rp_gcd_zero_casebezoutsum ge_second_rn_gcd_zero_casebezoutsum ge_second_ip_gcd_zero_casebezoutsum ge_second_in_gcd_zero_casebezoutsum. ((exists ge_representation_real_code_gcd_zero_casebezoutsumfirst ge_representation_imaginary_code_gcd_zero_casebezoutsumfirst. (((gr_first_product_gcd_zero_casebezout) = ((ge_representation_real_code_gcd_zero_casebezoutsumfirst) + (ge_representation_imaginary_code_gcd_zero_casebezoutsumfirst)) * S ((ge_representation_real_code_gcd_zero_casebezoutsumfirst) + (ge_representation_imaginary_code_gcd_zero_casebezoutsumfirst)) + ((ge_representation_imaginary_code_gcd_zero_casebezoutsumfirst) + (ge_representation_imaginary_code_gcd_zero_casebezoutsumfirst))) /\ ((exists ge_balance_positive_gcd_zero_casebezoutsumfirstreal ge_balance_negative_gcd_zero_casebezoutsumfirstreal. (((((ge_representation_real_code_gcd_zero_casebezoutsumfirst) = 2 * (ge_balance_positive_gcd_zero_casebezoutsumfirstreal) /\ (ge_balance_negative_gcd_zero_casebezoutsumfirstreal) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsumfirstrealdecode. (((ge_representation_real_code_gcd_zero_casebezoutsumfirst) = 2 * ge_signed_half_gcd_zero_casebezoutsumfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsumfirstreal) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsumfirstreal) = S ge_signed_half_gcd_zero_casebezoutsumfirstrealdecode))) /\ ((ge_first_rp_gcd_zero_casebezoutsum) + ge_balance_negative_gcd_zero_casebezoutsumfirstreal = (ge_first_rn_gcd_zero_casebezoutsum) + ge_balance_positive_gcd_zero_casebezoutsumfirstreal))) /\ (exists ge_balance_positive_gcd_zero_casebezoutsumfirstimaginary ge_balance_negative_gcd_zero_casebezoutsumfirstimaginary. (((((ge_representation_imaginary_code_gcd_zero_casebezoutsumfirst) = 2 * (ge_balance_positive_gcd_zero_casebezoutsumfirstimaginary) /\ (ge_balance_negative_gcd_zero_casebezoutsumfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsumfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casebezoutsumfirst) = 2 * ge_signed_half_gcd_zero_casebezoutsumfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsumfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsumfirstimaginary) = S ge_signed_half_gcd_zero_casebezoutsumfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zero_casebezoutsum) + ge_balance_negative_gcd_zero_casebezoutsumfirstimaginary = (ge_first_in_gcd_zero_casebezoutsum) + ge_balance_positive_gcd_zero_casebezoutsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zero_casebezoutsumsecond ge_representation_imaginary_code_gcd_zero_casebezoutsumsecond. (((gr_second_product_gcd_zero_casebezout) = ((ge_representation_real_code_gcd_zero_casebezoutsumsecond) + (ge_representation_imaginary_code_gcd_zero_casebezoutsumsecond)) * S ((ge_representation_real_code_gcd_zero_casebezoutsumsecond) + (ge_representation_imaginary_code_gcd_zero_casebezoutsumsecond)) + ((ge_representation_imaginary_code_gcd_zero_casebezoutsumsecond) + (ge_representation_imaginary_code_gcd_zero_casebezoutsumsecond))) /\ ((exists ge_balance_positive_gcd_zero_casebezoutsumsecondreal ge_balance_negative_gcd_zero_casebezoutsumsecondreal. (((((ge_representation_real_code_gcd_zero_casebezoutsumsecond) = 2 * (ge_balance_positive_gcd_zero_casebezoutsumsecondreal) /\ (ge_balance_negative_gcd_zero_casebezoutsumsecondreal) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsumsecondrealdecode. (((ge_representation_real_code_gcd_zero_casebezoutsumsecond) = 2 * ge_signed_half_gcd_zero_casebezoutsumsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsumsecondreal) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsumsecondreal) = S ge_signed_half_gcd_zero_casebezoutsumsecondrealdecode))) /\ ((ge_second_rp_gcd_zero_casebezoutsum) + ge_balance_negative_gcd_zero_casebezoutsumsecondreal = (ge_second_rn_gcd_zero_casebezoutsum) + ge_balance_positive_gcd_zero_casebezoutsumsecondreal))) /\ (exists ge_balance_positive_gcd_zero_casebezoutsumsecondimaginary ge_balance_negative_gcd_zero_casebezoutsumsecondimaginary. (((((ge_representation_imaginary_code_gcd_zero_casebezoutsumsecond) = 2 * (ge_balance_positive_gcd_zero_casebezoutsumsecondimaginary) /\ (ge_balance_negative_gcd_zero_casebezoutsumsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsumsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casebezoutsumsecond) = 2 * ge_signed_half_gcd_zero_casebezoutsumsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsumsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsumsecondimaginary) = S ge_signed_half_gcd_zero_casebezoutsumsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zero_casebezoutsum) + ge_balance_negative_gcd_zero_casebezoutsumsecondimaginary = (ge_second_in_gcd_zero_casebezoutsum) + ge_balance_positive_gcd_zero_casebezoutsumsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zero_casebezoutsumoutput ge_representation_imaginary_code_gcd_zero_casebezoutsumoutput. (((gr_gcd_gcd_zero_case) = ((ge_representation_real_code_gcd_zero_casebezoutsumoutput) + (ge_representation_imaginary_code_gcd_zero_casebezoutsumoutput)) * S ((ge_representation_real_code_gcd_zero_casebezoutsumoutput) + (ge_representation_imaginary_code_gcd_zero_casebezoutsumoutput)) + ((ge_representation_imaginary_code_gcd_zero_casebezoutsumoutput) + (ge_representation_imaginary_code_gcd_zero_casebezoutsumoutput))) /\ ((exists ge_balance_positive_gcd_zero_casebezoutsumoutputreal ge_balance_negative_gcd_zero_casebezoutsumoutputreal. (((((ge_representation_real_code_gcd_zero_casebezoutsumoutput) = 2 * (ge_balance_positive_gcd_zero_casebezoutsumoutputreal) /\ (ge_balance_negative_gcd_zero_casebezoutsumoutputreal) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsumoutputrealdecode. (((ge_representation_real_code_gcd_zero_casebezoutsumoutput) = 2 * ge_signed_half_gcd_zero_casebezoutsumoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsumoutputreal) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsumoutputreal) = S ge_signed_half_gcd_zero_casebezoutsumoutputrealdecode))) /\ ((((ge_first_rp_gcd_zero_casebezoutsum) + (ge_second_rp_gcd_zero_casebezoutsum))) + ge_balance_negative_gcd_zero_casebezoutsumoutputreal = (((ge_first_rn_gcd_zero_casebezoutsum) + (ge_second_rn_gcd_zero_casebezoutsum))) + ge_balance_positive_gcd_zero_casebezoutsumoutputreal))) /\ (exists ge_balance_positive_gcd_zero_casebezoutsumoutputimaginary ge_balance_negative_gcd_zero_casebezoutsumoutputimaginary. (((((ge_representation_imaginary_code_gcd_zero_casebezoutsumoutput) = 2 * (ge_balance_positive_gcd_zero_casebezoutsumoutputimaginary) /\ (ge_balance_negative_gcd_zero_casebezoutsumoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zero_casebezoutsumoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zero_casebezoutsumoutput) = 2 * ge_signed_half_gcd_zero_casebezoutsumoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zero_casebezoutsumoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zero_casebezoutsumoutputimaginary) = S ge_signed_half_gcd_zero_casebezoutsumoutputimaginarydecode))) /\ ((((ge_first_ip_gcd_zero_casebezoutsum) + (ge_second_ip_gcd_zero_casebezoutsum))) + ge_balance_negative_gcd_zero_casebezoutsumoutputimaginary = (((ge_first_in_gcd_zero_casebezoutsum) + (ge_second_in_gcd_zero_casebezoutsum))) + ge_balance_positive_gcd_zero_casebezoutsumoutputimaginary))))))))))))))