GStrictNonunitFactorization(z,N,a,b,A,B)

((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. ((((a)) = ((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. ((((b)) = ((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. ((((z)) = ((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 ge_norm_rp_gaussianfactorizationfirst_norm ge_norm_rn_gaussianfactorizationfirst_norm ge_norm_ip_gaussianfactorizationfirst_norm ge_norm_in_gaussianfactorizationfirst_norm. ((exists ge_representation_real_code_gaussianfactorizationfirst_normrepresentation ge_representation_imaginary_code_gaussianfactorizationfirst_normrepresentation. ((((a)) = ((ge_representation_real_code_gaussianfactorizationfirst_normrepresentation) + (ge_representation_imaginary_code_gaussianfactorizationfirst_normrepresentation)) * S ((ge_representation_real_code_gaussianfactorizationfirst_normrepresentation) + (ge_representation_imaginary_code_gaussianfactorizationfirst_normrepresentation)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_normrepresentation) + (ge_representation_imaginary_code_gaussianfactorizationfirst_normrepresentation))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_normrepresentationreal ge_balance_negative_gaussianfactorizationfirst_normrepresentationreal. (((((ge_representation_real_code_gaussianfactorizationfirst_normrepresentation) = 2 * (ge_balance_positive_gaussianfactorizationfirst_normrepresentationreal) /\ (ge_balance_negative_gaussianfactorizationfirst_normrepresentationreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_normrepresentationrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_normrepresentation) = 2 * ge_signed_half_gaussianfactorizationfirst_normrepresentationrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_normrepresentationreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_normrepresentationreal) = S ge_signed_half_gaussianfactorizationfirst_normrepresentationrealdecode))) /\ ((ge_norm_rp_gaussianfactorizationfirst_norm) + ge_balance_negative_gaussianfactorizationfirst_normrepresentationreal = (ge_norm_rn_gaussianfactorizationfirst_norm) + ge_balance_positive_gaussianfactorizationfirst_normrepresentationreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_normrepresentationimaginary ge_balance_negative_gaussianfactorizationfirst_normrepresentationimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_normrepresentation) = 2 * (ge_balance_positive_gaussianfactorizationfirst_normrepresentationimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_normrepresentationimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_normrepresentation) = 2 * ge_signed_half_gaussianfactorizationfirst_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_normrepresentationimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_normrepresentationimaginary) = S ge_signed_half_gaussianfactorizationfirst_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_gaussianfactorizationfirst_norm) + ge_balance_negative_gaussianfactorizationfirst_normrepresentationimaginary = (ge_norm_in_gaussianfactorizationfirst_norm) + ge_balance_positive_gaussianfactorizationfirst_normrepresentationimaginary)))))) /\ (exists ge_real_square_gaussianfactorizationfirst_normsquare ge_imaginary_square_gaussianfactorizationfirst_normsquare. ((((((ge_norm_rp_gaussianfactorizationfirst_norm) * (ge_norm_rp_gaussianfactorizationfirst_norm))) + (((ge_norm_rn_gaussianfactorizationfirst_norm) * (ge_norm_rn_gaussianfactorizationfirst_norm)))) = ((ge_real_square_gaussianfactorizationfirst_normsquare) + (((((ge_norm_rp_gaussianfactorizationfirst_norm) * (ge_norm_rn_gaussianfactorizationfirst_norm))) + (((ge_norm_rn_gaussianfactorizationfirst_norm) * (ge_norm_rp_gaussianfactorizationfirst_norm))))))) /\ ((((((ge_norm_ip_gaussianfactorizationfirst_norm) * (ge_norm_ip_gaussianfactorizationfirst_norm))) + (((ge_norm_in_gaussianfactorizationfirst_norm) * (ge_norm_in_gaussianfactorizationfirst_norm)))) = ((ge_imaginary_square_gaussianfactorizationfirst_normsquare) + (((((ge_norm_ip_gaussianfactorizationfirst_norm) * (ge_norm_in_gaussianfactorizationfirst_norm))) + (((ge_norm_in_gaussianfactorizationfirst_norm) * (ge_norm_ip_gaussianfactorizationfirst_norm))))))) /\ (((A)) = ge_real_square_gaussianfactorizationfirst_normsquare + ge_imaginary_square_gaussianfactorizationfirst_normsquare)))))) /\ ((exists ge_norm_rp_gaussianfactorizationsecond_norm ge_norm_rn_gaussianfactorizationsecond_norm ge_norm_ip_gaussianfactorizationsecond_norm ge_norm_in_gaussianfactorizationsecond_norm. ((exists ge_representation_real_code_gaussianfactorizationsecond_normrepresentation ge_representation_imaginary_code_gaussianfactorizationsecond_normrepresentation. ((((b)) = ((ge_representation_real_code_gaussianfactorizationsecond_normrepresentation) + (ge_representation_imaginary_code_gaussianfactorizationsecond_normrepresentation)) * S ((ge_representation_real_code_gaussianfactorizationsecond_normrepresentation) + (ge_representation_imaginary_code_gaussianfactorizationsecond_normrepresentation)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_normrepresentation) + (ge_representation_imaginary_code_gaussianfactorizationsecond_normrepresentation))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_normrepresentationreal ge_balance_negative_gaussianfactorizationsecond_normrepresentationreal. (((((ge_representation_real_code_gaussianfactorizationsecond_normrepresentation) = 2 * (ge_balance_positive_gaussianfactorizationsecond_normrepresentationreal) /\ (ge_balance_negative_gaussianfactorizationsecond_normrepresentationreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_normrepresentationrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_normrepresentation) = 2 * ge_signed_half_gaussianfactorizationsecond_normrepresentationrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_normrepresentationreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_normrepresentationreal) = S ge_signed_half_gaussianfactorizationsecond_normrepresentationrealdecode))) /\ ((ge_norm_rp_gaussianfactorizationsecond_norm) + ge_balance_negative_gaussianfactorizationsecond_normrepresentationreal = (ge_norm_rn_gaussianfactorizationsecond_norm) + ge_balance_positive_gaussianfactorizationsecond_normrepresentationreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_normrepresentationimaginary ge_balance_negative_gaussianfactorizationsecond_normrepresentationimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_normrepresentation) = 2 * (ge_balance_positive_gaussianfactorizationsecond_normrepresentationimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_normrepresentationimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_normrepresentation) = 2 * ge_signed_half_gaussianfactorizationsecond_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_normrepresentationimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_normrepresentationimaginary) = S ge_signed_half_gaussianfactorizationsecond_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_gaussianfactorizationsecond_norm) + ge_balance_negative_gaussianfactorizationsecond_normrepresentationimaginary = (ge_norm_in_gaussianfactorizationsecond_norm) + ge_balance_positive_gaussianfactorizationsecond_normrepresentationimaginary)))))) /\ (exists ge_real_square_gaussianfactorizationsecond_normsquare ge_imaginary_square_gaussianfactorizationsecond_normsquare. ((((((ge_norm_rp_gaussianfactorizationsecond_norm) * (ge_norm_rp_gaussianfactorizationsecond_norm))) + (((ge_norm_rn_gaussianfactorizationsecond_norm) * (ge_norm_rn_gaussianfactorizationsecond_norm)))) = ((ge_real_square_gaussianfactorizationsecond_normsquare) + (((((ge_norm_rp_gaussianfactorizationsecond_norm) * (ge_norm_rn_gaussianfactorizationsecond_norm))) + (((ge_norm_rn_gaussianfactorizationsecond_norm) * (ge_norm_rp_gaussianfactorizationsecond_norm))))))) /\ ((((((ge_norm_ip_gaussianfactorizationsecond_norm) * (ge_norm_ip_gaussianfactorizationsecond_norm))) + (((ge_norm_in_gaussianfactorizationsecond_norm) * (ge_norm_in_gaussianfactorizationsecond_norm)))) = ((ge_imaginary_square_gaussianfactorizationsecond_normsquare) + (((((ge_norm_ip_gaussianfactorizationsecond_norm) * (ge_norm_in_gaussianfactorizationsecond_norm))) + (((ge_norm_in_gaussianfactorizationsecond_norm) * (ge_norm_ip_gaussianfactorizationsecond_norm))))))) /\ (((B)) = ge_real_square_gaussianfactorizationsecond_normsquare + ge_imaginary_square_gaussianfactorizationsecond_normsquare)))))) /\ ((~(exists gr_inverse_gaussianfactorizationfirst_nonunit. (exists ge_first_rp_gaussianfactorizationfirst_nonunitidentity ge_first_rn_gaussianfactorizationfirst_nonunitidentity ge_first_ip_gaussianfactorizationfirst_nonunitidentity ge_first_in_gaussianfactorizationfirst_nonunitidentity ge_second_rp_gaussianfactorizationfirst_nonunitidentity ge_second_rn_gaussianfactorizationfirst_nonunitidentity ge_second_ip_gaussianfactorizationfirst_nonunitidentity ge_second_in_gaussianfactorizationfirst_nonunitidentity. ((exists ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityfirst. ((((a)) = ((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_nonunitidentityfirstreal ge_balance_negative_gaussianfactorizationfirst_nonunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirst_nonunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_nonunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationfirst_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationfirst_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationfirst_nonunitidentity) + ge_balance_negative_gaussianfactorizationfirst_nonunitidentityfirstreal = (ge_first_rn_gaussianfactorizationfirst_nonunitidentity) + ge_balance_positive_gaussianfactorizationfirst_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_nonunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationfirst_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationfirst_nonunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationfirst_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationfirst_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationfirst_nonunitidentity) + ge_balance_negative_gaussianfactorizationfirst_nonunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationfirst_nonunitidentity) + ge_balance_positive_gaussianfactorizationfirst_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationfirst_nonunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentitysecond. (((gr_inverse_gaussianfactorizationfirst_nonunit) = ((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_nonunitidentitysecondreal ge_balance_negative_gaussianfactorizationfirst_nonunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationfirst_nonunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_nonunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationfirst_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationfirst_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationfirst_nonunitidentity) + ge_balance_negative_gaussianfactorizationfirst_nonunitidentitysecondreal = (ge_second_rn_gaussianfactorizationfirst_nonunitidentity) + ge_balance_positive_gaussianfactorizationfirst_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_nonunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationfirst_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationfirst_nonunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationfirst_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationfirst_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationfirst_nonunitidentity) + ge_balance_negative_gaussianfactorizationfirst_nonunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationfirst_nonunitidentity) + ge_balance_positive_gaussianfactorizationfirst_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationfirst_nonunitidentityoutputreal ge_balance_negative_gaussianfactorizationfirst_nonunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirst_nonunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_nonunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationfirst_nonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationfirst_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationfirst_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirst_nonunitidentity) * (ge_second_rp_gaussianfactorizationfirst_nonunitidentity))) + (((ge_first_rn_gaussianfactorizationfirst_nonunitidentity) * (ge_second_rn_gaussianfactorizationfirst_nonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationfirst_nonunitidentity) * (ge_second_in_gaussianfactorizationfirst_nonunitidentity))) + (((ge_first_in_gaussianfactorizationfirst_nonunitidentity) * (ge_second_ip_gaussianfactorizationfirst_nonunitidentity))))))) + ge_balance_negative_gaussianfactorizationfirst_nonunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationfirst_nonunitidentity) * (ge_second_rn_gaussianfactorizationfirst_nonunitidentity))) + (((ge_first_rn_gaussianfactorizationfirst_nonunitidentity) * (ge_second_rp_gaussianfactorizationfirst_nonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationfirst_nonunitidentity) * (ge_second_ip_gaussianfactorizationfirst_nonunitidentity))) + (((ge_first_in_gaussianfactorizationfirst_nonunitidentity) * (ge_second_in_gaussianfactorizationfirst_nonunitidentity))))))) + ge_balance_positive_gaussianfactorizationfirst_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationfirst_nonunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationfirst_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationfirst_nonunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationfirst_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationfirst_nonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationfirst_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationfirst_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationfirst_nonunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationfirst_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationfirst_nonunitidentity) * (ge_second_ip_gaussianfactorizationfirst_nonunitidentity))) + (((ge_first_rn_gaussianfactorizationfirst_nonunitidentity) * (ge_second_in_gaussianfactorizationfirst_nonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationfirst_nonunitidentity) * (ge_second_rp_gaussianfactorizationfirst_nonunitidentity))) + (((ge_first_in_gaussianfactorizationfirst_nonunitidentity) * (ge_second_rn_gaussianfactorizationfirst_nonunitidentity))))))) + ge_balance_negative_gaussianfactorizationfirst_nonunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationfirst_nonunitidentity) * (ge_second_in_gaussianfactorizationfirst_nonunitidentity))) + (((ge_first_rn_gaussianfactorizationfirst_nonunitidentity) * (ge_second_ip_gaussianfactorizationfirst_nonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationfirst_nonunitidentity) * (ge_second_rn_gaussianfactorizationfirst_nonunitidentity))) + (((ge_first_in_gaussianfactorizationfirst_nonunitidentity) * (ge_second_rp_gaussianfactorizationfirst_nonunitidentity))))))) + ge_balance_positive_gaussianfactorizationfirst_nonunitidentityoutputimaginary))))))))))) /\ ((~(exists gr_inverse_gaussianfactorizationsecond_nonunit. (exists ge_first_rp_gaussianfactorizationsecond_nonunitidentity ge_first_rn_gaussianfactorizationsecond_nonunitidentity ge_first_ip_gaussianfactorizationsecond_nonunitidentity ge_first_in_gaussianfactorizationsecond_nonunitidentity ge_second_rp_gaussianfactorizationsecond_nonunitidentity ge_second_rn_gaussianfactorizationsecond_nonunitidentity ge_second_ip_gaussianfactorizationsecond_nonunitidentity ge_second_in_gaussianfactorizationsecond_nonunitidentity. ((exists ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityfirst. ((((b)) = ((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_nonunitidentityfirstreal ge_balance_negative_gaussianfactorizationsecond_nonunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecond_nonunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_nonunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationsecond_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationsecond_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationsecond_nonunitidentity) + ge_balance_negative_gaussianfactorizationsecond_nonunitidentityfirstreal = (ge_first_rn_gaussianfactorizationsecond_nonunitidentity) + ge_balance_positive_gaussianfactorizationsecond_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_nonunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationsecond_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationsecond_nonunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationsecond_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationsecond_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationsecond_nonunitidentity) + ge_balance_negative_gaussianfactorizationsecond_nonunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationsecond_nonunitidentity) + ge_balance_positive_gaussianfactorizationsecond_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationsecond_nonunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentitysecond. (((gr_inverse_gaussianfactorizationsecond_nonunit) = ((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_nonunitidentitysecondreal ge_balance_negative_gaussianfactorizationsecond_nonunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationsecond_nonunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_nonunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationsecond_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationsecond_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationsecond_nonunitidentity) + ge_balance_negative_gaussianfactorizationsecond_nonunitidentitysecondreal = (ge_second_rn_gaussianfactorizationsecond_nonunitidentity) + ge_balance_positive_gaussianfactorizationsecond_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_nonunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationsecond_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationsecond_nonunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationsecond_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationsecond_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationsecond_nonunitidentity) + ge_balance_negative_gaussianfactorizationsecond_nonunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationsecond_nonunitidentity) + ge_balance_positive_gaussianfactorizationsecond_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationsecond_nonunitidentityoutputreal ge_balance_negative_gaussianfactorizationsecond_nonunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecond_nonunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_nonunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationsecond_nonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationsecond_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationsecond_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecond_nonunitidentity) * (ge_second_rp_gaussianfactorizationsecond_nonunitidentity))) + (((ge_first_rn_gaussianfactorizationsecond_nonunitidentity) * (ge_second_rn_gaussianfactorizationsecond_nonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationsecond_nonunitidentity) * (ge_second_in_gaussianfactorizationsecond_nonunitidentity))) + (((ge_first_in_gaussianfactorizationsecond_nonunitidentity) * (ge_second_ip_gaussianfactorizationsecond_nonunitidentity))))))) + ge_balance_negative_gaussianfactorizationsecond_nonunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationsecond_nonunitidentity) * (ge_second_rn_gaussianfactorizationsecond_nonunitidentity))) + (((ge_first_rn_gaussianfactorizationsecond_nonunitidentity) * (ge_second_rp_gaussianfactorizationsecond_nonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationsecond_nonunitidentity) * (ge_second_ip_gaussianfactorizationsecond_nonunitidentity))) + (((ge_first_in_gaussianfactorizationsecond_nonunitidentity) * (ge_second_in_gaussianfactorizationsecond_nonunitidentity))))))) + ge_balance_positive_gaussianfactorizationsecond_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationsecond_nonunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationsecond_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationsecond_nonunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationsecond_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationsecond_nonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationsecond_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationsecond_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationsecond_nonunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationsecond_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationsecond_nonunitidentity) * (ge_second_ip_gaussianfactorizationsecond_nonunitidentity))) + (((ge_first_rn_gaussianfactorizationsecond_nonunitidentity) * (ge_second_in_gaussianfactorizationsecond_nonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationsecond_nonunitidentity) * (ge_second_rp_gaussianfactorizationsecond_nonunitidentity))) + (((ge_first_in_gaussianfactorizationsecond_nonunitidentity) * (ge_second_rn_gaussianfactorizationsecond_nonunitidentity))))))) + ge_balance_negative_gaussianfactorizationsecond_nonunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationsecond_nonunitidentity) * (ge_second_in_gaussianfactorizationsecond_nonunitidentity))) + (((ge_first_rn_gaussianfactorizationsecond_nonunitidentity) * (ge_second_ip_gaussianfactorizationsecond_nonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationsecond_nonunitidentity) * (ge_second_rn_gaussianfactorizationsecond_nonunitidentity))) + (((ge_first_in_gaussianfactorizationsecond_nonunitidentity) * (ge_second_rp_gaussianfactorizationsecond_nonunitidentity))))))) + ge_balance_positive_gaussianfactorizationsecond_nonunitidentityoutputimaginary))))))))))) /\ ((exists ge_gap_gaussianfactorizationfirst_strict. ge_gap_gaussianfactorizationfirst_strict + S ((A)) = ((N))) /\ (exists ge_gap_gaussianfactorizationsecond_strict. ge_gap_gaussianfactorizationsecond_strict + S ((B)) = ((N)))))))))

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