gaussian_gcd_bezout_zero_right

forall a. (exists ge_real_positive_gcd_zero_domain ge_real_negative_gcd_zero_domain ge_imaginary_positive_gcd_zero_domain ge_imaginary_negative_gcd_zero_domain. (exists ge_real_code_gcd_zero_domaindecode ge_imaginary_code_gcd_zero_domaindecode. (((a) = ((ge_real_code_gcd_zero_domaindecode) + (ge_imaginary_code_gcd_zero_domaindecode)) * S ((ge_real_code_gcd_zero_domaindecode) + (ge_imaginary_code_gcd_zero_domaindecode)) + ((ge_imaginary_code_gcd_zero_domaindecode) + (ge_imaginary_code_gcd_zero_domaindecode))) /\ (((((ge_real_code_gcd_zero_domaindecode) = 2 * (ge_real_positive_gcd_zero_domain) /\ (ge_real_negative_gcd_zero_domain) = 0) \/ exists ge_signed_half_ge_gcd_zero_domaindecode_real. (((ge_real_code_gcd_zero_domaindecode) = 2 * ge_signed_half_ge_gcd_zero_domaindecode_real + 1 /\ (ge_real_positive_gcd_zero_domain) = 0) /\ (ge_real_negative_gcd_zero_domain) = S ge_signed_half_ge_gcd_zero_domaindecode_real))) /\ ((((ge_imaginary_code_gcd_zero_domaindecode) = 2 * (ge_imaginary_positive_gcd_zero_domain) /\ (ge_imaginary_negative_gcd_zero_domain) = 0) \/ exists ge_signed_half_ge_gcd_zero_domaindecode_imaginary. (((ge_imaginary_code_gcd_zero_domaindecode) = 2 * ge_signed_half_ge_gcd_zero_domaindecode_imaginary + 1 /\ (ge_imaginary_positive_gcd_zero_domain) = 0) /\ (ge_imaginary_negative_gcd_zero_domain) = S ge_signed_half_ge_gcd_zero_domaindecode_imaginary))))))) -> ((((exists gr_quotient_gcd_zerofirst. (exists ge_first_rp_gcd_zerofirstproduct ge_first_rn_gcd_zerofirstproduct ge_first_ip_gcd_zerofirstproduct ge_first_in_gcd_zerofirstproduct ge_second_rp_gcd_zerofirstproduct ge_second_rn_gcd_zerofirstproduct ge_second_ip_gcd_zerofirstproduct ge_second_in_gcd_zerofirstproduct. ((exists ge_representation_real_code_gcd_zerofirstproductfirst ge_representation_imaginary_code_gcd_zerofirstproductfirst. (((a) = ((ge_representation_real_code_gcd_zerofirstproductfirst) + (ge_representation_imaginary_code_gcd_zerofirstproductfirst)) * S ((ge_representation_real_code_gcd_zerofirstproductfirst) + (ge_representation_imaginary_code_gcd_zerofirstproductfirst)) + ((ge_representation_imaginary_code_gcd_zerofirstproductfirst) + (ge_representation_imaginary_code_gcd_zerofirstproductfirst))) /\ ((exists ge_balance_positive_gcd_zerofirstproductfirstreal ge_balance_negative_gcd_zerofirstproductfirstreal. (((((ge_representation_real_code_gcd_zerofirstproductfirst) = 2 * (ge_balance_positive_gcd_zerofirstproductfirstreal) /\ (ge_balance_negative_gcd_zerofirstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zerofirstproductfirstrealdecode. (((ge_representation_real_code_gcd_zerofirstproductfirst) = 2 * ge_signed_half_gcd_zerofirstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zerofirstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zerofirstproductfirstreal) = S ge_signed_half_gcd_zerofirstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zerofirstproduct) + ge_balance_negative_gcd_zerofirstproductfirstreal = (ge_first_rn_gcd_zerofirstproduct) + ge_balance_positive_gcd_zerofirstproductfirstreal))) /\ (exists ge_balance_positive_gcd_zerofirstproductfirstimaginary ge_balance_negative_gcd_zerofirstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zerofirstproductfirst) = 2 * (ge_balance_positive_gcd_zerofirstproductfirstimaginary) /\ (ge_balance_negative_gcd_zerofirstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zerofirstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zerofirstproductfirst) = 2 * ge_signed_half_gcd_zerofirstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerofirstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zerofirstproductfirstimaginary) = S ge_signed_half_gcd_zerofirstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zerofirstproduct) + ge_balance_negative_gcd_zerofirstproductfirstimaginary = (ge_first_in_gcd_zerofirstproduct) + ge_balance_positive_gcd_zerofirstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zerofirstproductsecond ge_representation_imaginary_code_gcd_zerofirstproductsecond. (((gr_quotient_gcd_zerofirst) = ((ge_representation_real_code_gcd_zerofirstproductsecond) + (ge_representation_imaginary_code_gcd_zerofirstproductsecond)) * S ((ge_representation_real_code_gcd_zerofirstproductsecond) + (ge_representation_imaginary_code_gcd_zerofirstproductsecond)) + ((ge_representation_imaginary_code_gcd_zerofirstproductsecond) + (ge_representation_imaginary_code_gcd_zerofirstproductsecond))) /\ ((exists ge_balance_positive_gcd_zerofirstproductsecondreal ge_balance_negative_gcd_zerofirstproductsecondreal. (((((ge_representation_real_code_gcd_zerofirstproductsecond) = 2 * (ge_balance_positive_gcd_zerofirstproductsecondreal) /\ (ge_balance_negative_gcd_zerofirstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zerofirstproductsecondrealdecode. (((ge_representation_real_code_gcd_zerofirstproductsecond) = 2 * ge_signed_half_gcd_zerofirstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zerofirstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zerofirstproductsecondreal) = S ge_signed_half_gcd_zerofirstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zerofirstproduct) + ge_balance_negative_gcd_zerofirstproductsecondreal = (ge_second_rn_gcd_zerofirstproduct) + ge_balance_positive_gcd_zerofirstproductsecondreal))) /\ (exists ge_balance_positive_gcd_zerofirstproductsecondimaginary ge_balance_negative_gcd_zerofirstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zerofirstproductsecond) = 2 * (ge_balance_positive_gcd_zerofirstproductsecondimaginary) /\ (ge_balance_negative_gcd_zerofirstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zerofirstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zerofirstproductsecond) = 2 * ge_signed_half_gcd_zerofirstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerofirstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zerofirstproductsecondimaginary) = S ge_signed_half_gcd_zerofirstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zerofirstproduct) + ge_balance_negative_gcd_zerofirstproductsecondimaginary = (ge_second_in_gcd_zerofirstproduct) + ge_balance_positive_gcd_zerofirstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zerofirstproductoutput ge_representation_imaginary_code_gcd_zerofirstproductoutput. (((a) = ((ge_representation_real_code_gcd_zerofirstproductoutput) + (ge_representation_imaginary_code_gcd_zerofirstproductoutput)) * S ((ge_representation_real_code_gcd_zerofirstproductoutput) + (ge_representation_imaginary_code_gcd_zerofirstproductoutput)) + ((ge_representation_imaginary_code_gcd_zerofirstproductoutput) + (ge_representation_imaginary_code_gcd_zerofirstproductoutput))) /\ ((exists ge_balance_positive_gcd_zerofirstproductoutputreal ge_balance_negative_gcd_zerofirstproductoutputreal. (((((ge_representation_real_code_gcd_zerofirstproductoutput) = 2 * (ge_balance_positive_gcd_zerofirstproductoutputreal) /\ (ge_balance_negative_gcd_zerofirstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zerofirstproductoutputrealdecode. (((ge_representation_real_code_gcd_zerofirstproductoutput) = 2 * ge_signed_half_gcd_zerofirstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zerofirstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zerofirstproductoutputreal) = S ge_signed_half_gcd_zerofirstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zerofirstproduct) * (ge_second_rp_gcd_zerofirstproduct))) + (((ge_first_rn_gcd_zerofirstproduct) * (ge_second_rn_gcd_zerofirstproduct))))) + (((((ge_first_ip_gcd_zerofirstproduct) * (ge_second_in_gcd_zerofirstproduct))) + (((ge_first_in_gcd_zerofirstproduct) * (ge_second_ip_gcd_zerofirstproduct))))))) + ge_balance_negative_gcd_zerofirstproductoutputreal = (((((((ge_first_rp_gcd_zerofirstproduct) * (ge_second_rn_gcd_zerofirstproduct))) + (((ge_first_rn_gcd_zerofirstproduct) * (ge_second_rp_gcd_zerofirstproduct))))) + (((((ge_first_ip_gcd_zerofirstproduct) * (ge_second_ip_gcd_zerofirstproduct))) + (((ge_first_in_gcd_zerofirstproduct) * (ge_second_in_gcd_zerofirstproduct))))))) + ge_balance_positive_gcd_zerofirstproductoutputreal))) /\ (exists ge_balance_positive_gcd_zerofirstproductoutputimaginary ge_balance_negative_gcd_zerofirstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zerofirstproductoutput) = 2 * (ge_balance_positive_gcd_zerofirstproductoutputimaginary) /\ (ge_balance_negative_gcd_zerofirstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zerofirstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zerofirstproductoutput) = 2 * ge_signed_half_gcd_zerofirstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerofirstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zerofirstproductoutputimaginary) = S ge_signed_half_gcd_zerofirstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zerofirstproduct) * (ge_second_ip_gcd_zerofirstproduct))) + (((ge_first_rn_gcd_zerofirstproduct) * (ge_second_in_gcd_zerofirstproduct))))) + (((((ge_first_ip_gcd_zerofirstproduct) * (ge_second_rp_gcd_zerofirstproduct))) + (((ge_first_in_gcd_zerofirstproduct) * (ge_second_rn_gcd_zerofirstproduct))))))) + ge_balance_negative_gcd_zerofirstproductoutputimaginary = (((((((ge_first_rp_gcd_zerofirstproduct) * (ge_second_in_gcd_zerofirstproduct))) + (((ge_first_rn_gcd_zerofirstproduct) * (ge_second_ip_gcd_zerofirstproduct))))) + (((((ge_first_ip_gcd_zerofirstproduct) * (ge_second_rn_gcd_zerofirstproduct))) + (((ge_first_in_gcd_zerofirstproduct) * (ge_second_rp_gcd_zerofirstproduct))))))) + ge_balance_positive_gcd_zerofirstproductoutputimaginary)))))))))) /\ ((exists gr_quotient_gcd_zerosecond. (exists ge_first_rp_gcd_zerosecondproduct ge_first_rn_gcd_zerosecondproduct ge_first_ip_gcd_zerosecondproduct ge_first_in_gcd_zerosecondproduct ge_second_rp_gcd_zerosecondproduct ge_second_rn_gcd_zerosecondproduct ge_second_ip_gcd_zerosecondproduct ge_second_in_gcd_zerosecondproduct. ((exists ge_representation_real_code_gcd_zerosecondproductfirst ge_representation_imaginary_code_gcd_zerosecondproductfirst. (((a) = ((ge_representation_real_code_gcd_zerosecondproductfirst) + (ge_representation_imaginary_code_gcd_zerosecondproductfirst)) * S ((ge_representation_real_code_gcd_zerosecondproductfirst) + (ge_representation_imaginary_code_gcd_zerosecondproductfirst)) + ((ge_representation_imaginary_code_gcd_zerosecondproductfirst) + (ge_representation_imaginary_code_gcd_zerosecondproductfirst))) /\ ((exists ge_balance_positive_gcd_zerosecondproductfirstreal ge_balance_negative_gcd_zerosecondproductfirstreal. (((((ge_representation_real_code_gcd_zerosecondproductfirst) = 2 * (ge_balance_positive_gcd_zerosecondproductfirstreal) /\ (ge_balance_negative_gcd_zerosecondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zerosecondproductfirstrealdecode. (((ge_representation_real_code_gcd_zerosecondproductfirst) = 2 * ge_signed_half_gcd_zerosecondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zerosecondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zerosecondproductfirstreal) = S ge_signed_half_gcd_zerosecondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zerosecondproduct) + ge_balance_negative_gcd_zerosecondproductfirstreal = (ge_first_rn_gcd_zerosecondproduct) + ge_balance_positive_gcd_zerosecondproductfirstreal))) /\ (exists ge_balance_positive_gcd_zerosecondproductfirstimaginary ge_balance_negative_gcd_zerosecondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zerosecondproductfirst) = 2 * (ge_balance_positive_gcd_zerosecondproductfirstimaginary) /\ (ge_balance_negative_gcd_zerosecondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zerosecondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zerosecondproductfirst) = 2 * ge_signed_half_gcd_zerosecondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerosecondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zerosecondproductfirstimaginary) = S ge_signed_half_gcd_zerosecondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zerosecondproduct) + ge_balance_negative_gcd_zerosecondproductfirstimaginary = (ge_first_in_gcd_zerosecondproduct) + ge_balance_positive_gcd_zerosecondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zerosecondproductsecond ge_representation_imaginary_code_gcd_zerosecondproductsecond. (((gr_quotient_gcd_zerosecond) = ((ge_representation_real_code_gcd_zerosecondproductsecond) + (ge_representation_imaginary_code_gcd_zerosecondproductsecond)) * S ((ge_representation_real_code_gcd_zerosecondproductsecond) + (ge_representation_imaginary_code_gcd_zerosecondproductsecond)) + ((ge_representation_imaginary_code_gcd_zerosecondproductsecond) + (ge_representation_imaginary_code_gcd_zerosecondproductsecond))) /\ ((exists ge_balance_positive_gcd_zerosecondproductsecondreal ge_balance_negative_gcd_zerosecondproductsecondreal. (((((ge_representation_real_code_gcd_zerosecondproductsecond) = 2 * (ge_balance_positive_gcd_zerosecondproductsecondreal) /\ (ge_balance_negative_gcd_zerosecondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zerosecondproductsecondrealdecode. (((ge_representation_real_code_gcd_zerosecondproductsecond) = 2 * ge_signed_half_gcd_zerosecondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zerosecondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zerosecondproductsecondreal) = S ge_signed_half_gcd_zerosecondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zerosecondproduct) + ge_balance_negative_gcd_zerosecondproductsecondreal = (ge_second_rn_gcd_zerosecondproduct) + ge_balance_positive_gcd_zerosecondproductsecondreal))) /\ (exists ge_balance_positive_gcd_zerosecondproductsecondimaginary ge_balance_negative_gcd_zerosecondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zerosecondproductsecond) = 2 * (ge_balance_positive_gcd_zerosecondproductsecondimaginary) /\ (ge_balance_negative_gcd_zerosecondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zerosecondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zerosecondproductsecond) = 2 * ge_signed_half_gcd_zerosecondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerosecondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zerosecondproductsecondimaginary) = S ge_signed_half_gcd_zerosecondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zerosecondproduct) + ge_balance_negative_gcd_zerosecondproductsecondimaginary = (ge_second_in_gcd_zerosecondproduct) + ge_balance_positive_gcd_zerosecondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zerosecondproductoutput ge_representation_imaginary_code_gcd_zerosecondproductoutput. (((0) = ((ge_representation_real_code_gcd_zerosecondproductoutput) + (ge_representation_imaginary_code_gcd_zerosecondproductoutput)) * S ((ge_representation_real_code_gcd_zerosecondproductoutput) + (ge_representation_imaginary_code_gcd_zerosecondproductoutput)) + ((ge_representation_imaginary_code_gcd_zerosecondproductoutput) + (ge_representation_imaginary_code_gcd_zerosecondproductoutput))) /\ ((exists ge_balance_positive_gcd_zerosecondproductoutputreal ge_balance_negative_gcd_zerosecondproductoutputreal. (((((ge_representation_real_code_gcd_zerosecondproductoutput) = 2 * (ge_balance_positive_gcd_zerosecondproductoutputreal) /\ (ge_balance_negative_gcd_zerosecondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zerosecondproductoutputrealdecode. (((ge_representation_real_code_gcd_zerosecondproductoutput) = 2 * ge_signed_half_gcd_zerosecondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zerosecondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zerosecondproductoutputreal) = S ge_signed_half_gcd_zerosecondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zerosecondproduct) * (ge_second_rp_gcd_zerosecondproduct))) + (((ge_first_rn_gcd_zerosecondproduct) * (ge_second_rn_gcd_zerosecondproduct))))) + (((((ge_first_ip_gcd_zerosecondproduct) * (ge_second_in_gcd_zerosecondproduct))) + (((ge_first_in_gcd_zerosecondproduct) * (ge_second_ip_gcd_zerosecondproduct))))))) + ge_balance_negative_gcd_zerosecondproductoutputreal = (((((((ge_first_rp_gcd_zerosecondproduct) * (ge_second_rn_gcd_zerosecondproduct))) + (((ge_first_rn_gcd_zerosecondproduct) * (ge_second_rp_gcd_zerosecondproduct))))) + (((((ge_first_ip_gcd_zerosecondproduct) * (ge_second_ip_gcd_zerosecondproduct))) + (((ge_first_in_gcd_zerosecondproduct) * (ge_second_in_gcd_zerosecondproduct))))))) + ge_balance_positive_gcd_zerosecondproductoutputreal))) /\ (exists ge_balance_positive_gcd_zerosecondproductoutputimaginary ge_balance_negative_gcd_zerosecondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zerosecondproductoutput) = 2 * (ge_balance_positive_gcd_zerosecondproductoutputimaginary) /\ (ge_balance_negative_gcd_zerosecondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zerosecondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zerosecondproductoutput) = 2 * ge_signed_half_gcd_zerosecondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerosecondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zerosecondproductoutputimaginary) = S ge_signed_half_gcd_zerosecondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zerosecondproduct) * (ge_second_ip_gcd_zerosecondproduct))) + (((ge_first_rn_gcd_zerosecondproduct) * (ge_second_in_gcd_zerosecondproduct))))) + (((((ge_first_ip_gcd_zerosecondproduct) * (ge_second_rp_gcd_zerosecondproduct))) + (((ge_first_in_gcd_zerosecondproduct) * (ge_second_rn_gcd_zerosecondproduct))))))) + ge_balance_negative_gcd_zerosecondproductoutputimaginary = (((((((ge_first_rp_gcd_zerosecondproduct) * (ge_second_in_gcd_zerosecondproduct))) + (((ge_first_rn_gcd_zerosecondproduct) * (ge_second_ip_gcd_zerosecondproduct))))) + (((((ge_first_ip_gcd_zerosecondproduct) * (ge_second_rn_gcd_zerosecondproduct))) + (((ge_first_in_gcd_zerosecondproduct) * (ge_second_rp_gcd_zerosecondproduct))))))) + ge_balance_positive_gcd_zerosecondproductoutputimaginary)))))))))) /\ (forall gr_common_divisor_gcd_zero. (exists gr_quotient_gcd_zerocommon_first. (exists ge_first_rp_gcd_zerocommon_firstproduct ge_first_rn_gcd_zerocommon_firstproduct ge_first_ip_gcd_zerocommon_firstproduct ge_first_in_gcd_zerocommon_firstproduct ge_second_rp_gcd_zerocommon_firstproduct ge_second_rn_gcd_zerocommon_firstproduct ge_second_ip_gcd_zerocommon_firstproduct ge_second_in_gcd_zerocommon_firstproduct. ((exists ge_representation_real_code_gcd_zerocommon_firstproductfirst ge_representation_imaginary_code_gcd_zerocommon_firstproductfirst. (((gr_common_divisor_gcd_zero) = ((ge_representation_real_code_gcd_zerocommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_zerocommon_firstproductfirst)) * S ((ge_representation_real_code_gcd_zerocommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_zerocommon_firstproductfirst)) + ((ge_representation_imaginary_code_gcd_zerocommon_firstproductfirst) + (ge_representation_imaginary_code_gcd_zerocommon_firstproductfirst))) /\ ((exists ge_balance_positive_gcd_zerocommon_firstproductfirstreal ge_balance_negative_gcd_zerocommon_firstproductfirstreal. (((((ge_representation_real_code_gcd_zerocommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_zerocommon_firstproductfirstreal) /\ (ge_balance_negative_gcd_zerocommon_firstproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zerocommon_firstproductfirstrealdecode. (((ge_representation_real_code_gcd_zerocommon_firstproductfirst) = 2 * ge_signed_half_gcd_zerocommon_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zerocommon_firstproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zerocommon_firstproductfirstreal) = S ge_signed_half_gcd_zerocommon_firstproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zerocommon_firstproduct) + ge_balance_negative_gcd_zerocommon_firstproductfirstreal = (ge_first_rn_gcd_zerocommon_firstproduct) + ge_balance_positive_gcd_zerocommon_firstproductfirstreal))) /\ (exists ge_balance_positive_gcd_zerocommon_firstproductfirstimaginary ge_balance_negative_gcd_zerocommon_firstproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zerocommon_firstproductfirst) = 2 * (ge_balance_positive_gcd_zerocommon_firstproductfirstimaginary) /\ (ge_balance_negative_gcd_zerocommon_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zerocommon_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zerocommon_firstproductfirst) = 2 * ge_signed_half_gcd_zerocommon_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerocommon_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zerocommon_firstproductfirstimaginary) = S ge_signed_half_gcd_zerocommon_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zerocommon_firstproduct) + ge_balance_negative_gcd_zerocommon_firstproductfirstimaginary = (ge_first_in_gcd_zerocommon_firstproduct) + ge_balance_positive_gcd_zerocommon_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zerocommon_firstproductsecond ge_representation_imaginary_code_gcd_zerocommon_firstproductsecond. (((gr_quotient_gcd_zerocommon_first) = ((ge_representation_real_code_gcd_zerocommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_zerocommon_firstproductsecond)) * S ((ge_representation_real_code_gcd_zerocommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_zerocommon_firstproductsecond)) + ((ge_representation_imaginary_code_gcd_zerocommon_firstproductsecond) + (ge_representation_imaginary_code_gcd_zerocommon_firstproductsecond))) /\ ((exists ge_balance_positive_gcd_zerocommon_firstproductsecondreal ge_balance_negative_gcd_zerocommon_firstproductsecondreal. (((((ge_representation_real_code_gcd_zerocommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_zerocommon_firstproductsecondreal) /\ (ge_balance_negative_gcd_zerocommon_firstproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zerocommon_firstproductsecondrealdecode. (((ge_representation_real_code_gcd_zerocommon_firstproductsecond) = 2 * ge_signed_half_gcd_zerocommon_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zerocommon_firstproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zerocommon_firstproductsecondreal) = S ge_signed_half_gcd_zerocommon_firstproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zerocommon_firstproduct) + ge_balance_negative_gcd_zerocommon_firstproductsecondreal = (ge_second_rn_gcd_zerocommon_firstproduct) + ge_balance_positive_gcd_zerocommon_firstproductsecondreal))) /\ (exists ge_balance_positive_gcd_zerocommon_firstproductsecondimaginary ge_balance_negative_gcd_zerocommon_firstproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zerocommon_firstproductsecond) = 2 * (ge_balance_positive_gcd_zerocommon_firstproductsecondimaginary) /\ (ge_balance_negative_gcd_zerocommon_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zerocommon_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zerocommon_firstproductsecond) = 2 * ge_signed_half_gcd_zerocommon_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerocommon_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zerocommon_firstproductsecondimaginary) = S ge_signed_half_gcd_zerocommon_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zerocommon_firstproduct) + ge_balance_negative_gcd_zerocommon_firstproductsecondimaginary = (ge_second_in_gcd_zerocommon_firstproduct) + ge_balance_positive_gcd_zerocommon_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zerocommon_firstproductoutput ge_representation_imaginary_code_gcd_zerocommon_firstproductoutput. (((a) = ((ge_representation_real_code_gcd_zerocommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_zerocommon_firstproductoutput)) * S ((ge_representation_real_code_gcd_zerocommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_zerocommon_firstproductoutput)) + ((ge_representation_imaginary_code_gcd_zerocommon_firstproductoutput) + (ge_representation_imaginary_code_gcd_zerocommon_firstproductoutput))) /\ ((exists ge_balance_positive_gcd_zerocommon_firstproductoutputreal ge_balance_negative_gcd_zerocommon_firstproductoutputreal. (((((ge_representation_real_code_gcd_zerocommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_zerocommon_firstproductoutputreal) /\ (ge_balance_negative_gcd_zerocommon_firstproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zerocommon_firstproductoutputrealdecode. (((ge_representation_real_code_gcd_zerocommon_firstproductoutput) = 2 * ge_signed_half_gcd_zerocommon_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zerocommon_firstproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zerocommon_firstproductoutputreal) = S ge_signed_half_gcd_zerocommon_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zerocommon_firstproduct) * (ge_second_rp_gcd_zerocommon_firstproduct))) + (((ge_first_rn_gcd_zerocommon_firstproduct) * (ge_second_rn_gcd_zerocommon_firstproduct))))) + (((((ge_first_ip_gcd_zerocommon_firstproduct) * (ge_second_in_gcd_zerocommon_firstproduct))) + (((ge_first_in_gcd_zerocommon_firstproduct) * (ge_second_ip_gcd_zerocommon_firstproduct))))))) + ge_balance_negative_gcd_zerocommon_firstproductoutputreal = (((((((ge_first_rp_gcd_zerocommon_firstproduct) * (ge_second_rn_gcd_zerocommon_firstproduct))) + (((ge_first_rn_gcd_zerocommon_firstproduct) * (ge_second_rp_gcd_zerocommon_firstproduct))))) + (((((ge_first_ip_gcd_zerocommon_firstproduct) * (ge_second_ip_gcd_zerocommon_firstproduct))) + (((ge_first_in_gcd_zerocommon_firstproduct) * (ge_second_in_gcd_zerocommon_firstproduct))))))) + ge_balance_positive_gcd_zerocommon_firstproductoutputreal))) /\ (exists ge_balance_positive_gcd_zerocommon_firstproductoutputimaginary ge_balance_negative_gcd_zerocommon_firstproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zerocommon_firstproductoutput) = 2 * (ge_balance_positive_gcd_zerocommon_firstproductoutputimaginary) /\ (ge_balance_negative_gcd_zerocommon_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zerocommon_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zerocommon_firstproductoutput) = 2 * ge_signed_half_gcd_zerocommon_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerocommon_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zerocommon_firstproductoutputimaginary) = S ge_signed_half_gcd_zerocommon_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zerocommon_firstproduct) * (ge_second_ip_gcd_zerocommon_firstproduct))) + (((ge_first_rn_gcd_zerocommon_firstproduct) * (ge_second_in_gcd_zerocommon_firstproduct))))) + (((((ge_first_ip_gcd_zerocommon_firstproduct) * (ge_second_rp_gcd_zerocommon_firstproduct))) + (((ge_first_in_gcd_zerocommon_firstproduct) * (ge_second_rn_gcd_zerocommon_firstproduct))))))) + ge_balance_negative_gcd_zerocommon_firstproductoutputimaginary = (((((((ge_first_rp_gcd_zerocommon_firstproduct) * (ge_second_in_gcd_zerocommon_firstproduct))) + (((ge_first_rn_gcd_zerocommon_firstproduct) * (ge_second_ip_gcd_zerocommon_firstproduct))))) + (((((ge_first_ip_gcd_zerocommon_firstproduct) * (ge_second_rn_gcd_zerocommon_firstproduct))) + (((ge_first_in_gcd_zerocommon_firstproduct) * (ge_second_rp_gcd_zerocommon_firstproduct))))))) + ge_balance_positive_gcd_zerocommon_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_zerocommon_second. (exists ge_first_rp_gcd_zerocommon_secondproduct ge_first_rn_gcd_zerocommon_secondproduct ge_first_ip_gcd_zerocommon_secondproduct ge_first_in_gcd_zerocommon_secondproduct ge_second_rp_gcd_zerocommon_secondproduct ge_second_rn_gcd_zerocommon_secondproduct ge_second_ip_gcd_zerocommon_secondproduct ge_second_in_gcd_zerocommon_secondproduct. ((exists ge_representation_real_code_gcd_zerocommon_secondproductfirst ge_representation_imaginary_code_gcd_zerocommon_secondproductfirst. (((gr_common_divisor_gcd_zero) = ((ge_representation_real_code_gcd_zerocommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_zerocommon_secondproductfirst)) * S ((ge_representation_real_code_gcd_zerocommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_zerocommon_secondproductfirst)) + ((ge_representation_imaginary_code_gcd_zerocommon_secondproductfirst) + (ge_representation_imaginary_code_gcd_zerocommon_secondproductfirst))) /\ ((exists ge_balance_positive_gcd_zerocommon_secondproductfirstreal ge_balance_negative_gcd_zerocommon_secondproductfirstreal. (((((ge_representation_real_code_gcd_zerocommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_zerocommon_secondproductfirstreal) /\ (ge_balance_negative_gcd_zerocommon_secondproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zerocommon_secondproductfirstrealdecode. (((ge_representation_real_code_gcd_zerocommon_secondproductfirst) = 2 * ge_signed_half_gcd_zerocommon_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zerocommon_secondproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zerocommon_secondproductfirstreal) = S ge_signed_half_gcd_zerocommon_secondproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zerocommon_secondproduct) + ge_balance_negative_gcd_zerocommon_secondproductfirstreal = (ge_first_rn_gcd_zerocommon_secondproduct) + ge_balance_positive_gcd_zerocommon_secondproductfirstreal))) /\ (exists ge_balance_positive_gcd_zerocommon_secondproductfirstimaginary ge_balance_negative_gcd_zerocommon_secondproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zerocommon_secondproductfirst) = 2 * (ge_balance_positive_gcd_zerocommon_secondproductfirstimaginary) /\ (ge_balance_negative_gcd_zerocommon_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zerocommon_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zerocommon_secondproductfirst) = 2 * ge_signed_half_gcd_zerocommon_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerocommon_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zerocommon_secondproductfirstimaginary) = S ge_signed_half_gcd_zerocommon_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zerocommon_secondproduct) + ge_balance_negative_gcd_zerocommon_secondproductfirstimaginary = (ge_first_in_gcd_zerocommon_secondproduct) + ge_balance_positive_gcd_zerocommon_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zerocommon_secondproductsecond ge_representation_imaginary_code_gcd_zerocommon_secondproductsecond. (((gr_quotient_gcd_zerocommon_second) = ((ge_representation_real_code_gcd_zerocommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_zerocommon_secondproductsecond)) * S ((ge_representation_real_code_gcd_zerocommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_zerocommon_secondproductsecond)) + ((ge_representation_imaginary_code_gcd_zerocommon_secondproductsecond) + (ge_representation_imaginary_code_gcd_zerocommon_secondproductsecond))) /\ ((exists ge_balance_positive_gcd_zerocommon_secondproductsecondreal ge_balance_negative_gcd_zerocommon_secondproductsecondreal. (((((ge_representation_real_code_gcd_zerocommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_zerocommon_secondproductsecondreal) /\ (ge_balance_negative_gcd_zerocommon_secondproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zerocommon_secondproductsecondrealdecode. (((ge_representation_real_code_gcd_zerocommon_secondproductsecond) = 2 * ge_signed_half_gcd_zerocommon_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zerocommon_secondproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zerocommon_secondproductsecondreal) = S ge_signed_half_gcd_zerocommon_secondproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zerocommon_secondproduct) + ge_balance_negative_gcd_zerocommon_secondproductsecondreal = (ge_second_rn_gcd_zerocommon_secondproduct) + ge_balance_positive_gcd_zerocommon_secondproductsecondreal))) /\ (exists ge_balance_positive_gcd_zerocommon_secondproductsecondimaginary ge_balance_negative_gcd_zerocommon_secondproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zerocommon_secondproductsecond) = 2 * (ge_balance_positive_gcd_zerocommon_secondproductsecondimaginary) /\ (ge_balance_negative_gcd_zerocommon_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zerocommon_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zerocommon_secondproductsecond) = 2 * ge_signed_half_gcd_zerocommon_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerocommon_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zerocommon_secondproductsecondimaginary) = S ge_signed_half_gcd_zerocommon_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zerocommon_secondproduct) + ge_balance_negative_gcd_zerocommon_secondproductsecondimaginary = (ge_second_in_gcd_zerocommon_secondproduct) + ge_balance_positive_gcd_zerocommon_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zerocommon_secondproductoutput ge_representation_imaginary_code_gcd_zerocommon_secondproductoutput. (((0) = ((ge_representation_real_code_gcd_zerocommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_zerocommon_secondproductoutput)) * S ((ge_representation_real_code_gcd_zerocommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_zerocommon_secondproductoutput)) + ((ge_representation_imaginary_code_gcd_zerocommon_secondproductoutput) + (ge_representation_imaginary_code_gcd_zerocommon_secondproductoutput))) /\ ((exists ge_balance_positive_gcd_zerocommon_secondproductoutputreal ge_balance_negative_gcd_zerocommon_secondproductoutputreal. (((((ge_representation_real_code_gcd_zerocommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_zerocommon_secondproductoutputreal) /\ (ge_balance_negative_gcd_zerocommon_secondproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zerocommon_secondproductoutputrealdecode. (((ge_representation_real_code_gcd_zerocommon_secondproductoutput) = 2 * ge_signed_half_gcd_zerocommon_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zerocommon_secondproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zerocommon_secondproductoutputreal) = S ge_signed_half_gcd_zerocommon_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zerocommon_secondproduct) * (ge_second_rp_gcd_zerocommon_secondproduct))) + (((ge_first_rn_gcd_zerocommon_secondproduct) * (ge_second_rn_gcd_zerocommon_secondproduct))))) + (((((ge_first_ip_gcd_zerocommon_secondproduct) * (ge_second_in_gcd_zerocommon_secondproduct))) + (((ge_first_in_gcd_zerocommon_secondproduct) * (ge_second_ip_gcd_zerocommon_secondproduct))))))) + ge_balance_negative_gcd_zerocommon_secondproductoutputreal = (((((((ge_first_rp_gcd_zerocommon_secondproduct) * (ge_second_rn_gcd_zerocommon_secondproduct))) + (((ge_first_rn_gcd_zerocommon_secondproduct) * (ge_second_rp_gcd_zerocommon_secondproduct))))) + (((((ge_first_ip_gcd_zerocommon_secondproduct) * (ge_second_ip_gcd_zerocommon_secondproduct))) + (((ge_first_in_gcd_zerocommon_secondproduct) * (ge_second_in_gcd_zerocommon_secondproduct))))))) + ge_balance_positive_gcd_zerocommon_secondproductoutputreal))) /\ (exists ge_balance_positive_gcd_zerocommon_secondproductoutputimaginary ge_balance_negative_gcd_zerocommon_secondproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zerocommon_secondproductoutput) = 2 * (ge_balance_positive_gcd_zerocommon_secondproductoutputimaginary) /\ (ge_balance_negative_gcd_zerocommon_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zerocommon_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zerocommon_secondproductoutput) = 2 * ge_signed_half_gcd_zerocommon_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerocommon_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zerocommon_secondproductoutputimaginary) = S ge_signed_half_gcd_zerocommon_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zerocommon_secondproduct) * (ge_second_ip_gcd_zerocommon_secondproduct))) + (((ge_first_rn_gcd_zerocommon_secondproduct) * (ge_second_in_gcd_zerocommon_secondproduct))))) + (((((ge_first_ip_gcd_zerocommon_secondproduct) * (ge_second_rp_gcd_zerocommon_secondproduct))) + (((ge_first_in_gcd_zerocommon_secondproduct) * (ge_second_rn_gcd_zerocommon_secondproduct))))))) + ge_balance_negative_gcd_zerocommon_secondproductoutputimaginary = (((((((ge_first_rp_gcd_zerocommon_secondproduct) * (ge_second_in_gcd_zerocommon_secondproduct))) + (((ge_first_rn_gcd_zerocommon_secondproduct) * (ge_second_ip_gcd_zerocommon_secondproduct))))) + (((((ge_first_ip_gcd_zerocommon_secondproduct) * (ge_second_rn_gcd_zerocommon_secondproduct))) + (((ge_first_in_gcd_zerocommon_secondproduct) * (ge_second_rp_gcd_zerocommon_secondproduct))))))) + ge_balance_positive_gcd_zerocommon_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_gcd_zerogreatest. (exists ge_first_rp_gcd_zerogreatestproduct ge_first_rn_gcd_zerogreatestproduct ge_first_ip_gcd_zerogreatestproduct ge_first_in_gcd_zerogreatestproduct ge_second_rp_gcd_zerogreatestproduct ge_second_rn_gcd_zerogreatestproduct ge_second_ip_gcd_zerogreatestproduct ge_second_in_gcd_zerogreatestproduct. ((exists ge_representation_real_code_gcd_zerogreatestproductfirst ge_representation_imaginary_code_gcd_zerogreatestproductfirst. (((gr_common_divisor_gcd_zero) = ((ge_representation_real_code_gcd_zerogreatestproductfirst) + (ge_representation_imaginary_code_gcd_zerogreatestproductfirst)) * S ((ge_representation_real_code_gcd_zerogreatestproductfirst) + (ge_representation_imaginary_code_gcd_zerogreatestproductfirst)) + ((ge_representation_imaginary_code_gcd_zerogreatestproductfirst) + (ge_representation_imaginary_code_gcd_zerogreatestproductfirst))) /\ ((exists ge_balance_positive_gcd_zerogreatestproductfirstreal ge_balance_negative_gcd_zerogreatestproductfirstreal. (((((ge_representation_real_code_gcd_zerogreatestproductfirst) = 2 * (ge_balance_positive_gcd_zerogreatestproductfirstreal) /\ (ge_balance_negative_gcd_zerogreatestproductfirstreal) = 0) \/ exists ge_signed_half_gcd_zerogreatestproductfirstrealdecode. (((ge_representation_real_code_gcd_zerogreatestproductfirst) = 2 * ge_signed_half_gcd_zerogreatestproductfirstrealdecode + 1 /\ (ge_balance_positive_gcd_zerogreatestproductfirstreal) = 0) /\ (ge_balance_negative_gcd_zerogreatestproductfirstreal) = S ge_signed_half_gcd_zerogreatestproductfirstrealdecode))) /\ ((ge_first_rp_gcd_zerogreatestproduct) + ge_balance_negative_gcd_zerogreatestproductfirstreal = (ge_first_rn_gcd_zerogreatestproduct) + ge_balance_positive_gcd_zerogreatestproductfirstreal))) /\ (exists ge_balance_positive_gcd_zerogreatestproductfirstimaginary ge_balance_negative_gcd_zerogreatestproductfirstimaginary. (((((ge_representation_imaginary_code_gcd_zerogreatestproductfirst) = 2 * (ge_balance_positive_gcd_zerogreatestproductfirstimaginary) /\ (ge_balance_negative_gcd_zerogreatestproductfirstimaginary) = 0) \/ exists ge_signed_half_gcd_zerogreatestproductfirstimaginarydecode. (((ge_representation_imaginary_code_gcd_zerogreatestproductfirst) = 2 * ge_signed_half_gcd_zerogreatestproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerogreatestproductfirstimaginary) = 0) /\ (ge_balance_negative_gcd_zerogreatestproductfirstimaginary) = S ge_signed_half_gcd_zerogreatestproductfirstimaginarydecode))) /\ ((ge_first_ip_gcd_zerogreatestproduct) + ge_balance_negative_gcd_zerogreatestproductfirstimaginary = (ge_first_in_gcd_zerogreatestproduct) + ge_balance_positive_gcd_zerogreatestproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gcd_zerogreatestproductsecond ge_representation_imaginary_code_gcd_zerogreatestproductsecond. (((gr_quotient_gcd_zerogreatest) = ((ge_representation_real_code_gcd_zerogreatestproductsecond) + (ge_representation_imaginary_code_gcd_zerogreatestproductsecond)) * S ((ge_representation_real_code_gcd_zerogreatestproductsecond) + (ge_representation_imaginary_code_gcd_zerogreatestproductsecond)) + ((ge_representation_imaginary_code_gcd_zerogreatestproductsecond) + (ge_representation_imaginary_code_gcd_zerogreatestproductsecond))) /\ ((exists ge_balance_positive_gcd_zerogreatestproductsecondreal ge_balance_negative_gcd_zerogreatestproductsecondreal. (((((ge_representation_real_code_gcd_zerogreatestproductsecond) = 2 * (ge_balance_positive_gcd_zerogreatestproductsecondreal) /\ (ge_balance_negative_gcd_zerogreatestproductsecondreal) = 0) \/ exists ge_signed_half_gcd_zerogreatestproductsecondrealdecode. (((ge_representation_real_code_gcd_zerogreatestproductsecond) = 2 * ge_signed_half_gcd_zerogreatestproductsecondrealdecode + 1 /\ (ge_balance_positive_gcd_zerogreatestproductsecondreal) = 0) /\ (ge_balance_negative_gcd_zerogreatestproductsecondreal) = S ge_signed_half_gcd_zerogreatestproductsecondrealdecode))) /\ ((ge_second_rp_gcd_zerogreatestproduct) + ge_balance_negative_gcd_zerogreatestproductsecondreal = (ge_second_rn_gcd_zerogreatestproduct) + ge_balance_positive_gcd_zerogreatestproductsecondreal))) /\ (exists ge_balance_positive_gcd_zerogreatestproductsecondimaginary ge_balance_negative_gcd_zerogreatestproductsecondimaginary. (((((ge_representation_imaginary_code_gcd_zerogreatestproductsecond) = 2 * (ge_balance_positive_gcd_zerogreatestproductsecondimaginary) /\ (ge_balance_negative_gcd_zerogreatestproductsecondimaginary) = 0) \/ exists ge_signed_half_gcd_zerogreatestproductsecondimaginarydecode. (((ge_representation_imaginary_code_gcd_zerogreatestproductsecond) = 2 * ge_signed_half_gcd_zerogreatestproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerogreatestproductsecondimaginary) = 0) /\ (ge_balance_negative_gcd_zerogreatestproductsecondimaginary) = S ge_signed_half_gcd_zerogreatestproductsecondimaginarydecode))) /\ ((ge_second_ip_gcd_zerogreatestproduct) + ge_balance_negative_gcd_zerogreatestproductsecondimaginary = (ge_second_in_gcd_zerogreatestproduct) + ge_balance_positive_gcd_zerogreatestproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gcd_zerogreatestproductoutput ge_representation_imaginary_code_gcd_zerogreatestproductoutput. (((a) = ((ge_representation_real_code_gcd_zerogreatestproductoutput) + (ge_representation_imaginary_code_gcd_zerogreatestproductoutput)) * S ((ge_representation_real_code_gcd_zerogreatestproductoutput) + (ge_representation_imaginary_code_gcd_zerogreatestproductoutput)) + ((ge_representation_imaginary_code_gcd_zerogreatestproductoutput) + (ge_representation_imaginary_code_gcd_zerogreatestproductoutput))) /\ ((exists ge_balance_positive_gcd_zerogreatestproductoutputreal ge_balance_negative_gcd_zerogreatestproductoutputreal. (((((ge_representation_real_code_gcd_zerogreatestproductoutput) = 2 * (ge_balance_positive_gcd_zerogreatestproductoutputreal) /\ (ge_balance_negative_gcd_zerogreatestproductoutputreal) = 0) \/ exists ge_signed_half_gcd_zerogreatestproductoutputrealdecode. (((ge_representation_real_code_gcd_zerogreatestproductoutput) = 2 * ge_signed_half_gcd_zerogreatestproductoutputrealdecode + 1 /\ (ge_balance_positive_gcd_zerogreatestproductoutputreal) = 0) /\ (ge_balance_negative_gcd_zerogreatestproductoutputreal) = S ge_signed_half_gcd_zerogreatestproductoutputrealdecode))) /\ ((((((((ge_first_rp_gcd_zerogreatestproduct) * (ge_second_rp_gcd_zerogreatestproduct))) + (((ge_first_rn_gcd_zerogreatestproduct) * (ge_second_rn_gcd_zerogreatestproduct))))) + (((((ge_first_ip_gcd_zerogreatestproduct) * (ge_second_in_gcd_zerogreatestproduct))) + (((ge_first_in_gcd_zerogreatestproduct) * (ge_second_ip_gcd_zerogreatestproduct))))))) + ge_balance_negative_gcd_zerogreatestproductoutputreal = (((((((ge_first_rp_gcd_zerogreatestproduct) * (ge_second_rn_gcd_zerogreatestproduct))) + (((ge_first_rn_gcd_zerogreatestproduct) * (ge_second_rp_gcd_zerogreatestproduct))))) + (((((ge_first_ip_gcd_zerogreatestproduct) * (ge_second_ip_gcd_zerogreatestproduct))) + (((ge_first_in_gcd_zerogreatestproduct) * (ge_second_in_gcd_zerogreatestproduct))))))) + ge_balance_positive_gcd_zerogreatestproductoutputreal))) /\ (exists ge_balance_positive_gcd_zerogreatestproductoutputimaginary ge_balance_negative_gcd_zerogreatestproductoutputimaginary. (((((ge_representation_imaginary_code_gcd_zerogreatestproductoutput) = 2 * (ge_balance_positive_gcd_zerogreatestproductoutputimaginary) /\ (ge_balance_negative_gcd_zerogreatestproductoutputimaginary) = 0) \/ exists ge_signed_half_gcd_zerogreatestproductoutputimaginarydecode. (((ge_representation_imaginary_code_gcd_zerogreatestproductoutput) = 2 * ge_signed_half_gcd_zerogreatestproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gcd_zerogreatestproductoutputimaginary) = 0) /\ (ge_balance_negative_gcd_zerogreatestproductoutputimaginary) = S ge_signed_half_gcd_zerogreatestproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gcd_zerogreatestproduct) * (ge_second_ip_gcd_zerogreatestproduct))) + (((ge_first_rn_gcd_zerogreatestproduct) * (ge_second_in_gcd_zerogreatestproduct))))) + (((((ge_first_ip_gcd_zerogreatestproduct) * (ge_second_rp_gcd_zerogreatestproduct))) + (((ge_first_in_gcd_zerogreatestproduct) * (ge_second_rn_gcd_zerogreatestproduct))))))) + ge_balance_negative_gcd_zerogreatestproductoutputimaginary = (((((((ge_first_rp_gcd_zerogreatestproduct) * (ge_second_in_gcd_zerogreatestproduct))) + (((ge_first_rn_gcd_zerogreatestproduct) * (ge_second_ip_gcd_zerogreatestproduct))))) + (((((ge_first_ip_gcd_zerogreatestproduct) * (ge_second_rn_gcd_zerogreatestproduct))) + (((ge_first_in_gcd_zerogreatestproduct) * (ge_second_rp_gcd_zerogreatestproduct))))))) + ge_balance_positive_gcd_zerogreatestproductoutputimaginary)))))))))))))) /\ (exists gr_first_product_bezout_zero gr_second_product_bezout_zero. ((exists ge_first_rp_bezout_zerofirst ge_first_rn_bezout_zerofirst ge_first_ip_bezout_zerofirst ge_first_in_bezout_zerofirst ge_second_rp_bezout_zerofirst ge_second_rn_bezout_zerofirst ge_second_ip_bezout_zerofirst ge_second_in_bezout_zerofirst. ((exists ge_representation_real_code_bezout_zerofirstfirst ge_representation_imaginary_code_bezout_zerofirstfirst. (((a) = ((ge_representation_real_code_bezout_zerofirstfirst) + (ge_representation_imaginary_code_bezout_zerofirstfirst)) * S ((ge_representation_real_code_bezout_zerofirstfirst) + (ge_representation_imaginary_code_bezout_zerofirstfirst)) + ((ge_representation_imaginary_code_bezout_zerofirstfirst) + (ge_representation_imaginary_code_bezout_zerofirstfirst))) /\ ((exists ge_balance_positive_bezout_zerofirstfirstreal ge_balance_negative_bezout_zerofirstfirstreal. (((((ge_representation_real_code_bezout_zerofirstfirst) = 2 * (ge_balance_positive_bezout_zerofirstfirstreal) /\ (ge_balance_negative_bezout_zerofirstfirstreal) = 0) \/ exists ge_signed_half_bezout_zerofirstfirstrealdecode. (((ge_representation_real_code_bezout_zerofirstfirst) = 2 * ge_signed_half_bezout_zerofirstfirstrealdecode + 1 /\ (ge_balance_positive_bezout_zerofirstfirstreal) = 0) /\ (ge_balance_negative_bezout_zerofirstfirstreal) = S ge_signed_half_bezout_zerofirstfirstrealdecode))) /\ ((ge_first_rp_bezout_zerofirst) + ge_balance_negative_bezout_zerofirstfirstreal = (ge_first_rn_bezout_zerofirst) + ge_balance_positive_bezout_zerofirstfirstreal))) /\ (exists ge_balance_positive_bezout_zerofirstfirstimaginary ge_balance_negative_bezout_zerofirstfirstimaginary. (((((ge_representation_imaginary_code_bezout_zerofirstfirst) = 2 * (ge_balance_positive_bezout_zerofirstfirstimaginary) /\ (ge_balance_negative_bezout_zerofirstfirstimaginary) = 0) \/ exists ge_signed_half_bezout_zerofirstfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_zerofirstfirst) = 2 * ge_signed_half_bezout_zerofirstfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_zerofirstfirstimaginary) = 0) /\ (ge_balance_negative_bezout_zerofirstfirstimaginary) = S ge_signed_half_bezout_zerofirstfirstimaginarydecode))) /\ ((ge_first_ip_bezout_zerofirst) + ge_balance_negative_bezout_zerofirstfirstimaginary = (ge_first_in_bezout_zerofirst) + ge_balance_positive_bezout_zerofirstfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_zerofirstsecond ge_representation_imaginary_code_bezout_zerofirstsecond. (((6) = ((ge_representation_real_code_bezout_zerofirstsecond) + (ge_representation_imaginary_code_bezout_zerofirstsecond)) * S ((ge_representation_real_code_bezout_zerofirstsecond) + (ge_representation_imaginary_code_bezout_zerofirstsecond)) + ((ge_representation_imaginary_code_bezout_zerofirstsecond) + (ge_representation_imaginary_code_bezout_zerofirstsecond))) /\ ((exists ge_balance_positive_bezout_zerofirstsecondreal ge_balance_negative_bezout_zerofirstsecondreal. (((((ge_representation_real_code_bezout_zerofirstsecond) = 2 * (ge_balance_positive_bezout_zerofirstsecondreal) /\ (ge_balance_negative_bezout_zerofirstsecondreal) = 0) \/ exists ge_signed_half_bezout_zerofirstsecondrealdecode. (((ge_representation_real_code_bezout_zerofirstsecond) = 2 * ge_signed_half_bezout_zerofirstsecondrealdecode + 1 /\ (ge_balance_positive_bezout_zerofirstsecondreal) = 0) /\ (ge_balance_negative_bezout_zerofirstsecondreal) = S ge_signed_half_bezout_zerofirstsecondrealdecode))) /\ ((ge_second_rp_bezout_zerofirst) + ge_balance_negative_bezout_zerofirstsecondreal = (ge_second_rn_bezout_zerofirst) + ge_balance_positive_bezout_zerofirstsecondreal))) /\ (exists ge_balance_positive_bezout_zerofirstsecondimaginary ge_balance_negative_bezout_zerofirstsecondimaginary. (((((ge_representation_imaginary_code_bezout_zerofirstsecond) = 2 * (ge_balance_positive_bezout_zerofirstsecondimaginary) /\ (ge_balance_negative_bezout_zerofirstsecondimaginary) = 0) \/ exists ge_signed_half_bezout_zerofirstsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_zerofirstsecond) = 2 * ge_signed_half_bezout_zerofirstsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_zerofirstsecondimaginary) = 0) /\ (ge_balance_negative_bezout_zerofirstsecondimaginary) = S ge_signed_half_bezout_zerofirstsecondimaginarydecode))) /\ ((ge_second_ip_bezout_zerofirst) + ge_balance_negative_bezout_zerofirstsecondimaginary = (ge_second_in_bezout_zerofirst) + ge_balance_positive_bezout_zerofirstsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_zerofirstoutput ge_representation_imaginary_code_bezout_zerofirstoutput. (((gr_first_product_bezout_zero) = ((ge_representation_real_code_bezout_zerofirstoutput) + (ge_representation_imaginary_code_bezout_zerofirstoutput)) * S ((ge_representation_real_code_bezout_zerofirstoutput) + (ge_representation_imaginary_code_bezout_zerofirstoutput)) + ((ge_representation_imaginary_code_bezout_zerofirstoutput) + (ge_representation_imaginary_code_bezout_zerofirstoutput))) /\ ((exists ge_balance_positive_bezout_zerofirstoutputreal ge_balance_negative_bezout_zerofirstoutputreal. (((((ge_representation_real_code_bezout_zerofirstoutput) = 2 * (ge_balance_positive_bezout_zerofirstoutputreal) /\ (ge_balance_negative_bezout_zerofirstoutputreal) = 0) \/ exists ge_signed_half_bezout_zerofirstoutputrealdecode. (((ge_representation_real_code_bezout_zerofirstoutput) = 2 * ge_signed_half_bezout_zerofirstoutputrealdecode + 1 /\ (ge_balance_positive_bezout_zerofirstoutputreal) = 0) /\ (ge_balance_negative_bezout_zerofirstoutputreal) = S ge_signed_half_bezout_zerofirstoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_zerofirst) * (ge_second_rp_bezout_zerofirst))) + (((ge_first_rn_bezout_zerofirst) * (ge_second_rn_bezout_zerofirst))))) + (((((ge_first_ip_bezout_zerofirst) * (ge_second_in_bezout_zerofirst))) + (((ge_first_in_bezout_zerofirst) * (ge_second_ip_bezout_zerofirst))))))) + ge_balance_negative_bezout_zerofirstoutputreal = (((((((ge_first_rp_bezout_zerofirst) * (ge_second_rn_bezout_zerofirst))) + (((ge_first_rn_bezout_zerofirst) * (ge_second_rp_bezout_zerofirst))))) + (((((ge_first_ip_bezout_zerofirst) * (ge_second_ip_bezout_zerofirst))) + (((ge_first_in_bezout_zerofirst) * (ge_second_in_bezout_zerofirst))))))) + ge_balance_positive_bezout_zerofirstoutputreal))) /\ (exists ge_balance_positive_bezout_zerofirstoutputimaginary ge_balance_negative_bezout_zerofirstoutputimaginary. (((((ge_representation_imaginary_code_bezout_zerofirstoutput) = 2 * (ge_balance_positive_bezout_zerofirstoutputimaginary) /\ (ge_balance_negative_bezout_zerofirstoutputimaginary) = 0) \/ exists ge_signed_half_bezout_zerofirstoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_zerofirstoutput) = 2 * ge_signed_half_bezout_zerofirstoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_zerofirstoutputimaginary) = 0) /\ (ge_balance_negative_bezout_zerofirstoutputimaginary) = S ge_signed_half_bezout_zerofirstoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_zerofirst) * (ge_second_ip_bezout_zerofirst))) + (((ge_first_rn_bezout_zerofirst) * (ge_second_in_bezout_zerofirst))))) + (((((ge_first_ip_bezout_zerofirst) * (ge_second_rp_bezout_zerofirst))) + (((ge_first_in_bezout_zerofirst) * (ge_second_rn_bezout_zerofirst))))))) + ge_balance_negative_bezout_zerofirstoutputimaginary = (((((((ge_first_rp_bezout_zerofirst) * (ge_second_in_bezout_zerofirst))) + (((ge_first_rn_bezout_zerofirst) * (ge_second_ip_bezout_zerofirst))))) + (((((ge_first_ip_bezout_zerofirst) * (ge_second_rn_bezout_zerofirst))) + (((ge_first_in_bezout_zerofirst) * (ge_second_rp_bezout_zerofirst))))))) + ge_balance_positive_bezout_zerofirstoutputimaginary))))))))) /\ ((exists ge_first_rp_bezout_zerosecond ge_first_rn_bezout_zerosecond ge_first_ip_bezout_zerosecond ge_first_in_bezout_zerosecond ge_second_rp_bezout_zerosecond ge_second_rn_bezout_zerosecond ge_second_ip_bezout_zerosecond ge_second_in_bezout_zerosecond. ((exists ge_representation_real_code_bezout_zerosecondfirst ge_representation_imaginary_code_bezout_zerosecondfirst. (((0) = ((ge_representation_real_code_bezout_zerosecondfirst) + (ge_representation_imaginary_code_bezout_zerosecondfirst)) * S ((ge_representation_real_code_bezout_zerosecondfirst) + (ge_representation_imaginary_code_bezout_zerosecondfirst)) + ((ge_representation_imaginary_code_bezout_zerosecondfirst) + (ge_representation_imaginary_code_bezout_zerosecondfirst))) /\ ((exists ge_balance_positive_bezout_zerosecondfirstreal ge_balance_negative_bezout_zerosecondfirstreal. (((((ge_representation_real_code_bezout_zerosecondfirst) = 2 * (ge_balance_positive_bezout_zerosecondfirstreal) /\ (ge_balance_negative_bezout_zerosecondfirstreal) = 0) \/ exists ge_signed_half_bezout_zerosecondfirstrealdecode. (((ge_representation_real_code_bezout_zerosecondfirst) = 2 * ge_signed_half_bezout_zerosecondfirstrealdecode + 1 /\ (ge_balance_positive_bezout_zerosecondfirstreal) = 0) /\ (ge_balance_negative_bezout_zerosecondfirstreal) = S ge_signed_half_bezout_zerosecondfirstrealdecode))) /\ ((ge_first_rp_bezout_zerosecond) + ge_balance_negative_bezout_zerosecondfirstreal = (ge_first_rn_bezout_zerosecond) + ge_balance_positive_bezout_zerosecondfirstreal))) /\ (exists ge_balance_positive_bezout_zerosecondfirstimaginary ge_balance_negative_bezout_zerosecondfirstimaginary. (((((ge_representation_imaginary_code_bezout_zerosecondfirst) = 2 * (ge_balance_positive_bezout_zerosecondfirstimaginary) /\ (ge_balance_negative_bezout_zerosecondfirstimaginary) = 0) \/ exists ge_signed_half_bezout_zerosecondfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_zerosecondfirst) = 2 * ge_signed_half_bezout_zerosecondfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_zerosecondfirstimaginary) = 0) /\ (ge_balance_negative_bezout_zerosecondfirstimaginary) = S ge_signed_half_bezout_zerosecondfirstimaginarydecode))) /\ ((ge_first_ip_bezout_zerosecond) + ge_balance_negative_bezout_zerosecondfirstimaginary = (ge_first_in_bezout_zerosecond) + ge_balance_positive_bezout_zerosecondfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_zerosecondsecond ge_representation_imaginary_code_bezout_zerosecondsecond. (((0) = ((ge_representation_real_code_bezout_zerosecondsecond) + (ge_representation_imaginary_code_bezout_zerosecondsecond)) * S ((ge_representation_real_code_bezout_zerosecondsecond) + (ge_representation_imaginary_code_bezout_zerosecondsecond)) + ((ge_representation_imaginary_code_bezout_zerosecondsecond) + (ge_representation_imaginary_code_bezout_zerosecondsecond))) /\ ((exists ge_balance_positive_bezout_zerosecondsecondreal ge_balance_negative_bezout_zerosecondsecondreal. (((((ge_representation_real_code_bezout_zerosecondsecond) = 2 * (ge_balance_positive_bezout_zerosecondsecondreal) /\ (ge_balance_negative_bezout_zerosecondsecondreal) = 0) \/ exists ge_signed_half_bezout_zerosecondsecondrealdecode. (((ge_representation_real_code_bezout_zerosecondsecond) = 2 * ge_signed_half_bezout_zerosecondsecondrealdecode + 1 /\ (ge_balance_positive_bezout_zerosecondsecondreal) = 0) /\ (ge_balance_negative_bezout_zerosecondsecondreal) = S ge_signed_half_bezout_zerosecondsecondrealdecode))) /\ ((ge_second_rp_bezout_zerosecond) + ge_balance_negative_bezout_zerosecondsecondreal = (ge_second_rn_bezout_zerosecond) + ge_balance_positive_bezout_zerosecondsecondreal))) /\ (exists ge_balance_positive_bezout_zerosecondsecondimaginary ge_balance_negative_bezout_zerosecondsecondimaginary. (((((ge_representation_imaginary_code_bezout_zerosecondsecond) = 2 * (ge_balance_positive_bezout_zerosecondsecondimaginary) /\ (ge_balance_negative_bezout_zerosecondsecondimaginary) = 0) \/ exists ge_signed_half_bezout_zerosecondsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_zerosecondsecond) = 2 * ge_signed_half_bezout_zerosecondsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_zerosecondsecondimaginary) = 0) /\ (ge_balance_negative_bezout_zerosecondsecondimaginary) = S ge_signed_half_bezout_zerosecondsecondimaginarydecode))) /\ ((ge_second_ip_bezout_zerosecond) + ge_balance_negative_bezout_zerosecondsecondimaginary = (ge_second_in_bezout_zerosecond) + ge_balance_positive_bezout_zerosecondsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_zerosecondoutput ge_representation_imaginary_code_bezout_zerosecondoutput. (((gr_second_product_bezout_zero) = ((ge_representation_real_code_bezout_zerosecondoutput) + (ge_representation_imaginary_code_bezout_zerosecondoutput)) * S ((ge_representation_real_code_bezout_zerosecondoutput) + (ge_representation_imaginary_code_bezout_zerosecondoutput)) + ((ge_representation_imaginary_code_bezout_zerosecondoutput) + (ge_representation_imaginary_code_bezout_zerosecondoutput))) /\ ((exists ge_balance_positive_bezout_zerosecondoutputreal ge_balance_negative_bezout_zerosecondoutputreal. (((((ge_representation_real_code_bezout_zerosecondoutput) = 2 * (ge_balance_positive_bezout_zerosecondoutputreal) /\ (ge_balance_negative_bezout_zerosecondoutputreal) = 0) \/ exists ge_signed_half_bezout_zerosecondoutputrealdecode. (((ge_representation_real_code_bezout_zerosecondoutput) = 2 * ge_signed_half_bezout_zerosecondoutputrealdecode + 1 /\ (ge_balance_positive_bezout_zerosecondoutputreal) = 0) /\ (ge_balance_negative_bezout_zerosecondoutputreal) = S ge_signed_half_bezout_zerosecondoutputrealdecode))) /\ ((((((((ge_first_rp_bezout_zerosecond) * (ge_second_rp_bezout_zerosecond))) + (((ge_first_rn_bezout_zerosecond) * (ge_second_rn_bezout_zerosecond))))) + (((((ge_first_ip_bezout_zerosecond) * (ge_second_in_bezout_zerosecond))) + (((ge_first_in_bezout_zerosecond) * (ge_second_ip_bezout_zerosecond))))))) + ge_balance_negative_bezout_zerosecondoutputreal = (((((((ge_first_rp_bezout_zerosecond) * (ge_second_rn_bezout_zerosecond))) + (((ge_first_rn_bezout_zerosecond) * (ge_second_rp_bezout_zerosecond))))) + (((((ge_first_ip_bezout_zerosecond) * (ge_second_ip_bezout_zerosecond))) + (((ge_first_in_bezout_zerosecond) * (ge_second_in_bezout_zerosecond))))))) + ge_balance_positive_bezout_zerosecondoutputreal))) /\ (exists ge_balance_positive_bezout_zerosecondoutputimaginary ge_balance_negative_bezout_zerosecondoutputimaginary. (((((ge_representation_imaginary_code_bezout_zerosecondoutput) = 2 * (ge_balance_positive_bezout_zerosecondoutputimaginary) /\ (ge_balance_negative_bezout_zerosecondoutputimaginary) = 0) \/ exists ge_signed_half_bezout_zerosecondoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_zerosecondoutput) = 2 * ge_signed_half_bezout_zerosecondoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_zerosecondoutputimaginary) = 0) /\ (ge_balance_negative_bezout_zerosecondoutputimaginary) = S ge_signed_half_bezout_zerosecondoutputimaginarydecode))) /\ ((((((((ge_first_rp_bezout_zerosecond) * (ge_second_ip_bezout_zerosecond))) + (((ge_first_rn_bezout_zerosecond) * (ge_second_in_bezout_zerosecond))))) + (((((ge_first_ip_bezout_zerosecond) * (ge_second_rp_bezout_zerosecond))) + (((ge_first_in_bezout_zerosecond) * (ge_second_rn_bezout_zerosecond))))))) + ge_balance_negative_bezout_zerosecondoutputimaginary = (((((((ge_first_rp_bezout_zerosecond) * (ge_second_in_bezout_zerosecond))) + (((ge_first_rn_bezout_zerosecond) * (ge_second_ip_bezout_zerosecond))))) + (((((ge_first_ip_bezout_zerosecond) * (ge_second_rn_bezout_zerosecond))) + (((ge_first_in_bezout_zerosecond) * (ge_second_rp_bezout_zerosecond))))))) + ge_balance_positive_bezout_zerosecondoutputimaginary))))))))) /\ (exists ge_first_rp_bezout_zerosum ge_first_rn_bezout_zerosum ge_first_ip_bezout_zerosum ge_first_in_bezout_zerosum ge_second_rp_bezout_zerosum ge_second_rn_bezout_zerosum ge_second_ip_bezout_zerosum ge_second_in_bezout_zerosum. ((exists ge_representation_real_code_bezout_zerosumfirst ge_representation_imaginary_code_bezout_zerosumfirst. (((gr_first_product_bezout_zero) = ((ge_representation_real_code_bezout_zerosumfirst) + (ge_representation_imaginary_code_bezout_zerosumfirst)) * S ((ge_representation_real_code_bezout_zerosumfirst) + (ge_representation_imaginary_code_bezout_zerosumfirst)) + ((ge_representation_imaginary_code_bezout_zerosumfirst) + (ge_representation_imaginary_code_bezout_zerosumfirst))) /\ ((exists ge_balance_positive_bezout_zerosumfirstreal ge_balance_negative_bezout_zerosumfirstreal. (((((ge_representation_real_code_bezout_zerosumfirst) = 2 * (ge_balance_positive_bezout_zerosumfirstreal) /\ (ge_balance_negative_bezout_zerosumfirstreal) = 0) \/ exists ge_signed_half_bezout_zerosumfirstrealdecode. (((ge_representation_real_code_bezout_zerosumfirst) = 2 * ge_signed_half_bezout_zerosumfirstrealdecode + 1 /\ (ge_balance_positive_bezout_zerosumfirstreal) = 0) /\ (ge_balance_negative_bezout_zerosumfirstreal) = S ge_signed_half_bezout_zerosumfirstrealdecode))) /\ ((ge_first_rp_bezout_zerosum) + ge_balance_negative_bezout_zerosumfirstreal = (ge_first_rn_bezout_zerosum) + ge_balance_positive_bezout_zerosumfirstreal))) /\ (exists ge_balance_positive_bezout_zerosumfirstimaginary ge_balance_negative_bezout_zerosumfirstimaginary. (((((ge_representation_imaginary_code_bezout_zerosumfirst) = 2 * (ge_balance_positive_bezout_zerosumfirstimaginary) /\ (ge_balance_negative_bezout_zerosumfirstimaginary) = 0) \/ exists ge_signed_half_bezout_zerosumfirstimaginarydecode. (((ge_representation_imaginary_code_bezout_zerosumfirst) = 2 * ge_signed_half_bezout_zerosumfirstimaginarydecode + 1 /\ (ge_balance_positive_bezout_zerosumfirstimaginary) = 0) /\ (ge_balance_negative_bezout_zerosumfirstimaginary) = S ge_signed_half_bezout_zerosumfirstimaginarydecode))) /\ ((ge_first_ip_bezout_zerosum) + ge_balance_negative_bezout_zerosumfirstimaginary = (ge_first_in_bezout_zerosum) + ge_balance_positive_bezout_zerosumfirstimaginary)))))) /\ ((exists ge_representation_real_code_bezout_zerosumsecond ge_representation_imaginary_code_bezout_zerosumsecond. (((gr_second_product_bezout_zero) = ((ge_representation_real_code_bezout_zerosumsecond) + (ge_representation_imaginary_code_bezout_zerosumsecond)) * S ((ge_representation_real_code_bezout_zerosumsecond) + (ge_representation_imaginary_code_bezout_zerosumsecond)) + ((ge_representation_imaginary_code_bezout_zerosumsecond) + (ge_representation_imaginary_code_bezout_zerosumsecond))) /\ ((exists ge_balance_positive_bezout_zerosumsecondreal ge_balance_negative_bezout_zerosumsecondreal. (((((ge_representation_real_code_bezout_zerosumsecond) = 2 * (ge_balance_positive_bezout_zerosumsecondreal) /\ (ge_balance_negative_bezout_zerosumsecondreal) = 0) \/ exists ge_signed_half_bezout_zerosumsecondrealdecode. (((ge_representation_real_code_bezout_zerosumsecond) = 2 * ge_signed_half_bezout_zerosumsecondrealdecode + 1 /\ (ge_balance_positive_bezout_zerosumsecondreal) = 0) /\ (ge_balance_negative_bezout_zerosumsecondreal) = S ge_signed_half_bezout_zerosumsecondrealdecode))) /\ ((ge_second_rp_bezout_zerosum) + ge_balance_negative_bezout_zerosumsecondreal = (ge_second_rn_bezout_zerosum) + ge_balance_positive_bezout_zerosumsecondreal))) /\ (exists ge_balance_positive_bezout_zerosumsecondimaginary ge_balance_negative_bezout_zerosumsecondimaginary. (((((ge_representation_imaginary_code_bezout_zerosumsecond) = 2 * (ge_balance_positive_bezout_zerosumsecondimaginary) /\ (ge_balance_negative_bezout_zerosumsecondimaginary) = 0) \/ exists ge_signed_half_bezout_zerosumsecondimaginarydecode. (((ge_representation_imaginary_code_bezout_zerosumsecond) = 2 * ge_signed_half_bezout_zerosumsecondimaginarydecode + 1 /\ (ge_balance_positive_bezout_zerosumsecondimaginary) = 0) /\ (ge_balance_negative_bezout_zerosumsecondimaginary) = S ge_signed_half_bezout_zerosumsecondimaginarydecode))) /\ ((ge_second_ip_bezout_zerosum) + ge_balance_negative_bezout_zerosumsecondimaginary = (ge_second_in_bezout_zerosum) + ge_balance_positive_bezout_zerosumsecondimaginary)))))) /\ (exists ge_representation_real_code_bezout_zerosumoutput ge_representation_imaginary_code_bezout_zerosumoutput. (((a) = ((ge_representation_real_code_bezout_zerosumoutput) + (ge_representation_imaginary_code_bezout_zerosumoutput)) * S ((ge_representation_real_code_bezout_zerosumoutput) + (ge_representation_imaginary_code_bezout_zerosumoutput)) + ((ge_representation_imaginary_code_bezout_zerosumoutput) + (ge_representation_imaginary_code_bezout_zerosumoutput))) /\ ((exists ge_balance_positive_bezout_zerosumoutputreal ge_balance_negative_bezout_zerosumoutputreal. (((((ge_representation_real_code_bezout_zerosumoutput) = 2 * (ge_balance_positive_bezout_zerosumoutputreal) /\ (ge_balance_negative_bezout_zerosumoutputreal) = 0) \/ exists ge_signed_half_bezout_zerosumoutputrealdecode. (((ge_representation_real_code_bezout_zerosumoutput) = 2 * ge_signed_half_bezout_zerosumoutputrealdecode + 1 /\ (ge_balance_positive_bezout_zerosumoutputreal) = 0) /\ (ge_balance_negative_bezout_zerosumoutputreal) = S ge_signed_half_bezout_zerosumoutputrealdecode))) /\ ((((ge_first_rp_bezout_zerosum) + (ge_second_rp_bezout_zerosum))) + ge_balance_negative_bezout_zerosumoutputreal = (((ge_first_rn_bezout_zerosum) + (ge_second_rn_bezout_zerosum))) + ge_balance_positive_bezout_zerosumoutputreal))) /\ (exists ge_balance_positive_bezout_zerosumoutputimaginary ge_balance_negative_bezout_zerosumoutputimaginary. (((((ge_representation_imaginary_code_bezout_zerosumoutput) = 2 * (ge_balance_positive_bezout_zerosumoutputimaginary) /\ (ge_balance_negative_bezout_zerosumoutputimaginary) = 0) \/ exists ge_signed_half_bezout_zerosumoutputimaginarydecode. (((ge_representation_imaginary_code_bezout_zerosumoutput) = 2 * ge_signed_half_bezout_zerosumoutputimaginarydecode + 1 /\ (ge_balance_positive_bezout_zerosumoutputimaginary) = 0) /\ (ge_balance_negative_bezout_zerosumoutputimaginary) = S ge_signed_half_bezout_zerosumoutputimaginarydecode))) /\ ((((ge_first_ip_bezout_zerosum) + (ge_second_ip_bezout_zerosum))) + ge_balance_negative_bezout_zerosumoutputimaginary = (((ge_first_in_bezout_zerosum) + (ge_second_in_bezout_zerosum))) + ge_balance_positive_bezout_zerosumoutputimaginary)))))))))))))