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: |
|---|---|---|
| all-classes | ⊦ ¬ (∀ class. ∃ r, ty, fieldvar. r -- mkfs(class, ty, fieldvar) ' ∈ st) | A User Theorem |
| all-classes-01 | ⊦ ∀ rks. ∃ class. ∀ r, ty, fieldvar. ¬ r -- mkfs(class, ty, fieldvar) ' ∈ rks | A User Theorem |
| all-classes-02 | ⊦ ∃ str. ∀ rk. rk ∈ rks ∧ is_fskey(rk .key) → # rk .key .fs .class .class < # str | A User Theorem |
| arraytype-in | ⊦ r -- mkfs(class0, mkarraytype(ty), fieldvar) ' ∈ st[_mode, val] ↔ r -- mkfs(class0, mkarraytype(ty), fieldvar) ' ∈ st | A User Theorem |
| at-mode | ⊦ ty ≠ void_type → (st[r -- mkfs(class, ty, fieldvar) ', val][_mode]) = st[_mode] | A User Theorem |
| at-other | ⊦ (st[r -- i ', val][r0 -- fs ']) = st[r0 -- fs '] | A User Theorem |
| at-other-01 | ⊦ (st[r0 -- fs ', val][r -- i ']) = st[r -- i '] | A User Theorem |
| at-other-02 | ⊦ (st[r0 -- mkfs(class, byte_type, fieldvar) ', val][r -- _type]) = st[r -- _type] | A User Theorem |
| at-other-03 | ⊦ (st[r0 -- mkfs(class, short_type, fieldvar) ', val][r -- _type]) = st[r -- _type] | A User Theorem |
| at-other-04 | ⊦ (st[r0 -- mkfs(class, int_type, fieldvar) ', val][r -- _type]) = st[r -- _type] | A User Theorem |
| at-other-05 | ⊦ (st[r0 -- mkfs(class, boolean_type, fieldvar) ', val][r -- _type]) = st[r -- _type] | A User Theorem |
| at-other-06 | ⊦ (st[r0 -- mkfs(class, mkclasstype(class0), fieldvar) ', val][r -- _type]) = st[r -- _type] | A User Theorem |
| at-other-07 | ⊦ (st[r0 -- mkfs(class, mkarraytype(ty), fieldvar) ', val][r -- _type]) = st[r -- _type] | A User Theorem |
| at-other-08 | ⊦ (st[r0 -- mkfs(class, mkclasstype(class0), fieldvar) ', val][r -- mkfs(class1, mkarraytype(ty), fieldvar0) ']) = st[r -- mkfs(class1, mkarraytype(ty), fieldvar0) '] | A User Theorem |
| at-other-09 | ⊦ (st[r0 -- mkfs(class1, mkarraytype(ty), fieldvar0) ', val][r -- mkfs(class, mkclasstype(class0), fieldvar) ']) = st[r -- mkfs(class, mkclasstype(class0), fieldvar) '] | A User Theorem |
| at-other-10 | ⊦ (st[r0 -- mkfs(class, byte_type, fieldvar) ', val][_mode]) = st[_mode] | A User Theorem |
| at-other-11 | ⊦ (st[r0 -- mkfs(class, short_type, fieldvar) ', val][_mode]) = st[_mode] | A User Theorem |
| at-other-12 | ⊦ (st[r0 -- mkfs(class, int_type, fieldvar) ', val][_mode]) = st[_mode] | A User Theorem |
| at-other-13 | ⊦ (st[r0 -- mkfs(class, boolean_type, fieldvar) ', val][_mode]) = st[_mode] | A User Theorem |
| at-other-14 | ⊦ (st[r0 -- mkfs(class, mkclasstype(class0), fieldvar) ', val][_mode]) = st[_mode] | A User Theorem |
| at-other-15 | ⊦ (st[r0 -- mkfs(class, mkarraytype(ty), fieldvar) ', val][_mode]) = st[_mode] | A User Theorem |
| at-other-16 | ⊦ sk ≠ sk0 → (st[r -- sk, val][r0 -- sk0]) = st[r0 -- sk0] | A User Theorem |
| at-other-17 | ⊦ (st[r -- i ', val][_mode]) = st[_mode] | A User Theorem |
| at-other-18 | ⊦ (st[r0 -- _length, val][r -- i ']) = st[r -- i '] | A User Theorem |
| at-other-19 | ⊦ (st[r0 -- _type, val][r -- i ']) = st[r -- i '] | A User Theorem |
| at-other-20 | ⊦ ty ≠ void_type → (st[r -- mkfs(class, ty, fieldvar) ', val][r0 -- _type]) = st[r0 -- _type] | A User Theorem |
| at-other-21 | ⊦ r ≠ jvmref → (st[_mode, val][r -- sk]) = st[r -- sk] | A User Theorem |
| at-other-22 | ⊦ sk ∈ sks ∧ ¬ sk0 ∈ sks → (st[r -- sk, val][r0 -- sk0]) = st[r0 -- sk0] | A User Theorem |
| at-other-23 | ⊦ ¬ sk ∈ sks ∧ sk0 ∈ sks → (st[r -- sk, val][r0 -- sk0]) = st[r0 -- sk0] | A User Theorem |
| at-other-24 | ⊦ (st[_out, val][r -- i ']) = st[r -- i '] | A User Theorem |
| at-other-25 | ⊦ (st[_out, val][r -- mkfs(class, int_type, fieldvar) ']) = st[r -- mkfs(class, int_type, fieldvar) '] | A User Theorem |
| at-other-26 | ⊦ (st[_out, val][r -- mkfs(class, byte_type, fieldvar) ']) = st[r -- mkfs(class, byte_type, fieldvar) '] | A User Theorem |
| at-other-27 | ⊦ (st[_out, val][r -- mkfs(class, short_type, fieldvar) ']) = st[r -- mkfs(class, short_type, fieldvar) '] | A User Theorem |
| at-other-28 | ⊦ (st[_out, val][r -- mkfs(class, boolean_type, fieldvar) ']) = st[r -- mkfs(class, boolean_type, fieldvar) '] | A User Theorem |
| at-other-29 | ⊦ (st[_out, val][r -- mkfs(class, mkclasstype(class0), fieldvar) ']) = st[r -- mkfs(class, mkclasstype(class0), fieldvar) '] | A User Theorem |
| at-other-30 | ⊦ (st[_out, val][r -- mkfs(class, mkarraytype(ty), fieldvar) ']) = st[r -- mkfs(class, mkarraytype(ty), fieldvar) '] | A User Theorem |
| at-other-31 | ⊦ (st[_mode, val][_out]) = st[_out] | A User Theorem |
| at-other-32 | ⊦ (st[_out, val][r -- _length]) = st[r -- _length] | A User Theorem |
| at-other-33 | i ≠ j ⊦ (st[r -- ((* i)) ', val][r -- ((* j)) ']) = st[r -- j '] | A User Theorem |
| at-other-34 | ⊦ (st[r -- mkfs(class, int_type, fieldvar) ', val][_out]) = st[_out] | A User Theorem |
| at-other-35 | ⊦ (st[r -- mkfs(class, byte_type, fieldvar) ', val][_out]) = st[_out] | A User Theorem |
| at-other-36 | ⊦ (st[r -- mkfs(class, short_type, fieldvar) ', val][_out]) = st[_out] | A User Theorem |
| at-other-37 | ⊦ (st[r -- mkfs(class, boolean_type, fieldvar) ', val][_out]) = st[_out] | A User Theorem |
| at-other-38 | ⊦ (st[r -- mkfs(class, mkclasstype(class0), fieldvar) ', val][_out]) = st[_out] | A User Theorem |
| at-other-39 | ⊦ (st[r -- mkfs(class, mkarraytype(ty), fieldvar) ', val][_out]) = st[_out] | A User Theorem |
| at-other-40 | ⊦ (st[r -- mkfs(class, ty, `initstate' .field) ', val][r0 -- _type]) = st[r0 -- _type] | A User Theorem |
| at-other-41 | ⊦ (st[_mode, val][r -- _type]) = st[r -- _type] | A User Theorem |
| at-other-42 | ⊦ (st[r -- mkfs(class, ty, `initstate' .field) ', val][_mode]) = st[_mode] | A User Theorem |
| at-other-43 | ⊦ (st[r -- mkfs(class, ty, `initstate' .field) ', val][_out]) = st[_out] | A User Theorem |
| at-other-44 | ⊦ (st[_mode, val][r -- mkfs(class, int_type, fieldvar) ']) = st[r -- mkfs(class, int_type, fieldvar) '] | A User Theorem |
| at-other-45 | ⊦ (st[_mode, val][r -- mkfs(class, byte_type, fieldvar) ']) = st[r -- mkfs(class, byte_type, fieldvar) '] | A User Theorem |
| at-other-46 | ⊦ (st[_mode, val][r -- mkfs(class, short_type, fieldvar) ']) = st[r -- mkfs(class, short_type, fieldvar) '] | A User Theorem |
| at-other-47 | ⊦ (st[_mode, val][r -- mkfs(class, boolean_type, fieldvar) ']) = st[r -- mkfs(class, boolean_type, fieldvar) '] | A User Theorem |
| at-other-48 | ⊦ (st[_mode, val][r -- mkfs(class, mkclasstype(class0), fieldvar) ']) = st[r -- mkfs(class, mkclasstype(class0), fieldvar) '] | A User Theorem |
| at-other-49 | ⊦ (st[_mode, val][r -- mkfs(class, mkarraytype(ty), fieldvar) ']) = st[r -- mkfs(class, mkarraytype(ty), fieldvar) '] | A User Theorem |
| at-other-50 | str ≠ str0 ⊦ (st[r -- mkfs(class, ty, ((* str)) .field) ', val][r0 -- mkfs(class0, ty0, ((* str0)) .field) ']) = st[r0 -- mkfs(class0, ty0, str0 .field) '] | A User Theorem |
| at-other-51 | ⊦ (st[r -- _length, val][r0 -- _type]) = st[r0 -- _type] | A User Theorem |
| at-other-class | stringvar ≠ stringvar0 ⊦ (st[r0 -- mkfs(((* stringvar)) .class, ty, fieldvar) ', val][r -- mkfs(((* stringvar0)) .class, ty0, fieldvar0) ']) = st[r -- mkfs(stringvar0 .class, ty0, fieldvar0) '] | A User Theorem |
| at-other-class-01 | stringvar ≠ `*Array*' ⊦ (st[r0 -- mkfs(((* stringvar)) .class, ty, fieldvar) ', val][r -- _length]) = st[r -- _length] | A User Theorem |
| at-other-field | stringvar ≠ stringvar0 ⊦ (st[r0 -- mkfs(class, ty, ((* stringvar)) .field) ', val][r -- mkfs(class0, ty0, ((* stringvar0)) .field) ']) = st[r -- mkfs(class0, ty0, stringvar0 .field) '] | A User Theorem |
| at-other-type | ⊦ (st[r -- mkfs(class, int_type, fieldvar) ', val][r0 -- mkfs(class0, boolean_type, fieldvar0) ']) = st[r0 -- mkfs(class0, boolean_type, fieldvar0) '] | A User Theorem |
| at-other-type-01 | ⊦ (st[r -- mkfs(class, int_type, fieldvar) ', val][r0 -- mkfs(class0, short_type, fieldvar0) ']) = st[r0 -- mkfs(class0, short_type, fieldvar0) '] | A User Theorem |
| at-other-type-02 | ⊦ (st[r -- mkfs(class, int_type, fieldvar) ', val][r0 -- mkfs(class0, byte_type, fieldvar0) ']) = st[r0 -- mkfs(class0, byte_type, fieldvar0) '] | A User Theorem |
| at-other-type-03 | ⊦ (st[r -- mkfs(class, int_type, fieldvar) ', val][r0 -- mkfs(class0, mkarraytype(ty), fieldvar0) ']) = st[r0 -- mkfs(class0, mkarraytype(ty), fieldvar0) '] | A User Theorem |
| at-other-type-04 | ⊦ (st[r -- mkfs(class, int_type, fieldvar) ', val][r0 -- mkfs(class0, mkclasstype(class1), fieldvar0) ']) = st[r0 -- mkfs(class0, mkclasstype(class1), fieldvar0) '] | A User Theorem |
| at-other-type-05 | ⊦ (st[r -- _type, val][r0 -- mkfs(class, mkclasstype(class), fieldvar) ']) = st[r0 -- mkfs(class, mkclasstype(class), fieldvar) '] | A User Theorem |
| at-other-type-06 | ⊦ (st[r -- _type, val][r0 -- mkfs(class, mkarraytype(ty), fieldvar) ']) = st[r0 -- mkfs(class, mkarraytype(ty), fieldvar) '] | A User Theorem |
| at-other-type-07 | ⊦ (st[r -- _type, val][r0 -- mkfs(class, boolean_type, fieldvar) ']) = st[r0 -- mkfs(class, boolean_type, fieldvar) '] | A User Theorem |
| at-other-type-08 | ⊦ (st[r -- _type, val][r0 -- mkfs(class, int_type, fieldvar) ']) = st[r0 -- mkfs(class, int_type, fieldvar) '] | A User Theorem |
| at-other-type-09 | ⊦ (st[r -- _type, val][r0 -- mkfs(class, byte_type, fieldvar) ']) = st[r0 -- mkfs(class, byte_type, fieldvar) '] | A User Theorem |
| at-other-type-10 | ⊦ (st[r -- _type, val][r0 -- mkfs(class, short_type, fieldvar) ']) = st[r0 -- mkfs(class, short_type, fieldvar) '] | A User Theorem |
| byte-in | ⊦ r -- mkfs(class0, byte_type, fieldvar) ' ∈ st[_mode, val] ↔ r -- mkfs(class0, byte_type, fieldvar) ' ∈ st | A User Theorem |
| endfinmode | ⊦ r -- _type ∈ st[_endfinallymode, val0] ↔ r -- _type ∈ st | A User Theorem |
| endfinmode-in | ⊦ _endfinallymode ∈ st[r -- i ', val] ↔ _endfinallymode ∈ st | A User Theorem |
| in-01 | ⊦ r ≠ r0 → (r -- sk ∈ st[r0 -- sk0, val] ↔ r -- sk ∈ st) | A User Theorem |
| init-in | ⊦ r0 -- mkfs(class0, ty0, `initstate' .field) ' ∈ st[_mode, val] ↔ r0 -- mkfs(class0, ty0, `initstate' .field) ' ∈ st | A User Theorem |
| init-in-01 | ⊦ r0 -- mkfs(class0, ty0, `initstate' .field) ' ∈ st[r -- _type, val] ↔ r0 -- mkfs(class0, ty0, `initstate' .field) ' ∈ st | A User Theorem |
| instore | ⊦ _mode ∈ st[r -- _type, val] ↔ _mode ∈ st | A User Theorem |
| instore-01 | ⊦ _out ∈ st[r -- _type, val] ↔ _out ∈ st | A User Theorem |
| instore-02 | sk ≠ sk0 ⊦ r -- sk ∈ st[r -- sk0, val] ↔ r -- sk ∈ st | A User Theorem |
| int-in | ⊦ r -- mkfs(class0, int_type, fieldvar) ' ∈ st[_mode, val] ↔ r -- mkfs(class0, int_type, fieldvar) ' ∈ st | A User Theorem |
| length-at | ⊦ (st[r -- i ', val][r0 -- _length]) = st[r0 -- _length] | A User Theorem |
| look-del | ⊦ r ≠ r0 → (st -- (r -- sk))[r0 -- sk] = st[r0 -- sk] | A User Theorem |
| look-del-01 | ⊦ r ≠ r0 → (st -- (r -- sk))[r0 -- sk0] = st[r0 -- sk0] | A User Theorem |
| look-ins | ⊦ r ≠ r0 → (st[r0 -- sk0, val][r -- sk]) = st[r -- sk] | A User Theorem |
| look-ins-01 | ⊦ (st[_out, val][_mode]) = st[_mode] | A User Theorem |
| look-out | ⊦ (st[r -- _type, val][_out]) = st[_out] | A User Theorem |
| look-out-01 | ⊦ r ≠ jvmref → (st[r -- sk, val][_out]) = st[_out] | A User Theorem |
| look-type | ⊦ (st[_out, val][r -- _type]) = st[r -- _type] | A User Theorem |
| lookup-if | ⊦ (st[rk0, val][rk]) = ((rk = rk0 ⊃ val; st[rk])) | A User Theorem |
| lookup-put-mode | ⊦ r ≠ jvmref → (st[r -- sk, val][_mode]) = st[_mode] | A User Theorem |
| mode | ⊦ r ≠ jvmref → (r -- sk ∈ st[_mode, val] ↔ r -- sk ∈ st) | A User Theorem |
| mode-in | ⊦ _mode ∈ st[r -- i ', val] ↔ _mode ∈ st | A User Theorem |
| mode-noval-subset | ⊦ st ⊆ st0 ∧ _mode ∈ st ∧ st0[_mode] ≠ noval → st[_mode] ≠ noval | A User Theorem |
| refp | ⊦ rk ≠ rk0 → (refp((st -- rk)[rk0]) ↔ refp(st[rk0])) | A User Theorem |
| shift-out | class1 ≠ `java.lang.Object' .class ⊦ (st[_out, val][jvmref -- mkfs(class1, ty, fieldvar) ', val0]) = (st[jvmref -- mkfs(class1, ty, fieldvar) ', val0][_out, val]) | A User Theorem |
| short-in | ⊦ r -- mkfs(class0, short_type, fieldvar) ' ∈ st[_mode, val] ↔ r -- mkfs(class0, short_type, fieldvar) ' ∈ st | A User Theorem |
| sk | ⊦ r -- fs ' ∈ st[r0 -- i ', val0] ↔ r -- fs ' ∈ st | A User Theorem |
| sk-01 | ⊦ r -- i ' ∈ st[r0 -- fs ', val0] ↔ r -- i ' ∈ st | A User Theorem |
| subset-band | ⊦ j ≤ band(b2i(st[rk] .byteval), i) ∧ rk ∈ st ∧ st ⊆ st0 → j ≤ band(b2i(st0[rk] .byteval), i) | A User Theorem |
| subset-band-01 | ⊦ band(b2i(st[rk] .byteval), i) ≤ j ∧ rk ∈ st ∧ st ⊆ st0 → band(b2i(st0[rk] .byteval), i) ≤ j | A User Theorem |
| subset-eqval | ⊦ st[rk] .intval = i ∧ st ⊆ st0 ∧ rk ∈ st → st0[rk] .intval = i | A User Theorem |
| type | ⊦ r -- _type ∈ st[r0 -- i ', val0] ↔ r -- _type ∈ st | A User Theorem |
| type-01 | ⊦ r -- _type ∈ st[_mode, val] ↔ r -- _type ∈ st | A User Theorem |
| type-at | ⊦ (st[r -- i ', val][r0 -- _type]) = st[r0 -- _type] | A User Theorem |
| typeout | ⊦ r -- _type ∈ st[_out, val] ↔ r -- _type ∈ st | A User Theorem |
| uninit-mod | ⊦ _uninit ∈ st[_mode, val] ↔ _uninit ∈ st | A User Theorem |
| uninit-type | ⊦ _uninit ∈ st[r -- _type, val] ↔ _uninit ∈ st | A User Theorem |