PA00AU · theorem

beta_prefix_append_two_nonendpoint

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

A two-entry append preserves the nonendpoint invariant when both appended values satisfy it.

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

9 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

6 occurrences

Exact expanded native-PA statement
forall b c z d l n a e. (((((exists wpo_beta_height_nonendpoint_trace_first. wpo_beta_height_nonendpoint_trace_first + S (a) = S ((S (l)) * d)) /\ exists wpo_beta_quotient_nonendpoint_trace_first. z = wpo_beta_quotient_nonendpoint_trace_first * S ((S (l)) * d) + (a))) /\ ((((exists wpo_beta_height_nonendpoint_trace_second. wpo_beta_height_nonendpoint_trace_second + S (e) = S ((S (S (l))) * d)) /\ exists wpo_beta_quotient_nonendpoint_trace_second. z = wpo_beta_quotient_nonendpoint_trace_second * S ((S (S (l))) * d) + (e))) /\ (forall wpo_old_index_nonendpoint_trace wpo_old_value_nonendpoint_trace. (exists wpo_gap_nonendpoint_trace_old_bound. wpo_gap_nonendpoint_trace_old_bound + S (wpo_old_index_nonendpoint_trace) = l) -> (((exists wpo_beta_height_nonendpoint_trace_old_entry. wpo_beta_height_nonendpoint_trace_old_entry + S (wpo_old_value_nonendpoint_trace) = S ((S (wpo_old_index_nonendpoint_trace)) * c)) /\ exists wpo_beta_quotient_nonendpoint_trace_old_entry. b = wpo_beta_quotient_nonendpoint_trace_old_entry * S ((S (wpo_old_index_nonendpoint_trace)) * c) + (wpo_old_value_nonendpoint_trace))) -> (((exists wpo_beta_height_nonendpoint_trace_new_entry. wpo_beta_height_nonendpoint_trace_new_entry + S (wpo_old_value_nonendpoint_trace) = S ((S (wpo_old_index_nonendpoint_trace)) * d)) /\ exists wpo_beta_quotient_nonendpoint_trace_new_entry. z = wpo_beta_quotient_nonendpoint_trace_new_entry * S ((S (wpo_old_index_nonendpoint_trace)) * d) + (wpo_old_value_nonendpoint_trace))))))) -> (forall wpo_position_nonendpoint_before wpo_value_nonendpoint_before. (exists wpo_gap_nonendpoint_before_position_bound. wpo_gap_nonendpoint_before_position_bound + S (wpo_position_nonendpoint_before) = l) -> (((exists wpo_beta_height_nonendpoint_before_entry. wpo_beta_height_nonendpoint_before_entry + S (wpo_value_nonendpoint_before) = S ((S (wpo_position_nonendpoint_before)) * c)) /\ exists wpo_beta_quotient_nonendpoint_before_entry. b = wpo_beta_quotient_nonendpoint_before_entry * S ((S (wpo_position_nonendpoint_before)) * c) + (wpo_value_nonendpoint_before))) -> (~(wpo_value_nonendpoint_before = 0) /\ ~((S wpo_value_nonendpoint_before) = n))) -> ((~(a = 0) /\ ~((S a) = n))) -> ((~(e = 0) /\ ~((S e) = n))) -> (forall wpo_position_nonendpoint_after wpo_value_nonendpoint_after. (exists wpo_gap_nonendpoint_after_position_bound. wpo_gap_nonendpoint_after_position_bound + S (wpo_position_nonendpoint_after) = S (S l)) -> (((exists wpo_beta_height_nonendpoint_after_entry. wpo_beta_height_nonendpoint_after_entry + S (wpo_value_nonendpoint_after) = S ((S (wpo_position_nonendpoint_after)) * d)) /\ exists wpo_beta_quotient_nonendpoint_after_entry. z = wpo_beta_quotient_nonendpoint_after_entry * S ((S (wpo_position_nonendpoint_after)) * d) + (wpo_value_nonendpoint_after))) -> (~(wpo_value_nonendpoint_after = 0) /\ ~((S wpo_value_nonendpoint_after) = n)))

Proof neighborhood

Direct theorem prerequisites

PA009L beta_prefix_append_two_reflect

Direct theorem dependents

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

48 script commands · 12 reading checkpoints · 2 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)
beta prefix append two reflect
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_nonendpoint
02Fix variables and assumptionsL11–16

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

  1. L11
    intro hfirst_nonendpoint
  2. L12
    intro hsecond_nonendpoint
  3. L13
    intro q
  4. L14
    intro s
  5. L15
    intro hq
  6. L16
    intro hentry
03Establish hreflect_allL17–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta prefix append two reflect.

  1. L17
    have hreflect_all : ∀ q. ∀ s. Lt(q,S S l) → BetaAt(z,d,q,s) → q = S l ∧ s = e ∨ (q = l ∧ s = a ∨ Lt(q,l) ∧ BetaAt(b,c,q,s))Definitions: Lt(q,S S l)BetaAt(z,d,q,s)Lt(q,l)BetaAt(b,c,q,s)Original native command in the exact edition
  2. L18
    specialize beta_prefix_append_two_reflect b
  3. L19
    specialize beta_prefix_append_two_reflect c
  4. L20
    specialize beta_prefix_append_two_reflect z
  5. L21
    specialize beta_prefix_append_two_reflect d
  6. L22
    specialize beta_prefix_append_two_reflect l
  7. L23
    specialize beta_prefix_append_two_reflect a
  8. L24
    specialize beta_prefix_append_two_reflect e
  9. L25
    apply beta_prefix_append_two_reflect
  10. L26
    exact htrace
