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: |
|---|---|---|
| irreflexivity | ⊦ ¬ r < r | An Axiom |
| transitivity | ⊦ r < r0 ∧ r0 < r1 → r < r1 | An Axiom |
| totality | ⊦ r < r0 ∨ r = r0 ∨ r0 < r | An Axiom |
| no-maximum | ⊦ ∀ r. ∃ r0. r < r0 | An Axiom |
| step | ⊦ ∀ r. ∃ r0. r < r0 ∧ ¬ (∃ r1. r < r1 ∧ r1 < r0) | An Axiom |
| next | ⊦ r < next(r) ∧ ¬ (∃ r1. r < r1 ∧ r1 < next(r)) | An Axiom |
| smallest | ⊦ ∀ r. ¬ r < jvmref | An Axiom |
| exists-notjvmref | ⊦ ∃ r. r ≠ jvmref | A User Theorem |
| lel | ⊦ r < r0 ∧ r = r1 → r1 < r0 | A User Theorem |
| lel-01 | ⊦ r < r0 ∧ r0 = r1 → r < r1 | A User Theorem |
| loc | ⊦ ¬ r < r0 ↔ ¬ ¬ (r = r0 ∨ r0 < r) | A User Theorem |
| nen | ⊦ ¬ r0 < r ∧ r = r1 → ¬ r0 < r1 | A User Theorem |
| nen-01 | ⊦ ¬ r0 < r ∧ r0 = r1 → ¬ r1 < r | A User Theorem |
| next-ls | ⊦ r < next(r) | A User Theorem |
| next-neq | ⊦ next(r) ≠ r | A User Theorem |
| next-neq-01 | ⊦ next(r) ≠ jvmref | A User Theorem |
| nll | ⊦ ¬ r0 < r ∧ r0 < r1 → r < r1 | A User Theorem |
| nnn | ⊦ ¬ r1 < r0 ∧ ¬ r < r1 → ¬ r < r0 | A User Theorem |
| seq | ⊦ ¬ r0 < r → (¬ r < r0 ↔ r = r0) | A User Theorem |
| sls | ⊦ r ≠ r0 → (¬ r < r0 ↔ r0 < r) | A User Theorem |
| smallest-01 | ⊦ ¬ r < jvmref | A User Theorem |