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: |
|---|---|---|
| predef-classes | ⊦ predefined_classes = `java.lang.NullPointerException' .class + `java.lang.ArithmeticException' .class + `java.lang.ClassCastException' .class + `java.lang.ArrayStoreException' .class + `java.lang.NegativeArraySizeException' .class + `java.lang.ArrayIndexOutOfBoundsException' .class + `java.lang.IndexOutOfBoundsException' .class + `java.lang.RuntimeException' .class + `java.lang.NoClassDefFoundError' .class + `java.lang.ExceptionInInitializerError' .class + `java.lang.Error' .class + `java.lang.Exception' .class + `java.lang.Throwable' .class + (`*Array*' .class + `java.lang.Object' .class) | An Axiom |
| predefined | ⊦ is_predefined_class(class) ↔ class = `java.lang.Object' .class ∨ class = `*Array*' .class ∨ class = `java.lang.NullPointerException' .class ∨ class = `java.lang.ArithmeticException' .class ∨ class = `java.lang.ClassCastException' .class ∨ class = `java.lang.ArrayStoreException' .class ∨ class = `java.lang.NegativeArraySizeException' .class ∨ class = `java.lang.ArrayIndexOutOfBoundsException' .class ∨ class = `java.lang.IndexOutOfBoundsException' .class ∨ class = `java.lang.NoClassDefFoundError' .class ∨ class = `java.lang.ExceptionInInitializerError' .class ∨ class = `java.lang.Error' .class ∨ class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class | An Axiom |
| supers-not | ⊦ ¬ is_predefined_class(class) → predef_supers(class) = [] | An Axiom |
| supers-01 | ⊦ predef_supers(`java.lang.Object' .class) = `java.lang.Object' .class ' | An Axiom |
| supers-02 | ⊦ predef_supers(`*Array*' .class) = `*Array*' .class + `java.lang.Object' .class | An Axiom |
| supers-03 | ⊦ predef_supers(`java.lang.Throwable' .class) = `java.lang.Throwable' .class + `java.lang.Object' .class | An Axiom |
| supers-04 | ⊦ predef_supers(`java.lang.Error' .class) = `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-05 | ⊦ predef_supers(`java.lang.Exception' .class) = `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-06 | ⊦ predef_supers(`java.lang.NoClassDefFoundError' .class) = `java.lang.NoClassDefFoundError' .class + `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-07 | ⊦ predef_supers(`java.lang.ExceptionInInitializerError' .class) = `java.lang.ExceptionInInitializerError' .class + `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-08 | ⊦ predef_supers(`java.lang.RuntimeException' .class) = `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-09 | ⊦ predef_supers(`java.lang.NullPointerException' .class) = `java.lang.NullPointerException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-10 | ⊦ predef_supers(`java.lang.ArithmeticException' .class) = `java.lang.ArithmeticException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-11 | ⊦ predef_supers(`java.lang.ClassCastException' .class) = `java.lang.ClassCastException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-12 | ⊦ predef_supers(`java.lang.ArrayStoreException' .class) = `java.lang.ArrayStoreException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-13 | ⊦ predef_supers(`java.lang.NegativeArraySizeException' .class) = `java.lang.NegativeArraySizeException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| supers-14 | ⊦ predef_supers(`java.lang.IndexOutOfBoundsException' .class) = `java.lang.IndexOutOfBoundsException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| lsone-14 | ⊦ `java.lang.IndexOutOfBoundsException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class | An Axiom |
| lsone-13 | ⊦ `java.lang.NegativeArraySizeException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class | An Axiom |
| lsone-12 | ⊦ `java.lang.ArrayStoreException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class | An Axiom |
| lsone-11 | ⊦ `java.lang.ClassCastException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class | An Axiom |
| lsone-10 | ⊦ `java.lang.ArithmeticException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class | An Axiom |
| lsone-09 | ⊦ `java.lang.NullPointerException' .class <_1 class ↔ class = `java.lang.RuntimeException' .class | An Axiom |
| lsone-08 | ⊦ `java.lang.RuntimeException' .class <_1 class ↔ class = `java.lang.Exception' .class | An Axiom |
| lsone-07 | ⊦ `java.lang.ExceptionInInitializerError' .class <_1 class ↔ class = `java.lang.Error' .class | An Axiom |
| lsone-06 | ⊦ `java.lang.NoClassDefFoundError' .class <_1 class ↔ class = `java.lang.Error' .class | An Axiom |
| lsone-05 | ⊦ `java.lang.Exception' .class <_1 class ↔ class = `java.lang.Throwable' .class | An Axiom |
| lsone-04 | ⊦ `java.lang.Error' .class <_1 class ↔ class = `java.lang.Throwable' .class | An Axiom |
| lsone-03 | ⊦ `java.lang.Throwable' .class <_1 class ↔ class = `java.lang.Object' .class | An Axiom |
| lsone-02 | ⊦ `*Array*' .class <_1 class ↔ class = `java.lang.Object' .class | An Axiom |
| lsone-01 | ⊦ ¬ `java.lang.Object' .class <_1 class | An Axiom |
| superClass-14 | ⊦ predef_superClass(`java.lang.IndexOutOfBoundsException' .class) = `java.lang.RuntimeException' .class | An Axiom |
| superClass-13 | ⊦ predef_superClass(`java.lang.NegativeArraySizeException' .class) = `java.lang.RuntimeException' .class | An Axiom |
| superClass-12 | ⊦ predef_superClass(`java.lang.ArrayStoreException' .class) = `java.lang.RuntimeException' .class | An Axiom |
| superClass-11 | ⊦ predef_superClass(`java.lang.ClassCastException' .class) = `java.lang.RuntimeException' .class | An Axiom |
| superClass-10 | ⊦ predef_superClass(`java.lang.ArithmeticException' .class) = `java.lang.RuntimeException' .class | An Axiom |
| superClass-09 | ⊦ predef_superClass(`java.lang.NullPointerException' .class) = `java.lang.RuntimeException' .class | An Axiom |
| superClass-08 | ⊦ predef_superClass(`java.lang.RuntimeException' .class) = `java.lang.Exception' .class | An Axiom |
| superClass-07 | ⊦ predef_superClass(`java.lang.ExceptionInInitializerError' .class) = `java.lang.Error' .class | An Axiom |
| superClass-06 | ⊦ predef_superClass(`java.lang.NoClassDefFoundError' .class) = `java.lang.Error' .class | An Axiom |
| superClass-05 | ⊦ predef_superClass(`java.lang.Exception' .class) = `java.lang.Throwable' .class | An Axiom |
| superClass-04 | ⊦ predef_superClass(`java.lang.Error' .class) = `java.lang.Throwable' .class | An Axiom |
| superClass-03 | ⊦ predef_superClass(`java.lang.Throwable' .class) = `java.lang.Object' .class | An Axiom |
| superClass-02 | ⊦ predef_superClass(`*Array*' .class) = `java.lang.Object' .class | An Axiom |
| superClass-01 | ⊦ predef_superClass(`java.lang.Object' .class) = `java.lang.Object' .class | An Axiom |
| superClass-not | ⊦ ¬ is_predefined_class(class) → predef_superClass(class) = `java.lang.Object' .class | An Axiom |
| superClass-15 | ⊦ predef_superClass(`java.lang.ArrayIndexOutOfBoundsException' .class) = `java.lang.IndexOutOfBoundsException' .class | An Axiom |
| supers-15 | ⊦ predef_supers(`java.lang.ArrayIndexOutOfBoundsException' .class) = `java.lang.ArrayIndexOutOfBoundsException' .class + `java.lang.IndexOutOfBoundsException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) | An Axiom |
| lsone-15 | ⊦ `java.lang.ArrayIndexOutOfBoundsException' .class <_1 class ↔ class = `java.lang.IndexOutOfBoundsException' .class | An Axiom |
| class-le-predef | ⊦ is_predefined_class(class) ∧ ¬ is_predefined_class(class0) → ¬ class ≤ class0 | A User Theorem |
| in-predefs | ⊦ class ∈ predefined_classes ↔ is_predefined_class(class) | A User Theorem |
| le-01 | ⊦ `java.lang.Object' .class ≤ class ↔ class = `java.lang.Object' .class | A User Theorem |
| le-02 | ⊦ `*Array*' .class ≤ class ↔ ¬ ¬ (class = `*Array*' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-03 | ⊦ `java.lang.Throwable' .class ≤ class ↔ ¬ ¬ (class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-04 | ⊦ `java.lang.Error' .class ≤ class ↔ ¬ ¬ (class = `java.lang.Error' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-05 | ⊦ `java.lang.Exception' .class ≤ class ↔ ¬ ¬ (class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-06 | ⊦ `java.lang.NoClassDefFoundError' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.NoClassDefFoundError' .class ∨ class = `java.lang.Error' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-07 | ⊦ `java.lang.ExceptionInInitializerError' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.ExceptionInInitializerError' .class ∨ class = `java.lang.Error' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-08 | ⊦ `java.lang.RuntimeException' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-09 | ⊦ `java.lang.NullPointerException' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.NullPointerException' .class ∨ class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-10 | ⊦ `java.lang.ArithmeticException' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.ArithmeticException' .class ∨ class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-11 | ⊦ `java.lang.ClassCastException' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.ClassCastException' .class ∨ class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-12 | ⊦ `java.lang.ArrayStoreException' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.ArrayStoreException' .class ∨ class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-13 | ⊦ `java.lang.NegativeArraySizeException' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.NegativeArraySizeException' .class ∨ class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-14 | ⊦ `java.lang.IndexOutOfBoundsException' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.IndexOutOfBoundsException' .class ∨ class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| le-15 | ⊦ `java.lang.ArrayIndexOutOfBoundsException' .class ≤ class ↔ ¬ ¬ ( class = `java.lang.ArrayIndexOutOfBoundsException' .class ∨ class = `java.lang.IndexOutOfBoundsException' .class ∨ class = `java.lang.RuntimeException' .class ∨ class = `java.lang.Exception' .class ∨ class = `java.lang.Throwable' .class ∨ class = `java.lang.Object' .class) | A User Theorem |
| obj-predefs | ⊦ is_predefined_class(class) → `java.lang.Object' .class ∈ predef_supers(class) | A User Theorem |
| predef | ⊦ is_predefined_class(`java.lang.Object' .class) | A User Theorem |
| predef-01 | ⊦ is_predefined_class(`*Array*' .class) | A User Theorem |
| predef-02 | ⊦ is_predefined_class(`java.lang.NullPointerException' .class) | A User Theorem |
| predef-03 | ⊦ is_predefined_class(`java.lang.ArithmeticException' .class) | A User Theorem |
| predef-04 | ⊦ is_predefined_class(`java.lang.ClassCastException' .class) | A User Theorem |
| predef-05 | ⊦ is_predefined_class(`java.lang.ArrayStoreException' .class) | A User Theorem |
| predef-06 | ⊦ is_predefined_class(`java.lang.NegativeArraySizeException' .class) | A User Theorem |
| predef-07 | ⊦ is_predefined_class(`java.lang.IndexOutOfBoundsException' .class) | A User Theorem |
| predef-08 | ⊦ is_predefined_class(`java.lang.NoClassDefFoundError' .class) | A User Theorem |
| predef-09 | ⊦ is_predefined_class(`java.lang.ExceptionInInitializerError' .class) | A User Theorem |
| predef-10 | ⊦ is_predefined_class(`java.lang.Error' .class) | A User Theorem |
| predef-11 | ⊦ is_predefined_class(`java.lang.RuntimeException' .class) | A User Theorem |
| predef-12 | ⊦ is_predefined_class(`java.lang.Exception' .class) | A User Theorem |
| predef-13 | ⊦ is_predefined_class(`java.lang.Throwable' .class) | A User Theorem |
| predef-14 | ⊦ is_predefined_class(`java.lang.ArrayIndexOutOfBoundsException' .class) | A User Theorem |
| predef-const | ⊦ is_predefined_class(((* str)) .class) ↔ ¬ ¬ ( str .class = `java.lang.Object' .class ∨ str .class = `*Array*' .class ∨ str .class = `java.lang.NullPointerException' .class ∨ str .class = `java.lang.ArithmeticException' .class ∨ str .class = `java.lang.ClassCastException' .class ∨ str .class = `java.lang.ArrayStoreException' .class ∨ str .class = `java.lang.NegativeArraySizeException' .class ∨ str .class = `java.lang.ArrayIndexOutOfBoundsException' .class ∨ str .class = `java.lang.IndexOutOfBoundsException' .class ∨ str .class = `java.lang.NoClassDefFoundError' .class ∨ str .class = `java.lang.ExceptionInInitializerError' .class ∨ str .class = `java.lang.Error' .class ∨ str .class = `java.lang.RuntimeException' .class ∨ str .class = `java.lang.Exception' .class ∨ str .class = `java.lang.Throwable' .class) | A User Theorem |
| predef-supers-rec | ⊦ class ≠ `java.lang.Object' .class ∧ is_predefined_class(class) → predef_supers(class) = class ' + predef_supers(predef_superClass(class)) | A User Theorem |
| predef-supers-same | ⊦ is_predefined_class(class) → class ∈ predef_supers(class) | A User Theorem |
| predef_supers-if | ⊦ predef_supers(class) = ((class = `java.lang.Object' .class ⊃ `java.lang.Object' .class ' ; (class = `*Array*' .class ⊃ `*Array*' .class + `java.lang.Object' .class ; (class = `java.lang.Throwable' .class ⊃ `java.lang.Throwable' .class + `java.lang.Object' .class ; (class = `java.lang.Error' .class ⊃ `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.Exception' .class ⊃ `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.NoClassDefFoundError' .class ⊃ `java.lang.NoClassDefFoundError' .class + `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.ExceptionInInitializerError' .class ⊃ `java.lang.ExceptionInInitializerError' .class + `java.lang.Error' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.RuntimeException' .class ⊃ `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.NullPointerException' .class ⊃ `java.lang.NullPointerException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.ArithmeticException' .class ⊃ `java.lang.ArithmeticException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.ClassCastException' .class ⊃ `java.lang.ClassCastException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.ArrayStoreException' .class ⊃ `java.lang.ArrayStoreException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.NegativeArraySizeException' .class ⊃ `java.lang.NegativeArraySizeException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.IndexOutOfBoundsException' .class ⊃ `java.lang.IndexOutOfBoundsException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; (class = `java.lang.ArrayIndexOutOfBoundsException' .class ⊃ `java.lang.ArrayIndexOutOfBoundsException' .class + `java.lang.IndexOutOfBoundsException' .class + `java.lang.RuntimeException' .class + `java.lang.Exception' .class + (`java.lang.Throwable' .class + `java.lang.Object' .class) ; [] ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) | A User Theorem |
| predsupers-in | ⊦ ¬ is_predefined_class(class) → ¬ class ∈ predef_supers(class0) | A User Theorem |
| subclass-object | ⊦ is_predefined_class(class) → class ≤ `java.lang.Object' .class | A User Theorem |
| superClass-diff | ⊦ is_predefined_class(class) ∧ class ≠ `java.lang.Object' .class → predef_superClass(class) ≠ class | A User Theorem |
| superClass-predef | ⊦ is_predefined_class(predef_superClass(class)) | A User Theorem |
| superClass-supers | ⊦ is_predefined_class(class) ∧ class ≠ `java.lang.Object' .class → predef_superClass(class) = predef_supers(class) .rest .first | A User Theorem |
| supers-nodups | ⊦ ¬ dups(predef_supers(class)) | A User Theorem |