gaussian_factor_matched_unswap_exists

Exact expanded first-order arithmetic statement

forall b c d e D E u v l j a p q. (exists ge_gap_unswap_exists_index. ge_gap_unswap_exists_index + S (j) = (l)) -> (((((forall pfp_i_unswap_exists_prefixbijectionbounded. (exists pfp_gap_unswap_exists_prefixbijectionboundedindex. pfp_gap_unswap_exists_prefixbijectionboundedindex + S (pfp_i_unswap_exists_prefixbijectionbounded) = (l)) -> exists pfp_a_unswap_exists_prefixbijectionbounded. (((exists ff_h_pfp_unswap_exists_prefixbijectionboundedentry. ff_h_pfp_unswap_exists_prefixbijectionboundedentry + S (pfp_a_unswap_exists_prefixbijectionbounded) = S ((S (pfp_i_unswap_exists_prefixbijectionbounded)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixbijectionboundedentry. u = ff_q_pfp_unswap_exists_prefixbijectionboundedentry * S ((S (pfp_i_unswap_exists_prefixbijectionbounded)) * v) + (pfp_a_unswap_exists_prefixbijectionbounded))) /\ (exists pfp_gap_unswap_exists_prefixbijectionboundedvalue. pfp_gap_unswap_exists_prefixbijectionboundedvalue + S (pfp_a_unswap_exists_prefixbijectionbounded) = (l))) /\ (((forall pfp_i_unswap_exists_prefixbijectioninjective pfp_j_unswap_exists_prefixbijectioninjective pfp_a_unswap_exists_prefixbijectioninjective. (exists pfp_gap_unswap_exists_prefixbijectioninjectivefirst. pfp_gap_unswap_exists_prefixbijectioninjectivefirst + S (pfp_i_unswap_exists_prefixbijectioninjective) = (l)) -> (exists pfp_gap_unswap_exists_prefixbijectioninjectivesecond. pfp_gap_unswap_exists_prefixbijectioninjectivesecond + S (pfp_j_unswap_exists_prefixbijectioninjective) = (l)) -> (((exists ff_h_pfp_unswap_exists_prefixbijectioninjectiveleft. ff_h_pfp_unswap_exists_prefixbijectioninjectiveleft + S (pfp_a_unswap_exists_prefixbijectioninjective) = S ((S (pfp_i_unswap_exists_prefixbijectioninjective)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixbijectioninjectiveleft. u = ff_q_pfp_unswap_exists_prefixbijectioninjectiveleft * S ((S (pfp_i_unswap_exists_prefixbijectioninjective)) * v) + (pfp_a_unswap_exists_prefixbijectioninjective))) -> (((exists ff_h_pfp_unswap_exists_prefixbijectioninjectiveright. ff_h_pfp_unswap_exists_prefixbijectioninjectiveright + S (pfp_a_unswap_exists_prefixbijectioninjective) = S ((S (pfp_j_unswap_exists_prefixbijectioninjective)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixbijectioninjectiveright. u = ff_q_pfp_unswap_exists_prefixbijectioninjectiveright * S ((S (pfp_j_unswap_exists_prefixbijectioninjective)) * v) + (pfp_a_unswap_exists_prefixbijectioninjective))) -> pfp_i_unswap_exists_prefixbijectioninjective = pfp_j_unswap_exists_prefixbijectioninjective) /\ (forall pfp_a_unswap_exists_prefixbijectionsurjective. (exists pfp_gap_unswap_exists_prefixbijectionsurjectivevalue. pfp_gap_unswap_exists_prefixbijectionsurjectivevalue + S (pfp_a_unswap_exists_prefixbijectionsurjective) = (l)) -> exists pfp_i_unswap_exists_prefixbijectionsurjective. (exists pfp_gap_unswap_exists_prefixbijectionsurjectiveindex. pfp_gap_unswap_exists_prefixbijectionsurjectiveindex + S (pfp_i_unswap_exists_prefixbijectionsurjective) = (l)) /\ (((exists ff_h_pfp_unswap_exists_prefixbijectionsurjectiveentry. ff_h_pfp_unswap_exists_prefixbijectionsurjectiveentry + S (pfp_a_unswap_exists_prefixbijectionsurjective) = S ((S (pfp_i_unswap_exists_prefixbijectionsurjective)) * v)) /\ exists ff_q_pfp_unswap_exists_prefixbijectionsurjectiveentry. u = ff_q_pfp_unswap_exists_prefixbijectionsurjectiveentry * S ((S (pfp_i_unswap_exists_prefixbijectionsurjective)) * v) + (pfp_a_unswap_exists_prefixbijectionsurjective)))))))) /\ (forall gr_match_index_unswap_exists_prefixmatching gr_match_image_unswap_exists_prefixmatching gr_match_source_unswap_exists_prefixmatching gr_match_target_unswap_exists_prefixmatching. (exists ge_gap_unswap_exists_prefixmatchingindex. ge_gap_unswap_exists_prefixmatchingindex + S (gr_match_index_unswap_exists_prefixmatching) = (l)) -> (((exists ff_h_gprod_unswap_exists_prefixmatchingmap. ff_h_gprod_unswap_exists_prefixmatchingmap + S (gr_match_image_unswap_exists_prefixmatching) = S ((S (gr_match_index_unswap_exists_prefixmatching)) * v)) /\ exists ff_q_gprod_unswap_exists_prefixmatchingmap. u = ff_q_gprod_unswap_exists_prefixmatchingmap * S ((S (gr_match_index_unswap_exists_prefixmatching)) * v) + (gr_match_image_unswap_exists_prefixmatching))) -> (((exists ff_h_gprod_unswap_exists_prefixmatchingsource. ff_h_gprod_unswap_exists_prefixmatchingsource + S (gr_match_source_unswap_exists_prefixmatching) = S ((S (gr_match_index_unswap_exists_prefixmatching)) * c)) /\ exists ff_q_gprod_unswap_exists_prefixmatchingsource. b = ff_q_gprod_unswap_exists_prefixmatchingsource * S ((S (gr_match_index_unswap_exists_prefixmatching)) * c) + (gr_match_source_unswap_exists_prefixmatching))) -> (((exists ff_h_gprod_unswap_exists_prefixmatchingtarget. ff_h_gprod_unswap_exists_prefixmatchingtarget + S (gr_match_target_unswap_exists_prefixmatching) = S ((S (gr_match_image_unswap_exists_prefixmatching)) * E)) /\ exists ff_q_gprod_unswap_exists_prefixmatchingtarget. D = ff_q_gprod_unswap_exists_prefixmatchingtarget * S ((S (gr_match_image_unswap_exists_prefixmatching)) * E) + (gr_match_target_unswap_exists_prefixmatching))) -> (exists gr_unit_unswap_exists_prefixmatchingunit_witness. ((exists gr_inverse_unswap_exists_prefixmatchingunit_witnessunit. (exists ge_first_rp_unswap_exists_prefixmatchingunit_witnessunitidentity ge_first_rn_unswap_exists_prefixmatchingunit_witnessunitidentity ge_first_ip_unswap_exists_prefixmatchingunit_witnessunitidentity ge_first_in_unswap_exists_prefixmatchingunit_witnessunitidentity ge_second_rp_unswap_exists_prefixmatchingunit_witnessunitidentity ge_second_rn_unswap_exists_prefixmatchingunit_witnessunitidentity ge_second_ip_unswap_exists_prefixmatchingunit_witnessunitidentity ge_second_in_unswap_exists_prefixmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst. (((gr_unit_unswap_exists_prefixmatchingunit_witness) = ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityfirstreal ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_unswap_exists_prefixmatchingunit_witnessunitidentity) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_unswap_exists_prefixmatchingunit_witnessunitidentity) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unswap_exists_prefixmatchingunit_witnessunitidentity) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_unswap_exists_prefixmatchingunit_witnessunitidentity) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond. (((gr_inverse_unswap_exists_prefixmatchingunit_witnessunit) = ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentitysecondreal ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_unswap_exists_prefixmatchingunit_witnessunitidentity) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_unswap_exists_prefixmatchingunit_witnessunitidentity) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unswap_exists_prefixmatchingunit_witnessunitidentity) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_unswap_exists_prefixmatchingunit_witnessunitidentity) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityoutputreal ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_rp_unswap_exists_prefixmatchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_rn_unswap_exists_prefixmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_in_unswap_exists_prefixmatchingunit_witnessunitidentity))) + (((ge_first_in_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_ip_unswap_exists_prefixmatchingunit_witnessunitidentity))))))) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_rn_unswap_exists_prefixmatchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_rp_unswap_exists_prefixmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_ip_unswap_exists_prefixmatchingunit_witnessunitidentity))) + (((ge_first_in_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_in_unswap_exists_prefixmatchingunit_witnessunitidentity))))))) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_ip_unswap_exists_prefixmatchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_in_unswap_exists_prefixmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_rp_unswap_exists_prefixmatchingunit_witnessunitidentity))) + (((ge_first_in_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_rn_unswap_exists_prefixmatchingunit_witnessunitidentity))))))) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_in_unswap_exists_prefixmatchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_ip_unswap_exists_prefixmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_rn_unswap_exists_prefixmatchingunit_witnessunitidentity))) + (((ge_first_in_unswap_exists_prefixmatchingunit_witnessunitidentity) * (ge_second_rp_unswap_exists_prefixmatchingunit_witnessunitidentity))))))) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_unswap_exists_prefixmatchingunit_witnesstransport ge_first_rn_unswap_exists_prefixmatchingunit_witnesstransport ge_first_ip_unswap_exists_prefixmatchingunit_witnesstransport ge_first_in_unswap_exists_prefixmatchingunit_witnesstransport ge_second_rp_unswap_exists_prefixmatchingunit_witnesstransport ge_second_rn_unswap_exists_prefixmatchingunit_witnesstransport ge_second_ip_unswap_exists_prefixmatchingunit_witnesstransport ge_second_in_unswap_exists_prefixmatchingunit_witnesstransport. ((exists ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportfirst ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportfirst. (((gr_unit_unswap_exists_prefixmatchingunit_witness) = ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportfirstreal ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportfirstreal) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_unswap_exists_prefixmatchingunit_witnesstransport) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportfirstreal = (ge_first_rn_unswap_exists_prefixmatchingunit_witnesstransport) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginary ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_unswap_exists_prefixmatchingunit_witnesstransport) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginary = (ge_first_in_unswap_exists_prefixmatchingunit_witnesstransport) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportsecond ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportsecond. (((gr_match_source_unswap_exists_prefixmatching) = ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportsecondreal ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportsecondreal) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_unswap_exists_prefixmatchingunit_witnesstransport) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportsecondreal = (ge_second_rn_unswap_exists_prefixmatchingunit_witnesstransport) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginary ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_unswap_exists_prefixmatchingunit_witnesstransport) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginary = (ge_second_in_unswap_exists_prefixmatchingunit_witnesstransport) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportoutput ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportoutput. (((gr_match_target_unswap_exists_prefixmatching) = ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportoutputreal ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_unswap_exists_prefixmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportoutputreal) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_rp_unswap_exists_prefixmatchingunit_witnesstransport))) + (((ge_first_rn_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_rn_unswap_exists_prefixmatchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_in_unswap_exists_prefixmatchingunit_witnesstransport))) + (((ge_first_in_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_ip_unswap_exists_prefixmatchingunit_witnesstransport))))))) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_rn_unswap_exists_prefixmatchingunit_witnesstransport))) + (((ge_first_rn_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_rp_unswap_exists_prefixmatchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_ip_unswap_exists_prefixmatchingunit_witnesstransport))) + (((ge_first_in_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_in_unswap_exists_prefixmatchingunit_witnesstransport))))))) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginary ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_prefixmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_ip_unswap_exists_prefixmatchingunit_witnesstransport))) + (((ge_first_rn_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_in_unswap_exists_prefixmatchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_rp_unswap_exists_prefixmatchingunit_witnesstransport))) + (((ge_first_in_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_rn_unswap_exists_prefixmatchingunit_witnesstransport))))))) + ge_balance_negative_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_in_unswap_exists_prefixmatchingunit_witnesstransport))) + (((ge_first_rn_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_ip_unswap_exists_prefixmatchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_rn_unswap_exists_prefixmatchingunit_witnesstransport))) + (((ge_first_in_unswap_exists_prefixmatchingunit_witnesstransport) * (ge_second_rp_unswap_exists_prefixmatchingunit_witnesstransport))))))) + ge_balance_positive_unswap_exists_prefixmatchingunit_witnesstransportoutputimaginary)))))))))))))) -> (((exists ff_h_gprod_unswap_exists_source_last. ff_h_gprod_unswap_exists_source_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_gprod_unswap_exists_source_last. b = ff_q_gprod_unswap_exists_source_last * S ((S (l)) * c) + (a))) -> (((((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 gr_unit_unswap_exists_last_associate. ((exists gr_inverse_unswap_exists_last_associateunit. (exists ge_first_rp_unswap_exists_last_associateunitidentity ge_first_rn_unswap_exists_last_associateunitidentity ge_first_ip_unswap_exists_last_associateunitidentity ge_first_in_unswap_exists_last_associateunitidentity ge_second_rp_unswap_exists_last_associateunitidentity ge_second_rn_unswap_exists_last_associateunitidentity ge_second_ip_unswap_exists_last_associateunitidentity ge_second_in_unswap_exists_last_associateunitidentity. ((exists ge_representation_real_code_unswap_exists_last_associateunitidentityfirst ge_representation_imaginary_code_unswap_exists_last_associateunitidentityfirst. (((gr_unit_unswap_exists_last_associate) = ((ge_representation_real_code_unswap_exists_last_associateunitidentityfirst) + (ge_representation_imaginary_code_unswap_exists_last_associateunitidentityfirst)) * S ((ge_representation_real_code_unswap_exists_last_associateunitidentityfirst) + (ge_representation_imaginary_code_unswap_exists_last_associateunitidentityfirst)) + ((ge_representation_imaginary_code_unswap_exists_last_associateunitidentityfirst) + (ge_representation_imaginary_code_unswap_exists_last_associateunitidentityfirst))) /\ ((exists ge_balance_positive_unswap_exists_last_associateunitidentityfirstreal ge_balance_negative_unswap_exists_last_associateunitidentityfirstreal. (((((ge_representation_real_code_unswap_exists_last_associateunitidentityfirst) = 2 * (ge_balance_positive_unswap_exists_last_associateunitidentityfirstreal) /\ (ge_balance_negative_unswap_exists_last_associateunitidentityfirstreal) = 0) \/ exists ge_signed_half_unswap_exists_last_associateunitidentityfirstrealdecode. (((ge_representation_real_code_unswap_exists_last_associateunitidentityfirst) = 2 * ge_signed_half_unswap_exists_last_associateunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unswap_exists_last_associateunitidentityfirstreal) = 0) /\ (ge_balance_negative_unswap_exists_last_associateunitidentityfirstreal) = S ge_signed_half_unswap_exists_last_associateunitidentityfirstrealdecode))) /\ ((ge_first_rp_unswap_exists_last_associateunitidentity) + ge_balance_negative_unswap_exists_last_associateunitidentityfirstreal = (ge_first_rn_unswap_exists_last_associateunitidentity) + ge_balance_positive_unswap_exists_last_associateunitidentityfirstreal))) /\ (exists ge_balance_positive_unswap_exists_last_associateunitidentityfirstimaginary ge_balance_negative_unswap_exists_last_associateunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unswap_exists_last_associateunitidentityfirst) = 2 * (ge_balance_positive_unswap_exists_last_associateunitidentityfirstimaginary) /\ (ge_balance_negative_unswap_exists_last_associateunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unswap_exists_last_associateunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_last_associateunitidentityfirst) = 2 * ge_signed_half_unswap_exists_last_associateunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_last_associateunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unswap_exists_last_associateunitidentityfirstimaginary) = S ge_signed_half_unswap_exists_last_associateunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unswap_exists_last_associateunitidentity) + ge_balance_negative_unswap_exists_last_associateunitidentityfirstimaginary = (ge_first_in_unswap_exists_last_associateunitidentity) + ge_balance_positive_unswap_exists_last_associateunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_exists_last_associateunitidentitysecond ge_representation_imaginary_code_unswap_exists_last_associateunitidentitysecond. (((gr_inverse_unswap_exists_last_associateunit) = ((ge_representation_real_code_unswap_exists_last_associateunitidentitysecond) + (ge_representation_imaginary_code_unswap_exists_last_associateunitidentitysecond)) * S ((ge_representation_real_code_unswap_exists_last_associateunitidentitysecond) + (ge_representation_imaginary_code_unswap_exists_last_associateunitidentitysecond)) + ((ge_representation_imaginary_code_unswap_exists_last_associateunitidentitysecond) + (ge_representation_imaginary_code_unswap_exists_last_associateunitidentitysecond))) /\ ((exists ge_balance_positive_unswap_exists_last_associateunitidentitysecondreal ge_balance_negative_unswap_exists_last_associateunitidentitysecondreal. (((((ge_representation_real_code_unswap_exists_last_associateunitidentitysecond) = 2 * (ge_balance_positive_unswap_exists_last_associateunitidentitysecondreal) /\ (ge_balance_negative_unswap_exists_last_associateunitidentitysecondreal) = 0) \/ exists ge_signed_half_unswap_exists_last_associateunitidentitysecondrealdecode. (((ge_representation_real_code_unswap_exists_last_associateunitidentitysecond) = 2 * ge_signed_half_unswap_exists_last_associateunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unswap_exists_last_associateunitidentitysecondreal) = 0) /\ (ge_balance_negative_unswap_exists_last_associateunitidentitysecondreal) = S ge_signed_half_unswap_exists_last_associateunitidentitysecondrealdecode))) /\ ((ge_second_rp_unswap_exists_last_associateunitidentity) + ge_balance_negative_unswap_exists_last_associateunitidentitysecondreal = (ge_second_rn_unswap_exists_last_associateunitidentity) + ge_balance_positive_unswap_exists_last_associateunitidentitysecondreal))) /\ (exists ge_balance_positive_unswap_exists_last_associateunitidentitysecondimaginary ge_balance_negative_unswap_exists_last_associateunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unswap_exists_last_associateunitidentitysecond) = 2 * (ge_balance_positive_unswap_exists_last_associateunitidentitysecondimaginary) /\ (ge_balance_negative_unswap_exists_last_associateunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unswap_exists_last_associateunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_last_associateunitidentitysecond) = 2 * ge_signed_half_unswap_exists_last_associateunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_last_associateunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unswap_exists_last_associateunitidentitysecondimaginary) = S ge_signed_half_unswap_exists_last_associateunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unswap_exists_last_associateunitidentity) + ge_balance_negative_unswap_exists_last_associateunitidentitysecondimaginary = (ge_second_in_unswap_exists_last_associateunitidentity) + ge_balance_positive_unswap_exists_last_associateunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_exists_last_associateunitidentityoutput ge_representation_imaginary_code_unswap_exists_last_associateunitidentityoutput. (((6) = ((ge_representation_real_code_unswap_exists_last_associateunitidentityoutput) + (ge_representation_imaginary_code_unswap_exists_last_associateunitidentityoutput)) * S ((ge_representation_real_code_unswap_exists_last_associateunitidentityoutput) + (ge_representation_imaginary_code_unswap_exists_last_associateunitidentityoutput)) + ((ge_representation_imaginary_code_unswap_exists_last_associateunitidentityoutput) + (ge_representation_imaginary_code_unswap_exists_last_associateunitidentityoutput))) /\ ((exists ge_balance_positive_unswap_exists_last_associateunitidentityoutputreal ge_balance_negative_unswap_exists_last_associateunitidentityoutputreal. (((((ge_representation_real_code_unswap_exists_last_associateunitidentityoutput) = 2 * (ge_balance_positive_unswap_exists_last_associateunitidentityoutputreal) /\ (ge_balance_negative_unswap_exists_last_associateunitidentityoutputreal) = 0) \/ exists ge_signed_half_unswap_exists_last_associateunitidentityoutputrealdecode. (((ge_representation_real_code_unswap_exists_last_associateunitidentityoutput) = 2 * ge_signed_half_unswap_exists_last_associateunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unswap_exists_last_associateunitidentityoutputreal) = 0) /\ (ge_balance_negative_unswap_exists_last_associateunitidentityoutputreal) = S ge_signed_half_unswap_exists_last_associateunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_exists_last_associateunitidentity) * (ge_second_rp_unswap_exists_last_associateunitidentity))) + (((ge_first_rn_unswap_exists_last_associateunitidentity) * (ge_second_rn_unswap_exists_last_associateunitidentity))))) + (((((ge_first_ip_unswap_exists_last_associateunitidentity) * (ge_second_in_unswap_exists_last_associateunitidentity))) + (((ge_first_in_unswap_exists_last_associateunitidentity) * (ge_second_ip_unswap_exists_last_associateunitidentity))))))) + ge_balance_negative_unswap_exists_last_associateunitidentityoutputreal = (((((((ge_first_rp_unswap_exists_last_associateunitidentity) * (ge_second_rn_unswap_exists_last_associateunitidentity))) + (((ge_first_rn_unswap_exists_last_associateunitidentity) * (ge_second_rp_unswap_exists_last_associateunitidentity))))) + (((((ge_first_ip_unswap_exists_last_associateunitidentity) * (ge_second_ip_unswap_exists_last_associateunitidentity))) + (((ge_first_in_unswap_exists_last_associateunitidentity) * (ge_second_in_unswap_exists_last_associateunitidentity))))))) + ge_balance_positive_unswap_exists_last_associateunitidentityoutputreal))) /\ (exists ge_balance_positive_unswap_exists_last_associateunitidentityoutputimaginary ge_balance_negative_unswap_exists_last_associateunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unswap_exists_last_associateunitidentityoutput) = 2 * (ge_balance_positive_unswap_exists_last_associateunitidentityoutputimaginary) /\ (ge_balance_negative_unswap_exists_last_associateunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unswap_exists_last_associateunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_last_associateunitidentityoutput) = 2 * ge_signed_half_unswap_exists_last_associateunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_last_associateunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unswap_exists_last_associateunitidentityoutputimaginary) = S ge_signed_half_unswap_exists_last_associateunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_exists_last_associateunitidentity) * (ge_second_ip_unswap_exists_last_associateunitidentity))) + (((ge_first_rn_unswap_exists_last_associateunitidentity) * (ge_second_in_unswap_exists_last_associateunitidentity))))) + (((((ge_first_ip_unswap_exists_last_associateunitidentity) * (ge_second_rp_unswap_exists_last_associateunitidentity))) + (((ge_first_in_unswap_exists_last_associateunitidentity) * (ge_second_rn_unswap_exists_last_associateunitidentity))))))) + ge_balance_negative_unswap_exists_last_associateunitidentityoutputimaginary = (((((((ge_first_rp_unswap_exists_last_associateunitidentity) * (ge_second_in_unswap_exists_last_associateunitidentity))) + (((ge_first_rn_unswap_exists_last_associateunitidentity) * (ge_second_ip_unswap_exists_last_associateunitidentity))))) + (((((ge_first_ip_unswap_exists_last_associateunitidentity) * (ge_second_rn_unswap_exists_last_associateunitidentity))) + (((ge_first_in_unswap_exists_last_associateunitidentity) * (ge_second_rp_unswap_exists_last_associateunitidentity))))))) + ge_balance_positive_unswap_exists_last_associateunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_unswap_exists_last_associatetransport ge_first_rn_unswap_exists_last_associatetransport ge_first_ip_unswap_exists_last_associatetransport ge_first_in_unswap_exists_last_associatetransport ge_second_rp_unswap_exists_last_associatetransport ge_second_rn_unswap_exists_last_associatetransport ge_second_ip_unswap_exists_last_associatetransport ge_second_in_unswap_exists_last_associatetransport. ((exists ge_representation_real_code_unswap_exists_last_associatetransportfirst ge_representation_imaginary_code_unswap_exists_last_associatetransportfirst. (((gr_unit_unswap_exists_last_associate) = ((ge_representation_real_code_unswap_exists_last_associatetransportfirst) + (ge_representation_imaginary_code_unswap_exists_last_associatetransportfirst)) * S ((ge_representation_real_code_unswap_exists_last_associatetransportfirst) + (ge_representation_imaginary_code_unswap_exists_last_associatetransportfirst)) + ((ge_representation_imaginary_code_unswap_exists_last_associatetransportfirst) + (ge_representation_imaginary_code_unswap_exists_last_associatetransportfirst))) /\ ((exists ge_balance_positive_unswap_exists_last_associatetransportfirstreal ge_balance_negative_unswap_exists_last_associatetransportfirstreal. (((((ge_representation_real_code_unswap_exists_last_associatetransportfirst) = 2 * (ge_balance_positive_unswap_exists_last_associatetransportfirstreal) /\ (ge_balance_negative_unswap_exists_last_associatetransportfirstreal) = 0) \/ exists ge_signed_half_unswap_exists_last_associatetransportfirstrealdecode. (((ge_representation_real_code_unswap_exists_last_associatetransportfirst) = 2 * ge_signed_half_unswap_exists_last_associatetransportfirstrealdecode + 1 /\ (ge_balance_positive_unswap_exists_last_associatetransportfirstreal) = 0) /\ (ge_balance_negative_unswap_exists_last_associatetransportfirstreal) = S ge_signed_half_unswap_exists_last_associatetransportfirstrealdecode))) /\ ((ge_first_rp_unswap_exists_last_associatetransport) + ge_balance_negative_unswap_exists_last_associatetransportfirstreal = (ge_first_rn_unswap_exists_last_associatetransport) + ge_balance_positive_unswap_exists_last_associatetransportfirstreal))) /\ (exists ge_balance_positive_unswap_exists_last_associatetransportfirstimaginary ge_balance_negative_unswap_exists_last_associatetransportfirstimaginary. (((((ge_representation_imaginary_code_unswap_exists_last_associatetransportfirst) = 2 * (ge_balance_positive_unswap_exists_last_associatetransportfirstimaginary) /\ (ge_balance_negative_unswap_exists_last_associatetransportfirstimaginary) = 0) \/ exists ge_signed_half_unswap_exists_last_associatetransportfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_last_associatetransportfirst) = 2 * ge_signed_half_unswap_exists_last_associatetransportfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_last_associatetransportfirstimaginary) = 0) /\ (ge_balance_negative_unswap_exists_last_associatetransportfirstimaginary) = S ge_signed_half_unswap_exists_last_associatetransportfirstimaginarydecode))) /\ ((ge_first_ip_unswap_exists_last_associatetransport) + ge_balance_negative_unswap_exists_last_associatetransportfirstimaginary = (ge_first_in_unswap_exists_last_associatetransport) + ge_balance_positive_unswap_exists_last_associatetransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_exists_last_associatetransportsecond ge_representation_imaginary_code_unswap_exists_last_associatetransportsecond. (((a) = ((ge_representation_real_code_unswap_exists_last_associatetransportsecond) + (ge_representation_imaginary_code_unswap_exists_last_associatetransportsecond)) * S ((ge_representation_real_code_unswap_exists_last_associatetransportsecond) + (ge_representation_imaginary_code_unswap_exists_last_associatetransportsecond)) + ((ge_representation_imaginary_code_unswap_exists_last_associatetransportsecond) + (ge_representation_imaginary_code_unswap_exists_last_associatetransportsecond))) /\ ((exists ge_balance_positive_unswap_exists_last_associatetransportsecondreal ge_balance_negative_unswap_exists_last_associatetransportsecondreal. (((((ge_representation_real_code_unswap_exists_last_associatetransportsecond) = 2 * (ge_balance_positive_unswap_exists_last_associatetransportsecondreal) /\ (ge_balance_negative_unswap_exists_last_associatetransportsecondreal) = 0) \/ exists ge_signed_half_unswap_exists_last_associatetransportsecondrealdecode. (((ge_representation_real_code_unswap_exists_last_associatetransportsecond) = 2 * ge_signed_half_unswap_exists_last_associatetransportsecondrealdecode + 1 /\ (ge_balance_positive_unswap_exists_last_associatetransportsecondreal) = 0) /\ (ge_balance_negative_unswap_exists_last_associatetransportsecondreal) = S ge_signed_half_unswap_exists_last_associatetransportsecondrealdecode))) /\ ((ge_second_rp_unswap_exists_last_associatetransport) + ge_balance_negative_unswap_exists_last_associatetransportsecondreal = (ge_second_rn_unswap_exists_last_associatetransport) + ge_balance_positive_unswap_exists_last_associatetransportsecondreal))) /\ (exists ge_balance_positive_unswap_exists_last_associatetransportsecondimaginary ge_balance_negative_unswap_exists_last_associatetransportsecondimaginary. (((((ge_representation_imaginary_code_unswap_exists_last_associatetransportsecond) = 2 * (ge_balance_positive_unswap_exists_last_associatetransportsecondimaginary) /\ (ge_balance_negative_unswap_exists_last_associatetransportsecondimaginary) = 0) \/ exists ge_signed_half_unswap_exists_last_associatetransportsecondimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_last_associatetransportsecond) = 2 * ge_signed_half_unswap_exists_last_associatetransportsecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_last_associatetransportsecondimaginary) = 0) /\ (ge_balance_negative_unswap_exists_last_associatetransportsecondimaginary) = S ge_signed_half_unswap_exists_last_associatetransportsecondimaginarydecode))) /\ ((ge_second_ip_unswap_exists_last_associatetransport) + ge_balance_negative_unswap_exists_last_associatetransportsecondimaginary = (ge_second_in_unswap_exists_last_associatetransport) + ge_balance_positive_unswap_exists_last_associatetransportsecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_exists_last_associatetransportoutput ge_representation_imaginary_code_unswap_exists_last_associatetransportoutput. (((p) = ((ge_representation_real_code_unswap_exists_last_associatetransportoutput) + (ge_representation_imaginary_code_unswap_exists_last_associatetransportoutput)) * S ((ge_representation_real_code_unswap_exists_last_associatetransportoutput) + (ge_representation_imaginary_code_unswap_exists_last_associatetransportoutput)) + ((ge_representation_imaginary_code_unswap_exists_last_associatetransportoutput) + (ge_representation_imaginary_code_unswap_exists_last_associatetransportoutput))) /\ ((exists ge_balance_positive_unswap_exists_last_associatetransportoutputreal ge_balance_negative_unswap_exists_last_associatetransportoutputreal. (((((ge_representation_real_code_unswap_exists_last_associatetransportoutput) = 2 * (ge_balance_positive_unswap_exists_last_associatetransportoutputreal) /\ (ge_balance_negative_unswap_exists_last_associatetransportoutputreal) = 0) \/ exists ge_signed_half_unswap_exists_last_associatetransportoutputrealdecode. (((ge_representation_real_code_unswap_exists_last_associatetransportoutput) = 2 * ge_signed_half_unswap_exists_last_associatetransportoutputrealdecode + 1 /\ (ge_balance_positive_unswap_exists_last_associatetransportoutputreal) = 0) /\ (ge_balance_negative_unswap_exists_last_associatetransportoutputreal) = S ge_signed_half_unswap_exists_last_associatetransportoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_exists_last_associatetransport) * (ge_second_rp_unswap_exists_last_associatetransport))) + (((ge_first_rn_unswap_exists_last_associatetransport) * (ge_second_rn_unswap_exists_last_associatetransport))))) + (((((ge_first_ip_unswap_exists_last_associatetransport) * (ge_second_in_unswap_exists_last_associatetransport))) + (((ge_first_in_unswap_exists_last_associatetransport) * (ge_second_ip_unswap_exists_last_associatetransport))))))) + ge_balance_negative_unswap_exists_last_associatetransportoutputreal = (((((((ge_first_rp_unswap_exists_last_associatetransport) * (ge_second_rn_unswap_exists_last_associatetransport))) + (((ge_first_rn_unswap_exists_last_associatetransport) * (ge_second_rp_unswap_exists_last_associatetransport))))) + (((((ge_first_ip_unswap_exists_last_associatetransport) * (ge_second_ip_unswap_exists_last_associatetransport))) + (((ge_first_in_unswap_exists_last_associatetransport) * (ge_second_in_unswap_exists_last_associatetransport))))))) + ge_balance_positive_unswap_exists_last_associatetransportoutputreal))) /\ (exists ge_balance_positive_unswap_exists_last_associatetransportoutputimaginary ge_balance_negative_unswap_exists_last_associatetransportoutputimaginary. (((((ge_representation_imaginary_code_unswap_exists_last_associatetransportoutput) = 2 * (ge_balance_positive_unswap_exists_last_associatetransportoutputimaginary) /\ (ge_balance_negative_unswap_exists_last_associatetransportoutputimaginary) = 0) \/ exists ge_signed_half_unswap_exists_last_associatetransportoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_last_associatetransportoutput) = 2 * ge_signed_half_unswap_exists_last_associatetransportoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_last_associatetransportoutputimaginary) = 0) /\ (ge_balance_negative_unswap_exists_last_associatetransportoutputimaginary) = S ge_signed_half_unswap_exists_last_associatetransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_exists_last_associatetransport) * (ge_second_ip_unswap_exists_last_associatetransport))) + (((ge_first_rn_unswap_exists_last_associatetransport) * (ge_second_in_unswap_exists_last_associatetransport))))) + (((((ge_first_ip_unswap_exists_last_associatetransport) * (ge_second_rp_unswap_exists_last_associatetransport))) + (((ge_first_in_unswap_exists_last_associatetransport) * (ge_second_rn_unswap_exists_last_associatetransport))))))) + ge_balance_negative_unswap_exists_last_associatetransportoutputimaginary = (((((((ge_first_rp_unswap_exists_last_associatetransport) * (ge_second_in_unswap_exists_last_associatetransport))) + (((ge_first_rn_unswap_exists_last_associatetransport) * (ge_second_ip_unswap_exists_last_associatetransport))))) + (((((ge_first_ip_unswap_exists_last_associatetransport) * (ge_second_rn_unswap_exists_last_associatetransport))) + (((ge_first_in_unswap_exists_last_associatetransport) * (ge_second_rp_unswap_exists_last_associatetransport))))))) + ge_balance_positive_unswap_exists_last_associatetransportoutputimaginary))))))))))) -> exists U V. (((((forall pfp_i_unswap_exists_resultbijectionbounded. (exists pfp_gap_unswap_exists_resultbijectionboundedindex. pfp_gap_unswap_exists_resultbijectionboundedindex + S (pfp_i_unswap_exists_resultbijectionbounded) = (S l)) -> exists pfp_a_unswap_exists_resultbijectionbounded. (((exists ff_h_pfp_unswap_exists_resultbijectionboundedentry. ff_h_pfp_unswap_exists_resultbijectionboundedentry + S (pfp_a_unswap_exists_resultbijectionbounded) = S ((S (pfp_i_unswap_exists_resultbijectionbounded)) * V)) /\ exists ff_q_pfp_unswap_exists_resultbijectionboundedentry. U = ff_q_pfp_unswap_exists_resultbijectionboundedentry * S ((S (pfp_i_unswap_exists_resultbijectionbounded)) * V) + (pfp_a_unswap_exists_resultbijectionbounded))) /\ (exists pfp_gap_unswap_exists_resultbijectionboundedvalue. pfp_gap_unswap_exists_resultbijectionboundedvalue + S (pfp_a_unswap_exists_resultbijectionbounded) = (S l))) /\ (((forall pfp_i_unswap_exists_resultbijectioninjective pfp_j_unswap_exists_resultbijectioninjective pfp_a_unswap_exists_resultbijectioninjective. (exists pfp_gap_unswap_exists_resultbijectioninjectivefirst. pfp_gap_unswap_exists_resultbijectioninjectivefirst + S (pfp_i_unswap_exists_resultbijectioninjective) = (S l)) -> (exists pfp_gap_unswap_exists_resultbijectioninjectivesecond. pfp_gap_unswap_exists_resultbijectioninjectivesecond + S (pfp_j_unswap_exists_resultbijectioninjective) = (S l)) -> (((exists ff_h_pfp_unswap_exists_resultbijectioninjectiveleft. ff_h_pfp_unswap_exists_resultbijectioninjectiveleft + S (pfp_a_unswap_exists_resultbijectioninjective) = S ((S (pfp_i_unswap_exists_resultbijectioninjective)) * V)) /\ exists ff_q_pfp_unswap_exists_resultbijectioninjectiveleft. U = ff_q_pfp_unswap_exists_resultbijectioninjectiveleft * S ((S (pfp_i_unswap_exists_resultbijectioninjective)) * V) + (pfp_a_unswap_exists_resultbijectioninjective))) -> (((exists ff_h_pfp_unswap_exists_resultbijectioninjectiveright. ff_h_pfp_unswap_exists_resultbijectioninjectiveright + S (pfp_a_unswap_exists_resultbijectioninjective) = S ((S (pfp_j_unswap_exists_resultbijectioninjective)) * V)) /\ exists ff_q_pfp_unswap_exists_resultbijectioninjectiveright. U = ff_q_pfp_unswap_exists_resultbijectioninjectiveright * S ((S (pfp_j_unswap_exists_resultbijectioninjective)) * V) + (pfp_a_unswap_exists_resultbijectioninjective))) -> pfp_i_unswap_exists_resultbijectioninjective = pfp_j_unswap_exists_resultbijectioninjective) /\ (forall pfp_a_unswap_exists_resultbijectionsurjective. (exists pfp_gap_unswap_exists_resultbijectionsurjectivevalue. pfp_gap_unswap_exists_resultbijectionsurjectivevalue + S (pfp_a_unswap_exists_resultbijectionsurjective) = (S l)) -> exists pfp_i_unswap_exists_resultbijectionsurjective. (exists pfp_gap_unswap_exists_resultbijectionsurjectiveindex. pfp_gap_unswap_exists_resultbijectionsurjectiveindex + S (pfp_i_unswap_exists_resultbijectionsurjective) = (S l)) /\ (((exists ff_h_pfp_unswap_exists_resultbijectionsurjectiveentry. ff_h_pfp_unswap_exists_resultbijectionsurjectiveentry + S (pfp_a_unswap_exists_resultbijectionsurjective) = S ((S (pfp_i_unswap_exists_resultbijectionsurjective)) * V)) /\ exists ff_q_pfp_unswap_exists_resultbijectionsurjectiveentry. U = ff_q_pfp_unswap_exists_resultbijectionsurjectiveentry * S ((S (pfp_i_unswap_exists_resultbijectionsurjective)) * V) + (pfp_a_unswap_exists_resultbijectionsurjective)))))))) /\ (forall gr_match_index_unswap_exists_resultmatching gr_match_image_unswap_exists_resultmatching gr_match_source_unswap_exists_resultmatching gr_match_target_unswap_exists_resultmatching. (exists ge_gap_unswap_exists_resultmatchingindex. ge_gap_unswap_exists_resultmatchingindex + S (gr_match_index_unswap_exists_resultmatching) = (S l)) -> (((exists ff_h_gprod_unswap_exists_resultmatchingmap. ff_h_gprod_unswap_exists_resultmatchingmap + S (gr_match_image_unswap_exists_resultmatching) = S ((S (gr_match_index_unswap_exists_resultmatching)) * V)) /\ exists ff_q_gprod_unswap_exists_resultmatchingmap. U = ff_q_gprod_unswap_exists_resultmatchingmap * S ((S (gr_match_index_unswap_exists_resultmatching)) * V) + (gr_match_image_unswap_exists_resultmatching))) -> (((exists ff_h_gprod_unswap_exists_resultmatchingsource. ff_h_gprod_unswap_exists_resultmatchingsource + S (gr_match_source_unswap_exists_resultmatching) = S ((S (gr_match_index_unswap_exists_resultmatching)) * c)) /\ exists ff_q_gprod_unswap_exists_resultmatchingsource. b = ff_q_gprod_unswap_exists_resultmatchingsource * S ((S (gr_match_index_unswap_exists_resultmatching)) * c) + (gr_match_source_unswap_exists_resultmatching))) -> (((exists ff_h_gprod_unswap_exists_resultmatchingtarget. ff_h_gprod_unswap_exists_resultmatchingtarget + S (gr_match_target_unswap_exists_resultmatching) = S ((S (gr_match_image_unswap_exists_resultmatching)) * e)) /\ exists ff_q_gprod_unswap_exists_resultmatchingtarget. d = ff_q_gprod_unswap_exists_resultmatchingtarget * S ((S (gr_match_image_unswap_exists_resultmatching)) * e) + (gr_match_target_unswap_exists_resultmatching))) -> (exists gr_unit_unswap_exists_resultmatchingunit_witness. ((exists gr_inverse_unswap_exists_resultmatchingunit_witnessunit. (exists ge_first_rp_unswap_exists_resultmatchingunit_witnessunitidentity ge_first_rn_unswap_exists_resultmatchingunit_witnessunitidentity ge_first_ip_unswap_exists_resultmatchingunit_witnessunitidentity ge_first_in_unswap_exists_resultmatchingunit_witnessunitidentity ge_second_rp_unswap_exists_resultmatchingunit_witnessunitidentity ge_second_rn_unswap_exists_resultmatchingunit_witnessunitidentity ge_second_ip_unswap_exists_resultmatchingunit_witnessunitidentity ge_second_in_unswap_exists_resultmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst. (((gr_unit_unswap_exists_resultmatchingunit_witness) = ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityfirstreal ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_unswap_exists_resultmatchingunit_witnessunitidentity) + ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_unswap_exists_resultmatchingunit_witnessunitidentity) + ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_unswap_exists_resultmatchingunit_witnessunitidentity) + ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_unswap_exists_resultmatchingunit_witnessunitidentity) + ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond. (((gr_inverse_unswap_exists_resultmatchingunit_witnessunit) = ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentitysecondreal ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_unswap_exists_resultmatchingunit_witnessunitidentity) + ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_unswap_exists_resultmatchingunit_witnessunitidentity) + ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_unswap_exists_resultmatchingunit_witnessunitidentity) + ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_unswap_exists_resultmatchingunit_witnessunitidentity) + ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityoutputreal ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_rp_unswap_exists_resultmatchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_rn_unswap_exists_resultmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_in_unswap_exists_resultmatchingunit_witnessunitidentity))) + (((ge_first_in_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_ip_unswap_exists_resultmatchingunit_witnessunitidentity))))))) + ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_rn_unswap_exists_resultmatchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_rp_unswap_exists_resultmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_ip_unswap_exists_resultmatchingunit_witnessunitidentity))) + (((ge_first_in_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_in_unswap_exists_resultmatchingunit_witnessunitidentity))))))) + ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_ip_unswap_exists_resultmatchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_in_unswap_exists_resultmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_rp_unswap_exists_resultmatchingunit_witnessunitidentity))) + (((ge_first_in_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_rn_unswap_exists_resultmatchingunit_witnessunitidentity))))))) + ge_balance_negative_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_in_unswap_exists_resultmatchingunit_witnessunitidentity))) + (((ge_first_rn_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_ip_unswap_exists_resultmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_rn_unswap_exists_resultmatchingunit_witnessunitidentity))) + (((ge_first_in_unswap_exists_resultmatchingunit_witnessunitidentity) * (ge_second_rp_unswap_exists_resultmatchingunit_witnessunitidentity))))))) + ge_balance_positive_unswap_exists_resultmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_unswap_exists_resultmatchingunit_witnesstransport ge_first_rn_unswap_exists_resultmatchingunit_witnesstransport ge_first_ip_unswap_exists_resultmatchingunit_witnesstransport ge_first_in_unswap_exists_resultmatchingunit_witnesstransport ge_second_rp_unswap_exists_resultmatchingunit_witnesstransport ge_second_rn_unswap_exists_resultmatchingunit_witnesstransport ge_second_ip_unswap_exists_resultmatchingunit_witnesstransport ge_second_in_unswap_exists_resultmatchingunit_witnesstransport. ((exists ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportfirst ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportfirst. (((gr_unit_unswap_exists_resultmatchingunit_witness) = ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportfirstreal ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportfirstreal) = S ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_unswap_exists_resultmatchingunit_witnesstransport) + ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportfirstreal = (ge_first_rn_unswap_exists_resultmatchingunit_witnesstransport) + ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportfirstimaginary ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_unswap_exists_resultmatchingunit_witnesstransport) + ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportfirstimaginary = (ge_first_in_unswap_exists_resultmatchingunit_witnesstransport) + ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportsecond ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportsecond. (((gr_match_source_unswap_exists_resultmatching) = ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportsecondreal ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportsecondreal) = S ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_unswap_exists_resultmatchingunit_witnesstransport) + ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportsecondreal = (ge_second_rn_unswap_exists_resultmatchingunit_witnesstransport) + ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportsecondimaginary ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_unswap_exists_resultmatchingunit_witnesstransport) + ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportsecondimaginary = (ge_second_in_unswap_exists_resultmatchingunit_witnesstransport) + ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportoutput ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportoutput. (((gr_match_target_unswap_exists_resultmatching) = ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportoutputreal ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_unswap_exists_resultmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportoutputreal) = S ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_rp_unswap_exists_resultmatchingunit_witnesstransport))) + (((ge_first_rn_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_rn_unswap_exists_resultmatchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_in_unswap_exists_resultmatchingunit_witnesstransport))) + (((ge_first_in_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_ip_unswap_exists_resultmatchingunit_witnesstransport))))))) + ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_rn_unswap_exists_resultmatchingunit_witnesstransport))) + (((ge_first_rn_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_rp_unswap_exists_resultmatchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_ip_unswap_exists_resultmatchingunit_witnesstransport))) + (((ge_first_in_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_in_unswap_exists_resultmatchingunit_witnesstransport))))))) + ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportoutputimaginary ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_unswap_exists_resultmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_unswap_exists_resultmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_ip_unswap_exists_resultmatchingunit_witnesstransport))) + (((ge_first_rn_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_in_unswap_exists_resultmatchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_rp_unswap_exists_resultmatchingunit_witnesstransport))) + (((ge_first_in_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_rn_unswap_exists_resultmatchingunit_witnesstransport))))))) + ge_balance_negative_unswap_exists_resultmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_in_unswap_exists_resultmatchingunit_witnesstransport))) + (((ge_first_rn_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_ip_unswap_exists_resultmatchingunit_witnesstransport))))) + (((((ge_first_ip_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_rn_unswap_exists_resultmatchingunit_witnesstransport))) + (((ge_first_in_unswap_exists_resultmatchingunit_witnesstransport) * (ge_second_rp_unswap_exists_resultmatchingunit_witnesstransport))))))) + ge_balance_positive_unswap_exists_resultmatchingunit_witnesstransportoutputimaginary))))))))))))))