gaussian_factor_empty_matching

Exact expanded first-order arithmetic statement

forall b c d e. (((((forall pfp_i_empty_matchingbijectionbounded. (exists pfp_gap_empty_matchingbijectionboundedindex. pfp_gap_empty_matchingbijectionboundedindex + S (pfp_i_empty_matchingbijectionbounded) = (0)) -> exists pfp_a_empty_matchingbijectionbounded. (((exists ff_h_pfp_empty_matchingbijectionboundedentry. ff_h_pfp_empty_matchingbijectionboundedentry + S (pfp_a_empty_matchingbijectionbounded) = S ((S (pfp_i_empty_matchingbijectionbounded)) * 0)) /\ exists ff_q_pfp_empty_matchingbijectionboundedentry. 0 = ff_q_pfp_empty_matchingbijectionboundedentry * S ((S (pfp_i_empty_matchingbijectionbounded)) * 0) + (pfp_a_empty_matchingbijectionbounded))) /\ (exists pfp_gap_empty_matchingbijectionboundedvalue. pfp_gap_empty_matchingbijectionboundedvalue + S (pfp_a_empty_matchingbijectionbounded) = (0))) /\ (((forall pfp_i_empty_matchingbijectioninjective pfp_j_empty_matchingbijectioninjective pfp_a_empty_matchingbijectioninjective. (exists pfp_gap_empty_matchingbijectioninjectivefirst. pfp_gap_empty_matchingbijectioninjectivefirst + S (pfp_i_empty_matchingbijectioninjective) = (0)) -> (exists pfp_gap_empty_matchingbijectioninjectivesecond. pfp_gap_empty_matchingbijectioninjectivesecond + S (pfp_j_empty_matchingbijectioninjective) = (0)) -> (((exists ff_h_pfp_empty_matchingbijectioninjectiveleft. ff_h_pfp_empty_matchingbijectioninjectiveleft + S (pfp_a_empty_matchingbijectioninjective) = S ((S (pfp_i_empty_matchingbijectioninjective)) * 0)) /\ exists ff_q_pfp_empty_matchingbijectioninjectiveleft. 0 = ff_q_pfp_empty_matchingbijectioninjectiveleft * S ((S (pfp_i_empty_matchingbijectioninjective)) * 0) + (pfp_a_empty_matchingbijectioninjective))) -> (((exists ff_h_pfp_empty_matchingbijectioninjectiveright. ff_h_pfp_empty_matchingbijectioninjectiveright + S (pfp_a_empty_matchingbijectioninjective) = S ((S (pfp_j_empty_matchingbijectioninjective)) * 0)) /\ exists ff_q_pfp_empty_matchingbijectioninjectiveright. 0 = ff_q_pfp_empty_matchingbijectioninjectiveright * S ((S (pfp_j_empty_matchingbijectioninjective)) * 0) + (pfp_a_empty_matchingbijectioninjective))) -> pfp_i_empty_matchingbijectioninjective = pfp_j_empty_matchingbijectioninjective) /\ (forall pfp_a_empty_matchingbijectionsurjective. (exists pfp_gap_empty_matchingbijectionsurjectivevalue. pfp_gap_empty_matchingbijectionsurjectivevalue + S (pfp_a_empty_matchingbijectionsurjective) = (0)) -> exists pfp_i_empty_matchingbijectionsurjective. (exists pfp_gap_empty_matchingbijectionsurjectiveindex. pfp_gap_empty_matchingbijectionsurjectiveindex + S (pfp_i_empty_matchingbijectionsurjective) = (0)) /\ (((exists ff_h_pfp_empty_matchingbijectionsurjectiveentry. ff_h_pfp_empty_matchingbijectionsurjectiveentry + S (pfp_a_empty_matchingbijectionsurjective) = S ((S (pfp_i_empty_matchingbijectionsurjective)) * 0)) /\ exists ff_q_pfp_empty_matchingbijectionsurjectiveentry. 0 = ff_q_pfp_empty_matchingbijectionsurjectiveentry * S ((S (pfp_i_empty_matchingbijectionsurjective)) * 0) + (pfp_a_empty_matchingbijectionsurjective)))))))) /\ (forall gr_match_index_empty_matchingmatching gr_match_image_empty_matchingmatching gr_match_source_empty_matchingmatching gr_match_target_empty_matchingmatching. (exists ge_gap_empty_matchingmatchingindex. ge_gap_empty_matchingmatchingindex + S (gr_match_index_empty_matchingmatching) = (0)) -> (((exists ff_h_gprod_empty_matchingmatchingmap. ff_h_gprod_empty_matchingmatchingmap + S (gr_match_image_empty_matchingmatching) = S ((S (gr_match_index_empty_matchingmatching)) * 0)) /\ exists ff_q_gprod_empty_matchingmatchingmap. 0 = ff_q_gprod_empty_matchingmatchingmap * S ((S (gr_match_index_empty_matchingmatching)) * 0) + (gr_match_image_empty_matchingmatching))) -> (((exists ff_h_gprod_empty_matchingmatchingsource. ff_h_gprod_empty_matchingmatchingsource + S (gr_match_source_empty_matchingmatching) = S ((S (gr_match_index_empty_matchingmatching)) * c)) /\ exists ff_q_gprod_empty_matchingmatchingsource. b = ff_q_gprod_empty_matchingmatchingsource * S ((S (gr_match_index_empty_matchingmatching)) * c) + (gr_match_source_empty_matchingmatching))) -> (((exists ff_h_gprod_empty_matchingmatchingtarget. ff_h_gprod_empty_matchingmatchingtarget + S (gr_match_target_empty_matchingmatching) = S ((S (gr_match_image_empty_matchingmatching)) * e)) /\ exists ff_q_gprod_empty_matchingmatchingtarget. d = ff_q_gprod_empty_matchingmatchingtarget * S ((S (gr_match_image_empty_matchingmatching)) * e) + (gr_match_target_empty_matchingmatching))) -> (exists gr_unit_empty_matchingmatchingunit_witness. ((exists gr_inverse_empty_matchingmatchingunit_witnessunit. (exists ge_first_rp_empty_matchingmatchingunit_witnessunitidentity ge_first_rn_empty_matchingmatchingunit_witnessunitidentity ge_first_ip_empty_matchingmatchingunit_witnessunitidentity ge_first_in_empty_matchingmatchingunit_witnessunitidentity ge_second_rp_empty_matchingmatchingunit_witnessunitidentity ge_second_rn_empty_matchingmatchingunit_witnessunitidentity ge_second_ip_empty_matchingmatchingunit_witnessunitidentity ge_second_in_empty_matchingmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst. (((gr_unit_empty_matchingmatchingunit_witness) = ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstreal ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond. (((gr_inverse_empty_matchingmatchingunit_witnessunit) = ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondreal ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_empty_matchingmatchingunit_witnessunitidentity) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputreal ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rp_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_in_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_in_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_ip_empty_matchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rp_empty_matchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_ip_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_in_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_in_empty_matchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_ip_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_in_empty_matchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rp_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_in_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity))))))) + ge_balance_negative_empty_matchingmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_in_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_rn_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_ip_empty_matchingmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rn_empty_matchingmatchingunit_witnessunitidentity))) + (((ge_first_in_empty_matchingmatchingunit_witnessunitidentity) * (ge_second_rp_empty_matchingmatchingunit_witnessunitidentity))))))) + ge_balance_positive_empty_matchingmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_empty_matchingmatchingunit_witnesstransport ge_first_rn_empty_matchingmatchingunit_witnesstransport ge_first_ip_empty_matchingmatchingunit_witnesstransport ge_first_in_empty_matchingmatchingunit_witnesstransport ge_second_rp_empty_matchingmatchingunit_witnesstransport ge_second_rn_empty_matchingmatchingunit_witnesstransport ge_second_ip_empty_matchingmatchingunit_witnesstransport ge_second_in_empty_matchingmatchingunit_witnesstransport. ((exists ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst. (((gr_unit_empty_matchingmatchingunit_witness) = ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstreal ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstreal) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_empty_matchingmatchingunit_witnesstransport) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstreal = (ge_first_rn_empty_matchingmatchingunit_witnesstransport) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstimaginary ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_empty_matchingmatchingunit_witnesstransport) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportfirstimaginary = (ge_first_in_empty_matchingmatchingunit_witnesstransport) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond. (((gr_match_source_empty_matchingmatching) = ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondreal ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondreal) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_empty_matchingmatchingunit_witnesstransport) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondreal = (ge_second_rn_empty_matchingmatchingunit_witnesstransport) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondimaginary ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_empty_matchingmatchingunit_witnesstransport) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportsecondimaginary = (ge_second_in_empty_matchingmatchingunit_witnesstransport) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput. (((gr_match_target_empty_matchingmatching) = ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputreal ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_empty_matchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputreal) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_empty_matchingmatchingunit_witnesstransport) * (ge_second_rp_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_rn_empty_matchingmatchingunit_witnesstransport) * (ge_second_rn_empty_matchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnesstransport) * (ge_second_in_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_in_empty_matchingmatchingunit_witnesstransport) * (ge_second_ip_empty_matchingmatchingunit_witnesstransport))))))) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_empty_matchingmatchingunit_witnesstransport) * (ge_second_rn_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_rn_empty_matchingmatchingunit_witnesstransport) * (ge_second_rp_empty_matchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnesstransport) * (ge_second_ip_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_in_empty_matchingmatchingunit_witnesstransport) * (ge_second_in_empty_matchingmatchingunit_witnesstransport))))))) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputimaginary ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_empty_matchingmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_empty_matchingmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_empty_matchingmatchingunit_witnesstransport) * (ge_second_ip_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_rn_empty_matchingmatchingunit_witnesstransport) * (ge_second_in_empty_matchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnesstransport) * (ge_second_rp_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_in_empty_matchingmatchingunit_witnesstransport) * (ge_second_rn_empty_matchingmatchingunit_witnesstransport))))))) + ge_balance_negative_empty_matchingmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_empty_matchingmatchingunit_witnesstransport) * (ge_second_in_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_rn_empty_matchingmatchingunit_witnesstransport) * (ge_second_ip_empty_matchingmatchingunit_witnesstransport))))) + (((((ge_first_ip_empty_matchingmatchingunit_witnesstransport) * (ge_second_rn_empty_matchingmatchingunit_witnesstransport))) + (((ge_first_in_empty_matchingmatchingunit_witnesstransport) * (ge_second_rp_empty_matchingmatchingunit_witnesstransport))))))) + ge_balance_positive_empty_matchingmatchingunit_witnesstransportoutputimaginary))))))))))))))