GFactorAssociateMatching(b,c,d,e,u,v,l)

forall gr_match_index_gaussianfactorization gr_match_image_gaussianfactorization gr_match_source_gaussianfactorization gr_match_target_gaussianfactorization. (exists ge_gap_gaussianfactorizationindex. ge_gap_gaussianfactorizationindex + S (gr_match_index_gaussianfactorization) = ((l))) -> (((exists ff_h_gprod_gaussianfactorizationmap. ff_h_gprod_gaussianfactorizationmap + S (gr_match_image_gaussianfactorization) = S ((S (gr_match_index_gaussianfactorization)) * (v))) /\ exists ff_q_gprod_gaussianfactorizationmap. (u) = ff_q_gprod_gaussianfactorizationmap * S ((S (gr_match_index_gaussianfactorization)) * (v)) + (gr_match_image_gaussianfactorization))) -> (((exists ff_h_gprod_gaussianfactorizationsource. ff_h_gprod_gaussianfactorizationsource + S (gr_match_source_gaussianfactorization) = S ((S (gr_match_index_gaussianfactorization)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationsource. (b) = ff_q_gprod_gaussianfactorizationsource * S ((S (gr_match_index_gaussianfactorization)) * (c)) + (gr_match_source_gaussianfactorization))) -> (((exists ff_h_gprod_gaussianfactorizationtarget. ff_h_gprod_gaussianfactorizationtarget + S (gr_match_target_gaussianfactorization) = S ((S (gr_match_image_gaussianfactorization)) * (e))) /\ exists ff_q_gprod_gaussianfactorizationtarget. (d) = ff_q_gprod_gaussianfactorizationtarget * S ((S (gr_match_image_gaussianfactorization)) * (e)) + (gr_match_target_gaussianfactorization))) -> (exists gr_unit_gaussianfactorizationunit_witness. ((exists gr_inverse_gaussianfactorizationunit_witnessunit. (exists ge_first_rp_gaussianfactorizationunit_witnessunitidentity ge_first_rn_gaussianfactorizationunit_witnessunitidentity ge_first_ip_gaussianfactorizationunit_witnessunitidentity ge_first_in_gaussianfactorizationunit_witnessunitidentity ge_second_rp_gaussianfactorizationunit_witnessunitidentity ge_second_rn_gaussianfactorizationunit_witnessunitidentity ge_second_ip_gaussianfactorizationunit_witnessunitidentity ge_second_in_gaussianfactorizationunit_witnessunitidentity. ((exists ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityfirst. (((gr_unit_gaussianfactorizationunit_witness) = ((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationunit_witnessunitidentityfirstreal ge_balance_negative_gaussianfactorizationunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationunit_witnessunitidentityfirstreal = (ge_first_rn_gaussianfactorizationunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationunit_witnessunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationunit_witnessunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationunit_witnessunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentitysecond. (((gr_inverse_gaussianfactorizationunit_witnessunit) = ((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationunit_witnessunitidentitysecondreal ge_balance_negative_gaussianfactorizationunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationunit_witnessunitidentitysecondreal = (ge_second_rn_gaussianfactorizationunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationunit_witnessunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationunit_witnessunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationunit_witnessunitidentityoutputreal ge_balance_negative_gaussianfactorizationunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationunit_witnessunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationunit_witnessunitidentity))))))) + ge_balance_negative_gaussianfactorizationunit_witnessunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationunit_witnessunitidentity))))))) + ge_balance_positive_gaussianfactorizationunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationunit_witnessunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunit_witnessunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnessunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationunit_witnessunitidentity))))))) + ge_balance_negative_gaussianfactorizationunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationunit_witnessunitidentity))))))) + ge_balance_positive_gaussianfactorizationunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_gaussianfactorizationunit_witnesstransport ge_first_rn_gaussianfactorizationunit_witnesstransport ge_first_ip_gaussianfactorizationunit_witnesstransport ge_first_in_gaussianfactorizationunit_witnesstransport ge_second_rp_gaussianfactorizationunit_witnesstransport ge_second_rn_gaussianfactorizationunit_witnesstransport ge_second_ip_gaussianfactorizationunit_witnesstransport ge_second_in_gaussianfactorizationunit_witnesstransport. ((exists ge_representation_real_code_gaussianfactorizationunit_witnesstransportfirst ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportfirst. (((gr_unit_gaussianfactorizationunit_witness) = ((ge_representation_real_code_gaussianfactorizationunit_witnesstransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportfirst)) * S ((ge_representation_real_code_gaussianfactorizationunit_witnesstransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationunit_witnesstransportfirstreal ge_balance_negative_gaussianfactorizationunit_witnesstransportfirstreal. (((((ge_representation_real_code_gaussianfactorizationunit_witnesstransportfirst) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnesstransportfirstreal) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationunit_witnesstransportfirst) = 2 * ge_signed_half_gaussianfactorizationunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportfirstreal) = S ge_signed_half_gaussianfactorizationunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationunit_witnesstransport) + ge_balance_negative_gaussianfactorizationunit_witnesstransportfirstreal = (ge_first_rn_gaussianfactorizationunit_witnesstransport) + ge_balance_positive_gaussianfactorizationunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationunit_witnesstransportfirstimaginary ge_balance_negative_gaussianfactorizationunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportfirst) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportfirst) = 2 * ge_signed_half_gaussianfactorizationunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportfirstimaginary) = S ge_signed_half_gaussianfactorizationunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationunit_witnesstransport) + ge_balance_negative_gaussianfactorizationunit_witnesstransportfirstimaginary = (ge_first_in_gaussianfactorizationunit_witnesstransport) + ge_balance_positive_gaussianfactorizationunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationunit_witnesstransportsecond ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportsecond. (((gr_match_source_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationunit_witnesstransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportsecond)) * S ((ge_representation_real_code_gaussianfactorizationunit_witnesstransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationunit_witnesstransportsecondreal ge_balance_negative_gaussianfactorizationunit_witnesstransportsecondreal. (((((ge_representation_real_code_gaussianfactorizationunit_witnesstransportsecond) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnesstransportsecondreal) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationunit_witnesstransportsecond) = 2 * ge_signed_half_gaussianfactorizationunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportsecondreal) = S ge_signed_half_gaussianfactorizationunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationunit_witnesstransport) + ge_balance_negative_gaussianfactorizationunit_witnesstransportsecondreal = (ge_second_rn_gaussianfactorizationunit_witnesstransport) + ge_balance_positive_gaussianfactorizationunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationunit_witnesstransportsecondimaginary ge_balance_negative_gaussianfactorizationunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportsecond) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportsecond) = 2 * ge_signed_half_gaussianfactorizationunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportsecondimaginary) = S ge_signed_half_gaussianfactorizationunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationunit_witnesstransport) + ge_balance_negative_gaussianfactorizationunit_witnesstransportsecondimaginary = (ge_second_in_gaussianfactorizationunit_witnesstransport) + ge_balance_positive_gaussianfactorizationunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationunit_witnesstransportoutput ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportoutput. (((gr_match_target_gaussianfactorization) = ((ge_representation_real_code_gaussianfactorizationunit_witnesstransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportoutput)) * S ((ge_representation_real_code_gaussianfactorizationunit_witnesstransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationunit_witnesstransportoutputreal ge_balance_negative_gaussianfactorizationunit_witnesstransportoutputreal. (((((ge_representation_real_code_gaussianfactorizationunit_witnesstransportoutput) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnesstransportoutputreal) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationunit_witnesstransportoutput) = 2 * ge_signed_half_gaussianfactorizationunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportoutputreal) = S ge_signed_half_gaussianfactorizationunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunit_witnesstransport) * (ge_second_rp_gaussianfactorizationunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationunit_witnesstransport) * (ge_second_rn_gaussianfactorizationunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationunit_witnesstransport) * (ge_second_in_gaussianfactorizationunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationunit_witnesstransport) * (ge_second_ip_gaussianfactorizationunit_witnesstransport))))))) + ge_balance_negative_gaussianfactorizationunit_witnesstransportoutputreal = (((((((ge_first_rp_gaussianfactorizationunit_witnesstransport) * (ge_second_rn_gaussianfactorizationunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationunit_witnesstransport) * (ge_second_rp_gaussianfactorizationunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationunit_witnesstransport) * (ge_second_ip_gaussianfactorizationunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationunit_witnesstransport) * (ge_second_in_gaussianfactorizationunit_witnesstransport))))))) + ge_balance_positive_gaussianfactorizationunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationunit_witnesstransportoutputimaginary ge_balance_negative_gaussianfactorizationunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportoutput) = 2 * (ge_balance_positive_gaussianfactorizationunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationunit_witnesstransportoutput) = 2 * ge_signed_half_gaussianfactorizationunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationunit_witnesstransportoutputimaginary) = S ge_signed_half_gaussianfactorizationunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationunit_witnesstransport) * (ge_second_ip_gaussianfactorizationunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationunit_witnesstransport) * (ge_second_in_gaussianfactorizationunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationunit_witnesstransport) * (ge_second_rp_gaussianfactorizationunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationunit_witnesstransport) * (ge_second_rn_gaussianfactorizationunit_witnesstransport))))))) + ge_balance_negative_gaussianfactorizationunit_witnesstransportoutputimaginary = (((((((ge_first_rp_gaussianfactorizationunit_witnesstransport) * (ge_second_in_gaussianfactorizationunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationunit_witnesstransport) * (ge_second_ip_gaussianfactorizationunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationunit_witnesstransport) * (ge_second_rn_gaussianfactorizationunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationunit_witnesstransport) * (ge_second_rp_gaussianfactorizationunit_witnesstransport))))))) + ge_balance_positive_gaussianfactorizationunit_witnesstransportoutputimaginary)))))))))))

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