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
∀ p. ∀ q. ∀ i. ∀ rb. ∀ rc. ∀ l. (∀ x. Lt(x,l) → ∃ y. BetaAt(rb,rc,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))) → (∃ x. x = 0 ∧ (Lt(q · S i,p · S l) ∧ ¬Lt(p · S l,q · S i)) ∨ x = 1 ∧ (Lt(p · S l,q · S i) ∧ ¬Lt(q · S i,p · S l))) → ∃ x. ∃ y. ∀ z. Lt(z,S l) → ∃ n. BetaAt(x,y,z,n) ∧ (n = 0 ∧ (Lt(q · S i,p · S z) ∧ ¬Lt(p · S z,q · S i)) ∨ n = 1 ∧ (Lt(p · S z,q · S i) ∧ ¬Lt(q · S i,p · S z)))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
16 occurrences
In local proof propositions
6 occurrences
Exact expanded native-PA statement
forall p q i rb rc l. (forall eri_column_row_indicator_extend_before. (exists eri_gap_row_indicator_extend_before_bound. eri_gap_row_indicator_extend_before_bound + S (eri_column_row_indicator_extend_before) = l) -> exists eri_bit_row_indicator_extend_before. ((((exists ff_h_eri_row_indicator_extend_before_decoded. ff_h_eri_row_indicator_extend_before_decoded + S (eri_bit_row_indicator_extend_before) = S ((S (eri_column_row_indicator_extend_before)) * rc)) /\ exists ff_q_eri_row_indicator_extend_before_decoded. rb = ff_q_eri_row_indicator_extend_before_decoded * S ((S (eri_column_row_indicator_extend_before)) * rc) + (eri_bit_row_indicator_extend_before))) /\ (((eri_bit_row_indicator_extend_before = 0 /\ ((exists eri_gap_row_indicator_extend_before_choice_left. eri_gap_row_indicator_extend_before_choice_left + S (q * S i) = p * S eri_column_row_indicator_extend_before) /\ ~(exists eri_gap_row_indicator_extend_before_choice_right. eri_gap_row_indicator_extend_before_choice_right + S (p * S eri_column_row_indicator_extend_before) = q * S i))) \/ (eri_bit_row_indicator_extend_before = 1 /\ ((exists eri_gap_row_indicator_extend_before_choice_right. eri_gap_row_indicator_extend_before_choice_right + S (p * S eri_column_row_indicator_extend_before) = q * S i) /\ ~(exists eri_gap_row_indicator_extend_before_choice_left. eri_gap_row_indicator_extend_before_choice_left + S (q * S i) = p * S eri_column_row_indicator_extend_before))))))) -> (exists bit. (((bit = 0 /\ ((exists eri_gap_row_indicator_extend_last_left. eri_gap_row_indicator_extend_last_left + S (q * S i) = p * S l) /\ ~(exists eri_gap_row_indicator_extend_last_right. eri_gap_row_indicator_extend_last_right + S (p * S l) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_indicator_extend_last_right. eri_gap_row_indicator_extend_last_right + S (p * S l) = q * S i) /\ ~(exists eri_gap_row_indicator_extend_last_left. eri_gap_row_indicator_extend_last_left + S (q * S i) = p * S l)))))) -> exists z d. (forall eri_column_row_indicator_extend_after. (exists eri_gap_row_indicator_extend_after_bound. eri_gap_row_indicator_extend_after_bound + S (eri_column_row_indicator_extend_after) = S l) -> exists eri_bit_row_indicator_extend_after. ((((exists ff_h_eri_row_indicator_extend_after_decoded. ff_h_eri_row_indicator_extend_after_decoded + S (eri_bit_row_indicator_extend_after) = S ((S (eri_column_row_indicator_extend_after)) * d)) /\ exists ff_q_eri_row_indicator_extend_after_decoded. z = ff_q_eri_row_indicator_extend_after_decoded * S ((S (eri_column_row_indicator_extend_after)) * d) + (eri_bit_row_indicator_extend_after))) /\ (((eri_bit_row_indicator_extend_after = 0 /\ ((exists eri_gap_row_indicator_extend_after_choice_left. eri_gap_row_indicator_extend_after_choice_left + S (q * S i) = p * S eri_column_row_indicator_extend_after) /\ ~(exists eri_gap_row_indicator_extend_after_choice_right. eri_gap_row_indicator_extend_after_choice_right + S (p * S eri_column_row_indicator_extend_after) = q * S i))) \/ (eri_bit_row_indicator_extend_after = 1 /\ ((exists eri_gap_row_indicator_extend_after_choice_right. eri_gap_row_indicator_extend_after_choice_right + S (p * S eri_column_row_indicator_extend_after) = q * S i) /\ ~(exists eri_gap_row_indicator_extend_after_choice_left. eri_gap_row_indicator_extend_after_choice_left + S (q * S i) = p * S eri_column_row_indicator_extend_after)))))))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 (2)
01Fix variables and assumptionsL1–8
02Separate the logical casesL9–9
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L9
cases hchoice
03Use earlier factsL10–13
04Separate the logical casesL14–16
05Construct an explicit witnessL17–18
06Fix variables and assumptionsL19–20
07Establish hsplitL21–25
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.
08Separate the logical casesL26–26
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L26
cases hsplit
09Construct an explicit witnessL27–27
Supply the displayed value, then prove that it has the required property.
- L27
exists x
10Separate the logical casesL28–28
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L28
split
11Calculate and transport equalitiesL29–30
12Use earlier factsL31–31
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L31
exact beta_prefix_extend_witness_witness_left
13Calculate and transport equalitiesL32–35
14Use earlier factsL36–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L36
exact hchoice_witness
15Establish holdL37–40
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.
- L37
have hold : ∃ oldbit. BetaAt(rb,rc,j,oldbit) ∧ (oldbit = 0 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i)) ∨ oldbit = 1 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)))Definitions: BetaAt(rb,rc,j,oldbit)Lt(q · S i,p · S j)Lt(p · S j,q · S i)Original native command in the exact edition - L38
specialize hprefix j - L39
apply hprefix - L40
exact hsplit_right
16Separate the logical casesL41–42
17Construct an explicit witnessL43–43
Supply the displayed value, then prove that it has the required property.
- L43
exists x3
18Separate the logical casesL44–44
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L44
split
19Use earlier factsL45–50
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 50 lines
- 0001
intro p - 0002
intro q - 0003
intro i - 0004
intro rb - 0005
intro rc - 0006
intro l - 0007
intro hprefix - 0008
intro hchoice - 0009
cases hchoice - 0010
specialize beta_prefix_extend l - 0011
specialize beta_prefix_extend rb - 0012
specialize beta_prefix_extend rc - 0013
specialize beta_prefix_extend x - 0014
cases beta_prefix_extend - 0015
cases beta_prefix_extend_witness - 0016
cases beta_prefix_extend_witness_witness - 0017
exists x1 - 0018
exists x2 - 0019
intro j - 0020
intro hj - 0021
have hsplit : j = l ∨ Lt(j,l)Exact native replay line
have hsplit : j = l \/ exists gap. gap + S j = l - 0022
specialize finite_lt_succ_eq_or_lt l - 0023
specialize finite_lt_succ_eq_or_lt j - 0024
apply finite_lt_succ_eq_or_lt - 0025
exact hj - 0026
cases hsplit - 0027
exists x - 0028
split - 0029
rewrite hsplit_left - 0030
rewrite hsplit_left - 0031
exact beta_prefix_extend_witness_witness_left - 0032
rewrite hsplit_left - 0033
rewrite hsplit_left - 0034
rewrite hsplit_left - 0035
rewrite hsplit_left - 0036
exact hchoice_witness - 0037
have hold : ∃ oldbit. BetaAt(rb,rc,j,oldbit) ∧ (oldbit = 0 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i)) ∨ oldbit = 1 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)))Exact native replay line
have hold : exists oldbit. ((((exists ff_h_row_indicator_extend_old_entry. ff_h_row_indicator_extend_old_entry + S (oldbit) = S ((S (j)) * rc)) /\ exists ff_q_row_indicator_extend_old_entry. rb = ff_q_row_indicator_extend_old_entry * S ((S (j)) * rc) + (oldbit))) /\ (((oldbit = 0 /\ ((exists eri_gap_row_indicator_extend_old_choice_left. eri_gap_row_indicator_extend_old_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_extend_old_choice_right. eri_gap_row_indicator_extend_old_choice_right + S (p * S j) = q * S i))) \/ (oldbit = 1 /\ ((exists eri_gap_row_indicator_extend_old_choice_right. eri_gap_row_indicator_extend_old_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_extend_old_choice_left. eri_gap_row_indicator_extend_old_choice_left + S (q * S i) = p * S j)))))) - 0038
specialize hprefix j - 0039
apply hprefix - 0040
exact hsplit_right - 0041
cases hold - 0042
cases hold_witness - 0043
exists x3 - 0044
split - 0045
specialize beta_prefix_extend_witness_witness_right j - 0046
specialize beta_prefix_extend_witness_witness_right x3 - 0047
apply beta_prefix_extend_witness_witness_right - 0048
exact hsplit_right - 0049
exact hold_witness_left - 0050
exact hold_witness_right