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
∀ u. ∀ v. ∀ b. ∀ c. ∀ l. (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,y,z) → ContainsPrefix(b,c,l,z)) ∧ ((∀ x. Lt(x,l) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,S S l)) ∧ ((∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → ¬y = 0 ∧ ¬S y = S S l) ∧ InjectivePrefix(b,c,l))) → ∀ x. Lt(x,S S l) → ¬x = 0 ∧ ¬S x = S S l → ContainsPrefix(b,c,l,x)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
12 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall u v b c l. (((forall wpo_position_wpoi_terminal_state_closed wpo_source_wpoi_terminal_state_closed wpo_mate_wpoi_terminal_state_closed. (exists wpo_gap_wpoi_terminal_state_closed_position_bound. wpo_gap_wpoi_terminal_state_closed_position_bound + S (wpo_position_wpoi_terminal_state_closed) = l) -> (((exists wpo_beta_height_wpoi_terminal_state_closed_source_entry. wpo_beta_height_wpoi_terminal_state_closed_source_entry + S (wpo_source_wpoi_terminal_state_closed) = S ((S (wpo_position_wpoi_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_closed_source_entry. b = wpo_beta_quotient_wpoi_terminal_state_closed_source_entry * S ((S (wpo_position_wpoi_terminal_state_closed)) * c) + (wpo_source_wpoi_terminal_state_closed))) -> (((exists wpo_beta_height_wpoi_terminal_state_closed_inverse_entry. wpo_beta_height_wpoi_terminal_state_closed_inverse_entry + S (wpo_mate_wpoi_terminal_state_closed) = S ((S (wpo_source_wpoi_terminal_state_closed)) * v)) /\ exists wpo_beta_quotient_wpoi_terminal_state_closed_inverse_entry. u = wpo_beta_quotient_wpoi_terminal_state_closed_inverse_entry * S ((S (wpo_source_wpoi_terminal_state_closed)) * v) + (wpo_mate_wpoi_terminal_state_closed))) -> exists wpo_mate_position_wpoi_terminal_state_closed. ((exists wpo_gap_wpoi_terminal_state_closed_mate_bound. wpo_gap_wpoi_terminal_state_closed_mate_bound + S (wpo_mate_position_wpoi_terminal_state_closed) = l) /\ (((exists wpo_beta_height_wpoi_terminal_state_closed_mate_entry. wpo_beta_height_wpoi_terminal_state_closed_mate_entry + S (wpo_mate_wpoi_terminal_state_closed) = S ((S (wpo_mate_position_wpoi_terminal_state_closed)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_closed_mate_entry. b = wpo_beta_quotient_wpoi_terminal_state_closed_mate_entry * S ((S (wpo_mate_position_wpoi_terminal_state_closed)) * c) + (wpo_mate_wpoi_terminal_state_closed))))) /\ ((forall fom_index_wpoi_terminal_state_bounded. (exists fom_gap_wpoi_terminal_state_bounded_index_bound. fom_gap_wpoi_terminal_state_bounded_index_bound + S (fom_index_wpoi_terminal_state_bounded) = l) -> exists fom_value_wpoi_terminal_state_bounded. ((((exists fom_beta_height_wpoi_terminal_state_bounded_entry. fom_beta_height_wpoi_terminal_state_bounded_entry + S (fom_value_wpoi_terminal_state_bounded) = S ((S (fom_index_wpoi_terminal_state_bounded)) * c)) /\ exists fom_beta_quotient_wpoi_terminal_state_bounded_entry. b = fom_beta_quotient_wpoi_terminal_state_bounded_entry * S ((S (fom_index_wpoi_terminal_state_bounded)) * c) + (fom_value_wpoi_terminal_state_bounded))) /\ (exists fom_gap_wpoi_terminal_state_bounded_value_bound. fom_gap_wpoi_terminal_state_bounded_value_bound + S (fom_value_wpoi_terminal_state_bounded) = S (S l)))) /\ ((forall wpo_position_wpoi_terminal_state_nonendpoint wpo_value_wpoi_terminal_state_nonendpoint. (exists wpo_gap_wpoi_terminal_state_nonendpoint_position_bound. wpo_gap_wpoi_terminal_state_nonendpoint_position_bound + S (wpo_position_wpoi_terminal_state_nonendpoint) = l) -> (((exists wpo_beta_height_wpoi_terminal_state_nonendpoint_entry. wpo_beta_height_wpoi_terminal_state_nonendpoint_entry + S (wpo_value_wpoi_terminal_state_nonendpoint) = S ((S (wpo_position_wpoi_terminal_state_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_nonendpoint_entry. b = wpo_beta_quotient_wpoi_terminal_state_nonendpoint_entry * S ((S (wpo_position_wpoi_terminal_state_nonendpoint)) * c) + (wpo_value_wpoi_terminal_state_nonendpoint))) -> (~(wpo_value_wpoi_terminal_state_nonendpoint = 0) /\ ~((S wpo_value_wpoi_terminal_state_nonendpoint) = S (S l)))) /\ (forall wpo_injective_left_wpoi_terminal_state_injective wpo_injective_right_wpoi_terminal_state_injective wpo_injective_value_wpoi_terminal_state_injective. (exists wpo_gap_wpoi_terminal_state_injective_left_bound. wpo_gap_wpoi_terminal_state_injective_left_bound + S (wpo_injective_left_wpoi_terminal_state_injective) = l) -> (exists wpo_gap_wpoi_terminal_state_injective_right_bound. wpo_gap_wpoi_terminal_state_injective_right_bound + S (wpo_injective_right_wpoi_terminal_state_injective) = l) -> (((exists wpo_beta_height_wpoi_terminal_state_injective_left_entry. wpo_beta_height_wpoi_terminal_state_injective_left_entry + S (wpo_injective_value_wpoi_terminal_state_injective) = S ((S (wpo_injective_left_wpoi_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_injective_left_entry. b = wpo_beta_quotient_wpoi_terminal_state_injective_left_entry * S ((S (wpo_injective_left_wpoi_terminal_state_injective)) * c) + (wpo_injective_value_wpoi_terminal_state_injective))) -> (((exists wpo_beta_height_wpoi_terminal_state_injective_right_entry. wpo_beta_height_wpoi_terminal_state_injective_right_entry + S (wpo_injective_value_wpoi_terminal_state_injective) = S ((S (wpo_injective_right_wpoi_terminal_state_injective)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_state_injective_right_entry. b = wpo_beta_quotient_wpoi_terminal_state_injective_right_entry * S ((S (wpo_injective_right_wpoi_terminal_state_injective)) * c) + (wpo_injective_value_wpoi_terminal_state_injective))) -> wpo_injective_left_wpoi_terminal_state_injective = wpo_injective_right_wpoi_terminal_state_injective))))) -> forall s. (exists wpo_gap_wpoi_terminal_value_bound. wpo_gap_wpoi_terminal_value_bound + S (s) = S (S l)) -> (~(s = 0) /\ ~((S s) = S (S l))) -> (exists q. ((exists wpo_gap_wpoi_terminal_index_bound. wpo_gap_wpoi_terminal_index_bound + S (q) = l) /\ (((exists wpo_beta_height_wpoi_terminal_entry. wpo_beta_height_wpoi_terminal_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_entry. b = wpo_beta_quotient_wpoi_terminal_entry * S ((S (q)) * c) + (s)))))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
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
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)
01Fix variables and assumptionsL1–6
02Separate the logical casesL7–9
03Establish hall_coverageL10–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bounded nonendpoint injective coverage.
- L10
have hall_coverage : ∀ s. Lt(s,S S l) → ¬s = 0 ∧ ¬S s = S S l → ContainsPrefix(b,c,l,s)Definitions: Lt(s,S S l)ContainsPrefix(b,c,l,s)Original native command in the exact edition - L11
specialize finite_bounded_nonendpoint_injective_coverage b - L12
specialize finite_bounded_nonendpoint_injective_coverage c - L13
specialize finite_bounded_nonendpoint_injective_coverage l - L14
apply finite_bounded_nonendpoint_injective_coverage - L15
exact hstate_right_left - L16
exact hstate_right_right_left - L17
exact hstate_right_right_right - L18
intro s - L19
intro hsbound
04Fix variables and assumptionsL20–20
Work with arbitrary variables or the premises of the current implication.
- L20
intro hsendpoints
Original defined command ledger · 24 lines
- 0001
intro u - 0002
intro v - 0003
intro b - 0004
intro c - 0005
intro l - 0006
intro hstate - 0007
cases hstate - 0008
cases hstate_right - 0009
cases hstate_right_right - 0010
have hall_coverage : ∀ s. Lt(s,S S l) → ¬s = 0 ∧ ¬S s = S S l → ContainsPrefix(b,c,l,s)Exact native replay line
have hall_coverage : forall s. (exists wpo_gap_wpoi_terminal_value_bound. wpo_gap_wpoi_terminal_value_bound + S (s) = S (S l)) -> (~(s = 0) /\ ~((S s) = S (S l))) -> (exists q. ((exists wpo_gap_wpoi_terminal_index_bound. wpo_gap_wpoi_terminal_index_bound + S (q) = l) /\ (((exists wpo_beta_height_wpoi_terminal_entry. wpo_beta_height_wpoi_terminal_entry + S (s) = S ((S (q)) * c)) /\ exists wpo_beta_quotient_wpoi_terminal_entry. b = wpo_beta_quotient_wpoi_terminal_entry * S ((S (q)) * c) + (s))))) - 0011
specialize finite_bounded_nonendpoint_injective_coverage b - 0012
specialize finite_bounded_nonendpoint_injective_coverage c - 0013
specialize finite_bounded_nonendpoint_injective_coverage l - 0014
apply finite_bounded_nonendpoint_injective_coverage - 0015
exact hstate_right_left - 0016
exact hstate_right_right_left - 0017
exact hstate_right_right_right - 0018
intro s - 0019
intro hsbound - 0020
intro hsendpoints - 0021
specialize hall_coverage s - 0022
apply hall_coverage - 0023
exact hsbound - 0024
exact hsendpoints