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: |
|---|---|---|
| trans | ⊦ i < j ∧ j < j0 → i < j0 | An Axiom |
| succpred | ⊦ i +1 -1 = i | An Axiom |
| predsucc | ⊦ i -1 +1 = i | An Axiom |
| irref | ⊦ ¬ i < i | An Axiom |
| lsrec | ⊦ i < j ↔ i +1 = j ∨ i +1 < j | An Axiom |
| lssucc | ⊦ i +1 < j ↔ i < j -1 | An Axiom |
| gen | int generated by 0, +1, -1; | An Axiom |
| elim-pred | ⊦ i = j -1 ↔ j = i +1 | A User Theorem |
| forward-any-lsle | ⊦ ¬ i0 < j ∧ i < j → i < i0 | A User Theorem |
| forward-pos | ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j | A User Theorem |
| k-lsrec | ⊦ i < j ↔ i = j -1 ∨ (∃ j0. i = j0 -1 ∧ j0 < j) | A User Theorem |
| l | ⊦ ¬ i < j ↔ ¬ ¬(i = j ∨ j < i) | A User Theorem |
| lf | ⊦ i +1 < j → i < j | A User Theorem |
| lf-01 | ⊦ i < j ∧ j < i0 → i +1 < i0 | A User Theorem |
| lf-02 | ⊦ i < j ∧ j = i0 → i < i0 | A User Theorem |
| lf-03 | ⊦ i < j ∧ i = i0 → i0 < j | A User Theorem |
| lf-04 | ⊦ ¬ j < i ∧ j < i0 → i < i0 | A User Theorem |
| lf-05 | ⊦ ¬ j < i ∧ j = i0 → ¬ i0 < i | A User Theorem |
| lf-06 | ⊦ ¬ j < i ∧ i = i0 → ¬ j < i0 | A User Theorem |
| lf-07 | ⊦ ¬ i < i0 ∧ j < i0 → j < i | A User Theorem |
| lf-08 | ⊦ ¬ i < j ∧ ¬ i0 < i → ¬ i0 < j | A User Theorem |
| ls | ⊦ ¬ i +1 < i | A User Theorem |
| ls-01 | ⊦ i < j → ¬ j < i | A User Theorem |
| ls-02 | ⊦ i < 1 ∧ i ≠ 0 → i < 0 | A User Theorem |
| ls-pred | ⊦ i < j -1 ↔ i +1 < j | A User Theorem |
| ls-pred-01 | ⊦ i -1 < j -1 ↔ i < j | A User Theorem |
| ls-pred-02 | ⊦ i -1 < i | A User Theorem |
| ls-pred-03 | ⊦ j < i → ¬ i -1 < j | A User Theorem |
| ls-pred-04 | ⊦ i -1 < j ↔ i < j +1 | A User Theorem |
| ls-rec | ⊦ i ≠ j -1 → (i < j ↔ i < j -1) | A User Theorem |
| ls-succ | ⊦ i < j +1 ↔ ¬ j < i | A User Theorem |
| ls-succ-01 | ⊦ i < i +1 | A User Theorem |
| ls-succ-02 | ⊦ i +1 < j +1 ↔ i < j | A User Theorem |
| ls-succ-03 | ⊦ i < j → (i +1 < j ↔ i +1 ≠ j) | A User Theorem |
| ls-succ-04 | ⊦ i < j → (¬ i +1 < j ↔ i +1 = j) | A User Theorem |
| ls-zero | ⊦ i < 0 → (¬ i +1 < 0 ↔ i +1 = 0) | A User Theorem |
| lst | ⊦ i < j ∧ ¬ i0 < j → ¬ i0 < i | A User Theorem |
| lst-01 | ⊦ ¬ i < j → (i ≠ j ↔ j < i) | A User Theorem |
| lst-02 | ⊦ ¬ i < j → (¬ j < i ↔ i = j) | A User Theorem |
| minus-one | ⊦ i < 0 → (~2 < i ↔ i = ~1) | A User Theorem |
| mone | ⊦ i = ~1 ↔ i +1 = 0 | A User Theorem |
| neg | ⊦ 0 +1 ≠ 0 -1 | A User Theorem |
| num-ls-rec | i ≠ j -1 ⊦ i < (* j) ↔ i < j -1 | A User Theorem |
| numeral | ⊦ i +1 = (* j) ↔ i = j -1 | A User Theorem |
| numeral-01 | ⊦ i +1 < (* j) ↔ i < j -1 | A User Theorem |
| numeral-02 | ⊦ (* j) < i +1 ↔ j -1 < i | A User Theorem |
| numlsf | ⊦ i < (* j) ∧ j < 0 → i < 0 | A User Theorem |
| numlslsdel | j0 ≠ 0, j < j0 ⊦ i < (* j) → i < (* j0) | A User Theorem |
| numlslsdel-01 | i0 ≠ 0, i0 < i ⊦ (* i) < j → (* i0) < j | A User Theorem |
| one-less | ⊦ 1 < i ↔ 0 < i -1 | A User Theorem |
| pred | ⊦ i = j -1 ↔ i +1 = j | A User Theorem |
| pred-in | ⊦ i -1 = j -1 ↔ i = j | A User Theorem |
| succ | ⊦ i ≠ i +1 | A User Theorem |
| succ-in | ⊦ i +1 = j +1 ↔ i = j | A User Theorem |
| tot | ⊦ i < j ∨ i = j ∨ j < i | A User Theorem |
| trans-lem | ¬ i < i0, i < j ⊦ ¬ j < i0 | A User Theorem |
| trans-succ | ⊦ i < j ∧ j < j0 → i +1 < j0 | A User Theorem |
| two-ls | ⊦ 0 < j → (j < 2 ↔ j = 1) | A User Theorem |