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. ∀ n. ∀ v. InjectivePrefix(b,c,n) → BetaAt(b,c,n,v) → ¬ContainsPrefix(b,c,n,v) → InjectivePrefix(b,c,S n)Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
Exact expanded first-order statement
forall b c n v. (forall fp_i_fpcd_old fp_j_fpcd_old fp_value_fpcd_old. (exists fp_gap_fpcd_old_i. fp_gap_fpcd_old_i + S fp_i_fpcd_old = n) -> (exists fp_gap_fpcd_old_j. fp_gap_fpcd_old_j + S fp_j_fpcd_old = n) -> (((exists ff_h_fpcd_old_left. ff_h_fpcd_old_left + S (fp_value_fpcd_old) = S ((S (fp_i_fpcd_old)) * c)) /\ exists ff_q_fpcd_old_left. b = ff_q_fpcd_old_left * S ((S (fp_i_fpcd_old)) * c) + (fp_value_fpcd_old))) -> (((exists ff_h_fpcd_old_right. ff_h_fpcd_old_right + S (fp_value_fpcd_old) = S ((S (fp_j_fpcd_old)) * c)) /\ exists ff_q_fpcd_old_right. b = ff_q_fpcd_old_right * S ((S (fp_j_fpcd_old)) * c) + (fp_value_fpcd_old))) -> fp_i_fpcd_old = fp_j_fpcd_old) -> (((exists ff_h_fpcd_last. ff_h_fpcd_last + S (v) = S ((S (n)) * c)) /\ exists ff_q_fpcd_last. b = ff_q_fpcd_last * S ((S (n)) * c) + (v))) -> ~(exists fp_i_fpcd_contains. ((exists fp_gap_fpcd_contains_index. fp_gap_fpcd_contains_index + S fp_i_fpcd_contains = n) /\ (((exists ff_h_fpcd_contains_entry. ff_h_fpcd_contains_entry + S (v) = S ((S (fp_i_fpcd_contains)) * c)) /\ exists ff_q_fpcd_contains_entry. b = ff_q_fpcd_contains_entry * S ((S (fp_i_fpcd_contains)) * c) + (v))))) -> (forall fp_i_fpcd_next fp_j_fpcd_next fp_value_fpcd_next. (exists fp_gap_fpcd_next_i. fp_gap_fpcd_next_i + S fp_i_fpcd_next = S n) -> (exists fp_gap_fpcd_next_j. fp_gap_fpcd_next_j + S fp_j_fpcd_next = S n) -> (((exists ff_h_fpcd_next_left. ff_h_fpcd_next_left + S (fp_value_fpcd_next) = S ((S (fp_i_fpcd_next)) * c)) /\ exists ff_q_fpcd_next_left. b = ff_q_fpcd_next_left * S ((S (fp_i_fpcd_next)) * c) + (fp_value_fpcd_next))) -> (((exists ff_h_fpcd_next_right. ff_h_fpcd_next_right + S (fp_value_fpcd_next) = S ((S (fp_j_fpcd_next)) * c)) /\ exists ff_q_fpcd_next_right. b = ff_q_fpcd_next_right * S ((S (fp_j_fpcd_next)) * c) + (fp_value_fpcd_next))) -> fp_i_fpcd_next = fp_j_fpcd_next)Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay 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.
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–14
03Establish hiL15–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.
04Establish hjL20–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.
05Separate the logical casesL25–26
06Calculate and transport equalitiesL27–27
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L27
trans n
07Use earlier factsL28–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L28
exact hi_left
08Calculate and transport equalitiesL29–29
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L29
symm
09Use earlier factsL30–30
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L30
exact hj_left
10Separate the logical casesL31–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L31
exfalso
11Use earlier factsL32–32
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L32
apply hfresh
12Construct an explicit witnessL33–33
Supply the displayed value, then prove that it has the required property.
- L33
exists j
13Separate the logical casesL34–34
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L34
split
14Use earlier factsL35–35
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L35
exact hj_right
15Establish hsameL36–45
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
16Use earlier factsL46–46
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L46
exact hlast
17Calculate and transport equalitiesL47–48
18Use earlier factsL49–49
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L49
exact hright
19Separate the logical casesL50–51
20Use earlier factsL52–52
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L52
apply hfresh
21Construct an explicit witnessL53–53
Supply the displayed value, then prove that it has the required property.
- L53
exists i
22Separate the logical casesL54–54
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L54
split
23Use earlier factsL55–55
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L55
exact hi_right
24Establish hsameL56–65
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
25Use earlier factsL66–66
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L66
exact hlast
26Calculate and transport equalitiesL67–68
Original defined command ledger · 77 lines
- 0001
intro b - 0002
intro c - 0003
intro n - 0004
intro v - 0005
intro holdinjective - 0006
intro hlast - 0007
intro hfresh - 0008
intro i - 0009
intro j - 0010
intro y - 0011
intro hibound - 0012
intro hjbound - 0013
intro hleft - 0014
intro hright - 0015
have hi : i = n ∨ Lt(i,n)Exact native replay line
have hi : i = n \/ exists gap. gap + S i = n - 0016
specialize finite_lt_succ_eq_or_lt n - 0017
specialize finite_lt_succ_eq_or_lt i - 0018
apply finite_lt_succ_eq_or_lt - 0019
exact hibound - 0020
have hj : j = n ∨ Lt(j,n)Exact native replay line
have hj : j = n \/ exists gap. gap + S j = n - 0021
specialize finite_lt_succ_eq_or_lt n - 0022
specialize finite_lt_succ_eq_or_lt j - 0023
apply finite_lt_succ_eq_or_lt - 0024
exact hjbound - 0025
cases hi - 0026
cases hj - 0027
trans n - 0028
exact hi_left - 0029
symm - 0030
exact hj_left - 0031
exfalso - 0032
apply hfresh - 0033
exists j - 0034
split - 0035
exact hj_right - 0036
have hsame : y = v - 0037
specialize beta_at_unique b - 0038
specialize beta_at_unique c - 0039
specialize beta_at_unique n - 0040
specialize beta_at_unique y - 0041
specialize beta_at_unique v - 0042
apply beta_at_unique - 0043
rewrite hi_left at hleft - 0044
rewrite hi_left at hleft - 0045
exact hleft - 0046
exact hlast - 0047
rewrite hsame at hright - 0048
rewrite hsame at hright - 0049
exact hright - 0050
cases hj - 0051
exfalso - 0052
apply hfresh - 0053
exists i - 0054
split - 0055
exact hi_right - 0056
have hsame : y = v - 0057
specialize beta_at_unique b - 0058
specialize beta_at_unique c - 0059
specialize beta_at_unique n - 0060
specialize beta_at_unique y - 0061
specialize beta_at_unique v - 0062
apply beta_at_unique - 0063
rewrite hj_left at hright - 0064
rewrite hj_left at hright - 0065
exact hright - 0066
exact hlast - 0067
rewrite hsame at hleft - 0068
rewrite hsame at hleft - 0069
exact hleft - 0070
specialize holdinjective i - 0071
specialize holdinjective j - 0072
specialize holdinjective y - 0073
apply holdinjective - 0074
exact hi_right - 0075
exact hj_right - 0076
exact hleft - 0077
exact hright