04Establish hreflectL27–32

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

  1. L27
    have hreflect : q = S l ∧ s = e ∨ (q = l ∧ s = a ∨ Lt(q,l) ∧ BetaAt(b,c,q,s))Definitions: Lt(q,l)BetaAt(b,c,q,s)Original native command in the exact edition
  2. L28
    specialize hreflect_all q
  3. L29
    specialize hreflect_all s
  4. L30
    apply hreflect_all
  5. L31
    exact hq
  6. L32
    exact hentry
05Separate the logical casesL33–34

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

  1. L33
    cases hreflect
  2. L34
    cases hreflect_left
06Calculate and transport equalitiesL35–36

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

  1. L35
    rewrite hreflect_left_right
  2. L36
    rewrite hreflect_left_right
07Use earlier factsL37–37

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

  1. L37
    exact hsecond_nonendpoint
08Separate the logical casesL38–39

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

  1. L38
    cases hreflect_right
  2. L39
    cases hreflect_right_left
09Calculate and transport equalitiesL40–41

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

  1. L40
    rewrite hreflect_right_left_right
  2. L41
    rewrite hreflect_right_left_right
10Use earlier factsL42–42

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

  1. L42
    exact hfirst_nonendpoint
11Separate the logical casesL43–43

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

  1. L43
    cases hreflect_right_right
12Use earlier factsL44–48

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

  1. L44
    specialize hold_nonendpoint q
  2. L45
    specialize hold_nonendpoint s
  3. L46
    apply hold_nonendpoint
  4. L47
    exact hreflect_right_right_left
  5. L48
    exact hreflect_right_right_right

Library-wide reading audit

Original defined command ledger · 48 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_nonendpoint
  11. 0011intro hfirst_nonendpoint
  12. 0012intro hsecond_nonendpoint
  13. 0013intro q
  14. 0014intro s
  15. 0015intro hq
  16. 0016intro hentry
  17. 0017have hreflect_all : ∀ q. ∀ s. Lt(q,S S l) → BetaAt(z,d,q,s) → q = S l ∧ s = e ∨ (q = l ∧ s = a ∨ Lt(q,l) ∧ BetaAt(b,c,q,s))
    Exact native replay linehave hreflect_all : forall q s. (exists wpo_gap_nonendpoint_reflection_bound. wpo_gap_nonendpoint_reflection_bound + S (q) = S (S l)) -> (((exists wpo_beta_height_nonendpoint_reflection_entry. wpo_beta_height_nonendpoint_reflection_entry + S (s) = S ((S (q)) * d)) /\ exists wpo_beta_quotient_nonendpoint_reflection_entry. z = wpo_beta_quotient_nonendpoint_reflection_entry * S ((S (q)) * d) + (s))) -> (((q = S (l) /\ s = e) \/ ((q = l /\ s = a) \/ ((exists wpo_gap_nonendpoint_reflection_old_bound. wpo_gap_nonendpoint_reflection_old_bound + S (q) = l) /\ (((exists wpo_beta_height_nonendpoint_reflection_old_entry. wpo_beta_height_nonendpoint_reflection_old_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_nonendpoint_reflection_old_entry. b = wpo_beta_quotient_nonendpoint_reflection_old_entry * S ((S (q)) * c) + (s)))))))
  18. 0018specialize beta_prefix_append_two_reflect b
  19. 0019specialize beta_prefix_append_two_reflect c
  20. 0020specialize beta_prefix_append_two_reflect z
  21. 0021specialize beta_prefix_append_two_reflect d
  22. 0022specialize beta_prefix_append_two_reflect l
  23. 0023specialize beta_prefix_append_two_reflect a
  24. 0024specialize beta_prefix_append_two_reflect e
  25. 0025apply beta_prefix_append_two_reflect
  26. 0026exact htrace
  27. 0027have hreflect : q = S l ∧ s = e ∨ (q = l ∧ s = a ∨ Lt(q,l) ∧ BetaAt(b,c,q,s))
    Exact native replay linehave hreflect : ((q = S (l) /\ s = e) \/ ((q = l /\ s = a) \/ ((exists wpo_gap_nonendpoint_reflection_old_bound. wpo_gap_nonendpoint_reflection_old_bound + S (q) = l) /\ (((exists wpo_beta_height_nonendpoint_reflection_old_entry. wpo_beta_height_nonendpoint_reflection_old_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_nonendpoint_reflection_old_entry. b = wpo_beta_quotient_nonendpoint_reflection_old_entry * S ((S (q)) * c) + (s))))))
  28. 0028specialize hreflect_all q
  29. 0029specialize hreflect_all s
  30. 0030apply hreflect_all
  31. 0031exact hq
  32. 0032exact hentry
  33. 0033cases hreflect
  34. 0034cases hreflect_left
  35. 0035rewrite hreflect_left_right
  36. 0036rewrite hreflect_left_right
  37. 0037exact hsecond_nonendpoint
  38. 0038cases hreflect_right
  39. 0039cases hreflect_right_left
  40. 0040rewrite hreflect_right_left_right
  41. 0041rewrite hreflect_right_left_right
  42. 0042exact hfirst_nonendpoint
  43. 0043cases hreflect_right_right
  44. 0044specialize hold_nonendpoint q
  45. 0045specialize hold_nonendpoint s
  46. 0046apply hold_nonendpoint
  47. 0047exact hreflect_right_right_left
  48. 0048exact hreflect_right_right_right