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

((((forall pfp_i_gaussianfactorizationbijectionbounded. (exists pfp_gap_gaussianfactorizationbijectionboundedindex. pfp_gap_gaussianfactorizationbijectionboundedindex + S (pfp_i_gaussianfactorizationbijectionbounded) = ((l))) -> exists pfp_a_gaussianfactorizationbijectionbounded. (((exists ff_h_pfp_gaussianfactorizationbijectionboundedentry. ff_h_pfp_gaussianfactorizationbijectionboundedentry + S (pfp_a_gaussianfactorizationbijectionbounded) = S ((S (pfp_i_gaussianfactorizationbijectionbounded)) * (v))) /\ exists ff_q_pfp_gaussianfactorizationbijectionboundedentry. (u) = ff_q_pfp_gaussianfactorizationbijectionboundedentry * S ((S (pfp_i_gaussianfactorizationbijectionbounded)) * (v)) + (pfp_a_gaussianfactorizationbijectionbounded))) /\ (exists pfp_gap_gaussianfactorizationbijectionboundedvalue. pfp_gap_gaussianfactorizationbijectionboundedvalue + S (pfp_a_gaussianfactorizationbijectionbounded) = ((l)))) /\ (((forall pfp_i_gaussianfactorizationbijectioninjective pfp_j_gaussianfactorizationbijectioninjective pfp_a_gaussianfactorizationbijectioninjective. (exists pfp_gap_gaussianfactorizationbijectioninjectivefirst. pfp_gap_gaussianfactorizationbijectioninjectivefirst + S (pfp_i_gaussianfactorizationbijectioninjective) = ((l))) -> (exists pfp_gap_gaussianfactorizationbijectioninjectivesecond. pfp_gap_gaussianfactorizationbijectioninjectivesecond + S (pfp_j_gaussianfactorizationbijectioninjective) = ((l))) -> (((exists ff_h_pfp_gaussianfactorizationbijectioninjectiveleft. ff_h_pfp_gaussianfactorizationbijectioninjectiveleft + S (pfp_a_gaussianfactorizationbijectioninjective) = S ((S (pfp_i_gaussianfactorizationbijectioninjective)) * (v))) /\ exists ff_q_pfp_gaussianfactorizationbijectioninjectiveleft. (u) = ff_q_pfp_gaussianfactorizationbijectioninjectiveleft * S ((S (pfp_i_gaussianfactorizationbijectioninjective)) * (v)) + (pfp_a_gaussianfactorizationbijectioninjective))) -> (((exists ff_h_pfp_gaussianfactorizationbijectioninjectiveright. ff_h_pfp_gaussianfactorizationbijectioninjectiveright + S (pfp_a_gaussianfactorizationbijectioninjective) = S ((S (pfp_j_gaussianfactorizationbijectioninjective)) * (v))) /\ exists ff_q_pfp_gaussianfactorizationbijectioninjectiveright. (u) = ff_q_pfp_gaussianfactorizationbijectioninjectiveright * S ((S (pfp_j_gaussianfactorizationbijectioninjective)) * (v)) + (pfp_a_gaussianfactorizationbijectioninjective))) -> pfp_i_gaussianfactorizationbijectioninjective = pfp_j_gaussianfactorizationbijectioninjective) /\ (forall pfp_a_gaussianfactorizationbijectionsurjective. (exists pfp_gap_gaussianfactorizationbijectionsurjectivevalue. pfp_gap_gaussianfactorizationbijectionsurjectivevalue + S (pfp_a_gaussianfactorizationbijectionsurjective) = ((l))) -> exists pfp_i_gaussianfactorizationbijectionsurjective. (exists pfp_gap_gaussianfactorizationbijectionsurjectiveindex. pfp_gap_gaussianfactorizationbijectionsurjectiveindex + S (pfp_i_gaussianfactorizationbijectionsurjective) = ((l))) /\ (((exists ff_h_pfp_gaussianfactorizationbijectionsurjectiveentry. ff_h_pfp_gaussianfactorizationbijectionsurjectiveentry + S (pfp_a_gaussianfactorizationbijectionsurjective) = S ((S (pfp_i_gaussianfactorizationbijectionsurjective)) * (v))) /\ exists ff_q_pfp_gaussianfactorizationbijectionsurjectiveentry. (u) = ff_q_pfp_gaussianfactorizationbijectionsurjectiveentry * S ((S (pfp_i_gaussianfactorizationbijectionsurjective)) * (v)) + (pfp_a_gaussianfactorizationbijectionsurjective)))))))) /\ (forall gr_match_index_gaussianfactorizationmatching gr_match_image_gaussianfactorizationmatching gr_match_source_gaussianfactorizationmatching gr_match_target_gaussianfactorizationmatching. (exists ge_gap_gaussianfactorizationmatchingindex. ge_gap_gaussianfactorizationmatchingindex + S (gr_match_index_gaussianfactorizationmatching) = ((l))) -> (((exists ff_h_gprod_gaussianfactorizationmatchingmap. ff_h_gprod_gaussianfactorizationmatchingmap + S (gr_match_image_gaussianfactorizationmatching) = S ((S (gr_match_index_gaussianfactorizationmatching)) * (v))) /\ exists ff_q_gprod_gaussianfactorizationmatchingmap. (u) = ff_q_gprod_gaussianfactorizationmatchingmap * S ((S (gr_match_index_gaussianfactorizationmatching)) * (v)) + (gr_match_image_gaussianfactorizationmatching))) -> (((exists ff_h_gprod_gaussianfactorizationmatchingsource. ff_h_gprod_gaussianfactorizationmatchingsource + S (gr_match_source_gaussianfactorizationmatching) = S ((S (gr_match_index_gaussianfactorizationmatching)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationmatchingsource. (b) = ff_q_gprod_gaussianfactorizationmatchingsource * S ((S (gr_match_index_gaussianfactorizationmatching)) * (c)) + (gr_match_source_gaussianfactorizationmatching))) -> (((exists ff_h_gprod_gaussianfactorizationmatchingtarget. ff_h_gprod_gaussianfactorizationmatchingtarget + S (gr_match_target_gaussianfactorizationmatching) = S ((S (gr_match_image_gaussianfactorizationmatching)) * (e))) /\ exists ff_q_gprod_gaussianfactorizationmatchingtarget. (d) = ff_q_gprod_gaussianfactorizationmatchingtarget * S ((S (gr_match_image_gaussianfactorizationmatching)) * (e)) + (gr_match_target_gaussianfactorizationmatching))) -> (exists gr_unit_gaussianfactorizationmatchingunit_witness. ((exists gr_inverse_gaussianfactorizationmatchingunit_witnessunit. (exists ge_first_rp_gaussianfactorizationmatchingunit_witnessunitidentity ge_first_rn_gaussianfactorizationmatchingunit_witnessunitidentity ge_first_ip_gaussianfactorizationmatchingunit_witnessunitidentity ge_first_in_gaussianfactorizationmatchingunit_witnessunitidentity ge_second_rp_gaussianfactorizationmatchingunit_witnessunitidentity ge_second_rn_gaussianfactorizationmatchingunit_witnessunitidentity ge_second_ip_gaussianfactorizationmatchingunit_witnessunitidentity ge_second_in_gaussianfactorizationmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst. (((gr_unit_gaussianfactorizationmatchingunit_witness) = ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityfirstreal ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationmatchingunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_gaussianfactorizationmatchingunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationmatchingunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationmatchingunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond. (((gr_inverse_gaussianfactorizationmatchingunit_witnessunit) = ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentitysecondreal ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationmatchingunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_gaussianfactorizationmatchingunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationmatchingunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationmatchingunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityoutputreal ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationmatchingunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationmatchingunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationmatchingunit_witnessunitidentity))))))) + ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationmatchingunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationmatchingunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationmatchingunit_witnessunitidentity))))))) + ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationmatchingunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationmatchingunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationmatchingunit_witnessunitidentity))))))) + ge_balance_negative_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationmatchingunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationmatchingunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationmatchingunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationmatchingunit_witnessunitidentity))))))) + ge_balance_positive_gaussianfactorizationmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_gaussianfactorizationmatchingunit_witnesstransport ge_first_rn_gaussianfactorizationmatchingunit_witnesstransport ge_first_ip_gaussianfactorizationmatchingunit_witnesstransport ge_first_in_gaussianfactorizationmatchingunit_witnesstransport ge_second_rp_gaussianfactorizationmatchingunit_witnesstransport ge_second_rn_gaussianfactorizationmatchingunit_witnesstransport ge_second_ip_gaussianfactorizationmatchingunit_witnesstransport ge_second_in_gaussianfactorizationmatchingunit_witnesstransport. ((exists ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportfirst ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportfirst. (((gr_unit_gaussianfactorizationmatchingunit_witness) = ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportfirstreal ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportfirstreal) = S ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationmatchingunit_witnesstransport) + ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportfirstreal = (ge_first_rn_gaussianfactorizationmatchingunit_witnesstransport) + ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportfirstimaginary ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationmatchingunit_witnesstransport) + ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportfirstimaginary = (ge_first_in_gaussianfactorizationmatchingunit_witnesstransport) + ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportsecond ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportsecond. (((gr_match_source_gaussianfactorizationmatching) = ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportsecondreal ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportsecondreal) = S ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationmatchingunit_witnesstransport) + ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportsecondreal = (ge_second_rn_gaussianfactorizationmatchingunit_witnesstransport) + ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportsecondimaginary ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationmatchingunit_witnesstransport) + ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportsecondimaginary = (ge_second_in_gaussianfactorizationmatchingunit_witnesstransport) + ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportoutput ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportoutput. (((gr_match_target_gaussianfactorizationmatching) = ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportoutputreal ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportoutputreal) = S ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_rp_gaussianfactorizationmatchingunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_rn_gaussianfactorizationmatchingunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_in_gaussianfactorizationmatchingunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_ip_gaussianfactorizationmatchingunit_witnesstransport))))))) + ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_rn_gaussianfactorizationmatchingunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_rp_gaussianfactorizationmatchingunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_ip_gaussianfactorizationmatchingunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_in_gaussianfactorizationmatchingunit_witnesstransport))))))) + ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportoutputimaginary ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_gaussianfactorizationmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_ip_gaussianfactorizationmatchingunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_in_gaussianfactorizationmatchingunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_rp_gaussianfactorizationmatchingunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_rn_gaussianfactorizationmatchingunit_witnesstransport))))))) + ge_balance_negative_gaussianfactorizationmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_in_gaussianfactorizationmatchingunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_ip_gaussianfactorizationmatchingunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_rn_gaussianfactorizationmatchingunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationmatchingunit_witnesstransport) * (ge_second_rp_gaussianfactorizationmatchingunit_witnesstransport))))))) + ge_balance_positive_gaussianfactorizationmatchingunit_witnesstransportoutputimaginary)))))))))))))

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