PA00AU

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.

Exact expanded 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)))

Structural proof guide

Generated structural guide

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

Use the direct prerequisites beta_prefix_append_two_reflect as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (2), equality transport (4).

Referenced ingredients

PA009L beta_prefix_append_two_reflect

Proof neighborhood

Direct dependencies

PA009L beta_prefix_append_two_reflect

Direct dependents

PA00AV prime_pair_order_choose_append

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

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.

Named ingredients (1)
beta prefix append two reflect

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 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: LtBetaAt
  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) \/ ((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))))))
  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 exact 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 : 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) \/ ((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