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: |
|---|---|---|
| junkref-def | ⊦ junkref(str, r, st) ↔ (∃ refs. refs ≠ [] ∧ refs .first = r ∧ junkrefs(str, refs, st[r -- _type] .type, st)) | An Axiom |
| junkrefs-array | ⊦ is_array(str, r, st) ∧ st[r -- _type] .type ≤ ty → ( junkrefs(str, r ' + refs, ty, st) ↔ refs ≠ [] ∧ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ refs .first = st[r -- i '] .refval ∧ junkrefs(str, refs, st[r -- _type] .type .type, st))) | An Axiom |
| junkrefs-class | ⊦ is_obj(str, r, st) ∧ st[r -- _type] .type ≤ ty → ( junkrefs(str, r ' + refs, ty, st) ↔ refs ≠ [] ∧ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ refs .first = st[r -- fs '] .refval ∧ junkrefs(str, refs, fs .type, st))) | An Axiom |
| junkrefs-is-junk | ⊦ r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ ty) → junkrefs(str, r ' + refs, ty, st) | An Axiom |
| junkrefs-null | ⊦ r = jvmref → ¬ junkrefs(str, r ' + refs, ty, st) | An Axiom |
| junkrefs-empty | ⊦ ¬ junkrefs(str, [], ty, st) | An Axiom |
| validref-def | ⊦ validref(str, r, ty, st) ↔ r = jvmref ∨ st[r -- _type] .type ≤ ty ∧ ¬ junkref(str, r, st) | An Axiom |
| validrefnotnull-def | ⊦ validrefnotnull(str, r, ty, st) ↔ r ≠ jvmref ∧ validref(str, r, ty, st) | An Axiom |
| validrefkeynotnull-def | ⊦ validrefkeynotnull(str, rk, ty, st) ↔ rk ∈ st ∧ validrefvalnotnull(str, st[rk], ty, st) | An Axiom |
| validrefval-def | ⊦ validrefval(str, val, ty, st) ↔ is_referencevalue(val) ∧ validref(str, val .refval, ty, st) | An Axiom |
| validrefvalnotnull-def | ⊦ validrefvalnotnull(str, val, ty, st) ↔ is_referencevalue(val) ∧ validrefnotnull(str, val .refval, ty, st) | An Axiom |
| validreflist-def | ⊦ validreflist(str, vals, ty, st) ↔ (∀ val. val ∈ vals → is_referencevalue(val) ∧ validref(str, val .refval, ty, st)) | An Axiom |
| validstatfields-def | ⊦ validstatfields(str, st) ↔ (∀ class. tdname∃(str, class) ∧ initdone(class, st) → validfieldlist(str, jvmref, statfields(class), st)) | An Axiom |
| validmodeval-def | ⊦ validmode(str, val, st) ↔ val = noval ∨ is_break_mode(val) ∨ val = return(noval, void_type) ∨ is_return_mode(val) ∧ validref(str, val .refval, val .type, st) ∨ is_throw_mode(val) ∧ val .refval ≠ jvmref ∧ validref(str, val .refval, val .type, st) ∧ val .type ≤ mkclasstype(`java.lang.Throwable' .class) | An Axiom |
| validmode-def | ⊦ validmode(str, st) ↔ _mode ∈ st ∧ validmode(str, st[_mode], st) | An Axiom |
| validfield-def | ⊦ validfield(str, r, sk, st) ↔ goodfieldandtype(r, sk, st) ∧ type∃(str, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ (is_reftype(sk .fs .type) → validrefval(str, st[r -- sk], sk .fs .type, st)) | An Axiom |
| validstatfields-class | ⊦ validstatfields(str, class, st) ↔ validfieldlist(str, jvmref, statfields(class), st) | An Axiom |
| initsubset-def | ⊦ init⊆(str, st, st0) ↔ (∀ class. initdone(class, st) → initdone(class, st0)) ∧ (∀ class. initerror(class, st) → initerror(class, st0)) ∧ (∀ class. ¬ initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) → validstatfields(str, statfields(class), st0)) ∧ (∀ class, sk. initdone(class, st) ∧ initdone(class, st0) ∧ tdname∃(str, class) ∧ sk ∈ statfields(class) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0)) | An Axiom |
| validsubset-def | ⊦ valid⊆(str, st, st0) ↔ (∀ r, ty. validref(str, r, ty, st) → validref(str, r, ty, st0)) ∧ (∀ r. ¬ r ∈ st ∧ r ∈ st0 → ¬ junkref(str, r, st0)) | An Axiom |
| validval-def | ⊦ validval(str, val, ty, st) ↔ okval(val, ty) ∧ (is_referencevalue(val) → validrefval(str, val, ty, st)) | An Axiom |
| junkreflist-def | ⊦ junkrefs(str, vals, st) ↔ (∃ r. refval(r) ∈ vals ∧ junkref(str, r, st)) | An Axiom |
| validfieldinits-def | ⊦ validfieldinits(str, fis, st) ↔ (∀ sk, val. sk × val ∈ fis → is_fskey(sk) ∧ type∃(str, sk .fs .type) ∧ validval(str, val, sk .fs .type, st)) | An Axiom |
| validfieldlist-def-01 | ⊦ validfieldlist(str, r, sks, st) ↔ (∀ sk. sk ∈ sks → validfield(str, r, sk, st)) | An Axiom |
| validstatfields-storekeys-def | ⊦ validstatfields(str, sks, st) ↔ (∀ sk. sk ∈ sks → validstatfield(str, sk, st)) | An Axiom |
| validstatfield-storekey-def | ⊦ validstatfield(str, sk, st) ↔ is_fskey(sk) ∧ sk ∈ statfields(sk .fs .class) ∧ tdname∃(str, sk .fs .class) ∧ (initdone(sk .fs .class, st) → validfield(str, jvmref, sk, st)) | An Axiom |
| same-subclasses-one-def | ⊦ same-subclasses(class, str, str0) ↔ (∀ class0. class∃(str0, class0) ∧ class0 ≤ class → class∃(str, class0)) ∧ (∀ class0. interface∃(str0, class0) ∧ class0 ≤ class → interface∃(str, class0)) | An Axiom |
| levelsubset-def | ⊦ level⊆(str, str0) ↔ (∀ class. class∃(str, class) → class∃(str0, class)) ∧ (∀ class. interface∃(str, class) → interface∃(str0, class)) | An Axiom |
| validrefkeyvalues-def | ⊦ validvals(str, rkvs, st) ↔ (∀ rkv. rkv ∈ rkvs → validval(str, rkv .1, rkv .2, st)) | An Axiom |
| validrefkeyval-def | ⊦ validval(str, r -- sk, val, st) ↔ (is_fskey(sk) → validval(str, val, sk .fs .type, st) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length) ∧ (is_indexkey(sk) → validval(str, val, st[r -- _type] .type .type, st)) | An Axiom |
| bytearray-is-no-junk | ⊦ okbytearray(r, st) → ¬ junkref(str, r, st) | A User Theorem |
| initsubset-addclass | ⊦ validfieldinits(str, fis, st) ∧ fis .keys = statfields(class) ∧ initundone(class, st) ∧ class ≠ `java.lang.Object' .class → init⊆(str, st, addclass(class, fis, st)) | A User Theorem |
| initsubset-addclass-01 | ⊦ init⊆(str, st, st0) ∧ validfieldinits(str, fis, st0) ∧ fis .keys = statfields(class) ∧ initundone(class, st0) ∧ class ≠ `java.lang.Object' .class → init⊆(str, st, addclass(class, fis, st0)) | A User Theorem |
| initsubset-addobj | ⊦ init⊆(str, st, st0) ∧ newref(r, st0) → init⊆(str, st, addobj(r, class, fis, st0)) | A User Theorem |
| initsubset-addobj-01 | ⊦ newref(r, st0) → init⊆(str, st0, addobj(r, class, fis, st0)) | A User Theorem |
| initsubset-init | ⊦ init⊆(str, st, st0) ∧ init(str0, st) → init(str0, st0) | A User Theorem |
| initsubset-init-forward | ⊦ init⊆(str, st, st0) ∧ init(str, st) → init(str, st0) | A User Theorem |
| initsubset-initdone-forward | ⊦ init⊆(str, st, st0) ∧ initdone(class, st) → initdone(class, st0) | A User Theorem |
| initsubset-initerror | ⊦ ¬ initdone(class, st) → init⊆(str, st, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)]) | A User Theorem |
| initsubset-initerror-01 | ⊦ init⊆(str, st, st0) ∧ ¬ initdone(class, st0) → init⊆(str, st, st0[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)]) | A User Theorem |
| initsubset-initerror-02 | ⊦ ¬ initdone(class, st) ∧ class ≠ `java.lang.Object' .class ∧ ¬ mkfs(class, void_type, `initstate' .field) ' ∈ fis → init⊆(str, st, addclass(class, fis + (mkfs(class, void_type, `initstate' .field) ' × initval(error)) ', st)) | A User Theorem |
| initsubset-initerror-03 | ⊦ init⊆(str, st, st0) ∧ ¬ initdone(class, st0) ∧ class ≠ `java.lang.Object' .class ∧ ¬ mkfs(class, void_type, `initstate' .field) ' ∈ fis → init⊆(str, st, addclass(class, fis + (mkfs(class, void_type, `initstate' .field) ' × initval(error)) ', st0)) | A User Theorem |
| initsubset-initerror-04 | ⊦ init⊆(str, st, st0) ∧ ¬ initdone(class, st) → init⊆(str, st, st0[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)]) | A User Theorem |
| initsubset-mode | ⊦ init⊆(str, st, st0[_mode, val]) ↔ init⊆(str, st, st0) | A User Theorem |
| initsubset-mode-01 | ⊦ init⊆(str, st, st[_mode, val]) | A User Theorem |
| initsubset-mode-02 | ⊦ init⊆(str, st[_mode, val], st) | A User Theorem |
| initsubset-put-statfield | ⊦ validstatfield(str, rk .key, st0[rk, val]) ∧ init⊆(str, st, st0) ∧ rk .ref = jvmref ∧ (¬ is_fskey(rk .key) ∨ rk .key .fs .type ≠ void_type ∨ rk .key .fs .field ≠ `initstate' .field ∧ rk ≠ _uninit) → init⊆(str, st, st0[rk, val]) | A User Theorem |
| initsubset-put-statfield-01 | ⊦ init⊆(str, st, st0) ∧ (¬ rk .key ∈ statfields(rk .key .fs .class) ∨ ¬ tdname∃(str, rk .key .fs .class)) ∧ rk .ref = jvmref ∧ is_fskey(rk .key) ∧ (rk .key .fs .type ≠ void_type ∨ rk .key .fs .field ≠ `initstate' .field ∧ rk ≠ _uninit) → init⊆(str, st, st0[rk, val]) | A User Theorem |
| initsubset-put-statfield-int | ⊦ init⊆(str, st, st0) → init⊆(str, st, st0[jvmref -- mkfs(class, int_type, fieldvar) ', intval(i)]) | A User Theorem |
| initsubset-same | ⊦ init⊆(str, st, st) | A User Theorem |
| initsubset-trans | ⊦ init⊆(str, st, st0) ∧ init⊆(str, st0, st1) → init⊆(str, st, st1) | A User Theorem |
| initsubset-validstatfield-forward | ⊦ init⊆(str, st, st0) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st0) | A User Theorem |
| initsubset-validstatfields-forward | ⊦ init⊆(str, st, st0) ∧ validstatfields(str, sks, st) → validstatfields(str, sks, st0) | A User Theorem |
| is_valid_ref-levelsubset | ⊦ level⊆(str, str0) ∧ is_valid_ref(str, r, st) → is_valid_ref(str0, r, st) | A User Theorem |
| junkref-abstract | ⊦ st[r -- _type] .type = mkarraytype(abstract_type) ∧ r ≠ jvmref → junkref(str, r, st) | A User Theorem |
| junkref-ac | ⊦ junkref(str, r, addclass(class, fis, st)) ↔ junkref(str, r, st) | A User Theorem |
| junkref-addarray-01 | ⊦ newref(r, st) ∧ (∀ val. val ∈ vals → ¬ junkref(str, val .refval, st) ∧ is_referencevalue(val) ∧ (val .refval ≠ jvmref → st[val .refval -- _type] .type ≤ ty)) ∧ is_classtype(ty) ∧ class∃(str, ty .class) → ¬ junkref(str, r, addarray(r, ty, vals, st)) | A User Theorem |
| junkref-addarray-02 | ⊦ ¬ junkref(str, r, st) ∧ newref(r0, st) → ¬ junkref(str, r, addarray(r0, ty, i, st)) | A User Theorem |
| junkref-addarray-03 | ⊦ type∃(str, ty) ∧ r ≠ jvmref ∧ 0 ≤ i ∧ ty .jtelemtype ≠ abstract_type ∧ ty .jtelemtype ≠ void_type → ¬ junkref(str, r, addarray(r, ty, i, st)) | A User Theorem |
| junkref-addarray-04 | ⊦ validreflist(str, vals, ty, st) ∧ newref(r, st) ∧ type∃(str, ty) ∧ is_reftype(ty) ∧ ty .jtelemtype ≠ abstract_type ∧ ty .jtelemtype ≠ void_type → ¬ junkref(str, r, addarray(r, ty, vals, st)) | A User Theorem |
| junkref-addarray-newref | ⊦ ¬ junkref(str, r, st) ∧ newref(r0, st) → ¬ junkref(str, r, addarray(r0, ty0, vals, st)) | A User Theorem |
| junkref-addarray-newref-put | ⊦ ¬ junkref(str, r, st) ∧ newref(r0, st) ∧ fs .type = mkarraytype(byte_type) ∧ is_bytelist(vals) → ¬ junkref(str, r, addarray(r0, byte_type, vals, st)[r1 -- fs ', refval(r0)]) | A User Theorem |
| junkref-addarray-noreftype | ⊦ (∀ val. val ∈ vals → okprimtype(val, ty0)) ∧ is_primtype(ty0) → ¬ junkref(str, r, addarray(r, ty0, vals, st)) | A User Theorem |
| junkref-addbytearray | ⊦ ¬ junkref(str, r, addarray(r, byte_type, mkjavavalues(bytes), st)) | A User Theorem |
| junkref-addobj | ⊦ ¬ junkref(str, r, st) ∧ newref(r0, st) → ¬ junkref(str, r, addobj(r0, class, fis, st)) | A User Theorem |
| junkref-addobj-01 | ⊦ newref(r, st) ∧ class+∃(str, class) ∧ fis .keys = instfields(class) ∧ validfieldinits(fis, st) ∧ ¬ is_abstract(class) ∧ (∀ sk, r1. sk × refval(r1) ∈ fis → ¬ junkref(str, r1, st)) → ¬ junkref(str, r, addobj(r, class, fis, st)) | A User Theorem |
| junkref-array | ⊦ is_array(str, r, st) → ( junkref(str, r, st) ↔ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ st[r -- i '] .refval ≠ jvmref ∧ (¬ st[st[r -- i '] .refval -- _type] .type ≤ st[r -- _type] .type .type ∨ junkref(str, st[r -- i '] .refval, st)))) | A User Theorem |
| junkref-bad-type | ⊦ ¬ is_classtype(st[r -- _type] .type) ∧ ¬ is_arraytype(st[r -- _type] .type) → (junkref(str, r, st) ↔ r ≠ jvmref) | A User Theorem |
| junkref-class | ⊦ is_obj(str, r, st) → ( junkref(str, r, st) ↔ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ st[st[r -- fs '] .refval -- _type] .type ≤ fs .type ∨ junkref(str, st[r -- fs '] .refval, st)))) | A User Theorem |
| junkref-class-01 | ⊦ is_obj(str, r, st) → ( junkref(str, r, st) ↔ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ (is_reftype(fs .type) ∨ fs .type = abstract_type) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ is_referencevalue(st[r -- fs ']) ∨ ¬ st[st[r -- fs '] .refval -- _type] .type ≤ fs .type ∨ junkref(str, st[r -- fs '] .refval, st)))) | A User Theorem |
| junkref-class-02 | ⊦ is_obj(str, r, st) → ( junkref(str, r, st) ↔ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_reftype(fs .type) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ is_referencevalue(st[r -- fs ']) ∨ ¬ st[st[r -- fs '] .refval -- _type] .type ≤ fs .type ∨ junkref(str, st[r -- fs '] .refval, st)))) | A User Theorem |
| junkref-classtype | ⊦ ¬ is_obj(r, class, st) ∧ st[r -- _type] .type ≤ mkclasstype(class) ∧ st[r -- _type] .type = mkclasstype(class) ∧ r ≠ jvmref → junkref(str, r, st) | A User Theorem |
| junkref-field-reftype | ⊦ r ≠ jvmref ∧ st[r -- mkfs(class0, ty, fieldvar) '] = refval(r3) ∧ mkfs(class0, ty, fieldvar) ' ∈ instfields(class) ∧ st[r -- _type] .type = mkclasstype(class) ∧ ¬ junkref(str, r, st) → is_reftype(ty) | A User Theorem |
| junkref-is-junk | ⊦ r ≠ jvmref ∧ ¬ is_valid_ref(str, r, st) → junkref(str, r, st) | A User Theorem |
| junkref-is_array | ⊦ ¬ is_array(str, r, st) ∧ st[r -- _type] .type = mkarraytype(ty) → (junkref(str, r, st) ↔ r ≠ jvmref) | A User Theorem |
| junkref-isarray-typeex | ⊦ is_array(r3, st) ∧ st[r3 -- i '] .refval ≠ jvmref ∧ 0 ≤ i ∧ i < st[r3 -- _length] .intval ∧ is_referencevalue(st[r3 -- i ']) ∧ ¬ junkref(str, r3, st) → type∃(str, st[st[r3 -- i '] .refval -- _type] .type) | A User Theorem |
| junkref-keyin | ⊦ ¬ r -- _type ∈ st → (junkref(str, r, st) ↔ r ≠ jvmref) | A User Theorem |
| junkref-levelsubset | ⊦ level⊆(str, str0) ∧ ¬ junkref(str, r, st) → ¬ junkref(str0, r, st) | A User Theorem |
| junkref-levelsubset-01 | ⊦ level⊆(str, str0) ∧ ¬ junkref(str, r, st) → (junkref(str0, r, st) ↔ false) | A User Theorem |
| junkref-newref | ⊦ newref(r, st) → junkref(str, r, st) | A User Theorem |
| junkref-noreftype | ⊦ ¬ is_reftype(st[r -- _type] .type) ∧ r ≠ jvmref → junkref(str, r, st) | A User Theorem |
| junkref-not-hasclasstype | ⊦ ¬ has_classtype(st[r -- _type] .type) ∧ r ≠ jvmref → (junkref(str, r, st) ↔ junkref(str0, r, st)) | A User Theorem |
| junkref-not-hasclasstype-01 | ⊦ ¬ has_classtype(st[r -- _type] .type) ∧ r ≠ jvmref ∧ ¬ junkref(str, r, st) → ¬ junkref(str0, r, st) | A User Theorem |
| junkref-not-is-array | ⊦ ¬ is_array(r, st) ∧ st[r -- _type] .type = mkarraytype(ty) → (junkref(str, r, st) ↔ r ≠ jvmref) | A User Theorem |
| junkref-not-okreftype | ⊦ ¬ okreftype(refval(r), ty, st) ∧ st[r -- _type] .type ≤ ty ∧ type∃(str, st[r -- _type] .type) → junkref(str, r, st) | A User Theorem |
| junkref-not-okreftype-01 | ⊦ ¬ okreftype(refval(r), ty, st) ∧ (st[r -- _type] .type ≤ ty ∨ ¬ type∃(str, st[r -- _type] .type)) → junkref(str, r, st) | A User Theorem |
| junkref-not-valid | ⊦ ¬ is_valid_ref(r, st) ∧ r ≠ jvmref → junkref(str, r, st) | A User Theorem |
| junkref-not-valid-01 | ⊦ ¬ is_valid_ref(str, r, st) ∧ r ≠ jvmref → junkref(str, r, st) | A User Theorem |
| junkref-notin | ⊦ ¬ r ∈ st → (junkref(str, r, st) ↔ r ≠ jvmref) | A User Theorem |
| junkref-notypeex | ⊦ ¬ type∃(str, st[r -- _type] .type) ∧ r ≠ jvmref → junkref(str, r, st) | A User Theorem |
| junkref-null | ⊦ ¬ junkref(str, jvmref, st) | A User Theorem |
| junkref-okarray-byte | ⊦ okarray(val, byte_type, i, st) ∧ is_referencevalue(val) → ¬ junkref(str, val .refval, st) | A User Theorem |
| junkref-okbytearray | ⊦ ¬ junkref(str, r, st) ∧ st[r -- _type] .type = mkarraytype(byte_type) ∧ r ≠ jvmref → (¬ okbytearray(r, st) ↔ false) | A User Theorem |
| junkref-predefined | ⊦ is_predefined_class(class) ∧ newref(r, st) → ¬ junkref(str, r, addobj(r, class, [], st)) | A User Theorem |
| junkref-primarray-level | ⊦ ¬ has_classtype(st[r -- _type] .type) → (junkref(str, r, st) ↔ junkref(str1, r, st)) | A User Theorem |
| junkref-primarray-level-01 | ⊦ ¬ has_classtype(st[r -- _type] .type) ∧ junkref(str, r, st) → junkref(str1, r, st) | A User Theorem |
| junkref-primarray-lvl | ⊦ is_primtype(ty) ∧ st[r -- _type] = typeval(mkarraytype(ty)) → (junkref(str, r, st) ↔ junkref(str1, r, st)) | A User Theorem |
| junkref-put-array-norefval | ⊦ ¬ is_referencevalue(val) ∧ ¬ junkref(str, r, st) ∧ okval(val, st[r1 -- _type] .type .type) → ¬ junkref(str, r, st[r1 -- i ', val]) | A User Theorem |
| junkref-put-ba | ⊦ ¬ junkref(str, r, st) ∧ fs .type = mkarraytype(byte_type) ∧ is_array(r0, st) ∧ st[r0 -- _type] = typeval(mkarraytype(byte_type)) → ¬ junkref(str, r, st[r1 -- fs ', refval(r0)]) | A User Theorem |
| junkref-put-badarrayfield | ⊦ ¬ junkref(str, r, st) ∧ fs ' ≠ _type ∧ is_arraytype(st[r0 -- _type] .type) ∧ fs ' ≠ _length → ¬ junkref(str, r, st[r0 -- fs ', val]) | A User Theorem |
| junkref-put-badarrayindex | ⊦ ¬ junkref(str, r, st) ∧ ¬ is_array(str, r0, st) → ¬ junkref(str, r, st[r0 -- i ', val]) | A User Theorem |
| junkref-put-badclassfield | ⊦ ¬ junkref(str, r, st) ∧ fs ' ≠ _type ∧ is_classtype(st[r0 -- _type] .type) ∧ ¬ fs ' ∈ instfields(st[r0 -- _type] .type .class) → ¬ junkref(str, r, st[r0 -- fs ', val]) | A User Theorem |
| junkref-put-badfield | ⊦ ¬ junkref(str, r, st) ∧ ¬ (is_typevalue(st[r0 -- _type]) ∧ is_reftype(st[r0 -- _type] .type)) → ¬ junkref(str, r, st[r0 -- fs ', val]) | A User Theorem |
| junkref-put-field | ⊦ ¬ junkref(str, r0, st) ∧ ¬ junkref(str, r, st) ∧ is_obj(r, st) ∧ st[r0 -- _type] .type ≤ fs .type ∧ fs ' ∈ instfields(st[r -- _type] .type .class) ∧ r0 ≠ jvmref → ¬ junkref(str, r, st[r -- fs ', refval(r0)]) | A User Theorem |
| junkref-put-norefval | ⊦ ¬ is_referencevalue(val) ∧ ¬ junkref(str, r, st) ∧ is_fskey(sk) ∧ oktype(val, sk .fs .type, st) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → ¬ junkref(str, r, st[r1 -- sk, val]) | A User Theorem |
| junkref-put-norefval-01 | ⊦ ¬ is_referencevalue(val) ∧ ¬ junkref(str, r, st) ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → ¬ junkref(str, r, st[r1 -- sk, val]) | A User Theorem |
| junkref-put-norefval-equiv | ⊦ okval(st[r1 -- sk], sk .fs .type) ∧ r1 -- sk ∈ st ∧ ¬ is_referencevalue(val) ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → (junkref(str, r, st[r1 -- sk, val]) ↔ junkref(str, r, st)) | A User Theorem |
| junkref-put-null | ⊦ ¬ junkref(str, r, st) ∧ is_reftype(fs .type) → ¬ junkref(str, r, st[r0 -- fs ', refval(jvmref)]) | A User Theorem |
| junkref-put-refval | ⊦ ¬ junkref(str, r, st) ∧ validref(str, r1, ty, st) ∧ ty ≤ fs .type ∧ is_reftype(fs .type) → ¬ junkref(str, r, st[r0 -- fs ', refval(r1)]) | A User Theorem |
| junkref-put-refval-01 | ⊦ ¬ junkref(str, r, st) ∧ validref(str, r1, ty, st) ∧ mkarraytype(ty) ≤ st[r0 -- _type] .type ∧ r0 ≠ jvmref ∧ is_arraytype(st[r0 -- _type] .type) ∧ (r1 = jvmref → is_reftype(ty)) → ¬ junkref(str, r, st[r0 -- i ', refval(r1)]) | A User Theorem |
| junkref-put-refval-statfield | ⊦ ¬ junkref(str, r, st) → ¬ junkref(str, r, st[jvmref -- sk, val]) | A User Theorem |
| junkref-put-refval-statfield-01 | ⊦ junkref(str, r, st[jvmref -- sk, val]) → junkref(str, r, st) | A User Theorem |
| junkref-put-statfield | ⊦ rk1 .ref = jvmref ∧ r ≠ jvmref → (junkref(str, r, st[rk1, val]) ↔ junkref(str, r, st)) | A User Theorem |
| junkref-putbar | ⊦ okbytearray(r2, st) ∧ junkref(`docs2store', r, putByteArray(bytes1, r2, i, st)) → junkref(`docs2store', r, st) | A User Theorem |
| junkref-putbar-01 | ⊦ okbytearray(r0, st) ∧ ¬ junkref(str, r, st) → ¬ junkref(str, r, putByteArray(bytes, r0, i, st)) | A User Theorem |
| junkref-rec-case | ⊦ junkref(str, r, st) ↔ r ≠ jvmref ∧ ¬ is_valid_ref(str, r, st) ∨ r ≠ jvmref ∧ is_obj(str, r, st) ∧ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ st[st[r -- fs '] .refval -- _type] .type ≤ fs .type ∨ junkref(str, st[r -- fs '] .refval, st))) ∨ r ≠ jvmref ∧ is_array(str, r, st) ∧ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ st[r -- i '] .refval ≠ jvmref ∧ (¬ st[st[r -- i '] .refval -- _type] .type ≤ st[r -- _type] .type .type ∨ junkref(str, st[r -- i '] .refval, st))) | A User Theorem |
| junkref-rec-keep-case | ⊦ junkref(str, r, st) ↔ junkref(str, r, st) ∨ r ≠ jvmref ∧ ¬ is_valid_ref(str, r, st) ∨ r ≠ jvmref ∧ is_obj(str, r, st) ∧ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ st[st[r -- fs '] .refval -- _type] .type ≤ fs .type ∨ junkref(str, st[r -- fs '] .refval, st))) ∨ r ≠ jvmref ∧ is_array(str, r, st) ∧ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ st[r -- i '] .refval ≠ jvmref ∧ (¬ st[st[r -- i '] .refval -- _type] .type ≤ st[r -- _type] .type .type ∨ junkref(str, st[r -- i '] .refval, st))) | A User Theorem |
| junkref-subset | ⊦ ¬ junkref(str, r, st) ∧ st ⊆ st1 → ¬ junkref(str, r, st1) | A User Theorem |
| junkref-tdnameex | ⊦ ¬ tdname∃(str, class) ∧ ¬ is_predefined_class(class) ∧ st[r -- _type] .type = mkclasstype(class) → (junkref(str, r, st) ↔ r ≠ jvmref) | A User Theorem |
| junkref-union | ⊦ ¬ junkref(str, r, st) → ¬ junkref(str, r, st0 ∪ st) | A User Theorem |
| junkref-union-disjoint | ⊦ st1 .refs ∩ st .refs = ∅ ∧ r ∈ st1 ∧ junkref(str, r, st1 ∪ st) → junkref(str, r, st1) | A User Theorem |
| junkref-void | ⊦ ¬ junkref(str, r, st) ∧ r ≠ jvmref → st[r -- _type] ≠ typeval(void_type) | A User Theorem |
| junkref-voidarray | ⊦ ¬ junkref(str, r, st) ∧ r ≠ jvmref → st[r -- _type] .type ≠ mkarraytype(void_type) | A User Theorem |
| junkreflist-empty | ⊦ ¬ junkrefs(str, [], st) | A User Theorem |
| junkreflist-rec | ⊦ junkrefs(str, val ' + vals, st) ↔ is_referencevalue(val) ∧ junkref(str, val .refval, st) ∨ junkrefs(str, vals, st) | A User Theorem |
| junkrefs-addarray | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ newref(r0, st) → ¬ junkrefs(str, refs, ty, addarray(r0, ty0, vals, st)) | A User Theorem |
| junkrefs-addarray-newref-put | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ newref(r0, st) ∧ fs .type = mkarraytype(byte_type) ∧ is_bytelist(vals) → ¬ junkrefs(str, refs, ty, addarray(r0, byte_type, vals, st)[r1 -- fs ', refval(r0)]) | A User Theorem |
| junkrefs-addarray-noreftype | ⊦ (∀ val. val ∈ vals → okprimtype(val, ty0)) ∧ mkarraytype(ty0) ≤ ty ∧ is_primtype(ty0) → ¬ junkrefs(str, r ' + refs, ty, addarray(r, ty0, vals, st)) | A User Theorem |
| junkrefs-addobj | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ newref(r0, st) → ¬ junkrefs(str, refs, ty, addobj(r0, class, fis, st)) | A User Theorem |
| junkrefs-append | ⊦ junkrefs(str, refs, ty, st) → junkrefs(str, refs + refs0, ty, st) | A User Theorem |
| junkrefs-bytearray | ⊦ junkrefs(str, r ' + refs, mkarraytype(byte_type), st) ↔ r ≠ jvmref ∧ ¬ okbytearray(r, st) | A User Theorem |
| junkrefs-delete | ⊦ junkrefs(str, refs, ty, st -- r) ∧ ¬ r ∈ refs → junkrefs(str, refs, ty, st) | A User Theorem |
| junkrefs-delete-01 | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ ¬ r ∈ refs → ¬ junkrefs(str, refs, ty, st -- r) | A User Theorem |
| junkrefs-delete-02 | ⊦ junkrefs(str, refs, ty, st) → junkrefs(str, refs, ty, st -- r) | A User Theorem |
| junkrefs-empty-01 | ⊦ refs = [] → ¬ junkrefs(str, refs, ty, st) | A User Theorem |
| junkrefs-inttype | ⊦ refs ≠ [] ∧ refs .first ≠ jvmref → junkrefs(str, refs, int_type, st) | A User Theorem |
| junkrefs-junkref | ⊦ ¬ junkref(str, r, st) → (junkrefs(str, r ' + refs0, st[r -- _type] .type, st) ↔ false) | A User Theorem |
| junkrefs-levelsubset | ⊦ level⊆(str, str0) ∧ ¬ junkrefs(str, refs, ty, st) → ¬ junkrefs(str0, refs, ty, st) | A User Theorem |
| junkrefs-levelsubset-01 | ⊦ level⊆(str, str0) ∧ ¬ junkrefs(str, refs, ty, st) → (junkrefs(str0, refs, ty, st) ↔ false) | A User Theorem |
| junkrefs-newref | ⊦ newref(r, st) → (junkrefs(str, refs + r ' + refs0, ty, st) ↔ junkrefs(str, refs + r ', ty, st)) | A User Theorem |
| junkrefs-newref-01 | ⊦ newref(r, st) → junkrefs(str, r ', ty, st) | A User Theorem |
| junkrefs-newref-02 | ⊦ newref(r, st) → junkrefs(str, r ' + refs, ty, st) | A User Theorem |
| junkrefs-newref-03 | ⊦ newref(r, st) → (¬ junkrefs(str, r ' + refs, ty, st) ↔ false) | A User Theorem |
| junkrefs-newref-04 | ⊦ newref(r, st) → (¬ junkrefs(str, r ', ty, st) ↔ false) | A User Theorem |
| junkrefs-notin | ⊦ ¬ r ∈ st → (junkrefs(str, refs + r ' + refs0, ty, st) ↔ junkrefs(str, refs + r ', ty, st)) | A User Theorem |
| junkrefs-notin-01 | ⊦ ¬ r ∈ st → (junkrefs(str, r ' + refs, ty, st) ↔ r ≠ jvmref) | A User Theorem |
| junkrefs-notin-02 | ⊦ ¬ r ∈ st → (junkrefs(str, r ', ty, st) ↔ r ≠ jvmref) | A User Theorem |
| junkrefs-notin-03 | ⊦ junkrefs(str, refs + r ' + refs0, ty, st -- r) ↔ junkrefs(str, refs + r ', ty, st -- r) | A User Theorem |
| junkrefs-null-01 | ⊦ junkrefs(str, refs + jvmref ' + refs0, ty, st) ↔ junkrefs(str, refs, ty, st) | A User Theorem |
| junkrefs-null-02 | ⊦ ¬ junkrefs(str, jvmref ' + refs, ty, st) | A User Theorem |
| junkrefs-null-03 | ⊦ refs .first = jvmref ∧ refs ≠ [] → ¬ junkrefs(str, refs, ty, st) | A User Theorem |
| junkrefs-one | ⊦ junkrefs(str, r ', ty, st) ↔ r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ ty) | A User Theorem |
| junkrefs-primarray | ⊦ is_primtype(ty) → (junkrefs(str, r ' + refs, mkarraytype(ty), st) ↔ r ≠ jvmref ∧ ¬ okarray(r, ty, st)) | A User Theorem |
| junkrefs-put-array-norefval | ⊦ ¬ is_referencevalue(val) ∧ ¬ junkrefs(str, refs, ty, st) ∧ okval(val, st[r1 -- _type] .type .type) → ¬ junkrefs(str, refs, ty, st[r1 -- i ', val]) | A User Theorem |
| junkrefs-put-ba | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ fs .type = mkarraytype(byte_type) ∧ is_array(r0, st) ∧ st[r0 -- _type] = typeval(mkarraytype(byte_type)) → ¬ junkrefs(str, refs, ty, st[r1 -- fs ', refval(r0)]) | A User Theorem |
| junkrefs-put-badarrayfield | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ fs ' ≠ _type ∧ is_arraytype(st[r0 -- _type] .type) ∧ fs ' ≠ _length → ¬ junkrefs(str, refs, ty, st[r0 -- fs ', val]) | A User Theorem |
| junkrefs-put-badarrayindex | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ ¬ is_array(str, r0, st) → ¬ junkrefs(str, refs, ty, st[r0 -- i ', val]) | A User Theorem |
| junkrefs-put-badclassfield | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ fs ' ≠ _type ∧ is_classtype(st[r0 -- _type] .type) ∧ ¬ fs ' ∈ instfields(st[r0 -- _type] .type .class) → ¬ junkrefs(str, refs, ty, st[r0 -- fs ', val]) | A User Theorem |
| junkrefs-put-badfield | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ ¬ (is_typevalue(st[r0 -- _type]) ∧ is_reftype(st[r0 -- _type] .type)) → ¬ junkrefs(str, refs, ty, st[r0 -- fs ', val]) | A User Theorem |
| junkrefs-put-norefval | ⊦ ¬ is_referencevalue(val) ∧ ¬ junkrefs(str, refs, ty, st) ∧ is_fskey(sk) ∧ oktype(val, sk .fs .type, st) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → ¬ junkrefs(str, refs, ty, st[r1 -- sk, val]) | A User Theorem |
| junkrefs-put-norefval-01 | ⊦ ¬ is_referencevalue(val) ∧ ¬ junkrefs(str, refs, ty, st) ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → ¬ junkrefs(str, refs, ty, st[r1 -- sk, val]) | A User Theorem |
| junkrefs-put-norefval-equiv | ⊦ okval(st[r1 -- sk], sk .fs .type) ∧ r1 -- sk ∈ st ∧ ¬ is_referencevalue(val) ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → (junkrefs(str, refs, ty, st[r1 -- sk, val]) ↔ junkrefs(str, refs, ty, st)) | A User Theorem |
| junkrefs-put-notin | ⊦ ¬ r ∈ refs → (junkrefs(str, refs, ty, st[r -- sk, val]) ↔ junkrefs(str, refs, ty, st)) | A User Theorem |
| junkrefs-put-notin-butlast | ⊦ ¬ r ∈ refs ∧ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _length ∧ fs ' ≠ _type → (junkrefs(str, refs + r ', ty, st[r -- fs ', val]) ↔ junkrefs(str, refs + r ', ty, st)) | A User Theorem |
| junkrefs-put-null | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ is_obj(r, st) ∧ is_reftype(fs .type) ∧ fs ' ∈ instfields(st[r -- _type] .type .class) → ¬ junkrefs(str, refs, ty, st[r -- fs ', refval(jvmref)]) | A User Theorem |
| junkrefs-put-null-01 | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ is_reftype(fs .type) → ¬ junkrefs(str, refs, ty, st[r -- fs ', refval(jvmref)]) | A User Theorem |
| junkrefs-put-null-02 | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ r ≠ jvmref ∧ is_reftype(st[r -- _type] .type .type) → ¬ junkrefs(str, refs, ty, st[r -- i ', refval(jvmref)]) | A User Theorem |
| junkrefs-put-refval | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ ¬ junkref(str, r0, st) ∧ is_obj(r, st) ∧ st[r0 -- _type] .type ≤ fs .type ∧ r0 ≠ jvmref ∧ fs ' ∈ instfields(st[r -- _type] .type .class) → ¬ junkrefs(str, refs, ty, st[r -- fs ', refval(r0)]) | A User Theorem |
| junkrefs-put-refval-01 | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ ¬ junkref(str, r0, st) ∧ st[r0 -- _type] .type ≤ fs .type ∧ r0 ≠ jvmref ∧ fs .type ≠ void_type ∧ fs ' ≠ _length → ¬ junkrefs(str, refs, ty, st[r -- fs ', refval(r0)]) | A User Theorem |
| junkrefs-put-refval-02 | ⊦ ¬ junkrefs(str, refs, ty, st) ∧ ¬ junkref(str, r0, st) ∧ mkarraytype(st[r0 -- _type] .type) ≤ st[r -- _type] .type ∧ r ≠ jvmref ∧ r0 ≠ jvmref → ¬ junkrefs(str, refs, ty, st[r -- i ', refval(r0)]) | A User Theorem |
| junkrefs-put-refval-statfield | ⊦ ¬ junkrefs(str, refs, ty, st) → ¬ junkrefs(str, refs, ty, st[jvmref -- sk, val]) | A User Theorem |
| junkrefs-put-statfield | ⊦ junkrefs(str, refs, ty, st) → junkrefs(str, refs, ty, st[jvmref -- sk, val]) | A User Theorem |
| junkrefs-runtimetype | ⊦ junkrefs(str, r ' + refs, st[r -- _type] .type, st) → junkrefs(str, r ' + refs, ty, st) | A User Theorem |
| junkrefs-sametype | ⊦ ¬ junkrefs(str, r ' + refs, st[r -- _type] .type, st) ∧ r ≠ jvmref → (junkrefs(str, r ' + refs, ty, st) ↔ ¬ st[r -- _type] .type ≤ ty) | A User Theorem |
| junkrefs-sametype-01 | ⊦ junkrefs(str, r ' + refs, st[r -- _type] .type, st) ∧ st[r -- _type] .type ≤ ty ∧ r ≠ jvmref → junkrefs(str, r ' + refs, ty, st) | A User Theorem |
| junkrefs-subclass | ⊦ is_obj(refs .first, st) ∧ ¬ junkrefs(str, refs, st[refs .first -- _type] .type, st) ∧ refs ≠ [] → ¬ junkrefs(str, refs, mkclasstype(`java.lang.Object' .class), st) | A User Theorem |
| junkrefs-subset | ⊦ st ⊆ st1 ∧ junkrefs(str, refs, ty, st1) → junkrefs(str, refs, ty, st) | A User Theorem |
| junkrefs-subtype | ⊦ junkrefs(str, refs, ty0, st) ∧ ty ≤ ty0 → junkrefs(str, refs, ty, st) | A User Theorem |
| junkrefs-supertype | ⊦ junkrefs(str, r ' + refs, st[r -- _type] .type, st) ∧ st[r -- _type] .type ≤ ty0 → junkrefs(str, r ' + refs, ty0, st) | A User Theorem |
| junkrefs-typein | ⊦ r ≠ jvmref ∧ ¬ junkrefs(str, r + refs, ty, st) → r -- _type ∈ st | A User Theorem |
| junkrefs-union | ⊦ (∃ st0. st1 = st0 ∪ st) ∧ junkrefs(str, refs, ty, st1) → junkrefs(str, refs, ty, st) | A User Theorem |
| junkrefs-union-disjoint | ⊦ st1 .refs ∩ st .refs = ∅ ∧ r ∈ st1 ∧ junkrefs(str, r ' + refs0, ty, st1 ∪ st) → junkrefs(str, r ' + refs0, ty, st1) | A User Theorem |
| levelsubset-all-types | level⊆(str, str0) ⊦ ∀ ty. type∃(str, ty) → type∃(str0, ty) | A User Theorem |
| levelsubset-classex | ⊦ class+∃(str, class) ∧ level⊆(str, str0) → (¬ class+∃(str0, class) ↔ false) | A User Theorem |
| levelsubset-classex-01 | ⊦ class∃(str, class) ∧ level⊆(str, str0) → (¬ class∃(str0, class) ↔ false) | A User Theorem |
| levelsubset-classex-02 | ⊦ level⊆(str, str0) ∧ class+∃(str, class) → ¬ interface∃(str0, class) | A User Theorem |
| levelsubset-classex-03 | ⊦ level⊆(str, str0) ∧ interface∃(str, class) → ¬ class+∃(str0, class) | A User Theorem |
| levelsubset-is-array | ⊦ is_array(str, r, st) ∧ level⊆(str, str0) → (¬ is_array(str0, r, st) ↔ false) | A User Theorem |
| levelsubset-is-obj | ⊦ is_obj(str, r, st) ∧ level⊆(str, str0) → (¬ is_obj(str0, r, st) ↔ false) | A User Theorem |
| levelsubset-ref | ⊦ level⊆(str, str) | A User Theorem |
| levelsubset-tdnameex | ⊦ tdname∃(str, class) ∧ ¬ tdname∃(str0, class) → ¬ level⊆(str, str0) | A User Theorem |
| levelsubset-trans | ⊦ level⊆(str, str0) ∧ level⊆(str0, str1) → level⊆(str, str1) | A User Theorem |
| levelsubset-typeex | ⊦ type∃(str, ty) ∧ ¬ type∃(str0, ty) → ¬ level⊆(str, str0) | A User Theorem |
| nojunkref-typeex | ⊦ ¬ junkref(str, r, st) ∧ r ≠ jvmref → (¬ type∃(str, st[r -- _type] .type) ↔ false) | A User Theorem |
| nojunkref-typeex-01 | ⊦ ¬ junkref(str, st[r -- sks] .refval, st) ∧ st[r -- sks] .refval ≠ jvmref ∧ sks ≠ [] → (¬ type∃(str, st[r -- (sks + _type ')] .type) ↔ false) | A User Theorem |
| nojunkref-typeex-02 | ⊦ ¬ junkref(str, st[r -- (sk ' + sk0 ')] .refval, st) ∧ st[r -- (sk ' + sk0 ')] .refval ≠ jvmref → (¬ type∃(str, st[r -- (sk ' + sk0 ' + _type ')] .type) ↔ false) | A User Theorem |
| okbytearray | ⊦ ¬ okbytearray(st[rk] .refval, st) → ¬ validrefkeynotnull(str, rk, mkarraytype(byte_type), st) | A User Theorem |
| okbytearray-01 | ⊦ ¬ okbytearray(r, st) → ¬ validrefnotnull(str, r, mkarraytype(byte_type), st) | A User Theorem |
| okbytearray-02 | ⊦ ¬ okbytearray(r, st) ∧ r ≠ jvmref → ¬ validref(str, r, mkarraytype(byte_type), st) | A User Theorem |
| okbytearray-putrkvs | ⊦ validvals(str, rkvs, st) ∧ okbytearray(r, st) → okbytearray(r, st[rkvs]) | A User Theorem |
| okbytearray-validref | ⊦ validref(str, r, mkarraytype(byte_type), st) ↔ okbytearray(r, st) ∨ r = jvmref | A User Theorem |
| same-subclasses-classex | ⊦ ¬ class+∃(str, class) ∧ same-subclasses(class, str, str0) → ¬ class+∃(str0, class) | A User Theorem |
| same-subclasses-classex-01 | ⊦ class∃(str0, class) ∧ ¬ class∃(str, class) → ¬ same-subclasses(class, str, str0) | A User Theorem |
| same-subclasses-classex-02 | ⊦ class∃(str0, class) ∧ ¬ class∃(str, class) ∧ class ≤ class0 → ¬ same-subclasses(class0, str, str0) | A User Theorem |
| same-subclasses-interfaceex | ⊦ interface∃(str0, class) ∧ ¬ interface∃(str, class) → ¬ same-subclasses(class, str, str0) | A User Theorem |
| same-subclasses-interfaceex-01 | ⊦ interface∃(str0, class) ∧ ¬ interface∃(str, class) ∧ class ≤ class0 → ¬ same-subclasses(class0, str, str0) | A User Theorem |
| same-subclasses-is-array | ⊦ ¬ is_array(str, r, st) ∧ is_array(str0, r, st) → ¬ same-subclasses(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(st[r -- _type] .type .jtelemtype .class, str, str0) | A User Theorem |
| same-subclasses-ref | ⊦ same-subclasses(class, str, str) | A User Theorem |
| same-subclasses-subclass | ⊦ same-subclasses(class, str, str0) ∧ class0 ≤ class → same-subclasses(class0, str, str0) | A User Theorem |
| same-subclasses-tdnameex | ⊦ ¬ tdname+∃(str, class0) ∧ tdname+∃(str0, class0) → ¬ same-subclasses(`java.lang.Object' .class, str, str0) | A User Theorem |
| same-subclasses-tdnameex-01 | ⊦ ¬ tdname+∃(str, class0) ∧ tdname+∃(str0, class0) ∧ class0 ≤ class → ¬ same-subclasses(class, str, str0) | A User Theorem |
| same-subclasses-tdnameex-02 | ⊦ ¬ tdname∃(str, class0) ∧ tdname∃(str0, class0) ∧ class0 ≤ class → ¬ same-subclasses(class, str, str0) | A User Theorem |
| same-subclasses-tdnameex-03 | ⊦ ¬ tdname+∃(str, class0) ∧ tdname+∃(str0, class0) → ¬ same-subclasses(class0, str, str0) | A User Theorem |
| same-subclasses-tdnameex-04 | ⊦ tdname∃(str0, class) ∧ ¬ tdname∃(str, class) → ¬ same-subclasses(class, str, str0) | A User Theorem |
| same-subclasses-tdnameex-05 | ⊦ tdname∃(str0, class) ∧ ¬ tdname∃(str, class) ∧ class ≤ class0 → ¬ same-subclasses(class0, str, str0) | A User Theorem |
| same-subclasses-trans | ⊦ same-subclasses(class, str, str0) ∧ same-subclasses(class, str0, str1) → same-subclasses(class, str, str1) | A User Theorem |
| same-subclasses-typeex | ⊦ ¬ type∃(str, ty) ∧ type∃(str0, ty) ∧ ty ≤ mkclasstype(class) → ¬ same-subclasses(class, str, str0) | A User Theorem |
| valid-typeex | ⊦ ¬ st[r -- _type] .type ≤ ty → ¬ validrefnotnull(str, r, ty, st) | A User Theorem |
| validfield-levelsubset | ⊦ validfield(str, r, sk, st) ∧ level⊆(str, str0) → validfield(str0, r, sk, st) | A User Theorem |
| validfield-one | ⊦ validfield(str, r, sk, st) ↔ is_fskey(sk) ∧ r -- sk ∈ st ∧ type∃(str, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ validval(str, st[r -- sk], sk .fs .type, st) | A User Theorem |
| validfield-put-statfield | ⊦ r ≠ jvmref ∨ sk ≠ sk0 → (validfield(str, r, sk0, st[jvmref -- sk, val]) ↔ validfield(str, r, sk0, st)) | A User Theorem |
| validfield-put-statfield-01 | ⊦ rk .ref = jvmref ∧ (r ≠ jvmref ∨ rk .key ≠ sk0) → (validfield(str, r, sk0, st[rk, val]) ↔ validfield(str, r, sk0, st)) | A User Theorem |
| validfield-superset | ⊦ validfield(str, r, sk, st) ∧ st ⊆ st0 → validfield(str, r, sk, st0) | A User Theorem |
| validfieldinits-def-01 | ⊦ validfieldinits(str, fis, st) ↔ validfieldinits(fis, st) ∧ ¬ junkrefs(str, fis .vals, st) ∧ (∀ sk. sk ∈ fis → type∃(str, sk .fs .type)) | A User Theorem |
| validfieldinits-empty | ⊦ validfieldinits(str, [], st) | A User Theorem |
| validfieldinits-junkref | ⊦ junkref(str, r, st) ∧ fis[sk] = refval(r) ∧ sk ∈ fis → ¬ validfieldinits(str, fis, st) | A User Theorem |
| validfieldinits-one | ⊦ validfieldinits(str, fv ', st) ↔ is_fskey(fv .1) ∧ type∃(str, fv .1 .fs .type) ∧ validval(str, fv .2, fv .1 .fs .type, st) | A User Theorem |
| validfieldinits-rec | ⊦ validfieldinits(str, fv ' + fis, st) ↔ is_fskey(fv .1) ∧ validval(str, fv .2, fv .1 .fs .type, st) ∧ type∃(str, fv .1 .fs .type) ∧ validfieldinits(str, fis, st) | A User Theorem |
| validfieldinits-validreflist | ⊦ validfieldinits(str, fis, st) → validreflist(str, mkjavavalues(fis .vals .nonnullrefs), mkclasstype(`java.lang.Object' .class), st) | A User Theorem |
| validfieldlist-empty | ⊦ validfieldlist(str, r, [], st) | A User Theorem |
| validfieldlist-mode | ⊦ ¬ _mode .key ∈ sks → (validfieldlist(str, jvmref, sks, st[_mode, val]) ↔ validfieldlist(str, jvmref, sks, st)) | A User Theorem |
| validfieldlist-mode-01 | ⊦ sk ∈ statfields(class) → (validfieldlist(str, jvmref, sk ', st[_mode, val]) ↔ validfieldlist(str, jvmref, sk ', st)) | A User Theorem |
| validfieldlist-one-01 | ⊦ validfieldlist(str, r, sk ', st) ↔ validfield(str, r, sk, st) | A User Theorem |
| validfieldlist-put-statfield | ⊦ rk .ref = jvmref ∧ (r ≠ jvmref ∨ ¬ rk .key ∈ sks) → (validfieldlist(str, r, sks, st[rk, val]) ↔ validfieldlist(str, r, sks, st)) | A User Theorem |
| validfieldlist-rec | ⊦ validfieldlist(str, r, sk ' + sks, st) ↔ validfield(str, r, sk, st) ∧ validfieldlist(str, r, sks, st) | A User Theorem |
| validfieldlist-superset | ⊦ st ⊆ st0 ∧ validfieldlist(str, r, sks, st) → validfieldlist(str, r, sks, st0) | A User Theorem |
| validmode | ⊦ st[_mode] = noval → (validmode(str, st) ↔ _mode ∈ st) | A User Theorem |
| validmode-01 | ⊦ ¬ _mode ∈ st → ¬ validmode(str, st) | A User Theorem |
| validmode-addarray | ⊦ validmode(str, st) ∧ newref(r, st) → validmode(str, addarray(r, ty, vals, st)) | A User Theorem |
| validmode-addclass | ⊦ class ≠ `java.lang.Object' .class → (validmode(str, addclass(class, fis, st)) ↔ validmode(str, st)) | A User Theorem |
| validmode-addobj | ⊦ newref(r, st) → (validmode(str, addobj(r, class, fis, st)) ↔ validmode(str, st)) | A User Theorem |
| validmode-noval-put | ⊦ st[_mode] = noval ∧ rk ≠ _mode → (validmode(str, st[rk, val]) ↔ _mode ∈ st) | A User Theorem |
| validmode-noval-put-01 | ⊦ st[_mode] = noval ∧ r ≠ jvmref → (validmode(str, st[r -- sk, val]) ↔ _mode ∈ st) | A User Theorem |
| validmode-put-nonnull | ⊦ ¬ _mode ∈ rkvs ∧ st[_mode] = noval → (validmode(str, st[rkvs]) ↔ validmode(str, st)) | A User Theorem |
| validmode-put-nonnull-01 | ¬ _mode ∈ rkvs ⊦ st[_mode] = noval → (validmode(str, st[rkvs]) ↔ validmode(str, st)) | A User Theorem |
| validmode-put-statfield | ⊦ rk .ref = jvmref ∧ rk ≠ _mode → (validmode(str, st[rk, val]) ↔ validmode(str, st)) | A User Theorem |
| validmode-put-statfield-01 | ⊦ jvmref -- sk ≠ _mode → (validmode(str, st[jvmref -- sk, val]) ↔ validmode(str, st)) | A User Theorem |
| validmode-put-statfield-02 | str0 ≠ `java.lang.Object' ⊦ validmode(str, st[jvmref -- mkfs(((* str0)) .class, ty, fieldvar) ', val]) ↔ validmode(str, st) | A User Theorem |
| validmode-superset | ⊦ st ⊆ st0 ∧ validmode(str, st) → validmode(str, st0) | A User Theorem |
| validmode-throw-predef | ⊦ is_predefined_class(class) ∧ class ≤ `java.lang.Throwable' .class ∧ newref(r, st) → validmode(str, addobj(r, class, [], st)[_mode, throw(r, mkclasstype(class))]) | A User Theorem |
| validmode-throw-predef-01 | ⊦ newref(r, st) → validmode(str, addobj(r, `java.lang.NullPointerException' .class, [], st)[_mode, throw(r, mkclasstype(`java.lang.NullPointerException' .class))]) | A User Theorem |
| validmode-throw-predef-02 | ⊦ newref(r, st) → validmode(str, addobj(r, `java.lang.NoClassDefFoundError' .class, [], st)[_mode, throw(r, mkclasstype(`java.lang.NoClassDefFoundError' .class))]) | A User Theorem |
| validmode-throw-typeex | ⊦ validmode(str, st) ∧ is_throw_mode(st[_mode]) → (¬ type∃(str, st[st[_mode] .refval -- _type] .type) ↔ false) | A User Theorem |
| validref-ac | ⊦ validref(str, r, ty, addclass(class, fis, st)) ↔ validref(str, r, ty, st) | A User Theorem |
| validref-addarray | ⊦ newref(r1, st) ∧ validref(str, r, ty1, st) → validref(str, r, ty1, addarray(r1, ty, vals, st)) | A User Theorem |
| validref-addarray-get | ⊦ validref(str, r, ty, st) ∧ newref(r0, st) → getintarray(r, addarray(r0, ty, i0, st)) = getintarray(r, st) | A User Theorem |
| validref-addarray-get-01 | ⊦ validref(str, r, ty, st) ∧ newref(r0, st) → getintarray(r, i, j, addarray(r0, ty, i0, st)) = getintarray(r, i, j, st) | A User Theorem |
| validref-addarray-other-01 | ⊦ validref(str, r, ty, st) ∧ newref(r0, st) → (¬ validref(str, r, ty, addarray(r0, ty0, i, st)) ↔ false) | A User Theorem |
| validref-addarray-same | ⊦ validref(str, r, mkarraytype(ty), addarray(r, ty, i, st)) ↔ r = jvmref ∨ 0 ≤ i ∧ type∃(str, ty) ∧ ty .jtelemtype ≠ abstract_type ∧ ty .jtelemtype ≠ void_type | A User Theorem |
| validref-addarray-same-01 | ⊦ r ≠ jvmref → (validref(str, r, mkarraytype(int_type), addarray(r, int_type, i, st)) ↔ 0 ≤ i) | A User Theorem |
| validref-addobj | ⊦ newref(r1, st) ∧ validref(str, r, ty1, st) → validref(str, r, ty1, addobj(r1, class, fis, st)) | A User Theorem |
| validref-addobj-this | ⊦ (∀ sk, r1. sk × refval(r1) ∈ fis → ¬ junkref(str, r1, st)) ∧ ¬ _type ∈ fis ∧ class∃(str, class) ∧ type∃(str, ty) ∧ mkclasstype(class) ≤ ty ∧ newref(r, st) ∧ validfieldinits(fis, st) ∧ fis .keys = instfields(class) ∧ ¬ is_abstract(class) ∧ class+∃(str, class) → validref(str, r, ty, addobj(r, class, fis, st)) | A User Theorem |
| validref-array | ⊦ validref(str, r, mkarraytype(ty), st) ∧ r ≠ jvmref → val2int(st[r -- _length]) = st[r -- _length] .intval | A User Theorem |
| validref-array-01 | ⊦ validref(str, r, mkarraytype(ty), st) ∧ r ≠ jvmref → ¬ st[r -- _length] .intval < 0 | A User Theorem |
| validref-array-02 | ⊦ validref(str, r, mkarraytype(ty), st) ∧ r ≠ jvmref → is_integervalue(st[r -- _length]) | A User Theorem |
| validref-array-03 | str ≠ `java.lang.Object' ⊦ is_array(str0, r, st) → ¬ validref(str0, r, mkclasstype(((* str)) .class), st) | A User Theorem |
| validref-array-len-in | ⊦ validref(str, r, mkarraytype(ty), st) ∧ r ≠ jvmref → r -- _length ∈ st | A User Theorem |
| validref-array-notin | ⊦ ¬ r -- i ' ∈ st ∧ r ≠ jvmref ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ validref(str, r, mkarraytype(ty), st) | A User Theorem |
| validref-array-rec | ⊦ is_array(str, r, st) ∧ st[r -- _type] .type ≤ ty → ( validref(str, r, ty, st) ↔ ¬ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ st[r -- i '] .refval ≠ jvmref ∧ ( ¬ st[st[r -- i '] .refval -- _type] .type ≤ st[r -- _type] .type .type ∨ ¬ validref(str, st[r -- i '] .refval, st[r -- _type] .type .type, st)))) | A User Theorem |
| validref-arrayreftype | ⊦ ¬ is_referencevalue(st[r -- i ']) ∧ is_reftype(ty) ∧ r ≠ jvmref ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ validref(str, r, mkarraytype(ty), st) | A User Theorem |
| validref-arraytype | ⊦ is_obj(str, r, st) → ¬ validref(str, r, mkarraytype(ty), st) | A User Theorem |
| validref-bad-type | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (validref(str, r, ty, st) ↔ r = jvmref) | A User Theorem |
| validref-bytearray | ⊦ validref(str, r, mkarraytype(byte_type), st) ↔ r = jvmref ∨ okbytearray(r, st) | A User Theorem |
| validref-bytearray-level | ⊦ validref(str, r, mkarraytype(byte_type), st) ↔ validref(str0, r, mkarraytype(byte_type), st) | A User Theorem |
| validref-bytearray-level-01 | ⊦ ¬ validref(str, r, mkarraytype(byte_type), st) → ¬ validref(str0, r, mkarraytype(byte_type), st) | A User Theorem |
| validref-class | ⊦ r ≠ jvmref ∧ st[r -- _type] .type = mkclasstype(class) ∧ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ (is_reftype(fs .type) ∨ fs .type = abstract_type) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ is_referencevalue(st[r -- fs ']) ∨ ¬ st[r -- (fs ' + _type)] .type ≤ fs .type ∨ ¬ validref(str, st[r -- fs '] .refval, fs .type, st))) → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-class-rec | ⊦ is_obj(str, r, st) ∧ st[r -- _type] .type ≤ ty → ( validref(str, r, ty, st) ↔ ¬ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ st[st[r -- fs '] .refval -- _type] .type ≤ fs .type ∨ ¬ validref(str, st[r -- fs '] .refval, fs .type, st)))) | A User Theorem |
| validref-class-rec-better | ⊦ is_obj(str, r, st) → ( validref(str, r, ty, st) ↔ st[r -- _type] .type ≤ ty ∧ ¬ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ st[st[r -- fs '] .refval -- _type] .type ≤ fs .type ∨ ¬ validref(str, st[r -- fs '] .refval, fs .type, st)))) | A User Theorem |
| validref-class-rec-better-keep | ⊦ is_obj(str, r, st) → ( validref(str, r, ty, st) ↔ validref(str, r, ty, st) ∧ st[r -- _type] .type ≤ ty ∧ ¬ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ is_referencevalue(st[r -- fs ']) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ st[st[r -- fs '] .refval -- _type] .type ≤ fs .type ∨ ¬ validref(str, st[r -- fs '] .refval, fs .type, st)))) | A User Theorem |
| validref-forward | ⊦ r ≠ jvmref ∧ validref(str, r, mkclasstype(class), st0) ∧ fs ' ∈ instfields(class) ∧ is_reftype(fs .type) → validref(str, st0[r -- fs '] .refval, fs .type, st0) | A User Theorem |
| validref-forward-01 | ⊦ r ≠ jvmref ∧ ¬ validref(str, st0[r -- fs '] .refval, fs .type, st0) ∧ fs ' ∈ instfields(class) ∧ is_reftype(fs .type) → ¬ validref(str, r, mkclasstype(class), st0) | A User Theorem |
| validref-forward-array | ⊦ r ≠ jvmref ∧ validref(str, r, mkarraytype(ty), st0) ∧ 0 ≤ i ∧ i < st0[r -- _length] .intval → validref(str, st0[r -- i '] .refval, ty, st0) | A User Theorem |
| validref-forward-array-01 | ⊦ r ≠ jvmref ∧ ¬ validref(str, st0[r -- i '] .refval, ty, st0) ∧ 0 ≤ i ∧ i < st0[r -- _length] .intval → ¬ validref(str, r, mkarraytype(ty), st0) | A User Theorem |
| validref-hasnoclasstype-level | ⊦ ¬ has_classtype(ty) ∧ validref(str, r, ty, st) → validref(str0, r, ty, st) | A User Theorem |
| validref-intarray-put | ⊦ validref(str, r, mkarraytype(int_type), st) → (¬ validref(str, r, mkarraytype(int_type), st[r -- i ', intval(j)]) ↔ false) | A User Theorem |
| validref-intarray-put-01 | ⊦ validref(str, r, ty, st) ∧ validref(str, r0, mkarraytype(int_type), st) → (¬ validref(str, r, ty, st[r0 -- i ', intval(j)]) ↔ false) | A User Theorem |
| validref-is-junk | ⊦ r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ ty) → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-is-junk-better | ⊦ r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ ty ∧ ¬ type∃(str, st[r -- _type] .type)) → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-isarray | ⊦ r ≠ jvmref ∧ ¬ is_array(str, r, st) → ¬ validref(str, r, mkarraytype(ty), st) | A User Theorem |
| validref-isarrayref | ⊦ ¬ is_arrayref(r, i, st) ∧ i ≤ st[r -- _length] .intval ∧ r ≠ jvmref → ¬ validref(str, r, mkarraytype(ty), st) | A User Theorem |
| validref-isobj | ⊦ r ≠ jvmref ∧ ¬ is_obj(str, r, st) ∧ class ≠ `java.lang.Object' .class → ¬ validref(str, r, mkclasstype(class), st) | A User Theorem |
| validref-isvalidref | str ≠ `java.lang.Object' ⊦ validref(str0, r, mkclasstype(((* str)) .class), st) → (is_valid_ref(str0, r, st) ↔ is_obj(str0, r, st)) | A User Theorem |
| validref-junkref | ⊦ junkref(str, r, st) → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-levelsubset | ⊦ level⊆(str, str0) ∧ validref(str, r, ty, st) → validref(str0, r, ty, st) | A User Theorem |
| validref-levelsubset-01 | ⊦ level⊆(str, str0) ∧ validref(str, r, ty, st) → (¬ validref(str0, r, ty, st) ↔ false) | A User Theorem |
| validref-mode | ⊦ validref(str, r, ty, st[_mode, val]) ↔ validref(str, r, ty, st) | A User Theorem |
| validref-newref | ⊦ newref(r, st) → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-newref-subset | ⊦ validref(str, r, mkarraytype(byte_type), st) ∧ st ⊆ st0 → ¬ newref(r, st0) | A User Theorem |
| validref-no-len | ⊦ ¬ r -- _length ∈ st → (validref(str, r, mkarraytype(ty), st) ↔ r = jvmref) | A User Theorem |
| validref-no-obj | str0 ≠ `java.lang.Object' ⊦ ¬ is_obj(str, r, st) → (validref(str, r, mkclasstype(((* str0)) .class), st) ↔ r = jvmref) | A User Theorem |
| validref-no-type | ⊦ ¬ r -- _type ∈ st → (validref(str, r, ty, st) ↔ r = jvmref) | A User Theorem |
| validref-noreftype | ⊦ ¬ is_reftype(st[r -- _type] .type) ∧ r ≠ jvmref → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-not-junkrefs | ⊦ validref(str, r, ty, st) → (junkrefs(str, r ' + refs, ty, st) ↔ false) | A User Theorem |
| validref-not-tdnameex | ⊦ ¬ tdname+∃(str, class) ∧ st[r -- _type] .type = mkclasstype(class) ∧ r ≠ jvmref → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-notin | ⊦ ¬ r ∈ st ∧ r ≠ jvmref → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-null | ⊦ validref(str, jvmref, ty, st) | A User Theorem |
| validref-object | ⊦ ¬ validref(str, r, mkclasstype(`java.lang.Object' .class), st) ∧ r ≠ jvmref → junkref(str, r, st) | A User Theorem |
| validref-object-01 | ⊦ ¬ validref(str, r, mkclasstype(`java.lang.Object' .class), st) ∧ r ≠ jvmref → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-okarray | ⊦ validref(str, r, mkarraytype(ty), st) ∧ r ≠ jvmref → okarray(r, ty, st) | A User Theorem |
| validref-okreftype | ⊦ validref(str, r, ty, st) ↔ okreftype(refval(r), ty, st) ∧ ¬ junkref(str, r, st) | A User Theorem |
| validref-primarray | ⊦ is_primtype(ty) → (validref(str, r, mkarraytype(ty), st) ↔ r = jvmref ∨ okarray(r, ty, st)) | A User Theorem |
| validref-put-any | ⊦ validref(str, r, ty, st) ∧ ( is_fskey(sk) → (is_referencevalue(val) → validref(str, val .refval, sk .fs .type, st) ∧ is_reftype(sk .fs .type)) ∧ (¬ is_referencevalue(val) → is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length)) ∧ ( is_indexkey(sk) → ( is_referencevalue(val) → validref(str, val .refval, st[r0 -- _type] .type .type, st) ∧ r0 ≠ jvmref ∧ is_arraytype(st[r0 -- _type] .type) ∧ (val .refval = jvmref → is_reftype(st[r0 -- _type] .type .type))) ∧ (¬ is_referencevalue(val) → okval(val, st[r0 -- _type] .type .type))) → validref(str, r, ty, st[r0 -- sk, val]) | A User Theorem |
| validref-put-any-01 | ⊦ validref(str, r, ty, st) ∧ ( is_fskey(rk .key) → (is_referencevalue(val) → validref(str, val .refval, rk .key .fs .type, st) ∧ is_reftype(rk .key .fs .type)) ∧ (¬ is_referencevalue(val) → okval(val, rk .key .fs .type) ∧ rk .key .fs .type ≠ void_type ∧ rk .key ≠ _length)) ∧ ( is_indexkey(rk .key) → ( is_referencevalue(val) → validref(str, val .refval, st[rk .ref -- _type] .type .type, st) ∧ rk .ref ≠ jvmref ∧ is_arraytype(st[rk .ref -- _type] .type) ∧ (val .refval = jvmref → is_reftype(st[rk .ref -- _type] .type .type))) ∧ (¬ is_referencevalue(val) → okval(val, st[rk .ref -- _type] .type .type))) → validref(str, r, ty, st[rk, val]) | A User Theorem |
| validref-put-array-any | ⊦ validref(str, r, ty, st) ∧ is_indexkey(sk) ∧ ( is_referencevalue(val) → validref(str, val .refval, st[r0 -- _type] .type .type, st) ∧ r0 ≠ jvmref ∧ is_arraytype(st[r0 -- _type] .type) ∧ (val .refval = jvmref → is_reftype(st[r0 -- _type] .type .type))) ∧ (¬ is_referencevalue(val) → okval(val, st[r0 -- _type] .type .type)) → validref(str, r, ty, st[r0 -- sk, val]) | A User Theorem |
| validref-put-array-norefval | ⊦ ¬ is_referencevalue(val) ∧ validref(str, r, ty, st) ∧ okval(val, st[r1 -- _type] .type .type) → validref(str, r, ty, st[r1 -- i ', val]) | A User Theorem |
| validref-put-array-norefval-01 | ⊦ validref(str, r, ty, st) ∧ is_indexkey(sk) ∧ ¬ is_referencevalue(val) ∧ okval(val, st[r0 -- _type] .type .type) → validref(str, r, ty, st[r0 -- sk, val]) | A User Theorem |
| validref-put-array-refval | ⊦ validref(str, r, ty0, st) ∧ validref(str, r1, ty, st) ∧ mkarraytype(ty) ≤ st[r0 -- _type] .type ∧ r0 ≠ jvmref ∧ is_arraytype(st[r0 -- _type] .type) ∧ (r1 = jvmref → is_reftype(ty)) → validref(str, r, ty0, st[r0 -- i ', refval(r1)]) | A User Theorem |
| validref-put-array-refval-01 | ⊦ validref(str, r, ty0, st) ∧ validref(str, val .refval, ty, st) ∧ is_referencevalue(val) ∧ mkarraytype(ty) ≤ st[r0 -- _type] .type ∧ r0 ≠ jvmref ∧ is_arraytype(st[r0 -- _type] .type) ∧ (val .refval = jvmref → is_reftype(ty)) → validref(str, r, ty0, st[r0 -- i ', val]) | A User Theorem |
| validref-put-array-refval-02 | ⊦ validref(str, r, ty0, st) ∧ validref(str, val .refval, st[r0 -- _type] .type .type, st) ∧ is_referencevalue(val) ∧ r0 ≠ jvmref ∧ is_arraytype(st[r0 -- _type] .type) ∧ (val .refval = jvmref → is_reftype(st[r0 -- _type] .type .type)) → validref(str, r, ty0, st[r0 -- i ', val]) | A User Theorem |
| validref-put-array-refval-03 | ⊦ validref(str, r, ty, st) ∧ is_indexkey(sk) ∧ is_referencevalue(val) ∧ validref(str, val .refval, st[r0 -- _type] .type .type, st) ∧ r0 ≠ jvmref ∧ is_arraytype(st[r0 -- _type] .type) ∧ (val .refval = jvmref → is_reftype(st[r0 -- _type] .type .type)) → validref(str, r, ty, st[r0 -- sk, val]) | A User Theorem |
| validref-put-badarrayfield | ⊦ validref(str, r, ty, st) ∧ fs ' ≠ _type ∧ is_arraytype(st[r0 -- _type] .type) ∧ fs ' ≠ _length → validref(str, r, ty, st[r0 -- fs ', val]) | A User Theorem |
| validref-put-badarrayindex | ⊦ validref(str, r, ty, st) ∧ ¬ is_array(str, r0, st) → validref(str, r, ty, st[r0 -- i ', val]) | A User Theorem |
| validref-put-badclassfield | ⊦ validref(str, r, ty, st) ∧ fs ' ≠ _type ∧ is_classtype(st[r0 -- _type] .type) ∧ ¬ fs ' ∈ instfields(st[r0 -- _type] .type .class) → validref(str, r, ty, st[r0 -- fs ', val]) | A User Theorem |
| validref-put-badfield | ⊦ validref(str, r, ty, st) ∧ ¬ (is_typevalue(st[r0 -- _type]) ∧ is_reftype(st[r0 -- _type] .type)) → validref(str, r, ty, st[r0 -- fs ', val]) | A User Theorem |
| validref-put-byteval | ⊦ r ≠ jvmref ∧ sk ≠ _length ∧ sk ≠ _type ∧ sk .fs .type = byte_type ∧ ¬ is_indexkey(sk) ∧ is_bytevalue(st[r -- sk]) ∧ validref(str, r0, ty, st) → validref(str, r0, ty, st[r -- sk, byteval(by)]) | A User Theorem |
| validref-put-field | ⊦ validref(str, r0, ty0, st) ∧ validref(str, r, ty, st) ∧ is_obj(r, st) ∧ r0 ≠ jvmref ∧ st[r0 -- _type] .type ≤ fs .type ∧ fs ' ∈ instfields(st[r -- _type] .type .class) → validref(str, r, ty, st[r -- fs ', refval(r0)]) | A User Theorem |
| validref-put-field-any | ⊦ validref(str, r, ty, st) ∧ is_fskey(sk) ∧ (is_referencevalue(val) → validref(str, val .refval, sk .fs .type, st) ∧ is_reftype(sk .fs .type)) ∧ (¬ is_referencevalue(val) → is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length) → validref(str, r, ty, st[r0 -- sk, val]) | A User Theorem |
| validref-put-field-refval | ⊦ is_referencevalue(val) ∧ validref(str, val .refval, fs .type, st) ∧ validref(str, r, ty, st) ∧ is_reftype(fs .type) → validref(str, r, ty, st[r0 -- fs ', val]) | A User Theorem |
| validref-put-field-refval-01 | ⊦ is_referencevalue(val) ∧ is_fskey(sk) ∧ validref(str, val .refval, sk .fs .type, st) ∧ validref(str, r, ty, st) ∧ is_reftype(sk .fs .type) → validref(str, r, ty, st[r0 -- sk, val]) | A User Theorem |
| validref-put-norefval | ⊦ ¬ is_referencevalue(val) ∧ validref(str, r, ty, st) ∧ is_fskey(sk) ∧ oktype(val, sk .fs .type, st) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → validref(str, r, ty, st[r1 -- sk, val]) | A User Theorem |
| validref-put-norefval-01 | ⊦ ¬ is_referencevalue(val) ∧ validref(str, r, ty, st) ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → validref(str, r, ty, st[r1 -- sk, val]) | A User Theorem |
| validref-put-norefval-equiv | ⊦ okval(st[r1 -- sk], sk .fs .type) ∧ r1 -- sk ∈ st ∧ ¬ is_referencevalue(val) ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → (validref(str, r, ty, st[r1 -- sk, val]) ↔ validref(str, r, ty, st)) | A User Theorem |
| validref-put-null | ⊦ validref(str, r, ty, st) ∧ is_reftype(fs .type) → validref(str, r, ty, st[r0 -- fs ', refval(jvmref)]) | A User Theorem |
| validref-put-refval | ⊦ validref(str, r, ty0, st) ∧ validref(str, r1, ty, st) ∧ ty ≤ fs .type ∧ is_reftype(fs .type) → validref(str, r, ty0, st[r0 -- fs ', refval(r1)]) | A User Theorem |
| validref-put-shortval | ⊦ r ≠ jvmref ∧ sk ≠ _length ∧ sk .fs .type = short_type ∧ ¬ is_indexkey(sk) ∧ is_shortvalue(st[r -- sk]) ∧ validref(str, r0, ty, st) → validref(str, r0, ty, st[r -- sk, shortval(sho)]) | A User Theorem |
| validref-put-statfield | ⊦ rk1 .ref = jvmref ∧ r ≠ jvmref → (validref(str, r, ty1, st[rk1, val]) ↔ validref(str, r, ty1, st)) | A User Theorem |
| validref-put-statfield-01 | ⊦ rk1 .ref = jvmref ∧ validref(str, r, ty1, st) → validref(str, r, ty1, st[rk1, val]) | A User Theorem |
| validref-put-statfield-02 | ⊦ rk1 .ref = jvmref → (validref(str, r, ty1, st[rk1, val]) ↔ validref(str, r, ty1, st)) | A User Theorem |
| validref-put-statfield-03 | ⊦ validref(str, r, ty1, st[jvmref -- sk, val]) ↔ validref(str, r, ty1, st) | A User Theorem |
| validref-putbar | ⊦ okbytearray(r0, st) ∧ r ≠ r0 ∧ validref(str, r, ty, st) → validref(str, r, ty, putByteArray(bytes, r0, i, st)) | A User Theorem |
| validref-putrkvs | ⊦ validvals(str, rkvs, st) ∧ validref(str, r, ty, st) → validref(str, r, ty, st[rkvs]) | A User Theorem |
| validref-putrkvs-norefval | ⊦ ¬ is_referencevalue(val) ∧ okval(st[r1 -- sk], sk .fs .type) ∧ r1 -- sk ∈ st ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → (validref(str, r, ty, st[((r1 -- sk) × val) ' + rkvs]) ↔ validref(str, r, ty, st[rkvs])) | A User Theorem |
| validref-refin | ⊦ ¬ r ∈ st → (validref(str, r, ty, st) ↔ r = jvmref) | A User Theorem |
| validref-runtimetype | ⊦ validref(str, r, st[r -- _type] .type, st) ↔ ¬ junkref(str, r, st) | A User Theorem |
| validref-subset | ⊦ validref(str, r, ty, st) ∧ st ⊆ st1 → validref(str, r, ty, st1) | A User Theorem |
| validref-subset-01 | ⊦ ¬ junkref(str, r, st) ∧ st ⊆ st0 → (validref(str, r, ty, st0) ↔ validref(str, r, ty, st)) | A User Theorem |
| validref-subtype | ⊦ class ≤ class1 ∧ validref(str, r, mkclasstype(class1), st0) ∧ st0[r -- _type] = typeval(mkclasstype(class)) → validref(str, r, mkclasstype(class), st0) | A User Theorem |
| validref-subtype-01 | ⊦ class ≤ class1 ∧ ¬ validref(str, r, mkclasstype(class), st0) ∧ st0[r -- _type] = typeval(mkclasstype(class)) → ¬ validref(str, r, mkclasstype(class1), st0) | A User Theorem |
| validref-subtype-02 | ⊦ class1 ≤ class ∧ validref(str, r, mkclasstype(class1), st) ∧ type∃(str, mkclasstype(class)) → validref(str, r, mkclasstype(class), st) | A User Theorem |
| validref-supertype | ⊦ validref(str, r, ty, st) ∧ ty ≤ ty0 → validref(str, r, ty0, st) | A User Theorem |
| validref-throw | ⊦ validref(str, r0, ty, st) ∧ newref(r, st) → (¬ validref(str, r0, ty, addobj(r, class, [], st)[_mode, throw(r, mkclasstype(class))]) ↔ false) | A User Theorem |
| validref-type | ⊦ validref(str, r, mkarraytype(int_type), st) ∧ r ≠ jvmref → st[r -- _type] .type = mkarraytype(int_type) | A User Theorem |
| validref-type-forward | ⊦ validref(str, r, ty, st) ∧ st[r -- _type] .type = ty0 → validref(str, r, ty0, st) | A User Theorem |
| validref-type-forward-01 | ⊦ ¬ validref(str, r, ty0, st) ∧ st[r -- _type] .type = ty0 → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-typeex | ⊦ validref(str, r, ty, st) ∧ r ≠ jvmref → type∃(str, st[r -- _type] .type) | A User Theorem |
| validref-typeex-01 | ⊦ ¬ type∃(str, st[r -- _type] .type) ∧ r ≠ jvmref → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-typele | ⊦ r ≠ jvmref ∧ ¬ st[r -- _type] .type ≤ ty → ¬ validref(str, r, ty, st) | A User Theorem |
| validref-union | ⊦ validref(str, r, ty, st) → validref(str, r, ty, st0 ∪ st) | A User Theorem |
| validref-union-left | ⊦ validref(str, r, ty, st0) ∧ st0 .refs ∩ st .refs = ∅ → validref(str, r, ty, st0 ∪ st) | A User Theorem |
| validref-voidtype | ⊦ validref(str, r, void_type, st) ↔ r = jvmref | A User Theorem |
| validrefkeynotnull-addarray | ⊦ newref(r1, st) ∧ validrefkeynotnull(str, rk, ty1, st) → validrefkeynotnull(str, rk, ty1, addarray(r1, ty, vals, st)) | A User Theorem |
| validrefkeynotnull-addobj | ⊦ newref(r1, st) ∧ validrefkeynotnull(str, rk, ty1, st) → validrefkeynotnull(str, rk, ty1, addobj(r1, class, fis, st)) | A User Theorem |
| validrefkeynotnull-has-field | ⊦ validrefkeynotnull(str, rk, mkclasstype(class), st) ∧ sk ∈ instfields(class) ∧ is_fskey(sk) → st[rk] .refval -- sk ∈ st | A User Theorem |
| validrefkeynotnull-in | ⊦ validrefkeynotnull(str, rk, ty, st) → rk ∈ st | A User Theorem |
| validrefkeynotnull-no-newrefs | ⊦ st[r -- sk] .refval = r ∧ newref(r, st) → ¬ validrefkeynotnull(str, r -- sk, ty, st) | A User Theorem |
| validrefkeynotnull-notnewref | ⊦ validrefkeynotnull(str, rk, ty, st) → ¬ newref(st[rk] .refval, st) | A User Theorem |
| validrefkeynotnull-notnull | ⊦ validrefkeynotnull(str, rk, ty, st) → st[rk] .refval ≠ jvmref | A User Theorem |
| validrefkeynotnull-put-byteval | ⊦ r ≠ jvmref ∧ sk ≠ _length ∧ sk ≠ _type ∧ ¬ is_indexkey(sk) ∧ sk .fs .type = byte_type ∧ is_bytevalue(st[r -- sk]) ∧ validrefkeynotnull(str, rk, ty, st) → validrefkeynotnull(str, rk, ty, st[r -- sk, byteval(by)]) | A User Theorem |
| validrefkeynotnull-put-shortval | ⊦ r ≠ jvmref ∧ sk ≠ _length ∧ sk .fs .type = short_type ∧ ¬ is_indexkey(sk) ∧ is_shortvalue(st[r -- sk]) ∧ validrefkeynotnull(str, rk, ty, st) → validrefkeynotnull(str, rk, ty, st[r -- sk, shortval(sho)]) | A User Theorem |
| validrefkeynotnull-put-statfield | ⊦ rk1 .ref = jvmref ∧ rk ≠ rk1 ∧ validrefkeynotnull(str, rk, ty1, st) → validrefkeynotnull(str, rk, ty1, st[rk1, val]) | A User Theorem |
| validrefkeynotnull-refval-in | ⊦ validrefkeynotnull(str, r -- sk, ty, st) → st[r -- sk] .refval ∈ st | A User Theorem |
| validrefkeynotnull-statfield-intersect | ⊦ validrefkeynotnull(str, jvmref -- fs ', ty, st) ∧ st .refs ∩ st1 .refs = ∅ → ¬ jvmref ∈ st1 | A User Theorem |
| validrefkeynotnull-subset | ⊦ validrefkeynotnull(str, rk, ty, st) ∧ st ⊆ st1 → validrefkeynotnull(str, rk, ty, st1) | A User Theorem |
| validrefkeynotnull-union | ⊦ validrefkeynotnull(str, rk, ty, st) ∧ (∃ st0. st1 = st0 ∪ st) → validrefkeynotnull(str, rk, ty, st1) | A User Theorem |
| validrefkeynotnull-union-01 | ⊦ validrefkeynotnull(str, rk, ty, st) → validrefkeynotnull(str, rk, ty, st0 ∪ st) | A User Theorem |
| validrefkeynotnull-union-same | ⊦ validrefkeynotnull(str, r -- fs ', ty, st1) → st1[r -- fs '] = (st ∪ st1)[r -- fs '] | A User Theorem |
| validrefkeynotnull-union-same-01 | ⊦ validrefkeynotnull(str, rk, ty, st1) → st1[rk] = (st ∪ st1)[rk] | A User Theorem |
| validrefkeynotnull-union-same-02 | ⊦ validrefkeynotnull(str, rk, ty, st1) → (st ∪ st1)[rk] = st1[rk] | A User Theorem |
| validrefkeynotnull-validrefnotnull | ⊦ validrefkeynotnull(str, rk, ty1, st) → validrefnotnull(str, st[rk] .refval, ty1, st) | A User Theorem |
| validreflist-addarray | ⊦ validreflist(str, vals, ty1, st) → validreflist(str, vals, ty1, addarray(newref(st), ty, vals0, st)) | A User Theorem |
| validreflist-empty | ⊦ validreflist(str, [], ty, st) | A User Theorem |
| validreflist-getarray | ⊦ validref(str, r, mkarraytype(ty), st) ∧ is_reftype(ty) ∧ r ≠ jvmref → validreflist(str, getarray(r, st), ty, st) | A User Theorem |
| validreflist-getarray-less | ⊦ i < st[r -- _length '] .intval ∧ 0 ≤ i ∧ is_reftype(ty) ∧ validrefnotnull(str, r, mkarraytype(ty), st) → validreflist(str, getarray(r, 0, i, st), ty, st) | A User Theorem |
| validreflist-getarray-less-01 | ⊦ j + i < st[r -- _length '] .intval ∧ 0 ≤ i ∧ 0 ≤ j ∧ is_reftype(ty) ∧ validrefnotnull(str, r, mkarraytype(ty), st) → validreflist(str, getarray(r, j, i, st), ty, st) | A User Theorem |
| validreflist-getarray-less-02 | ⊦ j + i ≤ st[r -- _length '] .intval ∧ 0 ≤ i ∧ 0 ≤ j ∧ is_reftype(ty) ∧ validrefnotnull(str, r, mkarraytype(ty), st) → validreflist(str, getarray(r, j, i, st), ty, st) | A User Theorem |
| validreflist-getarray-less-03 | ⊦ i ≤ st[r -- _length '] .intval ∧ 0 ≤ i ∧ is_reftype(ty) ∧ validrefnotnull(str, r, mkarraytype(ty), st) → validreflist(str, getarray(r, 0, i, st), ty, st) | A User Theorem |
| validreflist-no-reftype | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (validreflist(str, vals, ty, st) ↔ (∀ val. val ∈ vals → val = refval(jvmref))) | A User Theorem |
| validreflist-one | ⊦ validreflist(str, val ', ty, st) ↔ is_referencevalue(val) ∧ validref(str, val .refval, ty, st) | A User Theorem |
| validreflist-one-01 | ⊦ validreflist(str, refval(r) ', ty, st) ↔ validref(str, r, ty, st) | A User Theorem |
| validreflist-rec | ⊦ validreflist(str, val ' + vals, ty, st) ↔ is_referencevalue(val) ∧ validref(str, val .refval, ty, st) ∧ validreflist(str, vals, ty, st) | A User Theorem |
| validreflist-rec-01 | ⊦ validreflist(str, refval(r) ' + vals, ty, st) ↔ validref(str, r, ty, st) ∧ validreflist(str, vals, ty, st) | A User Theorem |
| validreflist-supertype | ⊦ validreflist(str, vals, ty, st) ∧ ty ≤ ty0 → validreflist(str, vals, ty0, st) | A User Theorem |
| validrefnotnull | ⊦ validref(str, r, ty, st) → (validrefnotnull(str, r, ty, st) ↔ r ≠ jvmref) | A User Theorem |
| validrefnotnull-addarray | ⊦ newref(r1, st) ∧ validrefnotnull(str, r, ty1, st) → validrefnotnull(str, r, ty1, addarray(r1, ty, vals, st)) | A User Theorem |
| validrefnotnull-addarray-01 | ⊦ newref(r1, st) ∧ ¬ validrefnotnull(str, r, ty1, addarray(r1, ty, vals, st)) → ¬ validrefnotnull(str, r, ty1, st) | A User Theorem |
| validrefnotnull-addarray-len | ⊦ newref(r1, st) ∧ validrefnotnull(str, r, ty1, st) → validrefnotnull(str, r, ty1, addarray(r1, ty, i, st)) | A User Theorem |
| validrefnotnull-addobj | ⊦ newref(r1, st) ∧ validrefnotnull(str, r, ty1, st) → validrefnotnull(str, r, ty1, addobj(r1, class, fis, st)) | A User Theorem |
| validrefnotnull-array | ⊦ validrefnotnull(str, r, mkarraytype(ty), st) → val2int(st[r -- _length]) = st[r -- _length] .intval | A User Theorem |
| validrefnotnull-array-01 | ⊦ validrefnotnull(str, r, mkarraytype(ty), st) → is_integervalue(st[r -- _length]) | A User Theorem |
| validrefnotnull-array-02 | ⊦ validrefnotnull(str, r, mkarraytype(ty), st) → ¬ st[r -- _length] .intval < 0 | A User Theorem |
| validrefnotnull-array-len-subset | ⊦ st ⊆ st0 ∧ val2int(st[r -- _length]) ≠ st0[r -- _length] .intval → ¬ validrefnotnull(`docs2store', r, mkarraytype(byte_type), st) | A User Theorem |
| validrefnotnull-bytearray | ⊦ validrefnotnull(str, r, mkarraytype(byte_type), st) ↔ okbytearray(r, st) | A User Theorem |
| validrefnotnull-getarray-subset | ⊦ validrefnotnull(str, r, mkarraytype(ty), st) ∧ 0 ≤ i ∧ i + j ≤ st[r -- _length] .intval ∧ st ⊆ st1 → getarray(r, i, j, st) = getarray(r, i, j, st1) | A User Theorem |
| validrefnotnull-is-junk | ⊦ r = jvmref ∨ ¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ ty ∧ ¬ type∃(str, st[r -- _type] .type) → ¬ validrefnotnull(str, r, ty, st) | A User Theorem |
| validrefnotnull-isarray | ⊦ validrefnotnull(str, r, mkarraytype(ty), st) → (¬ is_array(str, r, st) ↔ false) | A User Theorem |
| validrefnotnull-isvalidref | str ≠ `java.lang.Object' ⊦ validrefnotnull(str0, r, mkclasstype(((* str)) .class), st) → (is_valid_ref(str0, r, st) ↔ is_obj(str0, r, st)) | A User Theorem |
| validrefnotnull-junk | ⊦ junkref(str, r, st) → ¬ validrefnotnull(str, r, ty, st) | A User Theorem |
| validrefnotnull-no-len | ⊦ ¬ r -- _length ∈ st → ¬ validrefnotnull(str, r, mkarraytype(ty), st) | A User Theorem |
| validrefnotnull-no-newref | ⊦ newref(r, st) → ¬ validrefnotnull(str, r, ty, st) | A User Theorem |
| validrefnotnull-no-type | ⊦ ¬ r -- _type ∈ st → ¬ validrefnotnull(str, r, ty, st) | A User Theorem |
| validrefnotnull-not | ⊦ ¬ validrefnotnull(str, r, ty, st) ∧ r ≠ jvmref → ¬ validref(str, r, ty, st) | A User Theorem |
| validrefnotnull-notnull | ⊦ validrefnotnull(str, r, ty, st) → r ≠ jvmref | A User Theorem |
| validrefnotnull-null | ⊦ ¬ validrefnotnull(str, jvmref, ty, st) | A User Theorem |
| validrefnotnull-primarray | ⊦ is_primtype(ty) → (validrefnotnull(str, r, mkarraytype(ty), st) ↔ okarray(r, ty, st)) | A User Theorem |
| validrefnotnull-put-byteval | ⊦ r ≠ jvmref ∧ sk ≠ _length ∧ sk ≠ _type ∧ ¬ is_indexkey(sk) ∧ sk .fs .type = byte_type ∧ is_bytevalue(st[r -- sk]) ∧ validrefnotnull(str, r0, ty, st) → validrefnotnull(str, r0, ty, st[r -- sk, byteval(by)]) | A User Theorem |
| validrefnotnull-put-shortval | ⊦ r ≠ jvmref ∧ sk ≠ _length ∧ sk .fs .type = short_type ∧ ¬ is_indexkey(sk) ∧ is_shortvalue(st[r -- sk]) ∧ validrefnotnull(str, r0, ty, st) → validrefnotnull(str, r0, ty, st[r -- sk, shortval(sho)]) | A User Theorem |
| validrefnotnull-put-statfield | ⊦ rk1 .ref = jvmref ∧ r ≠ jvmref ∧ validrefnotnull(str, r, ty1, st) → validrefnotnull(str, r, ty1, st[rk1, val]) | A User Theorem |
| validrefnotnull-put-statfield-01 | ⊦ rk1 .ref = jvmref ∧ r ≠ jvmref ∧ ¬ validrefnotnull(str, r, ty1, st[rk1, val]) → ¬ validrefnotnull(str, r, ty1, st) | A User Theorem |
| validrefnotnull-put-statfield-02 | ⊦ rk1 .ref = jvmref ∧ r ≠ jvmref → (validrefnotnull(str, r, ty1, st[rk1, val]) ↔ validrefnotnull(str, r, ty1, st)) | A User Theorem |
| validrefnotnull-putbar | ⊦ okbytearray(r0, st) ∧ r ≠ r0 ∧ validrefnotnull(str, r, ty, st) → validrefnotnull(str, r, ty, putByteArray(bytes, r0, i, st)) | A User Theorem |
| validrefnotnull-subset | ⊦ validrefnotnull(str, r, ty, st) ∧ st ⊆ st1 → validrefnotnull(str, r, ty, st1) | A User Theorem |
| validrefnotnull-type | ⊦ validrefnotnull(str, r, mkarraytype(int_type), st) → st[r -- _type] .type = mkarraytype(int_type) | A User Theorem |
| validrefnotnull-typeex | ⊦ ¬ type∃(str, st[r -- _type] .type) → ¬ validrefnotnull(str, r, ty, st) | A User Theorem |
| validrefnotnull-union-at-right | ⊦ validrefnotnull(str, r, ty, st0) ∧ is_classtype(ty) ∧ sk ∈ instfields(ty .class) ∧ is_fskey(sk) → (st ∪ st0)[r -- sk] = st0[r -- sk] | A User Theorem |
| validrefnotnull-validref | ⊦ ¬ validref(str, r, ty, st) → ¬ validrefnotnull(str, r, ty, st) | A User Theorem |
| validrefval-addarray | ⊦ validrefval(str, val, ty, st) ∧ newref(r, st) → validrefval(str, val, ty, addarray(r, ty0, vals, st)) | A User Theorem |
| validrefval-addobj | ⊦ validrefval(str, val, ty, st) ∧ newref(r, st) → validrefval(str, val, ty, addobj(r, class, fis, st)) | A User Theorem |
| validrefval-junkref | ⊦ junkref(str, val .refval, st) → ¬ validrefval(str, val, ty, st) | A User Theorem |
| validrefval-put-statfield | ⊦ rk .ref = jvmref → (validrefval(str, val, ty, st[rk, val0]) ↔ validrefval(str, val, ty, st)) | A User Theorem |
| validrefval-put-statfield-01 | ⊦ validrefval(str, val, ty, st[jvmref -- sk, val0]) ↔ validrefval(str, val, ty, st) | A User Theorem |
| validrefval-ref | ⊦ validrefval(str, refval(r), ty, st) ↔ validref(str, r, ty, st) | A User Theorem |
| validrefval-superset | ⊦ st ⊆ st0 ∧ validrefval(str, val, ty, st) → validrefval(str, val, ty, st0) | A User Theorem |
| validrefval-union | ⊦ validrefval(str, val, ty, st) → validrefval(str, val, ty, st0 ∪ st) | A User Theorem |
| validrefvalnotnull-addarray | ⊦ newref(r1, st) ∧ validrefvalnotnull(str, val, ty1, st) → validrefvalnotnull(str, val, ty1, addarray(r1, ty, vals, st)) | A User Theorem |
| validrefvalnotnull-addobj | ⊦ newref(r1, st) ∧ validrefvalnotnull(str, val, ty1, st) → validrefvalnotnull(str, val, ty1, addobj(r1, class, fis, st)) | A User Theorem |
| validrefvalnotnull-put-statfield | ⊦ rk1 .ref = jvmref ∧ rk ≠ rk1 ∧ validrefvalnotnull(str, val1, ty1, st) → validrefvalnotnull(str, val1, ty1, st[rk1, val]) | A User Theorem |
| validstatfield-addclass-other | ⊦ is_fskey(sk) ∧ sk .fs .class ≠ class ∧ class ≠ `java.lang.Object' .class → (validstatfield(str, sk, addclass(class, fis, st)) ↔ validstatfield(str, sk, st)) | A User Theorem |
| validstatfield-addclass-same | ⊦ validval(str, fis[sk], sk .fs .type, st) ∧ sk ∈ statfields(class) ∧ tdname∃(str, class) ∧ type∃(str, sk .fs .type) ∧ is_fskey(sk) ∧ sk .fs .class = class ∧ sk ∈ fis ∧ class ≠ `java.lang.Object' .class → validstatfield(str, sk, addclass(class, fis, st)) | A User Theorem |
| validstatfield-addobj | ⊦ validstatfield(str, sk, st) ∧ newref(r, st) → validstatfield(str, sk, addobj(r, class, fis, st)) | A User Theorem |
| validstatfield-index | ⊦ is_indexkey(sk) → ¬ validstatfield(str, sk, st) | A User Theorem |
| validstatfield-level-expand | ⊦ validstatfields(str, st) ↔ (∀ class, sk. tdname∃(str, class) ∧ initdone(class, st) ∧ sk ∈ statfields(class) → validstatfield(str, sk, st)) | A User Theorem |
| validstatfield-levelsubset | ⊦ validstatfield(str, sk, st) ∧ level⊆(str, str0) → validstatfield(str0, sk, st) | A User Theorem |
| validstatfield-mode | ⊦ sk ∈ statfields(class) → (validstatfield(str, sk, st[_mode, val]) ↔ validstatfield(str, sk, st)) | A User Theorem |
| validstatfield-other-statfield | ⊦ ¬ tdname∃(str, fs .class) ∧ fs .class ≠ `java.lang.Object' .class → ¬ validstatfield(str, fs ', st) | A User Theorem |
| validstatfield-primtype-level | ⊦ is_primtype(fs .type) ∧ validstatfield(str, fs ', st) ∧ tdname+∃(str, fs .class) ∧ tdname+∃(str0, fs .class) → validstatfield(str0, fs ', st) | A User Theorem |
| validstatfield-put-array-norefval | ⊦ ¬ is_referencevalue(val) ∧ validstatfield(str, sk, st) ∧ okval(val, st[r1 -- _type] .type .type) → validstatfield(str, sk, st[r1 -- i ', val]) | A User Theorem |
| validstatfield-put-norefval | ⊦ ¬ is_referencevalue(val) ∧ validstatfield(str, sk0, st) ∧ is_fskey(sk) ∧ oktype(val, sk .fs .type, st) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length → validstatfield(str, sk0, st[r -- sk, val]) | A User Theorem |
| validstatfield-put-statfield | ⊦ sk ≠ sk0 ∧ ( ¬ is_fskey(sk) ∨ sk .fs .type ≠ void_type ∨ sk .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field) ∧ (¬ is_fskey(sk0) ∨ sk .fs ≠ mkfs(sk0 .fs .class, void_type, `initstate' .field))) → (validstatfield(str, sk0, st[jvmref -- sk, val]) ↔ validstatfield(str, sk0, st)) | A User Theorem |
| validstatfield-put-statfield-int | ⊦ validstatfield(str, mkfs(class, int_type, fieldvar) ', st) → validstatfield(str, mkfs(class, int_type, fieldvar) ', st[jvmref -- mkfs(class, int_type, fieldvar) ', intval(i)]) | A User Theorem |
| validstatfield-putbytearray-noreftype | ⊦ ¬ is_reftype(sk .fs .type) → (validstatfield(str, sk, putByteArray(bytes, r, i, st)) ↔ validstatfield(str, sk, st)) | A User Theorem |
| validstatfield-putrkvs | ⊦ validvals(str, rkvs, st) ∧ validstatfield(str, sk, st) → validstatfield(str, sk, st[rkvs]) | A User Theorem |
| validstatfield-subset | ⊦ validstatfield(str, sk, st) ∧ st ⊆ st0 ∧ initdone(sk .fs .class, st0) ∧ initdone(sk .fs .class, st) → validstatfield(str, sk, st0) | A User Theorem |
| validstatfield-throw-predef | ⊦ validstatfield(str, sk, st) ∧ is_predefined_class(class) ∧ newref(r, st) → validstatfield(str, sk, addobj(r, class, [], st)[_mode, throw(r, mkclasstype(class))]) | A User Theorem |
| validstatfield-union | ⊦ validstatfield(str, sk, st0) ∧ ¬ jvmref ∈ st → validstatfield(str, sk, st ∪ st0) | A User Theorem |
| validstatfield-validref | ⊦ validstatfield(str, sk, st) ∧ initdone(sk .fs .class, st) → validref(str, st[jvmref -- sk] .refval, sk .fs .type, st) | A User Theorem |
| validstatfield-void | ⊦ ¬ validstatfield(str, mkfs(class, void_type, fieldvar) ', st) | A User Theorem |
| validstatfields-addclass | ⊦ validfieldinits(str, fis, st) ∧ fis .keys = statfields(class) ∧ class ≠ `java.lang.Object' .class ∧ tdname∃(str, class) → validstatfields(str, statfields(class), addclass(class, fis, st)) | A User Theorem |
| validstatfields-addclass-other | ⊦ class ≠ class0 ∧ class ≠ `java.lang.Object' .class → (validstatfields(str, statfields(class0), addclass(class, fis, st)) ↔ validstatfields(str, statfields(class0), st)) | A User Theorem |
| validstatfields-addobj | ⊦ validstatfields(str, sks, st) ∧ newref(r, st) → validstatfields(str, sks, addobj(r, class, fis, st)) | A User Theorem |
| validstatfields-addobj-01 | ⊦ validstatfields(str, st) ∧ newref(r, st) → validstatfields(str, addobj(r, class, fis, st)) | A User Theorem |
| validstatfields-class-01 | ⊦ initdone(class, st) ∧ tdname∃(str, class) → (validstatfields(str, class, st) ↔ (∀ sk. sk ∈ statfields(class) → validstatfield(str, sk, st))) | A User Theorem |
| validstatfields-empty | ⊦ validstatfields(str, [], st) | A User Theorem |
| validstatfields-empty-01 | ∀ class. tdname∃(str, class) → statfields(class) = [] ⊦ validstatfields(str, st) | A User Theorem |
| validstatfields-initundone | ⊦ ¬ initdone(class, st) → (validstatfields(str, statfields(class), st) ↔ statfields(class) = [] ∨ tdname∃(str, class)) | A User Theorem |
| validstatfields-levelsubset | ⊦ validstatfields(str, sks, st) ∧ level⊆(str, str0) → validstatfields(str0, sks, st) | A User Theorem |
| validstatfields-one | ⊦ validstatfields(str, sk ', st) ↔ validstatfield(str, sk, st) | A User Theorem |
| validstatfields-put-array-norefval | ⊦ validstatfields(str, st) ∧ ¬ is_referencevalue(val) ∧ okval(val, st[r1 -- _type] .type .type) → validstatfields(str, st[r1 -- i ', val]) | A User Theorem |
| validstatfields-put-byteval | ⊦ validstatfields(str, st) ∧ r ≠ jvmref ∧ ¬ is_indexkey(sk) ∧ sk .fs .type = byte_type → validstatfields(str, st[r -- sk, byteval(by)]) | A User Theorem |
| validstatfields-put-byteval-01 | ⊦ ¬ validstatfields(str, st[r -- sk, byteval(by)]) ∧ r ≠ jvmref ∧ ¬ is_indexkey(sk) ∧ sk .fs .type = byte_type → ¬ validstatfields(str, st) | A User Theorem |
| validstatfields-put-norefval-field | ⊦ validstatfields(str, st) ∧ ¬ is_referencevalue(val) ∧ r ≠ jvmref ∧ ¬ is_indexkey(sk) ∧ okval(val, sk .fs .type) ∧ sk ≠ _length ∧ sk ≠ _type → validstatfields(str, st[r -- sk, val]) | A User Theorem |
| validstatfields-put-norefval-field-better | ⊦ validstatfields(str, st) ∧ ¬ is_referencevalue(val) ∧ is_fskey(sk) ∧ okval(val, sk .fs .type) ∧ sk ≠ _length → validstatfields(str, st[r -- sk, val]) | A User Theorem |
| validstatfields-put-other-statfield | ⊦ ¬ tdname∃(str, fs .class) ∧ fs .class ≠ `java.lang.Object' .class → (validstatfields(str, st[jvmref -- fs ', val]) ↔ validstatfields(str, st)) | A User Theorem |
| validstatfields-put-statfield | ⊦ rk .ref = jvmref ∧ ¬ rk .key ∈ sks ∧ ( ¬ is_fskey(rk .key) ∨ rk .key .fs .type ≠ void_type ∨ rk .key .fs .field ≠ `initstate' .field ∧ rk .key .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field)) → (validstatfields(str, sks, st[rk, val]) ↔ validstatfields(str, sks, st)) | A User Theorem |
| validstatfields-put-statfield-01 | ⊦ ¬ sk ∈ sks ∧ ( ¬ is_fskey(sk) ∨ sk .fs .type ≠ void_type ∨ sk .fs .field ≠ `initstate' .field ∧ sk .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field)) → (validstatfields(str, sks, st[jvmref -- sk, val]) ↔ validstatfields(str, sks, st)) | A User Theorem |
| validstatfields-put-statfield-02 | ⊦ validstatfield(str, sk, st[jvmref -- sk, val]) ∧ validstatfields(str, sks, st) ∧ ( ¬ is_fskey(sk) ∨ sk .fs .type ≠ void_type ∨ sk .fs .field ≠ `initstate' .field ∧ sk .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field)) → validstatfields(str, sks, st[jvmref -- sk, val]) | A User Theorem |
| validstatfields-put-statfield-03 | ⊦ validstatfields(str, sks, st) ∧ (¬ sk ∈ statfields(sk .fs .class) ∨ ¬ tdname∃(str, sk .fs .class)) ∧ is_fskey(sk) ∧ (sk .fs .type ≠ void_type ∨ sk .fs .field ≠ `initstate' .field ∧ sk .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field)) → validstatfields(str, sks, st[jvmref -- sk, val]) | A User Theorem |
| validstatfields-put-statfield-04 | ⊦ sk ≠ sk0 ∧ ( ¬ is_fskey(sk0) ∨ sk0 .fs .type ≠ void_type ∨ sk0 .fs .field ≠ `initstate' .field ∧ sk0 .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field)) → (validstatfields(str, sk ' + sks, st[jvmref -- sk0, val]) ↔ validstatfield(str, sk, st) ∧ validstatfields(str, sks, st[jvmref -- sk0, val])) | A User Theorem |
| validstatfields-put-statfield-05 | str ≠ str0, str0 ≠ `initstate', str0 ≠ `uninit' ⊦ validstatfields(str2, mkfs(class, ty, ((* str)) .field) ' ' + sks, st[jvmref -- mkfs(class0, ty0, ((* str0)) .field) ', val]) ↔ ¬ ¬ (validstatfield(str2, mkfs(class, ty, str .field) ', st) ∧ validstatfields(str2, sks, st[jvmref -- mkfs(class0, ty0, str0 .field) ', val])) | A User Theorem |
| validstatfields-put-statfield-06 | ⊦ ¬ sk ∈ statfields(class) ∧ ( ¬ is_fskey(sk) ∨ sk .fs .type ≠ void_type ∨ sk .fs ≠ mkfs(`java.lang.Object' .class, void_type, `uninit' .field) ∧ sk .fs ≠ mkfs(class, void_type, `initstate' .field)) → (validstatfields(str, statfields(class), st[jvmref -- sk, val]) ↔ validstatfields(str, statfields(class), st)) | A User Theorem |
| validstatfields-rec | ⊦ validstatfields(str, sk ' + sks, st) ↔ validstatfield(str, sk, st) ∧ validstatfields(str, sks, st) | A User Theorem |
| validstatfields-subset | ⊦ validstatfields(str, st) ∧ st ⊆ st0 ∧ init(str, st) ∧ init(str, st0) → validstatfields(str, st0) | A User Theorem |
| validstatfields-throw-predef | ⊦ validstatfields(str, sks, st) ∧ is_predefined_class(class) ∧ newref(r, st) → validstatfields(str, sks, addobj(r, class, [], st)[_mode, throw(r, mkclasstype(class))]) | A User Theorem |
| validstatfields-throw-predef-01 | ⊦ validstatfields(str, sks, st) ∧ newref(r, st) → validstatfields (str, sks, addobj(r, `java.lang.NoClassDefFoundError' .class, [], st)[_mode, throw(r, mkclasstype(`java.lang.NoClassDefFoundError' .class))]) | A User Theorem |
| validstatfields-throw-predef-02 | ⊦ validstatfields(str, sks, st) ∧ newref(r, st) → validstatfields (str, sks, addobj(r, `java.lang.NullPointerException' .class, [], st)[_mode, throw(r, mkclasstype(`java.lang.NullPointerException' .class))]) | A User Theorem |
| validstatfields-union | ⊦ validstatfields(str, st0) ∧ ¬ jvmref ∈ st → validstatfields(str, st ∪ st0) | A User Theorem |
| validstatfields-validstatfield | ⊦ validstatfields(str, st) ↔ (∀ class. tdname∃(str, class) ∧ initdone(class, st) → validstatfields(str, class, st)) | A User Theorem |
| validstatfields-validstatfield-01 | ⊦ ¬ validstatfield(str, sk, st) ∧ sk ∈ statfields(class) ∧ tdname∃(str, class) ∧ initdone(class, st) → ¬ validstatfields(str, st) | A User Theorem |
| validstatfields-void | ⊦ mkfs(class, void_type, fieldvar) ' ∈ sks → ¬ validstatfields(str, sks, st) | A User Theorem |
| validsubset-addclass | ⊦ valid⊆(str, st, addclass(class, fis, st)) | A User Theorem |
| validsubset-addclass-01 | ⊦ valid⊆(str, st, st0) → valid⊆(str, st, addclass(class, fis, st0)) | A User Theorem |
| validsubset-addobj | ⊦ newref(r, st) ∧ class∃(str, class) ∧ fis .keys = instfields(class) ∧ validfieldinits(fis, st) ∧ ¬ is_abstract(class) ∧ class+∃(str, class) ∧ (∀ sk, r1. sk × refval(r1) ∈ fis → ¬ junkref(str, r1, st)) → valid⊆(str, st, addobj(r, class, fis, st)) | A User Theorem |
| validsubset-addobj-01 | ⊦ newref(r, st) ∧ class∃(str, class) ∧ fis .keys = instfields(class) ∧ validfieldinits(fis, st) ∧ ¬ junkrefs(str, fis .vals, st) ∧ ¬ is_abstract(class) → valid⊆(str, st, addobj(r, class, fis, st)) | A User Theorem |
| validsubset-addobj-02 | ⊦ valid⊆(str, st, st0) ∧ newref(r, st0) ∧ class∃(str, class) ∧ fis .keys = instfields(class) ∧ validfieldinits(fis, st0) ∧ ¬ junkrefs(str, fis .vals, st0) ∧ ¬ is_abstract(class) → valid⊆(str, st, addobj(r, class, fis, st0)) | A User Theorem |
| validsubset-okbytearray | ⊦ ¬ okbytearray(r, st0) ∧ valid⊆(str, st, st0) → ¬ okbytearray(r, st) | A User Theorem |
| validsubset-okbytearray-01 | ⊦ okbytearray(r, st) ∧ valid⊆(str, st, st0) → okbytearray(r, st0) | A User Theorem |
| validsubset-predefined | ⊦ is_predefined_class(class) ∧ newref(r, st) → valid⊆(str, st, addobj(r, class, [], st)) | A User Theorem |
| validsubset-predefined-01 | ⊦ valid⊆(str, st, st0) ∧ is_predefined_class(class) ∧ newref(r, st0) → (¬ valid⊆(str, st, addobj(r, class, [], st0)) ↔ false) | A User Theorem |
| validsubset-predefined-02 | ⊦ newref(r, st) → valid⊆(str, st, addobj(r, `java.lang.NoClassDefFoundError' .class, [], st)) | A User Theorem |
| validsubset-predefined-03 | ⊦ newref(r, st) → valid⊆(str, st, addobj(r, `java.lang.NullPointerException' .class, [], st)) | A User Theorem |
| validsubset-put-statfield | ⊦ rk .ref = jvmref → (valid⊆(str, st, st0[rk, val]) ↔ valid⊆(str, st, st0)) | A User Theorem |
| validsubset-put-statfield-01 | ⊦ valid⊆(str, st, st0[jvmref -- sk, val]) ↔ valid⊆(str, st, st0) | A User Theorem |
| validsubset-put-statfield-02 | ⊦ valid⊆(str, st, st0[_mode, val]) ↔ valid⊆(str, st, st0) | A User Theorem |
| validsubset-same | ⊦ valid⊆(str, st, st) | A User Theorem |
| validsubset-trans | ⊦ valid⊆(str, st, st0) ∧ valid⊆(str, st0, st1) → valid⊆(str, st, st1) | A User Theorem |
| validsubset-validref-forward | ⊦ valid⊆(str, st, st0) ∧ validref(str, r, ty, st) → validref(str, r, ty, st0) | A User Theorem |
| validval-field-byteval | ⊦ validval(str, r -- fs ', byteval(by), st) ↔ fs .type = byte_type | A User Theorem |
| validval-field-norefval | ⊦ ¬ is_referencevalue(val) → (validval(str, r -- fs ', val, st) ↔ okval(val, fs .type) ∧ fs ' ≠ _length) | A User Theorem |
| validval-field-shortval | ⊦ validval(str, r -- fs ', shortval(sho), st) ↔ fs .type = short_type | A User Theorem |
| validval-index-byteval | ⊦ validval(str, r -- i ', byteval(by), st) ↔ st[r -- _type] .type .type = byte_type | A User Theorem |
| validval-index-norefval | ⊦ ¬ is_referencevalue(val) → (validval(str, r -- i ', val, st) ↔ okval(val, st[r -- _type] .type .type)) | A User Theorem |
| validval-int | ⊦ validval(str, intval(i), int_type, st) | A User Theorem |
| validval-null | ⊦ validval(str, refval(jvmref), mkclasstype(class), st) | A User Theorem |
| validval-put-any | ⊦ validval(str, rk, val, st) ∧ validval(str, rk0, val0, st) → validval(str, rk0, val0, st[rk, val]) | A User Theorem |
| validval-putrkvs | ⊦ validval(str, rk, val, st) ∧ validvals(str, rkvs, st) → validval(str, rk, val, st[rkvs]) | A User Theorem |
| validvals-append | ⊦ validvals(str, rkvs + rkvs0, st) ↔ validvals(str, rkvs, st) ∧ validvals(str, rkvs0, st) | A User Theorem |
| validvals-append-01 | ⊦ validvals(str, rkvs + rkvs0, st) ↔ ¬ ¬ (validvals(str, rkvs, st) ∧ validvals(str, rkvs0, st)) | A User Theorem |
| validvals-one | ⊦ validvals(str, rkv ', st) ↔ validval(str, rkv .1, rkv .2, st) | A User Theorem |
| validvals-put-any | ⊦ validval(str, rk, val, st) ∧ validvals(str, rkvs, st) → validvals(str, rkvs, st[rk, val]) | A User Theorem |
| validvals-putrkvs | ⊦ validvals(str, rkvs0, st) ∧ validvals(str, rkvs1, st) → validvals(str, rkvs0, st[rkvs1]) | A User Theorem |
| validvals-voidtype | ⊦ validvals(str, rkvs, st) → ¬ r -- mkfs(class, void_type, fieldvar) ' ∈ rkvs | A User Theorem |
| validvals-voidtype-01 | ⊦ validvals(str, rkvs, st) → ¬ _uninit ∈ rkvs | A User Theorem |
| validvals-voidtype-02 | ⊦ validvals(str, rkvs, st) → ¬ r -- _type ∈ rkvs | A User Theorem |