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. Even(m + n) → Even(m) ∧ Even(n) ∨ Odd(m) ∧ Odd(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_even_even_sum. m + n = 2 * psc_even_even_sum) -> ((((exists psc_even_even_m. m = 2 * psc_even_even_m) /\ (exists psc_even_even_n. n = 2 * psc_even_even_n)) \/ ((exists psc_odd_odd_m. m = 2 * psc_odd_odd_m + 1) /\ (exists psc_odd_odd_n. n = 2 * psc_odd_odd_n + 1))))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–15
05Construct an explicit witnessL16–16
Supply the displayed value, then prove that it has the required property.
- L16
exists x
06Use earlier factsL17–17
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L17
exact hm_witness_left
07Construct an explicit witnessL18–18
Supply the displayed value, then prove that it has the required property.
- L18
exists x1
08Use earlier factsL19–19
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L19
exact hn_witness_left
09Separate the logical casesL20–20
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L20
exfalso
10Establish hoddL21–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even add odd.
11Construct an explicit witnessL25–25
Supply the displayed value, then prove that it has the required property.
- L25
exists x
12Use earlier factsL26–26
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L26
exact hm_witness_left
13Construct an explicit witnessL27–27
Supply the displayed value, then prove that it has the required property.
- L27
exists x1
14Use earlier factsL28–32
15Separate the logical casesL33–34
16Establish hoddL35–38
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd add even.
17Construct an explicit witnessL39–39
Supply the displayed value, then prove that it has the required property.
- L39
exists x
18Use earlier factsL40–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L40
exact hm_witness_right
19Construct an explicit witnessL41–41
Supply the displayed value, then prove that it has the required property.
- L41
exists x1
20Use earlier factsL42–46
21Separate the logical casesL47–48
22Construct an explicit witnessL49–49
Supply the displayed value, then prove that it has the required property.
- L49
exists x
23Use earlier factsL50–50
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L50
exact hm_witness_right
24Construct an explicit witnessL51–51
Supply the displayed value, then prove that it has the required property.
- L51
exists x1
25Use earlier factsL52–52
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L52
exact hn_witness_right
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
left - 0015
split - 0016
exists x - 0017
exact hm_witness_left - 0018
exists x1 - 0019
exact hn_witness_left - 0020
exfalso - 0021
have hodd : Odd(m + n)Exact native replay line
have hodd : exists c. m + n = 2 * c + 1 - 0022
specialize even_add_odd m - 0023
specialize even_add_odd n - 0024
apply even_add_odd - 0025
exists x - 0026
exact hm_witness_left - 0027
exists x1 - 0028
exact hn_witness_right - 0029
specialize even_not_odd (m + n) - 0030
apply even_not_odd - 0031
exact hsum - 0032
exact hodd - 0033
cases hn_witness - 0034
exfalso - 0035
have hodd : Odd(m + n)Exact native replay line
have hodd : exists c. m + n = 2 * c + 1 - 0036
specialize odd_add_even m - 0037
specialize odd_add_even n - 0038
apply odd_add_even - 0039
exists x - 0040
exact hm_witness_right - 0041
exists x1 - 0042
exact hn_witness_left - 0043
specialize even_not_odd (m + n) - 0044
apply even_not_odd - 0045
exact hsum - 0046
exact hodd - 0047
right - 0048
split - 0049
exists x - 0050
exact hm_witness_right - 0051
exists x1 - 0052
exact hn_witness_right