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.
Exact expanded PA statement
forall a b. a = b \/ ~(a = b)Structural proof guide
Generated structural guide
Equality of natural numbers is constructively decidable.
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by structural induction (3), case analysis (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
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–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro a
02Induction on aL2–3
03Induction on bL4–4
Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.
- L4
induction b
04Separate the logical casesL5–5
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L5
left
05Calculate and transport equalitiesL6–6
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L6
refl
06Separate the logical casesL7–7
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L7
right
07Fix variables and assumptionsL8–8
Work with arbitrary variables or the premises of the current implication.
- L8
intro h
08Use earlier factsL9–9
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
apply PA1
09Calculate and transport equalitiesL10–10
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L10
symm
10Use earlier factsL11–11
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L11
exact h
11Fix variables and assumptionsL12–12
Work with arbitrary variables or the premises of the current implication.
- L12
intro b
12Induction on bL13–13
Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.
- L13
induction b
13Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
right
14Fix variables and assumptionsL15–15
Work with arbitrary variables or the premises of the current implication.
- L15
intro h
15Use earlier factsL16–18
16Separate the logical casesL19–20
17Calculate and transport equalitiesL21–21
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L21
congr
18Use earlier factsL22–22
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L22
exact IH_left
19Separate the logical casesL23–23
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L23
right
20Fix variables and assumptionsL24–24
Work with arbitrary variables or the premises of the current implication.
- L24
intro h
Original exact command ledger · 27 lines
- 0001
intro a - 0002
induction a - 0003
intro b - 0004
induction b - 0005
left - 0006
refl - 0007
right - 0008
intro h - 0009
apply PA1 - 0010
symm - 0011
exact h - 0012
intro b - 0013
induction b - 0014
right - 0015
intro h - 0016
apply PA1 - 0017
exact h - 0018
specialize IH b - 0019
cases IH - 0020
left - 0021
congr - 0022
exact IH_left - 0023
right - 0024
intro h - 0025
apply IH_right - 0026
apply PA2 - 0027
exact h