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: |
|---|---|---|
| disj-01 | ⊦ boolean_type ≠ int_type | An Axiom |
| disj-04 | ⊦ boolean_type ≠ mkclasstype(class) | An Axiom |
| disj-05 | ⊦ boolean_type ≠ mkarraytype(ty) | An Axiom |
| disj-09 | ⊦ mkclasstype(class) ≠ void_type | An Axiom |
| disj-10 | ⊦ int_type ≠ mkarraytype(ty) | An Axiom |
| disj-13 | ⊦ int_type ≠ mkclasstype(class) | An Axiom |
| disj-16 | ⊦ short_type ≠ mkclasstype(class) | An Axiom |
| sel-01 | ⊦ mkarraytype(ty) .type = ty | An Axiom |
| sel-02 | ⊦ mkclasstype(class) .class = class | An Axiom |
| test-09 | ⊦ is_arraytype(mkarraytype(ty)) | An Axiom |
| test-10 | ⊦ is_classtype(mkclasstype(class)) | An Axiom |
| test-13 | ⊦ ¬ is_arraytype(int_type) | An Axiom |
| test-14 | ⊦ ¬ is_arraytype(boolean_type) | An Axiom |
| test-16 | ⊦ ¬ is_classtype(mkarraytype(ty)) | An Axiom |
| test-17 | ⊦ ¬ is_void_type(mkclasstype(class)) | An Axiom |
| test-20 | ⊦ ¬ is_classtype(int_type) | An Axiom |
| test-21 | ⊦ ¬ is_classtype(boolean_type) | An Axiom |
| inj-01 | ⊦ mkarraytype(ty) = mkarraytype(ty0) ↔ ty = ty0 | An Axiom |
| inj-02 | ⊦ mkclasstype(class) = mkclasstype(class0) ↔ class = class0 | An Axiom |
| case | ⊦ ty = boolean_type ∨ ty = int_type ∨ ty = short_type ∨ ty = byte_type ∨ ty = long_type ∨ ty = float_type ∨ ty = double_type ∨ ty = char_type ∨ ty = mkclasstype(ty .class) ∨ ty = mkarraytype(ty .type) ∨ ty = void_type ∨ ty = abstract_type | An Axiom |
| ex-02 | ⊦ is_arraytype(ty) ↔ (∃ ty0. ty = mkarraytype(ty0)) | An Axiom |
| ex-03 | ⊦ is_classtype(ty) ↔ (∃ class. ty = mkclasstype(class)) | An Axiom |
| elim-01 | ⊦ is_arraytype(ty) → (ty0 = ty .type ↔ ty = mkarraytype(ty0)) | An Axiom |
| elim-02 | ⊦ is_classtype(ty) → (class = ty .class ↔ ty = mkclasstype(class)) | An Axiom |
| ex-04 | ⊦ is_void_type(ty) ↔ ty = void_type | An Axiom |
| test-22 | ⊦ ¬ is_classtype(void_type) | An Axiom |
| test-23 | ⊦ ¬ is_arraytype(void_type) | An Axiom |
| test-24 | ⊦ ¬ is_void_type(boolean_type) | An Axiom |
| test-25 | ⊦ ¬ is_void_type(int_type) | An Axiom |
| test-28 | ⊦ ¬ is_arraytype(mkclasstype(class)) | An Axiom |
| test-29 | ⊦ ¬ is_void_type(mkarraytype(ty)) | An Axiom |
| test-30 | ⊦ is_void_type(void_type) | An Axiom |
| disj-22 | ⊦ mkarraytype(ty) ≠ void_type | An Axiom |
| disj-26 | ⊦ int_type ≠ void_type | An Axiom |
| disj-27 | ⊦ boolean_type ≠ void_type | An Axiom |
| gen | An Axiom | |
| test-01 | ⊦ ¬ is_classtype(short_type) | An Axiom |
| test-02 | ⊦ ¬ is_classtype(byte_type) | An Axiom |
| test-03 | ⊦ ¬ is_arraytype(short_type) | An Axiom |
| test-04 | ⊦ ¬ is_arraytype(byte_type) | An Axiom |
| test-05 | ⊦ ¬ is_void_type(short_type) | An Axiom |
| test-06 | ⊦ ¬ is_void_type(byte_type) | An Axiom |
| disj-06 | ⊦ byte_type ≠ void_type | An Axiom |
| disj-11 | ⊦ byte_type ≠ mkarraytype(ty) | An Axiom |
| disj-15 | ⊦ mkclasstype(class) ≠ mkarraytype(ty) | An Axiom |
| disj-21 | ⊦ short_type ≠ void_type | An Axiom |
| disj-28 | ⊦ short_type ≠ mkarraytype(ty) | An Axiom |
| disj-29 | ⊦ byte_type ≠ mkclasstype(class) | An Axiom |
| disj-32 | ⊦ short_type ≠ byte_type | An Axiom |
| disj-33 | ⊦ int_type ≠ byte_type | An Axiom |
| disj-34 | ⊦ int_type ≠ short_type | An Axiom |
| disj-35 | ⊦ boolean_type ≠ byte_type | An Axiom |
| disj-36 | ⊦ boolean_type ≠ short_type | An Axiom |
| test-07 | ⊦ ¬ is_classtype(abstract_type) | An Axiom |
| test-08 | ⊦ ¬ is_arraytype(abstract_type) | An Axiom |
| test-11 | ⊦ ¬ is_void_type(abstract_type) | An Axiom |
| disj-02 | ⊦ void_type ≠ abstract_type | An Axiom |
| disj-03 | ⊦ mkarraytype(ty) ≠ abstract_type | An Axiom |
| disj-07 | ⊦ mkclasstype(class) ≠ abstract_type | An Axiom |
| disj-08 | ⊦ byte_type ≠ abstract_type | An Axiom |
| disj-12 | ⊦ short_type ≠ abstract_type | An Axiom |
| disj-14 | ⊦ int_type ≠ abstract_type | An Axiom |
| disj-17 | ⊦ boolean_type ≠ abstract_type | An Axiom |
| test-12 | ⊦ ¬ is_classtype(long_type) | An Axiom |
| test-15 | ⊦ ¬ is_classtype(float_type) | An Axiom |
| test-18 | ⊦ ¬ is_classtype(double_type) | An Axiom |
| test-19 | ⊦ ¬ is_classtype(char_type) | An Axiom |
| test-26 | ⊦ ¬ is_arraytype(long_type) | An Axiom |
| test-27 | ⊦ ¬ is_arraytype(float_type) | An Axiom |
| test-31 | ⊦ ¬ is_arraytype(double_type) | An Axiom |
| test-32 | ⊦ ¬ is_arraytype(char_type) | An Axiom |
| test-33 | ⊦ ¬ is_void_type(long_type) | An Axiom |
| test-34 | ⊦ ¬ is_void_type(float_type) | An Axiom |
| test-35 | ⊦ ¬ is_void_type(double_type) | An Axiom |
| test-36 | ⊦ ¬ is_void_type(char_type) | An Axiom |
| disj-18 | ⊦ char_type ≠ abstract_type | An Axiom |
| disj-19 | ⊦ char_type ≠ void_type | An Axiom |
| disj-20 | ⊦ char_type ≠ mkarraytype(ty) | An Axiom |
| disj-23 | ⊦ char_type ≠ mkclasstype(class) | An Axiom |
| disj-24 | ⊦ double_type ≠ abstract_type | An Axiom |
| disj-25 | ⊦ double_type ≠ void_type | An Axiom |
| disj-30 | ⊦ double_type ≠ mkarraytype(ty) | An Axiom |
| disj-31 | ⊦ double_type ≠ mkclasstype(class) | An Axiom |
| disj-37 | ⊦ double_type ≠ char_type | An Axiom |
| disj-38 | ⊦ float_type ≠ abstract_type | An Axiom |
| disj-39 | ⊦ float_type ≠ void_type | An Axiom |
| disj-40 | ⊦ float_type ≠ mkarraytype(ty) | An Axiom |
| disj-41 | ⊦ float_type ≠ mkclasstype(class) | An Axiom |
| disj-42 | ⊦ float_type ≠ char_type | An Axiom |
| disj-43 | ⊦ float_type ≠ double_type | An Axiom |
| disj-44 | ⊦ long_type ≠ abstract_type | An Axiom |
| disj-45 | ⊦ long_type ≠ void_type | An Axiom |
| disj-46 | ⊦ long_type ≠ mkarraytype(ty) | An Axiom |
| disj-47 | ⊦ long_type ≠ mkclasstype(class) | An Axiom |
| disj-48 | ⊦ long_type ≠ char_type | An Axiom |
| disj-49 | ⊦ long_type ≠ double_type | An Axiom |
| disj-50 | ⊦ long_type ≠ float_type | An Axiom |
| disj-51 | ⊦ byte_type ≠ char_type | An Axiom |
| disj-52 | ⊦ byte_type ≠ double_type | An Axiom |
| disj-53 | ⊦ byte_type ≠ float_type | An Axiom |
| disj-54 | ⊦ byte_type ≠ long_type | An Axiom |
| disj-55 | ⊦ short_type ≠ char_type | An Axiom |
| disj-56 | ⊦ short_type ≠ double_type | An Axiom |
| disj-57 | ⊦ short_type ≠ float_type | An Axiom |
| disj-58 | ⊦ short_type ≠ long_type | An Axiom |
| disj-59 | ⊦ int_type ≠ char_type | An Axiom |
| disj-60 | ⊦ int_type ≠ double_type | An Axiom |
| disj-61 | ⊦ int_type ≠ float_type | An Axiom |
| disj-62 | ⊦ int_type ≠ long_type | An Axiom |
| disj-63 | ⊦ boolean_type ≠ char_type | An Axiom |
| disj-64 | ⊦ boolean_type ≠ double_type | An Axiom |
| disj-65 | ⊦ boolean_type ≠ float_type | An Axiom |
| disj-66 | ⊦ boolean_type ≠ long_type | An Axiom |
| arraytype | ⊦ is_arraytype(ty) → mkarraytype(ty .type) = ty | A User Theorem |
| diff | ⊦ is_classtype(ty) → ¬ is_arraytype(ty) | A User Theorem |
| diff-01 | ⊦ is_arraytype(ty) → ¬ is_classtype(ty) | A User Theorem |