gaussian_factor_matching_unswap

Exact expanded first-order arithmetic statement

forall b c d e D E u v U V l i j p q. (exists ge_gap_unswap_source_index. ge_gap_unswap_source_index + S (i) = (l)) -> (exists ge_gap_unswap_target_index. ge_gap_unswap_target_index + S (j) = (l)) -> (((forall pfp_i_unswap_old_bijectionbounded. (exists pfp_gap_unswap_old_bijectionboundedindex. pfp_gap_unswap_old_bijectionboundedindex + S (pfp_i_unswap_old_bijectionbounded) = (S l)) -> exists pfp_a_unswap_old_bijectionbounded. (((exists ff_h_pfp_unswap_old_bijectionboundedentry. ff_h_pfp_unswap_old_bijectionboundedentry + S (pfp_a_unswap_old_bijectionbounded) = S ((S (pfp_i_unswap_old_bijectionbounded)) * v)) /\ exists ff_q_pfp_unswap_old_bijectionboundedentry. u = ff_q_pfp_unswap_old_bijectionboundedentry * S ((S (pfp_i_unswap_old_bijectionbounded)) * v) + (pfp_a_unswap_old_bijectionbounded))) /\ (exists pfp_gap_unswap_old_bijectionboundedvalue. pfp_gap_unswap_old_bijectionboundedvalue + S (pfp_a_unswap_old_bijectionbounded) = (S l))) /\ (((forall pfp_i_unswap_old_bijectioninjective pfp_j_unswap_old_bijectioninjective pfp_a_unswap_old_bijectioninjective. (exists pfp_gap_unswap_old_bijectioninjectivefirst. pfp_gap_unswap_old_bijectioninjectivefirst + S (pfp_i_unswap_old_bijectioninjective) = (S l)) -> (exists pfp_gap_unswap_old_bijectioninjectivesecond. pfp_gap_unswap_old_bijectioninjectivesecond + S (pfp_j_unswap_old_bijectioninjective) = (S l)) -> (((exists ff_h_pfp_unswap_old_bijectioninjectiveleft. ff_h_pfp_unswap_old_bijectioninjectiveleft + S (pfp_a_unswap_old_bijectioninjective) = S ((S (pfp_i_unswap_old_bijectioninjective)) * v)) /\ exists ff_q_pfp_unswap_old_bijectioninjectiveleft. u = ff_q_pfp_unswap_old_bijectioninjectiveleft * S ((S (pfp_i_unswap_old_bijectioninjective)) * v) + (pfp_a_unswap_old_bijectioninjective))) -> (((exists ff_h_pfp_unswap_old_bijectioninjectiveright. ff_h_pfp_unswap_old_bijectioninjectiveright + S (pfp_a_unswap_old_bijectioninjective) = S ((S (pfp_j_unswap_old_bijectioninjective)) * v)) /\ exists ff_q_pfp_unswap_old_bijectioninjectiveright. u = ff_q_pfp_unswap_old_bijectioninjectiveright * S ((S (pfp_j_unswap_old_bijectioninjective)) * v) + (pfp_a_unswap_old_bijectioninjective))) -> pfp_i_unswap_old_bijectioninjective = pfp_j_unswap_old_bijectioninjective) /\ (forall pfp_a_unswap_old_bijectionsurjective. (exists pfp_gap_unswap_old_bijectionsurjectivevalue. pfp_gap_unswap_old_bijectionsurjectivevalue + S (pfp_a_unswap_old_bijectionsurjective) = (S l)) -> exists pfp_i_unswap_old_bijectionsurjective. (exists pfp_gap_unswap_old_bijectionsurjectiveindex. pfp_gap_unswap_old_bijectionsurjectiveindex + S (pfp_i_unswap_old_bijectionsurjective) = (S l)) /\ (((exists ff_h_pfp_unswap_old_bijectionsurjectiveentry. ff_h_pfp_unswap_old_bijectionsurjectiveentry + S (pfp_a_unswap_old_bijectionsurjective) = S ((S (pfp_i_unswap_old_bijectionsurjective)) * v)) /\ exists ff_q_pfp_unswap_old_bijectionsurjectiveentry. u = ff_q_pfp_unswap_old_bijectionsurjectiveentry * S ((S (pfp_i_unswap_old_bijectionsurjective)) * v) + (pfp_a_unswap_old_bijectionsurjective)))))))) -> (forall gr_match_index_unswap_old_matching gr_match_image_unswap_old_matching gr_match_source_unswap_old_matching gr_match_target_unswap_old_matching. (exists ge_gap_unswap_old_matchingindex. ge_gap_unswap_old_matchingindex + S (gr_match_index_unswap_old_matching) = (S l)) -> (((exists ff_h_gprod_unswap_old_matchingmap. ff_h_gprod_unswap_old_matchingmap + S (gr_match_image_unswap_old_matching) = S ((S (gr_match_index_unswap_old_matching)) * v)) /\ exists ff_q_gprod_unswap_old_matchingmap. u = ff_q_gprod_unswap_old_matchingmap * S ((S (gr_match_index_unswap_old_matching)) * v) + (gr_match_image_unswap_old_matching))) -> (((exists ff_h_gprod_unswap_old_matchingsource. ff_h_gprod_unswap_old_matchingsource + S (gr_match_source_unswap_old_matching) = S ((S (gr_match_index_unswap_old_matching)) * c)) /\ exists ff_q_gprod_unswap_old_matchingsource. b = ff_q_gprod_unswap_old_matchingsource * S ((S (gr_match_index_unswap_old_matching)) * c) + (gr_match_source_unswap_old_matching))) -> (((exists ff_h_gprod_unswap_old_matchingtarget. ff_h_gprod_unswap_old_matchingtarget + S (gr_match_target_unswap_old_matching) = S ((S (gr_match_image_unswap_old_matching)) * E)) /\ exists ff_q_gprod_unswap_old_matchingtarget. D = ff_q_gprod_unswap_old_matchingtarget * S ((S (gr_match_image_unswap_old_matching)) * E) + (gr_match_target_unswap_old_matching))) -> (exists gr_unit_unswap_old_matchingunit_witness. ((exists gr_inverse_unswap_old_matchingunit_witnessunit. (exists ge_first_rp_unswap_old_matchingunit_witnessunitidentity ge_first_rn_unswap_old_matchingunit_witnessunitidentity ge_first_ip_unswap_old_matchingunit_witnessunitidentity ge_first_in_unswap_old_matchingunit_witnessunitidentity ge_second_rp_unswap_old_matchingunit_witnessunitidentity ge_second_rn_unswap_old_matchingunit_witnessunitidentity ge_second_ip_unswap_old_matchingunit_witnessunitidentity ge_second_in_unswap_old_matchingunit_witnessunitidentity. ((exists ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityfirst ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityfirst. (((gr_unit_unswap_old_matchingunit_witness) = ((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_unswap_old_matchingunit_witnessunitidentityfirstreal ge_balance_negative_unswap_old_matchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unswap_old_matchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentityfirstreal) = S ge_signed_half_unswap_old_matchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_unswap_old_matchingunit_witnessunitidentity) + ge_balance_negative_unswap_old_matchingunit_witnessunitidentityfirstreal = (ge_first_rn_unswap_old_matchingunit_witnessunitidentity) + ge_balance_positive_unswap_old_matchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_unswap_old_matchingunit_witnessunitidentityfirstimaginary ge_balance_negative_unswap_old_matchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unswap_old_matchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_unswap_old_matchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unswap_old_matchingunit_witnessunitidentity) + ge_balance_negative_unswap_old_matchingunit_witnessunitidentityfirstimaginary = (ge_first_in_unswap_old_matchingunit_witnessunitidentity) + ge_balance_positive_unswap_old_matchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_old_matchingunit_witnessunitidentitysecond ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentitysecond. (((gr_inverse_unswap_old_matchingunit_witnessunit) = ((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_unswap_old_matchingunit_witnessunitidentitysecondreal ge_balance_negative_unswap_old_matchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unswap_old_matchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentitysecondreal) = S ge_signed_half_unswap_old_matchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_unswap_old_matchingunit_witnessunitidentity) + ge_balance_negative_unswap_old_matchingunit_witnessunitidentitysecondreal = (ge_second_rn_unswap_old_matchingunit_witnessunitidentity) + ge_balance_positive_unswap_old_matchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_unswap_old_matchingunit_witnessunitidentitysecondimaginary ge_balance_negative_unswap_old_matchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unswap_old_matchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_unswap_old_matchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unswap_old_matchingunit_witnessunitidentity) + ge_balance_negative_unswap_old_matchingunit_witnessunitidentitysecondimaginary = (ge_second_in_unswap_old_matchingunit_witnessunitidentity) + ge_balance_positive_unswap_old_matchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityoutput ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_unswap_old_matchingunit_witnessunitidentityoutputreal ge_balance_negative_unswap_old_matchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_unswap_old_matchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unswap_old_matchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentityoutputreal) = S ge_signed_half_unswap_old_matchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_old_matchingunit_witnessunitidentity) * (ge_second_rp_unswap_old_matchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_old_matchingunit_witnessunitidentity) * (ge_second_rn_unswap_old_matchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_old_matchingunit_witnessunitidentity) * (ge_second_in_unswap_old_matchingunit_witnessunitidentity))) + (((ge_first_in_unswap_old_matchingunit_witnessunitidentity) * (ge_second_ip_unswap_old_matchingunit_witnessunitidentity))))))) + ge_balance_negative_unswap_old_matchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_unswap_old_matchingunit_witnessunitidentity) * (ge_second_rn_unswap_old_matchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_old_matchingunit_witnessunitidentity) * (ge_second_rp_unswap_old_matchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_old_matchingunit_witnessunitidentity) * (ge_second_ip_unswap_old_matchingunit_witnessunitidentity))) + (((ge_first_in_unswap_old_matchingunit_witnessunitidentity) * (ge_second_in_unswap_old_matchingunit_witnessunitidentity))))))) + ge_balance_positive_unswap_old_matchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_unswap_old_matchingunit_witnessunitidentityoutputimaginary ge_balance_negative_unswap_old_matchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_old_matchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unswap_old_matchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_unswap_old_matchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_old_matchingunit_witnessunitidentity) * (ge_second_ip_unswap_old_matchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_old_matchingunit_witnessunitidentity) * (ge_second_in_unswap_old_matchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_old_matchingunit_witnessunitidentity) * (ge_second_rp_unswap_old_matchingunit_witnessunitidentity))) + (((ge_first_in_unswap_old_matchingunit_witnessunitidentity) * (ge_second_rn_unswap_old_matchingunit_witnessunitidentity))))))) + ge_balance_negative_unswap_old_matchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_unswap_old_matchingunit_witnessunitidentity) * (ge_second_in_unswap_old_matchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_old_matchingunit_witnessunitidentity) * (ge_second_ip_unswap_old_matchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_old_matchingunit_witnessunitidentity) * (ge_second_rn_unswap_old_matchingunit_witnessunitidentity))) + (((ge_first_in_unswap_old_matchingunit_witnessunitidentity) * (ge_second_rp_unswap_old_matchingunit_witnessunitidentity))))))) + ge_balance_positive_unswap_old_matchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_unswap_old_matchingunit_witnesstransport ge_first_rn_unswap_old_matchingunit_witnesstransport ge_first_ip_unswap_old_matchingunit_witnesstransport ge_first_in_unswap_old_matchingunit_witnesstransport ge_second_rp_unswap_old_matchingunit_witnesstransport ge_second_rn_unswap_old_matchingunit_witnesstransport ge_second_ip_unswap_old_matchingunit_witnesstransport ge_second_in_unswap_old_matchingunit_witnesstransport. ((exists ge_representation_real_code_unswap_old_matchingunit_witnesstransportfirst ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportfirst. (((gr_unit_unswap_old_matchingunit_witness) = ((ge_representation_real_code_unswap_old_matchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_unswap_old_matchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_unswap_old_matchingunit_witnesstransportfirstreal ge_balance_negative_unswap_old_matchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_unswap_old_matchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_unswap_old_matchingunit_witnesstransportfirst) = 2 * ge_signed_half_unswap_old_matchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportfirstreal) = S ge_signed_half_unswap_old_matchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_unswap_old_matchingunit_witnesstransport) + ge_balance_negative_unswap_old_matchingunit_witnesstransportfirstreal = (ge_first_rn_unswap_old_matchingunit_witnesstransport) + ge_balance_positive_unswap_old_matchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_unswap_old_matchingunit_witnesstransportfirstimaginary ge_balance_negative_unswap_old_matchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportfirst) = 2 * ge_signed_half_unswap_old_matchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportfirstimaginary) = S ge_signed_half_unswap_old_matchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_unswap_old_matchingunit_witnesstransport) + ge_balance_negative_unswap_old_matchingunit_witnesstransportfirstimaginary = (ge_first_in_unswap_old_matchingunit_witnesstransport) + ge_balance_positive_unswap_old_matchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_old_matchingunit_witnesstransportsecond ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportsecond. (((gr_match_source_unswap_old_matching) = ((ge_representation_real_code_unswap_old_matchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_unswap_old_matchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_unswap_old_matchingunit_witnesstransportsecondreal ge_balance_negative_unswap_old_matchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_unswap_old_matchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_unswap_old_matchingunit_witnesstransportsecond) = 2 * ge_signed_half_unswap_old_matchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportsecondreal) = S ge_signed_half_unswap_old_matchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_unswap_old_matchingunit_witnesstransport) + ge_balance_negative_unswap_old_matchingunit_witnesstransportsecondreal = (ge_second_rn_unswap_old_matchingunit_witnesstransport) + ge_balance_positive_unswap_old_matchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_unswap_old_matchingunit_witnesstransportsecondimaginary ge_balance_negative_unswap_old_matchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportsecond) = 2 * ge_signed_half_unswap_old_matchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportsecondimaginary) = S ge_signed_half_unswap_old_matchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_unswap_old_matchingunit_witnesstransport) + ge_balance_negative_unswap_old_matchingunit_witnesstransportsecondimaginary = (ge_second_in_unswap_old_matchingunit_witnesstransport) + ge_balance_positive_unswap_old_matchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_old_matchingunit_witnesstransportoutput ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportoutput. (((gr_match_target_unswap_old_matching) = ((ge_representation_real_code_unswap_old_matchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_unswap_old_matchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_unswap_old_matchingunit_witnesstransportoutputreal ge_balance_negative_unswap_old_matchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_unswap_old_matchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_unswap_old_matchingunit_witnesstransportoutput) = 2 * ge_signed_half_unswap_old_matchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportoutputreal) = S ge_signed_half_unswap_old_matchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_old_matchingunit_witnesstransport) * (ge_second_rp_unswap_old_matchingunit_witnesstransport))) + (((ge_first_rn_unswap_old_matchingunit_witnesstransport) * (ge_second_rn_unswap_old_matchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_old_matchingunit_witnesstransport) * (ge_second_in_unswap_old_matchingunit_witnesstransport))) + (((ge_first_in_unswap_old_matchingunit_witnesstransport) * (ge_second_ip_unswap_old_matchingunit_witnesstransport))))))) + ge_balance_negative_unswap_old_matchingunit_witnesstransportoutputreal = (((((((ge_first_rp_unswap_old_matchingunit_witnesstransport) * (ge_second_rn_unswap_old_matchingunit_witnesstransport))) + (((ge_first_rn_unswap_old_matchingunit_witnesstransport) * (ge_second_rp_unswap_old_matchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_old_matchingunit_witnesstransport) * (ge_second_ip_unswap_old_matchingunit_witnesstransport))) + (((ge_first_in_unswap_old_matchingunit_witnesstransport) * (ge_second_in_unswap_old_matchingunit_witnesstransport))))))) + ge_balance_positive_unswap_old_matchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_unswap_old_matchingunit_witnesstransportoutputimaginary ge_balance_negative_unswap_old_matchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unswap_old_matchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_unswap_old_matchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_old_matchingunit_witnesstransportoutput) = 2 * ge_signed_half_unswap_old_matchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_old_matchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_unswap_old_matchingunit_witnesstransportoutputimaginary) = S ge_signed_half_unswap_old_matchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_old_matchingunit_witnesstransport) * (ge_second_ip_unswap_old_matchingunit_witnesstransport))) + (((ge_first_rn_unswap_old_matchingunit_witnesstransport) * (ge_second_in_unswap_old_matchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_old_matchingunit_witnesstransport) * (ge_second_rp_unswap_old_matchingunit_witnesstransport))) + (((ge_first_in_unswap_old_matchingunit_witnesstransport) * (ge_second_rn_unswap_old_matchingunit_witnesstransport))))))) + ge_balance_negative_unswap_old_matchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_unswap_old_matchingunit_witnesstransport) * (ge_second_in_unswap_old_matchingunit_witnesstransport))) + (((ge_first_rn_unswap_old_matchingunit_witnesstransport) * (ge_second_ip_unswap_old_matchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_old_matchingunit_witnesstransport) * (ge_second_rn_unswap_old_matchingunit_witnesstransport))) + (((ge_first_in_unswap_old_matchingunit_witnesstransport) * (ge_second_rp_unswap_old_matchingunit_witnesstransport))))))) + ge_balance_positive_unswap_old_matchingunit_witnesstransportoutputimaginary)))))))))))) -> (((((exists ff_h_pfp_matching_target_swapoldi. ff_h_pfp_matching_target_swapoldi + S (p) = S ((S (j)) * e)) /\ exists ff_q_pfp_matching_target_swapoldi. d = ff_q_pfp_matching_target_swapoldi * S ((S (j)) * e) + (p))) /\ (((((exists ff_h_pfp_matching_target_swapoldlast. ff_h_pfp_matching_target_swapoldlast + S (q) = S ((S (l)) * e)) /\ exists ff_q_pfp_matching_target_swapoldlast. d = ff_q_pfp_matching_target_swapoldlast * S ((S (l)) * e) + (q))) /\ (((((exists ff_h_pfp_matching_target_swapnewi. ff_h_pfp_matching_target_swapnewi + S (q) = S ((S (j)) * E)) /\ exists ff_q_pfp_matching_target_swapnewi. D = ff_q_pfp_matching_target_swapnewi * S ((S (j)) * E) + (q))) /\ (((((exists ff_h_pfp_matching_target_swapnewlast. ff_h_pfp_matching_target_swapnewlast + S (p) = S ((S (l)) * E)) /\ exists ff_q_pfp_matching_target_swapnewlast. D = ff_q_pfp_matching_target_swapnewlast * S ((S (l)) * E) + (p))) /\ (forall pfp_j_matching_target_swap pfp_a_matching_target_swap. (exists pfp_gap_matching_target_swapbound. pfp_gap_matching_target_swapbound + S (pfp_j_matching_target_swap) = (S (l))) -> ~(pfp_j_matching_target_swap = j) -> ~(pfp_j_matching_target_swap = l) -> (((exists ff_h_pfp_matching_target_swapold. ff_h_pfp_matching_target_swapold + S (pfp_a_matching_target_swap) = S ((S (pfp_j_matching_target_swap)) * e)) /\ exists ff_q_pfp_matching_target_swapold. d = ff_q_pfp_matching_target_swapold * S ((S (pfp_j_matching_target_swap)) * e) + (pfp_a_matching_target_swap))) -> (((exists ff_h_pfp_matching_target_swapnew. ff_h_pfp_matching_target_swapnew + S (pfp_a_matching_target_swap) = S ((S (pfp_j_matching_target_swap)) * E)) /\ exists ff_q_pfp_matching_target_swapnew. D = ff_q_pfp_matching_target_swapnew * S ((S (pfp_j_matching_target_swap)) * E) + (pfp_a_matching_target_swap)))))))))))) -> (((((exists ff_h_pfp_matching_map_swapoldi. ff_h_pfp_matching_map_swapoldi + S (j) = S ((S (i)) * v)) /\ exists ff_q_pfp_matching_map_swapoldi. u = ff_q_pfp_matching_map_swapoldi * S ((S (i)) * v) + (j))) /\ (((((exists ff_h_pfp_matching_map_swapoldlast. ff_h_pfp_matching_map_swapoldlast + S (l) = S ((S (l)) * v)) /\ exists ff_q_pfp_matching_map_swapoldlast. u = ff_q_pfp_matching_map_swapoldlast * S ((S (l)) * v) + (l))) /\ (((((exists ff_h_pfp_matching_map_swapnewi. ff_h_pfp_matching_map_swapnewi + S (l) = S ((S (i)) * V)) /\ exists ff_q_pfp_matching_map_swapnewi. U = ff_q_pfp_matching_map_swapnewi * S ((S (i)) * V) + (l))) /\ (((((exists ff_h_pfp_matching_map_swapnewlast. ff_h_pfp_matching_map_swapnewlast + S (j) = S ((S (l)) * V)) /\ exists ff_q_pfp_matching_map_swapnewlast. U = ff_q_pfp_matching_map_swapnewlast * S ((S (l)) * V) + (j))) /\ (forall pfp_j_matching_map_swap pfp_a_matching_map_swap. (exists pfp_gap_matching_map_swapbound. pfp_gap_matching_map_swapbound + S (pfp_j_matching_map_swap) = (S (l))) -> ~(pfp_j_matching_map_swap = i) -> ~(pfp_j_matching_map_swap = l) -> (((exists ff_h_pfp_matching_map_swapold. ff_h_pfp_matching_map_swapold + S (pfp_a_matching_map_swap) = S ((S (pfp_j_matching_map_swap)) * v)) /\ exists ff_q_pfp_matching_map_swapold. u = ff_q_pfp_matching_map_swapold * S ((S (pfp_j_matching_map_swap)) * v) + (pfp_a_matching_map_swap))) -> (((exists ff_h_pfp_matching_map_swapnew. ff_h_pfp_matching_map_swapnew + S (pfp_a_matching_map_swap) = S ((S (pfp_j_matching_map_swap)) * V)) /\ exists ff_q_pfp_matching_map_swapnew. U = ff_q_pfp_matching_map_swapnew * S ((S (pfp_j_matching_map_swap)) * V) + (pfp_a_matching_map_swap)))))))))))) -> (forall gr_match_index_unswap_new_matching gr_match_image_unswap_new_matching gr_match_source_unswap_new_matching gr_match_target_unswap_new_matching. (exists ge_gap_unswap_new_matchingindex. ge_gap_unswap_new_matchingindex + S (gr_match_index_unswap_new_matching) = (S l)) -> (((exists ff_h_gprod_unswap_new_matchingmap. ff_h_gprod_unswap_new_matchingmap + S (gr_match_image_unswap_new_matching) = S ((S (gr_match_index_unswap_new_matching)) * V)) /\ exists ff_q_gprod_unswap_new_matchingmap. U = ff_q_gprod_unswap_new_matchingmap * S ((S (gr_match_index_unswap_new_matching)) * V) + (gr_match_image_unswap_new_matching))) -> (((exists ff_h_gprod_unswap_new_matchingsource. ff_h_gprod_unswap_new_matchingsource + S (gr_match_source_unswap_new_matching) = S ((S (gr_match_index_unswap_new_matching)) * c)) /\ exists ff_q_gprod_unswap_new_matchingsource. b = ff_q_gprod_unswap_new_matchingsource * S ((S (gr_match_index_unswap_new_matching)) * c) + (gr_match_source_unswap_new_matching))) -> (((exists ff_h_gprod_unswap_new_matchingtarget. ff_h_gprod_unswap_new_matchingtarget + S (gr_match_target_unswap_new_matching) = S ((S (gr_match_image_unswap_new_matching)) * e)) /\ exists ff_q_gprod_unswap_new_matchingtarget. d = ff_q_gprod_unswap_new_matchingtarget * S ((S (gr_match_image_unswap_new_matching)) * e) + (gr_match_target_unswap_new_matching))) -> (exists gr_unit_unswap_new_matchingunit_witness. ((exists gr_inverse_unswap_new_matchingunit_witnessunit. (exists ge_first_rp_unswap_new_matchingunit_witnessunitidentity ge_first_rn_unswap_new_matchingunit_witnessunitidentity ge_first_ip_unswap_new_matchingunit_witnessunitidentity ge_first_in_unswap_new_matchingunit_witnessunitidentity ge_second_rp_unswap_new_matchingunit_witnessunitidentity ge_second_rn_unswap_new_matchingunit_witnessunitidentity ge_second_ip_unswap_new_matchingunit_witnessunitidentity ge_second_in_unswap_new_matchingunit_witnessunitidentity. ((exists ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityfirst ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityfirst. (((gr_unit_unswap_new_matchingunit_witness) = ((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_unswap_new_matchingunit_witnessunitidentityfirstreal ge_balance_negative_unswap_new_matchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unswap_new_matchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentityfirstreal) = S ge_signed_half_unswap_new_matchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_unswap_new_matchingunit_witnessunitidentity) + ge_balance_negative_unswap_new_matchingunit_witnessunitidentityfirstreal = (ge_first_rn_unswap_new_matchingunit_witnessunitidentity) + ge_balance_positive_unswap_new_matchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_unswap_new_matchingunit_witnessunitidentityfirstimaginary ge_balance_negative_unswap_new_matchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unswap_new_matchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_unswap_new_matchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unswap_new_matchingunit_witnessunitidentity) + ge_balance_negative_unswap_new_matchingunit_witnessunitidentityfirstimaginary = (ge_first_in_unswap_new_matchingunit_witnessunitidentity) + ge_balance_positive_unswap_new_matchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_new_matchingunit_witnessunitidentitysecond ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentitysecond. (((gr_inverse_unswap_new_matchingunit_witnessunit) = ((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_unswap_new_matchingunit_witnessunitidentitysecondreal ge_balance_negative_unswap_new_matchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unswap_new_matchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentitysecondreal) = S ge_signed_half_unswap_new_matchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_unswap_new_matchingunit_witnessunitidentity) + ge_balance_negative_unswap_new_matchingunit_witnessunitidentitysecondreal = (ge_second_rn_unswap_new_matchingunit_witnessunitidentity) + ge_balance_positive_unswap_new_matchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_unswap_new_matchingunit_witnessunitidentitysecondimaginary ge_balance_negative_unswap_new_matchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unswap_new_matchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_unswap_new_matchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unswap_new_matchingunit_witnessunitidentity) + ge_balance_negative_unswap_new_matchingunit_witnessunitidentitysecondimaginary = (ge_second_in_unswap_new_matchingunit_witnessunitidentity) + ge_balance_positive_unswap_new_matchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityoutput ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_unswap_new_matchingunit_witnessunitidentityoutputreal ge_balance_negative_unswap_new_matchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_unswap_new_matchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unswap_new_matchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentityoutputreal) = S ge_signed_half_unswap_new_matchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_new_matchingunit_witnessunitidentity) * (ge_second_rp_unswap_new_matchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_new_matchingunit_witnessunitidentity) * (ge_second_rn_unswap_new_matchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_new_matchingunit_witnessunitidentity) * (ge_second_in_unswap_new_matchingunit_witnessunitidentity))) + (((ge_first_in_unswap_new_matchingunit_witnessunitidentity) * (ge_second_ip_unswap_new_matchingunit_witnessunitidentity))))))) + ge_balance_negative_unswap_new_matchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_unswap_new_matchingunit_witnessunitidentity) * (ge_second_rn_unswap_new_matchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_new_matchingunit_witnessunitidentity) * (ge_second_rp_unswap_new_matchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_new_matchingunit_witnessunitidentity) * (ge_second_ip_unswap_new_matchingunit_witnessunitidentity))) + (((ge_first_in_unswap_new_matchingunit_witnessunitidentity) * (ge_second_in_unswap_new_matchingunit_witnessunitidentity))))))) + ge_balance_positive_unswap_new_matchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_unswap_new_matchingunit_witnessunitidentityoutputimaginary ge_balance_negative_unswap_new_matchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_new_matchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unswap_new_matchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_unswap_new_matchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_new_matchingunit_witnessunitidentity) * (ge_second_ip_unswap_new_matchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_new_matchingunit_witnessunitidentity) * (ge_second_in_unswap_new_matchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_new_matchingunit_witnessunitidentity) * (ge_second_rp_unswap_new_matchingunit_witnessunitidentity))) + (((ge_first_in_unswap_new_matchingunit_witnessunitidentity) * (ge_second_rn_unswap_new_matchingunit_witnessunitidentity))))))) + ge_balance_negative_unswap_new_matchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_unswap_new_matchingunit_witnessunitidentity) * (ge_second_in_unswap_new_matchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_new_matchingunit_witnessunitidentity) * (ge_second_ip_unswap_new_matchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_new_matchingunit_witnessunitidentity) * (ge_second_rn_unswap_new_matchingunit_witnessunitidentity))) + (((ge_first_in_unswap_new_matchingunit_witnessunitidentity) * (ge_second_rp_unswap_new_matchingunit_witnessunitidentity))))))) + ge_balance_positive_unswap_new_matchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_unswap_new_matchingunit_witnesstransport ge_first_rn_unswap_new_matchingunit_witnesstransport ge_first_ip_unswap_new_matchingunit_witnesstransport ge_first_in_unswap_new_matchingunit_witnesstransport ge_second_rp_unswap_new_matchingunit_witnesstransport ge_second_rn_unswap_new_matchingunit_witnesstransport ge_second_ip_unswap_new_matchingunit_witnesstransport ge_second_in_unswap_new_matchingunit_witnesstransport. ((exists ge_representation_real_code_unswap_new_matchingunit_witnesstransportfirst ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportfirst. (((gr_unit_unswap_new_matchingunit_witness) = ((ge_representation_real_code_unswap_new_matchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_unswap_new_matchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_unswap_new_matchingunit_witnesstransportfirstreal ge_balance_negative_unswap_new_matchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_unswap_new_matchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_unswap_new_matchingunit_witnesstransportfirst) = 2 * ge_signed_half_unswap_new_matchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportfirstreal) = S ge_signed_half_unswap_new_matchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_unswap_new_matchingunit_witnesstransport) + ge_balance_negative_unswap_new_matchingunit_witnesstransportfirstreal = (ge_first_rn_unswap_new_matchingunit_witnesstransport) + ge_balance_positive_unswap_new_matchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_unswap_new_matchingunit_witnesstransportfirstimaginary ge_balance_negative_unswap_new_matchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportfirst) = 2 * ge_signed_half_unswap_new_matchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportfirstimaginary) = S ge_signed_half_unswap_new_matchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_unswap_new_matchingunit_witnesstransport) + ge_balance_negative_unswap_new_matchingunit_witnesstransportfirstimaginary = (ge_first_in_unswap_new_matchingunit_witnesstransport) + ge_balance_positive_unswap_new_matchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_new_matchingunit_witnesstransportsecond ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportsecond. (((gr_match_source_unswap_new_matching) = ((ge_representation_real_code_unswap_new_matchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_unswap_new_matchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_unswap_new_matchingunit_witnesstransportsecondreal ge_balance_negative_unswap_new_matchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_unswap_new_matchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_unswap_new_matchingunit_witnesstransportsecond) = 2 * ge_signed_half_unswap_new_matchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportsecondreal) = S ge_signed_half_unswap_new_matchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_unswap_new_matchingunit_witnesstransport) + ge_balance_negative_unswap_new_matchingunit_witnesstransportsecondreal = (ge_second_rn_unswap_new_matchingunit_witnesstransport) + ge_balance_positive_unswap_new_matchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_unswap_new_matchingunit_witnesstransportsecondimaginary ge_balance_negative_unswap_new_matchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportsecond) = 2 * ge_signed_half_unswap_new_matchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportsecondimaginary) = S ge_signed_half_unswap_new_matchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_unswap_new_matchingunit_witnesstransport) + ge_balance_negative_unswap_new_matchingunit_witnesstransportsecondimaginary = (ge_second_in_unswap_new_matchingunit_witnesstransport) + ge_balance_positive_unswap_new_matchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_new_matchingunit_witnesstransportoutput ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportoutput. (((gr_match_target_unswap_new_matching) = ((ge_representation_real_code_unswap_new_matchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_unswap_new_matchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_unswap_new_matchingunit_witnesstransportoutputreal ge_balance_negative_unswap_new_matchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_unswap_new_matchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_unswap_new_matchingunit_witnesstransportoutput) = 2 * ge_signed_half_unswap_new_matchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportoutputreal) = S ge_signed_half_unswap_new_matchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_new_matchingunit_witnesstransport) * (ge_second_rp_unswap_new_matchingunit_witnesstransport))) + (((ge_first_rn_unswap_new_matchingunit_witnesstransport) * (ge_second_rn_unswap_new_matchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_new_matchingunit_witnesstransport) * (ge_second_in_unswap_new_matchingunit_witnesstransport))) + (((ge_first_in_unswap_new_matchingunit_witnesstransport) * (ge_second_ip_unswap_new_matchingunit_witnesstransport))))))) + ge_balance_negative_unswap_new_matchingunit_witnesstransportoutputreal = (((((((ge_first_rp_unswap_new_matchingunit_witnesstransport) * (ge_second_rn_unswap_new_matchingunit_witnesstransport))) + (((ge_first_rn_unswap_new_matchingunit_witnesstransport) * (ge_second_rp_unswap_new_matchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_new_matchingunit_witnesstransport) * (ge_second_ip_unswap_new_matchingunit_witnesstransport))) + (((ge_first_in_unswap_new_matchingunit_witnesstransport) * (ge_second_in_unswap_new_matchingunit_witnesstransport))))))) + ge_balance_positive_unswap_new_matchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_unswap_new_matchingunit_witnesstransportoutputimaginary ge_balance_negative_unswap_new_matchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unswap_new_matchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_unswap_new_matchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_new_matchingunit_witnesstransportoutput) = 2 * ge_signed_half_unswap_new_matchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_new_matchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_unswap_new_matchingunit_witnesstransportoutputimaginary) = S ge_signed_half_unswap_new_matchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_new_matchingunit_witnesstransport) * (ge_second_ip_unswap_new_matchingunit_witnesstransport))) + (((ge_first_rn_unswap_new_matchingunit_witnesstransport) * (ge_second_in_unswap_new_matchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_new_matchingunit_witnesstransport) * (ge_second_rp_unswap_new_matchingunit_witnesstransport))) + (((ge_first_in_unswap_new_matchingunit_witnesstransport) * (ge_second_rn_unswap_new_matchingunit_witnesstransport))))))) + ge_balance_negative_unswap_new_matchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_unswap_new_matchingunit_witnesstransport) * (ge_second_in_unswap_new_matchingunit_witnesstransport))) + (((ge_first_rn_unswap_new_matchingunit_witnesstransport) * (ge_second_ip_unswap_new_matchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_new_matchingunit_witnesstransport) * (ge_second_rn_unswap_new_matchingunit_witnesstransport))) + (((ge_first_in_unswap_new_matchingunit_witnesstransport) * (ge_second_rp_unswap_new_matchingunit_witnesstransport))))))) + ge_balance_positive_unswap_new_matchingunit_witnesstransportoutputimaginary))))))))))))