GUnit(z)

exists gr_inverse_gaussianfactorization. (exists ge_first_rp_gaussianfactorizationidentity ge_first_rn_gaussianfactorizationidentity ge_first_ip_gaussianfactorizationidentity ge_first_in_gaussianfactorizationidentity ge_second_rp_gaussianfactorizationidentity ge_second_rn_gaussianfactorizationidentity ge_second_ip_gaussianfactorizationidentity ge_second_in_gaussianfactorizationidentity. ((exists ge_representation_real_code_gaussianfactorizationidentityfirst ge_representation_imaginary_code_gaussianfactorizationidentityfirst. ((((z)) = ((ge_representation_real_code_gaussianfactorizationidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationidentityfirstreal ge_balance_negative_gaussianfactorizationidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationidentityfirst) = 2 * ge_signed_half_gaussianfactorizationidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationidentityfirstreal) = S ge_signed_half_gaussianfactorizationidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationidentity) + ge_balance_negative_gaussianfactorizationidentityfirstreal = (ge_first_rn_gaussianfactorizationidentity) + ge_balance_positive_gaussianfactorizationidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationidentityfirstimaginary ge_balance_negative_gaussianfactorizationidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationidentityfirst) = 2 * ge_signed_half_gaussianfactorizationidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationidentity) + ge_balance_negative_gaussianfactorizationidentityfirstimaginary = (ge_first_in_gaussianfactorizationidentity) + ge_balance_positive_gaussianfactorizationidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationidentitysecond ge_representation_imaginary_code_gaussianfactorizationidentitysecond. (((gr_inverse_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationidentitysecondreal ge_balance_negative_gaussianfactorizationidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationidentitysecond) = 2 * ge_signed_half_gaussianfactorizationidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationidentitysecondreal) = S ge_signed_half_gaussianfactorizationidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationidentity) + ge_balance_negative_gaussianfactorizationidentitysecondreal = (ge_second_rn_gaussianfactorizationidentity) + ge_balance_positive_gaussianfactorizationidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationidentitysecondimaginary ge_balance_negative_gaussianfactorizationidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationidentitysecond) = 2 * ge_signed_half_gaussianfactorizationidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationidentity) + ge_balance_negative_gaussianfactorizationidentitysecondimaginary = (ge_second_in_gaussianfactorizationidentity) + ge_balance_positive_gaussianfactorizationidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationidentityoutput ge_representation_imaginary_code_gaussianfactorizationidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationidentityoutputreal ge_balance_negative_gaussianfactorizationidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationidentityoutput) = 2 * ge_signed_half_gaussianfactorizationidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationidentityoutputreal) = S ge_signed_half_gaussianfactorizationidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationidentity) * (ge_second_rp_gaussianfactorizationidentity))) + (((ge_first_rn_gaussianfactorizationidentity) * (ge_second_rn_gaussianfactorizationidentity))))) + (((((ge_first_ip_gaussianfactorizationidentity) * (ge_second_in_gaussianfactorizationidentity))) + (((ge_first_in_gaussianfactorizationidentity) * (ge_second_ip_gaussianfactorizationidentity))))))) + ge_balance_negative_gaussianfactorizationidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationidentity) * (ge_second_rn_gaussianfactorizationidentity))) + (((ge_first_rn_gaussianfactorizationidentity) * (ge_second_rp_gaussianfactorizationidentity))))) + (((((ge_first_ip_gaussianfactorizationidentity) * (ge_second_ip_gaussianfactorizationidentity))) + (((ge_first_in_gaussianfactorizationidentity) * (ge_second_in_gaussianfactorizationidentity))))))) + ge_balance_positive_gaussianfactorizationidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationidentityoutputimaginary ge_balance_negative_gaussianfactorizationidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationidentityoutput) = 2 * ge_signed_half_gaussianfactorizationidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationidentity) * (ge_second_ip_gaussianfactorizationidentity))) + (((ge_first_rn_gaussianfactorizationidentity) * (ge_second_in_gaussianfactorizationidentity))))) + (((((ge_first_ip_gaussianfactorizationidentity) * (ge_second_rp_gaussianfactorizationidentity))) + (((ge_first_in_gaussianfactorizationidentity) * (ge_second_rn_gaussianfactorizationidentity))))))) + ge_balance_negative_gaussianfactorizationidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationidentity) * (ge_second_in_gaussianfactorizationidentity))) + (((ge_first_rn_gaussianfactorizationidentity) * (ge_second_ip_gaussianfactorizationidentity))))) + (((((ge_first_ip_gaussianfactorizationidentity) * (ge_second_rn_gaussianfactorizationidentity))) + (((ge_first_in_gaussianfactorizationidentity) * (ge_second_rp_gaussianfactorizationidentity))))))) + ge_balance_positive_gaussianfactorizationidentityoutputimaginary)))))))))

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