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
∀ m. ∀ n. Odd(m + n) → Even(m) ∧ Odd(n) ∨ Odd(m) ∧ Even(n)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
5 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall m n. (exists psc_odd_odd_sum. m + n = 2 * psc_odd_odd_sum + 1) -> ((((exists psc_even_even_m. m = 2 * psc_even_even_m) /\ (exists psc_odd_odd_n. n = 2 * psc_odd_odd_n + 1)) \/ ((exists psc_odd_odd_m. m = 2 * psc_odd_odd_m + 1) /\ (exists psc_even_even_n. n = 2 * psc_even_even_n))))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 (4)
01Fix variables and assumptionsL1–3
02Establish hmL4–6
03Establish hnL7–9
04Separate the logical casesL10–14
05Establish hevenL15–18
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even add even.
06Construct an explicit witnessL19–19
Supply the displayed value, then prove that it has the required property.
- L19
exists x
07Use earlier factsL20–20
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L20
exact hm_witness_left
08Construct an explicit witnessL21–21
Supply the displayed value, then prove that it has the required property.
- L21
exists x1
09Use earlier factsL22–26
10Separate the logical casesL27–28
11Construct an explicit witnessL29–29
Supply the displayed value, then prove that it has the required property.
- L29
exists x
12Use earlier factsL30–30
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L30
exact hm_witness_left
13Construct an explicit witnessL31–31
Supply the displayed value, then prove that it has the required property.
- L31
exists x1
14Use earlier factsL32–32
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L32
exact hn_witness_right
15Separate the logical casesL33–35
16Construct an explicit witnessL36–36
Supply the displayed value, then prove that it has the required property.
- L36
exists x
17Use earlier factsL37–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L37
exact hm_witness_right
18Construct an explicit witnessL38–38
Supply the displayed value, then prove that it has the required property.
- L38
exists x1
19Use earlier factsL39–39
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L39
exact hn_witness_left
20Separate the logical casesL40–40
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L40
exfalso
21Establish hevenL41–44
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd add odd.
22Construct an explicit witnessL45–45
Supply the displayed value, then prove that it has the required property.
- L45
exists x
23Use earlier factsL46–46
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L46
exact hm_witness_right
24Construct an explicit witnessL47–47
Supply the displayed value, then prove that it has the required property.
- L47
exists x1
Original defined command ledger · 52 lines
- 0001
intro m - 0002
intro n - 0003
intro hsum - 0004
have hm : exists a. m = 2 * a \/ m = 2 * a + 1 - 0005
specialize parity_cases m - 0006
exact parity_cases - 0007
have hn : exists b. n = 2 * b \/ n = 2 * b + 1 - 0008
specialize parity_cases n - 0009
exact parity_cases - 0010
cases hm - 0011
cases hn - 0012
cases hm_witness - 0013
cases hn_witness - 0014
exfalso - 0015
have heven : Even(m + n)Exact native replay line
have heven : exists c. m + n = 2 * c - 0016
specialize even_add_even m - 0017
specialize even_add_even n - 0018
apply even_add_even - 0019
exists x - 0020
exact hm_witness_left - 0021
exists x1 - 0022
exact hn_witness_left - 0023
specialize odd_not_even (m + n) - 0024
apply odd_not_even - 0025
exact hsum - 0026
exact heven - 0027
left - 0028
split - 0029
exists x - 0030
exact hm_witness_left - 0031
exists x1 - 0032
exact hn_witness_right - 0033
cases hn_witness - 0034
right - 0035
split - 0036
exists x - 0037
exact hm_witness_right - 0038
exists x1 - 0039
exact hn_witness_left - 0040
exfalso - 0041
have heven : Even(m + n)Exact native replay line
have heven : exists c. m + n = 2 * c - 0042
specialize odd_add_odd m - 0043
specialize odd_add_odd n - 0044
apply odd_add_odd - 0045
exists x - 0046
exact hm_witness_right - 0047
exists x1 - 0048
exact hn_witness_right - 0049
specialize odd_not_even (m + n) - 0050
apply odd_not_even - 0051
exact hsum - 0052
exact heven