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: |
|---|---|---|
| subclass | ⊦ mkclasstype(class1) ≤ mkclasstype(class2) ↔ class1 ≤ class2 | An Axiom |
| subarray1 | ⊦ mkarraytype(ty) ≤ mkarraytype(ty0) ↔ ty ≤ ty0 | An Axiom |
| subarray2 | ⊦ mkarraytype(ty) ≤ mkclasstype(class1) ↔ class1 = `java.lang.Object' .class | An Axiom |
| subarray3 | ⊦ ¬ mkclasstype(class1) ≤ mkarraytype(ty) | An Axiom |
| subbasic1 | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (ty ≤ ty0 ↔ ty = ty0) | An Axiom |
| subbasic2 | ⊦ ¬ is_classtype(ty0) ∧ ¬ is_arraytype(ty0) → (ty ≤ ty0 ↔ ty = ty0) | An Axiom |
| mktype_rec | ⊦ 0 < i → mktype_from_dims(ty, i) = mkarraytype(mktype_from_dims(ty, i - 1)) | An Axiom |
| mktype_base | ⊦ i ≤ 0 → mktype_from_dims(ty, i) = ty | An Axiom |
| jtclass | ⊦ ty .jtclass = ty .jtelemtype .class | An Axiom |
| has-classtype | ⊦ has_classtype(ty) ↔ is_classtype(ty .jtelemtype) | An Axiom |
| elemtype-rec | ⊦ is_arraytype(ty) → ty .jtelemtype = ty .type .jtelemtype | An Axiom |
| elemtype-base | ⊦ ¬ is_arraytype(ty) → ty .jtelemtype = ty | An Axiom |
| dims-rec | ⊦ is_arraytype(ty) → ty .jtdims = ty .type .jtdims + 1 | An Axiom |
| dims-base | ⊦ ¬ is_arraytype(ty) → ty .jtdims = 0 | An Axiom |
| is-reftype | ⊦ is_reftype(ty) ↔ is_classtype(ty) ∨ is_arraytype(ty) | An Axiom |
| subtype-other | ⊦ ¬ is_reftype(ty2) → (is_subtype(ty1, ty2, claset) ↔ ty1 = ty2) | An Axiom |
| subtype-cla | ⊦ class ≠ `java.lang.Object' .class → (is_subtype(ty1, mkclasstype(class), claset) ↔ is_classtype(ty1) ∧ ty1 .class ∈ claset) | An Axiom |
| subtype-obj | ⊦ is_subtype(ty1, mkclasstype(`java.lang.Object' .class), claset) ↔ is_reftype(ty1) | An Axiom |
| subtype-arr | ⊦ is_subtype(ty1, mkarraytype(ty2), claset) ↔ is_arraytype(ty1) ∧ is_subtype(ty1 .type, ty2, claset) | An Axiom |
| subclass-other | ⊦ ¬ is_predefined_class(class1) → (is_subclass(class1, classes, class2) ↔ class2 = `java.lang.Object' .class ∨ class2 ∈ classes) | An Axiom |
| subclass-pre | ⊦ is_predefined_class(class1) → (is_subclass(class1, classes, class2) ↔ class2 ∈ predef_supers(class1)) | An Axiom |
| subsups-other | ⊦ ¬ is_reftype(ty1) → (is_subtype(ty1, classes, ty2) ↔ ty1 = ty2) | An Axiom |
| subsups-cla | ⊦ is_subtype(mkclasstype(class), classes, ty2) ↔ is_classtype(ty2) ∧ is_subclass(class, classes, ty2 .class) | An Axiom |
| subsups-arr | ⊦ is_subtype(mkarraytype(ty1), classes, ty2) ↔ ty2 = mkclasstype(`java.lang.Object' .class) ∨ is_arraytype(ty2) ∧ is_subtype(ty1, classes, ty2 .type) | An Axiom |
| is_subtype-level | ⊦ is_subtype(str, ty1, ty2) ↔ ty1 ≤ ty2 ∧ (has_classtype(ty1) → tdname+∃(str, ty1 .jtclass)) ∧ (has_classtype(ty2) → tdname+∃(str, ty2 .jtclass)) | An Axiom |
| classex-def | ⊦ class+∃(str, class) ↔ class∃(str, class) ∨ is_predefined_class(class) | An Axiom |
| tdname+ex-def | ⊦ tdname+∃(str, class) ↔ tdname∃(str, class) ∨ is_predefined_class(class) | An Axiom |
| tdnameex-def | ⊦ tdname∃(str, class) ↔ class∃(str, class) ∨ interface∃(str, class) | An Axiom |
| typeex-def | ⊦ type∃(str, ty) ↔ ¬ has_classtype(ty) ∨ tdname+∃(str, ty .jtclass) | An Axiom |
| classex-notpredef | ⊦ class∃(str, class) → ¬ is_predefined_class(class) | An Axiom |
| classex-object | ⊦ class∃(str, class) → class ≤ `java.lang.Object' .class | An Axiom |
| interfaceex-object | ⊦ interface∃(str, class) → class ≤ `java.lang.Object' .class | An Axiom |
| is_primtype | ⊦ is_primtype(ty) ↔ ty = boolean_type ∨ ty = int_type ∨ ty = short_type ∨ ty = byte_type ∨ ty = long_type ∨ ty = float_type ∨ ty = double_type ∨ ty = char_type | An Axiom |
| is_abstract-predef | ⊦ is_predefined_class(class) → ¬ is_abstract(class) | An Axiom |
| interfaceex-notpredef | ⊦ interface∃(str, class) → ¬ is_predefined_class(class) | An Axiom |
| classex-nointerface | ⊦ class∃(str, class) → ¬ interface∃(str, class) | An Axiom |
| array | ⊦ ty0 ≤ mkarraytype(ty) ↔ is_arraytype(ty0) ∧ ty0 .type ≤ ty | A User Theorem |
| array-le | ⊦ mkarraytype(ty) ≤ ty0 ↔ ty0 = mkclasstype(`java.lang.Object' .class) ∨ is_arraytype(ty0) ∧ ty ≤ ty0 .type | A User Theorem |
| bytearray | ⊦ ty ≤ mkarraytype(byte_type) ↔ ty = mkarraytype(byte_type) | A User Theorem |
| class+predef | ⊦ class+∃(str, `java.lang.NoClassDefFoundError' .class) | A User Theorem |
| class-le | ⊦ mkclasstype(class) ≤ ty ↔ is_classtype(ty) ∧ class ≤ ty .class | A User Theorem |
| class-le-class | ⊦ class ≠ `java.lang.Object' .class ∧ ¬ is_predefined_class(class) → (ty ≤ mkclasstype(class) ↔ (∃ class0. ty = mkclasstype(class0) ∧ class0 ≤ class ∧ ¬ is_predefined_class(class0))) | A User Theorem |
| class-le-class-01 | str ≠ `java.lang.Object', ¬ is_predefined_class(str .class) ⊦ ¬ ¬ ty ≤ mkclasstype(((* str)) .class) ↔ (∃ class0. ty = mkclasstype(class0) ∧ class0 ≤ str .class ∧ ¬ is_predefined_class(class0)) | A User Theorem |
| classex | ⊦ is_predefined_class(class) → class+∃(str, class) | A User Theorem |
| classex-01 | ⊦ class∃(str, class) → class+∃(str, class) | A User Theorem |
| classex-02 | ⊦ ¬ class∃(str, class) → (class+∃(str, class) ↔ is_predefined_class(class)) | A User Theorem |
| classex-03 | ⊦ ¬ is_predefined_class(class) → (class+∃(str, class) ↔ class∃(str, class)) | A User Theorem |
| classex-object-01 | ⊦ tdname+∃(str, class) → class ≤ `java.lang.Object' .class | A User Theorem |
| dims-pos | ⊦ ¬ ty .jtdims < 0 | A User Theorem |
| dims-pos-01 | ⊦ ty .jtdims ≠ (~1) | A User Theorem |
| dims-prim | ⊦ boolean_type .jtdims = 0 | A User Theorem |
| dims-prim-01 | ⊦ int_type .jtdims = 0 | A User Theorem |
| dims-prim-02 | ⊦ short_type .jtdims = 0 | A User Theorem |
| dims-prim-03 | ⊦ byte_type .jtdims = 0 | A User Theorem |
| dims-prim-04 | ⊦ long_type .jtdims = 0 | A User Theorem |
| dims-prim-05 | ⊦ float_type .jtdims = 0 | A User Theorem |
| dims-prim-06 | ⊦ double_type .jtdims = 0 | A User Theorem |
| dims-prim-07 | ⊦ char_type .jtdims = 0 | A User Theorem |
| dims-prim-08 | ⊦ void_type .jtdims = 0 | A User Theorem |
| dims-prim-09 | ⊦ abstract_type .jtdims = 0 | A User Theorem |
| dims-succ | ⊦ mkarraytype(ty) .jtdims = ty .jtdims + 1 | A User Theorem |
| dims-zero | ⊦ mkclasstype(class) .jtdims = 0 | A User Theorem |
| dims-zero-01 | ⊦ ty .jtdims = 0 → (has_classtype(ty) ↔ is_classtype(ty)) | A User Theorem |
| elemtype | ⊦ boolean_type .jtelemtype = boolean_type | A User Theorem |
| elemtype-01 | ⊦ int_type .jtelemtype = int_type | A User Theorem |
| elemtype-02 | ⊦ short_type .jtelemtype = short_type | A User Theorem |
| elemtype-03 | ⊦ byte_type .jtelemtype = byte_type | A User Theorem |
| elemtype-04 | ⊦ mkclasstype(class) .jtelemtype = mkclasstype(class) | A User Theorem |
| elemtype-05 | ⊦ void_type .jtelemtype = void_type | A User Theorem |
| elemtype-06 | ⊦ abstract_type .jtelemtype = abstract_type | A User Theorem |
| elemtype-07 | ⊦ mkarraytype(ty) .jtelemtype = ty .jtelemtype | A User Theorem |
| elemtype-08 | ⊦ ty .jtdims = 0 → ty .jtelemtype = ty | A User Theorem |
| elemtype-dims | ⊦ ty .jtdims = ty0 .jtdims → (ty .jtelemtype = ty0 .jtelemtype ↔ ty = ty0) | A User Theorem |
| elemtype-dims-01 | ⊦ ty .jtdims = ty0 .jtdims + i ∧ 0 ≤ i → (ty .jtelemtype = ty0 .jtelemtype ↔ ty = mktype_from_dims(ty0, i)) | A User Theorem |
| hasclass-class | ⊦ ¬ is_arraytype(ty) → (has_classtype(ty) ↔ is_classtype(ty)) | A User Theorem |
| hasclass-no | ⊦ ¬ is_reftype(ty) → ¬ has_classtype(ty) | A User Theorem |
| hasclasstype | ⊦ ¬ has_classtype(ty) → ¬ is_classtype(ty) | A User Theorem |
| hasct | ⊦ ¬ has_classtype(boolean_type) | A User Theorem |
| hasct-01 | ⊦ ¬ has_classtype(int_type) | A User Theorem |
| hasct-02 | ⊦ ¬ has_classtype(short_type) | A User Theorem |
| hasct-03 | ⊦ ¬ has_classtype(byte_type) | A User Theorem |
| hasct-04 | ⊦ has_classtype(mkclasstype(class)) | A User Theorem |
| hasct-05 | ⊦ has_classtype(mkarraytype(ty)) ↔ has_classtype(ty) | A User Theorem |
| hasct-06 | ⊦ ¬ has_classtype(void_type) | A User Theorem |
| hasct-07 | ⊦ ¬ has_classtype(abstract_type) | A User Theorem |
| hasct-08 | ⊦ ¬ has_classtype(long_type) | A User Theorem |
| hasct-09 | ⊦ ¬ has_classtype(char_type) | A User Theorem |
| hasct-10 | ⊦ ¬ has_classtype(float_type) | A User Theorem |
| hasct-11 | ⊦ ¬ has_classtype(double_type) | A User Theorem |
| interfaceex-noclass | ⊦ interface∃(str, class) → ¬ class∃(str, class) | A User Theorem |
| is_primtype-01 | ⊦ is_primtype(ty) → type∃(str, ty) | A User Theorem |
| is_primtype-02 | ⊦ is_primtype(ty) → ty .jtelemtype = ty | A User Theorem |
| is_primtype-03 | ⊦ is_reftype(ty) → ¬ is_primtype(ty) | A User Theorem |
| isreftype | ⊦ ¬ is_reftype(boolean_type) | A User Theorem |
| isreftype-01 | ⊦ ¬ is_reftype(int_type) | A User Theorem |
| isreftype-02 | ⊦ ¬ is_reftype(short_type) | A User Theorem |
| isreftype-03 | ⊦ ¬ is_reftype(byte_type) | A User Theorem |
| isreftype-04 | ⊦ is_reftype(mkclasstype(class)) | A User Theorem |
| isreftype-05 | ⊦ is_reftype(mkarraytype(ty)) | A User Theorem |
| isreftype-06 | ⊦ ¬ is_reftype(void_type) | A User Theorem |
| isreftype-07 | ⊦ ¬ is_reftype(abstract_type) | A User Theorem |
| isreftype-08 | ⊦ ¬ is_reftype(long_type) | A User Theorem |
| isreftype-09 | ⊦ ¬ is_reftype(char_type) | A User Theorem |
| isreftype-10 | ⊦ ¬ is_reftype(float_type) | A User Theorem |
| isreftype-11 | ⊦ ¬ is_reftype(double_type) | A User Theorem |
| jtdims-pos | ⊦ ty .jtdims ≤ 0 ↔ ¬ is_arraytype(ty) | A User Theorem |
| jtelemtype | ⊦ ¬ is_arraytype(ty .jtelemtype) | A User Theorem |
| jtelemtype-01 | ⊦ has_classtype(ty) → mkclasstype(ty .jtelemtype .class) = ty .jtelemtype | A User Theorem |
| jtelemtype-02 | ⊦ ty .jtelemtype .jtelemtype = ty .jtelemtype | A User Theorem |
| jtelemtype-03 | ⊦ char_type .jtelemtype = char_type | A User Theorem |
| jtelemtype-04 | ⊦ double_type .jtelemtype = double_type | A User Theorem |
| jtelemtype-05 | ⊦ float_type .jtelemtype = float_type | A User Theorem |
| jtelemtype-06 | ⊦ long_type .jtelemtype = long_type | A User Theorem |
| jtelemtype-class | ⊦ is_classtype(ty) → ty .jtelemtype = ty | A User Theorem |
| le | ⊦ boolean_type ≤ ty ↔ ty = boolean_type | A User Theorem |
| le-01 | ⊦ int_type ≤ ty ↔ ty = int_type | A User Theorem |
| le-02 | ⊦ ty ≤ abstract_type ↔ ty = abstract_type | A User Theorem |
| le-03 | ⊦ abstract_type ≤ ty ↔ ty = abstract_type | A User Theorem |
| le-04 | ⊦ void_type ≤ ty ↔ ty = void_type | A User Theorem |
| le-05 | ⊦ short_type ≤ ty ↔ ty = short_type | A User Theorem |
| le-06 | ⊦ byte_type ≤ ty ↔ ty = byte_type | A User Theorem |
| le-07 | ⊦ ty ≤ boolean_type ↔ ty = boolean_type | A User Theorem |
| le-08 | ⊦ ty ≤ int_type ↔ ty = int_type | A User Theorem |
| le-09 | ⊦ long_type ≤ ty ↔ ty = long_type | A User Theorem |
| le-10 | ⊦ char_type ≤ ty ↔ ty = char_type | A User Theorem |
| le-11 | ⊦ ty ≤ void_type ↔ ty = void_type | A User Theorem |
| le-12 | ⊦ ty ≤ short_type ↔ ty = short_type | A User Theorem |
| le-13 | ⊦ ty ≤ byte_type ↔ ty = byte_type | A User Theorem |
| le-14 | ⊦ float_type ≤ ty ↔ ty = float_type | A User Theorem |
| le-15 | ⊦ double_type ≤ ty ↔ ty = double_type | A User Theorem |
| le-16 | ⊦ ty ≤ long_type ↔ ty = long_type | A User Theorem |
| le-17 | ⊦ ty ≤ char_type ↔ ty = char_type | A User Theorem |
| le-18 | ⊦ ty ≤ float_type ↔ ty = float_type | A User Theorem |
| le-19 | ⊦ ty ≤ double_type ↔ ty = double_type | A User Theorem |
| le-bigger | ⊦ ty .jtelemtype ≠ mkclasstype(`java.lang.Object' .class) → ¬ mkarraytype(ty) ≤ ty | A User Theorem |
| le-hasct | ⊦ ¬ has_classtype(ty) → (ty0 ≤ ty ↔ ty0 = ty) | A User Theorem |
| le-noreftype | ⊦ ¬ is_reftype(ty) → (ty ≤ ty0 ↔ ty = ty0) | A User Theorem |
| le-noreftype-01 | ⊦ ¬ is_reftype(ty0) → (ty ≤ ty0 ↔ ty = ty0) | A User Theorem |
| mkarraydims | ⊦ has_classtype(mktype_from_dims(ty, i)) ↔ has_classtype(ty) | A User Theorem |
| mkarraydims-01 | ⊦ mktype_from_dims(ty, i) .jtelemtype = ty .jtelemtype | A User Theorem |
| mkarraydims-02 | ⊦ 0 ≤ i → mktype_from_dims(ty, i) .jtdims = ty .jtdims + i | A User Theorem |
| mkarraydims-array | ⊦ 0 ≤ i → mkarraytype(mktype_from_dims(ty, i)) = mktype_from_dims(ty, i + 1) | A User Theorem |
| mkarraydims-rec | ⊦ 0 ≤ i ∧ 0 ≤ j → mktype_from_dims(mktype_from_dims(ty, i), j) = mktype_from_dims(ty, i + j) | A User Theorem |
| mkarraydims-reftype | ⊦ is_reftype(mktype_from_dims(ty, i)) ↔ ¬ ¬ (is_reftype(ty) ∨ 0 < i) | A User Theorem |
| mkarraydims-ty | ⊦ is_classtype(mktype_from_dims(ty, i)) ↔ ¬ ¬ (i ≤ 0 ∧ is_classtype(ty)) | A User Theorem |
| mkarraytype-zero | ⊦ mktype_from_dims(ty, 0) = ty | A User Theorem |
| mkdims | 0 < i ⊦ mktype_from_dims(ty, (* i)) = mkarraytype(mktype_from_dims(ty, i - 1)) | A User Theorem |
| mkdims-void | ⊦ mktype_from_dims(ty, i) = void_type ↔ ¬ ¬ (i ≤ 0 ∧ ty = void_type) | A User Theorem |
| mktype-one | ⊦ mktype_from_dims(ty, 1) = mkarraytype(ty) | A User Theorem |
| prim-abstract | ⊦ ¬ is_primtype(abstract_type) | A User Theorem |
| prim-bool | ⊦ is_primtype(boolean_type) | A User Theorem |
| prim-byte | ⊦ is_primtype(byte_type) | A User Theorem |
| prim-char | ⊦ is_primtype(char_type) | A User Theorem |
| prim-classtype | ⊦ is_primtype(ty) → ¬ has_classtype(ty) | A User Theorem |
| prim-double | ⊦ is_primtype(double_type) | A User Theorem |
| prim-float | ⊦ is_primtype(float_type) | A User Theorem |
| prim-int | ⊦ is_primtype(int_type) | A User Theorem |
| prim-long | ⊦ is_primtype(long_type) | A User Theorem |
| prim-short | ⊦ is_primtype(short_type) | A User Theorem |
| prim-void | ⊦ ¬ is_primtype(void_type) | A User Theorem |
| ref | ⊦ ty ≤ ty | A User Theorem |
| reftype | ⊦ ¬ is_classtype(ty) → (is_reftype(ty) ↔ is_arraytype(ty)) | A User Theorem |
| reftype-01 | ⊦ ¬ is_arraytype(ty) → (is_reftype(ty) ↔ is_classtype(ty)) | A User Theorem |
| reftype-class | ⊦ is_classtype(ty) → is_reftype(ty) | A User Theorem |
| subclass-01 | ⊦ class ≠ `java.lang.Object' .class → (ty ≤ mkclasstype(class) ↔ is_classtype(ty) ∧ ty .class ≤ class) | A User Theorem |
| subclass-other-01 | ¬ is_predefined_class(str .class) ⊦ is_subclass(((* str)) .class, classes, class2) ↔ class2 = `java.lang.Object' .class ∨ class2 ∈ classes | A User Theorem |
| subclass-other-02 | ¬ is_predefined_class(str .class) ⊦ is_subclass(((* str)) .class, classes, class2) ↔ ¬ ¬ (class2 = `java.lang.Object' .class ∨ class2 ∈ classes) | A User Theorem |
| subclass-pre-01 | is_predefined_class(str .class) ⊦ is_subclass(((* str)) .class, classes, class2) ↔ class2 ∈ predef_supers(str .class) | A User Theorem |
| subsups | ⊦ is_subtype(long_type, classes, ty0) ↔ ty0 = long_type | A User Theorem |
| subsups-01 | ⊦ is_subtype(char_type, classes, ty0) ↔ ty0 = char_type | A User Theorem |
| subsups-02 | ⊦ is_subtype(float_type, classes, ty0) ↔ ty0 = float_type | A User Theorem |
| subsups-03 | ⊦ is_subtype(double_type, classes, ty0) ↔ ty0 = double_type | A User Theorem |
| subsups-abstract | ⊦ is_subtype(abstract_type, classes, ty0) ↔ ty0 = abstract_type | A User Theorem |
| subsups-bool | ⊦ is_subtype(boolean_type, classes, ty0) ↔ ty0 = boolean_type | A User Theorem |
| subsups-byte | ⊦ is_subtype(byte_type, classes, ty0) ↔ ty0 = byte_type | A User Theorem |
| subsups-cla-01 | ⊦ is_subtype(mkclasstype(class), classes, mkclasstype(class2)) ↔ is_subclass(class, classes, class2) | A User Theorem |
| subsups-empty | ⊦ is_subclass(class, [], class0) ↔ class0 = `java.lang.Object' .class ∨ is_predefined_class(class) ∧ class0 ∈ predef_supers(class) | A User Theorem |
| subsups-empty-01 | ⊦ is_subclass(class, [], class0) ↔ ¬ ¬ (class0 = `java.lang.Object' .class ∨ is_predefined_class(class) ∧ class0 ∈ predef_supers(class)) | A User Theorem |
| subsups-hasct | ⊦ ¬ has_classtype(ty) → (is_subtype(ty, classes, ty0) ↔ is_subtype(ty, [], ty0)) | A User Theorem |
| subsups-hasct-01 | ⊦ ¬ has_classtype(ty) ∧ ¬ is_subtype(ty, classes0, ty0) → ¬ is_subtype(ty, classes, ty0) | A User Theorem |
| subsups-int | ⊦ is_subtype(int_type, classes, ty0) ↔ ty0 = int_type | A User Theorem |
| subsups-short | ⊦ is_subtype(short_type, classes, ty0) ↔ ty0 = short_type | A User Theorem |
| subsups-void | ⊦ is_subtype(void_type, classes, ty0) ↔ ty0 = void_type | A User Theorem |
| subtype | ⊦ is_subtype(boolean_type, ty, claset) ↔ ty = boolean_type | A User Theorem |
| subtype-01 | ⊦ is_subtype(int_type, ty, claset) ↔ ty = int_type | A User Theorem |
| subtype-02 | ⊦ is_subtype(short_type, ty, claset) ↔ ty = short_type | A User Theorem |
| subtype-03 | ⊦ is_subtype(byte_type, ty, claset) ↔ ty = byte_type | A User Theorem |
| subtype-04 | ⊦ is_subtype(mkclasstype(class), ty, claset) ↔ is_classtype(ty) ∧ class ∈ claset ∨ ty = mkclasstype(`java.lang.Object' .class) | A User Theorem |
| subtype-05 | ⊦ is_subtype(mkarraytype(ty0), ty, claset) ↔ is_arraytype(ty) ∧ is_subtype(ty0, ty .type, claset) ∨ ty = mkclasstype(`java.lang.Object' .class) | A User Theorem |
| subtype-06 | ⊦ is_subtype(void_type, ty, claset) ↔ ty = void_type | A User Theorem |
| subtype-07 | ⊦ is_subtype(abstract_type, ty, claset) ↔ ty = abstract_type | A User Theorem |
| subtype-08 | ⊦ is_subtype(long_type, ty, claset) ↔ ty = long_type | A User Theorem |
| subtype-09 | ⊦ is_subtype(char_type, ty, claset) ↔ ty = char_type | A User Theorem |
| subtype-10 | ⊦ is_subtype(float_type, ty, claset) ↔ ty = float_type | A User Theorem |
| subtype-11 | ⊦ is_subtype(double_type, ty, claset) ↔ ty = double_type | A User Theorem |
| subtype-cla-01 | class ≠ `java.lang.Object' .class ⊦ is_subtype(ty1, mkclasstype(class), claset) ↔ is_classtype(ty1) ∧ ty1 .class ∈ claset | A User Theorem |
| subtype-hasct | ⊦ ¬ has_classtype(ty) → (is_subtype(ty0, ty, claset) ↔ ty = ty0) | A User Theorem |
| subtype-noclasstype | ⊦ ¬ has_classtype(ty) → (ty ≤ ty0 ↔ ty = ty0 ∨ ty0 .jtdims < ty .jtdims ∧ has_classtype(ty0) ∧ ty0 .jtclass = `java.lang.Object' .class) | A User Theorem |
| subtype-norec | ⊦ has_classtype(ty) → ( ty ≤ ty0 ↔ ty .jtdims = ty0 .jtdims ∧ has_classtype(ty0) ∧ ty .jtclass ≤ ty0 .jtclass ∨ ty .jtdims > ty0 .jtdims ∧ has_classtype(ty0) ∧ ty0 .jtclass = `java.lang.Object' .class) | A User Theorem |
| subtype-object | ⊦ type∃(str, ty) → (ty ≤ mkclasstype(`java.lang.Object' .class) ↔ is_classtype(ty) ∨ is_arraytype(ty)) | A User Theorem |
| subtype-object-01 | ⊦ ty ≤ mkclasstype(`java.lang.Object' .class) ↔ is_classtype(ty) ∨ is_arraytype(ty) | A User Theorem |
| subtype-predef | ⊦ is_subtype(str, mkclasstype(`java.lang.NoClassDefFoundError' .class), ty) ↔ ¬ ¬ (is_classtype(ty) ∧ `java.lang.NoClassDefFoundError' .class ≤ ty .class) | A User Theorem |
| subtype-reflexivity | ⊦ is_subtype(str, ty, ty) ↔ ¬ has_classtype(ty) ∨ tdname+∃(str, ty .jtclass) | A User Theorem |
| tdname+predef | ⊦ tdname+∃(str, `java.lang.NoClassDefFoundError' .class) | A User Theorem |
| tdname+predef-01 | ⊦ tdname+∃(str, `java.lang.Object' .class) | A User Theorem |
| tdname+predef-02 | ⊦ tdname+∃(str, `java.lang.Throwable' .class) | A User Theorem |
| tdname+predef-03 | ⊦ tdname+∃(str, `java.lang.Error' .class) | A User Theorem |
| tdnameex | ⊦ class∃(str, class) → tdname∃(str, class) | A User Theorem |
| tdnameex-01 | ⊦ interface∃(str, class) → tdname∃(str, class) | A User Theorem |
| tdnameex-02 | ⊦ tdname∃(str, class) → tdname+∃(str, class) | A User Theorem |
| tdnameex-03 | ⊦ ¬ is_predefined_class(class) → (tdname+∃(str, class) ↔ tdname∃(str, class)) | A User Theorem |
| tdnameex-04 | ⊦ ¬ tdname+∃(str, class) → ¬ class+∃(str, class) | A User Theorem |
| tdnameex-05 | ⊦ ¬ tdname+∃(str, class) → ¬ class∃(str, class) | A User Theorem |
| tdnameex-06 | ⊦ ¬ interface∃(str, class) → (tdname+∃(str, class) ↔ class+∃(str, class)) | A User Theorem |
| tdnameex-07 | ⊦ interface∃(str, class) → tdname+∃(str, class) | A User Theorem |
| tdnameex-08 | ⊦ ¬ interface∃(str, class) → (tdname∃(str, class) ↔ class∃(str, class)) | A User Theorem |
| tdnameex-09 | ⊦ ¬ class∃(str, class) → (tdname∃(str, class) ↔ interface∃(str, class)) | A User Theorem |
| transitivity | ⊦ ty ≤ ty0 ∧ ty0 ≤ ty1 → ty ≤ ty1 | A User Theorem |
| transitivity-01 | ⊦ ty ≤ mkclasstype(class1) ∧ class1 ≤ class → ty ≤ mkclasstype(class) | A User Theorem |
| transitivity-02 | ⊦ class ≤ class1 ∧ mkclasstype(class1) ≤ ty → mkclasstype(class) ≤ ty | A User Theorem |
| typeex | ⊦ ¬ has_classtype(ty) → type∃(str, ty) | A User Theorem |
| typeex-01 | ⊦ ¬ class+∃(str, class) → (tdname+∃(str, class) ↔ interface∃(str, class)) | A User Theorem |
| typeex-02 | ⊦ ¬ type∃(str, ty) ∧ is_classtype(ty) → ¬ class+∃(str, ty .class) | A User Theorem |
| typeex-array | ⊦ type∃(str, mkarraytype(ty)) ↔ type∃(str, ty) | A User Theorem |
| typeex-class | ⊦ type∃(str, mkclasstype(class)) ↔ tdname+∃(str, class) | A User Theorem |
| typeex-hasnoclasstype | ⊦ ¬ type∃(str, ty) ∧ ¬ has_classtype(ty) → ¬ type∃(str0, ty) | A User Theorem |
| typeex-prim | ⊦ type∃(str, int_type) | A User Theorem |
| typeex-prim-01 | ⊦ type∃(str, boolean_type) | A User Theorem |
| typeex-prim-02 | ⊦ type∃(str, short_type) | A User Theorem |
| typeex-prim-03 | ⊦ type∃(str, byte_type) | A User Theorem |
| typeex-prim-04 | ⊦ type∃(str, long_type) | A User Theorem |
| typeex-prim-05 | ⊦ type∃(str, float_type) | A User Theorem |
| typeex-prim-06 | ⊦ type∃(str, double_type) | A User Theorem |
| typeex-prim-07 | ⊦ type∃(str, char_type) | A User Theorem |
| typeex-prim-08 | ⊦ type∃(str, void_type) | A User Theorem |
| typele-elemtype | ⊦ ¬ ty .jtelemtype ≤ ty0 .jtelemtype ∧ ty0 .jtelemtype ≠ mkclasstype(`java.lang.Object' .class) → ¬ ty ≤ ty0 | A User Theorem |
| typele-elemtype-01 | ⊦ ty ≤ ty0 ∧ ty0 .jtelemtype ≠ mkclasstype(`java.lang.Object' .class) → ty .jtelemtype ≤ ty0 .jtelemtype | A User Theorem |
| typele-object | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → ¬ ty ≤ mkclasstype(`java.lang.Object' .class) | A User Theorem |
| typex-jtelemtype | ⊦ ¬ type∃(str, ty .jtelemtype) → ¬ type∃(str, ty) | A User Theorem |