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: |
|---|---|---|
| contains-type-def | ⊦ contains(str, ty, ty0) ↔ (∃ tys. contains(str, ty ' + (tys + ty0))) | An Axiom |
| contains-one | ⊦ contains(str, ty ') ↔ type∃(str, ty) | An Axiom |
| contains-rec | ⊦ contains(str, ty ' + ty0 ' + tys) ↔ type∃(str, ty) ∧ is_reftype(ty) ∧ (∃ ty1. ty1 ≤ ty ∧ type∃(str, ty1) ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ (∃ fs. fs ' ∈ instfields(ty1 .class) ∧ ty0 ≤ fs .type)) ∧ (is_arraytype(ty1) → ty0 ≤ ty1 .type) ∧ contains(str, ty0 ' + tys)) | An Axiom |
| contains-field-def | ⊦ contains(str, ty, fs) ↔ type∃(str, ty) ∧ (∃ tys. tys ≠ [] ∧ tys .first ≤ ty ∧ contains(str, tys) ∧ is_reftype(tys .last) ∧ (is_classtype(tys .last) → ¬ interface∃(str, tys .last .class) ∧ fs ' ∈ instfields(tys .last .class)) ∧ (is_arraytype(tys .last) → fs ' = _length)) | An Axiom |
| same-subclasses-all-def | ⊦ same-subclasses-contains(class, str, str0) ↔ same-subclasses(class, str, str0) ∧ (∀ class0. contains(str0, mkclasstype(class), mkclasstype(class0)) → same-subclasses(class0, str, str0)) | An Axiom |
| contains-append | ⊦ contains(str, tys + ty ' + tys0) ↔ contains(str, tys + ty ') ∧ contains(str, ty ' + tys0) | A User Theorem |
| contains-array | ⊦ ¬ contains(str, ty ' + tys .rest) ∧ tys ≠ [] → ¬ contains(str, mkarraytype(ty) ' + tys) | A User Theorem |
| contains-array-elemtype | ⊦ contains(str, ty, mkarraytype(ty0)) → contains(str, ty, ty0) | A User Theorem |
| contains-array-elemtype-01 | ⊦ contains(str, ty, ty0) → contains(str, ty, ty0 .jtelemtype) | A User Theorem |
| contains-array-elemtype-02 | ⊦ contains(str, ty .jtelemtype, ty0) → contains(str, ty, ty0) | A User Theorem |
| contains-array-elemtype-04 | ⊦ ty .jtelemtype = ty0 ∧ ty ≠ ty0 ∧ type∃(str, ty) → contains(str, ty, ty0) | A User Theorem |
| contains-array-elemtype-05 | ⊦ contains(str, ty, mkclasstype(class)) ∧ ¬ mkclasstype(class) ≤ ty .jtelemtype → contains(str, ty .jtelemtype, mkclasstype(class)) | A User Theorem |
| contains-array-elemtype-06 | ⊦ contains(str, ty, ty0) ∧ ¬ ty0 .jtelemtype ≤ ty .jtelemtype ∧ ty .jtelemtype ≠ mkclasstype(`java.lang.Object' .class) → contains(str, ty .jtelemtype, ty0 .jtelemtype) | A User Theorem |
| contains-array-elemtype-07 | ⊦ contains(str, mkarraytype(ty), mkarraytype(ty0)) ∧ ty ≠ mkclasstype(`java.lang.Object' .class) → contains(str, ty, ty0) | A User Theorem |
| contains-array-elemtype-08 | ⊦ contains(str, mkarraytype(ty), ty0) ↔ ty0 ≤ ty ∧ type∃(str, ty) ∧ type∃(str, ty0) ∨ contains(str, ty, ty0) | A User Theorem |
| contains-array-elemtype-09 | ⊦ ty0 ≤ ty → (contains(str, mkarraytype(ty), ty0) ↔ ¬ ¬ (type∃(str, ty) ∧ type∃(str, ty0))) | A User Theorem |
| contains-array-elemtype-10 | ⊦ contains(str, ty, ty0) → contains(str, mkarraytype(ty), ty0) | A User Theorem |
| contains-array-elemtype-11 | ⊦ contains(str, ty, ty0) ∧ ¬ ty0 ≤ ty .jtelemtype ∧ ¬ is_arraytype(ty0) → contains(str, ty .jtelemtype, ty0) | A User Theorem |
| contains-array-elemtype-ex | contains(str, ty + (tys + mkclasstype(class))), ¬ mkclasstype(class) ≤ ty .jtelemtype ⊦ ∃ tys1. # tys1 ≤ # tys ∧ contains(str, ty .jtelemtype + (tys1 + mkclasstype(class))) | A User Theorem |
| contains-bool | ⊦ contains(str, boolean_type ' + tys) ↔ tys = [] | A User Theorem |
| contains-boolarray | ⊦ contains(str, mkarraytype(boolean_type) ' + tys + ty ') ↔ tys = [] ∧ ty = boolean_type | A User Theorem |
| contains-boolarray-01 | ⊦ tys ≠ [] → (contains(str, mkarraytype(boolean_type) ' + tys) ↔ tys = boolean_type ') | A User Theorem |
| contains-boolarray-02 | ⊦ contains(`docs2store', mkarraytype(boolean_type) ' + ty ') ↔ ty = boolean_type | A User Theorem |
| contains-boolarray-03 | ⊦ contains(`docs2store', mkarraytype(boolean_type), ty) ↔ ty = boolean_type | A User Theorem |
| contains-byte | ⊦ contains(str, byte_type ' + tys) ↔ tys = [] | A User Theorem |
| contains-bytearray | ⊦ contains(str, mkarraytype(byte_type) ' + tys + ty ') ↔ tys = [] ∧ ty = byte_type | A User Theorem |
| contains-bytearray-01 | ⊦ tys ≠ [] → (contains(str, mkarraytype(byte_type) ' + tys) ↔ tys = byte_type ') | A User Theorem |
| contains-bytearray-02 | ⊦ contains(`docs2store', mkarraytype(byte_type) ' + ty ') ↔ ty = byte_type | A User Theorem |
| contains-bytearray-03 | ⊦ contains(`docs2store', mkarraytype(byte_type), ty) ↔ ty = byte_type | A User Theorem |
| contains-bytearray-04 | ⊦ contains(str, mkarraytype(byte_type), ty) ↔ ty = byte_type | A User Theorem |
| contains-field-def-case | ⊦ contains(str, ty, fs) ↔ type∃(str, ty) ∧ (∃ ty1. (ty1 ≤ ty ∧ type∃(str, ty1) ∨ contains(str, ty, ty1)) ∧ is_reftype(ty1) ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ fs ' ∈ instfields(ty1 .class)) ∧ (is_arraytype(ty1) → fs ' = _length)) | A User Theorem |
| contains-int | ⊦ contains(str, int_type ' + tys) ↔ tys = [] | A User Theorem |
| contains-intarray | ⊦ contains(str, mkarraytype(int_type) ' + tys + ty ') ↔ tys = [] ∧ ty = int_type | A User Theorem |
| contains-intarray-01 | ⊦ tys ≠ [] → (contains(str, mkarraytype(int_type) ' + tys) ↔ tys = int_type ') | A User Theorem |
| contains-intarray-02 | ⊦ contains(`docs2store', mkarraytype(int_type) ' + ty ') ↔ ty = int_type | A User Theorem |
| contains-intarray-03 | ⊦ contains(`docs2store', mkarraytype(int_type), ty) ↔ ty = int_type | A User Theorem |
| contains-length | ⊦ is_arraytype(ty) ∧ fs ' = _length → (contains(str, ty, fs) ↔ type∃(str, ty)) | A User Theorem |
| contains-levelsubset | ⊦ contains(str, ty, ty0) ∧ level⊆(str, str0) → contains(str0, ty, ty0) | A User Theorem |
| contains-no-reftype | ⊦ ¬ is_reftype(ty) → ¬ contains(str, ty, ty0) | A User Theorem |
| contains-not-has-classtype | ⊦ ¬ has_classtype(ty) → ¬ contains(str, ty, mkclasstype(class)) | A User Theorem |
| contains-not-has-classtype-01 | ⊦ ¬ has_classtype(ty) ∧ has_classtype(ty0) → ¬ contains(str, ty, ty0) | A User Theorem |
| contains-not-hasclasstype-level | ⊦ ¬ has_classtype(ty) → (contains(str, ty, ty0) ↔ contains(str0, ty, ty0)) | A User Theorem |
| contains-not-hasclasstype-level-01 | ⊦ ¬ has_classtype(ty) ∧ contains(str, ty, ty0) → contains(str0, ty, ty0) | A User Theorem |
| contains-objectarray | ⊦ ty .jtelemtype = mkclasstype(`java.lang.Object' .class) → ( contains(str, ty, ty0) ↔ type∃(str, ty0) ∧ ty0 ≤ mkclasstype(`java.lang.Object' .class) ∧ is_arraytype(ty) ∨ contains(str, mkclasstype(`java.lang.Object' .class), ty0)) | A User Theorem |
| contains-predefined | ⊦ is_predefined_class(class) ∧ class ≠ `java.lang.Object' .class ∧ (∀ class0. tdname+∃(str, class0) ∧ class0 ≤ class → is_predefined_class(class0)) → ¬ contains(str, mkclasstype(class), ty) | A User Theorem |
| contains-primtype | ⊦ ¬ contains(str, byte_type, ty) | A User Theorem |
| contains-primtype-01 | ⊦ ¬ contains(str, short_type, ty) | A User Theorem |
| contains-primtype-02 | ⊦ ¬ contains(str, int_type, ty) | A User Theorem |
| contains-primtype-03 | ⊦ ¬ contains(str, boolean_type, ty) | A User Theorem |
| contains-primtype-04 | ⊦ is_primtype(ty) → (contains(str, ty ' + tys) ↔ tys = []) | A User Theorem |
| contains-primtype-05 | ⊦ ¬ has_classtype(ty) → (contains(str, ty .jtelemtype ' + tys) ↔ tys = []) | A User Theorem |
| contains-rec-01 | ⊦ tys ≠ [] → ( contains(str, ty ' + tys) ↔ type∃(str, ty) ∧ is_reftype(ty) ∧ (∃ ty1. ty1 ≤ ty ∧ type∃(str, ty1) ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ (∃ fs. fs ' ∈ instfields(ty1 .class) ∧ tys .first ≤ fs .type)) ∧ (is_arraytype(ty1) → tys .first ≤ ty1 .type) ∧ contains(str, tys))) | A User Theorem |
| contains-short | ⊦ contains(str, short_type ' + tys) ↔ tys = [] | A User Theorem |
| contains-shortarray | ⊦ contains(str, mkarraytype(short_type) ' + tys + ty ') ↔ tys = [] ∧ ty = short_type | A User Theorem |
| contains-shortarray-01 | ⊦ tys ≠ [] → (contains(str, mkarraytype(short_type) ' + tys) ↔ tys = short_type ') | A User Theorem |
| contains-shortarray-02 | ⊦ contains(`docs2store', mkarraytype(short_type) ' + ty ') ↔ ty = short_type | A User Theorem |
| contains-shortarray-03 | ⊦ contains(`docs2store', mkarraytype(short_type), ty) ↔ ty = short_type | A User Theorem |
| contains-subex | ⊦ (∀ ty1. contains(str0, ty, ty1) → type∃(str, ty1)) ↔ (∀ class1. contains(str0, ty, mkclasstype(class1)) → tdname+∃(str, class1)) | A User Theorem |
| contains-subspec | ⊦ contains(str0, ty, ty0) ∧ type∃(str, ty) ∧ level⊆(str0, str) ∧ same-subclasses-contains(ty .jtelemtype .class, str, str0) → contains(str, ty, ty0) | A User Theorem |
| contains-subspec-better | ⊦ contains(str0, ty, ty0) ∧ type∃(str, ty) ∧ same-subclasses-contains(ty .jtelemtype .class, str, str0) → contains(str, ty, ty0) | A User Theorem |
| contains-subtype | ⊦ contains(str, ty, ty1) ∧ ty0 ≤ ty1 ∧ type∃(str, ty0) → contains(str, ty, ty0) | A User Theorem |
| contains-subtype-01 | ⊦ ¬ contains(str, ty, ty0) ∧ ty0 ≤ ty1 ∧ type∃(str, ty0) → ¬ contains(str, ty, ty1) | A User Theorem |
| contains-supertype | ⊦ contains(str, ty ' + tys) ∧ ty ≤ ty0 ∧ type∃(str, ty0) → contains(str, ty0 ' + tys) | A User Theorem |
| contains-supertype-01 | ⊦ ¬ contains(str, ty0 ' + tys) ∧ ty ≤ ty0 ∧ type∃(str, ty0) → ¬ contains(str, ty ' + tys) | A User Theorem |
| contains-supertype-02 | ⊦ contains(str, ty, fs) ∧ ty ≤ ty0 ∧ type∃(str, ty0) → contains(str, ty0, fs) | A User Theorem |
| contains-supertype-03 | ⊦ ¬ contains(str, ty0, ty1) ∧ ty ≤ ty0 ∧ type∃(str, ty0) → ¬ contains(str, ty, ty1) | A User Theorem |
| contains-supertype-04 | ⊦ contains(str, ty, ty1) ∧ ty ≤ ty0 ∧ type∃(str, ty0) → contains(str, ty0, ty1) | A User Theorem |
| contains-supertype-05 | ⊦ ¬ contains(str, ty0, fs) ∧ ty ≤ ty0 ∧ type∃(str, ty0) → ¬ contains(str, ty, fs) | A User Theorem |
| contains-trans | ⊦ contains(str, ty, ty0) ∧ contains(str, ty0, ty1) → contains(str, ty, ty1) | A User Theorem |
| contains-trans-01 | ⊦ contains(str, ty ' + tys + ty0 ') ∧ contains(str, ty0 ' + tys0 + ty1 ') → contains(str, ty ' + tys + ty0 ' + tys0 + ty1 ') | A User Theorem |
| contains-two | ⊦ contains(str, ty ' + ty0 ') ↔ type∃(str, ty) ∧ is_reftype(ty) ∧ (∃ ty1. ty1 ≤ ty ∧ type∃(str, ty1) ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ (∃ fs. fs ' ∈ instfields(ty1 .class) ∧ ty0 ≤ fs .type)) ∧ (is_arraytype(ty1) → ty0 ≤ ty1 .type) ∧ type∃(str, ty0)) | A User Theorem |
| contains-type-def-nodups | ⊦ contains(str, ty, ty0) ↔ (∃ tys. contains(str, ty ' + (tys + ty0)) ∧ ¬ dups(ty ' + tys)) | A User Theorem |
| contains-type-rec | ⊦ contains(str, ty, ty0) ↔ type∃(str, ty) ∧ is_reftype(ty) ∧ ( (∃ ty1. ty1 ≤ ty ∧ type∃(str, ty1) ∧ type∃(str, ty0) ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ (∃ fs. fs ' ∈ instfields(ty1 .class) ∧ ty0 ≤ fs .type)) ∧ (is_arraytype(ty1) → ty0 ≤ ty1 .type)) ∨ (∃ ty1, ty2. ty1 ≤ ty ∧ type∃(str, ty1) ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ (∃ fs. fs ' ∈ instfields(ty1 .class) ∧ ty2 ≤ fs .type)) ∧ (is_arraytype(ty1) → ty2 ≤ ty1 .type) ∧ contains(str, ty2, ty0))) | A User Theorem |
| contains-typeex | ⊦ ¬ type∃(str, ty) → ¬ contains(str, ty ' + tys) | A User Theorem |
| contains-typeex-01 | ⊦ ¬ type∃(str, ty) → ¬ contains(str, mkarraytype(ty) ' + tys) | A User Theorem |
| contains-typeex-02 | ⊦ ¬ type∃(str, ty) → ¬ contains(str, ty, ty0) | A User Theorem |
| contains-typeex-03 | ⊦ ¬ type∃(str, ty0) → ¬ contains(str, ty, ty0) | A User Theorem |
| contains-typeex-04 | ⊦ ¬ type∃(str, ty) ∧ ty ∈ tys → ¬ contains(str, tys) | A User Theorem |
| contains-typeex-05 | ⊦ ¬ type∃(str, ty) → ¬ contains(str, tys + ty ') | A User Theorem |
| junkref-put-other-fieldclass | ⊦ ¬ junkref(str, r, st) ∧ ¬ contains(str, st[r -- _type] .type, fs) ∧ fs ' ≠ _type → ¬ junkref(str, r, st[r0 -- fs ', val]) | A User Theorem |
| junkref-subspec-samesubclasses | ⊦ ¬ junkref(str0, r, st) ∧ same-subclasses-contains(st[r -- _type] .type .jtelemtype .class, str, str0) → ¬ junkref(str, r, st) | A User Theorem |
| nopathex-badarrayfield | ⊦ ¬ contains(str, st[r -- _type] .type, fs) ∧ fs ' ≠ _type ∧ is_arraytype(st[r0 -- _type] .type) ∧ fs ' = _length ∧ r0 ≠ jvmref → ¬ path∃(str, r, r0, st) | A User Theorem |
| nopathex-badclassfield | ⊦ ¬ contains(str, st[r -- _type] .type, fs) ∧ fs ' ≠ _type ∧ is_classtype(st[r0 -- _type] .type) ∧ fs ' ∈ instfields(st[r0 -- _type] .type .class) ∧ r0 ≠ jvmref → ¬ path∃(str, r, r0, st) | A User Theorem |
| nopathex-runtimetype | ⊦ ¬ contains(str, st[r -- _type] .type, st[r0 -- _type] .type) ∧ r ≠ r0 ∧ r0 ≠ jvmref → ¬ path∃(str, r, r0, st) | A User Theorem |
| same-subclasses | same-subclasses-contains(class, str, str0) ⊦ ∀ ty. contains(str0, mkclasstype(class), ty) → type∃(str, ty) | A User Theorem |
| same-subclasses-01 | same-subclasses-contains(class, str, str0) ⊦ ∀ class0. contains(str0, mkclasstype(class), mkclasstype(class0)) → tdname+∃(str, class0) | A User Theorem |
| same-subclasses-array-forward | ⊦ is_array(str, r, st) ∧ same-subclasses-contains(st[r -- _type] .type .jtelemtype .class, str, str0) ∧ r0 ≠ jvmref ∧ st[r -- i '] = refval(r0) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ ¬ junkref(str0, r, st) ∧ has_classtype(st[r0 -- _type] .type) → same-subclasses-contains(st[r0 -- _type] .type .jtelemtype .class, str, str0) | A User Theorem |
| same-subclasses-class-forward | ⊦ is_obj(str, r, st) ∧ same-subclasses-contains(st[r -- _type] .type .jtelemtype .class, str, str0) ∧ r0 ≠ jvmref ∧ st[r -- mkfs(class, ty, fieldvar) '] = refval(r0) ∧ mkfs(class, ty, fieldvar) ' ∈ instfields(st[r -- _type] .type .class) ∧ ¬ junkref(str0, r, st) ∧ has_classtype(st[r0 -- _type] .type) → same-subclasses-contains(st[r0 -- _type] .type .jtelemtype .class, str, str0) | A User Theorem |
| same-subclasses-contains-tdnameex | ⊦ tdname+∃(str0, class) ∧ ¬ tdname+∃(str, class) → ¬ same-subclasses-contains(class, str, str0) | A User Theorem |
| same-subclasses-contains-tdnameex-01 | ⊦ tdname∃(str0, class) ∧ ¬ tdname∃(str, class) → ¬ same-subclasses-contains(class, str, str0) | A User Theorem |
| same-subclasses-contains-tdnameex-02 | ⊦ tdname∃(str0, class) ∧ ¬ tdname∃(str, class) ∧ class ≤ class0 → ¬ same-subclasses-contains(class0, str, str0) | A User Theorem |
| same-subclasses-contains-tdnameex-03 | ⊦ tdname+∃(str0, class) ∧ ¬ tdname+∃(str, class) ∧ class ≤ class0 → ¬ same-subclasses-contains(class0, str, str0) | A User Theorem |
| same-subclasses-contains-trans | ⊦ same-subclasses-contains(class, str, str0) ∧ same-subclasses-contains(class, str0, str1) → same-subclasses-contains(class, str, str1) | A User Theorem |
| same-subclasses-contains-typeex | ⊦ type∃(str0, ty) ∧ ¬ type∃(str, ty) → ¬ same-subclasses-contains(ty .jtelemtype .class, str, str0) | A User Theorem |
| same-subclasses-contains-typeex-01 | ⊦ ¬ type∃(str, ty0) ∧ contains(str0, ty, ty0) → ¬ same-subclasses-contains(ty .jtelemtype .class, str, str0) | A User Theorem |
| same-subclasses-contains-typeex-02 | ⊦ type∃(str0, ty) ∧ ¬ type∃(str, ty) ∧ ty ≤ ty0 → ¬ same-subclasses-contains(ty0 .jtelemtype .class, str, str0) | A User Theorem |
| same-subclasses-forward | ⊦ same-subclasses-contains(ty .jtelemtype .class, str, str0) ∧ has_classtype(ty3) ∧ is_reftype(ty) ∧ type∃(str0, ty) ∧ type∃(str0, ty1) ∧ type∃(str0, ty3) ∧ ty1 ≤ ty ∧ (is_arraytype(ty1) → ty3 ≤ ty1 .type) ∧ (is_classtype(ty1) → ¬ interface∃(str0, ty1 .class) ∧ mkfs(class, ty2, fieldvar) ' ∈ instfields(ty1 .class) ∧ ty3 ≤ ty2) → same-subclasses-contains(ty3 .jtelemtype .class, str, str0) | A User Theorem |
| same-subclasses-is-array | ⊦ ¬ is_array(str, r, st) ∧ is_array(str0, r, st) → ¬ same-subclasses-contains(st[r -- _type] .type .jtelemtype .class, str, str0) | A User Theorem |
| same-subclasses-is-obj | ⊦ ¬ is_obj(str, r, st) ∧ is_obj(str0, r, st) → ¬ same-subclasses-contains(st[r -- _type] .type .jtelemtype .class, str, str0) | A User Theorem |
| same-subclasses-subclass | ⊦ same-subclasses-contains(class, str, str0) ∧ class0 ≤ class ∧ tdname+∃(str0, class) → same-subclasses-contains(class0, str, str0) | A User Theorem |
| validref-subspec-samesubclasses | ⊦ validref(str0, r, mkclasstype(class), st) ∧ same-subclasses-contains(class, str, str0) ∧ tdname+∃(str0, class) → validref(str, r, mkclasstype(class), st) | A User Theorem |
| validref-subspec-samesubclasses-01 | ⊦ validref(str0, r, ty, st) ∧ same-subclasses-contains(ty .jtelemtype .class, str, str0) ∧ tdname+∃(str0, ty .jtelemtype .class) → validref(str, r, ty, st) | A User Theorem |
| validrefs-not-contains | ⊦ ¬ contains(str, st[refs .first -- _type] .type, st[refs .last -- _type] .type) ∧ refs ≠ [] ∧ refs .first ≠ refs .last ∧ refs .last ≠ jvmref → ¬ validrefs(str, refs, ty, st) | A User Theorem |
| validstatfield-subspec-samesubclasses | ⊦ validstatfield(str0, sk, st) ∧ same-subclasses-contains(sk .fs .type .jtelemtype .class, str, str0) ∧ type∃(str, sk .fs .type) ∧ tdname∃(str, sk .fs .class) → validstatfield(str, sk, st) | A User Theorem |