PA009L · theorem

beta_prefix_append_two_reflect

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

Every entry of a two-appended prefix is the second append, the first append, or an 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. ∀ z. ∀ d. ∀ l. ∀ 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. ∀ y. Lt(x,S S l) → BetaAt(z,d,x,y) → x = S l ∧ y = e ∨ (x = l ∧ y = a ∨ Lt(x,l) ∧ BetaAt(b,c,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

9 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

4 occurrences

Exact expanded native-PA statement
forall b c z d l a e. (((((exists wpo_beta_height_reflect_trace_first. wpo_beta_height_reflect_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_reflect_trace_first. z = wpo_beta_quotient_reflect_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_reflect_trace_second. wpo_beta_height_reflect_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_reflect_trace_second. z = wpo_beta_quotient_reflect_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_reflect_trace wpo_old_value_reflect_trace. (exists wpo_gap_reflect_trace_old_bound. wpo_gap_reflect_trace_old_bound + S (wpo_old_index_reflect_trace) = l) -> (((exists wpo_beta_height_reflect_trace_old_entry. wpo_beta_height_reflect_trace_old_entry + S (wpo_old_value_reflect_trace) = S ((S (wpo_old_index_reflect_trace)) * c)) /\ exists wpo_beta_quotient_reflect_trace_old_entry. b = wpo_beta_quotient_reflect_trace_old_entry * S ((S (wpo_old_index_reflect_trace)) * c) + (wpo_old_value_reflect_trace))) -> (((exists wpo_beta_height_reflect_trace_new_entry. wpo_beta_height_reflect_trace_new_entry + S (wpo_old_value_reflect_trace) = S ((S (wpo_old_index_reflect_trace)) * d)) /\ exists wpo_beta_quotient_reflect_trace_new_entry. z = wpo_beta_quotient_reflect_trace_new_entry * S ((S (wpo_old_index_reflect_trace)) * d) + (wpo_old_value_reflect_trace))))))) -> forall i v. (exists wpo_gap_reflect_new_bound. wpo_gap_reflect_new_bound + S (i) = S (S l)) -> (((exists wpo_beta_height_reflect_new_entry. wpo_beta_height_reflect_new_entry + S (v) = S ((S (i)) * d)) /\ exists wpo_beta_quotient_reflect_new_entry. z = wpo_beta_quotient_reflect_new_entry * S ((S (i)) * d) + (v))) -> (((i = S (l) /\ v = e) \/ ((i = l /\ v = a) \/ ((exists wpo_gap_reflect_result_old_bound. wpo_gap_reflect_result_old_bound + S (i) = l) /\ (((exists wpo_beta_height_reflect_result_old_entry. wpo_beta_height_reflect_result_old_entry + S (v) = S ((S (i)) * c)) /\ exists wpo_beta_quotient_reflect_result_old_entry. b = wpo_beta_quotient_reflect_result_old_entry * S ((S (i)) * c) + (v)))))))

Proof neighborhood

Direct theorem prerequisites

PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique

Direct theorem dependents

PA009M beta_prefix_append_two_scaled_orbit_closed PA009N beta_prefix_append_two_injective PA00AT beta_prefix_append_two_orbit_closed PA00AU beta_prefix_append_two_nonendpoint

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

85 script commands · 21 reading checkpoints · 7 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)
finite lt succ eq or ltbeta at existsbeta at unique
01Fix variables and assumptionsL1–8

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 a
  7. L7
    intro e
  8. L8
    intro htrace
02Separate the logical casesL9–10

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

  1. L9
    cases htrace
  2. L10
    cases htrace_right
03Fix variables and assumptionsL11–14

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

  1. L11
    intro i
  2. L12
    intro v
  3. L13
    intro hi
  4. L14
    intro hentry
04Establish htopL15–19

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. L15
    have htop : i = S l ∨ Lt(i,S l)Definitions: Lt(i,S l)Original native command in the exact edition
  2. L16
    specialize finite_lt_succ_eq_or_lt (S l)
  3. L17
    specialize finite_lt_succ_eq_or_lt i
  4. L18
    apply finite_lt_succ_eq_or_lt
  5. L19
    exact hi
05Separate the logical casesL20–22

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

  1. L20
    cases htop
  2. L21
    left
  3. L22
    split
06Use earlier factsL23–23

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

  1. L23
    exact htop_left
07Establish hiveL24–33

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

  1. L24
    have hive : v = e
  2. L25
    specialize beta_at_unique z
  3. L26
    specialize beta_at_unique d
  4. L27
    specialize beta_at_unique (S l)
  5. L28
    specialize beta_at_unique v
  6. L29
    specialize beta_at_unique e
  7. L30
    apply beta_at_unique
  8. L31
    rewrite htop_left at hentry
  9. L32
    rewrite htop_left at hentry
  10. L33
    exact hentry
08Use earlier factsL34–35

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

  1. L34
    exact htrace_right_left
  2. L35
    exact hive
09Establish hmiddleL36–40

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. L36
    have hmiddle : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L37
    specialize finite_lt_succ_eq_or_lt l
  3. L38
    specialize finite_lt_succ_eq_or_lt i
  4. L39
    apply finite_lt_succ_eq_or_lt
  5. L40
    exact htop_right
10Separate the logical casesL41–44

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

  1. L41
    cases hmiddle
  2. L42
    right
  3. L43
    left
  4. L44
    split
11Use earlier factsL45–45

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

  1. L45
    exact hmiddle_left
12Establish hivaL46–55

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

  1. L46
    have hiva : v = a
  2. L47
    specialize beta_at_unique z
  3. L48
    specialize beta_at_unique d
  4. L49
    specialize beta_at_unique l
  5. L50
    specialize beta_at_unique v
  6. L51
    specialize beta_at_unique a
  7. L52
    apply beta_at_unique
  8. L53
    rewrite hmiddle_left at hentry
  9. L54
    rewrite hmiddle_left at hentry
  10. L55
    exact hentry
13Use earlier factsL56–57

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

  1. L56
    exact htrace_left
  2. L57
    exact hiva
14Establish holdL58–62

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

  1. L58
    have hold : ∃ w. BetaAt(b,c,i,w)Definitions: BetaAt(b,c,i,w)Original native command in the exact edition
  2. L59
    specialize beta_at_exists b
  3. L60
    specialize beta_at_exists c
  4. L61
    specialize beta_at_exists i
  5. L62
    exact beta_at_exists
15Separate the logical casesL63–63

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

  1. L63
    cases hold
16Establish hnew_oldL64–69

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

  1. L64
    have hnew_old : BetaAt(z,d,i,x)Definitions: BetaAt(z,d,i,x)Original native command in the exact edition
  2. L65
    specialize htrace_right_right i
  3. L66
    specialize htrace_right_right x
  4. L67
    apply htrace_right_right
  5. L68
    exact hmiddle_right
  6. L69
    exact hold_witness
17Establish hivxL70–78

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

  1. L70
    have hivx : v = x
  2. L71
    specialize beta_at_unique z
  3. L72
    specialize beta_at_unique d
  4. L73
    specialize beta_at_unique i
  5. L74
    specialize beta_at_unique v
  6. L75
    specialize beta_at_unique x
  7. L76
    apply beta_at_unique
  8. L77
    exact hentry
  9. L78
    exact hnew_old
18Separate the logical casesL79–81

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

  1. L79
    right
  2. L80
    right
  3. L81
    split
19Use earlier factsL82–82

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

  1. L82
    exact hmiddle_right
20Calculate and transport equalitiesL83–84

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

  1. L83
    rewrite <- hivx at hold_witness
  2. L84
    rewrite <- hivx at hold_witness
21Use earlier factsL85–85

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

  1. L85
    exact hold_witness

Library-wide reading audit

Original defined command ledger · 85 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro l
  6. 0006intro a
  7. 0007intro e
  8. 0008intro htrace
  9. 0009cases htrace
  10. 0010cases htrace_right
  11. 0011intro i
  12. 0012intro v
  13. 0013intro hi
  14. 0014intro hentry
  15. 0015have htop : i = S l ∨ Lt(i,S l)
    Exact native replay linehave htop : i = S l \/ exists h. h + S i = S l
  16. 0016specialize finite_lt_succ_eq_or_lt (S l)
  17. 0017specialize finite_lt_succ_eq_or_lt i
  18. 0018apply finite_lt_succ_eq_or_lt
  19. 0019exact hi
  20. 0020cases htop
  21. 0021left
  22. 0022split
  23. 0023exact htop_left
  24. 0024have hive : v = e
  25. 0025specialize beta_at_unique z
  26. 0026specialize beta_at_unique d
  27. 0027specialize beta_at_unique (S l)
  28. 0028specialize beta_at_unique v
  29. 0029specialize beta_at_unique e
  30. 0030apply beta_at_unique
  31. 0031rewrite htop_left at hentry
  32. 0032rewrite htop_left at hentry
  33. 0033exact hentry
  34. 0034exact htrace_right_left
  35. 0035exact hive
  36. 0036have hmiddle : i = l ∨ Lt(i,l)
    Exact native replay linehave hmiddle : i = l \/ exists h. h + S i = l
  37. 0037specialize finite_lt_succ_eq_or_lt l
  38. 0038specialize finite_lt_succ_eq_or_lt i
  39. 0039apply finite_lt_succ_eq_or_lt
  40. 0040exact htop_right
  41. 0041cases hmiddle
  42. 0042right
  43. 0043left
  44. 0044split
  45. 0045exact hmiddle_left
  46. 0046have hiva : v = a
  47. 0047specialize beta_at_unique z
  48. 0048specialize beta_at_unique d
  49. 0049specialize beta_at_unique l
  50. 0050specialize beta_at_unique v
  51. 0051specialize beta_at_unique a
  52. 0052apply beta_at_unique
  53. 0053rewrite hmiddle_left at hentry
  54. 0054rewrite hmiddle_left at hentry
  55. 0055exact hentry
  56. 0056exact htrace_left
  57. 0057exact hiva
  58. 0058have hold : ∃ w. BetaAt(b,c,i,w)
    Exact native replay linehave hold : exists w. (((exists wpo_beta_height_reflect_old_exists_entry. wpo_beta_height_reflect_old_exists_entry + S (w) = S ((S (i)) * c)) /\ exists wpo_beta_quotient_reflect_old_exists_entry. b = wpo_beta_quotient_reflect_old_exists_entry * S ((S (i)) * c) + (w)))
  59. 0059specialize beta_at_exists b
  60. 0060specialize beta_at_exists c
  61. 0061specialize beta_at_exists i
  62. 0062exact beta_at_exists
  63. 0063cases hold
  64. 0064have hnew_old : BetaAt(z,d,i,x)
    Exact native replay linehave hnew_old : ((exists h. h + S x = S ((S i) * d)) /\ exists q. z = q * S ((S i) * d) + x)
  65. 0065specialize htrace_right_right i
  66. 0066specialize htrace_right_right x
  67. 0067apply htrace_right_right
  68. 0068exact hmiddle_right
  69. 0069exact hold_witness
  70. 0070have hivx : v = x
  71. 0071specialize beta_at_unique z
  72. 0072specialize beta_at_unique d
  73. 0073specialize beta_at_unique i
  74. 0074specialize beta_at_unique v
  75. 0075specialize beta_at_unique x
  76. 0076apply beta_at_unique
  77. 0077exact hentry
  78. 0078exact hnew_old
  79. 0079right
  80. 0080right
  81. 0081split
  82. 0082exact hmiddle_right
  83. 0083rewrite <- hivx at hold_witness
  84. 0084rewrite <- hivx at hold_witness
  85. 0085exact hold_witness