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. ∀ a. ∀ l. ∀ i. ∀ j. ∀ x. ∀ y. Range(b,c,a,l) → Lt(i,l) → Lt(j,l) → BetaAt(b,c,i,x) → BetaAt(b,c,j,y) → x = y → i = jEvery 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
5 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall b c a l i j x y. (forall ff_i_generic. (exists ff_lt_generic_bound. ff_lt_generic_bound + S ff_i_generic = l) -> (((exists ff_h_generic_decoded. ff_h_generic_decoded + S (a + ff_i_generic) = S ((S (ff_i_generic)) * c)) /\ exists ff_q_generic_decoded. b = ff_q_generic_decoded * S ((S (ff_i_generic)) * c) + (a + ff_i_generic)))) -> (exists gh_lt_generic_i. gh_lt_generic_i + S i = l) -> (exists gh_lt_generic_j. gh_lt_generic_j + S j = l) -> (((exists ff_h_generic_i. ff_h_generic_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_generic_i. b = ff_q_generic_i * S ((S (i)) * c) + (x))) -> (((exists ff_h_generic_j. ff_h_generic_j + S (y) = S ((S (j)) * c)) /\ exists ff_q_generic_j. b = ff_q_generic_j * S ((S (j)) * c) + (y))) -> x = y -> i = jProof 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 (2)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–14
03Establish hxiaL15–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta range entry eq.
04Use earlier factsL25–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
exact hxi
05Establish hyjaL26–35
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta range entry eq.
06Use earlier factsL36–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L36
exact hyj
07Establish haijL37–46
Original defined command ledger · 48 lines
- 0001
intro b - 0002
intro c - 0003
intro a - 0004
intro l - 0005
intro i - 0006
intro j - 0007
intro x - 0008
intro y - 0009
intro hrange - 0010
intro hi - 0011
intro hj - 0012
intro hxi - 0013
intro hyj - 0014
intro hxy - 0015
have hxia : x = a + i - 0016
specialize beta_range_entry_eq b - 0017
specialize beta_range_entry_eq c - 0018
specialize beta_range_entry_eq a - 0019
specialize beta_range_entry_eq l - 0020
specialize beta_range_entry_eq i - 0021
specialize beta_range_entry_eq x - 0022
apply beta_range_entry_eq - 0023
exact hrange - 0024
exact hi - 0025
exact hxi - 0026
have hyja : y = a + j - 0027
specialize beta_range_entry_eq b - 0028
specialize beta_range_entry_eq c - 0029
specialize beta_range_entry_eq a - 0030
specialize beta_range_entry_eq l - 0031
specialize beta_range_entry_eq j - 0032
specialize beta_range_entry_eq y - 0033
apply beta_range_entry_eq - 0034
exact hrange - 0035
exact hj - 0036
exact hyj - 0037
have haij : a + i = a + j - 0038
trans x - 0039
symm - 0040
exact hxia - 0041
trans y - 0042
exact hxy - 0043
exact hyja - 0044
specialize add_left_cancel a - 0045
specialize add_left_cancel i - 0046
specialize add_left_cancel j - 0047
apply add_left_cancel - 0048
exact haij