GFactorPermutation(b,c,l,d,e,m,u,v)

((((l))=((m))) /\ (((((forall pfp_i_gaussianfactorizationmatchedbijectionbounded. (exists pfp_gap_gaussianfactorizationmatchedbijectionboundedindex. pfp_gap_gaussianfactorizationmatchedbijectionboundedindex + S (pfp_i_gaussianfactorizationmatchedbijectionbounded) = ((l))) -> exists pfp_a_gaussianfactorizationmatchedbijectionbounded. (((exists ff_h_pfp_gaussianfactorizationmatchedbijectionboundedentry. ff_h_pfp_gaussianfactorizationmatchedbijectionboundedentry + S (pfp_a_gaussianfactorizationmatchedbijectionbounded) = S ((S (pfp_i_gaussianfactorizationmatchedbijectionbounded)) * (v))) /\ exists ff_q_pfp_gaussianfactorizationmatchedbijectionboundedentry. (u) = ff_q_pfp_gaussianfactorizationmatchedbijectionboundedentry * S ((S (pfp_i_gaussianfactorizationmatchedbijectionbounded)) * (v)) + (pfp_a_gaussianfactorizationmatchedbijectionbounded))) /\ (exists pfp_gap_gaussianfactorizationmatchedbijectionboundedvalue. pfp_gap_gaussianfactorizationmatchedbijectionboundedvalue + S (pfp_a_gaussianfactorizationmatchedbijectionbounded) = ((l)))) /\ (((forall pfp_i_gaussianfactorizationmatchedbijectioninjective pfp_j_gaussianfactorizationmatchedbijectioninjective pfp_a_gaussianfactorizationmatchedbijectioninjective. (exists pfp_gap_gaussianfactorizationmatchedbijectioninjectivefirst. pfp_gap_gaussianfactorizationmatchedbijectioninjectivefirst + S (pfp_i_gaussianfactorizationmatchedbijectioninjective) = ((l))) -> (exists pfp_gap_gaussianfactorizationmatchedbijectioninjectivesecond. pfp_gap_gaussianfactorizationmatchedbijectioninjectivesecond + S (pfp_j_gaussianfactorizationmatchedbijectioninjective) = ((l))) -> (((exists ff_h_pfp_gaussianfactorizationmatchedbijectioninjectiveleft. ff_h_pfp_gaussianfactorizationmatchedbijectioninjectiveleft + S (pfp_a_gaussianfactorizationmatchedbijectioninjective) = S ((S (pfp_i_gaussianfactorizationmatchedbijectioninjective)) * (v))) /\ exists ff_q_pfp_gaussianfactorizationmatchedbijectioninjectiveleft. (u) = ff_q_pfp_gaussianfactorizationmatchedbijectioninjectiveleft * S ((S (pfp_i_gaussianfactorizationmatchedbijectioninjective)) * (v)) + (pfp_a_gaussianfactorizationmatchedbijectioninjective))) -> (((exists ff_h_pfp_gaussianfactorizationmatchedbijectioninjectiveright. ff_h_pfp_gaussianfactorizationmatchedbijectioninjectiveright + S (pfp_a_gaussianfactorizationmatchedbijectioninjective) = S ((S (pfp_j_gaussianfactorizationmatchedbijectioninjective)) * (v))) /\ exists ff_q_pfp_gaussianfactorizationmatchedbijectioninjectiveright. (u) = ff_q_pfp_gaussianfactorizationmatchedbijectioninjectiveright * S ((S (pfp_j_gaussianfactorizationmatchedbijectioninjective)) * (v)) + (pfp_a_gaussianfactorizationmatchedbijectioninjective))) -> pfp_i_gaussianfactorizationmatchedbijectioninjective = pfp_j_gaussianfactorizationmatchedbijectioninjective) /\ (forall pfp_a_gaussianfactorizationmatchedbijectionsurjective. (exists pfp_gap_gaussianfactorizationmatchedbijectionsurjectivevalue. pfp_gap_gaussianfactorizationmatchedbijectionsurjectivevalue + S (pfp_a_gaussianfactorizationmatchedbijectionsurjective) = ((l))) -> exists pfp_i_gaussianfactorizationmatchedbijectionsurjective. (exists pfp_gap_gaussianfactorizationmatchedbijectionsurjectiveindex. pfp_gap_gaussianfactorizationmatchedbijectionsurjectiveindex + S (pfp_i_gaussianfactorizationmatchedbijectionsurjective) = ((l))) /\ (((exists ff_h_pfp_gaussianfactorizationmatchedbijectionsurjectiveentry. ff_h_pfp_gaussianfactorizationmatchedbijectionsurjectiveentry + S (pfp_a_gaussianfactorizationmatchedbijectionsurjective) = S ((S (pfp_i_gaussianfactorizationmatchedbijectionsurjective)) * (v))) /\ exists ff_q_pfp_gaussianfactorizationmatchedbijectionsurjectiveentry. (u) = ff_q_pfp_gaussianfactorizationmatchedbijectionsurjectiveentry * S ((S (pfp_i_gaussianfactorizationmatchedbijectionsurjective)) * (v)) + (pfp_a_gaussianfactorizationmatchedbijectionsurjective)))))))) /\ (forall gr_match_index_gaussianfactorizationmatchedmatching gr_match_image_gaussianfactorizationmatchedmatching gr_match_source_gaussianfactorizationmatchedmatching gr_match_target_gaussianfactorizationmatchedmatching. (exists ge_gap_gaussianfactorizationmatchedmatchingindex. ge_gap_gaussianfactorizationmatchedmatchingindex + S (gr_match_index_gaussianfactorizationmatchedmatching) = ((l))) -> (((exists ff_h_gprod_gaussianfactorizationmatchedmatchingmap. ff_h_gprod_gaussianfactorizationmatchedmatchingmap + S (gr_match_image_gaussianfactorizationmatchedmatching) = S ((S (gr_match_index_gaussianfactorizationmatchedmatching)) * (v))) /\ exists ff_q_gprod_gaussianfactorizationmatchedmatchingmap. (u) = ff_q_gprod_gaussianfactorizationmatchedmatchingmap * S ((S (gr_match_index_gaussianfactorizationmatchedmatching)) * (v)) + (gr_match_image_gaussianfactorizationmatchedmatching))) -> (((exists ff_h_gprod_gaussianfactorizationmatchedmatchingsource. ff_h_gprod_gaussianfactorizationmatchedmatchingsource + S (gr_match_source_gaussianfactorizationmatchedmatching) = S ((S (gr_match_index_gaussianfactorizationmatchedmatching)) * (c))) /\ exists ff_q_gprod_gaussianfactorizationmatchedmatchingsource. (b) = ff_q_gprod_gaussianfactorizationmatchedmatchingsource * S ((S (gr_match_index_gaussianfactorizationmatchedmatching)) * (c)) + (gr_match_source_gaussianfactorizationmatchedmatching))) -> (((exists ff_h_gprod_gaussianfactorizationmatchedmatchingtarget. ff_h_gprod_gaussianfactorizationmatchedmatchingtarget + S (gr_match_target_gaussianfactorizationmatchedmatching) = S ((S (gr_match_image_gaussianfactorizationmatchedmatching)) * (e))) /\ exists ff_q_gprod_gaussianfactorizationmatchedmatchingtarget. (d) = ff_q_gprod_gaussianfactorizationmatchedmatchingtarget * S ((S (gr_match_image_gaussianfactorizationmatchedmatching)) * (e)) + (gr_match_target_gaussianfactorizationmatchedmatching))) -> (exists gr_unit_gaussianfactorizationmatchedmatchingunit_witness. ((exists gr_inverse_gaussianfactorizationmatchedmatchingunit_witnessunit. (exists ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity ge_first_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity ge_second_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst. (((gr_unit_gaussianfactorizationmatchedmatchingunit_witness) = ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstreal ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond. (((gr_inverse_gaussianfactorizationmatchedmatchingunit_witnessunit) = ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondreal ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputreal ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))))))) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))))))) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))))))) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))) + (((ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))) + (((ge_first_in_gaussianfactorizationmatchedmatchingunit_witnessunitidentity) * (ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnessunitidentity))))))) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport ge_first_in_gaussianfactorizationmatchedmatchingunit_witnesstransport ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport ge_second_in_gaussianfactorizationmatchedmatchingunit_witnesstransport. ((exists ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst. (((gr_unit_gaussianfactorizationmatchedmatchingunit_witness) = ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstreal ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstreal) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstreal = (ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginary ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginary = (ge_first_in_gaussianfactorizationmatchedmatchingunit_witnesstransport) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond. (((gr_match_source_gaussianfactorizationmatchedmatching) = ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondreal ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondreal) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondreal = (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginary ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginary = (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnesstransport) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput. (((gr_match_target_gaussianfactorizationmatchedmatching) = ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputreal ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputreal) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport))))))) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnesstransport))))))) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginary ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationmatchedmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport))))))) + ge_balance_negative_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_in_gaussianfactorizationmatchedmatchingunit_witnesstransport))) + (((ge_first_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport))))) + (((((ge_first_ip_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_rn_gaussianfactorizationmatchedmatchingunit_witnesstransport))) + (((ge_first_in_gaussianfactorizationmatchedmatchingunit_witnesstransport) * (ge_second_rp_gaussianfactorizationmatchedmatchingunit_witnesstransport))))))) + ge_balance_positive_gaussianfactorizationmatchedmatchingunit_witnesstransportoutputimaginary)))))))))))))))

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