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-def | ⊦ str1 .class l< str2 .class ↔ str1 < str2 | An Axiom |
| Irreflexivity | ⊦ ¬ class l< class | An Axiom |
| Transitivity | ⊦ class1 l< class2 ∧ class2 l< class3 → class1 l< class3 | An Axiom |
| Totality | ⊦ class1 l< class2 ∨ class1 = class2 ∨ class2 l< class1 | An Axiom |
| le-one | ⊦ class1 ≤ class2 ↔ class2 = `java.lang.Object' .class ∨ class1 = class2 ∨ class1 <_1 class2 ∨ (∃ class3. class1 <_1 class3 ∧ class3 ≤ class2) | An Axiom |
| le-transitive | ⊦ class1 ≤ class2 ∧ class2 ≤ class3 → class1 ≤ class3 | An Axiom |
| le-object | ⊦ class ≤ `java.lang.Object' .class | A User Theorem |
| le-reflexive | ⊦ class ≤ class | A User Theorem |