Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ b. ∀ c. ∀ d. ∀ e. ∀ u. ∀ v. ∀ l. ∀ p. ∀ q. GMatchedFactors(b,c,d,e,u,v,l) → BetaAt(b,c,l,p) → BetaAt(d,e,l,q) → GAssociate(p,q) → ∃ x. ∃ y. GMatchedFactors(b,c,d,e,x,y,S l) ∧ (BetaAt(x,y,l,l) ∧ (∀ z. ∀ n. Lt(z,l) → BetaAt(u,v,z,n) → BetaAt(x,y,z,n)))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order 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)))))))Complete tactic proof in conservative notation
All 46 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
46 script commands · 9 reading checkpoints · 1 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–13
03Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
cases hm
04Establish hextL15–20
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation index extend.
- L15
have hext : ∃ U. ∃ V. PermutationPrefix(U,V,S l) ∧ (BetaAt(U,V,l,l) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(u,v,x,y) → BetaAt(U,V,x,y)))Definitions: PermutationPrefix(U,V,S l)BetaAt(U,V,l,l)Lt(x,l)BetaAt(u,v,x,y)BetaAt(U,V,x,y)Original native command in the exact edition - L16
specialize factor_permutation_index_extend (u) - L17
specialize factor_permutation_index_extend (v) - L18
specialize factor_permutation_index_extend (l) - L19
apply factor_permutation_index_extend - L20
exact hm_left
05Separate the logical casesL21–23
06Construct an explicit witnessL24–25
07Separate the logical casesL26–27
08Use earlier factsL28–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L28
exact hext_witness_witness_left - L29
specialize gaussian_factor_matching_append (b) - L30
specialize gaussian_factor_matching_append (c) - L31
specialize gaussian_factor_matching_append (d) - L32
specialize gaussian_factor_matching_append (e) - L33
specialize gaussian_factor_matching_append (u) - L34
specialize gaussian_factor_matching_append (v) - L35
specialize gaussian_factor_matching_append (x) - L36
specialize gaussian_factor_matching_append (x1) - L37
specialize gaussian_factor_matching_append (l)
09Use earlier factsL38–46
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 46 lines
- 0001
intro b - 0002
intro c - 0003
intro d - 0004
intro e - 0005
intro u - 0006
intro v - 0007
intro l - 0008
intro p - 0009
intro q - 0010
intro hm - 0011
intro hp - 0012
intro hq - 0013
intro hpq - 0014
cases hm - 0015
have hext : ∃ U. ∃ V. PermutationPrefix(U,V,S l) ∧ (BetaAt(U,V,l,l) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(u,v,x,y) → BetaAt(U,V,x,y))) - 0016
specialize factor_permutation_index_extend (u) - 0017
specialize factor_permutation_index_extend (v) - 0018
specialize factor_permutation_index_extend (l) - 0019
apply factor_permutation_index_extend - 0020
exact hm_left - 0021
cases hext - 0022
cases hext_witness - 0023
cases hext_witness_witness - 0024
exists (x) - 0025
exists (x1) - 0026
split - 0027
split - 0028
exact hext_witness_witness_left - 0029
specialize gaussian_factor_matching_append (b) - 0030
specialize gaussian_factor_matching_append (c) - 0031
specialize gaussian_factor_matching_append (d) - 0032
specialize gaussian_factor_matching_append (e) - 0033
specialize gaussian_factor_matching_append (u) - 0034
specialize gaussian_factor_matching_append (v) - 0035
specialize gaussian_factor_matching_append (x) - 0036
specialize gaussian_factor_matching_append (x1) - 0037
specialize gaussian_factor_matching_append (l) - 0038
specialize gaussian_factor_matching_append (p) - 0039
specialize gaussian_factor_matching_append (q) - 0040
apply gaussian_factor_matching_append - 0041
exact hm_right - 0042
exact hext_witness_witness_right - 0043
exact hp - 0044
exact hq - 0045
exact hpq - 0046
exact hext_witness_witness_right