GBezout(g,a,b,u,v)

exists gr_first_product_gaussianfactorization gr_second_product_gaussianfactorization. ((exists ge_first_rp_gaussianfactorizationfirst ge_first_rn_gaussianfactorizationfirst ge_first_ip_gaussianfactorizationfirst ge_first_in_gaussianfactorizationfirst ge_second_rp_gaussianfactorizationfirst ge_second_rn_gaussianfactorizationfirst ge_second_ip_gaussianfactorizationfirst ge_second_in_gaussianfactorizationfirst. ((exists ge_representation_real_code_gaussianfactorizationfirstfirst ge_representation_imaginary_code_gaussianfactorizationfirstfirst. ((((a)) = ((ge_representation_real_code_gaussianfactorizationfirstfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirstfirst)) * S ((ge_representation_real_code_gaussianfactorizationfirstfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirstfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationfirstfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirstfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationfirstfirstreal ge_balance_negative_gaussianfactorizationfirstfirstreal. (((((ge_representation_real_code_gaussianfactorizationfirstfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirstfirstreal) /\ (ge_balance_negative_gaussianfactorizationfirstfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationfirstfirst) = 2 * ge_signed_half_gaussianfactorizationfirstfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstfirstreal) = S ge_signed_half_gaussianfactorizationfirstfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationfirst) + ge_balance_negative_gaussianfactorizationfirstfirstreal = (ge_first_rn_gaussianfactorizationfirst) + ge_balance_positive_gaussianfactorizationfirstfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirstfirstimaginary ge_balance_negative_gaussianfactorizationfirstfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirstfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirstfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationfirstfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirstfirst) = 2 * ge_signed_half_gaussianfactorizationfirstfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstfirstimaginary) = S ge_signed_half_gaussianfactorizationfirstfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationfirst) + ge_balance_negative_gaussianfactorizationfirstfirstimaginary = (ge_first_in_gaussianfactorizationfirst) + ge_balance_positive_gaussianfactorizationfirstfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationfirstsecond ge_representation_imaginary_code_gaussianfactorizationfirstsecond. ((((u)) = ((ge_representation_real_code_gaussianfactorizationfirstsecond) + (ge_representation_imaginary_code_gaussianfactorizationfirstsecond)) * S ((ge_representation_real_code_gaussianfactorizationfirstsecond) + (ge_representation_imaginary_code_gaussianfactorizationfirstsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationfirstsecond) + (ge_representation_imaginary_code_gaussianfactorizationfirstsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationfirstsecondreal ge_balance_negative_gaussianfactorizationfirstsecondreal. (((((ge_representation_real_code_gaussianfactorizationfirstsecond) = 2 * (ge_balance_positive_gaussianfactorizationfirstsecondreal) /\ (ge_balance_negative_gaussianfactorizationfirstsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationfirstsecond) = 2 * ge_signed_half_gaussianfactorizationfirstsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstsecondreal) = S ge_signed_half_gaussianfactorizationfirstsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationfirst) + ge_balance_negative_gaussianfactorizationfirstsecondreal = (ge_second_rn_gaussianfactorizationfirst) + ge_balance_positive_gaussianfactorizationfirstsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirstsecondimaginary ge_balance_negative_gaussianfactorizationfirstsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirstsecond) = 2 * (ge_balance_positive_gaussianfactorizationfirstsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationfirstsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirstsecond) = 2 * ge_signed_half_gaussianfactorizationfirstsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstsecondimaginary) = S ge_signed_half_gaussianfactorizationfirstsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationfirst) + ge_balance_negative_gaussianfactorizationfirstsecondimaginary = (ge_second_in_gaussianfactorizationfirst) + ge_balance_positive_gaussianfactorizationfirstsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationfirstoutput ge_representation_imaginary_code_gaussianfactorizationfirstoutput. (((gr_first_product_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationfirstoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirstoutput)) * S ((ge_representation_real_code_gaussianfactorizationfirstoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirstoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationfirstoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirstoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationfirstoutputreal ge_balance_negative_gaussianfactorizationfirstoutputreal. (((((ge_representation_real_code_gaussianfactorizationfirstoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirstoutputreal) /\ (ge_balance_negative_gaussianfactorizationfirstoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationfirstoutput) = 2 * ge_signed_half_gaussianfactorizationfirstoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstoutputreal) = S ge_signed_half_gaussianfactorizationfirstoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirst) * (ge_second_rp_gaussianfactorizationfirst))) + (((ge_first_rn_gaussianfactorizationfirst) * (ge_second_rn_gaussianfactorizationfirst))))) + (((((ge_first_ip_gaussianfactorizationfirst) * (ge_second_in_gaussianfactorizationfirst))) + (((ge_first_in_gaussianfactorizationfirst) * (ge_second_ip_gaussianfactorizationfirst))))))) + ge_balance_negative_gaussianfactorizationfirstoutputreal = (((((((ge_first_rp_gaussianfactorizationfirst) * (ge_second_rn_gaussianfactorizationfirst))) + (((ge_first_rn_gaussianfactorizationfirst) * (ge_second_rp_gaussianfactorizationfirst))))) + (((((ge_first_ip_gaussianfactorizationfirst) * (ge_second_ip_gaussianfactorizationfirst))) + (((ge_first_in_gaussianfactorizationfirst) * (ge_second_in_gaussianfactorizationfirst))))))) + ge_balance_positive_gaussianfactorizationfirstoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirstoutputimaginary ge_balance_negative_gaussianfactorizationfirstoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirstoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirstoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationfirstoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirstoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirstoutput) = 2 * ge_signed_half_gaussianfactorizationfirstoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirstoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirstoutputimaginary) = S ge_signed_half_gaussianfactorizationfirstoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirst) * (ge_second_ip_gaussianfactorizationfirst))) + (((ge_first_rn_gaussianfactorizationfirst) * (ge_second_in_gaussianfactorizationfirst))))) + (((((ge_first_ip_gaussianfactorizationfirst) * (ge_second_rp_gaussianfactorizationfirst))) + (((ge_first_in_gaussianfactorizationfirst) * (ge_second_rn_gaussianfactorizationfirst))))))) + ge_balance_negative_gaussianfactorizationfirstoutputimaginary = (((((((ge_first_rp_gaussianfactorizationfirst) * (ge_second_in_gaussianfactorizationfirst))) + (((ge_first_rn_gaussianfactorizationfirst) * (ge_second_ip_gaussianfactorizationfirst))))) + (((((ge_first_ip_gaussianfactorizationfirst) * (ge_second_rn_gaussianfactorizationfirst))) + (((ge_first_in_gaussianfactorizationfirst) * (ge_second_rp_gaussianfactorizationfirst))))))) + ge_balance_positive_gaussianfactorizationfirstoutputimaginary))))))))) /\ ((exists ge_first_rp_gaussianfactorizationsecond ge_first_rn_gaussianfactorizationsecond ge_first_ip_gaussianfactorizationsecond ge_first_in_gaussianfactorizationsecond ge_second_rp_gaussianfactorizationsecond ge_second_rn_gaussianfactorizationsecond ge_second_ip_gaussianfactorizationsecond ge_second_in_gaussianfactorizationsecond. ((exists ge_representation_real_code_gaussianfactorizationsecondfirst ge_representation_imaginary_code_gaussianfactorizationsecondfirst. ((((b)) = ((ge_representation_real_code_gaussianfactorizationsecondfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecondfirst)) * S ((ge_representation_real_code_gaussianfactorizationsecondfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecondfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationsecondfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecondfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationsecondfirstreal ge_balance_negative_gaussianfactorizationsecondfirstreal. (((((ge_representation_real_code_gaussianfactorizationsecondfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecondfirstreal) /\ (ge_balance_negative_gaussianfactorizationsecondfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationsecondfirst) = 2 * ge_signed_half_gaussianfactorizationsecondfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondfirstreal) = S ge_signed_half_gaussianfactorizationsecondfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationsecond) + ge_balance_negative_gaussianfactorizationsecondfirstreal = (ge_first_rn_gaussianfactorizationsecond) + ge_balance_positive_gaussianfactorizationsecondfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecondfirstimaginary ge_balance_negative_gaussianfactorizationsecondfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecondfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecondfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationsecondfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecondfirst) = 2 * ge_signed_half_gaussianfactorizationsecondfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondfirstimaginary) = S ge_signed_half_gaussianfactorizationsecondfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationsecond) + ge_balance_negative_gaussianfactorizationsecondfirstimaginary = (ge_first_in_gaussianfactorizationsecond) + ge_balance_positive_gaussianfactorizationsecondfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationsecondsecond ge_representation_imaginary_code_gaussianfactorizationsecondsecond. ((((v)) = ((ge_representation_real_code_gaussianfactorizationsecondsecond) + (ge_representation_imaginary_code_gaussianfactorizationsecondsecond)) * S ((ge_representation_real_code_gaussianfactorizationsecondsecond) + (ge_representation_imaginary_code_gaussianfactorizationsecondsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationsecondsecond) + (ge_representation_imaginary_code_gaussianfactorizationsecondsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationsecondsecondreal ge_balance_negative_gaussianfactorizationsecondsecondreal. (((((ge_representation_real_code_gaussianfactorizationsecondsecond) = 2 * (ge_balance_positive_gaussianfactorizationsecondsecondreal) /\ (ge_balance_negative_gaussianfactorizationsecondsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationsecondsecond) = 2 * ge_signed_half_gaussianfactorizationsecondsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondsecondreal) = S ge_signed_half_gaussianfactorizationsecondsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationsecond) + ge_balance_negative_gaussianfactorizationsecondsecondreal = (ge_second_rn_gaussianfactorizationsecond) + ge_balance_positive_gaussianfactorizationsecondsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecondsecondimaginary ge_balance_negative_gaussianfactorizationsecondsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecondsecond) = 2 * (ge_balance_positive_gaussianfactorizationsecondsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationsecondsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecondsecond) = 2 * ge_signed_half_gaussianfactorizationsecondsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondsecondimaginary) = S ge_signed_half_gaussianfactorizationsecondsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationsecond) + ge_balance_negative_gaussianfactorizationsecondsecondimaginary = (ge_second_in_gaussianfactorizationsecond) + ge_balance_positive_gaussianfactorizationsecondsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationsecondoutput ge_representation_imaginary_code_gaussianfactorizationsecondoutput. (((gr_second_product_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationsecondoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecondoutput)) * S ((ge_representation_real_code_gaussianfactorizationsecondoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecondoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationsecondoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecondoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationsecondoutputreal ge_balance_negative_gaussianfactorizationsecondoutputreal. (((((ge_representation_real_code_gaussianfactorizationsecondoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecondoutputreal) /\ (ge_balance_negative_gaussianfactorizationsecondoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationsecondoutput) = 2 * ge_signed_half_gaussianfactorizationsecondoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondoutputreal) = S ge_signed_half_gaussianfactorizationsecondoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecond) * (ge_second_rp_gaussianfactorizationsecond))) + (((ge_first_rn_gaussianfactorizationsecond) * (ge_second_rn_gaussianfactorizationsecond))))) + (((((ge_first_ip_gaussianfactorizationsecond) * (ge_second_in_gaussianfactorizationsecond))) + (((ge_first_in_gaussianfactorizationsecond) * (ge_second_ip_gaussianfactorizationsecond))))))) + ge_balance_negative_gaussianfactorizationsecondoutputreal = (((((((ge_first_rp_gaussianfactorizationsecond) * (ge_second_rn_gaussianfactorizationsecond))) + (((ge_first_rn_gaussianfactorizationsecond) * (ge_second_rp_gaussianfactorizationsecond))))) + (((((ge_first_ip_gaussianfactorizationsecond) * (ge_second_ip_gaussianfactorizationsecond))) + (((ge_first_in_gaussianfactorizationsecond) * (ge_second_in_gaussianfactorizationsecond))))))) + ge_balance_positive_gaussianfactorizationsecondoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecondoutputimaginary ge_balance_negative_gaussianfactorizationsecondoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecondoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecondoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationsecondoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecondoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecondoutput) = 2 * ge_signed_half_gaussianfactorizationsecondoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecondoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecondoutputimaginary) = S ge_signed_half_gaussianfactorizationsecondoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecond) * (ge_second_ip_gaussianfactorizationsecond))) + (((ge_first_rn_gaussianfactorizationsecond) * (ge_second_in_gaussianfactorizationsecond))))) + (((((ge_first_ip_gaussianfactorizationsecond) * (ge_second_rp_gaussianfactorizationsecond))) + (((ge_first_in_gaussianfactorizationsecond) * (ge_second_rn_gaussianfactorizationsecond))))))) + ge_balance_negative_gaussianfactorizationsecondoutputimaginary = (((((((ge_first_rp_gaussianfactorizationsecond) * (ge_second_in_gaussianfactorizationsecond))) + (((ge_first_rn_gaussianfactorizationsecond) * (ge_second_ip_gaussianfactorizationsecond))))) + (((((ge_first_ip_gaussianfactorizationsecond) * (ge_second_rn_gaussianfactorizationsecond))) + (((ge_first_in_gaussianfactorizationsecond) * (ge_second_rp_gaussianfactorizationsecond))))))) + ge_balance_positive_gaussianfactorizationsecondoutputimaginary))))))))) /\ (exists ge_first_rp_gaussianfactorizationsum ge_first_rn_gaussianfactorizationsum ge_first_ip_gaussianfactorizationsum ge_first_in_gaussianfactorizationsum ge_second_rp_gaussianfactorizationsum ge_second_rn_gaussianfactorizationsum ge_second_ip_gaussianfactorizationsum ge_second_in_gaussianfactorizationsum. ((exists ge_representation_real_code_gaussianfactorizationsumfirst ge_representation_imaginary_code_gaussianfactorizationsumfirst. (((gr_first_product_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationsumfirst) + (ge_representation_imaginary_code_gaussianfactorizationsumfirst)) * S ((ge_representation_real_code_gaussianfactorizationsumfirst) + (ge_representation_imaginary_code_gaussianfactorizationsumfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationsumfirst) + (ge_representation_imaginary_code_gaussianfactorizationsumfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationsumfirstreal ge_balance_negative_gaussianfactorizationsumfirstreal. (((((ge_representation_real_code_gaussianfactorizationsumfirst) = 2 * (ge_balance_positive_gaussianfactorizationsumfirstreal) /\ (ge_balance_negative_gaussianfactorizationsumfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsumfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationsumfirst) = 2 * ge_signed_half_gaussianfactorizationsumfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsumfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsumfirstreal) = S ge_signed_half_gaussianfactorizationsumfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationsum) + ge_balance_negative_gaussianfactorizationsumfirstreal = (ge_first_rn_gaussianfactorizationsum) + ge_balance_positive_gaussianfactorizationsumfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationsumfirstimaginary ge_balance_negative_gaussianfactorizationsumfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsumfirst) = 2 * (ge_balance_positive_gaussianfactorizationsumfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationsumfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsumfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsumfirst) = 2 * ge_signed_half_gaussianfactorizationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsumfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsumfirstimaginary) = S ge_signed_half_gaussianfactorizationsumfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationsum) + ge_balance_negative_gaussianfactorizationsumfirstimaginary = (ge_first_in_gaussianfactorizationsum) + ge_balance_positive_gaussianfactorizationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationsumsecond ge_representation_imaginary_code_gaussianfactorizationsumsecond. (((gr_second_product_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationsumsecond) + (ge_representation_imaginary_code_gaussianfactorizationsumsecond)) * S ((ge_representation_real_code_gaussianfactorizationsumsecond) + (ge_representation_imaginary_code_gaussianfactorizationsumsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationsumsecond) + (ge_representation_imaginary_code_gaussianfactorizationsumsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationsumsecondreal ge_balance_negative_gaussianfactorizationsumsecondreal. (((((ge_representation_real_code_gaussianfactorizationsumsecond) = 2 * (ge_balance_positive_gaussianfactorizationsumsecondreal) /\ (ge_balance_negative_gaussianfactorizationsumsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsumsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationsumsecond) = 2 * ge_signed_half_gaussianfactorizationsumsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsumsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsumsecondreal) = S ge_signed_half_gaussianfactorizationsumsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationsum) + ge_balance_negative_gaussianfactorizationsumsecondreal = (ge_second_rn_gaussianfactorizationsum) + ge_balance_positive_gaussianfactorizationsumsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationsumsecondimaginary ge_balance_negative_gaussianfactorizationsumsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsumsecond) = 2 * (ge_balance_positive_gaussianfactorizationsumsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationsumsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsumsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsumsecond) = 2 * ge_signed_half_gaussianfactorizationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsumsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsumsecondimaginary) = S ge_signed_half_gaussianfactorizationsumsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationsum) + ge_balance_negative_gaussianfactorizationsumsecondimaginary = (ge_second_in_gaussianfactorizationsum) + ge_balance_positive_gaussianfactorizationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationsumoutput ge_representation_imaginary_code_gaussianfactorizationsumoutput. ((((g)) = ((ge_representation_real_code_gaussianfactorizationsumoutput) + (ge_representation_imaginary_code_gaussianfactorizationsumoutput)) * S ((ge_representation_real_code_gaussianfactorizationsumoutput) + (ge_representation_imaginary_code_gaussianfactorizationsumoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationsumoutput) + (ge_representation_imaginary_code_gaussianfactorizationsumoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationsumoutputreal ge_balance_negative_gaussianfactorizationsumoutputreal. (((((ge_representation_real_code_gaussianfactorizationsumoutput) = 2 * (ge_balance_positive_gaussianfactorizationsumoutputreal) /\ (ge_balance_negative_gaussianfactorizationsumoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsumoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationsumoutput) = 2 * ge_signed_half_gaussianfactorizationsumoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsumoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsumoutputreal) = S ge_signed_half_gaussianfactorizationsumoutputrealdecode))) /\ ((((ge_first_rp_gaussianfactorizationsum) + (ge_second_rp_gaussianfactorizationsum))) + ge_balance_negative_gaussianfactorizationsumoutputreal = (((ge_first_rn_gaussianfactorizationsum) + (ge_second_rn_gaussianfactorizationsum))) + ge_balance_positive_gaussianfactorizationsumoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationsumoutputimaginary ge_balance_negative_gaussianfactorizationsumoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsumoutput) = 2 * (ge_balance_positive_gaussianfactorizationsumoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationsumoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsumoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsumoutput) = 2 * ge_signed_half_gaussianfactorizationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsumoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsumoutputimaginary) = S ge_signed_half_gaussianfactorizationsumoutputimaginarydecode))) /\ ((((ge_first_ip_gaussianfactorizationsum) + (ge_second_ip_gaussianfactorizationsum))) + ge_balance_negative_gaussianfactorizationsumoutputimaginary = (((ge_first_in_gaussianfactorizationsum) + (ge_second_in_gaussianfactorizationsum))) + ge_balance_positive_gaussianfactorizationsumoutputimaginary)))))))))))

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