gaussian_factor_matched_append

Exact expanded first-order arithmetic statement

forall b c d e u v l p q. (((((forall pfp_i_matched_append_oldbijectionbounded. (exists pfp_gap_matched_append_oldbijectionboundedindex. pfp_gap_matched_append_oldbijectionboundedindex + S (pfp_i_matched_append_oldbijectionbounded) = (l)) -> exists pfp_a_matched_append_oldbijectionbounded. (((exists ff_h_pfp_matched_append_oldbijectionboundedentry. ff_h_pfp_matched_append_oldbijectionboundedentry + S (pfp_a_matched_append_oldbijectionbounded) = S ((S (pfp_i_matched_append_oldbijectionbounded)) * v)) /\ exists ff_q_pfp_matched_append_oldbijectionboundedentry. u = ff_q_pfp_matched_append_oldbijectionboundedentry * S ((S (pfp_i_matched_append_oldbijectionbounded)) * v) + (pfp_a_matched_append_oldbijectionbounded))) /\ (exists pfp_gap_matched_append_oldbijectionboundedvalue. pfp_gap_matched_append_oldbijectionboundedvalue + S (pfp_a_matched_append_oldbijectionbounded) = (l))) /\ (((forall pfp_i_matched_append_oldbijectioninjective pfp_j_matched_append_oldbijectioninjective pfp_a_matched_append_oldbijectioninjective. (exists pfp_gap_matched_append_oldbijectioninjectivefirst. pfp_gap_matched_append_oldbijectioninjectivefirst + S (pfp_i_matched_append_oldbijectioninjective) = (l)) -> (exists pfp_gap_matched_append_oldbijectioninjectivesecond. pfp_gap_matched_append_oldbijectioninjectivesecond + S (pfp_j_matched_append_oldbijectioninjective) = (l)) -> (((exists ff_h_pfp_matched_append_oldbijectioninjectiveleft. ff_h_pfp_matched_append_oldbijectioninjectiveleft + S (pfp_a_matched_append_oldbijectioninjective) = S ((S (pfp_i_matched_append_oldbijectioninjective)) * v)) /\ exists ff_q_pfp_matched_append_oldbijectioninjectiveleft. u = ff_q_pfp_matched_append_oldbijectioninjectiveleft * S ((S (pfp_i_matched_append_oldbijectioninjective)) * v) + (pfp_a_matched_append_oldbijectioninjective))) -> (((exists ff_h_pfp_matched_append_oldbijectioninjectiveright. ff_h_pfp_matched_append_oldbijectioninjectiveright + S (pfp_a_matched_append_oldbijectioninjective) = S ((S (pfp_j_matched_append_oldbijectioninjective)) * v)) /\ exists ff_q_pfp_matched_append_oldbijectioninjectiveright. u = ff_q_pfp_matched_append_oldbijectioninjectiveright * S ((S (pfp_j_matched_append_oldbijectioninjective)) * v) + (pfp_a_matched_append_oldbijectioninjective))) -> pfp_i_matched_append_oldbijectioninjective = pfp_j_matched_append_oldbijectioninjective) /\ (forall pfp_a_matched_append_oldbijectionsurjective. (exists pfp_gap_matched_append_oldbijectionsurjectivevalue. pfp_gap_matched_append_oldbijectionsurjectivevalue + S (pfp_a_matched_append_oldbijectionsurjective) = (l)) -> exists pfp_i_matched_append_oldbijectionsurjective. (exists pfp_gap_matched_append_oldbijectionsurjectiveindex. pfp_gap_matched_append_oldbijectionsurjectiveindex + S (pfp_i_matched_append_oldbijectionsurjective) = (l)) /\ (((exists ff_h_pfp_matched_append_oldbijectionsurjectiveentry. ff_h_pfp_matched_append_oldbijectionsurjectiveentry + S (pfp_a_matched_append_oldbijectionsurjective) = S ((S (pfp_i_matched_append_oldbijectionsurjective)) * v)) /\ exists ff_q_pfp_matched_append_oldbijectionsurjectiveentry. u = ff_q_pfp_matched_append_oldbijectionsurjectiveentry * S ((S (pfp_i_matched_append_oldbijectionsurjective)) * v) + (pfp_a_matched_append_oldbijectionsurjective)))))))) /\ (forall gr_match_index_matched_append_oldmatching gr_match_image_matched_append_oldmatching gr_match_source_matched_append_oldmatching gr_match_target_matched_append_oldmatching. (exists ge_gap_matched_append_oldmatchingindex. ge_gap_matched_append_oldmatchingindex + S (gr_match_index_matched_append_oldmatching) = (l)) -> (((exists ff_h_gprod_matched_append_oldmatchingmap. ff_h_gprod_matched_append_oldmatchingmap + S (gr_match_image_matched_append_oldmatching) = S ((S (gr_match_index_matched_append_oldmatching)) * v)) /\ exists ff_q_gprod_matched_append_oldmatchingmap. u = ff_q_gprod_matched_append_oldmatchingmap * S ((S (gr_match_index_matched_append_oldmatching)) * v) + (gr_match_image_matched_append_oldmatching))) -> (((exists ff_h_gprod_matched_append_oldmatchingsource. ff_h_gprod_matched_append_oldmatchingsource + S (gr_match_source_matched_append_oldmatching) = S ((S (gr_match_index_matched_append_oldmatching)) * c)) /\ exists ff_q_gprod_matched_append_oldmatchingsource. b = ff_q_gprod_matched_append_oldmatchingsource * S ((S (gr_match_index_matched_append_oldmatching)) * c) + (gr_match_source_matched_append_oldmatching))) -> (((exists ff_h_gprod_matched_append_oldmatchingtarget. ff_h_gprod_matched_append_oldmatchingtarget + S (gr_match_target_matched_append_oldmatching) = S ((S (gr_match_image_matched_append_oldmatching)) * e)) /\ exists ff_q_gprod_matched_append_oldmatchingtarget. d = ff_q_gprod_matched_append_oldmatchingtarget * S ((S (gr_match_image_matched_append_oldmatching)) * e) + (gr_match_target_matched_append_oldmatching))) -> (exists gr_unit_matched_append_oldmatchingunit_witness. ((exists gr_inverse_matched_append_oldmatchingunit_witnessunit. (exists ge_first_rp_matched_append_oldmatchingunit_witnessunitidentity ge_first_rn_matched_append_oldmatchingunit_witnessunitidentity ge_first_ip_matched_append_oldmatchingunit_witnessunitidentity ge_first_in_matched_append_oldmatchingunit_witnessunitidentity ge_second_rp_matched_append_oldmatchingunit_witnessunitidentity ge_second_rn_matched_append_oldmatchingunit_witnessunitidentity ge_second_ip_matched_append_oldmatchingunit_witnessunitidentity ge_second_in_matched_append_oldmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityfirst. (((gr_unit_matched_append_oldmatchingunit_witness) = ((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityfirstreal ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_matched_append_oldmatchingunit_witnessunitidentity) + ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_matched_append_oldmatchingunit_witnessunitidentity) + ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_matched_append_oldmatchingunit_witnessunitidentity) + ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_matched_append_oldmatchingunit_witnessunitidentity) + ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentitysecond. (((gr_inverse_matched_append_oldmatchingunit_witnessunit) = ((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentitysecondreal ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_matched_append_oldmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_matched_append_oldmatchingunit_witnessunitidentity) + ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_matched_append_oldmatchingunit_witnessunitidentity) + ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_matched_append_oldmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_matched_append_oldmatchingunit_witnessunitidentity) + ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_matched_append_oldmatchingunit_witnessunitidentity) + ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityoutputreal ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_matched_append_oldmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_rp_matched_append_oldmatchingunit_witnessunitidentity))) + (((ge_first_rn_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_rn_matched_append_oldmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_in_matched_append_oldmatchingunit_witnessunitidentity))) + (((ge_first_in_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_ip_matched_append_oldmatchingunit_witnessunitidentity))))))) + ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_rn_matched_append_oldmatchingunit_witnessunitidentity))) + (((ge_first_rn_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_rp_matched_append_oldmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_ip_matched_append_oldmatchingunit_witnessunitidentity))) + (((ge_first_in_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_in_matched_append_oldmatchingunit_witnessunitidentity))))))) + ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_matched_append_oldmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_ip_matched_append_oldmatchingunit_witnessunitidentity))) + (((ge_first_rn_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_in_matched_append_oldmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_rp_matched_append_oldmatchingunit_witnessunitidentity))) + (((ge_first_in_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_rn_matched_append_oldmatchingunit_witnessunitidentity))))))) + ge_balance_negative_matched_append_oldmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_in_matched_append_oldmatchingunit_witnessunitidentity))) + (((ge_first_rn_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_ip_matched_append_oldmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_rn_matched_append_oldmatchingunit_witnessunitidentity))) + (((ge_first_in_matched_append_oldmatchingunit_witnessunitidentity) * (ge_second_rp_matched_append_oldmatchingunit_witnessunitidentity))))))) + ge_balance_positive_matched_append_oldmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_matched_append_oldmatchingunit_witnesstransport ge_first_rn_matched_append_oldmatchingunit_witnesstransport ge_first_ip_matched_append_oldmatchingunit_witnesstransport ge_first_in_matched_append_oldmatchingunit_witnesstransport ge_second_rp_matched_append_oldmatchingunit_witnesstransport ge_second_rn_matched_append_oldmatchingunit_witnesstransport ge_second_ip_matched_append_oldmatchingunit_witnesstransport ge_second_in_matched_append_oldmatchingunit_witnesstransport. ((exists ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportfirst ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportfirst. (((gr_unit_matched_append_oldmatchingunit_witness) = ((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_matched_append_oldmatchingunit_witnesstransportfirstreal ge_balance_negative_matched_append_oldmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportfirstreal) = S ge_signed_half_matched_append_oldmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_matched_append_oldmatchingunit_witnesstransport) + ge_balance_negative_matched_append_oldmatchingunit_witnesstransportfirstreal = (ge_first_rn_matched_append_oldmatchingunit_witnesstransport) + ge_balance_positive_matched_append_oldmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_matched_append_oldmatchingunit_witnesstransportfirstimaginary ge_balance_negative_matched_append_oldmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_matched_append_oldmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_matched_append_oldmatchingunit_witnesstransport) + ge_balance_negative_matched_append_oldmatchingunit_witnesstransportfirstimaginary = (ge_first_in_matched_append_oldmatchingunit_witnesstransport) + ge_balance_positive_matched_append_oldmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportsecond ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportsecond. (((gr_match_source_matched_append_oldmatching) = ((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_matched_append_oldmatchingunit_witnesstransportsecondreal ge_balance_negative_matched_append_oldmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportsecondreal) = S ge_signed_half_matched_append_oldmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_matched_append_oldmatchingunit_witnesstransport) + ge_balance_negative_matched_append_oldmatchingunit_witnesstransportsecondreal = (ge_second_rn_matched_append_oldmatchingunit_witnesstransport) + ge_balance_positive_matched_append_oldmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_matched_append_oldmatchingunit_witnesstransportsecondimaginary ge_balance_negative_matched_append_oldmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_matched_append_oldmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_matched_append_oldmatchingunit_witnesstransport) + ge_balance_negative_matched_append_oldmatchingunit_witnesstransportsecondimaginary = (ge_second_in_matched_append_oldmatchingunit_witnesstransport) + ge_balance_positive_matched_append_oldmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportoutput ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportoutput. (((gr_match_target_matched_append_oldmatching) = ((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_matched_append_oldmatchingunit_witnesstransportoutputreal ge_balance_negative_matched_append_oldmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_matched_append_oldmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportoutputreal) = S ge_signed_half_matched_append_oldmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_matched_append_oldmatchingunit_witnesstransport) * (ge_second_rp_matched_append_oldmatchingunit_witnesstransport))) + (((ge_first_rn_matched_append_oldmatchingunit_witnesstransport) * (ge_second_rn_matched_append_oldmatchingunit_witnesstransport))))) + (((((ge_first_ip_matched_append_oldmatchingunit_witnesstransport) * (ge_second_in_matched_append_oldmatchingunit_witnesstransport))) + (((ge_first_in_matched_append_oldmatchingunit_witnesstransport) * (ge_second_ip_matched_append_oldmatchingunit_witnesstransport))))))) + ge_balance_negative_matched_append_oldmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_matched_append_oldmatchingunit_witnesstransport) * (ge_second_rn_matched_append_oldmatchingunit_witnesstransport))) + (((ge_first_rn_matched_append_oldmatchingunit_witnesstransport) * (ge_second_rp_matched_append_oldmatchingunit_witnesstransport))))) + (((((ge_first_ip_matched_append_oldmatchingunit_witnesstransport) * (ge_second_ip_matched_append_oldmatchingunit_witnesstransport))) + (((ge_first_in_matched_append_oldmatchingunit_witnesstransport) * (ge_second_in_matched_append_oldmatchingunit_witnesstransport))))))) + ge_balance_positive_matched_append_oldmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_matched_append_oldmatchingunit_witnesstransportoutputimaginary ge_balance_negative_matched_append_oldmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_matched_append_oldmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_matched_append_oldmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_matched_append_oldmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_matched_append_oldmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_matched_append_oldmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_matched_append_oldmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_matched_append_oldmatchingunit_witnesstransport) * (ge_second_ip_matched_append_oldmatchingunit_witnesstransport))) + (((ge_first_rn_matched_append_oldmatchingunit_witnesstransport) * (ge_second_in_matched_append_oldmatchingunit_witnesstransport))))) + (((((ge_first_ip_matched_append_oldmatchingunit_witnesstransport) * (ge_second_rp_matched_append_oldmatchingunit_witnesstransport))) + (((ge_first_in_matched_append_oldmatchingunit_witnesstransport) * (ge_second_rn_matched_append_oldmatchingunit_witnesstransport))))))) + ge_balance_negative_matched_append_oldmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_matched_append_oldmatchingunit_witnesstransport) * (ge_second_in_matched_append_oldmatchingunit_witnesstransport))) + (((ge_first_rn_matched_append_oldmatchingunit_witnesstransport) * (ge_second_ip_matched_append_oldmatchingunit_witnesstransport))))) + (((((ge_first_ip_matched_append_oldmatchingunit_witnesstransport) * (ge_second_rn_matched_append_oldmatchingunit_witnesstransport))) + (((ge_first_in_matched_append_oldmatchingunit_witnesstransport) * (ge_second_rp_matched_append_oldmatchingunit_witnesstransport))))))) + ge_balance_positive_matched_append_oldmatchingunit_witnesstransportoutputimaginary)))))))))))))) -> (((exists ff_h_gprod_matched_append_source_last. ff_h_gprod_matched_append_source_last + S (p) = S ((S (l)) * c)) /\ exists ff_q_gprod_matched_append_source_last. b = ff_q_gprod_matched_append_source_last * S ((S (l)) * c) + (p))) -> (((exists ff_h_gprod_matched_append_target_last. ff_h_gprod_matched_append_target_last + S (q) = S ((S (l)) * e)) /\ exists ff_q_gprod_matched_append_target_last. d = ff_q_gprod_matched_append_target_last * S ((S (l)) * e) + (q))) -> (exists gr_unit_matched_append_unit. ((exists gr_inverse_matched_append_unitunit. (exists ge_first_rp_matched_append_unitunitidentity ge_first_rn_matched_append_unitunitidentity ge_first_ip_matched_append_unitunitidentity ge_first_in_matched_append_unitunitidentity ge_second_rp_matched_append_unitunitidentity ge_second_rn_matched_append_unitunitidentity ge_second_ip_matched_append_unitunitidentity ge_second_in_matched_append_unitunitidentity. ((exists ge_representation_real_code_matched_append_unitunitidentityfirst ge_representation_imaginary_code_matched_append_unitunitidentityfirst. (((gr_unit_matched_append_unit) = ((ge_representation_real_code_matched_append_unitunitidentityfirst) + (ge_representation_imaginary_code_matched_append_unitunitidentityfirst)) * S ((ge_representation_real_code_matched_append_unitunitidentityfirst) + (ge_representation_imaginary_code_matched_append_unitunitidentityfirst)) + ((ge_representation_imaginary_code_matched_append_unitunitidentityfirst) + (ge_representation_imaginary_code_matched_append_unitunitidentityfirst))) /\ ((exists ge_balance_positive_matched_append_unitunitidentityfirstreal ge_balance_negative_matched_append_unitunitidentityfirstreal. (((((ge_representation_real_code_matched_append_unitunitidentityfirst) = 2 * (ge_balance_positive_matched_append_unitunitidentityfirstreal) /\ (ge_balance_negative_matched_append_unitunitidentityfirstreal) = 0) \/ exists ge_signed_half_matched_append_unitunitidentityfirstrealdecode. (((ge_representation_real_code_matched_append_unitunitidentityfirst) = 2 * ge_signed_half_matched_append_unitunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_matched_append_unitunitidentityfirstreal) = 0) /\ (ge_balance_negative_matched_append_unitunitidentityfirstreal) = S ge_signed_half_matched_append_unitunitidentityfirstrealdecode))) /\ ((ge_first_rp_matched_append_unitunitidentity) + ge_balance_negative_matched_append_unitunitidentityfirstreal = (ge_first_rn_matched_append_unitunitidentity) + ge_balance_positive_matched_append_unitunitidentityfirstreal))) /\ (exists ge_balance_positive_matched_append_unitunitidentityfirstimaginary ge_balance_negative_matched_append_unitunitidentityfirstimaginary. (((((ge_representation_imaginary_code_matched_append_unitunitidentityfirst) = 2 * (ge_balance_positive_matched_append_unitunitidentityfirstimaginary) /\ (ge_balance_negative_matched_append_unitunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_matched_append_unitunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_matched_append_unitunitidentityfirst) = 2 * ge_signed_half_matched_append_unitunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_matched_append_unitunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_matched_append_unitunitidentityfirstimaginary) = S ge_signed_half_matched_append_unitunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_matched_append_unitunitidentity) + ge_balance_negative_matched_append_unitunitidentityfirstimaginary = (ge_first_in_matched_append_unitunitidentity) + ge_balance_positive_matched_append_unitunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_matched_append_unitunitidentitysecond ge_representation_imaginary_code_matched_append_unitunitidentitysecond. (((gr_inverse_matched_append_unitunit) = ((ge_representation_real_code_matched_append_unitunitidentitysecond) + (ge_representation_imaginary_code_matched_append_unitunitidentitysecond)) * S ((ge_representation_real_code_matched_append_unitunitidentitysecond) + (ge_representation_imaginary_code_matched_append_unitunitidentitysecond)) + ((ge_representation_imaginary_code_matched_append_unitunitidentitysecond) + (ge_representation_imaginary_code_matched_append_unitunitidentitysecond))) /\ ((exists ge_balance_positive_matched_append_unitunitidentitysecondreal ge_balance_negative_matched_append_unitunitidentitysecondreal. (((((ge_representation_real_code_matched_append_unitunitidentitysecond) = 2 * (ge_balance_positive_matched_append_unitunitidentitysecondreal) /\ (ge_balance_negative_matched_append_unitunitidentitysecondreal) = 0) \/ exists ge_signed_half_matched_append_unitunitidentitysecondrealdecode. (((ge_representation_real_code_matched_append_unitunitidentitysecond) = 2 * ge_signed_half_matched_append_unitunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_matched_append_unitunitidentitysecondreal) = 0) /\ (ge_balance_negative_matched_append_unitunitidentitysecondreal) = S ge_signed_half_matched_append_unitunitidentitysecondrealdecode))) /\ ((ge_second_rp_matched_append_unitunitidentity) + ge_balance_negative_matched_append_unitunitidentitysecondreal = (ge_second_rn_matched_append_unitunitidentity) + ge_balance_positive_matched_append_unitunitidentitysecondreal))) /\ (exists ge_balance_positive_matched_append_unitunitidentitysecondimaginary ge_balance_negative_matched_append_unitunitidentitysecondimaginary. (((((ge_representation_imaginary_code_matched_append_unitunitidentitysecond) = 2 * (ge_balance_positive_matched_append_unitunitidentitysecondimaginary) /\ (ge_balance_negative_matched_append_unitunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_matched_append_unitunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_matched_append_unitunitidentitysecond) = 2 * ge_signed_half_matched_append_unitunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_matched_append_unitunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_matched_append_unitunitidentitysecondimaginary) = S ge_signed_half_matched_append_unitunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_matched_append_unitunitidentity) + ge_balance_negative_matched_append_unitunitidentitysecondimaginary = (ge_second_in_matched_append_unitunitidentity) + ge_balance_positive_matched_append_unitunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_matched_append_unitunitidentityoutput ge_representation_imaginary_code_matched_append_unitunitidentityoutput. (((6) = ((ge_representation_real_code_matched_append_unitunitidentityoutput) + (ge_representation_imaginary_code_matched_append_unitunitidentityoutput)) * S ((ge_representation_real_code_matched_append_unitunitidentityoutput) + (ge_representation_imaginary_code_matched_append_unitunitidentityoutput)) + ((ge_representation_imaginary_code_matched_append_unitunitidentityoutput) + (ge_representation_imaginary_code_matched_append_unitunitidentityoutput))) /\ ((exists ge_balance_positive_matched_append_unitunitidentityoutputreal ge_balance_negative_matched_append_unitunitidentityoutputreal. (((((ge_representation_real_code_matched_append_unitunitidentityoutput) = 2 * (ge_balance_positive_matched_append_unitunitidentityoutputreal) /\ (ge_balance_negative_matched_append_unitunitidentityoutputreal) = 0) \/ exists ge_signed_half_matched_append_unitunitidentityoutputrealdecode. (((ge_representation_real_code_matched_append_unitunitidentityoutput) = 2 * ge_signed_half_matched_append_unitunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_matched_append_unitunitidentityoutputreal) = 0) /\ (ge_balance_negative_matched_append_unitunitidentityoutputreal) = S ge_signed_half_matched_append_unitunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_matched_append_unitunitidentity) * (ge_second_rp_matched_append_unitunitidentity))) + (((ge_first_rn_matched_append_unitunitidentity) * (ge_second_rn_matched_append_unitunitidentity))))) + (((((ge_first_ip_matched_append_unitunitidentity) * (ge_second_in_matched_append_unitunitidentity))) + (((ge_first_in_matched_append_unitunitidentity) * (ge_second_ip_matched_append_unitunitidentity))))))) + ge_balance_negative_matched_append_unitunitidentityoutputreal = (((((((ge_first_rp_matched_append_unitunitidentity) * (ge_second_rn_matched_append_unitunitidentity))) + (((ge_first_rn_matched_append_unitunitidentity) * (ge_second_rp_matched_append_unitunitidentity))))) + (((((ge_first_ip_matched_append_unitunitidentity) * (ge_second_ip_matched_append_unitunitidentity))) + (((ge_first_in_matched_append_unitunitidentity) * (ge_second_in_matched_append_unitunitidentity))))))) + ge_balance_positive_matched_append_unitunitidentityoutputreal))) /\ (exists ge_balance_positive_matched_append_unitunitidentityoutputimaginary ge_balance_negative_matched_append_unitunitidentityoutputimaginary. (((((ge_representation_imaginary_code_matched_append_unitunitidentityoutput) = 2 * (ge_balance_positive_matched_append_unitunitidentityoutputimaginary) /\ (ge_balance_negative_matched_append_unitunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_matched_append_unitunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_matched_append_unitunitidentityoutput) = 2 * ge_signed_half_matched_append_unitunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_matched_append_unitunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_matched_append_unitunitidentityoutputimaginary) = S ge_signed_half_matched_append_unitunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_matched_append_unitunitidentity) * (ge_second_ip_matched_append_unitunitidentity))) + (((ge_first_rn_matched_append_unitunitidentity) * (ge_second_in_matched_append_unitunitidentity))))) + (((((ge_first_ip_matched_append_unitunitidentity) * (ge_second_rp_matched_append_unitunitidentity))) + (((ge_first_in_matched_append_unitunitidentity) * (ge_second_rn_matched_append_unitunitidentity))))))) + ge_balance_negative_matched_append_unitunitidentityoutputimaginary = (((((((ge_first_rp_matched_append_unitunitidentity) * (ge_second_in_matched_append_unitunitidentity))) + (((ge_first_rn_matched_append_unitunitidentity) * (ge_second_ip_matched_append_unitunitidentity))))) + (((((ge_first_ip_matched_append_unitunitidentity) * (ge_second_rn_matched_append_unitunitidentity))) + (((ge_first_in_matched_append_unitunitidentity) * (ge_second_rp_matched_append_unitunitidentity))))))) + ge_balance_positive_matched_append_unitunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_matched_append_unittransport ge_first_rn_matched_append_unittransport ge_first_ip_matched_append_unittransport ge_first_in_matched_append_unittransport ge_second_rp_matched_append_unittransport ge_second_rn_matched_append_unittransport ge_second_ip_matched_append_unittransport ge_second_in_matched_append_unittransport. ((exists ge_representation_real_code_matched_append_unittransportfirst ge_representation_imaginary_code_matched_append_unittransportfirst. (((gr_unit_matched_append_unit) = ((ge_representation_real_code_matched_append_unittransportfirst) + (ge_representation_imaginary_code_matched_append_unittransportfirst)) * S ((ge_representation_real_code_matched_append_unittransportfirst) + (ge_representation_imaginary_code_matched_append_unittransportfirst)) + ((ge_representation_imaginary_code_matched_append_unittransportfirst) + (ge_representation_imaginary_code_matched_append_unittransportfirst))) /\ ((exists ge_balance_positive_matched_append_unittransportfirstreal ge_balance_negative_matched_append_unittransportfirstreal. (((((ge_representation_real_code_matched_append_unittransportfirst) = 2 * (ge_balance_positive_matched_append_unittransportfirstreal) /\ (ge_balance_negative_matched_append_unittransportfirstreal) = 0) \/ exists ge_signed_half_matched_append_unittransportfirstrealdecode. (((ge_representation_real_code_matched_append_unittransportfirst) = 2 * ge_signed_half_matched_append_unittransportfirstrealdecode + 1 /\ (ge_balance_positive_matched_append_unittransportfirstreal) = 0) /\ (ge_balance_negative_matched_append_unittransportfirstreal) = S ge_signed_half_matched_append_unittransportfirstrealdecode))) /\ ((ge_first_rp_matched_append_unittransport) + ge_balance_negative_matched_append_unittransportfirstreal = (ge_first_rn_matched_append_unittransport) + ge_balance_positive_matched_append_unittransportfirstreal))) /\ (exists ge_balance_positive_matched_append_unittransportfirstimaginary ge_balance_negative_matched_append_unittransportfirstimaginary. (((((ge_representation_imaginary_code_matched_append_unittransportfirst) = 2 * (ge_balance_positive_matched_append_unittransportfirstimaginary) /\ (ge_balance_negative_matched_append_unittransportfirstimaginary) = 0) \/ exists ge_signed_half_matched_append_unittransportfirstimaginarydecode. (((ge_representation_imaginary_code_matched_append_unittransportfirst) = 2 * ge_signed_half_matched_append_unittransportfirstimaginarydecode + 1 /\ (ge_balance_positive_matched_append_unittransportfirstimaginary) = 0) /\ (ge_balance_negative_matched_append_unittransportfirstimaginary) = S ge_signed_half_matched_append_unittransportfirstimaginarydecode))) /\ ((ge_first_ip_matched_append_unittransport) + ge_balance_negative_matched_append_unittransportfirstimaginary = (ge_first_in_matched_append_unittransport) + ge_balance_positive_matched_append_unittransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_matched_append_unittransportsecond ge_representation_imaginary_code_matched_append_unittransportsecond. (((p) = ((ge_representation_real_code_matched_append_unittransportsecond) + (ge_representation_imaginary_code_matched_append_unittransportsecond)) * S ((ge_representation_real_code_matched_append_unittransportsecond) + (ge_representation_imaginary_code_matched_append_unittransportsecond)) + ((ge_representation_imaginary_code_matched_append_unittransportsecond) + (ge_representation_imaginary_code_matched_append_unittransportsecond))) /\ ((exists ge_balance_positive_matched_append_unittransportsecondreal ge_balance_negative_matched_append_unittransportsecondreal. (((((ge_representation_real_code_matched_append_unittransportsecond) = 2 * (ge_balance_positive_matched_append_unittransportsecondreal) /\ (ge_balance_negative_matched_append_unittransportsecondreal) = 0) \/ exists ge_signed_half_matched_append_unittransportsecondrealdecode. (((ge_representation_real_code_matched_append_unittransportsecond) = 2 * ge_signed_half_matched_append_unittransportsecondrealdecode + 1 /\ (ge_balance_positive_matched_append_unittransportsecondreal) = 0) /\ (ge_balance_negative_matched_append_unittransportsecondreal) = S ge_signed_half_matched_append_unittransportsecondrealdecode))) /\ ((ge_second_rp_matched_append_unittransport) + ge_balance_negative_matched_append_unittransportsecondreal = (ge_second_rn_matched_append_unittransport) + ge_balance_positive_matched_append_unittransportsecondreal))) /\ (exists ge_balance_positive_matched_append_unittransportsecondimaginary ge_balance_negative_matched_append_unittransportsecondimaginary. (((((ge_representation_imaginary_code_matched_append_unittransportsecond) = 2 * (ge_balance_positive_matched_append_unittransportsecondimaginary) /\ (ge_balance_negative_matched_append_unittransportsecondimaginary) = 0) \/ exists ge_signed_half_matched_append_unittransportsecondimaginarydecode. (((ge_representation_imaginary_code_matched_append_unittransportsecond) = 2 * ge_signed_half_matched_append_unittransportsecondimaginarydecode + 1 /\ (ge_balance_positive_matched_append_unittransportsecondimaginary) = 0) /\ (ge_balance_negative_matched_append_unittransportsecondimaginary) = S ge_signed_half_matched_append_unittransportsecondimaginarydecode))) /\ ((ge_second_ip_matched_append_unittransport) + ge_balance_negative_matched_append_unittransportsecondimaginary = (ge_second_in_matched_append_unittransport) + ge_balance_positive_matched_append_unittransportsecondimaginary)))))) /\ (exists ge_representation_real_code_matched_append_unittransportoutput ge_representation_imaginary_code_matched_append_unittransportoutput. (((q) = ((ge_representation_real_code_matched_append_unittransportoutput) + (ge_representation_imaginary_code_matched_append_unittransportoutput)) * S ((ge_representation_real_code_matched_append_unittransportoutput) + (ge_representation_imaginary_code_matched_append_unittransportoutput)) + ((ge_representation_imaginary_code_matched_append_unittransportoutput) + (ge_representation_imaginary_code_matched_append_unittransportoutput))) /\ ((exists ge_balance_positive_matched_append_unittransportoutputreal ge_balance_negative_matched_append_unittransportoutputreal. (((((ge_representation_real_code_matched_append_unittransportoutput) = 2 * (ge_balance_positive_matched_append_unittransportoutputreal) /\ (ge_balance_negative_matched_append_unittransportoutputreal) = 0) \/ exists ge_signed_half_matched_append_unittransportoutputrealdecode. (((ge_representation_real_code_matched_append_unittransportoutput) = 2 * ge_signed_half_matched_append_unittransportoutputrealdecode + 1 /\ (ge_balance_positive_matched_append_unittransportoutputreal) = 0) /\ (ge_balance_negative_matched_append_unittransportoutputreal) = S ge_signed_half_matched_append_unittransportoutputrealdecode))) /\ ((((((((ge_first_rp_matched_append_unittransport) * (ge_second_rp_matched_append_unittransport))) + (((ge_first_rn_matched_append_unittransport) * (ge_second_rn_matched_append_unittransport))))) + (((((ge_first_ip_matched_append_unittransport) * (ge_second_in_matched_append_unittransport))) + (((ge_first_in_matched_append_unittransport) * (ge_second_ip_matched_append_unittransport))))))) + ge_balance_negative_matched_append_unittransportoutputreal = (((((((ge_first_rp_matched_append_unittransport) * (ge_second_rn_matched_append_unittransport))) + (((ge_first_rn_matched_append_unittransport) * (ge_second_rp_matched_append_unittransport))))) + (((((ge_first_ip_matched_append_unittransport) * (ge_second_ip_matched_append_unittransport))) + (((ge_first_in_matched_append_unittransport) * (ge_second_in_matched_append_unittransport))))))) + ge_balance_positive_matched_append_unittransportoutputreal))) /\ (exists ge_balance_positive_matched_append_unittransportoutputimaginary ge_balance_negative_matched_append_unittransportoutputimaginary. (((((ge_representation_imaginary_code_matched_append_unittransportoutput) = 2 * (ge_balance_positive_matched_append_unittransportoutputimaginary) /\ (ge_balance_negative_matched_append_unittransportoutputimaginary) = 0) \/ exists ge_signed_half_matched_append_unittransportoutputimaginarydecode. (((ge_representation_imaginary_code_matched_append_unittransportoutput) = 2 * ge_signed_half_matched_append_unittransportoutputimaginarydecode + 1 /\ (ge_balance_positive_matched_append_unittransportoutputimaginary) = 0) /\ (ge_balance_negative_matched_append_unittransportoutputimaginary) = S ge_signed_half_matched_append_unittransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_matched_append_unittransport) * (ge_second_ip_matched_append_unittransport))) + (((ge_first_rn_matched_append_unittransport) * (ge_second_in_matched_append_unittransport))))) + (((((ge_first_ip_matched_append_unittransport) * (ge_second_rp_matched_append_unittransport))) + (((ge_first_in_matched_append_unittransport) * (ge_second_rn_matched_append_unittransport))))))) + ge_balance_negative_matched_append_unittransportoutputimaginary = (((((((ge_first_rp_matched_append_unittransport) * (ge_second_in_matched_append_unittransport))) + (((ge_first_rn_matched_append_unittransport) * (ge_second_ip_matched_append_unittransport))))) + (((((ge_first_ip_matched_append_unittransport) * (ge_second_rn_matched_append_unittransport))) + (((ge_first_in_matched_append_unittransport) * (ge_second_rp_matched_append_unittransport))))))) + ge_balance_positive_matched_append_unittransportoutputimaginary))))))))))) -> exists U V. ((((((forall pfp_i_matched_append_newbijectionbounded. (exists pfp_gap_matched_append_newbijectionboundedindex. pfp_gap_matched_append_newbijectionboundedindex + S (pfp_i_matched_append_newbijectionbounded) = (S l)) -> exists pfp_a_matched_append_newbijectionbounded. (((exists ff_h_pfp_matched_append_newbijectionboundedentry. ff_h_pfp_matched_append_newbijectionboundedentry + S (pfp_a_matched_append_newbijectionbounded) = S ((S (pfp_i_matched_append_newbijectionbounded)) * V)) /\ exists ff_q_pfp_matched_append_newbijectionboundedentry. U = ff_q_pfp_matched_append_newbijectionboundedentry * S ((S (pfp_i_matched_append_newbijectionbounded)) * V) + (pfp_a_matched_append_newbijectionbounded))) /\ (exists pfp_gap_matched_append_newbijectionboundedvalue. pfp_gap_matched_append_newbijectionboundedvalue + S (pfp_a_matched_append_newbijectionbounded) = (S l))) /\ (((forall pfp_i_matched_append_newbijectioninjective pfp_j_matched_append_newbijectioninjective pfp_a_matched_append_newbijectioninjective. (exists pfp_gap_matched_append_newbijectioninjectivefirst. pfp_gap_matched_append_newbijectioninjectivefirst + S (pfp_i_matched_append_newbijectioninjective) = (S l)) -> (exists pfp_gap_matched_append_newbijectioninjectivesecond. pfp_gap_matched_append_newbijectioninjectivesecond + S (pfp_j_matched_append_newbijectioninjective) = (S l)) -> (((exists ff_h_pfp_matched_append_newbijectioninjectiveleft. ff_h_pfp_matched_append_newbijectioninjectiveleft + S (pfp_a_matched_append_newbijectioninjective) = S ((S (pfp_i_matched_append_newbijectioninjective)) * V)) /\ exists ff_q_pfp_matched_append_newbijectioninjectiveleft. U = ff_q_pfp_matched_append_newbijectioninjectiveleft * S ((S (pfp_i_matched_append_newbijectioninjective)) * V) + (pfp_a_matched_append_newbijectioninjective))) -> (((exists ff_h_pfp_matched_append_newbijectioninjectiveright. ff_h_pfp_matched_append_newbijectioninjectiveright + S (pfp_a_matched_append_newbijectioninjective) = S ((S (pfp_j_matched_append_newbijectioninjective)) * V)) /\ exists ff_q_pfp_matched_append_newbijectioninjectiveright. U = ff_q_pfp_matched_append_newbijectioninjectiveright * S ((S (pfp_j_matched_append_newbijectioninjective)) * V) + (pfp_a_matched_append_newbijectioninjective))) -> pfp_i_matched_append_newbijectioninjective = pfp_j_matched_append_newbijectioninjective) /\ (forall pfp_a_matched_append_newbijectionsurjective. (exists pfp_gap_matched_append_newbijectionsurjectivevalue. pfp_gap_matched_append_newbijectionsurjectivevalue + S (pfp_a_matched_append_newbijectionsurjective) = (S l)) -> exists pfp_i_matched_append_newbijectionsurjective. (exists pfp_gap_matched_append_newbijectionsurjectiveindex. pfp_gap_matched_append_newbijectionsurjectiveindex + S (pfp_i_matched_append_newbijectionsurjective) = (S l)) /\ (((exists ff_h_pfp_matched_append_newbijectionsurjectiveentry. ff_h_pfp_matched_append_newbijectionsurjectiveentry + S (pfp_a_matched_append_newbijectionsurjective) = S ((S (pfp_i_matched_append_newbijectionsurjective)) * V)) /\ exists ff_q_pfp_matched_append_newbijectionsurjectiveentry. U = ff_q_pfp_matched_append_newbijectionsurjectiveentry * S ((S (pfp_i_matched_append_newbijectionsurjective)) * V) + (pfp_a_matched_append_newbijectionsurjective)))))))) /\ (forall gr_match_index_matched_append_newmatching gr_match_image_matched_append_newmatching gr_match_source_matched_append_newmatching gr_match_target_matched_append_newmatching. (exists ge_gap_matched_append_newmatchingindex. ge_gap_matched_append_newmatchingindex + S (gr_match_index_matched_append_newmatching) = (S l)) -> (((exists ff_h_gprod_matched_append_newmatchingmap. ff_h_gprod_matched_append_newmatchingmap + S (gr_match_image_matched_append_newmatching) = S ((S (gr_match_index_matched_append_newmatching)) * V)) /\ exists ff_q_gprod_matched_append_newmatchingmap. U = ff_q_gprod_matched_append_newmatchingmap * S ((S (gr_match_index_matched_append_newmatching)) * V) + (gr_match_image_matched_append_newmatching))) -> (((exists ff_h_gprod_matched_append_newmatchingsource. ff_h_gprod_matched_append_newmatchingsource + S (gr_match_source_matched_append_newmatching) = S ((S (gr_match_index_matched_append_newmatching)) * c)) /\ exists ff_q_gprod_matched_append_newmatchingsource. b = ff_q_gprod_matched_append_newmatchingsource * S ((S (gr_match_index_matched_append_newmatching)) * c) + (gr_match_source_matched_append_newmatching))) -> (((exists ff_h_gprod_matched_append_newmatchingtarget. ff_h_gprod_matched_append_newmatchingtarget + S (gr_match_target_matched_append_newmatching) = S ((S (gr_match_image_matched_append_newmatching)) * e)) /\ exists ff_q_gprod_matched_append_newmatchingtarget. d = ff_q_gprod_matched_append_newmatchingtarget * S ((S (gr_match_image_matched_append_newmatching)) * e) + (gr_match_target_matched_append_newmatching))) -> (exists gr_unit_matched_append_newmatchingunit_witness. ((exists gr_inverse_matched_append_newmatchingunit_witnessunit. (exists ge_first_rp_matched_append_newmatchingunit_witnessunitidentity ge_first_rn_matched_append_newmatchingunit_witnessunitidentity ge_first_ip_matched_append_newmatchingunit_witnessunitidentity ge_first_in_matched_append_newmatchingunit_witnessunitidentity ge_second_rp_matched_append_newmatchingunit_witnessunitidentity ge_second_rn_matched_append_newmatchingunit_witnessunitidentity ge_second_ip_matched_append_newmatchingunit_witnessunitidentity ge_second_in_matched_append_newmatchingunit_witnessunitidentity. ((exists ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityfirst ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityfirst. (((gr_unit_matched_append_newmatchingunit_witness) = ((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityfirstreal ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_matched_append_newmatchingunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityfirstreal) = S ge_signed_half_matched_append_newmatchingunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_matched_append_newmatchingunit_witnessunitidentity) + ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityfirstreal = (ge_first_rn_matched_append_newmatchingunit_witnessunitidentity) + ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityfirstimaginary ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityfirst) = 2 * ge_signed_half_matched_append_newmatchingunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityfirstimaginary) = S ge_signed_half_matched_append_newmatchingunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_matched_append_newmatchingunit_witnessunitidentity) + ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityfirstimaginary = (ge_first_in_matched_append_newmatchingunit_witnessunitidentity) + ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentitysecond ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentitysecond. (((gr_inverse_matched_append_newmatchingunit_witnessunit) = ((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_matched_append_newmatchingunit_witnessunitidentitysecondreal ge_balance_negative_matched_append_newmatchingunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_matched_append_newmatchingunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentitysecondreal) = S ge_signed_half_matched_append_newmatchingunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_matched_append_newmatchingunit_witnessunitidentity) + ge_balance_negative_matched_append_newmatchingunit_witnessunitidentitysecondreal = (ge_second_rn_matched_append_newmatchingunit_witnessunitidentity) + ge_balance_positive_matched_append_newmatchingunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_matched_append_newmatchingunit_witnessunitidentitysecondimaginary ge_balance_negative_matched_append_newmatchingunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentitysecond) = 2 * ge_signed_half_matched_append_newmatchingunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentitysecondimaginary) = S ge_signed_half_matched_append_newmatchingunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_matched_append_newmatchingunit_witnessunitidentity) + ge_balance_negative_matched_append_newmatchingunit_witnessunitidentitysecondimaginary = (ge_second_in_matched_append_newmatchingunit_witnessunitidentity) + ge_balance_positive_matched_append_newmatchingunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityoutput ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityoutputreal ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_matched_append_newmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_matched_append_newmatchingunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityoutputreal) = S ge_signed_half_matched_append_newmatchingunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_rp_matched_append_newmatchingunit_witnessunitidentity))) + (((ge_first_rn_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_rn_matched_append_newmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_in_matched_append_newmatchingunit_witnessunitidentity))) + (((ge_first_in_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_ip_matched_append_newmatchingunit_witnessunitidentity))))))) + ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityoutputreal = (((((((ge_first_rp_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_rn_matched_append_newmatchingunit_witnessunitidentity))) + (((ge_first_rn_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_rp_matched_append_newmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_ip_matched_append_newmatchingunit_witnessunitidentity))) + (((ge_first_in_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_in_matched_append_newmatchingunit_witnessunitidentity))))))) + ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityoutputimaginary ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_matched_append_newmatchingunit_witnessunitidentityoutput) = 2 * ge_signed_half_matched_append_newmatchingunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityoutputimaginary) = S ge_signed_half_matched_append_newmatchingunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_ip_matched_append_newmatchingunit_witnessunitidentity))) + (((ge_first_rn_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_in_matched_append_newmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_rp_matched_append_newmatchingunit_witnessunitidentity))) + (((ge_first_in_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_rn_matched_append_newmatchingunit_witnessunitidentity))))))) + ge_balance_negative_matched_append_newmatchingunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_in_matched_append_newmatchingunit_witnessunitidentity))) + (((ge_first_rn_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_ip_matched_append_newmatchingunit_witnessunitidentity))))) + (((((ge_first_ip_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_rn_matched_append_newmatchingunit_witnessunitidentity))) + (((ge_first_in_matched_append_newmatchingunit_witnessunitidentity) * (ge_second_rp_matched_append_newmatchingunit_witnessunitidentity))))))) + ge_balance_positive_matched_append_newmatchingunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_matched_append_newmatchingunit_witnesstransport ge_first_rn_matched_append_newmatchingunit_witnesstransport ge_first_ip_matched_append_newmatchingunit_witnesstransport ge_first_in_matched_append_newmatchingunit_witnesstransport ge_second_rp_matched_append_newmatchingunit_witnesstransport ge_second_rn_matched_append_newmatchingunit_witnesstransport ge_second_ip_matched_append_newmatchingunit_witnesstransport ge_second_in_matched_append_newmatchingunit_witnesstransport. ((exists ge_representation_real_code_matched_append_newmatchingunit_witnesstransportfirst ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportfirst. (((gr_unit_matched_append_newmatchingunit_witness) = ((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportfirst)) * S ((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportfirst) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_matched_append_newmatchingunit_witnesstransportfirstreal ge_balance_negative_matched_append_newmatchingunit_witnesstransportfirstreal. (((((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnesstransportfirstreal) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_matched_append_newmatchingunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportfirstreal) = S ge_signed_half_matched_append_newmatchingunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_matched_append_newmatchingunit_witnesstransport) + ge_balance_negative_matched_append_newmatchingunit_witnesstransportfirstreal = (ge_first_rn_matched_append_newmatchingunit_witnesstransport) + ge_balance_positive_matched_append_newmatchingunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_matched_append_newmatchingunit_witnesstransportfirstimaginary ge_balance_negative_matched_append_newmatchingunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportfirst) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportfirst) = 2 * ge_signed_half_matched_append_newmatchingunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportfirstimaginary) = S ge_signed_half_matched_append_newmatchingunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_matched_append_newmatchingunit_witnesstransport) + ge_balance_negative_matched_append_newmatchingunit_witnesstransportfirstimaginary = (ge_first_in_matched_append_newmatchingunit_witnesstransport) + ge_balance_positive_matched_append_newmatchingunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_matched_append_newmatchingunit_witnesstransportsecond ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportsecond. (((gr_match_source_matched_append_newmatching) = ((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportsecond)) * S ((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportsecond) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_matched_append_newmatchingunit_witnesstransportsecondreal ge_balance_negative_matched_append_newmatchingunit_witnesstransportsecondreal. (((((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnesstransportsecondreal) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_matched_append_newmatchingunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportsecondreal) = S ge_signed_half_matched_append_newmatchingunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_matched_append_newmatchingunit_witnesstransport) + ge_balance_negative_matched_append_newmatchingunit_witnesstransportsecondreal = (ge_second_rn_matched_append_newmatchingunit_witnesstransport) + ge_balance_positive_matched_append_newmatchingunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_matched_append_newmatchingunit_witnesstransportsecondimaginary ge_balance_negative_matched_append_newmatchingunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportsecond) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportsecond) = 2 * ge_signed_half_matched_append_newmatchingunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportsecondimaginary) = S ge_signed_half_matched_append_newmatchingunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_matched_append_newmatchingunit_witnesstransport) + ge_balance_negative_matched_append_newmatchingunit_witnesstransportsecondimaginary = (ge_second_in_matched_append_newmatchingunit_witnesstransport) + ge_balance_positive_matched_append_newmatchingunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_matched_append_newmatchingunit_witnesstransportoutput ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportoutput. (((gr_match_target_matched_append_newmatching) = ((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportoutput)) * S ((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportoutput) + (ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_matched_append_newmatchingunit_witnesstransportoutputreal ge_balance_negative_matched_append_newmatchingunit_witnesstransportoutputreal. (((((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnesstransportoutputreal) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_matched_append_newmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_matched_append_newmatchingunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportoutputreal) = S ge_signed_half_matched_append_newmatchingunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_matched_append_newmatchingunit_witnesstransport) * (ge_second_rp_matched_append_newmatchingunit_witnesstransport))) + (((ge_first_rn_matched_append_newmatchingunit_witnesstransport) * (ge_second_rn_matched_append_newmatchingunit_witnesstransport))))) + (((((ge_first_ip_matched_append_newmatchingunit_witnesstransport) * (ge_second_in_matched_append_newmatchingunit_witnesstransport))) + (((ge_first_in_matched_append_newmatchingunit_witnesstransport) * (ge_second_ip_matched_append_newmatchingunit_witnesstransport))))))) + ge_balance_negative_matched_append_newmatchingunit_witnesstransportoutputreal = (((((((ge_first_rp_matched_append_newmatchingunit_witnesstransport) * (ge_second_rn_matched_append_newmatchingunit_witnesstransport))) + (((ge_first_rn_matched_append_newmatchingunit_witnesstransport) * (ge_second_rp_matched_append_newmatchingunit_witnesstransport))))) + (((((ge_first_ip_matched_append_newmatchingunit_witnesstransport) * (ge_second_ip_matched_append_newmatchingunit_witnesstransport))) + (((ge_first_in_matched_append_newmatchingunit_witnesstransport) * (ge_second_in_matched_append_newmatchingunit_witnesstransport))))))) + ge_balance_positive_matched_append_newmatchingunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_matched_append_newmatchingunit_witnesstransportoutputimaginary ge_balance_negative_matched_append_newmatchingunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportoutput) = 2 * (ge_balance_positive_matched_append_newmatchingunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_matched_append_newmatchingunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_matched_append_newmatchingunit_witnesstransportoutput) = 2 * ge_signed_half_matched_append_newmatchingunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_matched_append_newmatchingunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_matched_append_newmatchingunit_witnesstransportoutputimaginary) = S ge_signed_half_matched_append_newmatchingunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_matched_append_newmatchingunit_witnesstransport) * (ge_second_ip_matched_append_newmatchingunit_witnesstransport))) + (((ge_first_rn_matched_append_newmatchingunit_witnesstransport) * (ge_second_in_matched_append_newmatchingunit_witnesstransport))))) + (((((ge_first_ip_matched_append_newmatchingunit_witnesstransport) * (ge_second_rp_matched_append_newmatchingunit_witnesstransport))) + (((ge_first_in_matched_append_newmatchingunit_witnesstransport) * (ge_second_rn_matched_append_newmatchingunit_witnesstransport))))))) + ge_balance_negative_matched_append_newmatchingunit_witnesstransportoutputimaginary = (((((((ge_first_rp_matched_append_newmatchingunit_witnesstransport) * (ge_second_in_matched_append_newmatchingunit_witnesstransport))) + (((ge_first_rn_matched_append_newmatchingunit_witnesstransport) * (ge_second_ip_matched_append_newmatchingunit_witnesstransport))))) + (((((ge_first_ip_matched_append_newmatchingunit_witnesstransport) * (ge_second_rn_matched_append_newmatchingunit_witnesstransport))) + (((ge_first_in_matched_append_newmatchingunit_witnesstransport) * (ge_second_rp_matched_append_newmatchingunit_witnesstransport))))))) + ge_balance_positive_matched_append_newmatchingunit_witnesstransportoutputimaginary)))))))))))))) /\ (((((exists ff_h_pfp_matched_append_extensionlast. ff_h_pfp_matched_append_extensionlast + S (l) = S ((S (l)) * V)) /\ exists ff_q_pfp_matched_append_extensionlast. U = ff_q_pfp_matched_append_extensionlast * S ((S (l)) * V) + (l))) /\ (forall pfp_i_matched_append_extensionprefix pfp_a_matched_append_extensionprefix. (exists pfp_gap_matched_append_extensionprefixbound. pfp_gap_matched_append_extensionprefixbound + S (pfp_i_matched_append_extensionprefix) = (l)) -> (((exists ff_h_pfp_matched_append_extensionprefixold. ff_h_pfp_matched_append_extensionprefixold + S (pfp_a_matched_append_extensionprefix) = S ((S (pfp_i_matched_append_extensionprefix)) * v)) /\ exists ff_q_pfp_matched_append_extensionprefixold. u = ff_q_pfp_matched_append_extensionprefixold * S ((S (pfp_i_matched_append_extensionprefix)) * v) + (pfp_a_matched_append_extensionprefix))) -> (((exists ff_h_pfp_matched_append_extensionprefixnew. ff_h_pfp_matched_append_extensionprefixnew + S (pfp_a_matched_append_extensionprefix) = S ((S (pfp_i_matched_append_extensionprefix)) * V)) /\ exists ff_q_pfp_matched_append_extensionprefixnew. U = ff_q_pfp_matched_append_extensionprefixnew * S ((S (pfp_i_matched_append_extensionprefix)) * V) + (pfp_a_matched_append_extensionprefix)))))))