GPrime(z)

((exists ge_real_positive_gaussianfactorizationcarrier ge_real_negative_gaussianfactorizationcarrier ge_imaginary_positive_gaussianfactorizationcarrier ge_imaginary_negative_gaussianfactorizationcarrier. (exists ge_real_code_gaussianfactorizationcarrierdecode ge_imaginary_code_gaussianfactorizationcarrierdecode. ((((z)) = ((ge_real_code_gaussianfactorizationcarrierdecode) + (ge_imaginary_code_gaussianfactorizationcarrierdecode)) * S ((ge_real_code_gaussianfactorizationcarrierdecode) + (ge_imaginary_code_gaussianfactorizationcarrierdecode)) + ((ge_imaginary_code_gaussianfactorizationcarrierdecode) + (ge_imaginary_code_gaussianfactorizationcarrierdecode))) /\ (((((ge_real_code_gaussianfactorizationcarrierdecode) = 2 * (ge_real_positive_gaussianfactorizationcarrier) /\ (ge_real_negative_gaussianfactorizationcarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationcarrierdecode_real. (((ge_real_code_gaussianfactorizationcarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationcarrierdecode_real + 1 /\ (ge_real_positive_gaussianfactorizationcarrier) = 0) /\ (ge_real_negative_gaussianfactorizationcarrier) = S ge_signed_half_ge_gaussianfactorizationcarrierdecode_real))) /\ ((((ge_imaginary_code_gaussianfactorizationcarrierdecode) = 2 * (ge_imaginary_positive_gaussianfactorizationcarrier) /\ (ge_imaginary_negative_gaussianfactorizationcarrier) = 0) \/ exists ge_signed_half_ge_gaussianfactorizationcarrierdecode_imaginary. (((ge_imaginary_code_gaussianfactorizationcarrierdecode) = 2 * ge_signed_half_ge_gaussianfactorizationcarrierdecode_imaginary + 1 /\ (ge_imaginary_positive_gaussianfactorizationcarrier) = 0) /\ (ge_imaginary_negative_gaussianfactorizationcarrier) = S ge_signed_half_ge_gaussianfactorizationcarrierdecode_imaginary))))))) /\ ((~(((z))=0)) /\ ((~(exists gr_inverse_gaussianfactorizationnonunit. (exists ge_first_rp_gaussianfactorizationnonunitidentity ge_first_rn_gaussianfactorizationnonunitidentity ge_first_ip_gaussianfactorizationnonunitidentity ge_first_in_gaussianfactorizationnonunitidentity ge_second_rp_gaussianfactorizationnonunitidentity ge_second_rn_gaussianfactorizationnonunitidentity ge_second_ip_gaussianfactorizationnonunitidentity ge_second_in_gaussianfactorizationnonunitidentity. ((exists ge_representation_real_code_gaussianfactorizationnonunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst. ((((z)) = ((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal = (ge_first_rn_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationnonunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond. (((gr_inverse_gaussianfactorizationnonunit) = ((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal = (ge_second_rn_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationnonunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))))))) + ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))))))) + ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))))))) + ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))))))) + ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary))))))))))) /\ (forall gr_first_factor_gaussianfactorization gr_second_factor_gaussianfactorization gr_product_gaussianfactorization. (exists ge_first_rp_gaussianfactorizationproduct ge_first_rn_gaussianfactorizationproduct ge_first_ip_gaussianfactorizationproduct ge_first_in_gaussianfactorizationproduct ge_second_rp_gaussianfactorizationproduct ge_second_rn_gaussianfactorizationproduct ge_second_ip_gaussianfactorizationproduct ge_second_in_gaussianfactorizationproduct. ((exists ge_representation_real_code_gaussianfactorizationproductfirst ge_representation_imaginary_code_gaussianfactorizationproductfirst. (((gr_first_factor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationproductfirstreal ge_balance_negative_gaussianfactorizationproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationproductfirst) = 2 * ge_signed_half_gaussianfactorizationproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationproductfirstreal) = S ge_signed_half_gaussianfactorizationproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationproduct) + ge_balance_negative_gaussianfactorizationproductfirstreal = (ge_first_rn_gaussianfactorizationproduct) + ge_balance_positive_gaussianfactorizationproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationproductfirstimaginary ge_balance_negative_gaussianfactorizationproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationproductfirst) = 2 * ge_signed_half_gaussianfactorizationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationproductfirstimaginary) = S ge_signed_half_gaussianfactorizationproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationproduct) + ge_balance_negative_gaussianfactorizationproductfirstimaginary = (ge_first_in_gaussianfactorizationproduct) + ge_balance_positive_gaussianfactorizationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationproductsecond ge_representation_imaginary_code_gaussianfactorizationproductsecond. (((gr_second_factor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationproductsecondreal ge_balance_negative_gaussianfactorizationproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationproductsecond) = 2 * ge_signed_half_gaussianfactorizationproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationproductsecondreal) = S ge_signed_half_gaussianfactorizationproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationproduct) + ge_balance_negative_gaussianfactorizationproductsecondreal = (ge_second_rn_gaussianfactorizationproduct) + ge_balance_positive_gaussianfactorizationproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationproductsecondimaginary ge_balance_negative_gaussianfactorizationproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationproductsecond) = 2 * ge_signed_half_gaussianfactorizationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationproductsecondimaginary) = S ge_signed_half_gaussianfactorizationproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationproduct) + ge_balance_negative_gaussianfactorizationproductsecondimaginary = (ge_second_in_gaussianfactorizationproduct) + ge_balance_positive_gaussianfactorizationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationproductoutput ge_representation_imaginary_code_gaussianfactorizationproductoutput. (((gr_product_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationproductoutputreal ge_balance_negative_gaussianfactorizationproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationproductoutput) = 2 * ge_signed_half_gaussianfactorizationproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationproductoutputreal) = S ge_signed_half_gaussianfactorizationproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationproduct) * (ge_second_rp_gaussianfactorizationproduct))) + (((ge_first_rn_gaussianfactorizationproduct) * (ge_second_rn_gaussianfactorizationproduct))))) + (((((ge_first_ip_gaussianfactorizationproduct) * (ge_second_in_gaussianfactorizationproduct))) + (((ge_first_in_gaussianfactorizationproduct) * (ge_second_ip_gaussianfactorizationproduct))))))) + ge_balance_negative_gaussianfactorizationproductoutputreal = (((((((ge_first_rp_gaussianfactorizationproduct) * (ge_second_rn_gaussianfactorizationproduct))) + (((ge_first_rn_gaussianfactorizationproduct) * (ge_second_rp_gaussianfactorizationproduct))))) + (((((ge_first_ip_gaussianfactorizationproduct) * (ge_second_ip_gaussianfactorizationproduct))) + (((ge_first_in_gaussianfactorizationproduct) * (ge_second_in_gaussianfactorizationproduct))))))) + ge_balance_positive_gaussianfactorizationproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationproductoutputimaginary ge_balance_negative_gaussianfactorizationproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationproductoutput) = 2 * ge_signed_half_gaussianfactorizationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationproductoutputimaginary) = S ge_signed_half_gaussianfactorizationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationproduct) * (ge_second_ip_gaussianfactorizationproduct))) + (((ge_first_rn_gaussianfactorizationproduct) * (ge_second_in_gaussianfactorizationproduct))))) + (((((ge_first_ip_gaussianfactorizationproduct) * (ge_second_rp_gaussianfactorizationproduct))) + (((ge_first_in_gaussianfactorizationproduct) * (ge_second_rn_gaussianfactorizationproduct))))))) + ge_balance_negative_gaussianfactorizationproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationproduct) * (ge_second_in_gaussianfactorizationproduct))) + (((ge_first_rn_gaussianfactorizationproduct) * (ge_second_ip_gaussianfactorizationproduct))))) + (((((ge_first_ip_gaussianfactorizationproduct) * (ge_second_rn_gaussianfactorizationproduct))) + (((ge_first_in_gaussianfactorizationproduct) * (ge_second_rp_gaussianfactorizationproduct))))))) + ge_balance_positive_gaussianfactorizationproductoutputimaginary))))))))) -> (exists gr_quotient_gaussianfactorizationdivisor. (exists ge_first_rp_gaussianfactorizationdivisorproduct ge_first_rn_gaussianfactorizationdivisorproduct ge_first_ip_gaussianfactorizationdivisorproduct ge_first_in_gaussianfactorizationdivisorproduct ge_second_rp_gaussianfactorizationdivisorproduct ge_second_rn_gaussianfactorizationdivisorproduct ge_second_ip_gaussianfactorizationdivisorproduct ge_second_in_gaussianfactorizationdivisorproduct. ((exists ge_representation_real_code_gaussianfactorizationdivisorproductfirst ge_representation_imaginary_code_gaussianfactorizationdivisorproductfirst. ((((z)) = ((ge_representation_real_code_gaussianfactorizationdivisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationdivisorproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationdivisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationdivisorproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationdivisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationdivisorproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationdivisorproductfirstreal ge_balance_negative_gaussianfactorizationdivisorproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationdivisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationdivisorproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationdivisorproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationdivisorproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationdivisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationdivisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationdivisorproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationdivisorproductfirstreal) = S ge_signed_half_gaussianfactorizationdivisorproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationdivisorproduct) + ge_balance_negative_gaussianfactorizationdivisorproductfirstreal = (ge_first_rn_gaussianfactorizationdivisorproduct) + ge_balance_positive_gaussianfactorizationdivisorproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationdivisorproductfirstimaginary ge_balance_negative_gaussianfactorizationdivisorproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationdivisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationdivisorproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationdivisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationdivisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationdivisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationdivisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationdivisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationdivisorproductfirstimaginary) = S ge_signed_half_gaussianfactorizationdivisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationdivisorproduct) + ge_balance_negative_gaussianfactorizationdivisorproductfirstimaginary = (ge_first_in_gaussianfactorizationdivisorproduct) + ge_balance_positive_gaussianfactorizationdivisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationdivisorproductsecond ge_representation_imaginary_code_gaussianfactorizationdivisorproductsecond. (((gr_quotient_gaussianfactorizationdivisor) = ((ge_representation_real_code_gaussianfactorizationdivisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationdivisorproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationdivisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationdivisorproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationdivisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationdivisorproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationdivisorproductsecondreal ge_balance_negative_gaussianfactorizationdivisorproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationdivisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationdivisorproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationdivisorproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationdivisorproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationdivisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationdivisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationdivisorproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationdivisorproductsecondreal) = S ge_signed_half_gaussianfactorizationdivisorproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationdivisorproduct) + ge_balance_negative_gaussianfactorizationdivisorproductsecondreal = (ge_second_rn_gaussianfactorizationdivisorproduct) + ge_balance_positive_gaussianfactorizationdivisorproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationdivisorproductsecondimaginary ge_balance_negative_gaussianfactorizationdivisorproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationdivisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationdivisorproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationdivisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationdivisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationdivisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationdivisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationdivisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationdivisorproductsecondimaginary) = S ge_signed_half_gaussianfactorizationdivisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationdivisorproduct) + ge_balance_negative_gaussianfactorizationdivisorproductsecondimaginary = (ge_second_in_gaussianfactorizationdivisorproduct) + ge_balance_positive_gaussianfactorizationdivisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationdivisorproductoutput ge_representation_imaginary_code_gaussianfactorizationdivisorproductoutput. (((gr_product_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationdivisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationdivisorproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationdivisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationdivisorproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationdivisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationdivisorproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationdivisorproductoutputreal ge_balance_negative_gaussianfactorizationdivisorproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationdivisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationdivisorproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationdivisorproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationdivisorproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationdivisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationdivisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationdivisorproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationdivisorproductoutputreal) = S ge_signed_half_gaussianfactorizationdivisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationdivisorproduct) * (ge_second_rp_gaussianfactorizationdivisorproduct))) + (((ge_first_rn_gaussianfactorizationdivisorproduct) * (ge_second_rn_gaussianfactorizationdivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationdivisorproduct) * (ge_second_in_gaussianfactorizationdivisorproduct))) + (((ge_first_in_gaussianfactorizationdivisorproduct) * (ge_second_ip_gaussianfactorizationdivisorproduct))))))) + ge_balance_negative_gaussianfactorizationdivisorproductoutputreal = (((((((ge_first_rp_gaussianfactorizationdivisorproduct) * (ge_second_rn_gaussianfactorizationdivisorproduct))) + (((ge_first_rn_gaussianfactorizationdivisorproduct) * (ge_second_rp_gaussianfactorizationdivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationdivisorproduct) * (ge_second_ip_gaussianfactorizationdivisorproduct))) + (((ge_first_in_gaussianfactorizationdivisorproduct) * (ge_second_in_gaussianfactorizationdivisorproduct))))))) + ge_balance_positive_gaussianfactorizationdivisorproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationdivisorproductoutputimaginary ge_balance_negative_gaussianfactorizationdivisorproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationdivisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationdivisorproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationdivisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationdivisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationdivisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationdivisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationdivisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationdivisorproductoutputimaginary) = S ge_signed_half_gaussianfactorizationdivisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationdivisorproduct) * (ge_second_ip_gaussianfactorizationdivisorproduct))) + (((ge_first_rn_gaussianfactorizationdivisorproduct) * (ge_second_in_gaussianfactorizationdivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationdivisorproduct) * (ge_second_rp_gaussianfactorizationdivisorproduct))) + (((ge_first_in_gaussianfactorizationdivisorproduct) * (ge_second_rn_gaussianfactorizationdivisorproduct))))))) + ge_balance_negative_gaussianfactorizationdivisorproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationdivisorproduct) * (ge_second_in_gaussianfactorizationdivisorproduct))) + (((ge_first_rn_gaussianfactorizationdivisorproduct) * (ge_second_ip_gaussianfactorizationdivisorproduct))))) + (((((ge_first_ip_gaussianfactorizationdivisorproduct) * (ge_second_rn_gaussianfactorizationdivisorproduct))) + (((ge_first_in_gaussianfactorizationdivisorproduct) * (ge_second_rp_gaussianfactorizationdivisorproduct))))))) + ge_balance_positive_gaussianfactorizationdivisorproductoutputimaginary)))))))))) -> (exists gr_quotient_gaussianfactorizationfirst_divisor. (exists ge_first_rp_gaussianfactorizationfirst_divisorproduct ge_first_rn_gaussianfactorizationfirst_divisorproduct ge_first_ip_gaussianfactorizationfirst_divisorproduct ge_first_in_gaussianfactorizationfirst_divisorproduct ge_second_rp_gaussianfactorizationfirst_divisorproduct ge_second_rn_gaussianfactorizationfirst_divisorproduct ge_second_ip_gaussianfactorizationfirst_divisorproduct ge_second_in_gaussianfactorizationfirst_divisorproduct. ((exists ge_representation_real_code_gaussianfactorizationfirst_divisorproductfirst ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductfirst. ((((z)) = ((ge_representation_real_code_gaussianfactorizationfirst_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationfirst_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_divisorproductfirstreal ge_balance_negative_gaussianfactorizationfirst_divisorproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationfirst_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirst_divisorproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_divisorproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationfirst_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_divisorproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductfirstreal) = S ge_signed_half_gaussianfactorizationfirst_divisorproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationfirst_divisorproduct) + ge_balance_negative_gaussianfactorizationfirst_divisorproductfirstreal = (ge_first_rn_gaussianfactorizationfirst_divisorproduct) + ge_balance_positive_gaussianfactorizationfirst_divisorproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_divisorproductfirstimaginary ge_balance_negative_gaussianfactorizationfirst_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirst_divisorproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationfirst_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductfirstimaginary) = S ge_signed_half_gaussianfactorizationfirst_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationfirst_divisorproduct) + ge_balance_negative_gaussianfactorizationfirst_divisorproductfirstimaginary = (ge_first_in_gaussianfactorizationfirst_divisorproduct) + ge_balance_positive_gaussianfactorizationfirst_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationfirst_divisorproductsecond ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductsecond. (((gr_quotient_gaussianfactorizationfirst_divisor) = ((ge_representation_real_code_gaussianfactorizationfirst_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationfirst_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_divisorproductsecondreal ge_balance_negative_gaussianfactorizationfirst_divisorproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationfirst_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationfirst_divisorproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_divisorproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationfirst_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_divisorproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductsecondreal) = S ge_signed_half_gaussianfactorizationfirst_divisorproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationfirst_divisorproduct) + ge_balance_negative_gaussianfactorizationfirst_divisorproductsecondreal = (ge_second_rn_gaussianfactorizationfirst_divisorproduct) + ge_balance_positive_gaussianfactorizationfirst_divisorproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_divisorproductsecondimaginary ge_balance_negative_gaussianfactorizationfirst_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationfirst_divisorproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationfirst_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductsecondimaginary) = S ge_signed_half_gaussianfactorizationfirst_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationfirst_divisorproduct) + ge_balance_negative_gaussianfactorizationfirst_divisorproductsecondimaginary = (ge_second_in_gaussianfactorizationfirst_divisorproduct) + ge_balance_positive_gaussianfactorizationfirst_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationfirst_divisorproductoutput ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductoutput. (((gr_first_factor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationfirst_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationfirst_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_divisorproductoutputreal ge_balance_negative_gaussianfactorizationfirst_divisorproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationfirst_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirst_divisorproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_divisorproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationfirst_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_divisorproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductoutputreal) = S ge_signed_half_gaussianfactorizationfirst_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirst_divisorproduct) * (ge_second_rp_gaussianfactorizationfirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationfirst_divisorproduct) * (ge_second_rn_gaussianfactorizationfirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationfirst_divisorproduct) * (ge_second_in_gaussianfactorizationfirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationfirst_divisorproduct) * (ge_second_ip_gaussianfactorizationfirst_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationfirst_divisorproductoutputreal = (((((((ge_first_rp_gaussianfactorizationfirst_divisorproduct) * (ge_second_rn_gaussianfactorizationfirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationfirst_divisorproduct) * (ge_second_rp_gaussianfactorizationfirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationfirst_divisorproduct) * (ge_second_ip_gaussianfactorizationfirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationfirst_divisorproduct) * (ge_second_in_gaussianfactorizationfirst_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationfirst_divisorproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_divisorproductoutputimaginary ge_balance_negative_gaussianfactorizationfirst_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirst_divisorproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationfirst_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_divisorproductoutputimaginary) = S ge_signed_half_gaussianfactorizationfirst_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirst_divisorproduct) * (ge_second_ip_gaussianfactorizationfirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationfirst_divisorproduct) * (ge_second_in_gaussianfactorizationfirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationfirst_divisorproduct) * (ge_second_rp_gaussianfactorizationfirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationfirst_divisorproduct) * (ge_second_rn_gaussianfactorizationfirst_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationfirst_divisorproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationfirst_divisorproduct) * (ge_second_in_gaussianfactorizationfirst_divisorproduct))) + (((ge_first_rn_gaussianfactorizationfirst_divisorproduct) * (ge_second_ip_gaussianfactorizationfirst_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationfirst_divisorproduct) * (ge_second_rn_gaussianfactorizationfirst_divisorproduct))) + (((ge_first_in_gaussianfactorizationfirst_divisorproduct) * (ge_second_rp_gaussianfactorizationfirst_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationfirst_divisorproductoutputimaginary)))))))))) \/ (exists gr_quotient_gaussianfactorizationsecond_divisor. (exists ge_first_rp_gaussianfactorizationsecond_divisorproduct ge_first_rn_gaussianfactorizationsecond_divisorproduct ge_first_ip_gaussianfactorizationsecond_divisorproduct ge_first_in_gaussianfactorizationsecond_divisorproduct ge_second_rp_gaussianfactorizationsecond_divisorproduct ge_second_rn_gaussianfactorizationsecond_divisorproduct ge_second_ip_gaussianfactorizationsecond_divisorproduct ge_second_in_gaussianfactorizationsecond_divisorproduct. ((exists ge_representation_real_code_gaussianfactorizationsecond_divisorproductfirst ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductfirst. ((((z)) = ((ge_representation_real_code_gaussianfactorizationsecond_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationsecond_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_divisorproductfirstreal ge_balance_negative_gaussianfactorizationsecond_divisorproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationsecond_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecond_divisorproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_divisorproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationsecond_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_divisorproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductfirstreal) = S ge_signed_half_gaussianfactorizationsecond_divisorproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationsecond_divisorproduct) + ge_balance_negative_gaussianfactorizationsecond_divisorproductfirstreal = (ge_first_rn_gaussianfactorizationsecond_divisorproduct) + ge_balance_positive_gaussianfactorizationsecond_divisorproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_divisorproductfirstimaginary ge_balance_negative_gaussianfactorizationsecond_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecond_divisorproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductfirst) = 2 * ge_signed_half_gaussianfactorizationsecond_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductfirstimaginary) = S ge_signed_half_gaussianfactorizationsecond_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationsecond_divisorproduct) + ge_balance_negative_gaussianfactorizationsecond_divisorproductfirstimaginary = (ge_first_in_gaussianfactorizationsecond_divisorproduct) + ge_balance_positive_gaussianfactorizationsecond_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationsecond_divisorproductsecond ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductsecond. (((gr_quotient_gaussianfactorizationsecond_divisor) = ((ge_representation_real_code_gaussianfactorizationsecond_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationsecond_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_divisorproductsecondreal ge_balance_negative_gaussianfactorizationsecond_divisorproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationsecond_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationsecond_divisorproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_divisorproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationsecond_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_divisorproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductsecondreal) = S ge_signed_half_gaussianfactorizationsecond_divisorproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationsecond_divisorproduct) + ge_balance_negative_gaussianfactorizationsecond_divisorproductsecondreal = (ge_second_rn_gaussianfactorizationsecond_divisorproduct) + ge_balance_positive_gaussianfactorizationsecond_divisorproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_divisorproductsecondimaginary ge_balance_negative_gaussianfactorizationsecond_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationsecond_divisorproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductsecond) = 2 * ge_signed_half_gaussianfactorizationsecond_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductsecondimaginary) = S ge_signed_half_gaussianfactorizationsecond_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationsecond_divisorproduct) + ge_balance_negative_gaussianfactorizationsecond_divisorproductsecondimaginary = (ge_second_in_gaussianfactorizationsecond_divisorproduct) + ge_balance_positive_gaussianfactorizationsecond_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationsecond_divisorproductoutput ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductoutput. (((gr_second_factor_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationsecond_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationsecond_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_divisorproductoutputreal ge_balance_negative_gaussianfactorizationsecond_divisorproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationsecond_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecond_divisorproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_divisorproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationsecond_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_divisorproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductoutputreal) = S ge_signed_half_gaussianfactorizationsecond_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecond_divisorproduct) * (ge_second_rp_gaussianfactorizationsecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationsecond_divisorproduct) * (ge_second_rn_gaussianfactorizationsecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationsecond_divisorproduct) * (ge_second_in_gaussianfactorizationsecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationsecond_divisorproduct) * (ge_second_ip_gaussianfactorizationsecond_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationsecond_divisorproductoutputreal = (((((((ge_first_rp_gaussianfactorizationsecond_divisorproduct) * (ge_second_rn_gaussianfactorizationsecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationsecond_divisorproduct) * (ge_second_rp_gaussianfactorizationsecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationsecond_divisorproduct) * (ge_second_ip_gaussianfactorizationsecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationsecond_divisorproduct) * (ge_second_in_gaussianfactorizationsecond_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationsecond_divisorproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_divisorproductoutputimaginary ge_balance_negative_gaussianfactorizationsecond_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecond_divisorproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_divisorproductoutput) = 2 * ge_signed_half_gaussianfactorizationsecond_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_divisorproductoutputimaginary) = S ge_signed_half_gaussianfactorizationsecond_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecond_divisorproduct) * (ge_second_ip_gaussianfactorizationsecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationsecond_divisorproduct) * (ge_second_in_gaussianfactorizationsecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationsecond_divisorproduct) * (ge_second_rp_gaussianfactorizationsecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationsecond_divisorproduct) * (ge_second_rn_gaussianfactorizationsecond_divisorproduct))))))) + ge_balance_negative_gaussianfactorizationsecond_divisorproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationsecond_divisorproduct) * (ge_second_in_gaussianfactorizationsecond_divisorproduct))) + (((ge_first_rn_gaussianfactorizationsecond_divisorproduct) * (ge_second_ip_gaussianfactorizationsecond_divisorproduct))))) + (((((ge_first_ip_gaussianfactorizationsecond_divisorproduct) * (ge_second_rn_gaussianfactorizationsecond_divisorproduct))) + (((ge_first_in_gaussianfactorizationsecond_divisorproduct) * (ge_second_rp_gaussianfactorizationsecond_divisorproduct))))))) + ge_balance_positive_gaussianfactorizationsecond_divisorproductoutputimaginary))))))))))))))

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