GAssociate(a,b)

exists gr_unit_gaussianfactorization. ((exists gr_inverse_gaussianfactorizationunit. (exists ge_first_rp_gaussianfactorizationunitidentity ge_first_rn_gaussianfactorizationunitidentity ge_first_ip_gaussianfactorizationunitidentity ge_first_in_gaussianfactorizationunitidentity ge_second_rp_gaussianfactorizationunitidentity ge_second_rn_gaussianfactorizationunitidentity ge_second_ip_gaussianfactorizationunitidentity ge_second_in_gaussianfactorizationunitidentity. ((exists ge_representation_real_code_gaussianfactorizationunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst. (((gr_unit_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationunitidentityfirstreal ge_balance_negative_gaussianfactorizationunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentityfirstreal = (ge_first_rn_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond. (((gr_inverse_gaussianfactorizationunit) = ((ge_representation_real_code_gaussianfactorizationunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationunitidentitysecondreal ge_balance_negative_gaussianfactorizationunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentitysecondreal = (ge_second_rn_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationunitidentity) + ge_balance_negative_gaussianfactorizationunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationunitidentity) + ge_balance_positive_gaussianfactorizationunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationunitidentityoutputreal ge_balance_negative_gaussianfactorizationunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))))))) + ge_balance_negative_gaussianfactorizationunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))))))) + ge_balance_positive_gaussianfactorizationunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))))))) + ge_balance_negative_gaussianfactorizationunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationunitidentity) * (ge_second_in_gaussianfactorizationunitidentity))) + (((ge_first_rn_gaussianfactorizationunitidentity) * (ge_second_ip_gaussianfactorizationunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunitidentity) * (ge_second_rn_gaussianfactorizationunitidentity))) + (((ge_first_in_gaussianfactorizationunitidentity) * (ge_second_rp_gaussianfactorizationunitidentity))))))) + ge_balance_positive_gaussianfactorizationunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_gaussianfactorizationtransport ge_first_rn_gaussianfactorizationtransport ge_first_ip_gaussianfactorizationtransport ge_first_in_gaussianfactorizationtransport ge_second_rp_gaussianfactorizationtransport ge_second_rn_gaussianfactorizationtransport ge_second_ip_gaussianfactorizationtransport ge_second_in_gaussianfactorizationtransport. ((exists ge_representation_real_code_gaussianfactorizationtransportfirst ge_representation_imaginary_code_gaussianfactorizationtransportfirst. (((gr_unit_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationtransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationtransportfirst)) * S ((ge_representation_real_code_gaussianfactorizationtransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationtransportfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationtransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationtransportfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationtransportfirstreal ge_balance_negative_gaussianfactorizationtransportfirstreal. (((((ge_representation_real_code_gaussianfactorizationtransportfirst) = 2 * (ge_balance_positive_gaussianfactorizationtransportfirstreal) /\ (ge_balance_negative_gaussianfactorizationtransportfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationtransportfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationtransportfirst) = 2 * ge_signed_half_gaussianfactorizationtransportfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationtransportfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationtransportfirstreal) = S ge_signed_half_gaussianfactorizationtransportfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationtransport) + ge_balance_negative_gaussianfactorizationtransportfirstreal = (ge_first_rn_gaussianfactorizationtransport) + ge_balance_positive_gaussianfactorizationtransportfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationtransportfirstimaginary ge_balance_negative_gaussianfactorizationtransportfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationtransportfirst) = 2 * (ge_balance_positive_gaussianfactorizationtransportfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationtransportfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationtransportfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationtransportfirst) = 2 * ge_signed_half_gaussianfactorizationtransportfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationtransportfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationtransportfirstimaginary) = S ge_signed_half_gaussianfactorizationtransportfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationtransport) + ge_balance_negative_gaussianfactorizationtransportfirstimaginary = (ge_first_in_gaussianfactorizationtransport) + ge_balance_positive_gaussianfactorizationtransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationtransportsecond ge_representation_imaginary_code_gaussianfactorizationtransportsecond. ((((a)) = ((ge_representation_real_code_gaussianfactorizationtransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationtransportsecond)) * S ((ge_representation_real_code_gaussianfactorizationtransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationtransportsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationtransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationtransportsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationtransportsecondreal ge_balance_negative_gaussianfactorizationtransportsecondreal. (((((ge_representation_real_code_gaussianfactorizationtransportsecond) = 2 * (ge_balance_positive_gaussianfactorizationtransportsecondreal) /\ (ge_balance_negative_gaussianfactorizationtransportsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationtransportsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationtransportsecond) = 2 * ge_signed_half_gaussianfactorizationtransportsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationtransportsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationtransportsecondreal) = S ge_signed_half_gaussianfactorizationtransportsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationtransport) + ge_balance_negative_gaussianfactorizationtransportsecondreal = (ge_second_rn_gaussianfactorizationtransport) + ge_balance_positive_gaussianfactorizationtransportsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationtransportsecondimaginary ge_balance_negative_gaussianfactorizationtransportsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationtransportsecond) = 2 * (ge_balance_positive_gaussianfactorizationtransportsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationtransportsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationtransportsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationtransportsecond) = 2 * ge_signed_half_gaussianfactorizationtransportsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationtransportsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationtransportsecondimaginary) = S ge_signed_half_gaussianfactorizationtransportsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationtransport) + ge_balance_negative_gaussianfactorizationtransportsecondimaginary = (ge_second_in_gaussianfactorizationtransport) + ge_balance_positive_gaussianfactorizationtransportsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationtransportoutput ge_representation_imaginary_code_gaussianfactorizationtransportoutput. ((((b)) = ((ge_representation_real_code_gaussianfactorizationtransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationtransportoutput)) * S ((ge_representation_real_code_gaussianfactorizationtransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationtransportoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationtransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationtransportoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationtransportoutputreal ge_balance_negative_gaussianfactorizationtransportoutputreal. (((((ge_representation_real_code_gaussianfactorizationtransportoutput) = 2 * (ge_balance_positive_gaussianfactorizationtransportoutputreal) /\ (ge_balance_negative_gaussianfactorizationtransportoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationtransportoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationtransportoutput) = 2 * ge_signed_half_gaussianfactorizationtransportoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationtransportoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationtransportoutputreal) = S ge_signed_half_gaussianfactorizationtransportoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationtransport) * (ge_second_rp_gaussianfactorizationtransport))) + (((ge_first_rn_gaussianfactorizationtransport) * (ge_second_rn_gaussianfactorizationtransport))))) + (((((ge_first_ip_gaussianfactorizationtransport) * (ge_second_in_gaussianfactorizationtransport))) + (((ge_first_in_gaussianfactorizationtransport) * (ge_second_ip_gaussianfactorizationtransport))))))) + ge_balance_negative_gaussianfactorizationtransportoutputreal = (((((((ge_first_rp_gaussianfactorizationtransport) * (ge_second_rn_gaussianfactorizationtransport))) + (((ge_first_rn_gaussianfactorizationtransport) * (ge_second_rp_gaussianfactorizationtransport))))) + (((((ge_first_ip_gaussianfactorizationtransport) * (ge_second_ip_gaussianfactorizationtransport))) + (((ge_first_in_gaussianfactorizationtransport) * (ge_second_in_gaussianfactorizationtransport))))))) + ge_balance_positive_gaussianfactorizationtransportoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationtransportoutputimaginary ge_balance_negative_gaussianfactorizationtransportoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationtransportoutput) = 2 * (ge_balance_positive_gaussianfactorizationtransportoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationtransportoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationtransportoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationtransportoutput) = 2 * ge_signed_half_gaussianfactorizationtransportoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationtransportoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationtransportoutputimaginary) = S ge_signed_half_gaussianfactorizationtransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationtransport) * (ge_second_ip_gaussianfactorizationtransport))) + (((ge_first_rn_gaussianfactorizationtransport) * (ge_second_in_gaussianfactorizationtransport))))) + (((((ge_first_ip_gaussianfactorizationtransport) * (ge_second_rp_gaussianfactorizationtransport))) + (((ge_first_in_gaussianfactorizationtransport) * (ge_second_rn_gaussianfactorizationtransport))))))) + ge_balance_negative_gaussianfactorizationtransportoutputimaginary = (((((((ge_first_rp_gaussianfactorizationtransport) * (ge_second_in_gaussianfactorizationtransport))) + (((ge_first_rn_gaussianfactorizationtransport) * (ge_second_ip_gaussianfactorizationtransport))))) + (((((ge_first_ip_gaussianfactorizationtransport) * (ge_second_rn_gaussianfactorizationtransport))) + (((ge_first_in_gaussianfactorizationtransport) * (ge_second_rp_gaussianfactorizationtransport))))))) + ge_balance_positive_gaussianfactorizationtransportoutputimaginary))))))))))

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