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-succ | ⊦ i + j +1 = (i + j)+1 | An Axiom |
| add-zero | ⊦ i + 0 = i | An Axiom |
| add-pred | ⊦ i + j -1 = (i + j)-1 | An Axiom |
| add-a | ⊦ i + j + i0 = (i + j) + i0 | A User Theorem |
| add-c | ⊦ i + j = j + i | A User Theorem |
| add-in | ⊦ i + j = i + i0 ↔ j = i0 | A User Theorem |
| add-less | ⊦ 0 < i → i1 < i1 + i | A User Theorem |
| add-pred-01 | ⊦ i -1 + j = (i + j)-1 | A User Theorem |
| add-succ-01 | ⊦ (i + j)+1 = i + i0 ↔ j +1 = i0 | A User Theorem |
| add-succ-02 | ⊦ i +1 + j = (i + j)+1 | A User Theorem |
| add-zero-rev | ⊦ 0 + i = i | A User Theorem |
| eq | ⊦ i = i + j ↔ j = 0 | A User Theorem |
| ex-ls-add | ⊦ i < j ↔ (∃ i0. j = i + i0 ∧ 0 < i0) | A User Theorem |
| ex-oddeven | ⊦ ∃ i. i + i = j ∨ i + i + 1 = j | A User Theorem |
| ls | ⊦ i + j < j ↔ i < 0 | A User Theorem |
| ls-01 | ⊦ i + j < i + i0 ↔ j < i0 | A User Theorem |
| ls-02 | ⊦ i < i + j ↔ 0 < j | A User Theorem |
| ls-03 | ⊦ j + i < j ↔ i < 0 | A User Theorem |
| ls-add-both | ⊦ i < j → i1 + i < i1 + j | A User Theorem |
| ls-succ-01 | ⊦ (i + j)+1 < i + i0 ↔ j +1 < i0 | A User Theorem |
| ls-succ-02 | ⊦ i + j < (i + i0)+1 ↔ j < i0 +1 | A User Theorem |
| ls-succ-03 | ⊦ (i + j)+1 < i ↔ j +1 < 0 | A User Theorem |
| ls-zero | ⊦ i < 0 ∧ j < 0 → ¬ 0 < i + j | A User Theorem |
| lst | i + j < i0, j0 < j ⊦ i + j0 < i0 | A User Theorem |
| lst-01 | ⊦ i < j + i0 ∧ j < j0 → i < j0 + i0 | A User Theorem |
| lst-02 | ⊦ i < j + i0 ∧ ¬ j0 < j → i < j0 + i0 | A User Theorem |
| lst-03 | ⊦ i + j < i0 ∧ ¬ j < j0 → i + j0 < i0 | A User Theorem |
| lst-04 | ⊦ i + j < i0 ∧ j0 < j → i + j0 < i0 | A User Theorem |
| lst-05 | ⊦ i < 0 ∧ j < j0 ∧ ¬ i0 < 0 → i + j < j0 + i0 | A User Theorem |
| mone-01 | ⊦ 0 = i + 1 ↔ i = ~1 | A User Theorem |
| mone-02 | ⊦ i + 1 = ~1 ↔ i + 1 + 1 = 0 | A User Theorem |
| mone-03 | ⊦ i + 1 = 0 → i < 0 | A User Theorem |
| mthree | ⊦ i + 3 = 0 → ¬ 2 < i | A User Theorem |
| neq | ⊦ j < 0 ∧ ¬ i0 < i → i0 ≠ i + j | A User Theorem |
| neq-01 | ⊦ i0 < i + j0 ∧ ¬ j < j0 → i0 ≠ i + j | A User Theorem |
| nls | ⊦ ¬ i < j ∧ ¬ i0 < j0 → ¬ i + i0 < j + j0 | A User Theorem |
| not-zero-pos | ⊦ 0 < i ∧ 0 < j → i + j ≠ 0 | A User Theorem |
| num-between | i + 1 = i0 ⊦ j < (* i0) → ¬ (* i) < j | A User Theorem |
| pls | i < j, i0 < j0 ⊦ i + i0 < j + j0 | A User Theorem |
| pls-01 | ¬ i < 0, ¬ j < 0 ⊦ ¬ i + j < 0 | A User Theorem |
| pls-02 | ¬ i < 0, ¬ j < j0 ⊦ ¬ i + j < j0 | A User Theorem |
| pls-03 | ¬ i < j, ¬ i0 < j0 ⊦ ¬ i + i0 < j + j0 | A User Theorem |
| pls-04 | i + j < i0 + j0, ¬ j < j0 ⊦ i < i0 | A User Theorem |
| plst | i < j, ¬ j0 < i0 ⊦ i + i0 < j + j0 | A User Theorem |
| plst-01 | i + i0 < j + j0, ¬ j1 < j0, ¬ i0 < i1 ⊦ i + i1 < j + j1 | A User Theorem |
| pred | ⊦ (i + 1)-1 = i | A User Theorem |
| rewz | ⊦ i + 1 = 0 ↔ i = 0 -1 | A User Theorem |
| succ | ⊦ (i + j)+1 = i ↔ j +1 = 0 | A User Theorem |
| succ-01 | ⊦ i +1 = i + 1 | A User Theorem |
| ttwo | ⊦ i + i < j + j ↔ i < j | A User Theorem |
| zero | ⊦ i < 0 ∧ j < 0 → i + j ≠ 0 | A User Theorem |
| zero-01 | ⊦ i < 0 ∧ j < 0 → i + j < 0 | A User Theorem |
| zero-02 | ⊦ 0 < i ∧ 0 < j → 0 < i + j | A User Theorem |
| zero-03 | ⊦ 0 < i ∧ ¬ j < 0 → 0 < i + j | A User Theorem |
| zero-04 | ⊦ 0 < i ∧ 0 < j → 0 ≠ i + j | A User Theorem |
| zero-05 | ⊦ 0 < i ∧ ¬ j < 0 → 0 ≠ i + j | A User Theorem |
| zero-06 | ⊦ ¬ i < 0 ∧ ¬ j < 0 → (0 = i + j ↔ i = 0 ∧ j = 0) | A User Theorem |
| zero-07 | ⊦ i + i = 0 ↔ i = 0 | A User Theorem |