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: |
|---|---|---|
| instore | ⊦ r ∈ st ↔ (∃ sk. r -- sk ∈ st) | An Axiom |
| out | ⊦ _out(st) = flatten(st[_out]) | An Axiom |
| normalmode | ⊦ normalmode(st) ↔ _mode ∈ st ∧ st[_mode] = noval | An Axiom |
| newref | ⊦ newref(r, st) ↔ r ≠ jvmref ∧ (∀ rk. rk ∈ st → rk .ref ≠ r) | An Axiom |
| initerror | ⊦ initerror(class1, st) ↔ (jvmref -- mkfs(class1, void_type, `initstate' .field) ') × initval(error) ∈ st | An Axiom |
| initundone | ⊦ initundone(class1, st) ↔ (jvmref -- mkfs(class1, void_type, `initstate' .field) ') × initval(undone) ∈ st ∨ ¬ jvmref -- mkfs(class1, void_type, `initstate' .field) ' ∈ st ∧ _uninit ∈ st | An Axiom |
| initdone | ⊦ initdone(class1, st) ↔ ¬ initerror(class1, st) ∧ ¬ initundone(class1, st) | An Axiom |
| list_ok | ⊦ is_newref_list(refs, st) ↔ ¬ dups(refs) ∧ (∀ r. r ∈ refs → newref(r, st)) | An Axiom |
| deleteref | ⊦ ¬ r ∈ st -- r ∧ (∀ r0, sk. r ≠ r0 → (r0 -- sk ∈ st ↔ r0 -- sk ∈ st -- r) ∧ st[r0 -- sk] = (st -- r)[r0 -- sk]) | An Axiom |
| init-04 | ⊦ init(st) ↔ (∀ class1. initdone(class1, st)) | An Axiom |
| maxref-ok | ⊦ r ∈ st → maxref(st) ∈ st ∧ (∀ r. r ∈ st → ¬ maxref(st) < r) | An Axiom |
| maxref-empty | ⊦ ¬ (∃ r. r ∈ st) → maxref(st) = jvmref | An Axiom |
| newref-fun | ⊦ newref(st) = next(maxref(st)) | An Axiom |
| newrefs-succ | ⊦ newref_list(n + 1, st) = newref(st) + newref_list(n, st[newref(st) -- 0 ', noval]) | An Axiom |
| newrefs-zero | ⊦ newref_list(0, st) = [] | An Axiom |
| uninit | ⊦ uninit(st) ↔ (∀ class1. initundone(class1, st)) | An Axiom |
| initundoneP | ⊦ initundoneP(class, st) ↔ ¬ is_predefined_class(class) ∧ initundone(class, st) | An Axiom |
| initdoneP | ⊦ initdoneP(class, st) ↔ is_predefined_class(class) ∨ initdone(class, st) | An Axiom |
| jump | ⊦ jump(st) ↔ _mode ∈ st ∧ ¬ is_normal_mode(st[_mode]) | An Axiom |
| is_the_newref | ⊦ is_the_newref(r, st) ↔ r = newref(st) | An Axiom |
| is_a_newref | ⊦ is_a_newref(r, st) ↔ r ≠ jvmref ∧ ¬ r ∈ st | An Axiom |
| lookup-rec | ⊦ st[r -- (sk ' + sk0 ' + sks)] = st[st[r -- sk] .refval -- (sk0 ' + sks)] | An Axiom |
| lookup-one | ⊦ st[r -- sk '] = st[r -- sk] | An Axiom |
| lookup-storerefs | ⊦ st[sks] = st[jvmref -- sks] | An Axiom |
| put-rec | ⊦ st[r -- (sk ' + sk0 ' + sks), val] = st[st[r -- sk] .refval -- (sk0 ' + sks), val] | An Axiom |
| put-one | ⊦ st[r -- sk ', val] = st[r -- sk, val] | An Axiom |
| put-storerefs | ⊦ st[sks, val] = st[jvmref -- sks, val] | An Axiom |
| put-staticfield | ⊦ st[sk, val] = st[jvmref -- sk, val] | An Axiom |
| lookup-staticfield | ⊦ st[sk] = st[jvmref -- sk] | An Axiom |
| instore-rec | ⊦ r -- (sk ' + sk0 ' + sks) ∈ st ↔ r -- sk ∈ st ∧ st[r -- sk] .refval -- (sk0 ' + sks) ∈ st | An Axiom |
| instore-one | ⊦ r -- sk ' ∈ st ↔ r -- sk ∈ st | An Axiom |
| init-existing | ⊦ init(str, st) ↔ (∀ class. tdname∃(str, class) → initdone(class, st)) | An Axiom |
| lookup-empty | ⊦ st[r -- []] = refval(r) | An Axiom |
| instore-empty | ⊦ r -- [] ∈ st ↔ r ∈ st | An Axiom |
| put-refkeyvalues-rec | ⊦ st[(rk × val) ' + rkvs] = (st[rk, val][rkvs]) | An Axiom |
| put-refkeyvalues-empty | ⊦ st[[]] = st | An Axiom |
| uninit-existing | ⊦ uninit(str, st) ↔ (∀ class. tdname∃(str, class) → initundone(class, st)) | An Axiom |
| catch-continue | ⊦ catch_continue(st) = ((st[_mode] = continue(`' .label) ⊃ st[_mode, noval]; st)) | An Axiom |
| catch-break | ⊦ catch_break(st) = ((st[_mode] = break(`' .label) ⊃ st[_mode, noval]; st)) | An Axiom |
| getrefs-rec | ⊦ getrefs(r, sk ' + sks, st) = r ' + getrefs(st[r -- sk] .refval, sks, st) | An Axiom |
| getrefs-empty | ⊦ getrefs(r, [], st) = r ' | An Axiom |
| at-put-first | ⊦ rk = jvmref -- sk ∧ sks ≠ [] → (st[rk, val][sk ' + sks]) = (st[rk, val][val .refval -- sks]) | A User Theorem |
| at-put-first-01 | ⊦ ¬ sk ∈ sks ∧ sks ≠ [] → (st[r -- sk, val][r -- (sk ' + sks)]) = st[val .refval -- sks] | A User Theorem |
| at-put-first-02 | ⊦ sk ≠ sk0 → (st[r -- sk, val][r -- (sk ' + sk0 ')]) = st[val .refval -- sk0] | A User Theorem |
| at-put-first-03 | str ≠ str0 ⊦ (st[r -- mkfs(class, ty, ((* str)) .field) ', val][r -- (mkfs(class, ty, ((* str)) .field) ' ' + mkfs(class0, ty0, ((* str0)) .field) ' ')]) = st[val .refval -- mkfs(class0, ty0, str0 .field) '] | A User Theorem |
| at-put-first-04 | ⊦ sks0 ≠ [] → (st[r -- (sk ' + sk0 '), val][st[r -- sk] .refval -- (sk0 ' + sks0)]) = (st[r -- (sk ' + sk0 '), val][val .refval -- sks0]) | A User Theorem |
| at-put-first-05 | ⊦ (st[r -- (sk ' + sk0 '), val][st[r -- sk] .refval -- (sk0 ' + sk1 ')]) = (st[r -- (sk ' + sk0 '), val][val .refval -- sk1 ']) | A User Theorem |
| at-put-first-06 | ⊦ (st[r -- (sk ' + sk0 '), val][st[r -- sk] .refval -- (sk0 ' + sk1 ' + sks)]) = (st[r -- (sk ' + sk0 '), val][val .refval -- (sk1 ' + sks)]) | A User Theorem |
| at-put-first-rec | ⊦ sk ≠ sk0 ∧ sks ≠ [] → (st[r -- sk, val][r0 -- (sk0 ' + sks)]) = (st[r -- sk, val][st[r0 -- sk0] .refval -- sks]) | A User Theorem |
| at-put-first-rec-01 | ⊦ sk ≠ sk0 → (st[r -- sk, val][r0 -- (sk0 ' + sk1 ')]) = (st[r -- sk, val][st[r0 -- sk0] .refval -- sk1]) | A User Theorem |
| at-put-first-rec-02 | ⊦ sk ≠ sk0 → (st[r -- sk, val][r0 -- (sk0 ' + sk1 ' + sks)]) = (st[r -- sk, val][st[r0 -- sk0] .refval -- (sk1 ' + sks)]) | A User Theorem |
| at-put-first-rec-03 | str ≠ str0 ⊦ (st[r -- mkfs(class, ty, ((* str)) .field) ', val][r0 -- (mkfs(class0, ty0, ((* str0)) .field) ' ' + sk1 ')]) = (st[r -- mkfs(class, ty, str .field) ', val][st[r0 -- mkfs(class0, ty0, str0 .field) '] .refval -- sk1]) | A User Theorem |
| at-put-first-rec-04 | str ≠ str0 ⊦ (st[r -- mkfs(class, ty, ((* str)) .field) ', val][r0 -- (mkfs(class0, ty0, str0 .field) ' ' + sk1 ' + sks)]) = (st[r -- mkfs(class, ty, str .field) ', val][st[r0 -- mkfs(class0, ty0, str0 .field) '] .refval -- (sk1 ' + sks)]) | A User Theorem |
| at-put-keys | str ≠ str0 ⊦ (st[r -- (sks + mkfs(class, ty, ((* str)) .field) ' '), val][r0 -- mkfs(class0, ty0, ((* str0)) .field) ']) = st[r0 -- mkfs(class0, ty0, str0 .field) '] | A User Theorem |
| at-put-keys-01 | ⊦ sk ≠ sk0 → (st[r -- (sks + sk '), val][r0 -- sk0]) = st[r0 -- sk0] | A User Theorem |
| at-put-keys-02 | ⊦ sk0 ≠ sks .last ∧ sks ≠ [] → (st[r -- sks, val][r0 -- sk0]) = st[r0 -- sk0] | A User Theorem |
| at-put-keys-03 | str ≠ `java.lang.Object' ⊦ (st[r -- (sks + mkfs(((* str)) .class, ty, fieldvar) ' '), val][r0 -- _type]) = st[r0 -- _type] | A User Theorem |
| at-put-keys-04 | str ≠ str0 ⊦ (st[r -- (sk ' + mkfs(class, ty, ((* str)) .field) ' '), val][r0 -- mkfs(class0, ty0, ((* str0)) .field) ']) = st[r0 -- mkfs(class0, ty0, str0 .field) '] | A User Theorem |
| at-put-keys-05 | str ≠ `*Array*' ⊦ (st[r -- (sks + mkfs(((* str)) .class, ty, fieldvar) ' '), val][r0 -- _length]) = st[r0 -- _length] | A User Theorem |
| at-put-last-other | ⊦ (r0 ≠ st[r -- sks] .refval ∨ sk ≠ sk0) ∧ sks ≠ [] → (st[r -- (sks + sk '), val][r0 -- sk0]) = st[r0 -- sk0] | A User Theorem |
| at-put-last-other-01 | ⊦ (r0 ≠ st[r -- sks .butlast] .refval ∨ sk ≠ sks .last) ∧ 1 < # sks → (st[r -- sks, val][r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| at-put-other | ⊦ rk ≠ jvmref -- sk ∧ sks ≠ [] → (st[rk, val][sk ' + sks]) = (st[rk, val][st[jvmref -- sk] .refval -- sks]) | A User Theorem |
| at-put-other-01 | ⊦ ¬ sk ∈ sks ∧ sks ≠ [] → (st[r -- sk, val][sks]) = st[sks] | A User Theorem |
| at-put-other-02 | ⊦ ¬ sk ∈ sks ∧ sks ≠ [] → (st[r -- sk, val][r0 -- sks]) = st[r0 -- sks] | A User Theorem |
| at-put-other-03 | ⊦ (st[r -- i ', val][r0 -- (mkfs(class, ty, fieldvar) ' ' + mkfs(class0, ty0, fieldvar0) ' ')]) = st[r0 -- (mkfs(class, ty, fieldvar) ' ' + mkfs(class0, ty0, fieldvar0) ' ')] | A User Theorem |
| at-put-same | ⊦ sks ≠ [] ∧ ¬ dups(sks) → (st[r -- sks, val][r -- sks]) = val | A User Theorem |
| at-put-same-01 | ⊦ (st[r -- (sks + sk0 ' + sk '), val][st[r -- (sks + sk0 ')] .refval -- sk]) = val | A User Theorem |
| at-put-same-02 | ⊦ sks ≠ [] → (st[r -- (sks + sk '), val][st[r -- sks] .refval -- sk]) = val | A User Theorem |
| at-put-same-04 | ⊦ (st[r -- (sk ' + sk0 '), val][st[r -- sk] .refval -- sk0]) = val | A User Theorem |
| del-notin | ⊦ ¬ r ∈ st -- r | A User Theorem |
| del-notin-01 | ⊦ ¬ r ∈ st → st -- r = st | A User Theorem |
| del-put | ⊦ st[r -- sk, val] -- r = st -- r | A User Theorem |
| del-put-switch | ⊦ r ≠ r0 → st[r -- sk, val] -- r0 = (st -- r0)[r -- sk, val] | A User Theorem |
| del-refs-size | ⊦ # st ≤ # (st -- r) ↔ ¬ r ∈ st | A User Theorem |
| del-subset | ⊦ st -- r ⊆ st | A User Theorem |
| del-subset-del | ⊦ st -- r ⊆ st -- (r -- sk) | A User Theorem |
| del-switch | ⊦ st -- r -- r0 = st -- r0 -- r | A User Theorem |
| delete-at | ⊦ r ≠ rk .ref → (st -- r)[rk] = st[rk] | A User Theorem |
| exists-fournew | ⊦ ∃ r, r0, r1, r2. r ≠ r0 ∧ r ≠ r1 ∧ r ≠ r2 ∧ r0 ≠ r1 ∧ r0 ≠ r2 ∧ r1 ≠ r2 ∧ newref(r, st) ∧ newref(r0, st) ∧ newref(r1, st) ∧ newref(r2, st) | A User Theorem |
| exists-twonew | ⊦ ∃ r, r0. r ≠ r0 ∧ newref(r, st) ∧ newref(r0, st) | A User Theorem |
| extension-neqrefs | ⊦ ¬ (∀ sk. (r -- sk ∈ st ↔ r0 -- sk ∈ st) ∧ st[r -- sk] = st[r0 -- sk]) → r ≠ r0 | A User Theorem |
| in-butmin | ⊦ r ∈ st ∧ r ≠ st .min .ref → r ∈ st .butmin | A User Theorem |
| in-butmin-01 | ⊦ ¬ r ∈ st → ¬ r ∈ st .butmin | A User Theorem |
| in-del | ⊦ r -- sk ∈ st -- r0 ↔ r ≠ r0 ∧ r -- sk ∈ st | A User Theorem |
| in-del-01 | ⊦ r -- sk ∈ st -- r0 ↔ ¬ ¬ (r ≠ r0 ∧ r -- sk ∈ st) | A User Theorem |
| in-empty | ⊦ ¬ r ∈ ∅ | A User Theorem |
| in-list-put | ⊦ ¬ rk .key ∈ sks ∧ sks ≠ [] → (r -- sks ∈ st[rk, val] ↔ r -- sks ∈ st) | A User Theorem |
| in-list-subset | ⊦ st ⊆ st0 ∧ r -- sks ∈ st ∧ sks ≠ [] → r -- sks ∈ st0 | A User Theorem |
| in-min | ⊦ ¬ r ∈ st ∧ st ≠ ∅ → st .min ≠ r -- sk | A User Theorem |
| in-mode-put | str ≠ `java.lang.Object' ⊦ _mode ∈ st[r -- (sks + mkfs(((* str)) .class, ty, fieldvar) ' '), val] ↔ _mode ∈ st | A User Theorem |
| in-put | ⊦ 1 < # sks → (rk ∈ st[r -- sks, val] ↔ rk ∈ st ∨ rk = st[r -- sks .butlast] .refval -- sks .last) | A User Theorem |
| in-put-keys | ⊦ sk ≠ sk0 → (r0 -- sk0 ∈ st[r -- (sks + sk '), val] ↔ r0 -- sk0 ∈ st) | A User Theorem |
| in-put-keys-01 | str ≠ `java.lang.Object' ⊦ r0 -- _type ∈ st[r -- (sks + mkfs(((* str)) .class, ty, fieldvar) ' '), val] ↔ r0 -- _type ∈ st | A User Theorem |
| in-put-keys-02 | str ≠ str0 ⊦ r0 -- mkfs(class, ty, ((* str)) .field) ' ∈ st[r -- (sks + mkfs(class0, ty0, ((* str0)) .field) ' '), val] ↔ r0 -- mkfs(class, ty, str .field) ' ∈ st | A User Theorem |
| in-put-rkvs | ⊦ rk ∈ st[rkvs] ↔ rk ∈ st ∨ rk ∈ rkvs | A User Theorem |
| in-put-rkvs-01 | ⊦ rk ∈ st[(rk0 × val) ' + rkvs] ↔ rk = rk0 ∨ rk ∈ st[rkvs] | A User Theorem |
| in-put-rkvs-mode | ⊦ r ≠ jvmref → (_mode ∈ st[((r -- sk) × val) ' + rkvs] ↔ _mode ∈ st[rkvs]) | A User Theorem |
| in-put-same | ⊦ st[r -- sk] .refval -- sk0 ∈ st[r -- (sk ' + sk0 '), val] | A User Theorem |
| indel | ⊦ r ∈ st ∧ r ≠ r0 → r ∈ st -- (r0 -- sk) | A User Theorem |
| init | ⊦ initundone(class1, st) → ¬ initerror(class1, st) | A User Theorem |
| init-01 | ⊦ initundone(class1, st) → ¬ initdone(class1, st) | A User Theorem |
| init-02 | ⊦ initdone(class1, st) → ¬ initerror(class1, st) | A User Theorem |
| init-03 | ⊦ initdone(class1, st) → ¬ initundone(class1, st) | A User Theorem |
| init-05 | ⊦ rk ≠ _uninit ∧ rk ≠ jvmref -- mkfs(class, void_type, `initstate' .field) ' → (initundone(class, st[rk, val]) ↔ initundone(class, st)) | A User Theorem |
| init-06 | ⊦ rk ≠ jvmref -- mkfs(class, void_type, `initstate' .field) ' → (initerror(class, st[rk, val]) ↔ initerror(class, st)) | A User Theorem |
| init-def | ⊦ init(st) ↔ ¬ _uninit ∈ st ∧ (∀ rk. rk ∈ st ∧ rk .ref = jvmref ∧ is_fskey(rk .key) ∧ rk .key .fs .type = void_type ∧ rk .key .fs .field = `initstate' .field → st[rk] ≠ initval(undone) ∧ st[rk] ≠ initval(error)) | A User Theorem |
| init-done | ⊦ initdone(class, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(done)]) | A User Theorem |
| init-done-01 | ⊦ initdone(class, st) → initdone(class, st[jvmref -- mkfs(class0, void_type, `initstate' .field) ', initval(done)]) | A User Theorem |
| init-endfmode | ⊦ initdone(class1, st[_endfinallymode, val]) ↔ initdone(class1, st) | A User Theorem |
| init-endfmode-01 | ⊦ initundone(class1, st[_endfinallymode, val]) ↔ initundone(class1, st) | A User Theorem |
| init-endfmode-02 | ⊦ initerror(class1, st[_endfinallymode, val]) ↔ initerror(class1, st) | A User Theorem |
| init-error | ⊦ initerror(class, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(error)]) | A User Theorem |
| init-mode-03 | ⊦ initdone(class1, st[_mode, val]) ↔ initdone(class1, st) | A User Theorem |
| init-mode-04 | ⊦ initundone(class1, st[_mode, val]) ↔ initundone(class1, st) | A User Theorem |
| init-mode-05 | ⊦ initerror(class1, st[_mode, val]) ↔ initerror(class1, st) | A User Theorem |
| init-out | ⊦ initdone(class1, st[_out, val]) ↔ initdone(class1, st) | A User Theorem |
| init-out-01 | ⊦ initundone(class1, st[_out, val]) ↔ initundone(class1, st) | A User Theorem |
| init-out-02 | ⊦ initerror(class1, st[_out, val]) ↔ initerror(class1, st) | A User Theorem |
| init-put | ⊦ r ≠ jvmref → (initdone(class1, st[r -- sk, val]) ↔ initdone(class1, st)) | A User Theorem |
| init-put-01 | ⊦ r ≠ jvmref → (initundone(class1, st[r -- sk, val]) ↔ initundone(class1, st)) | A User Theorem |
| init-put-02 | ⊦ r ≠ jvmref → (initerror(class1, st[r -- sk, val]) ↔ initerror(class1, st)) | A User Theorem |
| init-put-03 | ⊦ jvmref -- fs ' ≠ _uninit ∧ fs ≠ mkfs(class1, void_type, `initstate' .field) → (initdone(class1, st[jvmref -- fs ', val]) ↔ initdone(class1, st)) | A User Theorem |
| init-put-04 | ⊦ rk ≠ jvmref -- mkfs(class, void_type, `initstate' .field) ' ∧ rk ≠ _uninit → (initdone(class, st[rk, val]) ↔ initdone(class, st)) | A User Theorem |
| init-put-05 | class1 ≠ class2 ⊦ initerror(class1, st[jvmref -- mkfs(class2, ty, fieldvar) ', val]) ↔ initerror(class1, st) | A User Theorem |
| init-put-06 | ⊦ init(st[r -- i ', val]) ↔ init(st) | A User Theorem |
| init-put-07 | ⊦ initundone(class1, st[r -- mkfs(class0, int_type, fieldvar) ', val]) ↔ initundone(class1, st) | A User Theorem |
| init-put-08 | sk ≠ mkfs(class1, void_type, `initstate' .field) ' ⊦ initerror(class1, st[jvmref -- sk, val]) ↔ initerror(class1, st) | A User Theorem |
| init-put-09 | ⊦ initundone(class1, st[r -- mkfs(class0, byte_type, fieldvar) ', val]) ↔ initundone(class1, st) | A User Theorem |
| init-put-10 | ⊦ initerror(class1, st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', val]) ↔ val = initval(error) | A User Theorem |
| init-put-11 | ⊦ initundone(class1, st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', val]) ↔ val = initval(undone) | A User Theorem |
| init-put-12 | ⊦ initdone(class1, st[jvmref -- mkfs(class1, void_type, `initstate' .field) ', val]) ↔ val ≠ initval(error) ∧ val ≠ initval(undone) | A User Theorem |
| init-put-13 | ⊦ initundone(class1, st[r -- mkfs(class0, short_type, fieldvar) ', val]) ↔ initundone(class1, st) | A User Theorem |
| init-put-14 | ⊦ initundone(class1, st[r -- mkfs(class0, boolean_type, fieldvar) ', val]) ↔ initundone(class1, st) | A User Theorem |
| init-put-15 | ⊦ initundone(class1, st[r -- mkfs(class0, mkclasstype(class2), fieldvar) ', val]) ↔ initundone(class1, st) | A User Theorem |
| init-put-16 | ⊦ initundone(class1, st[r -- mkfs(class0, mkarraytype(ty), fieldvar) ', val]) ↔ initundone(class1, st) | A User Theorem |
| init-put-17 | ⊦ initdone(class1, st[r -- mkfs(class0, int_type, fieldvar) ', val]) ↔ initdone(class1, st) | A User Theorem |
| init-put-18 | ⊦ initdone(class1, st[r -- mkfs(class0, byte_type, fieldvar) ', val]) ↔ initdone(class1, st) | A User Theorem |
| init-put-19 | ⊦ initdone(class1, st[r -- mkfs(class0, short_type, fieldvar) ', val]) ↔ initdone(class1, st) | A User Theorem |
| init-put-20 | ⊦ initdone(class1, st[r -- mkfs(class0, boolean_type, fieldvar) ', val]) ↔ initdone(class1, st) | A User Theorem |
| init-put-21 | ⊦ initdone(class1, st[r -- mkfs(class0, mkclasstype(class2), fieldvar) ', val]) ↔ initdone(class1, st) | A User Theorem |
| init-put-22 | ⊦ initdone(class1, st[r -- mkfs(class0, mkarraytype(ty), fieldvar) ', val]) ↔ initdone(class1, st) | A User Theorem |
| init-put-23 | ⊦ r ≠ jvmref → (init(st[r -- sk, val]) ↔ init(st)) | A User Theorem |
| init-put-24 | ⊦ ty ≠ void_type → (initdone(class1, st[jvmref -- mkfs(class, ty, fieldvar) ', val]) ↔ initdone(class1, st)) | A User Theorem |
| init-put-field | ⊦ is_fskey(sk) ∧ sk .fs .type ≠ void_type → (init(st[r -- sk, val]) ↔ init(st)) | A User Theorem |
| init-put-field-01 | ⊦ ty ≠ void_type → (init(st[r -- (sks + mkfs(class, ty, fieldvar) ' '), val]) ↔ init(st)) | A User Theorem |
| init-put-field-02 | ⊦ init(st[r -- (sks + mkfs(class, int_type, fieldvar) ' '), val]) ↔ init(st) | A User Theorem |
| init-put-field-03 | ⊦ init(st[r -- (sks + mkfs(class, byte_type, fieldvar) ' '), val]) ↔ init(st) | A User Theorem |
| init-put-field-04 | ⊦ init(st[r -- (sks + mkfs(class, short_type, fieldvar) ' '), val]) ↔ init(st) | A User Theorem |
| init-put-field-05 | ⊦ init(st[r -- (sks + mkfs(class, boolean_type, fieldvar) ' '), val]) ↔ init(st) | A User Theorem |
| init-put-field-06 | ⊦ init(st[r -- (sks + mkfs(class, mkclasstype(class0), fieldvar) ' '), val]) ↔ init(st) | A User Theorem |
| init-put-field-07 | ⊦ init(st[r -- (sks + mkfs(class, mkarraytype(ty), fieldvar) ' '), val]) ↔ init(st) | A User Theorem |
| init-put-index | ⊦ init(str, st[r -- i ', val]) ↔ init(str, st) | A User Theorem |
| init-put-nonvoid | ⊦ fs .type ≠ void_type → (init(str, st[r -- fs ', val]) ↔ init(str, st)) | A User Theorem |
| init-put-notnull | ⊦ r ≠ jvmref → (init(str, st[r -- sk, val]) ↔ init(str, st)) | A User Theorem |
| init-put-rkvs | ⊦ r ≠ jvmref → (init(str, st[((r -- sk) × val) ' + rkvs]) ↔ init(str, st[rkvs])) | A User Theorem |
| init-put-rkvs-01 | ⊦ (∀ class. ¬ jvmref -- mkfs(class, void_type, `initstate' .field) ' ∈ rkvs) ∧ ¬ _uninit ∈ rkvs → (init(str, st[rkvs]) ↔ init(str, st)) | A User Theorem |
| init-put-short | ⊦ rk ∈ st ∧ is_shortvalue(st[rk]) → (initdone(class, st[rk, shortval(sho)]) ↔ initdone(class, st)) | A User Theorem |
| init-total | ⊦ ¬ initdone(class, st) → (¬ initundone(class, st) ↔ initerror(class, st)) | A User Theorem |
| init-uninit | ⊦ init(st) → (uninit(st) ↔ false) | A User Theorem |
| init-uninit-01 | ⊦ uninit(st) → (init(st) ↔ false) | A User Theorem |
| initP-put | ⊦ initdoneP(class, st[jvmref -- mkfs(class, void_type, `initstate' .field) ', initval(done)]) | A User Theorem |
| initdone-01 | ⊦ initdone(class1, st) ↔ ¬ ¬ (¬ initerror(class1, st) ∧ ¬ initundone(class1, st)) | A User Theorem |
| initdone-02 | ⊦ initdone(class1, st[r -- i ', val]) ↔ initdone(class1, st) | A User Theorem |
| initdone-03 | ⊦ initdone(class1, st[r -- _length, val]) ↔ initdone(class1, st) | A User Theorem |
| initdone-04 | ⊦ initdone(class1, st[r -- _type, val]) ↔ initdone(class1, st) | A User Theorem |
| initdone-05 | ⊦ init(st) → (¬ initdone(class1, st) ↔ false) | A User Theorem |
| initdone-06 | ⊦ initdone(class0, st[r -- mkfs(class, short_type, fieldvar) ', val]) ↔ initdone(class0, st) | A User Theorem |
| initdone-at-type | ⊦ initdone(class1, st[r -- (sks + mkfs(class, int_type, fieldvar) ' '), val]) ↔ initdone(class1, st) | A User Theorem |
| initdone-at-type-01 | ⊦ initdone(class1, st[r -- (sks + mkfs(class, byte_type, fieldvar) ' '), val]) ↔ initdone(class1, st) | A User Theorem |
| initdone-at-type-02 | ⊦ initdone(class1, st[r -- (sks + mkfs(class, short_type, fieldvar) ' '), val]) ↔ initdone(class1, st) | A User Theorem |
| initdone-at-type-03 | ⊦ initdone(class1, st[r -- (sks + mkfs(class, boolean_type, fieldvar) ' '), val]) ↔ initdone(class1, st) | A User Theorem |
| initdone-at-type-04 | ⊦ initdone(class1, st[r -- (sks + mkfs(class, mkclasstype(class0), fieldvar) ' '), val]) ↔ initdone(class1, st) | A User Theorem |
| initdone-at-type-05 | ⊦ initdone(class1, st[r -- (sks + mkfs(class, mkarraytype(ty), fieldvar) ' '), val]) ↔ initdone(class1, st) | A User Theorem |
| initdone-put-rkvs | ⊦ ¬ jvmref -- mkfs(class, void_type, `initstate' .field) ' ∈ rkvs ∧ ¬ _uninit ∈ rkvs → (initdone(class, st[rkvs]) ↔ initdone(class, st)) | A User Theorem |
| initdone-uninit | ⊦ initdone(class, st[_uninit, val]) ↔ jvmref -- mkfs(class, void_type, `initstate' .field) ' ∈ st ∧ st[jvmref -- mkfs(class, void_type, `initstate' .field) '] ≠ initval(undone) ∧ st[jvmref -- mkfs(class, void_type, `initstate' .field) '] ≠ initval(error) | A User Theorem |
| initerror-01 | ⊦ initerror(class1, st) ↔ ¬ ¬ (jvmref -- mkfs(class1, void_type, `initstate' .field) ' ∈ st ∧ st[jvmref -- mkfs(class1, void_type, `initstate' .field) '] = initval(error)) | A User Theorem |
| initerror-02 | ⊦ initerror(class1, st[r -- i ', val]) ↔ initerror(class1, st) | A User Theorem |
| initerror-03 | ⊦ initerror(class1, st[r -- _length, val]) ↔ initerror(class1, st) | A User Theorem |
| initerror-04 | ⊦ initerror(class1, st[r -- _type, val]) ↔ initerror(class1, st) | A User Theorem |
| initerror-05 | ⊦ init(st) → ¬ initerror(class1, st) | A User Theorem |
| initundone-01 | ⊦ initundone(class1, st) ↔ ¬ ¬ ( (jvmref -- mkfs(class1, void_type, `initstate' .field) ') × initval(undone) ∈ st ∨ ¬ jvmref -- mkfs(class1, void_type, `initstate' .field) ' ∈ st ∧ _uninit ∈ st) | A User Theorem |
| initundone-02 | ⊦ initundone(class1, st[r -- i ', val]) ↔ initundone(class1, st) | A User Theorem |
| initundone-03 | ⊦ initundone(class1, st[r -- _length, val]) ↔ initundone(class1, st) | A User Theorem |
| initundone-04 | ⊦ initundone(class1, st[r -- _type, val]) ↔ initundone(class1, st) | A User Theorem |
| initundone-05 | ⊦ init(st) → ¬ initundone(class1, st) | A User Theorem |
| instore-01 | ⊦ r -- sk ∈ st → r ∈ st | A User Theorem |
| instore-02 | ⊦ r ∈ st[r0 -- sk, val] ↔ r = r0 ∨ r ∈ st | A User Theorem |
| instore-rec-01 | ⊦ sks ≠ [] → (r -- (sk ' + sks) ∈ st ↔ r -- sk ∈ st ∧ st[r -- sk] .refval -- sks ∈ st) | A User Theorem |
| instore-two | ⊦ r -- (sk ' + sk0 ') ∈ st ↔ r -- sk ∈ st ∧ st[r -- sk] .refval -- sk0 ' ∈ st | A User Theorem |
| look-del | ⊦ r ≠ r0 → (st -- r)[r0 -- sk0] = st[r0 -- sk0] | A User Theorem |
| lookup-append | ⊦ sks ≠ [] ∧ sks0 ≠ [] → st[r -- (sks + sks0)] = st[st[r -- sks] .refval -- sks0] | A User Theorem |
| lookup-five | ⊦ st[r -- (sk ' + sk0 ' + sk1 ' + sk2 ' + sk3 ')] = st[st[st[st[st[r -- sk] .refval -- sk0] .refval -- sk1] .refval -- sk2] .refval -- sk3] | A User Theorem |
| lookup-four | ⊦ st[r -- (sk ' + sk0 ' + sk1 ' + sk2 ')] = st[st[st[st[r -- sk] .refval -- sk0] .refval -- sk1] .refval -- sk2] | A User Theorem |
| lookup-last-rec | ⊦ sks ≠ [] → st[r -- (sks + sk ')] = st[st[r -- sks] .refval -- sk] | A User Theorem |
| lookup-list-butlast | ⊦ sks ≠ [] → st[r0 -- sks] = st[st[r0 -- sks .butlast] .refval -- sks .last] | A User Theorem |
| lookup-list-intro | ⊦ st[st[r -- sk] .refval -- sk0] = st[r -- (sk ' + sk0 ')] | A User Theorem |
| lookup-list-intro-01 | ⊦ sks ≠ [] → st[st[r -- sks] .refval -- sk0] = st[r -- (sks + sk0 ')] | A User Theorem |
| lookup-list-intro-02 | ⊦ sks ≠ [] ∧ sks0 ≠ [] → st[st[r -- sks] .refval -- sks0] = st[r -- (sks + sks0)] | A User Theorem |
| lookup-list-intro-03 | ⊦ st[st[r -- (sk ' + sks)] .refval -- sk0] = st[r -- (sk ' + sks + sk0 ')] | A User Theorem |
| lookup-list-intro-04 | ⊦ st[st[r -- (sk ' + sks)] .refval -- (sk0 ' + sks0)] = st[r -- (sk ' + sks + sk0 ' + sks0)] | A User Theorem |
| lookup-list-intro-05 | ⊦ sks ≠ [] → st[st[r -- sk] .refval -- sks] = st[r -- (sk ' + sks)] | A User Theorem |
| lookup-list-intro-06 | ⊦ st[st[r -- sk] .refval -- (sk0 ' + sks)] = st[r -- (sk ' + sk0 ' + sks)] | A User Theorem |
| lookup-list-list-append | ⊦ sks0 ≠ [] → st[st[r -- sks] .refval -- sks0] = st[r -- (sks + sks0)] | A User Theorem |
| lookup-list-put-ex | (st[r0 -- sk, val][r -- sks]) ≠ st[r -- sks] ⊦ ∃ sks0, sks1. sks = sks0 + (sk + sks1) ∧ st[r -- sks0] .refval = r0 | A User Theorem |
| lookup-put-ex-first | (st[r0 -- sk, val][r -- sks]) ≠ st[r -- sks] ⊦ ∃ sks0, sks1. sks = sks0 + (sk + sks1) ∧ st[r -- sks0] .refval = r0 ∧ (∀ sks2. sks2 + sk ⊑ sks0 → st[r -- sks2] .refval ≠ r0) | A User Theorem |
| lookup-put-keys | ⊦ sk ≠ sk0 ∧ sks0 ≠ [] → (st[r -- (sks + sk '), val][r0 -- (sk0 ' + sks0)]) = (st[r -- (sks + sk '), val][st[r0 -- sk0] .refval -- sks0]) | A User Theorem |
| lookup-put-keys-01 | str ≠ str0 ⊦ (st[r -- (sks + mkfs(class, ty, ((* str)) .field) ' '), val][r0 -- (mkfs(class0, ty0, ((* str0)) .field) ' ' + sk1 ')]) = (st[r -- (sks + mkfs(class, ty, str .field) ' '), val][st[r0 -- mkfs(class0, ty0, str0 .field) '] .refval -- sk1]) | A User Theorem |
| lookup-put-keys-02 | str ≠ str0 ⊦ (st[r -- (sks + mkfs(class, ty, ((* str)) .field) ' '), val][r0 -- (mkfs(class0, ty0, ((* str0)) .field) ' ' + sk1 ' + sks0)]) = (st[r -- (sks + mkfs(class, ty, str .field) ' '), val][st[r0 -- mkfs(class0, ty0, str0 .field) '] .refval -- (sk1 ' + sks0)]) | A User Theorem |
| lookup-put-other | ⊦ ¬ (∃ sks0, sks1. sks = sks0 + (sk + sks1) ∧ st[r -- sks0] .refval = r0 ∧ (∀ sks2. sks2 + sk ⊑ sks0 → st[r -- sks2] .refval ≠ r0)) → (st[r0 -- sk, val][r -- sks]) = st[r -- sks] | A User Theorem |
| lookup-put-rkvs | ⊦ rk ≠ rk0 → (st[(rk × val) ' + rkvs][rk0]) = (st[rkvs][rk0]) | A User Theorem |
| lookup-put-rkvs-01 | ⊦ rk ≠ rk0 → (st[rk, val][rkvs][rk0]) = (st[rkvs][rk0]) | A User Theorem |
| lookup-put-rkvs-diff | ⊦ r ≠ r0 → (st[((r -- sk) × val) ' + rkvs][r0 -- sk0]) = (st[rkvs][r0 -- sk0]) | A User Theorem |
| lookup-put-rkvs-diff-01 | ⊦ (st[((r -- i ') × val) ' + rkvs][r0 -- mkfs(class, ty, fieldvar) ']) = (st[rkvs][r0 -- mkfs(class, ty, fieldvar) ']) | A User Theorem |
| lookup-put-rkvs-diff-02 | ⊦ (st[((r -- mkfs(class, ty, fieldvar) ') × val) ' + rkvs][r0 -- i ']) = (st[rkvs][r0 -- i ']) | A User Theorem |
| lookup-put-rkvs-diff-03 | str ≠ str0 ⊦ (st[((r -- mkfs(class, ty, ((* str)) .field) ') × val) ' + rkvs][r0 -- mkfs(class0, ty0, ((* str0)) .field) ']) = (st[rkvs][r0 -- mkfs(class0, ty0, str0 .field) ']) | A User Theorem |
| lookup-put-rkvs-mode | ⊦ r ≠ jvmref → (st[((r -- sk) × val) ' + rkvs][_mode]) = (st[rkvs][_mode]) | A User Theorem |
| lookup-put-rkvs-notin | ⊦ ¬ rk ∈ rkvs → (st[rkvs][rk]) = st[rk] | A User Theorem |
| lookup-rec-01 | ⊦ sks ≠ [] → st[r -- (sk ' + sks)] = st[st[r -- sk] .refval -- sks] | A User Theorem |
| lookup-rec-refval | ⊦ is_referencevalue(st[r -- sks]) ∧ sks ≠ [] → st[r -- sks] = st[st[r -- sks .first] .refval -- sks .rest] | A User Theorem |
| lookup-seven | ⊦ st[r -- (sk ' + sk0 ' + sk1 ' + sk2 ' + sk3 ' + sk4 ' + sk5 ')] = st[st[st[st[st[st[st[r -- sk] .refval -- sk0] .refval -- sk1] .refval -- sk2] .refval -- sk3] .refval -- sk4] .refval -- sk5] | A User Theorem |
| lookup-six | ⊦ st[r -- (sk ' + sk0 ' + sk1 ' + sk2 ' + sk3 ' + sk4 ')] = st[st[st[st[st[st[r -- sk] .refval -- sk0] .refval -- sk1] .refval -- sk2] .refval -- sk3] .refval -- sk4] | A User Theorem |
| lookup-sk-list-append | ⊦ sks0 ≠ [] → st[st[r -- sk] .refval -- sks0] = st[r -- (sk ' + sks0)] | A User Theorem |
| lookup-subset | ⊦ st ⊆ st0 ∧ r -- sks ∈ st ∧ sks ≠ [] → st0[r -- sks] = st[r -- sks] | A User Theorem |
| lookup-subset-01 | ⊦ st ⊆ st0 ∧ r -- sks ∈ st → st0[r -- sks] = st[r -- sks] | A User Theorem |
| lookup-superset | ⊦ st ⊆ st0 ∧ r -- sks ∈ st → st[r -- sks] = st0[r -- sks] | A User Theorem |
| lookup-three | ⊦ st[r -- (sk ' + sk0 ' + sk1 ')] = st[st[st[r -- sk] .refval -- sk0] .refval -- sk1] | A User Theorem |
| lookup-two | ⊦ st[r -- (sk ' + sk0 ')] = st[st[r -- sk] .refval -- sk0] | A User Theorem |
| maxref-exists | ⊦ ∃ r. ∀ r0. r0 ∈ st → r0 < r | A User Theorem |
| maxref-exists-01 | ⊦ ∃ r. jvmref < r ∧ (∀ r0. r0 ∈ st → r0 < r) | A User Theorem |
| mode-01 | ⊦ r ≠ jvmref → (r ∈ st[_mode, val] ↔ r ∈ st) | A User Theorem |
| mode-at-type | ⊦ (st[r -- (sks + mkfs(class, int_type, fieldvar) ' '), val][_mode]) = st[_mode] | A User Theorem |
| mode-at-type-01 | ⊦ (st[r -- (sks + mkfs(class, byte_type, fieldvar) ' '), val][_mode]) = st[_mode] | A User Theorem |
| mode-at-type-02 | ⊦ (st[r -- (sks + mkfs(class, short_type, fieldvar) ' '), val][_mode]) = st[_mode] | A User Theorem |
| mode-at-type-03 | ⊦ (st[r -- (sks + mkfs(class, boolean_type, fieldvar) ' '), val][_mode]) = st[_mode] | A User Theorem |
| mode-at-type-04 | ⊦ (st[r -- (sks + mkfs(class, mkclasstype(class0), fieldvar) ' '), val][_mode]) = st[_mode] | A User Theorem |
| mode-at-type-05 | ⊦ (st[r -- (sks + mkfs(class, mkarraytype(ty), fieldvar) ' '), val][_mode]) = st[_mode] | A User Theorem |
| mode-del | r ≠ jvmref ⊦ (st -- r)[_mode] = st[_mode] | A User Theorem |
| mode-notin | ⊦ ¬ jvmref ∈ st → ¬ _mode ∈ st | A User Theorem |
| mode-put-sks-array | ⊦ (st[jvmref -- (sks + i ' '), val][_mode]) = st[_mode] | A User Theorem |
| mode-put-sks-array-01 | ⊦ (st[sks + i ' ', val][_mode]) = st[_mode] | A User Theorem |
| neqref-type | ⊦ st[r -- _type] ≠ st[r0 -- _type] → r ≠ r0 | A User Theorem |
| new-insert | ⊦ newref(r, st[rk, val]) → newref(r, st) | A User Theorem |
| new-insert-01 | ⊦ newref(r0, st[r -- sk, val]) → r ≠ r0 | A User Theorem |
| new-mode | ⊦ newref(r, st) → _mode ≠ r -- sk | A User Theorem |
| new-mode-01 | ⊦ newref(r, st[_mode, val]) ↔ newref(r, st) | A User Theorem |
| new-out | ⊦ newref(r, st[_out, val]) ↔ newref(r, st) | A User Theorem |
| newjvmref | ⊦ ¬ newref(jvmref, st) | A User Theorem |
| newref-01 | ⊦ newref(r, st) → r ≠ jvmref | A User Theorem |
| newref-02 | ⊦ newref(r, st[r0 -- sk, val]) ↔ r ≠ r0 ∧ newref(r, st) | A User Theorem |
| newref-03 | ⊦ r ∈ st → ¬ newref(r, st) | A User Theorem |
| newref-def | ⊦ newref(r, st) ↔ r ≠ jvmref ∧ ¬ r ∈ st | A User Theorem |
| newref-del | ⊦ newref(r0, st) → newref(r0, st -- r) | A User Theorem |
| newref-del-01 | ⊦ newref(r, st -- r) ↔ r ≠ jvmref | A User Theorem |
| newref-empty | ⊦ newref(r, ∅) ↔ r ≠ jvmref | A User Theorem |
| newref-exists | ⊦ ∃ r. newref(r, st) | A User Theorem |
| newref-in | ⊦ ¬ newref(st) ∈ st | A User Theorem |
| newref-in-01 | ⊦ newref(r, st) ∧ r0 ∈ st → r ≠ r0 | A User Theorem |
| newref-in-02 | ⊦ r -- sk ∈ st → ¬ newref(r, st) | A User Theorem |
| newref-in-03 | ⊦ newref(r, st) ∧ r0 ∈ st ∧ r0 ≠ jvmref → r ≠ r0 | A User Theorem |
| newref-jvmref | ⊦ newref(st) ≠ jvmref | A User Theorem |
| newref-new | ⊦ r ∈ st → newref(st) ≠ r | A User Theorem |
| newref-newref | ⊦ newref(newref(st[newref(st) -- 0 ', noval]), st) | A User Theorem |
| newref-newref-notin | ⊦ ¬ newref(st[newref(st) -- 0 ', noval]) ∈ st | A User Theorem |
| newref-newref-subset | ⊦ ¬ newref(newref(st), st0) → ¬ st0 ⊆ st | A User Theorem |
| newref-newreflist-subset | ⊦ r ∈ newref_list(n, st) ∧ st0 ⊆ st → newref(r, st0) | A User Theorem |
| newref-notin | ⊦ ¬ newref(st) -- sk ∈ st | A User Theorem |
| newref-notin-01 | ⊦ ¬ newref(st[rk, val][rk0, val0]) ∈ st | A User Theorem |
| newref-put | ⊦ newref(r, st[rk, val]) ↔ newref(r, st) ∧ r ≠ rk .ref | A User Theorem |
| newref-put-01 | ⊦ newref(st[r -- sk, val]) ≠ r | A User Theorem |
| newref-put-in | ⊦ rk ∈ st → newref(st[rk, val]) = newref(st) | A User Theorem |
| newref-put-in-01 | ⊦ newref(newref(st[r -- sk, val]), st) | A User Theorem |
| newref-same | ⊦ (∀ r. r ∈ st ↔ r ∈ st0) → newref(st) = newref(st0) | A User Theorem |
| newref-subset | ⊦ (∀ r. r ∈ st → r ∈ st0) → ¬ newref(st0) ∈ st | A User Theorem |
| newref-subset-01 | ⊦ newref(r, st1) ∧ st ⊆ st1 → newref(r, st) | A User Theorem |
| newref-subset-02 | ⊦ ¬ newref(r, st) ∧ st ⊆ st1 → ¬ newref(r, st1) | A User Theorem |
| newreflist-dups | ⊦ dups(refs) → newref_list(n, st) ≠ refs | A User Theorem |
| newreflist-dups-01 | ⊦ ¬ dups(newref_list(n, st)) | A User Theorem |
| newreflist-null | ⊦ jvmref ∈ refs → newref_list(n, st) ≠ refs | A User Theorem |
| newreflist-null-01 | ⊦ jvmref ∈ refs → newref_list(n, st) ≠ r ' + refs | A User Theorem |
| newrefs | ⊦ ¬ is_newref_list(r ' + jvmref ', st) | A User Theorem |
| newrefs-01 | ⊦ is_newref_list(r ' + r0 ', st) ↔ r ≠ r0 ∧ newref(r, st) ∧ newref(r0, st) | A User Theorem |
| newrefs-base | ⊦ is_newref_list([], st) | A User Theorem |
| newrefs-butlast | ⊦ ¬ newref_list(n + 1, st) .last ∈ newref_list(n + 1, st) .butlast | A User Theorem |
| newrefs-butlast-01 | ⊦ newref_list(n + 1, st) .butlast = newref_list(n, st) | A User Theorem |
| newrefs-empty | ⊦ newref_list(n, st) = [] ↔ n = 0 | A User Theorem |
| newrefs-first | ⊦ newref(newref_list(n + 1, st) .first, st) | A User Theorem |
| newrefs-firstn | ⊦ is_newref_list(refs, st) ∧ n ≤ # refs → is_newref_list(firstn(n, refs), st) | A User Theorem |
| newrefs-in | ⊦ r ∈ st → ¬ r ∈ newref_list(n, st) | A User Theorem |
| newrefs-jvmref | 0 < n ⊦ is_newref_list(refs, st) ∧ # refs = ((* n)) → refs[0] ≠ jvmref | A User Theorem |
| newrefs-last | ⊦ newref(newref_list(n + 1, st) .last, st) | A User Theorem |
| newrefs-last-01 | ⊦ ¬ newref_list(n + 1, st) .last ∈ newref_list(n, st) | A User Theorem |
| newrefs-lastn | ⊦ is_newref_list(refs, st) ∧ n ≤ # refs → is_newref_list(lastn(n, refs), st) | A User Theorem |
| newrefs-length | ⊦ # newref_list(n, st) = n | A User Theorem |
| newrefs-new | ⊦ r ∈ newref_list(n, st) → newref(r, st) | A User Theorem |
| newrefs-new-01 | ⊦ is_newref_list(newref_list(n, st), st) | A User Theorem |
| newrefs-null | ⊦ ¬ jvmref ∈ newref_list(n, st) | A User Theorem |
| newrefs-one | ⊦ is_newref_list(r ', st) ↔ newref(r, st) | A User Theorem |
| newrefs-one-01 | ⊦ newref_list(1, st) = newref(st) ' | A User Theorem |
| newrefs-rec | ⊦ is_newref_list(r ' + refs, st) ↔ ¬ ¬ (¬ r ∈ refs ∧ newref(r, st) ∧ is_newref_list(refs, st)) | A User Theorem |
| newrefs-rec-01 | ⊦ 0 < n → newref_list(n, st) = newref(st) + newref_list(n -1, st[newref(st) -- 0 ', noval]) | A User Theorem |
| newrefs-rest | ⊦ ¬ newref_list(n + 1, st) .first ∈ newref_list(n + 1, st) .rest | A User Theorem |
| newrefs-three | ⊦ ¬ (∃ r, r0, r1. refs = r + (r0 + r1) ∧ newref(r1, st) ∧ newref(r, st) ∧ newref(r0, st) ∧ r ≠ r0 ∧ r ≠ r1 ∧ r0 ≠ r1) → newref_list(3, st) ≠ refs | A User Theorem |
| newrefs-two | ⊦ ¬ (∃ r, r0. refs = r + r0 ∧ newref(r, st) ∧ newref(r0, st) ∧ r ≠ r0) → newref_list(2, st) ≠ refs | A User Theorem |
| newrefsnew | ⊦ newref(newref(st), st) | A User Theorem |
| normal | ⊦ normalmode(st) → st[_mode] = noval | A User Theorem |
| normal-lookup | ⊦ st0 = st[_out, val] ∧ normalmode(st) → normalmode(st0) | A User Theorem |
| normal-lookup-01 | ⊦ st0 = st[r -- sk, val] ∧ r ≠ jvmref ∧ normalmode(st) → normalmode(st0) | A User Theorem |
| normal-lookup-02 | ⊦ st0 = st[r -- sk, val] ∧ newref(r, st) ∧ normalmode(st) → normalmode(st0) | A User Theorem |
| normal-out | ⊦ normalmode(st[_out, val]) ↔ normalmode(st) | A User Theorem |
| normal-return | ⊦ normalmode(st) → ¬ is_return_mode(st[_mode]) | A User Theorem |
| normal-throw | ⊦ normalmode(st) → ¬ is_throw_mode(st[_mode]) | A User Theorem |
| put-last-rec | ⊦ sks ≠ [] → st[r -- (sks + sk '), val] = st[st[r -- sks] .refval -- sk, val] | A User Theorem |
| put-last-rec-better | ⊦ st[r -- (sks + sk '), val] = st[st[r -- sks] .refval -- sk, val] | A User Theorem |
| put-list-intro | ⊦ st[st[r -- sk] .refval -- sk0, val] = st[r -- (sk ' + sk0 '), val] | A User Theorem |
| put-list-intro-01 | ⊦ st[st[r -- sks] .refval -- sk0, val] = st[r -- (sks + sk0 '), val] | A User Theorem |
| put-put-first-01 | ⊦ sks ≠ [] → (st[r -- sk, val][r -- (sk ' + sks), val0]) = (st[r -- sk, val][val .refval -- sks, val0]) | A User Theorem |
| put-put-switch | ⊦ ¬ sk ∈ sks0 ∧ sks0 ≠ [] → (st[r -- sk, val][r0 -- sks0, val0]) = (st[r0 -- sks0, val0][r -- sk, val]) | A User Theorem |
| put-rec-01 | ⊦ sks ≠ [] → st[r -- (sk ' + sks), val] = st[st[r -- sk] .refval -- sks, val] | A User Theorem |
| put-rkvs-absorb | ⊦ rk ∈ rkvs → (st[rk, val][rkvs]) = st[rkvs] | A User Theorem |
| put-rkvs-absorb-01 | ⊦ rk ∈ rkvs → st[(rk × val) ' + rkvs] = st[rkvs] | A User Theorem |
| put-rkvs-append | ⊦ st[rkvs + rkvs0] = (st[rkvs][rkvs0]) | A User Theorem |
| put-rkvs-last | ⊦ rkvs ≠ [] → st[rkvs] = (st[rkvs .butlast][rkvs .last .1, rkvs .last .2]) | A User Theorem |
| put-rkvs-list | ⊦ (st[rk, val][rk0, val0]) = st[(rk × val) ' + (rk0 × val0) '] | A User Theorem |
| put-rkvs-list-01 | ⊦ (st[rk, val][rkvs]) = st[(rk × val) ' + rkvs] | A User Theorem |
| put-rkvs-list-02 | ⊦ (st[rkvs][rk0, val0]) = st[rkvs + (rk0 × val0) '] | A User Theorem |
| put-rkvs-one | ⊦ st[(rk × val) '] = st[rk, val] | A User Theorem |
| put-rkvs-one-01 | ⊦ st[rkv '] = st[rkv .1, rkv .2] | A User Theorem |
| put-rkvs-rec | ⊦ st[rkv ' + rkvs] = (st[rkv .1, rkv .2][rkvs]) | A User Theorem |
| put-rkvs-switch | ⊦ ¬ rk ∈ rkvs → (st[rk, val][rkvs]) = (st[rkvs][rk, val]) | A User Theorem |
| put-rkvs-switch-01 | ⊦ ¬ rk ∈ rkvs → st[(rk × val) ' + rkvs] = (st[rkvs][rk, val]) | A User Theorem |
| put-rkvs-switch-02 | ⊦ ¬ rk ∈ rkvs → (st[rkvs][rk, val]) = (st[rk, val][rkvs]) | A User Theorem |
| put-sks-fs-array | ⊦ (st[jvmref -- (sks + i ' '), val][jvmref -- fs ']) = st[jvmref -- fs '] | A User Theorem |
| put-sks-fs-array-01 | ⊦ (st[sks + i ' ', val][jvmref -- fs ']) = st[jvmref -- fs '] | A User Theorem |
| put-two | ⊦ st[r -- (sk ' + sk0 '), val] = st[st[r -- sk] .refval -- sk0, val] | A User Theorem |
| ref-in | ⊦ r ∈ st[rk, val] ↔ r = rk .ref ∨ r ∈ st | A User Theorem |
| refin | ⊦ r ∈ st[r -- sk, val] | A User Theorem |
| refin-del | ⊦ r ≠ r1 → (r ∈ st -- r1 ↔ r ∈ st) | A User Theorem |
| stsubset-new | ⊦ newref(r, st) → (st ⊆ st0[r -- sk, val] ↔ st ⊆ st0) | A User Theorem |
| subset-delete | ⊦ ¬ r ∈ st → (st ⊆ st0 -- r ↔ st ⊆ st0) | A User Theorem |
| subset-instore | ⊦ r ∈ st ∧ st ⊆ st0 → r ∈ st0 | A User Theorem |
| subset-newref | ⊦ ¬ newref(r, st) ∧ newref(r, st0) → ¬ st ⊆ st0 | A User Theorem |
| subset-notin | ⊦ r ∈ st ∧ ¬ r ∈ st0 → ¬ st ⊆ st0 | A User Theorem |
| subset-put-notin | ⊦ ¬ r ∈ st → (st ⊆ st0[r -- sk, val] ↔ st ⊆ st0) | A User Theorem |
| uninit-01 | ⊦ uninit(st) → ¬ initdone(class, st) | A User Theorem |
| uninit-02 | ⊦ uninit(st) → ¬ initerror(class, st) | A User Theorem |
| uninit-03 | ⊦ uninit(st) → initundone(class, st) | A User Theorem |
| uninit-def | ⊦ uninit(st) ↔ _uninit ∈ st ∧ (∀ rk. rk ∈ st ∧ rk .ref = jvmref ∧ is_fskey(rk .key) ∧ rk .key .fs .type = void_type ∧ rk .key .fs .field = `initstate' .field → st[rk] = initval(undone)) | A User Theorem |