AF0011

factor_permutation_matched_append_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Existence-only append interface still returns an actual fully bijective matching beta map.

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.

Exact expanded first-order arithmetic statement

forall b c d e u v l p. (((((forall pfp_i_exists_append_oldpermutationbounded. (exists pfp_gap_exists_append_oldpermutationboundedindex. pfp_gap_exists_append_oldpermutationboundedindex + S (pfp_i_exists_append_oldpermutationbounded) = (l)) -> exists pfp_a_exists_append_oldpermutationbounded. (((exists ff_h_pfp_exists_append_oldpermutationboundedentry. ff_h_pfp_exists_append_oldpermutationboundedentry + S (pfp_a_exists_append_oldpermutationbounded) = S ((S (pfp_i_exists_append_oldpermutationbounded)) * v)) /\ exists ff_q_pfp_exists_append_oldpermutationboundedentry. u = ff_q_pfp_exists_append_oldpermutationboundedentry * S ((S (pfp_i_exists_append_oldpermutationbounded)) * v) + (pfp_a_exists_append_oldpermutationbounded))) /\ (exists pfp_gap_exists_append_oldpermutationboundedvalue. pfp_gap_exists_append_oldpermutationboundedvalue + S (pfp_a_exists_append_oldpermutationbounded) = (l))) /\ (((forall pfp_i_exists_append_oldpermutationinjective pfp_j_exists_append_oldpermutationinjective pfp_a_exists_append_oldpermutationinjective. (exists pfp_gap_exists_append_oldpermutationinjectivefirst. pfp_gap_exists_append_oldpermutationinjectivefirst + S (pfp_i_exists_append_oldpermutationinjective) = (l)) -> (exists pfp_gap_exists_append_oldpermutationinjectivesecond. pfp_gap_exists_append_oldpermutationinjectivesecond + S (pfp_j_exists_append_oldpermutationinjective) = (l)) -> (((exists ff_h_pfp_exists_append_oldpermutationinjectiveleft. ff_h_pfp_exists_append_oldpermutationinjectiveleft + S (pfp_a_exists_append_oldpermutationinjective) = S ((S (pfp_i_exists_append_oldpermutationinjective)) * v)) /\ exists ff_q_pfp_exists_append_oldpermutationinjectiveleft. u = ff_q_pfp_exists_append_oldpermutationinjectiveleft * S ((S (pfp_i_exists_append_oldpermutationinjective)) * v) + (pfp_a_exists_append_oldpermutationinjective))) -> (((exists ff_h_pfp_exists_append_oldpermutationinjectiveright. ff_h_pfp_exists_append_oldpermutationinjectiveright + S (pfp_a_exists_append_oldpermutationinjective) = S ((S (pfp_j_exists_append_oldpermutationinjective)) * v)) /\ exists ff_q_pfp_exists_append_oldpermutationinjectiveright. u = ff_q_pfp_exists_append_oldpermutationinjectiveright * S ((S (pfp_j_exists_append_oldpermutationinjective)) * v) + (pfp_a_exists_append_oldpermutationinjective))) -> pfp_i_exists_append_oldpermutationinjective = pfp_j_exists_append_oldpermutationinjective) /\ (forall pfp_a_exists_append_oldpermutationsurjective. (exists pfp_gap_exists_append_oldpermutationsurjectivevalue. pfp_gap_exists_append_oldpermutationsurjectivevalue + S (pfp_a_exists_append_oldpermutationsurjective) = (l)) -> exists pfp_i_exists_append_oldpermutationsurjective. (exists pfp_gap_exists_append_oldpermutationsurjectiveindex. pfp_gap_exists_append_oldpermutationsurjectiveindex + S (pfp_i_exists_append_oldpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_exists_append_oldpermutationsurjectiveentry. ff_h_pfp_exists_append_oldpermutationsurjectiveentry + S (pfp_a_exists_append_oldpermutationsurjective) = S ((S (pfp_i_exists_append_oldpermutationsurjective)) * v)) /\ exists ff_q_pfp_exists_append_oldpermutationsurjectiveentry. u = ff_q_pfp_exists_append_oldpermutationsurjectiveentry * S ((S (pfp_i_exists_append_oldpermutationsurjective)) * v) + (pfp_a_exists_append_oldpermutationsurjective)))))))) /\ (forall pfp_i_exists_append_oldmatching pfp_j_exists_append_oldmatching pfp_a_exists_append_oldmatching. (exists pfp_gap_exists_append_oldmatchingbound. pfp_gap_exists_append_oldmatchingbound + S (pfp_i_exists_append_oldmatching) = (l)) -> (((exists ff_h_pfp_exists_append_oldmatchingmap. ff_h_pfp_exists_append_oldmatchingmap + S (pfp_j_exists_append_oldmatching) = S ((S (pfp_i_exists_append_oldmatching)) * v)) /\ exists ff_q_pfp_exists_append_oldmatchingmap. u = ff_q_pfp_exists_append_oldmatchingmap * S ((S (pfp_i_exists_append_oldmatching)) * v) + (pfp_j_exists_append_oldmatching))) -> (((exists ff_h_pfp_exists_append_oldmatchingsource. ff_h_pfp_exists_append_oldmatchingsource + S (pfp_a_exists_append_oldmatching) = S ((S (pfp_i_exists_append_oldmatching)) * c)) /\ exists ff_q_pfp_exists_append_oldmatchingsource. b = ff_q_pfp_exists_append_oldmatchingsource * S ((S (pfp_i_exists_append_oldmatching)) * c) + (pfp_a_exists_append_oldmatching))) -> (((exists ff_h_pfp_exists_append_oldmatchingtarget. ff_h_pfp_exists_append_oldmatchingtarget + S (pfp_a_exists_append_oldmatching) = S ((S (pfp_j_exists_append_oldmatching)) * e)) /\ exists ff_q_pfp_exists_append_oldmatchingtarget. d = ff_q_pfp_exists_append_oldmatchingtarget * S ((S (pfp_j_exists_append_oldmatching)) * e) + (pfp_a_exists_append_oldmatching)))))) -> (((exists ff_h_pfp_exists_append_left. ff_h_pfp_exists_append_left + S (p) = S ((S (l)) * c)) /\ exists ff_q_pfp_exists_append_left. b = ff_q_pfp_exists_append_left * S ((S (l)) * c) + (p))) -> (((exists ff_h_pfp_exists_append_right. ff_h_pfp_exists_append_right + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_exists_append_right. d = ff_q_pfp_exists_append_right * S ((S (l)) * e) + (p))) -> exists U V. (((((forall pfp_i_exists_append_newpermutationbounded. (exists pfp_gap_exists_append_newpermutationboundedindex. pfp_gap_exists_append_newpermutationboundedindex + S (pfp_i_exists_append_newpermutationbounded) = (S l)) -> exists pfp_a_exists_append_newpermutationbounded. (((exists ff_h_pfp_exists_append_newpermutationboundedentry. ff_h_pfp_exists_append_newpermutationboundedentry + S (pfp_a_exists_append_newpermutationbounded) = S ((S (pfp_i_exists_append_newpermutationbounded)) * V)) /\ exists ff_q_pfp_exists_append_newpermutationboundedentry. U = ff_q_pfp_exists_append_newpermutationboundedentry * S ((S (pfp_i_exists_append_newpermutationbounded)) * V) + (pfp_a_exists_append_newpermutationbounded))) /\ (exists pfp_gap_exists_append_newpermutationboundedvalue. pfp_gap_exists_append_newpermutationboundedvalue + S (pfp_a_exists_append_newpermutationbounded) = (S l))) /\ (((forall pfp_i_exists_append_newpermutationinjective pfp_j_exists_append_newpermutationinjective pfp_a_exists_append_newpermutationinjective. (exists pfp_gap_exists_append_newpermutationinjectivefirst. pfp_gap_exists_append_newpermutationinjectivefirst + S (pfp_i_exists_append_newpermutationinjective) = (S l)) -> (exists pfp_gap_exists_append_newpermutationinjectivesecond. pfp_gap_exists_append_newpermutationinjectivesecond + S (pfp_j_exists_append_newpermutationinjective) = (S l)) -> (((exists ff_h_pfp_exists_append_newpermutationinjectiveleft. ff_h_pfp_exists_append_newpermutationinjectiveleft + S (pfp_a_exists_append_newpermutationinjective) = S ((S (pfp_i_exists_append_newpermutationinjective)) * V)) /\ exists ff_q_pfp_exists_append_newpermutationinjectiveleft. U = ff_q_pfp_exists_append_newpermutationinjectiveleft * S ((S (pfp_i_exists_append_newpermutationinjective)) * V) + (pfp_a_exists_append_newpermutationinjective))) -> (((exists ff_h_pfp_exists_append_newpermutationinjectiveright. ff_h_pfp_exists_append_newpermutationinjectiveright + S (pfp_a_exists_append_newpermutationinjective) = S ((S (pfp_j_exists_append_newpermutationinjective)) * V)) /\ exists ff_q_pfp_exists_append_newpermutationinjectiveright. U = ff_q_pfp_exists_append_newpermutationinjectiveright * S ((S (pfp_j_exists_append_newpermutationinjective)) * V) + (pfp_a_exists_append_newpermutationinjective))) -> pfp_i_exists_append_newpermutationinjective = pfp_j_exists_append_newpermutationinjective) /\ (forall pfp_a_exists_append_newpermutationsurjective. (exists pfp_gap_exists_append_newpermutationsurjectivevalue. pfp_gap_exists_append_newpermutationsurjectivevalue + S (pfp_a_exists_append_newpermutationsurjective) = (S l)) -> exists pfp_i_exists_append_newpermutationsurjective. (exists pfp_gap_exists_append_newpermutationsurjectiveindex. pfp_gap_exists_append_newpermutationsurjectiveindex + S (pfp_i_exists_append_newpermutationsurjective) = (S l)) /\ (((exists ff_h_pfp_exists_append_newpermutationsurjectiveentry. ff_h_pfp_exists_append_newpermutationsurjectiveentry + S (pfp_a_exists_append_newpermutationsurjective) = S ((S (pfp_i_exists_append_newpermutationsurjective)) * V)) /\ exists ff_q_pfp_exists_append_newpermutationsurjectiveentry. U = ff_q_pfp_exists_append_newpermutationsurjectiveentry * S ((S (pfp_i_exists_append_newpermutationsurjective)) * V) + (pfp_a_exists_append_newpermutationsurjective)))))))) /\ (forall pfp_i_exists_append_newmatching pfp_j_exists_append_newmatching pfp_a_exists_append_newmatching. (exists pfp_gap_exists_append_newmatchingbound. pfp_gap_exists_append_newmatchingbound + S (pfp_i_exists_append_newmatching) = (S l)) -> (((exists ff_h_pfp_exists_append_newmatchingmap. ff_h_pfp_exists_append_newmatchingmap + S (pfp_j_exists_append_newmatching) = S ((S (pfp_i_exists_append_newmatching)) * V)) /\ exists ff_q_pfp_exists_append_newmatchingmap. U = ff_q_pfp_exists_append_newmatchingmap * S ((S (pfp_i_exists_append_newmatching)) * V) + (pfp_j_exists_append_newmatching))) -> (((exists ff_h_pfp_exists_append_newmatchingsource. ff_h_pfp_exists_append_newmatchingsource + S (pfp_a_exists_append_newmatching) = S ((S (pfp_i_exists_append_newmatching)) * c)) /\ exists ff_q_pfp_exists_append_newmatchingsource. b = ff_q_pfp_exists_append_newmatchingsource * S ((S (pfp_i_exists_append_newmatching)) * c) + (pfp_a_exists_append_newmatching))) -> (((exists ff_h_pfp_exists_append_newmatchingtarget. ff_h_pfp_exists_append_newmatchingtarget + S (pfp_a_exists_append_newmatching) = S ((S (pfp_j_exists_append_newmatching)) * e)) /\ exists ff_q_pfp_exists_append_newmatchingtarget. d = ff_q_pfp_exists_append_newmatchingtarget * S ((S (pfp_j_exists_append_newmatching)) * e) + (pfp_a_exists_append_newmatching))))))

Constructive proof overview

Generated structural guide

Existence-only append interface still returns an actual fully bijective matching beta map.

The unchanged tactic script uses 1 declared prerequisite and contains 30 exact native proof lines.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

AF0010 factor_permutation_matched_append

Direct dependents

AF0019 prime_factor_lists_matching_by_length

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

30 script commands · 7 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.

Named ingredients (1)
factor permutation matched append

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro u
  6. L6
    intro v
  7. L7
    intro l
  8. L8
    intro p
  9. L9
    intro hm
  10. L10
    intro hleft
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hright
03Establish hexL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation matched append.

  1. L12
    have hex : ∃ U. ∃ V. PermutationPrefix(U,V,S l) ∧ FactorListMatching(b,c,d,e,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: PermutationPrefixFactorListMatchingLtBetaAt
  2. L13
    specialize factor_permutation_matched_append (b)
  3. L14
    specialize factor_permutation_matched_append (c)
  4. L15
    specialize factor_permutation_matched_append (d)
  5. L16
    specialize factor_permutation_matched_append (e)
  6. L17
    specialize factor_permutation_matched_append (u)
  7. L18
    specialize factor_permutation_matched_append (v)
  8. L19
    specialize factor_permutation_matched_append (l)
  9. L20
    specialize factor_permutation_matched_append (p)
  10. L21
    apply factor_permutation_matched_append
04Use earlier factsL22–24

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L22
    exact hm
  2. L23
    exact hleft
  3. L24
    exact hright
05Separate the logical casesL25–27

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

  1. L25
    cases hex
  2. L26
    cases hex_witness
  3. L27
    cases hex_witness_witness
06Construct an explicit witnessL28–29

Supply the displayed value, then prove that it has the required property.

  1. L28
    exists x
  2. L29
    exists x1
07Use earlier factsL30–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L30
    exact hex_witness_witness_left

Library-wide reading audit

Original exact command ledger · 30 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro u
  6. 0006intro v
  7. 0007intro l
  8. 0008intro p
  9. 0009intro hm
  10. 0010intro hleft
  11. 0011intro hright
  12. 0012have hex : exists U V. ((((((forall pfp_i_exists_append_witnesspermutationbounded. (exists pfp_gap_exists_append_witnesspermutationboundedindex. pfp_gap_exists_append_witnesspermutationboundedindex + S (pfp_i_exists_append_witnesspermutationbounded) = (S l)) -> exists pfp_a_exists_append_witnesspermutationbounded. (((exists ff_h_pfp_exists_append_witnesspermutationboundedentry. ff_h_pfp_exists_append_witnesspermutationboundedentry + S (pfp_a_exists_append_witnesspermutationbounded) = S ((S (pfp_i_exists_append_witnesspermutationbounded)) * V)) /\ exists ff_q_pfp_exists_append_witnesspermutationboundedentry. U = ff_q_pfp_exists_append_witnesspermutationboundedentry * S ((S (pfp_i_exists_append_witnesspermutationbounded)) * V) + (pfp_a_exists_append_witnesspermutationbounded))) /\ (exists pfp_gap_exists_append_witnesspermutationboundedvalue. pfp_gap_exists_append_witnesspermutationboundedvalue + S (pfp_a_exists_append_witnesspermutationbounded) = (S l))) /\ (((forall pfp_i_exists_append_witnesspermutationinjective pfp_j_exists_append_witnesspermutationinjective pfp_a_exists_append_witnesspermutationinjective. (exists pfp_gap_exists_append_witnesspermutationinjectivefirst. pfp_gap_exists_append_witnesspermutationinjectivefirst + S (pfp_i_exists_append_witnesspermutationinjective) = (S l)) -> (exists pfp_gap_exists_append_witnesspermutationinjectivesecond. pfp_gap_exists_append_witnesspermutationinjectivesecond + S (pfp_j_exists_append_witnesspermutationinjective) = (S l)) -> (((exists ff_h_pfp_exists_append_witnesspermutationinjectiveleft. ff_h_pfp_exists_append_witnesspermutationinjectiveleft + S (pfp_a_exists_append_witnesspermutationinjective) = S ((S (pfp_i_exists_append_witnesspermutationinjective)) * V)) /\ exists ff_q_pfp_exists_append_witnesspermutationinjectiveleft. U = ff_q_pfp_exists_append_witnesspermutationinjectiveleft * S ((S (pfp_i_exists_append_witnesspermutationinjective)) * V) + (pfp_a_exists_append_witnesspermutationinjective))) -> (((exists ff_h_pfp_exists_append_witnesspermutationinjectiveright. ff_h_pfp_exists_append_witnesspermutationinjectiveright + S (pfp_a_exists_append_witnesspermutationinjective) = S ((S (pfp_j_exists_append_witnesspermutationinjective)) * V)) /\ exists ff_q_pfp_exists_append_witnesspermutationinjectiveright. U = ff_q_pfp_exists_append_witnesspermutationinjectiveright * S ((S (pfp_j_exists_append_witnesspermutationinjective)) * V) + (pfp_a_exists_append_witnesspermutationinjective))) -> pfp_i_exists_append_witnesspermutationinjective = pfp_j_exists_append_witnesspermutationinjective) /\ (forall pfp_a_exists_append_witnesspermutationsurjective. (exists pfp_gap_exists_append_witnesspermutationsurjectivevalue. pfp_gap_exists_append_witnesspermutationsurjectivevalue + S (pfp_a_exists_append_witnesspermutationsurjective) = (S l)) -> exists pfp_i_exists_append_witnesspermutationsurjective. (exists pfp_gap_exists_append_witnesspermutationsurjectiveindex. pfp_gap_exists_append_witnesspermutationsurjectiveindex + S (pfp_i_exists_append_witnesspermutationsurjective) = (S l)) /\ (((exists ff_h_pfp_exists_append_witnesspermutationsurjectiveentry. ff_h_pfp_exists_append_witnesspermutationsurjectiveentry + S (pfp_a_exists_append_witnesspermutationsurjective) = S ((S (pfp_i_exists_append_witnesspermutationsurjective)) * V)) /\ exists ff_q_pfp_exists_append_witnesspermutationsurjectiveentry. U = ff_q_pfp_exists_append_witnesspermutationsurjectiveentry * S ((S (pfp_i_exists_append_witnesspermutationsurjective)) * V) + (pfp_a_exists_append_witnesspermutationsurjective)))))))) /\ (forall pfp_i_exists_append_witnessmatching pfp_j_exists_append_witnessmatching pfp_a_exists_append_witnessmatching. (exists pfp_gap_exists_append_witnessmatchingbound. pfp_gap_exists_append_witnessmatchingbound + S (pfp_i_exists_append_witnessmatching) = (S l)) -> (((exists ff_h_pfp_exists_append_witnessmatchingmap. ff_h_pfp_exists_append_witnessmatchingmap + S (pfp_j_exists_append_witnessmatching) = S ((S (pfp_i_exists_append_witnessmatching)) * V)) /\ exists ff_q_pfp_exists_append_witnessmatchingmap. U = ff_q_pfp_exists_append_witnessmatchingmap * S ((S (pfp_i_exists_append_witnessmatching)) * V) + (pfp_j_exists_append_witnessmatching))) -> (((exists ff_h_pfp_exists_append_witnessmatchingsource. ff_h_pfp_exists_append_witnessmatchingsource + S (pfp_a_exists_append_witnessmatching) = S ((S (pfp_i_exists_append_witnessmatching)) * c)) /\ exists ff_q_pfp_exists_append_witnessmatchingsource. b = ff_q_pfp_exists_append_witnessmatchingsource * S ((S (pfp_i_exists_append_witnessmatching)) * c) + (pfp_a_exists_append_witnessmatching))) -> (((exists ff_h_pfp_exists_append_witnessmatchingtarget. ff_h_pfp_exists_append_witnessmatchingtarget + S (pfp_a_exists_append_witnessmatching) = S ((S (pfp_j_exists_append_witnessmatching)) * e)) /\ exists ff_q_pfp_exists_append_witnessmatchingtarget. d = ff_q_pfp_exists_append_witnessmatchingtarget * S ((S (pfp_j_exists_append_witnessmatching)) * e) + (pfp_a_exists_append_witnessmatching)))))) /\ (((((exists ff_h_pfp_exists_append_extensionlast. ff_h_pfp_exists_append_extensionlast + S (l) = S ((S (l)) * V)) /\ exists ff_q_pfp_exists_append_extensionlast. U = ff_q_pfp_exists_append_extensionlast * S ((S (l)) * V) + (l))) /\ (forall pfp_i_exists_append_extensionprefix pfp_a_exists_append_extensionprefix. (exists pfp_gap_exists_append_extensionprefixbound. pfp_gap_exists_append_extensionprefixbound + S (pfp_i_exists_append_extensionprefix) = (l)) -> (((exists ff_h_pfp_exists_append_extensionprefixold. ff_h_pfp_exists_append_extensionprefixold + S (pfp_a_exists_append_extensionprefix) = S ((S (pfp_i_exists_append_extensionprefix)) * v)) /\ exists ff_q_pfp_exists_append_extensionprefixold. u = ff_q_pfp_exists_append_extensionprefixold * S ((S (pfp_i_exists_append_extensionprefix)) * v) + (pfp_a_exists_append_extensionprefix))) -> (((exists ff_h_pfp_exists_append_extensionprefixnew. ff_h_pfp_exists_append_extensionprefixnew + S (pfp_a_exists_append_extensionprefix) = S ((S (pfp_i_exists_append_extensionprefix)) * V)) /\ exists ff_q_pfp_exists_append_extensionprefixnew. U = ff_q_pfp_exists_append_extensionprefixnew * S ((S (pfp_i_exists_append_extensionprefix)) * V) + (pfp_a_exists_append_extensionprefix)))))))
  13. 0013specialize factor_permutation_matched_append (b)
  14. 0014specialize factor_permutation_matched_append (c)
  15. 0015specialize factor_permutation_matched_append (d)
  16. 0016specialize factor_permutation_matched_append (e)
  17. 0017specialize factor_permutation_matched_append (u)
  18. 0018specialize factor_permutation_matched_append (v)
  19. 0019specialize factor_permutation_matched_append (l)
  20. 0020specialize factor_permutation_matched_append (p)
  21. 0021apply factor_permutation_matched_append
  22. 0022exact hm
  23. 0023exact hleft
  24. 0024exact hright
  25. 0025cases hex
  26. 0026cases hex_witness
  27. 0027cases hex_witness_witness
  28. 0028exists x
  29. 0029exists x1
  30. 0030exact hex_witness_witness_left