PA009P · theorem

beta_prefix_append_two_bounded_into

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

A two-entry append remains bounded when the old prefix and both appended values are bounded.

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. ∀ z. ∀ d. ∀ l. ∀ n. ∀ a. ∀ e. 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))) → (∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) → Lt(a,n) → Lt(e,n) → ∀ x. Lt(x,S S l) → ∃ y. BetaAt(z,d,x,y) ∧ Lt(y,n)

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

13 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

4 occurrences

Exact expanded native-PA statement
forall b c z d l n a e. (((((exists wpo_beta_height_wpoi_append_bounded_trace_first. wpo_beta_height_wpoi_append_bounded_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_wpoi_append_bounded_trace_first. z = wpo_beta_quotient_wpoi_append_bounded_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_wpoi_append_bounded_trace_second. wpo_beta_height_wpoi_append_bounded_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_wpoi_append_bounded_trace_second. z = wpo_beta_quotient_wpoi_append_bounded_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_wpoi_append_bounded_trace wpo_old_value_wpoi_append_bounded_trace. (exists wpo_gap_wpoi_append_bounded_trace_old_bound. wpo_gap_wpoi_append_bounded_trace_old_bound + S (wpo_old_index_wpoi_append_bounded_trace) = l) -> (((exists wpo_beta_height_wpoi_append_bounded_trace_old_entry. wpo_beta_height_wpoi_append_bounded_trace_old_entry + S (wpo_old_value_wpoi_append_bounded_trace) = S ((S (wpo_old_index_wpoi_append_bounded_trace)) * c)) /\ exists wpo_beta_quotient_wpoi_append_bounded_trace_old_entry. b = wpo_beta_quotient_wpoi_append_bounded_trace_old_entry * S ((S (wpo_old_index_wpoi_append_bounded_trace)) * c) + (wpo_old_value_wpoi_append_bounded_trace))) -> (((exists wpo_beta_height_wpoi_append_bounded_trace_new_entry. wpo_beta_height_wpoi_append_bounded_trace_new_entry + S (wpo_old_value_wpoi_append_bounded_trace) = S ((S (wpo_old_index_wpoi_append_bounded_trace)) * d)) /\ exists wpo_beta_quotient_wpoi_append_bounded_trace_new_entry. z = wpo_beta_quotient_wpoi_append_bounded_trace_new_entry * S ((S (wpo_old_index_wpoi_append_bounded_trace)) * d) + (wpo_old_value_wpoi_append_bounded_trace))))))) -> (forall fom_index_wpoi_append_bounded_before. (exists fom_gap_wpoi_append_bounded_before_index_bound. fom_gap_wpoi_append_bounded_before_index_bound + S (fom_index_wpoi_append_bounded_before) = l) -> exists fom_value_wpoi_append_bounded_before. ((((exists fom_beta_height_wpoi_append_bounded_before_entry. fom_beta_height_wpoi_append_bounded_before_entry + S (fom_value_wpoi_append_bounded_before) = S ((S (fom_index_wpoi_append_bounded_before)) * c)) /\ exists fom_beta_quotient_wpoi_append_bounded_before_entry. b = fom_beta_quotient_wpoi_append_bounded_before_entry * S ((S (fom_index_wpoi_append_bounded_before)) * c) + (fom_value_wpoi_append_bounded_before))) /\ (exists fom_gap_wpoi_append_bounded_before_value_bound. fom_gap_wpoi_append_bounded_before_value_bound + S (fom_value_wpoi_append_bounded_before) = n))) -> (exists wpo_gap_wpoi_append_first_bound. wpo_gap_wpoi_append_first_bound + S (a) = n) -> (exists wpo_gap_wpoi_append_second_bound. wpo_gap_wpoi_append_second_bound + S (e) = n) -> (forall fom_index_wpoi_append_bounded_after. (exists fom_gap_wpoi_append_bounded_after_index_bound. fom_gap_wpoi_append_bounded_after_index_bound + S (fom_index_wpoi_append_bounded_after) = S (S l)) -> exists fom_value_wpoi_append_bounded_after. ((((exists fom_beta_height_wpoi_append_bounded_after_entry. fom_beta_height_wpoi_append_bounded_after_entry + S (fom_value_wpoi_append_bounded_after) = S ((S (fom_index_wpoi_append_bounded_after)) * d)) /\ exists fom_beta_quotient_wpoi_append_bounded_after_entry. z = fom_beta_quotient_wpoi_append_bounded_after_entry * S ((S (fom_index_wpoi_append_bounded_after)) * d) + (fom_value_wpoi_append_bounded_after))) /\ (exists fom_gap_wpoi_append_bounded_after_value_bound. fom_gap_wpoi_append_bounded_after_value_bound + S (fom_value_wpoi_append_bounded_after) = n)))

Proof neighborhood

Direct theorem prerequisites

PA003D finite_lt_succ_eq_or_lt

Direct theorem dependents

PA009T scaled_inverse_pair_order_paired_state_step PA00AX prime_pair_order_choose_append_state

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

54 script commands · 21 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 (1)
finite lt succ eq or lt
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 z
  4. L4
    intro d
  5. L5
    intro l
  6. L6
    intro n
  7. L7
    intro a
  8. L8
    intro e
  9. L9
    intro htrace
  10. L10
    intro hold_bounded
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hfirst_bounded
  2. L12
    intro hsecond_bounded
03Separate the logical casesL13–14

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

  1. L13
    cases htrace
  2. L14
    cases htrace_right
04Fix variables and assumptionsL15–16

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

  1. L15
    intro q
  2. L16
    intro hq
05Establish htopL17–21

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

  1. L17
    have htop : q = S l ∨ Lt(q,S l)Definitions: Lt(q,S l)Original native command in the exact edition
  2. L18
    specialize finite_lt_succ_eq_or_lt (S l)
  3. L19
    specialize finite_lt_succ_eq_or_lt q
  4. L20
    apply finite_lt_succ_eq_or_lt
  5. L21
    exact hq
06Separate the logical casesL22–22

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

  1. L22
    cases htop
07Construct an explicit witnessL23–23

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

  1. L23
    exists e
08Separate the logical casesL24–24

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

  1. L24
    split
09Calculate and transport equalitiesL25–26

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L25
    rewrite htop_left
  2. L26
    rewrite htop_left
10Use earlier factsL27–28

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

  1. L27
    exact htrace_right_left
  2. L28
    exact hsecond_bounded
11Establish hmiddleL29–33

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

  1. L29
    have hmiddle : q = l ∨ Lt(q,l)Definitions: Lt(q,l)Original native command in the exact edition
  2. L30
    specialize finite_lt_succ_eq_or_lt l
  3. L31
    specialize finite_lt_succ_eq_or_lt q
  4. L32
    apply finite_lt_succ_eq_or_lt
  5. L33
    exact htop_right
12Separate the logical casesL34–34

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

  1. L34
    cases hmiddle
13Construct an explicit witnessL35–35

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

  1. L35
    exists a
14Separate the logical casesL36–36

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

  1. L36
    split
15Calculate and transport equalitiesL37–38

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L37
    rewrite hmiddle_left
  2. L38
    rewrite hmiddle_left
16Use earlier factsL39–40

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

  1. L39
    exact htrace_left
  2. L40
    exact hfirst_bounded
17Establish hold_entryL41–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hold bounded.

  1. L41
    have hold_entry : ∃ w. BetaAt(b,c,q,w) ∧ Lt(w,n)Definitions: BetaAt(b,c,q,w)Lt(w,n)Original native command in the exact edition
  2. L42
    specialize hold_bounded q
  3. L43
    apply hold_bounded
  4. L44
    exact hmiddle_right
18Separate the logical casesL45–46

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

  1. L45
    cases hold_entry
  2. L46
    cases hold_entry_witness
19Construct an explicit witnessL47–47

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

  1. L47
    exists x
20Separate the logical casesL48–48

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

  1. L48
    split
21Use earlier factsL49–54

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

  1. L49
    specialize htrace_right_right q
  2. L50
    specialize htrace_right_right x
  3. L51
    apply htrace_right_right
  4. L52
    exact hmiddle_right
  5. L53
    exact hold_entry_witness_left
  6. L54
    exact hold_entry_witness_right

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro l
  6. 0006intro n
  7. 0007intro a
  8. 0008intro e
  9. 0009intro htrace
  10. 0010intro hold_bounded
  11. 0011intro hfirst_bounded
  12. 0012intro hsecond_bounded
  13. 0013cases htrace
  14. 0014cases htrace_right
  15. 0015intro q
  16. 0016intro hq
  17. 0017have htop : q = S l ∨ Lt(q,S l)
    Exact native replay linehave htop : q = S l \/ exists h. h + S q = S l
  18. 0018specialize finite_lt_succ_eq_or_lt (S l)
  19. 0019specialize finite_lt_succ_eq_or_lt q
  20. 0020apply finite_lt_succ_eq_or_lt
  21. 0021exact hq
  22. 0022cases htop
  23. 0023exists e
  24. 0024split
  25. 0025rewrite htop_left
  26. 0026rewrite htop_left
  27. 0027exact htrace_right_left
  28. 0028exact hsecond_bounded
  29. 0029have hmiddle : q = l ∨ Lt(q,l)
    Exact native replay linehave hmiddle : q = l \/ exists h. h + S q = l
  30. 0030specialize finite_lt_succ_eq_or_lt l
  31. 0031specialize finite_lt_succ_eq_or_lt q
  32. 0032apply finite_lt_succ_eq_or_lt
  33. 0033exact htop_right
  34. 0034cases hmiddle
  35. 0035exists a
  36. 0036split
  37. 0037rewrite hmiddle_left
  38. 0038rewrite hmiddle_left
  39. 0039exact htrace_left
  40. 0040exact hfirst_bounded
  41. 0041have hold_entry : ∃ w. BetaAt(b,c,q,w) ∧ Lt(w,n)
    Exact native replay linehave hold_entry : exists w. ((((exists wpo_beta_height_wpoi_append_bounded_old_entry. wpo_beta_height_wpoi_append_bounded_old_entry + S (w) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wpoi_append_bounded_old_entry. b = wpo_beta_quotient_wpoi_append_bounded_old_entry * S ((S (q)) * c) + (w))) /\ (exists wpo_gap_wpoi_append_bounded_old_value_bound. wpo_gap_wpoi_append_bounded_old_value_bound + S (w) = n))
  42. 0042specialize hold_bounded q
  43. 0043apply hold_bounded
  44. 0044exact hmiddle_right
  45. 0045cases hold_entry
  46. 0046cases hold_entry_witness
  47. 0047exists x
  48. 0048split
  49. 0049specialize htrace_right_right q
  50. 0050specialize htrace_right_right x
  51. 0051apply htrace_right_right
  52. 0052exact hmiddle_right
  53. 0053exact hold_entry_witness_left
  54. 0054exact hold_entry_witness_right