GF00A8 — gaussian_factor_matching_append

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. ∀ U. ∀ V. ∀ l. ∀ p. ∀ q. GFactorAssociateMatching(b,c,d,e,u,v,l) → BetaAt(U,V,l,l) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(u,v,x,y) → BetaAt(U,V,x,y)) → BetaAt(b,c,l,p) → BetaAt(d,e,l,q) → GAssociate(p,q) → GFactorAssociateMatching(b,c,d,e,U,V,S l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

GAssociate(a,b) · 1 GFactorAssociateMatching(b,c,d,e,u,v,l) · 2 Lt(a,b) · 2 BetaAt(b,c,i,x) · 5

Actual proof prerequisites

finite_lt_succ_eq_or_lt · checked external prerequisitegaussian_product_beta_index_transportbeta_at_unique · checked external prerequisitegaussian_factor_associate_code_transport factor_permutation_prefix_reflect · checked external prerequisite

Original expanded first-order statement

forall b c d e u v U V l p q. (forall gr_match_index_append_matching_old gr_match_image_append_matching_old gr_match_source_append_matching_old gr_match_target_append_matching_old. (exists ge_gap_append_matching_oldindex. ge_gap_append_matching_oldindex + S (gr_match_index_append_matching_old) = (l)) -> (((exists ff_h_gprod_append_matching_oldmap. ff_h_gprod_append_matching_oldmap + S (gr_match_image_append_matching_old) = S ((S (gr_match_index_append_matching_old)) * v)) /\ exists ff_q_gprod_append_matching_oldmap. u = ff_q_gprod_append_matching_oldmap * S ((S (gr_match_index_append_matching_old)) * v) + (gr_match_image_append_matching_old))) -> (((exists ff_h_gprod_append_matching_oldsource. ff_h_gprod_append_matching_oldsource + S (gr_match_source_append_matching_old) = S ((S (gr_match_index_append_matching_old)) * c)) /\ exists ff_q_gprod_append_matching_oldsource. b = ff_q_gprod_append_matching_oldsource * S ((S (gr_match_index_append_matching_old)) * c) + (gr_match_source_append_matching_old))) -> (((exists ff_h_gprod_append_matching_oldtarget. ff_h_gprod_append_matching_oldtarget + S (gr_match_target_append_matching_old) = S ((S (gr_match_image_append_matching_old)) * e)) /\ exists ff_q_gprod_append_matching_oldtarget. d = ff_q_gprod_append_matching_oldtarget * S ((S (gr_match_image_append_matching_old)) * e) + (gr_match_target_append_matching_old))) -> (exists gr_unit_append_matching_oldunit_witness. ((exists gr_inverse_append_matching_oldunit_witnessunit. (exists ge_first_rp_append_matching_oldunit_witnessunitidentity ge_first_rn_append_matching_oldunit_witnessunitidentity ge_first_ip_append_matching_oldunit_witnessunitidentity ge_first_in_append_matching_oldunit_witnessunitidentity ge_second_rp_append_matching_oldunit_witnessunitidentity ge_second_rn_append_matching_oldunit_witnessunitidentity ge_second_ip_append_matching_oldunit_witnessunitidentity ge_second_in_append_matching_oldunit_witnessunitidentity. ((exists ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst. (((gr_unit_append_matching_oldunit_witness) = ((ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstreal ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnessunitidentityfirst) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstreal) = S ge_signed_half_append_matching_oldunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_matching_oldunit_witnessunitidentity) + ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstreal = (ge_first_rn_append_matching_oldunit_witnessunitidentity) + ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstimaginary ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityfirst) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstimaginary) = S ge_signed_half_append_matching_oldunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_oldunit_witnessunitidentity) + ge_balance_negative_append_matching_oldunit_witnessunitidentityfirstimaginary = (ge_first_in_append_matching_oldunit_witnessunitidentity) + ge_balance_positive_append_matching_oldunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond. (((gr_inverse_append_matching_oldunit_witnessunit) = ((ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondreal ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnessunitidentitysecond) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondreal) = S ge_signed_half_append_matching_oldunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_matching_oldunit_witnessunitidentity) + ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondreal = (ge_second_rn_append_matching_oldunit_witnessunitidentity) + ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondimaginary ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentitysecond) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondimaginary) = S ge_signed_half_append_matching_oldunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_matching_oldunit_witnessunitidentity) + ge_balance_negative_append_matching_oldunit_witnessunitidentitysecondimaginary = (ge_second_in_append_matching_oldunit_witnessunitidentity) + ge_balance_positive_append_matching_oldunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputreal ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnessunitidentityoutput) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputreal) = S ge_signed_half_append_matching_oldunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_oldunit_witnessunitidentity) * (ge_second_rp_append_matching_oldunit_witnessunitidentity))) + (((ge_first_rn_append_matching_oldunit_witnessunitidentity) * (ge_second_rn_append_matching_oldunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_oldunit_witnessunitidentity) * (ge_second_in_append_matching_oldunit_witnessunitidentity))) + (((ge_first_in_append_matching_oldunit_witnessunitidentity) * (ge_second_ip_append_matching_oldunit_witnessunitidentity))))))) + ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputreal = (((((((ge_first_rp_append_matching_oldunit_witnessunitidentity) * (ge_second_rn_append_matching_oldunit_witnessunitidentity))) + (((ge_first_rn_append_matching_oldunit_witnessunitidentity) * (ge_second_rp_append_matching_oldunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_oldunit_witnessunitidentity) * (ge_second_ip_append_matching_oldunit_witnessunitidentity))) + (((ge_first_in_append_matching_oldunit_witnessunitidentity) * (ge_second_in_append_matching_oldunit_witnessunitidentity))))))) + ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputimaginary ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnessunitidentityoutput) = 2 * ge_signed_half_append_matching_oldunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputimaginary) = S ge_signed_half_append_matching_oldunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_oldunit_witnessunitidentity) * (ge_second_ip_append_matching_oldunit_witnessunitidentity))) + (((ge_first_rn_append_matching_oldunit_witnessunitidentity) * (ge_second_in_append_matching_oldunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_oldunit_witnessunitidentity) * (ge_second_rp_append_matching_oldunit_witnessunitidentity))) + (((ge_first_in_append_matching_oldunit_witnessunitidentity) * (ge_second_rn_append_matching_oldunit_witnessunitidentity))))))) + ge_balance_negative_append_matching_oldunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_append_matching_oldunit_witnessunitidentity) * (ge_second_in_append_matching_oldunit_witnessunitidentity))) + (((ge_first_rn_append_matching_oldunit_witnessunitidentity) * (ge_second_ip_append_matching_oldunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_oldunit_witnessunitidentity) * (ge_second_rn_append_matching_oldunit_witnessunitidentity))) + (((ge_first_in_append_matching_oldunit_witnessunitidentity) * (ge_second_rp_append_matching_oldunit_witnessunitidentity))))))) + ge_balance_positive_append_matching_oldunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_append_matching_oldunit_witnesstransport ge_first_rn_append_matching_oldunit_witnesstransport ge_first_ip_append_matching_oldunit_witnesstransport ge_first_in_append_matching_oldunit_witnesstransport ge_second_rp_append_matching_oldunit_witnesstransport ge_second_rn_append_matching_oldunit_witnesstransport ge_second_ip_append_matching_oldunit_witnesstransport ge_second_in_append_matching_oldunit_witnesstransport. ((exists ge_representation_real_code_append_matching_oldunit_witnesstransportfirst ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst. (((gr_unit_append_matching_oldunit_witness) = ((ge_representation_real_code_append_matching_oldunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst)) * S ((ge_representation_real_code_append_matching_oldunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnesstransportfirstreal ge_balance_negative_append_matching_oldunit_witnesstransportfirstreal. (((((ge_representation_real_code_append_matching_oldunit_witnesstransportfirst) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportfirstreal) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnesstransportfirst) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportfirstreal) = S ge_signed_half_append_matching_oldunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_append_matching_oldunit_witnesstransport) + ge_balance_negative_append_matching_oldunit_witnesstransportfirstreal = (ge_first_rn_append_matching_oldunit_witnesstransport) + ge_balance_positive_append_matching_oldunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnesstransportfirstimaginary ge_balance_negative_append_matching_oldunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportfirst) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportfirstimaginary) = S ge_signed_half_append_matching_oldunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_oldunit_witnesstransport) + ge_balance_negative_append_matching_oldunit_witnesstransportfirstimaginary = (ge_first_in_append_matching_oldunit_witnesstransport) + ge_balance_positive_append_matching_oldunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_oldunit_witnesstransportsecond ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond. (((gr_match_source_append_matching_old) = ((ge_representation_real_code_append_matching_oldunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond)) * S ((ge_representation_real_code_append_matching_oldunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnesstransportsecondreal ge_balance_negative_append_matching_oldunit_witnesstransportsecondreal. (((((ge_representation_real_code_append_matching_oldunit_witnesstransportsecond) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportsecondreal) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnesstransportsecond) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportsecondreal) = S ge_signed_half_append_matching_oldunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_append_matching_oldunit_witnesstransport) + ge_balance_negative_append_matching_oldunit_witnesstransportsecondreal = (ge_second_rn_append_matching_oldunit_witnesstransport) + ge_balance_positive_append_matching_oldunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnesstransportsecondimaginary ge_balance_negative_append_matching_oldunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportsecond) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportsecondimaginary) = S ge_signed_half_append_matching_oldunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_append_matching_oldunit_witnesstransport) + ge_balance_negative_append_matching_oldunit_witnesstransportsecondimaginary = (ge_second_in_append_matching_oldunit_witnesstransport) + ge_balance_positive_append_matching_oldunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_oldunit_witnesstransportoutput ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput. (((gr_match_target_append_matching_old) = ((ge_representation_real_code_append_matching_oldunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput)) * S ((ge_representation_real_code_append_matching_oldunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_append_matching_oldunit_witnesstransportoutputreal ge_balance_negative_append_matching_oldunit_witnesstransportoutputreal. (((((ge_representation_real_code_append_matching_oldunit_witnesstransportoutput) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportoutputreal) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_append_matching_oldunit_witnesstransportoutput) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportoutputreal) = S ge_signed_half_append_matching_oldunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_oldunit_witnesstransport) * (ge_second_rp_append_matching_oldunit_witnesstransport))) + (((ge_first_rn_append_matching_oldunit_witnesstransport) * (ge_second_rn_append_matching_oldunit_witnesstransport))))) + (((((ge_first_ip_append_matching_oldunit_witnesstransport) * (ge_second_in_append_matching_oldunit_witnesstransport))) + (((ge_first_in_append_matching_oldunit_witnesstransport) * (ge_second_ip_append_matching_oldunit_witnesstransport))))))) + ge_balance_negative_append_matching_oldunit_witnesstransportoutputreal = (((((((ge_first_rp_append_matching_oldunit_witnesstransport) * (ge_second_rn_append_matching_oldunit_witnesstransport))) + (((ge_first_rn_append_matching_oldunit_witnesstransport) * (ge_second_rp_append_matching_oldunit_witnesstransport))))) + (((((ge_first_ip_append_matching_oldunit_witnesstransport) * (ge_second_ip_append_matching_oldunit_witnesstransport))) + (((ge_first_in_append_matching_oldunit_witnesstransport) * (ge_second_in_append_matching_oldunit_witnesstransport))))))) + ge_balance_positive_append_matching_oldunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_append_matching_oldunit_witnesstransportoutputimaginary ge_balance_negative_append_matching_oldunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput) = 2 * (ge_balance_positive_append_matching_oldunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_oldunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_oldunit_witnesstransportoutput) = 2 * ge_signed_half_append_matching_oldunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_oldunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_oldunit_witnesstransportoutputimaginary) = S ge_signed_half_append_matching_oldunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_oldunit_witnesstransport) * (ge_second_ip_append_matching_oldunit_witnesstransport))) + (((ge_first_rn_append_matching_oldunit_witnesstransport) * (ge_second_in_append_matching_oldunit_witnesstransport))))) + (((((ge_first_ip_append_matching_oldunit_witnesstransport) * (ge_second_rp_append_matching_oldunit_witnesstransport))) + (((ge_first_in_append_matching_oldunit_witnesstransport) * (ge_second_rn_append_matching_oldunit_witnesstransport))))))) + ge_balance_negative_append_matching_oldunit_witnesstransportoutputimaginary = (((((((ge_first_rp_append_matching_oldunit_witnesstransport) * (ge_second_in_append_matching_oldunit_witnesstransport))) + (((ge_first_rn_append_matching_oldunit_witnesstransport) * (ge_second_ip_append_matching_oldunit_witnesstransport))))) + (((((ge_first_ip_append_matching_oldunit_witnesstransport) * (ge_second_rn_append_matching_oldunit_witnesstransport))) + (((ge_first_in_append_matching_oldunit_witnesstransport) * (ge_second_rp_append_matching_oldunit_witnesstransport))))))) + ge_balance_positive_append_matching_oldunit_witnesstransportoutputimaginary)))))))))))) -> (((((exists ff_h_pfp_append_matching_extensionlast. ff_h_pfp_append_matching_extensionlast + S (l) = S ((S (l)) * V)) /\ exists ff_q_pfp_append_matching_extensionlast. U = ff_q_pfp_append_matching_extensionlast * S ((S (l)) * V) + (l))) /\ (forall pfp_i_append_matching_extensionprefix pfp_a_append_matching_extensionprefix. (exists pfp_gap_append_matching_extensionprefixbound. pfp_gap_append_matching_extensionprefixbound + S (pfp_i_append_matching_extensionprefix) = (l)) -> (((exists ff_h_pfp_append_matching_extensionprefixold. ff_h_pfp_append_matching_extensionprefixold + S (pfp_a_append_matching_extensionprefix) = S ((S (pfp_i_append_matching_extensionprefix)) * v)) /\ exists ff_q_pfp_append_matching_extensionprefixold. u = ff_q_pfp_append_matching_extensionprefixold * S ((S (pfp_i_append_matching_extensionprefix)) * v) + (pfp_a_append_matching_extensionprefix))) -> (((exists ff_h_pfp_append_matching_extensionprefixnew. ff_h_pfp_append_matching_extensionprefixnew + S (pfp_a_append_matching_extensionprefix) = S ((S (pfp_i_append_matching_extensionprefix)) * V)) /\ exists ff_q_pfp_append_matching_extensionprefixnew. U = ff_q_pfp_append_matching_extensionprefixnew * S ((S (pfp_i_append_matching_extensionprefix)) * V) + (pfp_a_append_matching_extensionprefix)))))) -> (((exists ff_h_gprod_append_matching_source_last. ff_h_gprod_append_matching_source_last + S (p) = S ((S (l)) * c)) /\ exists ff_q_gprod_append_matching_source_last. b = ff_q_gprod_append_matching_source_last * S ((S (l)) * c) + (p))) -> (((exists ff_h_gprod_append_matching_target_last. ff_h_gprod_append_matching_target_last + S (q) = S ((S (l)) * e)) /\ exists ff_q_gprod_append_matching_target_last. d = ff_q_gprod_append_matching_target_last * S ((S (l)) * e) + (q))) -> (exists gr_unit_append_matching_last_unit. ((exists gr_inverse_append_matching_last_unitunit. (exists ge_first_rp_append_matching_last_unitunitidentity ge_first_rn_append_matching_last_unitunitidentity ge_first_ip_append_matching_last_unitunitidentity ge_first_in_append_matching_last_unitunitidentity ge_second_rp_append_matching_last_unitunitidentity ge_second_rn_append_matching_last_unitunitidentity ge_second_ip_append_matching_last_unitunitidentity ge_second_in_append_matching_last_unitunitidentity. ((exists ge_representation_real_code_append_matching_last_unitunitidentityfirst ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst. (((gr_unit_append_matching_last_unit) = ((ge_representation_real_code_append_matching_last_unitunitidentityfirst) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst)) * S ((ge_representation_real_code_append_matching_last_unitunitidentityfirst) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst)) + ((ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst))) /\ ((exists ge_balance_positive_append_matching_last_unitunitidentityfirstreal ge_balance_negative_append_matching_last_unitunitidentityfirstreal. (((((ge_representation_real_code_append_matching_last_unitunitidentityfirst) = 2 * (ge_balance_positive_append_matching_last_unitunitidentityfirstreal) /\ (ge_balance_negative_append_matching_last_unitunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentityfirstrealdecode. (((ge_representation_real_code_append_matching_last_unitunitidentityfirst) = 2 * ge_signed_half_append_matching_last_unitunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentityfirstreal) = S ge_signed_half_append_matching_last_unitunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_matching_last_unitunitidentity) + ge_balance_negative_append_matching_last_unitunitidentityfirstreal = (ge_first_rn_append_matching_last_unitunitidentity) + ge_balance_positive_append_matching_last_unitunitidentityfirstreal))) /\ (exists ge_balance_positive_append_matching_last_unitunitidentityfirstimaginary ge_balance_negative_append_matching_last_unitunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst) = 2 * (ge_balance_positive_append_matching_last_unitunitidentityfirstimaginary) /\ (ge_balance_negative_append_matching_last_unitunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unitunitidentityfirst) = 2 * ge_signed_half_append_matching_last_unitunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentityfirstimaginary) = S ge_signed_half_append_matching_last_unitunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_last_unitunitidentity) + ge_balance_negative_append_matching_last_unitunitidentityfirstimaginary = (ge_first_in_append_matching_last_unitunitidentity) + ge_balance_positive_append_matching_last_unitunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_last_unitunitidentitysecond ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond. (((gr_inverse_append_matching_last_unitunit) = ((ge_representation_real_code_append_matching_last_unitunitidentitysecond) + (ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond)) * S ((ge_representation_real_code_append_matching_last_unitunitidentitysecond) + (ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond)) + ((ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond) + (ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond))) /\ ((exists ge_balance_positive_append_matching_last_unitunitidentitysecondreal ge_balance_negative_append_matching_last_unitunitidentitysecondreal. (((((ge_representation_real_code_append_matching_last_unitunitidentitysecond) = 2 * (ge_balance_positive_append_matching_last_unitunitidentitysecondreal) /\ (ge_balance_negative_append_matching_last_unitunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentitysecondrealdecode. (((ge_representation_real_code_append_matching_last_unitunitidentitysecond) = 2 * ge_signed_half_append_matching_last_unitunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentitysecondreal) = S ge_signed_half_append_matching_last_unitunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_matching_last_unitunitidentity) + ge_balance_negative_append_matching_last_unitunitidentitysecondreal = (ge_second_rn_append_matching_last_unitunitidentity) + ge_balance_positive_append_matching_last_unitunitidentitysecondreal))) /\ (exists ge_balance_positive_append_matching_last_unitunitidentitysecondimaginary ge_balance_negative_append_matching_last_unitunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond) = 2 * (ge_balance_positive_append_matching_last_unitunitidentitysecondimaginary) /\ (ge_balance_negative_append_matching_last_unitunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unitunitidentitysecond) = 2 * ge_signed_half_append_matching_last_unitunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentitysecondimaginary) = S ge_signed_half_append_matching_last_unitunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_matching_last_unitunitidentity) + ge_balance_negative_append_matching_last_unitunitidentitysecondimaginary = (ge_second_in_append_matching_last_unitunitidentity) + ge_balance_positive_append_matching_last_unitunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_last_unitunitidentityoutput ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput. (((6) = ((ge_representation_real_code_append_matching_last_unitunitidentityoutput) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput)) * S ((ge_representation_real_code_append_matching_last_unitunitidentityoutput) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput)) + ((ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput) + (ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput))) /\ ((exists ge_balance_positive_append_matching_last_unitunitidentityoutputreal ge_balance_negative_append_matching_last_unitunitidentityoutputreal. (((((ge_representation_real_code_append_matching_last_unitunitidentityoutput) = 2 * (ge_balance_positive_append_matching_last_unitunitidentityoutputreal) /\ (ge_balance_negative_append_matching_last_unitunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentityoutputrealdecode. (((ge_representation_real_code_append_matching_last_unitunitidentityoutput) = 2 * ge_signed_half_append_matching_last_unitunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentityoutputreal) = S ge_signed_half_append_matching_last_unitunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_last_unitunitidentity) * (ge_second_rp_append_matching_last_unitunitidentity))) + (((ge_first_rn_append_matching_last_unitunitidentity) * (ge_second_rn_append_matching_last_unitunitidentity))))) + (((((ge_first_ip_append_matching_last_unitunitidentity) * (ge_second_in_append_matching_last_unitunitidentity))) + (((ge_first_in_append_matching_last_unitunitidentity) * (ge_second_ip_append_matching_last_unitunitidentity))))))) + ge_balance_negative_append_matching_last_unitunitidentityoutputreal = (((((((ge_first_rp_append_matching_last_unitunitidentity) * (ge_second_rn_append_matching_last_unitunitidentity))) + (((ge_first_rn_append_matching_last_unitunitidentity) * (ge_second_rp_append_matching_last_unitunitidentity))))) + (((((ge_first_ip_append_matching_last_unitunitidentity) * (ge_second_ip_append_matching_last_unitunitidentity))) + (((ge_first_in_append_matching_last_unitunitidentity) * (ge_second_in_append_matching_last_unitunitidentity))))))) + ge_balance_positive_append_matching_last_unitunitidentityoutputreal))) /\ (exists ge_balance_positive_append_matching_last_unitunitidentityoutputimaginary ge_balance_negative_append_matching_last_unitunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput) = 2 * (ge_balance_positive_append_matching_last_unitunitidentityoutputimaginary) /\ (ge_balance_negative_append_matching_last_unitunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unitunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unitunitidentityoutput) = 2 * ge_signed_half_append_matching_last_unitunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unitunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unitunitidentityoutputimaginary) = S ge_signed_half_append_matching_last_unitunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_last_unitunitidentity) * (ge_second_ip_append_matching_last_unitunitidentity))) + (((ge_first_rn_append_matching_last_unitunitidentity) * (ge_second_in_append_matching_last_unitunitidentity))))) + (((((ge_first_ip_append_matching_last_unitunitidentity) * (ge_second_rp_append_matching_last_unitunitidentity))) + (((ge_first_in_append_matching_last_unitunitidentity) * (ge_second_rn_append_matching_last_unitunitidentity))))))) + ge_balance_negative_append_matching_last_unitunitidentityoutputimaginary = (((((((ge_first_rp_append_matching_last_unitunitidentity) * (ge_second_in_append_matching_last_unitunitidentity))) + (((ge_first_rn_append_matching_last_unitunitidentity) * (ge_second_ip_append_matching_last_unitunitidentity))))) + (((((ge_first_ip_append_matching_last_unitunitidentity) * (ge_second_rn_append_matching_last_unitunitidentity))) + (((ge_first_in_append_matching_last_unitunitidentity) * (ge_second_rp_append_matching_last_unitunitidentity))))))) + ge_balance_positive_append_matching_last_unitunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_append_matching_last_unittransport ge_first_rn_append_matching_last_unittransport ge_first_ip_append_matching_last_unittransport ge_first_in_append_matching_last_unittransport ge_second_rp_append_matching_last_unittransport ge_second_rn_append_matching_last_unittransport ge_second_ip_append_matching_last_unittransport ge_second_in_append_matching_last_unittransport. ((exists ge_representation_real_code_append_matching_last_unittransportfirst ge_representation_imaginary_code_append_matching_last_unittransportfirst. (((gr_unit_append_matching_last_unit) = ((ge_representation_real_code_append_matching_last_unittransportfirst) + (ge_representation_imaginary_code_append_matching_last_unittransportfirst)) * S ((ge_representation_real_code_append_matching_last_unittransportfirst) + (ge_representation_imaginary_code_append_matching_last_unittransportfirst)) + ((ge_representation_imaginary_code_append_matching_last_unittransportfirst) + (ge_representation_imaginary_code_append_matching_last_unittransportfirst))) /\ ((exists ge_balance_positive_append_matching_last_unittransportfirstreal ge_balance_negative_append_matching_last_unittransportfirstreal. (((((ge_representation_real_code_append_matching_last_unittransportfirst) = 2 * (ge_balance_positive_append_matching_last_unittransportfirstreal) /\ (ge_balance_negative_append_matching_last_unittransportfirstreal) = 0) \/ exists ge_signed_half_append_matching_last_unittransportfirstrealdecode. (((ge_representation_real_code_append_matching_last_unittransportfirst) = 2 * ge_signed_half_append_matching_last_unittransportfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportfirstreal) = 0) /\ (ge_balance_negative_append_matching_last_unittransportfirstreal) = S ge_signed_half_append_matching_last_unittransportfirstrealdecode))) /\ ((ge_first_rp_append_matching_last_unittransport) + ge_balance_negative_append_matching_last_unittransportfirstreal = (ge_first_rn_append_matching_last_unittransport) + ge_balance_positive_append_matching_last_unittransportfirstreal))) /\ (exists ge_balance_positive_append_matching_last_unittransportfirstimaginary ge_balance_negative_append_matching_last_unittransportfirstimaginary. (((((ge_representation_imaginary_code_append_matching_last_unittransportfirst) = 2 * (ge_balance_positive_append_matching_last_unittransportfirstimaginary) /\ (ge_balance_negative_append_matching_last_unittransportfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unittransportfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unittransportfirst) = 2 * ge_signed_half_append_matching_last_unittransportfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unittransportfirstimaginary) = S ge_signed_half_append_matching_last_unittransportfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_last_unittransport) + ge_balance_negative_append_matching_last_unittransportfirstimaginary = (ge_first_in_append_matching_last_unittransport) + ge_balance_positive_append_matching_last_unittransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_last_unittransportsecond ge_representation_imaginary_code_append_matching_last_unittransportsecond. (((p) = ((ge_representation_real_code_append_matching_last_unittransportsecond) + (ge_representation_imaginary_code_append_matching_last_unittransportsecond)) * S ((ge_representation_real_code_append_matching_last_unittransportsecond) + (ge_representation_imaginary_code_append_matching_last_unittransportsecond)) + ((ge_representation_imaginary_code_append_matching_last_unittransportsecond) + (ge_representation_imaginary_code_append_matching_last_unittransportsecond))) /\ ((exists ge_balance_positive_append_matching_last_unittransportsecondreal ge_balance_negative_append_matching_last_unittransportsecondreal. (((((ge_representation_real_code_append_matching_last_unittransportsecond) = 2 * (ge_balance_positive_append_matching_last_unittransportsecondreal) /\ (ge_balance_negative_append_matching_last_unittransportsecondreal) = 0) \/ exists ge_signed_half_append_matching_last_unittransportsecondrealdecode. (((ge_representation_real_code_append_matching_last_unittransportsecond) = 2 * ge_signed_half_append_matching_last_unittransportsecondrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportsecondreal) = 0) /\ (ge_balance_negative_append_matching_last_unittransportsecondreal) = S ge_signed_half_append_matching_last_unittransportsecondrealdecode))) /\ ((ge_second_rp_append_matching_last_unittransport) + ge_balance_negative_append_matching_last_unittransportsecondreal = (ge_second_rn_append_matching_last_unittransport) + ge_balance_positive_append_matching_last_unittransportsecondreal))) /\ (exists ge_balance_positive_append_matching_last_unittransportsecondimaginary ge_balance_negative_append_matching_last_unittransportsecondimaginary. (((((ge_representation_imaginary_code_append_matching_last_unittransportsecond) = 2 * (ge_balance_positive_append_matching_last_unittransportsecondimaginary) /\ (ge_balance_negative_append_matching_last_unittransportsecondimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unittransportsecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unittransportsecond) = 2 * ge_signed_half_append_matching_last_unittransportsecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportsecondimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unittransportsecondimaginary) = S ge_signed_half_append_matching_last_unittransportsecondimaginarydecode))) /\ ((ge_second_ip_append_matching_last_unittransport) + ge_balance_negative_append_matching_last_unittransportsecondimaginary = (ge_second_in_append_matching_last_unittransport) + ge_balance_positive_append_matching_last_unittransportsecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_last_unittransportoutput ge_representation_imaginary_code_append_matching_last_unittransportoutput. (((q) = ((ge_representation_real_code_append_matching_last_unittransportoutput) + (ge_representation_imaginary_code_append_matching_last_unittransportoutput)) * S ((ge_representation_real_code_append_matching_last_unittransportoutput) + (ge_representation_imaginary_code_append_matching_last_unittransportoutput)) + ((ge_representation_imaginary_code_append_matching_last_unittransportoutput) + (ge_representation_imaginary_code_append_matching_last_unittransportoutput))) /\ ((exists ge_balance_positive_append_matching_last_unittransportoutputreal ge_balance_negative_append_matching_last_unittransportoutputreal. (((((ge_representation_real_code_append_matching_last_unittransportoutput) = 2 * (ge_balance_positive_append_matching_last_unittransportoutputreal) /\ (ge_balance_negative_append_matching_last_unittransportoutputreal) = 0) \/ exists ge_signed_half_append_matching_last_unittransportoutputrealdecode. (((ge_representation_real_code_append_matching_last_unittransportoutput) = 2 * ge_signed_half_append_matching_last_unittransportoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportoutputreal) = 0) /\ (ge_balance_negative_append_matching_last_unittransportoutputreal) = S ge_signed_half_append_matching_last_unittransportoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_last_unittransport) * (ge_second_rp_append_matching_last_unittransport))) + (((ge_first_rn_append_matching_last_unittransport) * (ge_second_rn_append_matching_last_unittransport))))) + (((((ge_first_ip_append_matching_last_unittransport) * (ge_second_in_append_matching_last_unittransport))) + (((ge_first_in_append_matching_last_unittransport) * (ge_second_ip_append_matching_last_unittransport))))))) + ge_balance_negative_append_matching_last_unittransportoutputreal = (((((((ge_first_rp_append_matching_last_unittransport) * (ge_second_rn_append_matching_last_unittransport))) + (((ge_first_rn_append_matching_last_unittransport) * (ge_second_rp_append_matching_last_unittransport))))) + (((((ge_first_ip_append_matching_last_unittransport) * (ge_second_ip_append_matching_last_unittransport))) + (((ge_first_in_append_matching_last_unittransport) * (ge_second_in_append_matching_last_unittransport))))))) + ge_balance_positive_append_matching_last_unittransportoutputreal))) /\ (exists ge_balance_positive_append_matching_last_unittransportoutputimaginary ge_balance_negative_append_matching_last_unittransportoutputimaginary. (((((ge_representation_imaginary_code_append_matching_last_unittransportoutput) = 2 * (ge_balance_positive_append_matching_last_unittransportoutputimaginary) /\ (ge_balance_negative_append_matching_last_unittransportoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_last_unittransportoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_last_unittransportoutput) = 2 * ge_signed_half_append_matching_last_unittransportoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_last_unittransportoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_last_unittransportoutputimaginary) = S ge_signed_half_append_matching_last_unittransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_last_unittransport) * (ge_second_ip_append_matching_last_unittransport))) + (((ge_first_rn_append_matching_last_unittransport) * (ge_second_in_append_matching_last_unittransport))))) + (((((ge_first_ip_append_matching_last_unittransport) * (ge_second_rp_append_matching_last_unittransport))) + (((ge_first_in_append_matching_last_unittransport) * (ge_second_rn_append_matching_last_unittransport))))))) + ge_balance_negative_append_matching_last_unittransportoutputimaginary = (((((((ge_first_rp_append_matching_last_unittransport) * (ge_second_in_append_matching_last_unittransport))) + (((ge_first_rn_append_matching_last_unittransport) * (ge_second_ip_append_matching_last_unittransport))))) + (((((ge_first_ip_append_matching_last_unittransport) * (ge_second_rn_append_matching_last_unittransport))) + (((ge_first_in_append_matching_last_unittransport) * (ge_second_rp_append_matching_last_unittransport))))))) + ge_balance_positive_append_matching_last_unittransportoutputimaginary))))))))))) -> (forall gr_match_index_append_matching_new gr_match_image_append_matching_new gr_match_source_append_matching_new gr_match_target_append_matching_new. (exists ge_gap_append_matching_newindex. ge_gap_append_matching_newindex + S (gr_match_index_append_matching_new) = (S l)) -> (((exists ff_h_gprod_append_matching_newmap. ff_h_gprod_append_matching_newmap + S (gr_match_image_append_matching_new) = S ((S (gr_match_index_append_matching_new)) * V)) /\ exists ff_q_gprod_append_matching_newmap. U = ff_q_gprod_append_matching_newmap * S ((S (gr_match_index_append_matching_new)) * V) + (gr_match_image_append_matching_new))) -> (((exists ff_h_gprod_append_matching_newsource. ff_h_gprod_append_matching_newsource + S (gr_match_source_append_matching_new) = S ((S (gr_match_index_append_matching_new)) * c)) /\ exists ff_q_gprod_append_matching_newsource. b = ff_q_gprod_append_matching_newsource * S ((S (gr_match_index_append_matching_new)) * c) + (gr_match_source_append_matching_new))) -> (((exists ff_h_gprod_append_matching_newtarget. ff_h_gprod_append_matching_newtarget + S (gr_match_target_append_matching_new) = S ((S (gr_match_image_append_matching_new)) * e)) /\ exists ff_q_gprod_append_matching_newtarget. d = ff_q_gprod_append_matching_newtarget * S ((S (gr_match_image_append_matching_new)) * e) + (gr_match_target_append_matching_new))) -> (exists gr_unit_append_matching_newunit_witness. ((exists gr_inverse_append_matching_newunit_witnessunit. (exists ge_first_rp_append_matching_newunit_witnessunitidentity ge_first_rn_append_matching_newunit_witnessunitidentity ge_first_ip_append_matching_newunit_witnessunitidentity ge_first_in_append_matching_newunit_witnessunitidentity ge_second_rp_append_matching_newunit_witnessunitidentity ge_second_rn_append_matching_newunit_witnessunitidentity ge_second_ip_append_matching_newunit_witnessunitidentity ge_second_in_append_matching_newunit_witnessunitidentity. ((exists ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst. (((gr_unit_append_matching_newunit_witness) = ((ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst)) * S ((ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst)) + ((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst))) /\ ((exists ge_balance_positive_append_matching_newunit_witnessunitidentityfirstreal ge_balance_negative_append_matching_newunit_witnessunitidentityfirstreal. (((((ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentityfirstreal) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityfirstreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentityfirstrealdecode. (((ge_representation_real_code_append_matching_newunit_witnessunitidentityfirst) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentityfirstreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityfirstreal) = S ge_signed_half_append_matching_newunit_witnessunitidentityfirstrealdecode))) /\ ((ge_first_rp_append_matching_newunit_witnessunitidentity) + ge_balance_negative_append_matching_newunit_witnessunitidentityfirstreal = (ge_first_rn_append_matching_newunit_witnessunitidentity) + ge_balance_positive_append_matching_newunit_witnessunitidentityfirstreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnessunitidentityfirstimaginary ge_balance_negative_append_matching_newunit_witnessunitidentityfirstimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentityfirstimaginary) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityfirst) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityfirstimaginary) = S ge_signed_half_append_matching_newunit_witnessunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_newunit_witnessunitidentity) + ge_balance_negative_append_matching_newunit_witnessunitidentityfirstimaginary = (ge_first_in_append_matching_newunit_witnessunitidentity) + ge_balance_positive_append_matching_newunit_witnessunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond. (((gr_inverse_append_matching_newunit_witnessunit) = ((ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond)) * S ((ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond)) + ((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond))) /\ ((exists ge_balance_positive_append_matching_newunit_witnessunitidentitysecondreal ge_balance_negative_append_matching_newunit_witnessunitidentitysecondreal. (((((ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentitysecondreal) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentitysecondreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentitysecondrealdecode. (((ge_representation_real_code_append_matching_newunit_witnessunitidentitysecond) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentitysecondreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentitysecondreal) = S ge_signed_half_append_matching_newunit_witnessunitidentitysecondrealdecode))) /\ ((ge_second_rp_append_matching_newunit_witnessunitidentity) + ge_balance_negative_append_matching_newunit_witnessunitidentitysecondreal = (ge_second_rn_append_matching_newunit_witnessunitidentity) + ge_balance_positive_append_matching_newunit_witnessunitidentitysecondreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnessunitidentitysecondimaginary ge_balance_negative_append_matching_newunit_witnessunitidentitysecondimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentitysecondimaginary) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentitysecond) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentitysecondimaginary) = S ge_signed_half_append_matching_newunit_witnessunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_append_matching_newunit_witnessunitidentity) + ge_balance_negative_append_matching_newunit_witnessunitidentitysecondimaginary = (ge_second_in_append_matching_newunit_witnessunitidentity) + ge_balance_positive_append_matching_newunit_witnessunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput. (((6) = ((ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput)) * S ((ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput)) + ((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput))) /\ ((exists ge_balance_positive_append_matching_newunit_witnessunitidentityoutputreal ge_balance_negative_append_matching_newunit_witnessunitidentityoutputreal. (((((ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentityoutputreal) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityoutputreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentityoutputrealdecode. (((ge_representation_real_code_append_matching_newunit_witnessunitidentityoutput) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentityoutputreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityoutputreal) = S ge_signed_half_append_matching_newunit_witnessunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_newunit_witnessunitidentity) * (ge_second_rp_append_matching_newunit_witnessunitidentity))) + (((ge_first_rn_append_matching_newunit_witnessunitidentity) * (ge_second_rn_append_matching_newunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_newunit_witnessunitidentity) * (ge_second_in_append_matching_newunit_witnessunitidentity))) + (((ge_first_in_append_matching_newunit_witnessunitidentity) * (ge_second_ip_append_matching_newunit_witnessunitidentity))))))) + ge_balance_negative_append_matching_newunit_witnessunitidentityoutputreal = (((((((ge_first_rp_append_matching_newunit_witnessunitidentity) * (ge_second_rn_append_matching_newunit_witnessunitidentity))) + (((ge_first_rn_append_matching_newunit_witnessunitidentity) * (ge_second_rp_append_matching_newunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_newunit_witnessunitidentity) * (ge_second_ip_append_matching_newunit_witnessunitidentity))) + (((ge_first_in_append_matching_newunit_witnessunitidentity) * (ge_second_in_append_matching_newunit_witnessunitidentity))))))) + ge_balance_positive_append_matching_newunit_witnessunitidentityoutputreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnessunitidentityoutputimaginary ge_balance_negative_append_matching_newunit_witnessunitidentityoutputimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput) = 2 * (ge_balance_positive_append_matching_newunit_witnessunitidentityoutputimaginary) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnessunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnessunitidentityoutput) = 2 * ge_signed_half_append_matching_newunit_witnessunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnessunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnessunitidentityoutputimaginary) = S ge_signed_half_append_matching_newunit_witnessunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_newunit_witnessunitidentity) * (ge_second_ip_append_matching_newunit_witnessunitidentity))) + (((ge_first_rn_append_matching_newunit_witnessunitidentity) * (ge_second_in_append_matching_newunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_newunit_witnessunitidentity) * (ge_second_rp_append_matching_newunit_witnessunitidentity))) + (((ge_first_in_append_matching_newunit_witnessunitidentity) * (ge_second_rn_append_matching_newunit_witnessunitidentity))))))) + ge_balance_negative_append_matching_newunit_witnessunitidentityoutputimaginary = (((((((ge_first_rp_append_matching_newunit_witnessunitidentity) * (ge_second_in_append_matching_newunit_witnessunitidentity))) + (((ge_first_rn_append_matching_newunit_witnessunitidentity) * (ge_second_ip_append_matching_newunit_witnessunitidentity))))) + (((((ge_first_ip_append_matching_newunit_witnessunitidentity) * (ge_second_rn_append_matching_newunit_witnessunitidentity))) + (((ge_first_in_append_matching_newunit_witnessunitidentity) * (ge_second_rp_append_matching_newunit_witnessunitidentity))))))) + ge_balance_positive_append_matching_newunit_witnessunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_append_matching_newunit_witnesstransport ge_first_rn_append_matching_newunit_witnesstransport ge_first_ip_append_matching_newunit_witnesstransport ge_first_in_append_matching_newunit_witnesstransport ge_second_rp_append_matching_newunit_witnesstransport ge_second_rn_append_matching_newunit_witnesstransport ge_second_ip_append_matching_newunit_witnesstransport ge_second_in_append_matching_newunit_witnesstransport. ((exists ge_representation_real_code_append_matching_newunit_witnesstransportfirst ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst. (((gr_unit_append_matching_newunit_witness) = ((ge_representation_real_code_append_matching_newunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst)) * S ((ge_representation_real_code_append_matching_newunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst)) + ((ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst))) /\ ((exists ge_balance_positive_append_matching_newunit_witnesstransportfirstreal ge_balance_negative_append_matching_newunit_witnesstransportfirstreal. (((((ge_representation_real_code_append_matching_newunit_witnesstransportfirst) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportfirstreal) /\ (ge_balance_negative_append_matching_newunit_witnesstransportfirstreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportfirstrealdecode. (((ge_representation_real_code_append_matching_newunit_witnesstransportfirst) = 2 * ge_signed_half_append_matching_newunit_witnesstransportfirstrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportfirstreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportfirstreal) = S ge_signed_half_append_matching_newunit_witnesstransportfirstrealdecode))) /\ ((ge_first_rp_append_matching_newunit_witnesstransport) + ge_balance_negative_append_matching_newunit_witnesstransportfirstreal = (ge_first_rn_append_matching_newunit_witnesstransport) + ge_balance_positive_append_matching_newunit_witnesstransportfirstreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnesstransportfirstimaginary ge_balance_negative_append_matching_newunit_witnesstransportfirstimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportfirstimaginary) /\ (ge_balance_negative_append_matching_newunit_witnesstransportfirstimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportfirstimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnesstransportfirst) = 2 * ge_signed_half_append_matching_newunit_witnesstransportfirstimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportfirstimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportfirstimaginary) = S ge_signed_half_append_matching_newunit_witnesstransportfirstimaginarydecode))) /\ ((ge_first_ip_append_matching_newunit_witnesstransport) + ge_balance_negative_append_matching_newunit_witnesstransportfirstimaginary = (ge_first_in_append_matching_newunit_witnesstransport) + ge_balance_positive_append_matching_newunit_witnesstransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_append_matching_newunit_witnesstransportsecond ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond. (((gr_match_source_append_matching_new) = ((ge_representation_real_code_append_matching_newunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond)) * S ((ge_representation_real_code_append_matching_newunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond)) + ((ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond))) /\ ((exists ge_balance_positive_append_matching_newunit_witnesstransportsecondreal ge_balance_negative_append_matching_newunit_witnesstransportsecondreal. (((((ge_representation_real_code_append_matching_newunit_witnesstransportsecond) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportsecondreal) /\ (ge_balance_negative_append_matching_newunit_witnesstransportsecondreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportsecondrealdecode. (((ge_representation_real_code_append_matching_newunit_witnesstransportsecond) = 2 * ge_signed_half_append_matching_newunit_witnesstransportsecondrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportsecondreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportsecondreal) = S ge_signed_half_append_matching_newunit_witnesstransportsecondrealdecode))) /\ ((ge_second_rp_append_matching_newunit_witnesstransport) + ge_balance_negative_append_matching_newunit_witnesstransportsecondreal = (ge_second_rn_append_matching_newunit_witnesstransport) + ge_balance_positive_append_matching_newunit_witnesstransportsecondreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnesstransportsecondimaginary ge_balance_negative_append_matching_newunit_witnesstransportsecondimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportsecondimaginary) /\ (ge_balance_negative_append_matching_newunit_witnesstransportsecondimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportsecondimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnesstransportsecond) = 2 * ge_signed_half_append_matching_newunit_witnesstransportsecondimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportsecondimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportsecondimaginary) = S ge_signed_half_append_matching_newunit_witnesstransportsecondimaginarydecode))) /\ ((ge_second_ip_append_matching_newunit_witnesstransport) + ge_balance_negative_append_matching_newunit_witnesstransportsecondimaginary = (ge_second_in_append_matching_newunit_witnesstransport) + ge_balance_positive_append_matching_newunit_witnesstransportsecondimaginary)))))) /\ (exists ge_representation_real_code_append_matching_newunit_witnesstransportoutput ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput. (((gr_match_target_append_matching_new) = ((ge_representation_real_code_append_matching_newunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput)) * S ((ge_representation_real_code_append_matching_newunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput)) + ((ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput) + (ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput))) /\ ((exists ge_balance_positive_append_matching_newunit_witnesstransportoutputreal ge_balance_negative_append_matching_newunit_witnesstransportoutputreal. (((((ge_representation_real_code_append_matching_newunit_witnesstransportoutput) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportoutputreal) /\ (ge_balance_negative_append_matching_newunit_witnesstransportoutputreal) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportoutputrealdecode. (((ge_representation_real_code_append_matching_newunit_witnesstransportoutput) = 2 * ge_signed_half_append_matching_newunit_witnesstransportoutputrealdecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportoutputreal) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportoutputreal) = S ge_signed_half_append_matching_newunit_witnesstransportoutputrealdecode))) /\ ((((((((ge_first_rp_append_matching_newunit_witnesstransport) * (ge_second_rp_append_matching_newunit_witnesstransport))) + (((ge_first_rn_append_matching_newunit_witnesstransport) * (ge_second_rn_append_matching_newunit_witnesstransport))))) + (((((ge_first_ip_append_matching_newunit_witnesstransport) * (ge_second_in_append_matching_newunit_witnesstransport))) + (((ge_first_in_append_matching_newunit_witnesstransport) * (ge_second_ip_append_matching_newunit_witnesstransport))))))) + ge_balance_negative_append_matching_newunit_witnesstransportoutputreal = (((((((ge_first_rp_append_matching_newunit_witnesstransport) * (ge_second_rn_append_matching_newunit_witnesstransport))) + (((ge_first_rn_append_matching_newunit_witnesstransport) * (ge_second_rp_append_matching_newunit_witnesstransport))))) + (((((ge_first_ip_append_matching_newunit_witnesstransport) * (ge_second_ip_append_matching_newunit_witnesstransport))) + (((ge_first_in_append_matching_newunit_witnesstransport) * (ge_second_in_append_matching_newunit_witnesstransport))))))) + ge_balance_positive_append_matching_newunit_witnesstransportoutputreal))) /\ (exists ge_balance_positive_append_matching_newunit_witnesstransportoutputimaginary ge_balance_negative_append_matching_newunit_witnesstransportoutputimaginary. (((((ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput) = 2 * (ge_balance_positive_append_matching_newunit_witnesstransportoutputimaginary) /\ (ge_balance_negative_append_matching_newunit_witnesstransportoutputimaginary) = 0) \/ exists ge_signed_half_append_matching_newunit_witnesstransportoutputimaginarydecode. (((ge_representation_imaginary_code_append_matching_newunit_witnesstransportoutput) = 2 * ge_signed_half_append_matching_newunit_witnesstransportoutputimaginarydecode + 1 /\ (ge_balance_positive_append_matching_newunit_witnesstransportoutputimaginary) = 0) /\ (ge_balance_negative_append_matching_newunit_witnesstransportoutputimaginary) = S ge_signed_half_append_matching_newunit_witnesstransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_append_matching_newunit_witnesstransport) * (ge_second_ip_append_matching_newunit_witnesstransport))) + (((ge_first_rn_append_matching_newunit_witnesstransport) * (ge_second_in_append_matching_newunit_witnesstransport))))) + (((((ge_first_ip_append_matching_newunit_witnesstransport) * (ge_second_rp_append_matching_newunit_witnesstransport))) + (((ge_first_in_append_matching_newunit_witnesstransport) * (ge_second_rn_append_matching_newunit_witnesstransport))))))) + ge_balance_negative_append_matching_newunit_witnesstransportoutputimaginary = (((((((ge_first_rp_append_matching_newunit_witnesstransport) * (ge_second_in_append_matching_newunit_witnesstransport))) + (((ge_first_rn_append_matching_newunit_witnesstransport) * (ge_second_ip_append_matching_newunit_witnesstransport))))) + (((((ge_first_ip_append_matching_newunit_witnesstransport) * (ge_second_rn_append_matching_newunit_witnesstransport))) + (((ge_first_in_append_matching_newunit_witnesstransport) * (ge_second_rp_append_matching_newunit_witnesstransport))))))) + ge_balance_positive_append_matching_newunit_witnesstransportoutputimaginary))))))))))))

