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
∀ w. ∃ b. ∃ c. ∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
2 occurrences
In local proof propositions
4 occurrences
Exact expanded native-PA statement
forall w. exists b c. (forall bcf_index_bpzrx_result. (exists bcf_lt_gap_bpzrx_result_bound. bcf_lt_gap_bpzrx_result_bound + S (bcf_index_bpzrx_result) = w) -> exists bcf_value_bpzrx_result. ((((exists bcf_height_bpzrx_result_entry. bcf_height_bpzrx_result_entry + S (bcf_value_bpzrx_result) = S ((S (bcf_index_bpzrx_result)) * c)) /\ exists bcf_quotient_bpzrx_result_entry. b = bcf_quotient_bpzrx_result_entry * S ((S (bcf_index_bpzrx_result)) * c) + (bcf_value_bpzrx_result))) /\ ((bcf_index_bpzrx_result = 0 /\ bcf_value_bpzrx_result = 1) \/ exists bcf_predecessor_bpzrx_result. bcf_index_bpzrx_result = S bcf_predecessor_bpzrx_result /\ bcf_value_bpzrx_result = 0)))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
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 (3)
01Induction on wL1–1
Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.
- L1
induction w
02Construct an explicit witnessL2–3
03Fix variables and assumptionsL4–5
04Separate the logical casesL6–7
05Establish hsiL8–15
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.
06Establish hpreviousL16–17
Establish this local claim before using it. It is not an additional assumption.
- L16
have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))Definitions: Lt(x,w)BetaAt(b,c,x,y)Original native command in the exact edition - L17
exact IH
07Separate the logical casesL18–19
08Establish hnextL20–26
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta pascal zero row extend.
- L20
have hnext : ∃ b. ∃ c. ∀ x. Lt(x,S w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))Definitions: Lt(x,S w)BetaAt(b,c,x,y)Original native command in the exact edition - L21
specialize beta_pascal_zero_row_extend x - L22
specialize beta_pascal_zero_row_extend x1 - L23
specialize beta_pascal_zero_row_extend w - L24
apply beta_pascal_zero_row_extend - L25
exact hprevious_witness_witness - L26
exact hnext
Original defined command ledger · 26 lines
- 0001
induction w - 0002
exists 0 - 0003
exists 0 - 0004
intro i - 0005
intro hi - 0006
exfalso - 0007
cases hi - 0008
have hsi : S i = 0 - 0009
specialize add_eq_zero_right x - 0010
specialize add_eq_zero_right (S i) - 0011
apply add_eq_zero_right - 0012
exact hi_witness - 0013
specialize succ_ne_zero i - 0014
apply succ_ne_zero - 0015
exact hsi - 0016
have hprevious : ∃ b. ∃ c. ∀ x. Lt(x,w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))Exact native replay line
have hprevious : exists b c. (forall bcf_index_bpzrx_previous. (exists bcf_lt_gap_bpzrx_previous_bound. bcf_lt_gap_bpzrx_previous_bound + S (bcf_index_bpzrx_previous) = w) -> exists bcf_value_bpzrx_previous. ((((exists bcf_height_bpzrx_previous_entry. bcf_height_bpzrx_previous_entry + S (bcf_value_bpzrx_previous) = S ((S (bcf_index_bpzrx_previous)) * c)) /\ exists bcf_quotient_bpzrx_previous_entry. b = bcf_quotient_bpzrx_previous_entry * S ((S (bcf_index_bpzrx_previous)) * c) + (bcf_value_bpzrx_previous))) /\ ((bcf_index_bpzrx_previous = 0 /\ bcf_value_bpzrx_previous = 1) \/ exists bcf_predecessor_bpzrx_previous. bcf_index_bpzrx_previous = S bcf_predecessor_bpzrx_previous /\ bcf_value_bpzrx_previous = 0))) - 0017
exact IH - 0018
cases hprevious - 0019
cases hprevious_witness - 0020
have hnext : ∃ b. ∃ c. ∀ x. Lt(x,S w) → ∃ y. BetaAt(b,c,x,y) ∧ (x = 0 ∧ y = 1 ∨ (∃ z. x = S z ∧ y = 0))Exact native replay line
have hnext : exists b c. (forall bcf_index_bpzrx_successor. (exists bcf_lt_gap_bpzrx_successor_bound. bcf_lt_gap_bpzrx_successor_bound + S (bcf_index_bpzrx_successor) = S (w)) -> exists bcf_value_bpzrx_successor. ((((exists bcf_height_bpzrx_successor_entry. bcf_height_bpzrx_successor_entry + S (bcf_value_bpzrx_successor) = S ((S (bcf_index_bpzrx_successor)) * c)) /\ exists bcf_quotient_bpzrx_successor_entry. b = bcf_quotient_bpzrx_successor_entry * S ((S (bcf_index_bpzrx_successor)) * c) + (bcf_value_bpzrx_successor))) /\ ((bcf_index_bpzrx_successor = 0 /\ bcf_value_bpzrx_successor = 1) \/ exists bcf_predecessor_bpzrx_successor. bcf_index_bpzrx_successor = S bcf_predecessor_bpzrx_successor /\ bcf_value_bpzrx_successor = 0))) - 0021
specialize beta_pascal_zero_row_extend x - 0022
specialize beta_pascal_zero_row_extend x1 - 0023
specialize beta_pascal_zero_row_extend w - 0024
apply beta_pascal_zero_row_extend - 0025
exact hprevious_witness_witness - 0026
exact hnext