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
∀ r. ∀ s. ∀ l. ∃ z. ∃ d. ∀ i. ∀ j. Lt(i,l) → BetaAt(r,s,i,j) → BetaAt(z,d,i,S j)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
3 occurrences
In local proof propositions
1 occurrences
Exact expanded native-PA statement
forall r s l. exists z d. forall i j. (exists frm_gap_successor_lift_bound. frm_gap_successor_lift_bound + S i = l) -> (((exists ff_h_frm_successor_lift_source. ff_h_frm_successor_lift_source + S (j) = S ((S (i)) * s)) /\ exists ff_q_frm_successor_lift_source. r = ff_q_frm_successor_lift_source * S ((S (i)) * s) + (j))) -> (((exists frm_height_successor_lift_target. frm_height_successor_lift_target + S (S j) = S ((S (i)) * d)) /\ exists frm_quotient_successor_lift_target. z = frm_quotient_successor_lift_target * S ((S (i)) * d) + (S j)))Proof neighborhood
Direct theorem prerequisites
PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique PA002X beta_prefix_extendDirect 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 (6)
01Fix variables and assumptionsL1–2
02Induction on lL3–3
Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.
- L3
induction l
03Construct an explicit witnessL4–5
04Fix variables and assumptionsL6–9
05Separate the logical casesL10–11
06Establish hsiL12–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.
07Separate the logical casesL20–21
08Use earlier factsL22–24
09Separate the logical casesL25–25
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L25
cases beta_at_exists
10Use earlier factsL26–29
11Separate the logical casesL30–32
12Construct an explicit witnessL33–34
13Fix variables and assumptionsL35–38
14Establish hsplitL39–43
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.
15Separate the logical casesL44–44
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L44
cases hsplit
16Establish hjxL45–54
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
17Use earlier factsL55–55
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L55
exact beta_at_exists_witness
18Calculate and transport equalitiesL56–59
19Use earlier factsL60–69
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L60
exact beta_prefix_extend_witness_witness_left - L61
specialize beta_prefix_extend_witness_witness_right i - L62
specialize beta_prefix_extend_witness_witness_right (S j) - L63
apply beta_prefix_extend_witness_witness_right - L64
exact hsplit_right - L65
specialize IH_witness_witness i - L66
specialize IH_witness_witness j - L67
apply IH_witness_witness - L68
exact hsplit_right - L69
exact hsource
Original defined command ledger · 69 lines
- 0001
intro r - 0002
intro s - 0003
induction l - 0004
exists 0 - 0005
exists 0 - 0006
intro i - 0007
intro j - 0008
intro hi - 0009
intro hsource - 0010
exfalso - 0011
cases hi - 0012
have hsi : S i = 0 - 0013
specialize add_eq_zero_right x - 0014
specialize add_eq_zero_right (S i) - 0015
apply add_eq_zero_right - 0016
exact hi_witness - 0017
specialize succ_ne_zero i - 0018
apply succ_ne_zero - 0019
exact hsi - 0020
cases IH - 0021
cases IH_witness - 0022
specialize beta_at_exists r - 0023
specialize beta_at_exists s - 0024
specialize beta_at_exists l - 0025
cases beta_at_exists - 0026
specialize beta_prefix_extend l - 0027
specialize beta_prefix_extend x - 0028
specialize beta_prefix_extend x1 - 0029
specialize beta_prefix_extend (S x2) - 0030
cases beta_prefix_extend - 0031
cases beta_prefix_extend_witness - 0032
cases beta_prefix_extend_witness_witness - 0033
exists x3 - 0034
exists x4 - 0035
intro i - 0036
intro j - 0037
intro hi - 0038
intro hsource - 0039
have hsplit : i = l ∨ Lt(i,l)Exact native replay line
have hsplit : i = l \/ exists h. h + S i = l - 0040
specialize finite_lt_succ_eq_or_lt l - 0041
specialize finite_lt_succ_eq_or_lt i - 0042
apply finite_lt_succ_eq_or_lt - 0043
exact hi - 0044
cases hsplit - 0045
have hjx : j = x2 - 0046
specialize beta_at_unique r - 0047
specialize beta_at_unique s - 0048
specialize beta_at_unique l - 0049
specialize beta_at_unique j - 0050
specialize beta_at_unique x2 - 0051
apply beta_at_unique - 0052
rewrite hsplit_left at hsource - 0053
rewrite hsplit_left at hsource - 0054
exact hsource - 0055
exact beta_at_exists_witness - 0056
rewrite hsplit_left - 0057
rewrite hsplit_left - 0058
rewrite hjx - 0059
rewrite hjx - 0060
exact beta_prefix_extend_witness_witness_left - 0061
specialize beta_prefix_extend_witness_witness_right i - 0062
specialize beta_prefix_extend_witness_witness_right (S j) - 0063
apply beta_prefix_extend_witness_witness_right - 0064
exact hsplit_right - 0065
specialize IH_witness_witness i - 0066
specialize IH_witness_witness j - 0067
apply IH_witness_witness - 0068
exact hsplit_right - 0069
exact hsource