Complete tactic proof in conservative notation

All 106 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

106 script commands · 15 reading checkpoints · 4 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 (2)

gaussian product beta index transport gaussian factor associate code transport

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

L1
intro b
L2
intro c
L3
intro d
L4
intro e
L5
intro u
L6
intro v
L7
intro U
L8
intro V
L9
intro l
L10
intro p

02Fix variables and assumptionsL11–16

Work with arbitrary variables or the premises of the current implication.

L11
intro q
L12
intro hm
L13
intro hext
L14
intro hp
L15
intro hq
L16
intro hpq

03Separate the logical casesL17–17

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L17
cases hext

04Fix variables and assumptionsL18–25

Work with arbitrary variables or the premises of the current implication.

L18
intro i
L19
intro j
L20
intro a
L21
intro t
L22
intro hi
L23
intro hmap
L24
intro hsource
L25
intro htarget

05Establish hcL26–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

L26
have hc : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
L27
specialize finite_lt_succ_eq_or_lt (l)
L28
specialize finite_lt_succ_eq_or_lt (i)
L29
apply finite_lt_succ_eq_or_lt
L30
exact hi

06Separate the logical casesL31–31

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L31
cases hc

07Establish hjL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

L32
have hj : j=l
L33
specialize beta_at_unique (U)
L34
specialize beta_at_unique (V)
L35
specialize beta_at_unique (l)
L36
specialize beta_at_unique (j)
L37
specialize beta_at_unique (l)
L38
apply beta_at_unique
L39
specialize gaussian_product_beta_index_transport (U)
L40
specialize gaussian_product_beta_index_transport (V)
L41
specialize gaussian_product_beta_index_transport (i)

08Use earlier factsL42–47