This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| add-base | ⊦ n + 0 = n | An Axiom |
| less-total | ⊦ n < n0 ∨ n = n0 ∨ n0 < n | An Axiom |
| add-rec | ⊦ m + n +1 = (m + n)+1 | An Axiom |
| a | ⊦ (m + n0) + n1 = m + n0 + n1 | A User Theorem |
| addex | ⊦ m < n ↔ (∃ m0. m + m0 = n ∧ m0 ≠ 0) | A User Theorem |
| between | ⊦ m < n → (n < m + 2 ↔ m + 1 = n) | A User Theorem |
| c | ⊦ m + n = n + m | A User Theorem |
| eq | ⊦ m = m + n ↔ n = 0 | A User Theorem |
| eq-01 | ⊦ m + n = m + n0 ↔ n = n0 | A User Theorem |
| eq-inc-neq | ⊦ m = m0 + 1 + n → m ≠ n | A User Theorem |
| eqs | ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1 | A User Theorem |
| even | ⊦ n + n = m + m ↔ n = m | A User Theorem |
| even-01 | ⊦ m + m ≠ 1 | A User Theorem |
| even-02 | ⊦ m + m < n + n ↔ m < n | A User Theorem |
| even-04 | ⊦ m + m ≠ 3 | A User Theorem |
| even-05 | ⊦ m + m = (m0 + m0) + n → ¬ m < m0 | A User Theorem |
| even-06 | ⊦ m + m ≠ n + n + 1 | A User Theorem |
| ex-oddeven | ⊦ ∃ m. m + m = n ∨ m + m + 1 = n | A User Theorem |
| expand-nat | ⊦ n < n1 → n + m < n1 + m | A User Theorem |
| k-two | ⊦ 2 = 1 +1 | A User Theorem |
| l | ⊦ m + n < m + n0 ↔ n < n0 | A User Theorem |
| l-01 | ⊦ m < m + n ↔ n ≠ 0 | A User Theorem |
| l-02 | ⊦ ¬ m + n < m | A User Theorem |
| l-03 | ⊦ m < m0 ∧ n < n0 → (¬ m + n < m0 + n0 ↔ false) | A User Theorem |
| l-04 | ⊦ m + m0 < n + n0 → (¬ m + m0 < n + n0 ↔ false) | A User Theorem |
| l-05 | ⊦ m + m0 < n → ¬ n + n0 < m | A User Theorem |
| l-06 | ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m | A User Theorem |
| l-07 | ⊦ m = m0 + n0 ∧ n < n0 → ¬ m < m0 + n | A User Theorem |
| l-08 | ⊦ m + n < m0 → m + n < m0 + n0 | A User Theorem |
| l-addone | ⊦ n < n + 1 | A User Theorem |
| less | ¬ m0 < n0, n < m ⊦ n + n0 < m + m0 | A User Theorem |
| less-01 | ¬ n0 < n, ¬ n + m < m0 ⊦ ¬ n0 + m < m0 | A User Theorem |
| less-02 | ⊦ ¬ n0 + n1 + n2 < m ∧ ¬ n < n2 → ¬ n0 + n1 + n < m | A User Theorem |
| less-03 | ¬ m0 < n1, n + n0 < m ⊦ n + n0 + n1 < m + m0 | A User Theorem |
| less-04 | m + m0 < n + n0, ¬ m < n ⊦ m0 < n0 | A User Theorem |
| less-05 | m < m0, ¬ n0 < n ⊦ m + n < m0 + n0 | A User Theorem |
| less-06 | m + n < m0, n0 < n ⊦ m + n0 < m0 | A User Theorem |
| lp | ⊦ m ≠ 0 → (m + n < m -1 ↔ false) | A User Theorem |
| ls | ⊦ (m + n)+1 < m + n0 ↔ n +1 < n0 | A User Theorem |
| lsls | ⊦ n + m < m0 → ¬ n0 + m0 < m | A User Theorem |
| neq | ⊦ m < m0 ∧ n0 < n + m → n0 + 1 ≠ n + m0 | A User Theorem |
| neq-01 | ⊦ m ≠ n → (m < n + 1 ↔ m < n) | A User Theorem |
| neq-02 | ⊦ m < m0 ∧ n0 < n → m + n0 + 1 ≠ n + m0 | A User Theorem |
| nls-fst | ⊦ ¬ m < n → ¬ m + m0 < n | A User Theorem |
| nls-snd | ⊦ ¬ m0 < n → ¬ m + m0 < n | A User Theorem |
| one | ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1 | A User Theorem |
| one-01 | ⊦ n ≠ 0 → (m + n = 1 ↔ n = 1 ∧ m = 0) | A User Theorem |
| one-02 | ⊦ m ≠ 1 → (m + n = 1 ↔ m = 0 ∧ n = 1) | A User Theorem |
| one-03 | ⊦ 1 = m + 1 ↔ m = 0 | A User Theorem |
| one-def | ⊦ 1 = 0 +1 | A User Theorem |
| oz | ⊦ m + 1 ≠ 0 | A User Theorem |
| pe | ⊦ n ≠ 0 → m + n -1 = (m + n)-1 | A User Theorem |
| pe-01 | ⊦ m0 < m → n0 + (m + n)-1 = ((n0 + m) + n)-1 | A User Theorem |
| pls | m < m0, n < n0 ⊦ m + n + 1 < m0 + n0 | A User Theorem |
| pred | ⊦ (m + 1)-1 = m | A User Theorem |
| ps | ⊦ m ≠ 0 → (m + n)-1 +1 = m + n | A User Theorem |
| pse | ⊦ n ≠ 0 ∧ n ≠ 1 → m + n -1 -1 = (m + n)-1 -1 | A User Theorem |
| q | ⊦ ∃ n. m = n + n ∨ m = (n + n)+1 | A User Theorem |
| q-01 | ¬ n < m ⊦ ∃ m0. m + m0 = n | A User Theorem |
| rec | ⊦ m +1 + n = (m + n)+1 | A User Theorem |
| s | ⊦ m < n + 1 ↔ ¬ n < m | A User Theorem |
| succ | ⊦ m +1 = m + 1 | A User Theorem |
| succ-03 | ⊦ m < n ∧ m + 1 ≠ n → m + 1 < n | A User Theorem |
| three | ⊦ m ≠ 0 ∧ n ≠ 0 ∧ m ≠ 1 → (m + n = 3 ↔ m = 2 ∧ n = 1) | A User Theorem |
| two | ⊦ m + m = 2 ↔ m = 1 | A User Theorem |
| two-01 | ⊦ m ≠ 0 ∧ n ≠ 0 → (m + n = 2 ↔ m = 1 ∧ n = 1) | A User Theorem |
| two-02 | ⊦ m + m + m ≠ 2 | A User Theorem |
| twols | ⊦ m < n → (m + n < 2 ↔ m = 0 ∧ n = 1) | A User Theorem |
| z | ⊦ 0 + m = m | A User Theorem |
| z-01 | ⊦ m + n = 0 ↔ m = 0 ∧ n = 0 | A User Theorem |
| zero-neq-one | ⊦ 0 ≠ 1 | A User Theorem |