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: |
|---|---|---|
| less-2 | ⊦ n0 < n +1 ↔ n0 = n ∨ n0 < n | An Axiom |
| less-1 | ⊦ ¬ n < 0 | An Axiom |
| trans-1 | ⊦ n < n0 ∧ n0 < n1 → n < n1 | An Axiom |
| ref-1 | ⊦ ¬ n < n | An Axiom |
| case-1 | ⊦ n = 0 ∨ n = n -1 +1 | An Axiom |
| disj-1 | ⊦ 0 ≠ n +1 | An Axiom |
| inj-1 | ⊦ n +1 = n0 +1 ↔ n = n0 | An Axiom |
| sel-1 | ⊦ n +1 -1 = n | An Axiom |
| elim-1 | ⊦ n ≠ 0 → (n0 = n -1 ↔ n = n0 +1) | An Axiom |
| noeth | < wellfounded | An Axiom |
| gen | nat freely generated by 0, +1; | An Axiom |
| constrrew | ⊦ 0 +1 = 1 | A User Theorem |
| elim-pred-c | n ≠ 0 ⊦ m = n -1 ↔ n = m +1 | A User Theorem |
| eq | ⊦ m < n → (¬ m +1 < n ↔ n = m +1) | A User Theorem |
| f | ⊦ m < n → n ≠ 0 | A User Theorem |
| ilf | ⊦ m +1 < m -1 → m = 0 | A User Theorem |
| ilf-01 | ⊦ m < m -1 → m = 0 | A User Theorem |
| ilf-02 | ⊦ m = m -1 → m = 0 | A User Theorem |
| ilf-03 | ⊦ ¬ m -1 -1 < m → m = 0 ∨ m = 1 | A User Theorem |
| k-two | ⊦ 2 = 1 +1 | A User Theorem |
| lf | ⊦ m < n ∧ n < n0 → m +1 < n0 | A User Theorem |
| lf-01 | ⊦ m < n ∧ n = n0 → m < n0 | A User Theorem |
| lf-02 | ⊦ m < n ∧ m = n0 → n0 < n | A User Theorem |
| lf-03 | ⊦ ¬ n < m ∧ n < n0 → m < n0 | A User Theorem |
| lf-04 | ⊦ ¬ n < m ∧ n = n0 → ¬ n0 < m | A User Theorem |
| lf-05 | ⊦ ¬ n < m ∧ m = n0 → ¬ n < n0 | A User Theorem |
| lf-06 | ⊦ ¬ m < n0 ∧ n < n0 → n < m | A User Theorem |
| lf-07 | ⊦ ¬ m < n ∧ ¬ n0 < m → ¬ n0 < n | A User Theorem |
| lf-08 | ⊦ m +1 < n → m < n | A User Theorem |
| lrec | ⊦ m +1 < n +1 ↔ m < n | A User Theorem |
| ls | ⊦ m < m +1 | A User Theorem |
| ls-01 | ⊦ ¬ m +1 < m | A User Theorem |
| ls-02 | ⊦ m < n → ¬ n < m | A User Theorem |
| ls-03 | ⊦ ¬ m < n → (¬ n < m ↔ n = m) | A User Theorem |
| ls-04 | ⊦ ¬ m < n ↔ ¬ ¬(m = n ∨ n < m) | A User Theorem |
| lstwo | ⊦ n ≠ 1 → (n < 2 ↔ n = 0) | A User Theorem |
| neq | ⊦ m ≠ n → (m < n +1 ↔ m < n) | A User Theorem |
| neq-01 | ⊦ m ≠ n → (¬ m < n ↔ n < m) | A User Theorem |
| numeral-1 | m ≠ 0 ⊦ n +1 = (* m) ↔ n = m -1 | A User Theorem |
| numeral-2 | m ≠ 0 ⊦ n +1 < (* m) ↔ n < m -1 | A User Theorem |
| one | ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1) | A User Theorem |
| one-01 | ⊦ m < 1 ↔ m = 0 | A User Theorem |
| one-02 | ⊦ m ≠ 0 → (¬ 1 < m ↔ m = 1) | A User Theorem |
| prop-ls | ⊦ m < n ∧ ¬ n0 < n → m < n0 | A User Theorem |
| prop-p | ⊦ m -1 = n -1 ∧ m ≠ 0 ∧ n ≠ 0 → m = n | A User Theorem |
| prop-p-01 | ⊦ n ≠ 0 ∧ m < n -1 → m < n | A User Theorem |
| psh | ⊦ m -1 < m ↔ m ≠ 0 | A User Theorem |
| psh-01 | ⊦ m < n0 → (n < n0 -1 ↔ n +1 < n0) | A User Theorem |
| psh-02 | ⊦ m ≠ 0 → (m -1 < n ↔ ¬ n < m) | A User Theorem |
| psh-03 | ⊦ m ≠ 0 → (m -1 = n ↔ m = n +1) | A User Theorem |
| psh-04 | ⊦ n ≠ 0 → (m < n -1 ↔ m +1 < n) | A User Theorem |
| psh-05 | ⊦ n ≠ 0 ∧ n ≠ 1 → (m < n -1 -1 ↔ m +1 +1 < n) | A User Theorem |
| psh-06 | ⊦ n ≠ 0 ∧ n ≠ 1 → (n -1 -1 < m ↔ n < m +1 +1) | A User Theorem |
| psh-07 | ⊦ ¬ n < m -1 → ¬ n +1 < m | A User Theorem |
| psh-08 | ⊦ ¬ n < m ∧ n ≠ 0 → (n -1 < m ↔ m = n) | A User Theorem |
| psh-09 | m ≠ 0 ⊦ m -1 < n ↔ m < n +1 | A User Theorem |
| psu | ⊦ m ≠ 0 → m -1 +1 = m | A User Theorem |
| psu-01 | ⊦ m ≠ 0 ∧ m ≠ 1 → m -1 -1 +1 = m -1 | A User Theorem |
| psu-02 | ⊦ n -1 +1 ≠ n ↔ n = 0 | A User Theorem |
| psu-03 | ⊦ n < m → m -1 +1 = m | A User Theorem |
| psu-04 | ⊦ ¬ m -1 +1 < m | A User Theorem |
| q | n ≠ 0, n ≠ 1 ⊦ ∃ m. m +1 +1 = n | A User Theorem |
| rax | ⊦ n0 < n +1 ↔ ¬ ¬(n0 = n ∨ n0 < n) | A User Theorem |
| s | ⊦ m < n +1 ↔ ¬ n < m | A User Theorem |
| s-01 | ⊦ m ≠ m +1 +1 | A User Theorem |
| s-02 | ⊦ m ≠ m +1 | A User Theorem |
| s-03 | ⊦ ¬ n +1 +1 < n | A User Theorem |
| tot | ⊦ n < m ∨ n = m ∨ m < n | A User Theorem |
| trans | ⊦ n < n0 ∧ n0 < n1 → n +1 < n1 | A User Theorem |
| twols-01 | ⊦ m ≠ 1 → (m < 2 ↔ m = 0) | A User Theorem |
| twols-02 | ⊦ m ≠ 0 → (m < 2 ↔ m = 1) | A User Theorem |
| z | ⊦ 0 < n ↔ n ≠ 0 | A User Theorem |
| zero | ⊦ 0 < m ↔ m ≠ 0 | A User Theorem |
| zero-01 | ⊦ ¬ m < 0 | A User Theorem |