PA009K · theorem

beta_prefix_append_two_exists

Alpha v34 checked-use theorem · independently closed; not Stable

Append two values at consecutive beta positions while preserving every old entry.

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.

Statement with defined notation

∀ b. ∀ c. ∀ l. ∀ a. ∀ e. ∃ z. ∃ d. BetaAt(z,d,l,a) ∧ (BetaAt(z,d,S l,e) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,y)))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0013 BetaAt

5 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

9 occurrences

Exact expanded native-PA statement
forall b c l a e. exists z d. (((((exists wpo_beta_height_append_result_first. wpo_beta_height_append_result_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_append_result_first. z = wpo_beta_quotient_append_result_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_append_result_second. wpo_beta_height_append_result_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_append_result_second. z = wpo_beta_quotient_append_result_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_append_result wpo_old_value_append_result. (exists wpo_gap_append_result_old_bound. wpo_gap_append_result_old_bound + S (wpo_old_index_append_result) = l) -> (((exists wpo_beta_height_append_result_old_entry. wpo_beta_height_append_result_old_entry + S (wpo_old_value_append_result) = S ((S (wpo_old_index_append_result)) * c)) /\ exists wpo_beta_quotient_append_result_old_entry. b = wpo_beta_quotient_append_result_old_entry * S ((S (wpo_old_index_append_result)) * c) + (wpo_old_value_append_result))) -> (((exists wpo_beta_height_append_result_new_entry. wpo_beta_height_append_result_new_entry + S (wpo_old_value_append_result) = S ((S (wpo_old_index_append_result)) * d)) /\ exists wpo_beta_quotient_append_result_new_entry. z = wpo_beta_quotient_append_result_new_entry * S ((S (wpo_old_index_append_result)) * d) + (wpo_old_value_append_result)))))))

Proof neighborhood

Direct theorem prerequisites

PA002X beta_prefix_extend PA001A le_refl PA002O le_succ

Direct theorem dependents

PA009O scaled_inverse_pair_order_choose_append PA00AE finite_prefix_choose_unused_nonendpoint PA00AV prime_pair_order_choose_append

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

52 script commands · 14 reading checkpoints · 3 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 (3)
beta prefix extendle reflle succ
01Fix variables and assumptionsL1–5

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro a
  5. L5
    intro e
02Establish hfirst_extendL6–7

Establish this local claim before using it. It is not an additional assumption.

  1. L6
    have hfirst_extend : ∀ k. ∀ q. ∀ s. ∀ v. ∃ r. ∃ t. BetaAt(r,t,k,v) ∧ (∀ x. ∀ y. Lt(x,k) → BetaAt(q,s,x,y) → BetaAt(r,t,x,y))Definitions: BetaAt(r,t,k,v)Lt(x,k)BetaAt(q,s,x,y)BetaAt(r,t,x,y)Original native command in the exact edition
  2. L7
    exact beta_prefix_extend
03Establish hsecond_extendL8–13

Establish this local claim before using it. It is not an additional assumption.

  1. L8
    have hsecond_extend : ∀ k. ∀ q. ∀ s. ∀ v. ∃ r. ∃ t. BetaAt(r,t,k,v) ∧ (∀ x. ∀ y. Lt(x,k) → BetaAt(q,s,x,y) → BetaAt(r,t,x,y))Definitions: BetaAt(r,t,k,v)Lt(x,k)BetaAt(q,s,x,y)BetaAt(r,t,x,y)Original native command in the exact edition
  2. L9
    exact beta_prefix_extend
  3. L10
    specialize hfirst_extend l
  4. L11
    specialize hfirst_extend b
  5. L12
    specialize hfirst_extend c
  6. L13
    specialize hfirst_extend a
04Separate the logical casesL14–16

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

  1. L14
    cases hfirst_extend
  2. L15
    cases hfirst_extend_witness
  3. L16
    cases hfirst_extend_witness_witness
05Use earlier factsL17–20

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

  1. L17
    specialize hsecond_extend (S l)
  2. L18
    specialize hsecond_extend x
  3. L19
    specialize hsecond_extend x1
  4. L20
    specialize hsecond_extend e
06Separate the logical casesL21–23

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

  1. L21
    cases hsecond_extend
  2. L22
    cases hsecond_extend_witness
  3. L23
    cases hsecond_extend_witness_witness
07Construct an explicit witnessL24–25

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

  1. L24
    exists x2
  2. L25
    exists x3
08Separate the logical casesL26–26

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

  1. L26
    split
09Use earlier factsL27–32

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

  1. L27
    specialize hsecond_extend_witness_witness_right l
  2. L28
    specialize hsecond_extend_witness_witness_right a
  3. L29
    apply hsecond_extend_witness_witness_right
  4. L30
    specialize le_refl (S l)
  5. L31
    exact le_refl
  6. L32
    exact hfirst_extend_witness_witness_left
10Separate the logical casesL33–33

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

  1. L33
    split
11Use earlier factsL34–34

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

  1. L34
    exact hsecond_extend_witness_witness_left
12Fix variables and assumptionsL35–38

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

  1. L35
    intro i
  2. L36
    intro v
  3. L37
    intro hi
  4. L38
    intro hold
13Establish hmiddleL39–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hfirst extend witness witness right.

  1. L39
    have hmiddle : BetaAt(x,x1,i,v)Definitions: BetaAt(x,x1,i,v)Original native command in the exact edition
  2. L40
    specialize hfirst_extend_witness_witness_right i
  3. L41
    specialize hfirst_extend_witness_witness_right v
  4. L42
    apply hfirst_extend_witness_witness_right
  5. L43
    exact hi
  6. L44
    exact hold
  7. L45
    specialize hsecond_extend_witness_witness_right i
  8. L46
    specialize hsecond_extend_witness_witness_right v
  9. L47
    apply hsecond_extend_witness_witness_right
  10. L48
    specialize le_succ (S i)
14Use earlier factsL49–52

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

  1. L49
    specialize le_succ l
  2. L50
    apply le_succ
  3. L51
    exact hi
  4. L52
    exact hmiddle

Library-wide reading audit

Original defined command ledger · 52 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro a
  5. 0005intro e
  6. 0006have hfirst_extend : ∀ k. ∀ q. ∀ s. ∀ v. ∃ r. ∃ t. BetaAt(r,t,k,v) ∧ (∀ x. ∀ y. Lt(x,k) → BetaAt(q,s,x,y) → BetaAt(r,t,x,y))
    Exact native replay linehave hfirst_extend : forall k q s v. exists r t. (((exists h. h + S v = S ((S k) * t)) /\ exists u. r = u * S ((S k) * t) + v) /\ forall i w. (exists h. h + S i = k) -> ((exists h. h + S w = S ((S i) * s)) /\ exists u. q = u * S ((S i) * s) + w) -> ((exists h. h + S w = S ((S i) * t)) /\ exists u. r = u * S ((S i) * t) + w))
  7. 0007exact beta_prefix_extend
  8. 0008have hsecond_extend : ∀ k. ∀ q. ∀ s. ∀ v. ∃ r. ∃ t. BetaAt(r,t,k,v) ∧ (∀ x. ∀ y. Lt(x,k) → BetaAt(q,s,x,y) → BetaAt(r,t,x,y))
    Exact native replay linehave hsecond_extend : forall k q s v. exists r t. (((exists h. h + S v = S ((S k) * t)) /\ exists u. r = u * S ((S k) * t) + v) /\ forall i w. (exists h. h + S i = k) -> ((exists h. h + S w = S ((S i) * s)) /\ exists u. q = u * S ((S i) * s) + w) -> ((exists h. h + S w = S ((S i) * t)) /\ exists u. r = u * S ((S i) * t) + w))
  9. 0009exact beta_prefix_extend
  10. 0010specialize hfirst_extend l
  11. 0011specialize hfirst_extend b
  12. 0012specialize hfirst_extend c
  13. 0013specialize hfirst_extend a
  14. 0014cases hfirst_extend
  15. 0015cases hfirst_extend_witness
  16. 0016cases hfirst_extend_witness_witness
  17. 0017specialize hsecond_extend (S l)
  18. 0018specialize hsecond_extend x
  19. 0019specialize hsecond_extend x1
  20. 0020specialize hsecond_extend e
  21. 0021cases hsecond_extend
  22. 0022cases hsecond_extend_witness
  23. 0023cases hsecond_extend_witness_witness
  24. 0024exists x2
  25. 0025exists x3
  26. 0026split
  27. 0027specialize hsecond_extend_witness_witness_right l
  28. 0028specialize hsecond_extend_witness_witness_right a
  29. 0029apply hsecond_extend_witness_witness_right
  30. 0030specialize le_refl (S l)
  31. 0031exact le_refl
  32. 0032exact hfirst_extend_witness_witness_left
  33. 0033split
  34. 0034exact hsecond_extend_witness_witness_left
  35. 0035intro i
  36. 0036intro v
  37. 0037intro hi
  38. 0038intro hold
  39. 0039have hmiddle : BetaAt(x,x1,i,v)
    Exact native replay linehave hmiddle : ((exists wpo_beta_height_append_old_middle. wpo_beta_height_append_old_middle + S (v) = S ((S (i)) * x1)) /\ exists wpo_beta_quotient_append_old_middle. x = wpo_beta_quotient_append_old_middle * S ((S (i)) * x1) + (v))
  40. 0040specialize hfirst_extend_witness_witness_right i
  41. 0041specialize hfirst_extend_witness_witness_right v
  42. 0042apply hfirst_extend_witness_witness_right
  43. 0043exact hi
  44. 0044exact hold
  45. 0045specialize hsecond_extend_witness_witness_right i
  46. 0046specialize hsecond_extend_witness_witness_right v
  47. 0047apply hsecond_extend_witness_witness_right
  48. 0048specialize le_succ (S i)
  49. 0049specialize le_succ l
  50. 0050apply le_succ
  51. 0051exact hi
  52. 0052exact hmiddle