GGcd(g,a,b)

((exists gr_quotient_gaussianfactorizationfirst. (exists ge_first_rp_gaussianfactorizationfirstproduct ge_first_rn_gaussianfactorizationfirstproduct ge_first_ip_gaussianfactorizationfirstproduct ge_first_in_gaussianfactorizationfirstproduct ge_second_rp_gaussianfactorizationfirstproduct ge_second_rn_gaussianfactorizationfirstproduct ge_second_ip_gaussianfactorizationfirstproduct ge_second_in_gaussianfactorizationfirstproduct. ((exists ge_representation_real_code_gaussianfactorizationfirstproductfirst ge_representation_imaginary_code_gaussianfactorizationfirstproductfirst. ((((g)) = ((ge_representation_real_code_gaussianfactorizationfirstproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirstproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationfirstproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirstproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationfirstproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirstproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationfirstproductfirstreal ge_balance_negative_gaussianfactorizationfirstproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationfirstproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirstproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationfirstproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationfirstproductfirst) = 2 * ge_signed_half_gaussianfactorizationfirstproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstproductfirstreal) = S ge_signed_half_gaussianfactorizationfirstproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationfirstproduct) + ge_balance_negative_gaussianfactorizationfirstproductfirstreal = (ge_first_rn_gaussianfactorizationfirstproduct) + ge_balance_positive_gaussianfactorizationfirstproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirstproductfirstimaginary ge_balance_negative_gaussianfactorizationfirstproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirstproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirstproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationfirstproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirstproductfirst) = 2 * ge_signed_half_gaussianfactorizationfirstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstproductfirstimaginary) = S ge_signed_half_gaussianfactorizationfirstproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationfirstproduct) + ge_balance_negative_gaussianfactorizationfirstproductfirstimaginary = (ge_first_in_gaussianfactorizationfirstproduct) + ge_balance_positive_gaussianfactorizationfirstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationfirstproductsecond ge_representation_imaginary_code_gaussianfactorizationfirstproductsecond. (((gr_quotient_gaussianfactorizationfirst) = ((ge_representation_real_code_gaussianfactorizationfirstproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationfirstproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationfirstproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationfirstproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationfirstproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationfirstproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationfirstproductsecondreal ge_balance_negative_gaussianfactorizationfirstproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationfirstproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationfirstproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationfirstproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationfirstproductsecond) = 2 * ge_signed_half_gaussianfactorizationfirstproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstproductsecondreal) = S ge_signed_half_gaussianfactorizationfirstproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationfirstproduct) + ge_balance_negative_gaussianfactorizationfirstproductsecondreal = (ge_second_rn_gaussianfactorizationfirstproduct) + ge_balance_positive_gaussianfactorizationfirstproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirstproductsecondimaginary ge_balance_negative_gaussianfactorizationfirstproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirstproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationfirstproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationfirstproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirstproductsecond) = 2 * ge_signed_half_gaussianfactorizationfirstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstproductsecondimaginary) = S ge_signed_half_gaussianfactorizationfirstproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationfirstproduct) + ge_balance_negative_gaussianfactorizationfirstproductsecondimaginary = (ge_second_in_gaussianfactorizationfirstproduct) + ge_balance_positive_gaussianfactorizationfirstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationfirstproductoutput ge_representation_imaginary_code_gaussianfactorizationfirstproductoutput. ((((a)) = ((ge_representation_real_code_gaussianfactorizationfirstproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirstproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationfirstproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirstproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationfirstproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirstproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationfirstproductoutputreal ge_balance_negative_gaussianfactorizationfirstproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationfirstproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirstproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationfirstproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationfirstproductoutput) = 2 * ge_signed_half_gaussianfactorizationfirstproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstproductoutputreal) = S ge_signed_half_gaussianfactorizationfirstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirstproduct) * (ge_second_rp_gaussianfactorizationfirstproduct))) + (((ge_first_rn_gaussianfactorizationfirstproduct) * (ge_second_rn_gaussianfactorizationfirstproduct))))) + (((((ge_first_ip_gaussianfactorizationfirstproduct) * (ge_second_in_gaussianfactorizationfirstproduct))) + (((ge_first_in_gaussianfactorizationfirstproduct) * (ge_second_ip_gaussianfactorizationfirstproduct))))))) + ge_balance_negative_gaussianfactorizationfirstproductoutputreal = (((((((ge_first_rp_gaussianfactorizationfirstproduct) * (ge_second_rn_gaussianfactorizationfirstproduct))) + (((ge_first_rn_gaussianfactorizationfirstproduct) * (ge_second_rp_gaussianfactorizationfirstproduct))))) + (((((ge_first_ip_gaussianfactorizationfirstproduct) * (ge_second_ip_gaussianfactorizationfirstproduct))) + (((ge_first_in_gaussianfactorizationfirstproduct) * (ge_second_in_gaussianfactorizationfirstproduct))))))) + ge_balance_positive_gaussianfactorizationfirstproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirstproductoutputimaginary ge_balance_negative_gaussianfactorizationfirstproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirstproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirstproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationfirstproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirstproductoutput) = 2 * ge_signed_half_gaussianfactorizationfirstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstproductoutputimaginary) = S ge_signed_half_gaussianfactorizationfirstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirstproduct) * (ge_second_ip_gaussianfactorizationfirstproduct))) + (((ge_first_rn_gaussianfactorizationfirstproduct) * (ge_second_in_gaussianfactorizationfirstproduct))))) + (((((ge_first_ip_gaussianfactorizationfirstproduct) * (ge_second_rp_gaussianfactorizationfirstproduct))) + (((ge_first_in_gaussianfactorizationfirstproduct) * (ge_second_rn_gaussianfactorizationfirstproduct))))))) + ge_balance_negative_gaussianfactorizationfirstproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationfirstproduct) * (ge_second_in_gaussianfactorizationfirstproduct))) + (((ge_first_rn_gaussianfactorizationfirstproduct) * (ge_second_ip_gaussianfactorizationfirstproduct))))) + (((((ge_first_ip_gaussianfactorizationfirstproduct) * (ge_second_rn_gaussianfactorizationfirstproduct))) + (((ge_first_in_gaussianfactorizationfirstproduct) * (ge_second_rp_gaussianfactorizationfirstproduct))))))) + ge_balance_positive_gaussianfactorizationfirstproductoutputimaginary)))))))))) /\ ((exists gr_quotient_gaussianfactorizationsecond. (exists ge_first_rp_gaussianfactorizationsecondproduct ge_first_rn_gaussianfactorizationsecondproduct ge_first_ip_gaussianfactorizationsecondproduct ge_first_in_gaussianfactorizationsecondproduct ge_second_rp_gaussianfactorizationsecondproduct ge_second_rn_gaussianfactorizationsecondproduct ge_second_ip_gaussianfactorizationsecondproduct ge_second_in_gaussianfactorizationsecondproduct. ((exists ge_representation_real_code_gaussianfactorizationsecondproductfirst ge_representation_imaginary_code_gaussianfactorizationsecondproductfirst. ((((g)) = ((ge_representation_real_code_gaussianfactorizationsecondproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecondproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationsecondproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecondproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationsecondproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecondproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationsecondproductfirstreal ge_balance_negative_gaussianfactorizationsecondproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationsecondproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecondproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationsecondproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationsecondproductfirst) = 2 * ge_signed_half_gaussianfactorizationsecondproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondproductfirstreal) = S ge_signed_half_gaussianfactorizationsecondproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationsecondproduct) + ge_balance_negative_gaussianfactorizationsecondproductfirstreal = (ge_first_rn_gaussianfactorizationsecondproduct) + ge_balance_positive_gaussianfactorizationsecondproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecondproductfirstimaginary ge_balance_negative_gaussianfactorizationsecondproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecondproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecondproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationsecondproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecondproductfirst) = 2 * ge_signed_half_gaussianfactorizationsecondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondproductfirstimaginary) = S ge_signed_half_gaussianfactorizationsecondproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationsecondproduct) + ge_balance_negative_gaussianfactorizationsecondproductfirstimaginary = (ge_first_in_gaussianfactorizationsecondproduct) + ge_balance_positive_gaussianfactorizationsecondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationsecondproductsecond ge_representation_imaginary_code_gaussianfactorizationsecondproductsecond. (((gr_quotient_gaussianfactorizationsecond) = ((ge_representation_real_code_gaussianfactorizationsecondproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationsecondproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationsecondproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationsecondproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationsecondproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationsecondproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationsecondproductsecondreal ge_balance_negative_gaussianfactorizationsecondproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationsecondproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationsecondproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationsecondproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationsecondproductsecond) = 2 * ge_signed_half_gaussianfactorizationsecondproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondproductsecondreal) = S ge_signed_half_gaussianfactorizationsecondproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationsecondproduct) + ge_balance_negative_gaussianfactorizationsecondproductsecondreal = (ge_second_rn_gaussianfactorizationsecondproduct) + ge_balance_positive_gaussianfactorizationsecondproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecondproductsecondimaginary ge_balance_negative_gaussianfactorizationsecondproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecondproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationsecondproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationsecondproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecondproductsecond) = 2 * ge_signed_half_gaussianfactorizationsecondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondproductsecondimaginary) = S ge_signed_half_gaussianfactorizationsecondproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationsecondproduct) + ge_balance_negative_gaussianfactorizationsecondproductsecondimaginary = (ge_second_in_gaussianfactorizationsecondproduct) + ge_balance_positive_gaussianfactorizationsecondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationsecondproductoutput ge_representation_imaginary_code_gaussianfactorizationsecondproductoutput. ((((b)) = ((ge_representation_real_code_gaussianfactorizationsecondproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecondproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationsecondproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecondproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationsecondproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecondproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationsecondproductoutputreal ge_balance_negative_gaussianfactorizationsecondproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationsecondproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecondproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationsecondproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationsecondproductoutput) = 2 * ge_signed_half_gaussianfactorizationsecondproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondproductoutputreal) = S ge_signed_half_gaussianfactorizationsecondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecondproduct) * (ge_second_rp_gaussianfactorizationsecondproduct))) + (((ge_first_rn_gaussianfactorizationsecondproduct) * (ge_second_rn_gaussianfactorizationsecondproduct))))) + (((((ge_first_ip_gaussianfactorizationsecondproduct) * (ge_second_in_gaussianfactorizationsecondproduct))) + (((ge_first_in_gaussianfactorizationsecondproduct) * (ge_second_ip_gaussianfactorizationsecondproduct))))))) + ge_balance_negative_gaussianfactorizationsecondproductoutputreal = (((((((ge_first_rp_gaussianfactorizationsecondproduct) * (ge_second_rn_gaussianfactorizationsecondproduct))) + (((ge_first_rn_gaussianfactorizationsecondproduct) * (ge_second_rp_gaussianfactorizationsecondproduct))))) + (((((ge_first_ip_gaussianfactorizationsecondproduct) * (ge_second_ip_gaussianfactorizationsecondproduct))) + (((ge_first_in_gaussianfactorizationsecondproduct) * (ge_second_in_gaussianfactorizationsecondproduct))))))) + ge_balance_positive_gaussianfactorizationsecondproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecondproductoutputimaginary ge_balance_negative_gaussianfactorizationsecondproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecondproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecondproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationsecondproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecondproductoutput) = 2 * ge_signed_half_gaussianfactorizationsecondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondproductoutputimaginary) = S ge_signed_half_gaussianfactorizationsecondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecondproduct) * (ge_second_ip_gaussianfactorizationsecondproduct))) + (((ge_first_rn_gaussianfactorizationsecondproduct) * (ge_second_in_gaussianfactorizationsecondproduct))))) + (((((ge_first_ip_gaussianfactorizationsecondproduct) * (ge_second_rp_gaussianfactorizationsecondproduct))) + (((ge_first_in_gaussianfactorizationsecondproduct) * (ge_second_rn_gaussianfactorizationsecondproduct))))))) + ge_balance_negative_gaussianfactorizationsecondproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationsecondproduct) * (ge_second_in_gaussianfactorizationsecondproduct))) + (((ge_first_rn_gaussianfactorizationsecondproduct) * (ge_second_ip_gaussianfactorizationsecondproduct))))) + (((((ge_first_ip_gaussianfactorizationsecondproduct) * (ge_second_rn_gaussianfactorizationsecondproduct))) + (((ge_first_in_gaussianfactorizationsecondproduct) * (ge_second_rp_gaussianfactorizationsecondproduct))))))) + ge_balance_positive_gaussianfactorizationsecondproductoutputimaginary)))))))))) /\ (forall gr_common_divisor_gaussianfactorization. (exists gr_quotient_gaussianfactorizationcommon_first. (exists ge_first_rp_gaussianfactorizationcommon_firstproduct ge_first_rn_gaussianfactorizationcommon_firstproduct ge_first_ip_gaussianfactorizationcommon_firstproduct ge_first_in_gaussianfactorizationcommon_firstproduct ge_second_rp_gaussianfactorizationcommon_firstproduct ge_second_rn_gaussianfactorizationcommon_firstproduct ge_second_ip_gaussianfactorizationcommon_firstproduct ge_second_in_gaussianfactorizationcommon_firstproduct. ((exists ge_representation_real_code_gaussianfactorizationcommon_firstproductfirst ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductfirst. (((gr_common_divisor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationcommon_firstproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationcommon_firstproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationcommon_firstproductfirstreal ge_balance_negative_gaussianfactorizationcommon_firstproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationcommon_firstproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationcommon_firstproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_firstproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationcommon_firstproductfirst) = 2 * ge_signed_half_gaussianfactorizationcommon_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_firstproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductfirstreal) = S ge_signed_half_gaussianfactorizationcommon_firstproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationcommon_firstproduct) + ge_balance_negative_gaussianfactorizationcommon_firstproductfirstreal = (ge_first_rn_gaussianfactorizationcommon_firstproduct) + ge_balance_positive_gaussianfactorizationcommon_firstproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationcommon_firstproductfirstimaginary ge_balance_negative_gaussianfactorizationcommon_firstproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationcommon_firstproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductfirst) = 2 * ge_signed_half_gaussianfactorizationcommon_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductfirstimaginary) = S ge_signed_half_gaussianfactorizationcommon_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationcommon_firstproduct) + ge_balance_negative_gaussianfactorizationcommon_firstproductfirstimaginary = (ge_first_in_gaussianfactorizationcommon_firstproduct) + ge_balance_positive_gaussianfactorizationcommon_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationcommon_firstproductsecond ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductsecond. (((gr_quotient_gaussianfactorizationcommon_first) = ((ge_representation_real_code_gaussianfactorizationcommon_firstproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationcommon_firstproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationcommon_firstproductsecondreal ge_balance_negative_gaussianfactorizationcommon_firstproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationcommon_firstproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationcommon_firstproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_firstproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationcommon_firstproductsecond) = 2 * ge_signed_half_gaussianfactorizationcommon_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_firstproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductsecondreal) = S ge_signed_half_gaussianfactorizationcommon_firstproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationcommon_firstproduct) + ge_balance_negative_gaussianfactorizationcommon_firstproductsecondreal = (ge_second_rn_gaussianfactorizationcommon_firstproduct) + ge_balance_positive_gaussianfactorizationcommon_firstproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationcommon_firstproductsecondimaginary ge_balance_negative_gaussianfactorizationcommon_firstproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationcommon_firstproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductsecond) = 2 * ge_signed_half_gaussianfactorizationcommon_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductsecondimaginary) = S ge_signed_half_gaussianfactorizationcommon_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationcommon_firstproduct) + ge_balance_negative_gaussianfactorizationcommon_firstproductsecondimaginary = (ge_second_in_gaussianfactorizationcommon_firstproduct) + ge_balance_positive_gaussianfactorizationcommon_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationcommon_firstproductoutput ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductoutput. ((((a)) = ((ge_representation_real_code_gaussianfactorizationcommon_firstproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationcommon_firstproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationcommon_firstproductoutputreal ge_balance_negative_gaussianfactorizationcommon_firstproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationcommon_firstproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationcommon_firstproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_firstproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationcommon_firstproductoutput) = 2 * ge_signed_half_gaussianfactorizationcommon_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_firstproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductoutputreal) = S ge_signed_half_gaussianfactorizationcommon_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationcommon_firstproduct) * (ge_second_rp_gaussianfactorizationcommon_firstproduct))) + (((ge_first_rn_gaussianfactorizationcommon_firstproduct) * (ge_second_rn_gaussianfactorizationcommon_firstproduct))))) + (((((ge_first_ip_gaussianfactorizationcommon_firstproduct) * (ge_second_in_gaussianfactorizationcommon_firstproduct))) + (((ge_first_in_gaussianfactorizationcommon_firstproduct) * (ge_second_ip_gaussianfactorizationcommon_firstproduct))))))) + ge_balance_negative_gaussianfactorizationcommon_firstproductoutputreal = (((((((ge_first_rp_gaussianfactorizationcommon_firstproduct) * (ge_second_rn_gaussianfactorizationcommon_firstproduct))) + (((ge_first_rn_gaussianfactorizationcommon_firstproduct) * (ge_second_rp_gaussianfactorizationcommon_firstproduct))))) + (((((ge_first_ip_gaussianfactorizationcommon_firstproduct) * (ge_second_ip_gaussianfactorizationcommon_firstproduct))) + (((ge_first_in_gaussianfactorizationcommon_firstproduct) * (ge_second_in_gaussianfactorizationcommon_firstproduct))))))) + ge_balance_positive_gaussianfactorizationcommon_firstproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationcommon_firstproductoutputimaginary ge_balance_negative_gaussianfactorizationcommon_firstproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationcommon_firstproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationcommon_firstproductoutput) = 2 * ge_signed_half_gaussianfactorizationcommon_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_firstproductoutputimaginary) = S ge_signed_half_gaussianfactorizationcommon_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationcommon_firstproduct) * (ge_second_ip_gaussianfactorizationcommon_firstproduct))) + (((ge_first_rn_gaussianfactorizationcommon_firstproduct) * (ge_second_in_gaussianfactorizationcommon_firstproduct))))) + (((((ge_first_ip_gaussianfactorizationcommon_firstproduct) * (ge_second_rp_gaussianfactorizationcommon_firstproduct))) + (((ge_first_in_gaussianfactorizationcommon_firstproduct) * (ge_second_rn_gaussianfactorizationcommon_firstproduct))))))) + ge_balance_negative_gaussianfactorizationcommon_firstproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationcommon_firstproduct) * (ge_second_in_gaussianfactorizationcommon_firstproduct))) + (((ge_first_rn_gaussianfactorizationcommon_firstproduct) * (ge_second_ip_gaussianfactorizationcommon_firstproduct))))) + (((((ge_first_ip_gaussianfactorizationcommon_firstproduct) * (ge_second_rn_gaussianfactorizationcommon_firstproduct))) + (((ge_first_in_gaussianfactorizationcommon_firstproduct) * (ge_second_rp_gaussianfactorizationcommon_firstproduct))))))) + ge_balance_positive_gaussianfactorizationcommon_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_gaussianfactorizationcommon_second. (exists ge_first_rp_gaussianfactorizationcommon_secondproduct ge_first_rn_gaussianfactorizationcommon_secondproduct ge_first_ip_gaussianfactorizationcommon_secondproduct ge_first_in_gaussianfactorizationcommon_secondproduct ge_second_rp_gaussianfactorizationcommon_secondproduct ge_second_rn_gaussianfactorizationcommon_secondproduct ge_second_ip_gaussianfactorizationcommon_secondproduct ge_second_in_gaussianfactorizationcommon_secondproduct. ((exists ge_representation_real_code_gaussianfactorizationcommon_secondproductfirst ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductfirst. (((gr_common_divisor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationcommon_secondproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationcommon_secondproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationcommon_secondproductfirstreal ge_balance_negative_gaussianfactorizationcommon_secondproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationcommon_secondproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationcommon_secondproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_secondproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationcommon_secondproductfirst) = 2 * ge_signed_half_gaussianfactorizationcommon_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_secondproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductfirstreal) = S ge_signed_half_gaussianfactorizationcommon_secondproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationcommon_secondproduct) + ge_balance_negative_gaussianfactorizationcommon_secondproductfirstreal = (ge_first_rn_gaussianfactorizationcommon_secondproduct) + ge_balance_positive_gaussianfactorizationcommon_secondproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationcommon_secondproductfirstimaginary ge_balance_negative_gaussianfactorizationcommon_secondproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationcommon_secondproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductfirst) = 2 * ge_signed_half_gaussianfactorizationcommon_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductfirstimaginary) = S ge_signed_half_gaussianfactorizationcommon_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationcommon_secondproduct) + ge_balance_negative_gaussianfactorizationcommon_secondproductfirstimaginary = (ge_first_in_gaussianfactorizationcommon_secondproduct) + ge_balance_positive_gaussianfactorizationcommon_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationcommon_secondproductsecond ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductsecond. (((gr_quotient_gaussianfactorizationcommon_second) = ((ge_representation_real_code_gaussianfactorizationcommon_secondproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationcommon_secondproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationcommon_secondproductsecondreal ge_balance_negative_gaussianfactorizationcommon_secondproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationcommon_secondproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationcommon_secondproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_secondproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationcommon_secondproductsecond) = 2 * ge_signed_half_gaussianfactorizationcommon_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_secondproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductsecondreal) = S ge_signed_half_gaussianfactorizationcommon_secondproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationcommon_secondproduct) + ge_balance_negative_gaussianfactorizationcommon_secondproductsecondreal = (ge_second_rn_gaussianfactorizationcommon_secondproduct) + ge_balance_positive_gaussianfactorizationcommon_secondproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationcommon_secondproductsecondimaginary ge_balance_negative_gaussianfactorizationcommon_secondproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationcommon_secondproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductsecond) = 2 * ge_signed_half_gaussianfactorizationcommon_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductsecondimaginary) = S ge_signed_half_gaussianfactorizationcommon_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationcommon_secondproduct) + ge_balance_negative_gaussianfactorizationcommon_secondproductsecondimaginary = (ge_second_in_gaussianfactorizationcommon_secondproduct) + ge_balance_positive_gaussianfactorizationcommon_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationcommon_secondproductoutput ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductoutput. ((((b)) = ((ge_representation_real_code_gaussianfactorizationcommon_secondproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationcommon_secondproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationcommon_secondproductoutputreal ge_balance_negative_gaussianfactorizationcommon_secondproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationcommon_secondproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationcommon_secondproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_secondproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationcommon_secondproductoutput) = 2 * ge_signed_half_gaussianfactorizationcommon_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_secondproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductoutputreal) = S ge_signed_half_gaussianfactorizationcommon_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationcommon_secondproduct) * (ge_second_rp_gaussianfactorizationcommon_secondproduct))) + (((ge_first_rn_gaussianfactorizationcommon_secondproduct) * (ge_second_rn_gaussianfactorizationcommon_secondproduct))))) + (((((ge_first_ip_gaussianfactorizationcommon_secondproduct) * (ge_second_in_gaussianfactorizationcommon_secondproduct))) + (((ge_first_in_gaussianfactorizationcommon_secondproduct) * (ge_second_ip_gaussianfactorizationcommon_secondproduct))))))) + ge_balance_negative_gaussianfactorizationcommon_secondproductoutputreal = (((((((ge_first_rp_gaussianfactorizationcommon_secondproduct) * (ge_second_rn_gaussianfactorizationcommon_secondproduct))) + (((ge_first_rn_gaussianfactorizationcommon_secondproduct) * (ge_second_rp_gaussianfactorizationcommon_secondproduct))))) + (((((ge_first_ip_gaussianfactorizationcommon_secondproduct) * (ge_second_ip_gaussianfactorizationcommon_secondproduct))) + (((ge_first_in_gaussianfactorizationcommon_secondproduct) * (ge_second_in_gaussianfactorizationcommon_secondproduct))))))) + ge_balance_positive_gaussianfactorizationcommon_secondproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationcommon_secondproductoutputimaginary ge_balance_negative_gaussianfactorizationcommon_secondproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationcommon_secondproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationcommon_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationcommon_secondproductoutput) = 2 * ge_signed_half_gaussianfactorizationcommon_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationcommon_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationcommon_secondproductoutputimaginary) = S ge_signed_half_gaussianfactorizationcommon_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationcommon_secondproduct) * (ge_second_ip_gaussianfactorizationcommon_secondproduct))) + (((ge_first_rn_gaussianfactorizationcommon_secondproduct) * (ge_second_in_gaussianfactorizationcommon_secondproduct))))) + (((((ge_first_ip_gaussianfactorizationcommon_secondproduct) * (ge_second_rp_gaussianfactorizationcommon_secondproduct))) + (((ge_first_in_gaussianfactorizationcommon_secondproduct) * (ge_second_rn_gaussianfactorizationcommon_secondproduct))))))) + ge_balance_negative_gaussianfactorizationcommon_secondproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationcommon_secondproduct) * (ge_second_in_gaussianfactorizationcommon_secondproduct))) + (((ge_first_rn_gaussianfactorizationcommon_secondproduct) * (ge_second_ip_gaussianfactorizationcommon_secondproduct))))) + (((((ge_first_ip_gaussianfactorizationcommon_secondproduct) * (ge_second_rn_gaussianfactorizationcommon_secondproduct))) + (((ge_first_in_gaussianfactorizationcommon_secondproduct) * (ge_second_rp_gaussianfactorizationcommon_secondproduct))))))) + ge_balance_positive_gaussianfactorizationcommon_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_gaussianfactorizationgreatest. (exists ge_first_rp_gaussianfactorizationgreatestproduct ge_first_rn_gaussianfactorizationgreatestproduct ge_first_ip_gaussianfactorizationgreatestproduct ge_first_in_gaussianfactorizationgreatestproduct ge_second_rp_gaussianfactorizationgreatestproduct ge_second_rn_gaussianfactorizationgreatestproduct ge_second_ip_gaussianfactorizationgreatestproduct ge_second_in_gaussianfactorizationgreatestproduct. ((exists ge_representation_real_code_gaussianfactorizationgreatestproductfirst ge_representation_imaginary_code_gaussianfactorizationgreatestproductfirst. (((gr_common_divisor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationgreatestproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationgreatestproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationgreatestproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationgreatestproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationgreatestproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationgreatestproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationgreatestproductfirstreal ge_balance_negative_gaussianfactorizationgreatestproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationgreatestproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationgreatestproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationgreatestproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationgreatestproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationgreatestproductfirst) = 2 * ge_signed_half_gaussianfactorizationgreatestproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationgreatestproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationgreatestproductfirstreal) = S ge_signed_half_gaussianfactorizationgreatestproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationgreatestproduct) + ge_balance_negative_gaussianfactorizationgreatestproductfirstreal = (ge_first_rn_gaussianfactorizationgreatestproduct) + ge_balance_positive_gaussianfactorizationgreatestproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationgreatestproductfirstimaginary ge_balance_negative_gaussianfactorizationgreatestproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationgreatestproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationgreatestproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationgreatestproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationgreatestproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationgreatestproductfirst) = 2 * ge_signed_half_gaussianfactorizationgreatestproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationgreatestproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationgreatestproductfirstimaginary) = S ge_signed_half_gaussianfactorizationgreatestproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationgreatestproduct) + ge_balance_negative_gaussianfactorizationgreatestproductfirstimaginary = (ge_first_in_gaussianfactorizationgreatestproduct) + ge_balance_positive_gaussianfactorizationgreatestproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationgreatestproductsecond ge_representation_imaginary_code_gaussianfactorizationgreatestproductsecond. (((gr_quotient_gaussianfactorizationgreatest) = ((ge_representation_real_code_gaussianfactorizationgreatestproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationgreatestproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationgreatestproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationgreatestproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationgreatestproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationgreatestproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationgreatestproductsecondreal ge_balance_negative_gaussianfactorizationgreatestproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationgreatestproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationgreatestproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationgreatestproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationgreatestproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationgreatestproductsecond) = 2 * ge_signed_half_gaussianfactorizationgreatestproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationgreatestproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationgreatestproductsecondreal) = S ge_signed_half_gaussianfactorizationgreatestproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationgreatestproduct) + ge_balance_negative_gaussianfactorizationgreatestproductsecondreal = (ge_second_rn_gaussianfactorizationgreatestproduct) + ge_balance_positive_gaussianfactorizationgreatestproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationgreatestproductsecondimaginary ge_balance_negative_gaussianfactorizationgreatestproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationgreatestproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationgreatestproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationgreatestproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationgreatestproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationgreatestproductsecond) = 2 * ge_signed_half_gaussianfactorizationgreatestproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationgreatestproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationgreatestproductsecondimaginary) = S ge_signed_half_gaussianfactorizationgreatestproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationgreatestproduct) + ge_balance_negative_gaussianfactorizationgreatestproductsecondimaginary = (ge_second_in_gaussianfactorizationgreatestproduct) + ge_balance_positive_gaussianfactorizationgreatestproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationgreatestproductoutput ge_representation_imaginary_code_gaussianfactorizationgreatestproductoutput. ((((g)) = ((ge_representation_real_code_gaussianfactorizationgreatestproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationgreatestproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationgreatestproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationgreatestproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationgreatestproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationgreatestproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationgreatestproductoutputreal ge_balance_negative_gaussianfactorizationgreatestproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationgreatestproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationgreatestproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationgreatestproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationgreatestproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationgreatestproductoutput) = 2 * ge_signed_half_gaussianfactorizationgreatestproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationgreatestproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationgreatestproductoutputreal) = S ge_signed_half_gaussianfactorizationgreatestproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationgreatestproduct) * (ge_second_rp_gaussianfactorizationgreatestproduct))) + (((ge_first_rn_gaussianfactorizationgreatestproduct) * (ge_second_rn_gaussianfactorizationgreatestproduct))))) + (((((ge_first_ip_gaussianfactorizationgreatestproduct) * (ge_second_in_gaussianfactorizationgreatestproduct))) + (((ge_first_in_gaussianfactorizationgreatestproduct) * (ge_second_ip_gaussianfactorizationgreatestproduct))))))) + ge_balance_negative_gaussianfactorizationgreatestproductoutputreal = (((((((ge_first_rp_gaussianfactorizationgreatestproduct) * (ge_second_rn_gaussianfactorizationgreatestproduct))) + (((ge_first_rn_gaussianfactorizationgreatestproduct) * (ge_second_rp_gaussianfactorizationgreatestproduct))))) + (((((ge_first_ip_gaussianfactorizationgreatestproduct) * (ge_second_ip_gaussianfactorizationgreatestproduct))) + (((ge_first_in_gaussianfactorizationgreatestproduct) * (ge_second_in_gaussianfactorizationgreatestproduct))))))) + ge_balance_positive_gaussianfactorizationgreatestproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationgreatestproductoutputimaginary ge_balance_negative_gaussianfactorizationgreatestproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationgreatestproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationgreatestproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationgreatestproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationgreatestproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationgreatestproductoutput) = 2 * ge_signed_half_gaussianfactorizationgreatestproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationgreatestproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationgreatestproductoutputimaginary) = S ge_signed_half_gaussianfactorizationgreatestproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationgreatestproduct) * (ge_second_ip_gaussianfactorizationgreatestproduct))) + (((ge_first_rn_gaussianfactorizationgreatestproduct) * (ge_second_in_gaussianfactorizationgreatestproduct))))) + (((((ge_first_ip_gaussianfactorizationgreatestproduct) * (ge_second_rp_gaussianfactorizationgreatestproduct))) + (((ge_first_in_gaussianfactorizationgreatestproduct) * (ge_second_rn_gaussianfactorizationgreatestproduct))))))) + ge_balance_negative_gaussianfactorizationgreatestproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationgreatestproduct) * (ge_second_in_gaussianfactorizationgreatestproduct))) + (((ge_first_rn_gaussianfactorizationgreatestproduct) * (ge_second_ip_gaussianfactorizationgreatestproduct))))) + (((((ge_first_ip_gaussianfactorizationgreatestproduct) * (ge_second_rn_gaussianfactorizationgreatestproduct))) + (((ge_first_in_gaussianfactorizationgreatestproduct) * (ge_second_rp_gaussianfactorizationgreatestproduct))))))) + ge_balance_positive_gaussianfactorizationgreatestproductoutputimaginary)))))))))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.