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: |
|---|---|---|
| okstore | ⊦ okstore(st) ↔ is_javastore(st) ∧ (∀ r. r ≠ jvmref ∧ r ∈ st → r -- _type ∈ st ∧ is_typevalue(st[r -- _type])) | An Axiom |
| okclass | ⊦ okclass(val, class1, st) ↔ reftypep(val, st) ∧ (val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ st[val .refval -- _type] = typeval(mkclasstype(class1))) | An Axiom |
| oktype-void | ⊦ oktype(val, void_type, st) ↔ is_referencevalue(val) | An Axiom |
| oktype-array | ⊦ oktype(val, mkarraytype(ty), st) ↔ is_referencevalue(val) | An Axiom |
| oktype-class | ⊦ oktype(val, mkclasstype(class1), st) ↔ is_referencevalue(val) | An Axiom |
| oktype-byte | ⊦ oktype(val, byte_type, st) ↔ is_bytevalue(val) | An Axiom |
| oktype-short | ⊦ oktype(val, short_type, st) ↔ is_shortvalue(val) | An Axiom |
| oktype-int | ⊦ oktype(val, int_type, st) ↔ is_integervalue(val) | An Axiom |
| oktype-bool | ⊦ oktype(val, boolean_type, st) ↔ is_boolvalue(val) | An Axiom |
| good-field | ⊦ goodfieldandtype(r, mkfs(class1, ty, fieldvar) ', st) ↔ r -- mkfs(class1, ty, fieldvar) ' ∈ st ∧ oktype(st[r -- mkfs(class1, ty, fieldvar) '], ty, st) | An Axiom |
| good-rec | ⊦ goodfieldsandtypes(r, sk ' + sks, st) ↔ goodfieldandtype(r, sk, st) ∧ goodfieldsandtypes(r, sks, st) | An Axiom |
| good-base | ⊦ goodfieldsandtypes(r, [], st) | An Axiom |
| okreftype | ⊦ okreftype(val, ty, st) ↔ is_referencevalue(val) ∧ (val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ st[val .refval -- _type] .type ≤ ty) | An Axiom |
| okarrays-rec | ⊦ okarrays(r, (sk × val) ' + fis, st) ↔ is_integervalue(val) ∧ is_fskey(sk) ∧ is_arraytype(sk .fs .type) ∧ okarray(st[r -- sk], sk .fs .type .type, val .intval, st) ∧ okarrays(r, fis, st) | An Axiom |
| okarrays-base | ⊦ okarrays(r, [], st) | An Axiom |
| instore-rec | ⊦ (sk × val) ' + fis ∈ st ↔ (jvmref -- sk) × val ∈ st ∧ fis ∈ st | An Axiom |
| instore-base | ⊦ [] ∈ st | An Axiom |
| good-index | ⊦ ¬ goodfieldandtype(r, i ', st) | An Axiom |
| okarrayNotNull | ⊦ okarray(r, ty, st) ↔ okreftype(refval(r), mkarraytype(ty), st) ∧ r ≠ jvmref ∧ r -- _length ∈ st ∧ is_integervalue(st[r -- _length]) ∧ 0 ≤ st[r -- _length] .intval ∧ is_arrayref(r, st[r -- _length] .intval, st) ∧ (∀ j. 0 ≤ j ∧ j < st[r -- _length] .intval → oktype(st[r -- j '], ty, st)) | An Axiom |
| okarraytype | ⊦ okarraytype(val, ty, st) ↔ is_referencevalue(val) ∧ (val .refval ≠ jvmref → okarray(val .refval, ty, st)) | An Axiom |
| oktype-abstract | ⊦ ¬ oktype(val, abstract_type, st) | An Axiom |
| eqval-throwr | ⊦ is_throw_mode(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-throwl | ⊦ is_throw_mode(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-returnr | ⊦ is_return_mode(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-returnl | ⊦ is_return_mode(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-continuer | ⊦ is_continue_mode(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-continuel | ⊦ is_continue_mode(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-breakr | ⊦ is_break_mode(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-breakl | ⊦ is_break_mode(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-initr | ⊦ is_initvalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-initl | ⊦ is_initvalue(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-typer | ⊦ is_typevalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-typel | ⊦ is_typevalue(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-novalr | ⊦ is_novalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-novall | ⊦ is_novalue(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-concr | ⊦ is_valuelist(val0) → (eqval(val, val0, st, st0) ↔ is_valuelist(val) ∧ eqval(val .firstval, val0 .firstval, st, st0) ∧ eqval(val .restval, val0 .restval, st, st0)) | An Axiom |
| eqval-concl | ⊦ is_valuelist(val) → (eqval(val, val0, st, st0) ↔ is_valuelist(val0) ∧ eqval(val .firstval, val0 .firstval, st, st0) ∧ eqval(val .restval, val0 .restval, st, st0)) | An Axiom |
| eqval-refr | ⊦ is_referencevalue(val0) → (eqval(val, val0, st, st0) ↔ is_referencevalue(val) ∧ eqref(val .refval, val0 .refval, st, st0)) | An Axiom |
| eqval-refl | ⊦ is_referencevalue(val) → (eqval(val, val0, st, st0) ↔ is_referencevalue(val0) ∧ eqref(val .refval, val0 .refval, st, st0)) | An Axiom |
| eqval-boolr | ⊦ is_boolvalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-booll | ⊦ is_boolvalue(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-shortr | ⊦ is_shortvalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-shortl | ⊦ is_shortvalue(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-byter | ⊦ is_bytevalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-bytel | ⊦ is_bytevalue(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-intr | ⊦ is_integervalue(val0) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqval-intl | ⊦ is_integervalue(val) → (eqval(val, val0, st, st0) ↔ val = val0) | An Axiom |
| eqref | ⊦ eqref(r, r0, st, st0) ↔ r = jvmref ∧ r0 = jvmref ∨ r ≠ jvmref ∧ r0 ≠ jvmref ∧ (∀ sk. (r -- sk ∈ st ↔ r0 -- sk ∈ st0) ∧ (r -- sk ∈ st → eqval(st[r -- sk], st0[r0 -- sk], st, st0))) | An Axiom |
| is_javastore | ⊦ is_javastore(st) ↔ _mode ∈ st ∧ _out ∈ st | An Axiom |
| okbytearray-01 | ⊦ okbytearray(r, st) ↔ okarray(r, byte_type, st) | An Axiom |
| exacttype-abstract | ⊦ exacttype(val, abstract_type, st) | An Axiom |
| exacttype-void | ⊦ exacttype(val, void_type, st) | An Axiom |
| exacttype-array | ⊦ exacttype(val, mkarraytype(ty), st) ↔ exactreftype(val, mkarraytype(ty), st) | An Axiom |
| exacttype-class | ⊦ exacttype(val, mkclasstype(class1), st) ↔ okclass(val, class1, st) | An Axiom |
| exacttype-byte | ⊦ exacttype(val, byte_type, st) ↔ is_bytevalue(val) | An Axiom |
| exacttype-short | ⊦ exacttype(val, short_type, st) ↔ is_shortvalue(val) | An Axiom |
| exacttype-int | ⊦ exacttype(val, int_type, st) ↔ is_integervalue(val) | An Axiom |
| exacttype-bool | ⊦ exacttype(val, boolean_type, st) ↔ is_boolvalue(val) | An Axiom |
| exact-index | ⊦ ¬ exactfieldandtype(r, i ', st) | An Axiom |
| exact-field | ⊦ exactfieldandtype(r, mkfs(class1, ty, fieldvar) ', st) ↔ r -- mkfs(class1, ty, fieldvar) ' ∈ st ∧ exacttype(st[r -- mkfs(class1, ty, fieldvar) '], ty, st) | An Axiom |
| exact-rec | ⊦ exactfieldsandtypes(r, sk ' + sks, st) ↔ exactfieldandtype(r, sk, st) ∧ exactfieldsandtypes(r, sks, st) | An Axiom |
| exact-base | ⊦ exactfieldsandtypes(r, [], st) | An Axiom |
| exactreftype | ⊦ exactreftype(val, ty, st) ↔ is_referencevalue(val) ∧ val .refval ∈ st ∧ (val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ st[val .refval -- _type] .type = ty) | An Axiom |
| exactarray-01 | ⊦ exactarray(val, ty, i, st) ↔ exactreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ is_arrayref(val .refval, i, st) | An Axiom |
| exactarray-02 | ⊦ exactarray(r, ty, st) ↔ exactreftype(refval(r), mkarraytype(ty), st) ∧ r ≠ jvmref ∧ r -- _length ∈ st ∧ is_integervalue(st[r -- _length]) ∧ 0 ≤ st[r -- _length] .intval ∧ is_arrayref(r, st[r -- _length] .intval, st) | An Axiom |
| instore-rec-02 | ⊦ instore(r, class, (sk × val) ' + fis, st) ↔ (r -- sk) × val ∈ st ∧ instore(r, class, fis, st) | An Axiom |
| instore-empty | ⊦ instore(r, class, [], st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ st[r -- _type] = typeval(mkclasstype(class)) | An Axiom |
| oktype-double | ⊦ oktype(val, double_type, st) ↔ is_doublevalue(val) | An Axiom |
| oktype-float | ⊦ oktype(val, float_type, st) ↔ is_floatvalue(val) | An Axiom |
| oktype-char | ⊦ oktype(val, char_type, st) ↔ is_charvalue(val) | An Axiom |
| oktype-long | ⊦ oktype(val, long_type, st) ↔ is_longvalue(val) | An Axiom |
| okarrayOfLength | ⊦ okarray(val, ty, i, st) ↔ okreftype(val, mkarraytype(ty), st) ∧ val .refval ≠ jvmref ∧ (val .refval -- _length) × intval(i) ∈ st ∧ 0 ≤ i ∧ is_arrayref(val .refval, i, st) ∧ (∀ j. 0 ≤ j ∧ j < i → oktype(st[val .refval -- j '], ty, st)) | An Axiom |
| getvals-rec | ⊦ ((sk × val) ' + fis) .vals = val ' + fis .vals | An Axiom |
| getvals-empty | ⊦ [] .vals = [] | An Axiom |
| getkeys-rec | ⊦ ((sk × val) ' + fis) .keys = sk ' + fis .keys | An Axiom |
| getkeys-empty | ⊦ [] .keys = [] | An Axiom |
| update-rec | ⊦ update(r, (sk × val) ' + fis, st) = (update(r, fis, st)[r -- sk, val]) | An Axiom |
| update-empty | ⊦ update(r, [], st) = st | An Axiom |
| oksubtype | ⊦ oksubtype(val, class, st) ↔ reftypep(val, st) ∧ (val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ st[val .refval -- _type] .type .class ≤ class) | An Axiom |
| hasKeys-rec | ⊦ hasKeys(r, sk ' + sks, st) ↔ r -- sk ∈ st ∧ hasKeys(r, sks, st) | An Axiom |
| hasKeys-empty | ⊦ hasKeys(r, [], st) | An Axiom |
| validFields | ⊦ validFields(r, fis, st) ↔ unique_al(fis) ∧ ¬ _type ∈ fis ∧ ¬ _length ∈ fis ∧ hasKeys(r, fis .keys, st) | An Axiom |
| asgcomp | ⊦ asgcomp(str, val, ty, st) ↔ ¬ is_referencevalue(val) ∨ val .refval = jvmref ∨ is_subtype(str, st[val .refval -- _type] .type, ty) | An Axiom |
| is-any-array | ⊦ is_array(r, st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) ∧ is_arraytype(st[r -- _type] .type) ∧ okarray(r, st[r -- _type] .type .type, st) | An Axiom |
| validFieldValue-def | ⊦ validFieldValue(r, sk, st) ↔ is_fskey(sk) ∧ r -- sk ∈ st ∧ okval(st[r -- sk], sk .fs .type) | An Axiom |
| validFieldValues-def | ⊦ validFieldValues(r, sks, st) ↔ (∀ sk. sk ∈ sks → validFieldValue(r, sk, st)) | An Axiom |
| is-real-array-def | ⊦ is_array(str, r, st) ↔ type∃(str, st[r -- _type] .type) ∧ st[r -- _type] .type .jtelemtype ≠ void_type ∧ st[r -- _type] .type .jtelemtype ≠ abstract_type ∧ is_array(r, st) | An Axiom |
| byteval | ⊦ 0 ≤ i + i0 ∧ i0 ≤ j ∧ i + j < st[r -- _length] .intval ∧ okarray(r, byte_type, st) → byteval(st[r -- (i + i0) '] .byteval) = st[r -- (i + i0) '] | A User Theorem |
| byteval-01 | ⊦ 0 ≤ i + i0 ∧ i + i0 < st[r -- _length] .intval ∧ okarray(r, byte_type, st) → byteval(st[r -- (i + i0) '] .byteval) = st[r -- (i + i0) '] | A User Theorem |
| byteval-02 | ⊦ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ okbytearray(r, st) → byteval(st[r -- i '] .byteval) = st[r -- i '] | A User Theorem |
| bytevalues-eq | ⊦ okarray(r, byte_type, st) ∧ i + j ≤ st[r -- _length] .intval ∧ 0 ≤ i ∧ okarray(r0, byte_type, st) ∧ i0 + j0 ≤ st[r0 -- _length] .intval ∧ 0 ≤ i0 → (bytevalues(getarray(r, i, j, st)) = bytevalues(getarray(r0, i0, j0, st)) ↔ getarray(r, i, j, st) = getarray(r0, i0, j0, st)) | A User Theorem |
| comp-same | ⊦ arraycomp(r1, i1, r2, i2, i3, st0) ∧ i2 + i3 ≤ st0[r2 -- _length] .intval ∧ 0 ≤ i2 ∧ i < i3 ∧ 0 ≤ i ∧ okarray(r2, int_type, st0) → st0[r2 -- (i2 + i) ', intval(st0[r1 -- (i1 + i) '] .intval)] = st0 | A User Theorem |
| copy-comp | ⊦ arraycomp(r1, i1, r2, i2, i3, st0) ∧ i2 + i3 ≤ st0[r2 -- _length] .intval ∧ 0 ≤ i3 ∧ 0 ≤ i2 ∧ okarray(r2, ty, st0) → arraycopy(r1, i1, r2, i2, i3, st0) = st0 | A User Theorem |
| copy-same | ⊦ i2 + i3 ≤ st0[r2 -- _length] .intval ∧ 0 ≤ i2 ∧ i < i3 ∧ 0 ≤ i ∧ r1 ≠ r2 ∧ okarray(r2, int_type, st0) → arraycopy(r1, i1, r2, i2, i3, st0[r2 -- (i2 + i) ', intval(st0[r1 -- (i1 + i) '] .intval)]) = arraycopy(r1, i1, r2, i2, i3, st0) | A User Theorem |
| copy-same-01 | ⊦ i2 + i3 ≤ st0[r2 -- _length] .intval ∧ 0 ≤ i2 ∧ i < i3 ∧ 0 ≤ i ∧ r1 ≠ r2 ∧ okarray(r2, int_type, st0) → arraycopy(r1, i1, r2, i2, i3, st0[r2 -- (i2 + i) ', val]) = arraycopy(r1, i1, r2, i2, i3, st0) | A User Theorem |
| copy-same-01-01 | ⊦ i2 + i3 ≤ st0[r2 -- _length] .intval ∧ 0 ≤ i2 ∧ i < i3 ∧ 0 ≤ i ∧ r1 ≠ r2 ∧ exactarray(r2, int_type, st0) → arraycopy(r1, i1, r2, i2, i3, st0[r2 -- (i2 + i) ', val]) = arraycopy(r1, i1, r2, i2, i3, st0) | A User Theorem |
| copy-same-02 | ⊦ i2 + i3 ≤ st0[r2 -- _length] .intval ∧ 0 ≤ i2 ∧ i < i3 ∧ 0 ≤ i ∧ r1 ≠ r2 ∧ exactarray(r2, int_type, st0) → arraycopy(r1, i1, r2, i2, i3, st0[r2 -- (i2 + i) ', intval(st0[r1 -- (i1 + i) '] .intval)]) = arraycopy(r1, i1, r2, i2, i3, st0) | A User Theorem |
| dups-fis-keys | ⊦ dups(fis[sk, val] .keys) ↔ dups(fis .keys) | A User Theorem |
| exactarray-01-01 | ⊦ exactarray(refval(r), ty, i, st) → st[r -- _length] .intval = i | A User Theorem |
| exactarray-02-01 | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) ∧ r ≠ r0 → (exactarray(refval(r), ty, i, st[r0 -- sk, val0]) ↔ exactarray(refval(r), ty, i, st)) | A User Theorem |
| exactarray-04 | ⊦ ¬ exactarray(jvmref, ty, st) | A User Theorem |
| exactarray-05 | ⊦ exactarray(r, ty, st) → r ≠ jvmref ∧ r ∈ st | A User Theorem |
| exactarray-06 | ⊦ r ≠ r0 → (exactarray(r, int_type, st[r0 -- sk, val]) ↔ exactarray(r, int_type, st)) | A User Theorem |
| exactarray-07 | ⊦ exactarray(r, int_type, st) → exactarray(r, int_type, st[r0 -- j ', intval(i)]) | A User Theorem |
| exactarray-08 | ⊦ ¬ exactarray(r, int_type, st[r0 -- j ', val]) ∧ exactarray(r, int_type, st) → ¬ is_integervalue(val) | A User Theorem |
| exactarray-byteput | ⊦ 0 ≤ j ∧ j < i ∧ exactarray(refval(r), byte_type, i, st) → exactarray(refval(r), byte_type, i, st[r -- j ', byteval(by)]) | A User Theorem |
| exactarray-copy | r1 ≠ r0 ⊦ exactarray(r1, ty, arraycopy(r, i, r0, i0, j, st)) ↔ exactarray(r1, ty, st) | A User Theorem |
| exactarray-copy-01 | ⊦ exactarray(r, byte_type, st) ∧ exactarray(r0, byte_type, st) ∧ 0 ≤ i ∧ 0 ≤ j ∧ i + j ≤ st[r0 -- _length] .intval → exactarray(r, byte_type, arraycopy(r0, i, r, i0, j, st)) | A User Theorem |
| exactarray-in | ⊦ ¬ r -- i ' ∈ st ∧ 0 ≤ i ∧ i < j → ¬ exactarray(refval(r), ty, j, st) | A User Theorem |
| exactarray-intval-01 | ⊦ exactarray(r, ty, st) → intval(st[r -- _length] .intval) = st[r -- _length] | A User Theorem |
| exactarray-jvmref | ⊦ ¬ exactarray(refval(jvmref), ty, i, st) | A User Theorem |
| exactarray-jvmref-01 | ⊦ exactarray(refval(r), ty, i, st) → r ≠ jvmref | A User Theorem |
| exactarray-len | ⊦ exactarray(r, ty, st) → ¬ st[r -- _length] .intval < 0 | A User Theorem |
| exactarray-length | ⊦ exactarray(r, ty, st) → ¬ val2int(st[r -- _length]) < 0 | A User Theorem |
| exactarray-length-01 | ⊦ exactarray(refval(r), ty, i, st) → val2int(st[r -- _length]) = i | A User Theorem |
| exactarray-length-02 | ⊦ exactarray(refval(r), ty, i, st) → ¬ val2int(st[r -- _length]) < i | A User Theorem |
| exactarray-lenin | ⊦ st[r -- _length] .intval = 141 * j0 ∧ 0 ≤ i ∧ i < j0 ∧ exactarray(r, ty, st) → r -- (i * 141) ' ∈ st | A User Theorem |
| exactarray-new | ⊦ newref(r, st) → ¬ exactarray(refval(r), ty, i, st[rk, val]) | A User Theorem |
| exactarray-new-01 | ⊦ exactarray(refval(r), ty, i, st) → ¬ newref(r, st) | A User Theorem |
| exactarray-null | ⊦ val .refval = jvmref → ¬ exactarray(val, ty, i, st) | A User Theorem |
| exactarray-out | ⊦ exactarray(val, ty, i, st[_out, val0]) ↔ exactarray(val, ty, i, st) | A User Theorem |
| exactarray-primput | ⊦ okprimtype(val, ty) ∧ 0 ≤ j ∧ j < i ∧ exactarray(refval(r), ty, i, st) → exactarray(refval(r), ty, i, st[r -- j ', val]) | A User Theorem |
| exactarray-put | ⊦ exactarray(r, byte_type, st) → exactarray(r, byte_type, st[r0 -- i ', byteval(by)]) | A User Theorem |
| exactarray-put-01 | ⊦ sk ≠ _type ∧ goodfieldandtype(r0, sk, st) ∧ oktype(val0, sk .fs .type, st) ∧ sk ≠ _length → (exactarray(val, ty, i, st[r0 -- sk, val0]) ↔ exactarray(val, ty, i, st)) | A User Theorem |
| exactarray-put-02 | ⊦ exactarray(val, byte_type, i, st) → exactarray(val, byte_type, i, st[r0 -- j ', byteval(by)]) | A User Theorem |
| exactarray-put-03 | ⊦ r ≠ r0 → (exactarray(refval(r), byte_type, i, st[r0 -- sk, val0]) ↔ exactarray(refval(r), byte_type, i, st)) | A User Theorem |
| exactarray-put-04 | ⊦ exactarray(r, int_type, st) → exactarray(r, int_type, st[r0 -- i ', intval(j)]) | A User Theorem |
| exactarray-put-05 | ⊦ r ≠ r0 → (exactarray(r, byte_type, st[r0 -- sk, val]) ↔ exactarray(r, byte_type, st)) | A User Theorem |
| exactarray-put-06 | ⊦ is_bytevalue(val) ∧ exactarray(r, byte_type, st) → exactarray(r, byte_type, st[r -- i ', val]) | A User Theorem |
| exactarray-put-07 | ⊦ rk .ref ≠ val .refval → (exactarray(val, ty, i, st[rk, val0]) ↔ exactarray(val, ty, i, st)) | A User Theorem |
| exactarray-putar | ⊦ r ≠ r1 → (exactarray(refval(r1), byte_type, j, putArray(vals, r, i, st)) ↔ exactarray(refval(r1), byte_type, j, st)) | A User Theorem |
| exactarray-putbar | ⊦ r ≠ r1 → (exactarray(refval(r1), byte_type, j, putByteArray(bytes, r, i, st)) ↔ exactarray(refval(r1), byte_type, j, st)) | A User Theorem |
| exactarray-putin | ⊦ exactarray(refval(r), mkclasstype(class), j, st) → exactarray(refval(r), mkclasstype(class), j, st[r -- i ', refval(r0)]) | A User Theorem |
| exactarray-type | ⊦ exactarray(refval(r), ty, i, st) → is_typevalue(st[r -- _type]) | A User Theorem |
| exactarray-type-01 | ⊦ exactarray(refval(r), ty, i, st) → st[r -- _type] = typeval(mkarraytype(ty)) | A User Theorem |
| exactarray-type-02 | ⊦ exactarray(refval(r), ty, i, st) → (¬ st[r -- _type] .type .type ≤ ty ↔ false) | A User Theorem |
| exactarray-type-03 | ⊦ exactarray(refval(r), ty, i, st) → (¬ ty ≤ st[r -- _type] .type .type ↔ false) | A User Theorem |
| exactref-in | ⊦ exactreftype(refval(r), ty, st) → r ∈ st | A User Theorem |
| exactref-put | ⊦ rk .ref ≠ r ∧ exactreftype(refval(r), ty, st) → exactreftype(refval(r), ty, st[rk, val]) | A User Theorem |
| exactref-put-01 | ⊦ rk .ref ≠ r ∧ ¬ exactreftype(refval(r), ty, st[rk, val]) → ¬ exactreftype(refval(r), ty, st) | A User Theorem |
| gengft | ⊦ sk ≠ _type ∧ goodfieldandtype(r, sk, st) ∧ oktype(val, sk .fs .type, st) → (goodfieldandtype(r0, sk0, st[r -- sk, val]) ↔ goodfieldandtype(r0, sk0, st)) | A User Theorem |
| gengfts | ⊦ sk ≠ _type ∧ goodfieldandtype(r, sk, st) ∧ oktype(val, sk .fs .type, st) → (goodfieldsandtypes(r0, sks, st[r -- sk, val]) ↔ goodfieldsandtypes(r0, sks, st)) | A User Theorem |
| getarray-bytes | ⊦ okbytearray(r, st) → bytevalues(getarray(r, st)) = getbytearray(r, st) | A User Theorem |
| getarray-subset | ⊦ st ⊆ st0 ∧ is_array(r, st) → getarray(r, st) = getarray(r, st0) | A User Theorem |
| getarray-subset-01 | ⊦ st ⊆ st0 ∧ is_array(str, r, st) → getarray(r, st) = getarray(r, st0) | A User Theorem |
| getarray-subset-02 | ⊦ st ⊆ st0 ∧ is_array(r, st) ∧ i + j ≤ st[r -- _length] .intval ∧ 0 ≤ i → getarray(r, i, j, st) = getarray(r, i, j, st0) | A User Theorem |
| getarray-superset | ⊦ st ⊆ st0 ∧ is_array(str, r, st) → getarray(r, st0) = getarray(r, st) | A User Theorem |
| getarray-superset-01 | ⊦ st ⊆ st0 ∧ is_array(r, st) → getarray(r, st0) = getarray(r, st) | A User Theorem |
| getbar-subset | ⊦ st ⊆ st0 ∧ okbytearray(r, st) → getbytearray(r, st) = getbytearray(r, st0) | A User Theorem |
| getbar-superset | ⊦ st ⊆ st0 ∧ okbytearray(r, st) → getbytearray(r, st0) = getbytearray(r, st) | A User Theorem |
| getbar-update | ⊦ r ≠ r0 → getbytearray(r, update(r0, fis, st)) = getbytearray(r, st) | A User Theorem |
| getbar-update-01 | ⊦ r ≠ r0 → getbytearray(r, i, j, update(r0, fis, st)) = getbytearray(r, i, j, st) | A User Theorem |
| getbytearray-mkjavavalues | ⊦ okbytearray(r, st) → mkjavavalues(getbytearray(r, st)) = getarray(r, st) | A User Theorem |
| getintarray-subset | ⊦ st ⊆ st0 ∧ is_array(r, st) → getintarray(r, st) = getintarray(r, st0) | A User Theorem |
| getintarray-subset-01 | ⊦ st ⊆ st0 ∧ is_array(str, r, st) → getintarray(r, st) = getintarray(r, st0) | A User Theorem |
| getkeys-app | ⊦ (fis + fis0) .keys = fis .keys + fis0 .keys | A User Theorem |
| getkeys-one | ⊦ fv ' .keys = fv .1 ' | A User Theorem |
| getvals-rec-01 | ⊦ (fv ' + fis) .vals = fv .2 ' + fis .vals | A User Theorem |
| gft | sk0 ≠ _type ⊦ r ≠ r0 → (goodfieldandtype(r, sk, st[r0 -- sk0, val]) ↔ goodfieldandtype(r, sk, st)) | A User Theorem |
| gft-mode-01 | mkfs(`java.lang.Object' .class, void_type, `mode' .field) ' ≠ sk0 ⊦ goodfieldandtype(r0, sk0, st[_mode, val]) ↔ goodfieldandtype(r0, sk0, st) | A User Theorem |
| gft-not | sk0 ≠ _type ∧ is_fskey(sk0) ∧ oktype(val, sk0 .fs .type, st) ⊦ ¬ goodfieldandtype(r, sk, st[r0 -- sk0, val]) → ¬ goodfieldandtype(r, sk, st) | A User Theorem |
| gft-not-01 | ⊦ ¬ goodfieldandtype(r, sk, st[r0 -- mkfs(class0, ty, fieldvar) ', val]) ∧ mkfs(class0, ty, fieldvar) ' ≠ _type ∧ oktype(val, ty, st) → ¬ goodfieldandtype(r, sk, st) | A User Theorem |
| gft-null | ⊦ sk ≠ _type ∧ sk ≠ sk0 → (goodfieldandtype(r0, sk0, st[jvmref -- sk, val]) ↔ goodfieldandtype(r0, sk0, st)) | A User Theorem |
| gft-out | ⊦ r ≠ jvmref → (goodfieldandtype(r, sk, st[_out, val]) ↔ goodfieldandtype(r, sk, st)) | A User Theorem |
| gft-out-01 | mkfs(`java.lang.Object' .class, void_type, `out' .field) ' ≠ sk0 ⊦ goodfieldandtype(r0, sk0, st[_out, val]) ↔ goodfieldandtype(r0, sk0, st) | A User Theorem |
| gft-put | ⊦ r ≠ r0 → (goodfieldandtype(r, sk, st[r0 -- sk0, val]) ↔ goodfieldandtype(r, sk, st)) | A User Theorem |
| gft-union | ⊦ ¬ r ∈ st .refs → (goodfieldandtype(r, sk, st ∪ st0) ↔ goodfieldandtype(r, sk, st0)) | A User Theorem |
| gfts | sk0 ≠ _type ⊦ r ≠ r0 → (goodfieldsandtypes(r, sks, st[r0 -- sk0, val]) ↔ goodfieldsandtypes(r, sks, st)) | A User Theorem |
| gfts-all | ⊦ goodfieldsandtypes(r, sks, st) ↔ (∀ sk. sk ∈ sks → goodfieldandtype(r, sk, st)) | A User Theorem |
| gfts-in | ⊦ goodfieldsandtypes(r, sks, st) ∧ sk ∈ sks → goodfieldandtype(r, sk, st) | A User Theorem |
| gfts-not | sk ≠ _type ∧ is_fskey(sk) ∧ oktype(val, sk .fs .type, st) ⊦ ¬ goodfieldsandtypes(r, sks, st[r0 -- sk, val]) → ¬ goodfieldsandtypes(r, sks, st) | A User Theorem |
| gfts-not-01 | ⊦ ¬ goodfieldsandtypes(r, sks, st[r0 -- mkfs(class0, ty, fieldvar) ', val]) ∧ mkfs(class0, ty, fieldvar) ' ≠ _type ∧ oktype(val, ty, st) → ¬ goodfieldsandtypes(r, sks, st) | A User Theorem |
| gfts-null | ⊦ sk ≠ _type ∧ ¬ sk ∈ sks → (goodfieldsandtypes(r0, sks, st[jvmref -- sk, val]) ↔ goodfieldsandtypes(r0, sks, st)) | A User Theorem |
| gfts-put | ⊦ r ≠ r0 → (goodfieldsandtypes(r, sks, st[r0 -- sk0, val]) ↔ goodfieldsandtypes(r, sks, st)) | A User Theorem |
| good-field-01 | ⊦ goodfieldandtype(r, mkfs(class1, ty, fieldvar) ', st) ↔ ¬ ¬ (r -- mkfs(class1, ty, fieldvar) ' ∈ st ∧ okval(st[r -- mkfs(class1, ty, fieldvar) '], ty)) | A User Theorem |
| good-field-02 | ⊦ is_fskey(sk) → (goodfieldandtype(r, sk, st) ↔ r -- sk ∈ st ∧ oktype(st[r -- sk], sk .fs .type, st)) | A User Theorem |
| good-field-def | ⊦ goodfieldandtype(r, sk, st) ↔ is_fskey(sk) ∧ r -- sk ∈ st ∧ okval(st[r -- sk], sk .fs .type) | A User Theorem |
| good-field-del | ⊦ r ≠ r0 → (goodfieldandtype(r, sk, st -- r0) ↔ goodfieldandtype(r, sk, st)) | A User Theorem |
| good-field-field | ⊦ is_fskey(sk) → (goodfieldandtype(r, sk, st) ↔ r -- sk ∈ st ∧ okval(st[r -- sk], sk .fs .type)) | A User Theorem |
| good-field-field-01 | ⊦ goodfieldandtype(r, mkfs(class1, ty, fieldvar) ', st) ↔ r -- mkfs(class1, ty, fieldvar) ' ∈ st ∧ okval(st[r -- mkfs(class1, ty, fieldvar) '], ty) | A User Theorem |
| good-field-field-02 | ⊦ goodfieldandtype(r, fs ', st) ↔ r -- fs ' ∈ st ∧ okval(st[r -- fs '], fs .type) | A User Theorem |
| good-field-field-03 | ⊦ goodfieldandtype(r, fs ', st) ↔ ¬ ¬ (r -- fs ' ∈ st ∧ okval(st[r -- fs '], fs .type)) | A User Theorem |
| good-field-in | ⊦ r -- sk ∈ st → (goodfieldandtype(r, sk, st) ↔ ¬ ¬ (is_fskey(sk) ∧ okval(st[r -- sk], sk .fs .type))) | A User Theorem |
| good-field-in-01 | ⊦ ¬ r -- sk ∈ st → ¬ goodfieldandtype(r, sk, st) | A User Theorem |
| good-field-index | ⊦ is_indexkey(sk) → ¬ goodfieldandtype(r, sk, st) | A User Theorem |
| good-field-put | ⊦ goodfieldandtype(r, sk, st[r0 -- i ', val]) ↔ goodfieldandtype(r, sk, st) | A User Theorem |
| good-field-rew | ⊦ goodfieldandtype(r, sk, st) ↔ ¬ ¬ (is_fskey(sk) ∧ r -- sk ∈ st ∧ okval(st[r -- sk], sk .fs .type)) | A User Theorem |
| good-field-subset | ⊦ st ⊆ st0 ∧ r -- sk ∈ st → (goodfieldandtype(r, sk, st0) ↔ goodfieldandtype(r, sk, st)) | A User Theorem |
| good-one | ⊦ goodfieldsandtypes(r, sk ', st) ↔ goodfieldandtype(r, sk, st) | A User Theorem |
| good-rec-01 | ⊦ goodfieldsandtypes(r, sk ' + sks, st) ↔ ¬ ¬ (goodfieldandtype(r, sk, st) ∧ goodfieldsandtypes(r, sks, st)) | A User Theorem |
| goodfields-putba | ⊦ r ≠ r1 → (goodfieldandtype(r, sk, putByteArray(bytes, r1, i, st)) ↔ goodfieldandtype(r, sk, st)) | A User Theorem |
| hasKeys-all | ⊦ hasKeys(r, sks, st) ↔ (∀ sk. sk ∈ sks → r -- sk ∈ st) | A User Theorem |
| hasKeys-app | ⊦ hasKeys(r, sks + sks0, st) ↔ hasKeys(r, sks, st) ∧ hasKeys(r, sks0, st) | A User Theorem |
| hasKeys-one | ⊦ hasKeys(r, sk ', st) ↔ r -- sk ∈ st | A User Theorem |
| hasKeys-put | ⊦ r ≠ r0 → (hasKeys(r, sks, st[r0 -- sk, val]) ↔ hasKeys(r, sks, st)) | A User Theorem |
| hasKeys-put-01 | ⊦ rk ∈ st → (hasKeys(r, sks, st[rk, val]) ↔ hasKeys(r, sks, st)) | A User Theorem |
| hasKeys-put-02 | ⊦ ¬ sk ∈ sks → (hasKeys(r, sks, st[r -- sk, val]) ↔ hasKeys(r, sks, st)) | A User Theorem |
| infis-jvmref | r ≠ jvmref ⊦ fis ∈ st[r -- sk, val] ↔ fis ∈ st | A User Theorem |
| infis-notin | ¬ sk ∈ fis ⊦ fis ∈ st[jvmref -- sk, val] ↔ fis ∈ st | A User Theorem |
| infis-notin-01 | ⊦ ¬ sk ∈ fis → (fis ∈ st[r -- sk, val] ↔ fis ∈ st) | A User Theorem |
| inst-in | ⊦ r = jvmref ∨ ¬ r -- _type ∈ st ∨ st[r -- _type] ≠ typeval(mkclasstype(class)) → ¬ instore(r, class, fis, st) | A User Theorem |
| inst-single | ⊦ instore(r, class, (sk × val) ', st) ↔ r ≠ jvmref ∧ r -- _type ∈ st ∧ st[r -- _type] = typeval(mkclasstype(class)) ∧ (r -- sk) × val ∈ st | A User Theorem |
| instore-afterputs | ⊦ ¬ _type ∈ fv + fis ∧ instore(r, class, fv + fis, st) ∧ unique_al(fv + fis) ∧ st1 = st[r -- fv .1, refval(r1)] → instore(r, class, fis, st1) ∧ instore(r, class, (fv .1 × refval(r1)) ', st1) | A User Theorem |
| instore-null | ⊦ ¬ instore(jvmref, class, fis, st) | A User Theorem |
| instore-one | ⊦ (sk × val) ' ∈ st ↔ (jvmref -- sk) × val ∈ st | A User Theorem |
| instore-rec-01 | ⊦ (sk × val) ' + fis ∈ st ↔ ¬ ¬ ((jvmref -- sk) × val ∈ st ∧ fis ∈ st) | A User Theorem |
| instore-rec-03 | ⊦ instore(r, class, fv ' + fis, st) ↔ (r -- fv .1) × fv .2 ∈ st ∧ instore(r, class, fis, st) | A User Theorem |
| intval-01 | ⊦ okarray(r, int_type, st) ∧ i < st[r -- _length] .intval ∧ 0 ≤ i → is_integervalue(st[r -- i ']) | A User Theorem |
| is-real-array-def-01 | ⊦ is_array(str, r, st) ↔ ¬ ¬ ( type∃(str, st[r -- _type] .type) ∧ st[r -- _type] .type .jtelemtype ≠ void_type ∧ st[r -- _type] .type .jtelemtype ≠ abstract_type ∧ is_array(r, st)) | A User Theorem |
| is_array-abstract | ⊦ is_array(str, r, st) → st[r -- _type] .type .type ≠ abstract_type | A User Theorem |
| is_array-arrayreftype | ⊦ ¬ is_referencevalue(st[r -- i ']) ∧ is_reftype(ty) ∧ ty0 ≤ ty ∧ st[r -- _type] .type = mkarraytype(ty0) ∧ r ≠ jvmref ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ is_array(str, r, st) | A User Theorem |
| is_array-arraytype | ⊦ ¬ is_arraytype(st[r -- _type] .type) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-badlength | ⊦ ¬ is_integervalue(st[r -- _length]) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-byte-noref | ⊦ is_array(r, st) ∧ st[r -- _type] .type = mkarraytype(byte_type) ∧ r ≠ jvmref ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → st[r -- i '] ≠ refval(r1) | A User Theorem |
| is_array-byte-noref-01 | ⊦ is_array(str, r, st) ∧ st[r -- _type] .type = mkarraytype(byte_type) ∧ r ≠ jvmref ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → st[r -- i '] ≠ refval(r1) | A User Theorem |
| is_array-bytearray | ⊦ st[r -- _type] = typeval(mkarraytype(byte_type)) ∧ r ≠ jvmref → (is_array(str, r, st) ↔ is_array(r, st)) | A User Theorem |
| is_array-bytearray-01 | ⊦ st[r -- _type] .type = mkarraytype(byte_type) ∧ r ≠ jvmref → (is_array(str, r, st) ↔ is_array(r, st)) | A User Theorem |
| is_array-classtype | ⊦ is_classtype(st[r -- _type] .type) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-del | ⊦ r ≠ r0 → (is_array(str, r0, st -- r) ↔ is_array(str, r0, st)) | A User Theorem |
| is_array-del-01 | ⊦ ¬ is_array(str, r, st -- r) | A User Theorem |
| is_array-hasnoclasstype | ⊦ ¬ is_array(str, r, st) ∧ ¬ has_classtype(st[r -- _type] .type) → ¬ is_array(str0, r, st) | A User Theorem |
| is_array-hasnoclasstype-01 | ⊦ ¬ is_array(str, r, st) ∧ ¬ has_classtype(ty) ∧ st[r -- _type] .type = mkarraytype(ty) → ¬ is_array(str0, r, st) | A User Theorem |
| is_array-is-array | ⊦ ¬ is_array(r, st) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-isarrayref | ⊦ ¬ is_arrayref(r, i, st) ∧ i ≤ st[r -- _length] .intval ∧ r ≠ jvmref → ¬ is_array(str, r, st) | A User Theorem |
| is_array-keyin | ⊦ ¬ st[r -- sk] .refval -- i ' ∈ st ∧ 0 ≤ i ∧ i < st[r -- (sk ' + _length ')] .intval → ¬ is_array(str, st[r -- sk] .refval, st) | A User Theorem |
| is_array-len | ⊦ is_array(str, r, st) → ¬ st[r -- _length] .intval < 0 | A User Theorem |
| is_array-lenfield | ⊦ ¬ r -- _length ∈ st → ¬ is_array(str, r, st) | A User Theorem |
| is_array-length | ⊦ is_array(str, r, st) → val2int(st[r -- _length]) = st[r -- _length] .intval | A User Theorem |
| is_array-length-01 | ⊦ st[r -- _length] .intval < 0 → ¬ is_array(str, r, st) | A User Theorem |
| is_array-length-02 | ⊦ st[r -- (sks + _length ')] .intval < 0 ∧ sks ≠ [] → ¬ is_array(str, st[r -- sks] .refval, st) | A User Theorem |
| is_array-length-03 | ⊦ st[r -- (sks + sk ' + _length ')] .intval < 0 → ¬ is_array(str, st[r -- (sks + sk ')] .refval, st) | A User Theorem |
| is_array-length-04 | ⊦ st[r -- (sk0 ' + sk ' + _length ')] .intval < 0 → ¬ is_array(str, st[r -- (sk0 ' + sk ')] .refval, st) | A User Theorem |
| is_array-length-05 | ⊦ st[r -- (sk1 ' + sk0 ' + sk ' + _length ')] .intval < 0 → ¬ is_array(str, st[r -- (sk1 ' + sk0 ' + sk ')] .refval, st) | A User Theorem |
| is_array-length-06 | ⊦ is_array(str, st[r -- sks] .refval, st) ∧ sks ≠ [] → ¬ st[r -- (sks + _length ')] .intval < 0 | A User Theorem |
| is_array-length-07 | ⊦ is_array(str, r, st) → is_integervalue(st[r -- _length]) | A User Theorem |
| is_array-newref | ⊦ newref(r, st) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-noreftype | ⊦ is_referencevalue(st[r -- i ']) ∧ ¬ is_reftype(st[r -- _type] .type .type) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ is_array(str, r, st) | A User Theorem |
| is_array-norefval | ⊦ ¬ is_referencevalue(st[r -- i ']) ∧ is_reftype(st[r -- _type] .type .type) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ is_array(str, r, st) | A User Theorem |
| is_array-notin | ⊦ ¬ r ∈ st → ¬ is_array(str, r, st) | A User Theorem |
| is_array-notin-01 | ⊦ ¬ r -- i ' ∈ st ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ r ≠ jvmref → ¬ is_array(str, r, st) | A User Theorem |
| is_array-nottypeex | ⊦ ¬ type∃(str, st[r -- _type] .type .type) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-notypeval | ⊦ ¬ is_typevalue(st[r -- _type]) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-null | ⊦ ¬ is_array(str, jvmref, st) | A User Theorem |
| is_array-okarray | ⊦ okarray(r, byte_type, st) → is_array(str, r, st) | A User Theorem |
| is_array-okarray-01 | ⊦ ¬ okarray(r, ty, st) ∧ st[r -- _type] .type = mkarraytype(ty0) ∧ ty0 ≤ ty → ¬ is_array(str, r, st) | A User Theorem |
| is_array-okbytearray | ⊦ okbytearray(r, st) → is_array(str, r, st) | A User Theorem |
| is_array-primtype | ⊦ is_array(r, st) ∧ is_primtype(ty) ∧ st[r -- _type] = typeval(mkarraytype(ty)) → is_array(str, r, st) | A User Theorem |
| is_array-primtype-01 | ⊦ is_array(r, st) ∧ is_primtype(ty) ∧ st[r -- _type] = typeval(mkarraytype(ty)) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → st[r -- i '] ≠ refval(r0) | A User Theorem |
| is_array-put | ⊦ is_array(str, r, st) ∧ oktype(val, ty, st) ∧ ty ≠ void_type ∧ mkfs(class, ty, fieldvar) ' ≠ _length → is_array(str, r, st[r1 -- mkfs(class, ty, fieldvar) ', val]) | A User Theorem |
| is_array-put-01 | ⊦ r ≠ r0 → (is_array(str, r0, st[r -- sk, val]) ↔ is_array(str, r0, st)) | A User Theorem |
| is_array-put-badfield | ⊦ is_array(str, r, st) ∧ fs ' ≠ _type ∧ fs ' ≠ _length → is_array(str, r, st[r -- fs ', val]) | A User Theorem |
| is_array-put-byte | ⊦ is_array(str, r0, st) ∧ okbytearray(r, st) → is_array(str, r0, st[r -- i ', byteval(by)]) | A User Theorem |
| is_array-put-field | ⊦ fs ' ≠ _length ∧ fs ' ≠ _type → (is_array(str, r, st[r0 -- fs ', val]) ↔ is_array(str, r, st)) | A User Theorem |
| is_array-put-jvmref | ⊦ is_array(str, r, st) → is_array(str, r, st[jvmref -- sk, val]) | A User Theorem |
| is_array-put-okval | ⊦ is_array(str, r, st) ∧ okval(val, st[r -- _type] .type .type) → is_array(str, r, st[r -- i ', val]) | A User Theorem |
| is_array-put-samefield | ⊦ is_array(str, r, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type ∧ fs ' ≠ _length → is_array(str, r, st[r -- fs ', val]) | A User Theorem |
| is_array-put-samefield-01 | ⊦ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type ∧ fs ' ≠ _length → (is_array(str, r, st[r -- fs ', val]) ↔ is_array(str, r, st)) | A User Theorem |
| is_array-putbar | ⊦ okbytearray(r1, st) ∧ is_array(str, r, putByteArray(bytes, r1, i, st)) → is_array(str, r, st) | A User Theorem |
| is_array-putbar-01 | ⊦ ¬ is_array(str, r, st) ∧ okbytearray(r1, st) → ¬ is_array(str, r, putByteArray(bytes, r1, i, st)) | A User Theorem |
| is_array-reftype | ⊦ ¬ is_reftype(st[r -- _type] .type) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-subset | ⊦ st ⊆ st1 ∧ is_array(str, r, st) → is_array(str, r, st1) | A User Theorem |
| is_array-type | ⊦ is_array(str, r, st) → st[r -- _type] ≠ typeval(mkclasstype(class)) | A User Theorem |
| is_array-type-01 | ⊦ is_array(str, r, st) → st[r -- _type] .type ≠ mkclasstype(class) | A User Theorem |
| is_array-type-02 | ⊦ ¬ r -- _type ∈ st → ¬ is_array(str, r, st) | A User Theorem |
| is_array-type-03 | ⊦ st[r -- _type] = typeval(mkclasstype(class)) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-type-04 | ⊦ st[r -- _type] .type = mkclasstype(class) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-typeex | ⊦ ¬ type∃(str, st[r -- _type] .type) ∧ r ≠ jvmref → ¬ is_array(str, r, st) | A User Theorem |
| is_array-typeex-01 | ⊦ ¬ type∃(str, st[r -- _type] .type) → ¬ is_array(str, r, st) | A User Theorem |
| is_array-typele | ⊦ is_array(str, r, st) → (st[r -- _type] .type ≤ mkclasstype(class) ↔ class = `java.lang.Object' .class) | A User Theorem |
| is_array-union | ⊦ is_array(str, r, st) → is_array(str, r, st0 ∪ st) | A User Theorem |
| is_array-union-disjoint | ⊦ st1 .refs ∩ st .refs = ∅ ∧ r ∈ st1 ∧ is_array(str, r, st1) → is_array(str, r, st1 ∪ st) | A User Theorem |
| is_array-update | ⊦ r ≠ r0 → (is_array(str, r, update(r0, fis, st)) ↔ is_array(str, r, st)) | A User Theorem |
| isarray-abstract | ⊦ is_array(r, st) ∧ st[r -- _type] .type .type = abstract_type → st[r -- _length] .intval = 0 | A User Theorem |
| isarray-arrayreftype | ⊦ ¬ is_referencevalue(st[r -- i ']) ∧ is_reftype(ty) ∧ ty0 ≤ ty ∧ st[r -- _type] .type = mkarraytype(ty0) ∧ r ≠ jvmref ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ is_array(r, st) | A User Theorem |
| isarray-arrayrefval | ⊦ is_referencevalue(st[r -- i ']) ∧ ¬ is_reftype(st[r -- _type] .type .type) ∧ st[r -- _type] .type .type ≠ void_type ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ is_array(r, st) | A User Theorem |
| isarray-bytearray | ⊦ ¬ okbytearray(r, st) ∧ st[r -- _type] .type = mkarraytype(byte_type) ∧ r ≠ jvmref → ¬ is_array(r, st) | A User Theorem |
| isarray-del | ⊦ r ≠ r0 → (is_array(r0, st -- r) ↔ is_array(r0, st)) | A User Theorem |
| isarray-del-01 | ⊦ ¬ is_array(r, st -- r) | A User Theorem |
| isarray-isarrayref | ⊦ ¬ is_arrayref(r, i, st) ∧ i ≤ st[r -- _length] .intval ∧ r ≠ jvmref → ¬ is_array(r, st) | A User Theorem |
| isarray-keyin | ⊦ ¬ st[r -- sk] .refval -- i ' ∈ st ∧ 0 ≤ i ∧ i < st[r -- (sk ' + _length ')] .intval → ¬ is_array(st[r -- sk] .refval, st) | A User Theorem |
| isarray-len | ⊦ is_array(r, st) → ¬ st[r -- _length] .intval < 0 | A User Theorem |
| isarray-lenfield | ⊦ ¬ r -- _length ∈ st → ¬ is_array(r, st) | A User Theorem |
| isarray-length | ⊦ is_array(r, st) → val2int(st[r -- _length]) = st[r -- _length] .intval | A User Theorem |
| isarray-length-01 | ⊦ st[r -- _length] .intval < 0 → ¬ is_array(r, st) | A User Theorem |
| isarray-length-02 | ⊦ st[r -- (sks + _length ')] .intval < 0 ∧ sks ≠ [] → ¬ is_array(st[r -- sks] .refval, st) | A User Theorem |
| isarray-length-03 | ⊦ st[r -- (sks + sk ' + _length ')] .intval < 0 → ¬ is_array(st[r -- (sks + sk ')] .refval, st) | A User Theorem |
| isarray-length-04 | ⊦ st[r -- (sk0 ' + sk ' + _length ')] .intval < 0 → ¬ is_array(st[r -- (sk0 ' + sk ')] .refval, st) | A User Theorem |
| isarray-length-05 | ⊦ st[r -- (sk1 ' + sk0 ' + sk ' + _length ')] .intval < 0 → ¬ is_array(st[r -- (sk1 ' + sk0 ' + sk ')] .refval, st) | A User Theorem |
| isarray-length-06 | ⊦ is_array(st[r -- sks] .refval, st) ∧ sks ≠ [] → ¬ st[r -- (sks + _length ')] .intval < 0 | A User Theorem |
| isarray-length-07 | ⊦ is_array(r, st) → is_integervalue(st[r -- _length]) | A User Theorem |
| isarray-newref | ⊦ newref(r, st) → ¬ is_array(r, st) | A User Theorem |
| isarray-notin | ⊦ ¬ r ∈ st → ¬ is_array(r, st) | A User Theorem |
| isarray-notin-01 | ⊦ ¬ r -- i ' ∈ st ∧ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ r ≠ jvmref → ¬ is_array(r, st) | A User Theorem |
| isarray-null | ⊦ ¬ is_array(jvmref, st) | A User Theorem |
| isarray-okarray | ⊦ ¬ is_array(r, st) → ¬ okarray(r, ty, st) | A User Theorem |
| isarray-okarray-01 | ⊦ ¬ okarray(r, ty, st) ∧ st[r -- _type] .type = mkarraytype(ty0) ∧ ty0 ≤ ty → ¬ is_array(r, st) | A User Theorem |
| isarray-okreftype | ⊦ is_array(r, st) → (okreftype(refval(r), mkclasstype(class), st) ↔ class = `java.lang.Object' .class) | A User Theorem |
| isarray-okval | ⊦ ¬ okval(st[r -- i '], st[r -- _type] .type .type) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ is_array(r, st) | A User Theorem |
| isarray-put | ⊦ is_array(r, st) ∧ oktype(val, ty, st) ∧ ty ≠ void_type ∧ mkfs(class, ty, fieldvar) ' ≠ _length → is_array(r, st[r1 -- mkfs(class, ty, fieldvar) ', val]) | A User Theorem |
| isarray-put-01 | ⊦ r ≠ r0 → (is_array(r0, st[r -- sk, val]) ↔ is_array(r0, st)) | A User Theorem |
| isarray-put-array-badindex | ⊦ i < 0 → (is_array(r0, st[r -- i ', val]) ↔ is_array(r0, st)) | A User Theorem |
| isarray-put-badfield | ⊦ is_array(r, st) ∧ fs ' ≠ _type ∧ fs ' ≠ _length → is_array(r, st[r -- fs ', val]) | A User Theorem |
| isarray-put-byte | ⊦ is_array(r0, st) ∧ okbytearray(r, st) → is_array(r0, st[r -- i ', byteval(by)]) | A User Theorem |
| isarray-put-field | ⊦ fs ' ≠ _length ∧ fs ' ≠ _type → (is_array(r, st[r0 -- fs ', val]) ↔ is_array(r, st)) | A User Theorem |
| isarray-put-jvmref | ⊦ is_array(r, st) → is_array(r, st[jvmref -- sk, val]) | A User Theorem |
| isarray-put-okval | ⊦ is_array(r, st) ∧ okval(val, st[r -- _type] .type .type) → is_array(r, st[r -- i ', val]) | A User Theorem |
| isarray-put-samefield | ⊦ is_array(r, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type ∧ fs ' ≠ _length → is_array(r, st[r -- fs ', val]) | A User Theorem |
| isarray-put-samefield-01 | ⊦ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type ∧ fs ' ≠ _length → (is_array(r, st[r -- fs ', val]) ↔ is_array(r, st)) | A User Theorem |
| isarray-putbar | ⊦ okbytearray(r1, st) ∧ is_array(r, putByteArray(bytes, r1, i, st)) → is_array(r, st) | A User Theorem |
| isarray-reftype | ⊦ ¬ is_reftype(st[r -- _type] .type) → ¬ is_array(r, st) | A User Theorem |
| isarray-subset | ⊦ st ⊆ st1 ∧ is_array(r, st) → is_array(r, st1) | A User Theorem |
| isarray-type | ⊦ ¬ is_arraytype(st[r -- _type] .type) → ¬ is_array(r, st) | A User Theorem |
| isarray-type-01 | ⊦ is_array(r, st) → st[r -- _type] .type ≠ mkclasstype(class) | A User Theorem |
| isarray-type-02 | ⊦ is_array(r, st) → st[r -- _type] ≠ typeval(mkclasstype(class)) | A User Theorem |
| isarray-type-03 | ⊦ st[r -- _type] = typeval(mkclasstype(class)) → ¬ is_array(r, st) | A User Theorem |
| isarray-type-04 | ⊦ st[r -- _type] .type = mkclasstype(class) → ¬ is_array(r, st) | A User Theorem |
| isarray-type-05 | ⊦ ¬ r -- _type ∈ st → ¬ is_array(r, st) | A User Theorem |
| isarray-union | ⊦ is_array(r, st) → is_array(r, st0 ∪ st) | A User Theorem |
| isarray-union-disjoint | ⊦ st1 .refs ∩ st .refs = ∅ ∧ r ∈ st1 ∧ is_array(r, st1) → is_array(r, st1 ∪ st) | A User Theorem |
| isarray-update | ⊦ r ≠ r0 → (is_array(r, update(r0, fis, st)) ↔ is_array(r, st)) | A User Theorem |
| keys-at | ⊦ n < # fis → (fis .keys)[n] = fis[n] .1 | A User Theorem |
| keys-empty | ⊦ fis .keys = [] ↔ fis = [] | A User Theorem |
| keys-in | ⊦ sk ∈ fis .keys ↔ sk ∈ fis | A User Theorem |
| keys-in-01 | ⊦ sk ∈ fis ↔ sk ∈ fis .keys | A User Theorem |
| keys-length | ⊦ # fis .keys = # fis | A User Theorem |
| keys-notin | ⊦ ¬ sk ∈ fis ∧ sk ∈ sks → fis .keys ≠ sks | A User Theorem |
| keys-notin-01 | ⊦ ¬ sk ∈ fis → ¬ sk ∈ fis .keys | A User Theorem |
| keys-notin-02 | ⊦ ¬ sk ∈ fis .keys → ¬ sk ∈ fis | A User Theorem |
| keys-put | ⊦ sk0 ∈ fis[sk, val] .keys ↔ sk0 ∈ fis .keys ∨ sk0 = sk | A User Theorem |
| keys-put-in | ⊦ sk ∈ fis → fis[sk, val] .keys = fis .keys | A User Theorem |
| keys-put-notin | ⊦ ¬ sk ∈ fis → fis[sk, val] .keys = fis .keys + sk | A User Theorem |
| mode | r ≠ jvmref ⊦ okclass(refval(r), class1, st[_mode, val]) ↔ okclass(refval(r), class1, st) | A User Theorem |
| mode-01 | r ≠ jvmref ⊦ goodfieldandtype(r, sk, st[_mode, val]) ↔ goodfieldandtype(r, sk, st) | A User Theorem |
| mode-02 | ⊦ okarray(val, ty, i, st[_mode, val0]) ↔ okarray(val, ty, i, st) | A User Theorem |
| mode-02-01 | ⊦ exactarray(val, ty, i, st[_mode, val0]) ↔ exactarray(val, ty, i, st) | A User Theorem |
| mode-03 | ⊦ oktype(val, ty, st[_mode, val0]) ↔ oktype(val, ty, st) | A User Theorem |
| nonnullrefs-dups | ⊦ fis[sk] = refval(r) ∧ fis[sk0] = refval(r) ∧ sk ≠ sk0 ∧ sk ∈ fis ∧ sk0 ∈ fis ∧ r ≠ jvmref → dups(fis .vals .nonnullrefs) | A User Theorem |
| nonnullrefs-dups-key | ⊦ ¬ dups(fis .keys) → (dups(fis .vals .nonnullrefs) ↔ (∃ r, sk, sk0. sk ≠ sk0 ∧ r ≠ jvmref ∧ fis[sk] = refval(r) ∧ fis[sk0] = refval(r) ∧ sk ∈ fis ∧ sk0 ∈ fis)) | A User Theorem |
| nonnullrefs-in | ⊦ fis[sk] = refval(r) ∧ sk ∈ fis ∧ r ≠ jvmref → r ∈ fis .vals .nonnullrefs | A User Theorem |
| nonnullrefs-in-key | ⊦ ¬ dups(fis .keys) → (r ∈ fis .vals .nonnullrefs ↔ r ≠ jvmref ∧ (∃ sk. fis[sk] = refval(r) ∧ sk ∈ fis)) | A User Theorem |
| okarray-01 | ⊦ okarray(refval(r), ty, i, st) → st[r -- _length] .intval = i | A User Theorem |
| okarray-02 | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) ∧ r ≠ r0 → (okarray(refval(r), ty, i, st[r0 -- sk, val0]) ↔ okarray(refval(r), ty, i, st)) | A User Theorem |
| okarray-04 | ⊦ ¬ okarray(jvmref, ty, st) | A User Theorem |
| okarray-05 | ⊦ okarray(r, ty, st) → r ≠ jvmref ∧ r ∈ st | A User Theorem |
| okarray-06 | ⊦ r ≠ r0 → (okarray(r, int_type, st[r0 -- sk, val]) ↔ okarray(r, int_type, st)) | A User Theorem |
| okarray-07 | ⊦ okarray(r, int_type, st) → okarray(r, int_type, st[r0 -- j ', intval(i)]) | A User Theorem |
| okarray-08 | ⊦ ¬ okarray(r, int_type, st[r0 -- j ', val]) ∧ okarray(r, int_type, st) → ¬ is_integervalue(val) | A User Theorem |
| okarray-byte | ⊦ st[r -- i '] .byteval = st[r0 -- j '] .byteval ∧ okarray(r, byte_type, st) ∧ okarray(r0, byte_type, st) ∧ i < st[r -- _length] .intval ∧ j < st[r0 -- _length] .intval ∧ 0 ≤ i ∧ 0 ≤ j → (st[r -- i '] = st[r0 -- j '] ↔ true) | A User Theorem |
| okarray-byte-01 | ⊦ st[r -- (i0 + i) '] .byteval = st[r0 -- (j0 + i) '] .byteval ∧ okarray(r, byte_type, st) ∧ okarray(r0, byte_type, st) ∧ i < j ∧ i0 + j < st[r -- _length] .intval ∧ j0 + j < st[r0 -- _length] .intval ∧ 0 ≤ i0 + i ∧ 0 ≤ j0 + i → (st[r -- (i0 + i) '] = st[r0 -- (j0 + i) '] ↔ true) | A User Theorem |
| okarray-byteput | ⊦ 0 ≤ j ∧ j < i ∧ okarray(refval(r), byte_type, i, st) → okarray(refval(r), byte_type, i, st[r -- j ', byteval(by)]) | A User Theorem |
| okarray-copy | r1 ≠ r0 ⊦ okarray(r1, ty, arraycopy(r, i, r0, i0, j, st)) ↔ okarray(r1, ty, st) | A User Theorem |
| okarray-copy-01 | ⊦ okarray(r, byte_type, st) ∧ okarray(r0, byte_type, st) ∧ 0 ≤ i ∧ 0 ≤ j ∧ i + j ≤ st[r0 -- _length] .intval → okarray(r, byte_type, arraycopy(r0, i, r, i0, j, st)) | A User Theorem |
| okarray-del | ⊦ r ≠ r0 → (okarray(r0, ty, st -- r) ↔ okarray(r0, ty, st)) | A User Theorem |
| okarray-getbar-len | ⊦ okarray(val, byte_type, n→i(n), st) → # getbytearray(val .refval, st) = n | A User Theorem |
| okarray-int-put | ⊦ okarray(r, int_type, st) → okarray(r, int_type, st[r -- i ', intval(j)]) | A User Theorem |
| okarray-int-put-01 | ⊦ okarray(r, int_type, st) ∧ is_integervalue(val) → okarray(r, int_type, st[r -- i ', val]) | A User Theorem |
| okarray-int-put-02 | ⊦ okarray(r, int_type, st) ∧ 0 ≤ j ∧ j < st[r -- _length] .intval → okarray(r, int_type, st[r -- i ', st[r -- j ']]) | A User Theorem |
| okarray-intval | ⊦ okarray(r, int_type, st) ∧ i < st[r -- _length] .intval ∧ 0 ≤ i → intval(st[r -- i '] .intval) = st[r -- i '] | A User Theorem |
| okarray-intval-01 | ⊦ okarray(r, ty, st) → intval(st[r -- _length] .intval) = st[r -- _length] | A User Theorem |
| okarray-jvmref | ⊦ ¬ okarray(refval(jvmref), ty, i, st) | A User Theorem |
| okarray-jvmref-01 | ⊦ okarray(refval(r), ty, i, st) → r ≠ jvmref | A User Theorem |
| okarray-len | ⊦ okarray(r, ty, st) → ¬ st[r -- _length] .intval < 0 | A User Theorem |
| okarray-length | ⊦ okarray(r, ty, st) → ¬ val2int(st[r -- _length]) < 0 | A User Theorem |
| okarray-length-01 | ⊦ okarray(refval(r), ty, i, st) → val2int(st[r -- _length]) = i | A User Theorem |
| okarray-length-02 | ⊦ okarray(r, ty, st) → val2int(st[r -- _length]) = st[r -- _length] .intval | A User Theorem |
| okarray-new | ⊦ newref(r, st) → ¬ okarray(refval(r), ty, i, st[rk, val]) | A User Theorem |
| okarray-new-01 | ⊦ okarray(refval(r), ty, i, st) → ¬ newref(r, st) | A User Theorem |
| okarray-noval | ⊦ ¬ okarray(noval, ty, i, st) | A User Theorem |
| okarray-null | ⊦ val .refval = jvmref → ¬ okarray(val, ty, i, st) | A User Theorem |
| okarray-okarray | ⊦ ¬ okarray(val .refval, ty, st) → ¬ okarray(val, ty, i, st) | A User Theorem |
| okarray-okarray-01 | ⊦ okarray(val, ty, i, st) ↔ okarray(val .refval, ty, st) ∧ st[val .refval -- _length] .intval = i | A User Theorem |
| okarray-okarray-02 | ⊦ ¬ okarray(r, ty, st) → ¬ okarray(refval(r), ty, i, st) | A User Theorem |
| okarray-onlymod | ⊦ val .refval ≠ r0 ∧ ¬ okarray(val, ty, i, st0) ∧ onlyModified(r0, st, st0) ∧ is_referencevalue(val) → ¬ okarray(val, ty, i, st) | A User Theorem |
| okarray-out | ⊦ okarray(val, ty, i, st[_out, val0]) ↔ okarray(val, ty, i, st) | A User Theorem |
| okarray-primput | ⊦ okprimtype(val, ty) ∧ 0 ≤ j ∧ j < i ∧ okarray(refval(r), ty, i, st) → okarray(refval(r), ty, i, st[r -- j ', val]) | A User Theorem |
| okarray-put | ⊦ sk ≠ _type ∧ goodfieldandtype(r0, sk, st) ∧ oktype(val0, sk .fs .type, st) ∧ sk ≠ _length → (okarray(val, ty, i, st[r0 -- sk, val0]) ↔ okarray(val, ty, i, st)) | A User Theorem |
| okarray-put-01 | ⊦ okarray(r, byte_type, st) → okarray(r, byte_type, st[r0 -- i ', byteval(by)]) | A User Theorem |
| okarray-put-02 | ⊦ okarray(val, byte_type, i, st) → okarray(val, byte_type, i, st[r0 -- j ', byteval(by)]) | A User Theorem |
| okarray-put-03 | ⊦ r ≠ r0 → (okarray(refval(r), byte_type, i, st[r0 -- sk, val0]) ↔ okarray(refval(r), byte_type, i, st)) | A User Theorem |
| okarray-put-04 | ⊦ okarray(r, int_type, st) → okarray(r, int_type, st[r0 -- i ', intval(j)]) | A User Theorem |
| okarray-put-05 | ⊦ r ≠ r0 → (okarray(r, byte_type, st[r0 -- sk, val]) ↔ okarray(r, byte_type, st)) | A User Theorem |
| okarray-put-06 | ⊦ is_bytevalue(val) ∧ okarray(r, byte_type, st) → okarray(r, byte_type, st[r -- i ', val]) | A User Theorem |
| okarray-put-07 | ⊦ refval(rk .ref) ≠ val → (okarray(val, ty, i, st[rk, val0]) ↔ okarray(val, ty, i, st)) | A User Theorem |
| okarray-put-08 | ⊦ sk ≠ _length ∧ sk ≠ _type ∧ is_fskey(sk) → (okarray(val, ty, i, st[r -- sk, val0]) ↔ okarray(val, ty, i, st)) | A User Theorem |
| okarray-put-badfield | ⊦ okarray(r, ty, st) ∧ fs ' ≠ _type ∧ fs ' ≠ _length → okarray(r, ty, st[r -- fs ', val]) | A User Theorem |
| okarray-put-okval | ⊦ okarray(r, ty, st) ∧ okval(val, ty) → okarray(r, ty, st[r -- i ', val]) | A User Theorem |
| okarray-put-okval-01 | ⊦ okarray(val, ty, j, st) ∧ okval(val0, ty) → okarray(val, ty, j, st[r -- i ', val0]) | A User Theorem |
| okarray-put-other | ⊦ r ≠ r1 → (okarray(r, ty, st[r1 -- sk, val]) ↔ okarray(r, ty, st)) | A User Theorem |
| okarray-put-samefield | ⊦ okarray(r, ty, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type ∧ fs ' ≠ _length → okarray(r, ty, st[r -- fs ', val]) | A User Theorem |
| okarray-put-samefield-01 | ⊦ r -- fs ' ∈ st ∧ oktype(st[r -- fs '], fs .type, st) ∧ oktype(val, fs .type, st) ∧ fs ' ≠ _type ∧ fs ' ≠ _length → (okarray(r, ty, st[r -- fs ', val]) ↔ okarray(r, ty, st)) | A User Theorem |
| okarray-putar | ⊦ r ≠ r1 → (okarray(refval(r1), byte_type, j, putArray(vals, r, i, st)) ↔ okarray(refval(r1), byte_type, j, st)) | A User Theorem |
| okarray-putba | ⊦ r ≠ val .refval → (okarray(val, ty, i, putByteArray(bytes, r, i1, st)) ↔ okarray(val, ty, i, st)) | A User Theorem |
| okarray-putbar | ⊦ r ≠ r1 → (okarray(refval(r1), byte_type, j, putByteArray(bytes, r, i, st)) ↔ okarray(refval(r1), byte_type, j, st)) | A User Theorem |
| okarray-putbar-01 | ⊦ r ≠ r1 ∧ ¬ okarray(r, byte_type, st) → ¬ okarray(r, byte_type, putByteArray(bytes, r1, st)) | A User Theorem |
| okarray-putbar-02 | ⊦ r ≠ r1 ∧ ¬ okarray(r, byte_type, putByteArray(bytes, r1, st)) → ¬ okarray(r, byte_type, st) | A User Theorem |
| okarray-putbar-03 | ⊦ r ≠ r1 ∧ okarray(r, byte_type, putByteArray(bytes, r1, st)) → okarray(r, byte_type, st) | A User Theorem |
| okarray-putbar-04 | ⊦ r ≠ r1 ∧ okarray(r, byte_type, st) → okarray(r, byte_type, putByteArray(bytes, r1, st)) | A User Theorem |
| okarray-putbar-05 | ⊦ okarray(r, byte_type, st) → okarray(r, byte_type, putByteArray(bytes, r, st)) | A User Theorem |
| okarray-putbar-any | ⊦ okarray(r, byte_type, st) → okarray(r, byte_type, putByteArray(bytes, r0, i, st)) | A User Theorem |
| okarray-putbar-any-01 | ⊦ okarray(val, byte_type, j, st) → okarray(val, byte_type, j, putByteArray(bytes, r0, i, st)) | A User Theorem |
| okarray-putbar-other | ⊦ r ≠ r1 → (okarray(r, ty, putByteArray(bytes, r1, i, st)) ↔ okarray(r, ty, st)) | A User Theorem |
| okarray-putbar-same | ⊦ ¬ okarray(r, byte_type, putByteArray(bytes, r, i, st)) → ¬ okarray(r, byte_type, st) | A User Theorem |
| okarray-putbar-same-01 | ⊦ ¬ okarray(refval(r), byte_type, j, putByteArray(bytes, r, i, st)) → ¬ okarray(refval(r), byte_type, j, st) | A User Theorem |
| okarray-putbar-same-02 | ⊦ okarray(refval(r), byte_type, j, st) → okarray(refval(r), byte_type, j, putByteArray(bytes, r, i, st)) | A User Theorem |
| okarray-putbar-same-03 | ⊦ okarray(r, byte_type, st) → okarray(r, byte_type, putByteArray(bytes, r, i, st)) | A User Theorem |
| okarray-refval | ⊦ ¬ is_referencevalue(val) → ¬ okarray(val, ty, i, st) | A User Theorem |
| okarray-subset | ⊦ okarray(val, ty, i, st) ∧ st ⊆ st0 → okarray(val, ty, i, st0) | A User Theorem |
| okarray-subset-01 | ⊦ okarray(r, ty, st) ∧ st ⊆ st0 → okarray(r, ty, st0) | A User Theorem |
| okarray-subset-02 | ⊦ okarray(r, ty, st) ∧ ¬ okarray(r, ty, st0) → ¬ st ⊆ st0 | A User Theorem |
| okarray-substore | ⊦ okarray(val, ty, i, st) ∧ ¬ okarray(val, ty, i, st0) → ¬ st ⊆ st0 | A User Theorem |
| okarray-supertype | ⊦ okarray(r, ty, st) ∧ ty ≤ ty0 → okarray(r, ty0, st) | A User Theorem |
| okarray-type | ⊦ okarray(refval(r), ty, i, st) → is_typevalue(st[r -- _type]) | A User Theorem |
| okarray-type-01 | ⊦ okarray(refval(r), ty, i, st) → st[r -- _type] .type ≤ mkarraytype(ty) | A User Theorem |
| okarray-type-02 | ⊦ okarray(refval(r), ty, i, st) → (¬ st[r -- _type] .type .type ≤ ty ↔ false) | A User Theorem |
| okarray-type-03 | ⊦ okarray(r, byte_type, st) → st[r -- _type] .type = mkarraytype(byte_type) | A User Theorem |
| okarray-union | ⊦ ¬ r ∈ st .refs → (okarray(refval(r), ty, i, st ∪ st0) ↔ okarray(refval(r), ty, i, st0)) | A User Theorem |
| okarray-union-01 | ⊦ ¬ r ∈ st → (okarray(refval(r), ty, i, st ∪ st0) ↔ okarray(refval(r), ty, i, st0)) | A User Theorem |
| okarray-union-02 | ⊦ r ∈ st0 ∧ st .refs ∩ st0 .refs = ∅ → (okarray(refval(r), ty, i, st ∪ st0) ↔ okarray(refval(r), ty, i, st0)) | A User Theorem |
| okarray-union-03 | ⊦ okarray(val, ty, i, st) → okarray(val, ty, i, st0 ∪ st) | A User Theorem |
| okarray-union-04 | ⊦ okarray(val, ty, i, st0) → (¬ okarray(val, ty, i, st ∪ st0) ↔ false) | A User Theorem |
| okarray-update | ⊦ r ≠ r0 → (okarray(refval(r), ty, i, update(r0, fis, st)) ↔ okarray(refval(r), ty, i, st)) | A User Theorem |
| okarray-update-01 | ⊦ r ≠ val .refval → (okarray(val, ty, i, update(r, fis, st)) ↔ okarray(val, ty, i, st)) | A User Theorem |
| okarrays-all | ⊦ okarrays(r, fis, st) ↔ (∀ sk, val. sk × val ∈ fis → is_integervalue(val) ∧ is_fskey(sk) ∧ is_arraytype(sk .fs .type) ∧ okarray(st[r -- sk], sk .fs .type .type, val .intval, st)) | A User Theorem |
| okarrays-mode | ⊦ r ≠ jvmref → (okarrays(r, fis, st[_mode, val]) ↔ okarrays(r, fis, st)) | A User Theorem |
| okarrays-not | ⊦ ¬ okarrays(r, fis, st[r0 -- mkfs(class0, ty, fieldvar) ', val]) ∧ mkfs(class0, ty, fieldvar) ' ≠ _type ∧ oktype(val, ty, st) ∧ ¬ mkfs(class0, ty, fieldvar) ' ∈ fis ∧ mkfs(class0, ty, fieldvar) ' ≠ _length → ¬ okarrays(r, fis, st) | A User Theorem |
| okarrays-one | ⊦ okarrays(r, (sk × val) ', st) ↔ is_integervalue(val) ∧ is_fskey(sk) ∧ is_arraytype(sk .fs .type) ∧ okarray(st[r -- sk], sk .fs .type .type, val .intval, st) | A User Theorem |
| okarrays-one-01 | ⊦ okarrays(r, (sk × val) ', st) ↔ ¬ ¬ (is_integervalue(val) ∧ is_fskey(sk) ∧ is_arraytype(sk .fs .type) ∧ okarray(st[r -- sk], sk .fs .type .type, val .intval, st)) | A User Theorem |
| okarrays-put | ⊦ sk ≠ _type ∧ goodfieldandtype(r0, sk, st) ∧ oktype(val, sk .fs .type, st) ∧ ¬ sk ∈ fis ∧ sk ≠ _length → (okarrays(r, fis, st[r0 -- sk, val]) ↔ okarrays(r, fis, st)) | A User Theorem |
| okarrays-put-01 | ⊦ sk ≠ _type ∧ is_fskey(sk) ∧ oktype(val, sk .fs .type, st) ∧ ¬ sk ∈ fis ∧ sk ≠ _length → (okarrays(r, fis, st[jvmref -- sk, val]) ↔ okarrays(r, fis, st)) | A User Theorem |
| okarrays-put-02 | ⊦ ¬ sk ∈ fis ∧ sk ≠ _type ∧ sk ≠ _length ∧ is_fskey(sk) → (okarrays(r, fis, st[r0 -- sk, val]) ↔ okarrays(r, fis, st)) | A User Theorem |
| okarrays-put-03 | ⊦ ¬ rk .key ∈ fis ∧ rk .key ≠ _type ∧ rk .key ≠ _length ∧ is_fskey(rk .key) → (okarrays(r, fis, st[rk, val]) ↔ okarrays(r, fis, st)) | A User Theorem |
| okarrays-rec-01 | ⊦ okarrays(r, (sk × val) ' + fis, st) ↔ ¬ ¬ ( is_integervalue(val) ∧ is_fskey(sk) ∧ is_arraytype(sk .fs .type) ∧ okarray(st[r -- sk], sk .fs .type .type, val .intval, st) ∧ okarrays(r, fis, st)) | A User Theorem |
| okarraytype-01 | ⊦ okarraytype(val, ty, st) ↔ ¬ ¬ (is_referencevalue(val) ∧ (val .refval ≠ jvmref → okarray(val .refval, ty, st))) | A User Theorem |
| okbar | ⊦ ¬ okbytearray(jvmref, st) | A User Theorem |
| okbar-01 | ⊦ okbytearray(r, st) → val2int(st[r -- _length]) = st[r -- _length] .intval | A User Theorem |
| okbar-bytes2int-same | ⊦ okarray(r, byte_type, st) ∧ okarray(r1, byte_type, st) ∧ st[r -- _length] .intval = st[r1 -- _length] .intval ∧ getbytearray(r, st) ≠ getbytearray(r1, st) → bytes2int(getbytearray(r, st)) ≠ bytes2int(getbytearray(r1, st)) | A User Theorem |
| okbar-byteval | ⊦ okbytearray(r, st) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → (¬ is_bytevalue(st[r -- i ']) ↔ false) | A User Theorem |
| okbar-len | ⊦ okbytearray(r, st) → ¬ st[r -- _length] .intval < 0 | A User Theorem |
| okbar-lenfield | ⊦ ¬ r -- _length ∈ st → ¬ okbytearray(r, st) | A User Theorem |
| okbar-new | ⊦ newref(r, st) → ¬ okbytearray(r, st) | A User Theorem |
| okbar-norefval | ⊦ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ okbytearray(r, st) → st[r -- i '] ≠ refval(r1) | A User Theorem |
| okbar-put | ⊦ r ≠ rk .ref → (okbytearray(r, st[rk, val]) ↔ okbytearray(r, st)) | A User Theorem |
| okbar-put-01 | ⊦ okbytearray(r, st) ∧ okbytearray(r0, st) ∧ 0 ≤ j ∧ j < st[r0 -- _length] .intval → okbytearray(r, st[r -- i ', st[r0 -- j ']]) | A User Theorem |
| okbar-put-byte-01 | ⊦ okbytearray(r1, st) ∧ okbytearray(r, st) → okbytearray(r, st[r1 -- i ', byteval(by)]) | A User Theorem |
| okbar-put-byte-same | ⊦ okbytearray(r, st) → okbytearray(r, st[r -- i ', byteval(by)]) | A User Theorem |
| okbar-putbar | ⊦ r ≠ r1 ∧ ¬ okarray(r, byte_type, putByteArray(bytes, r1, i, st)) → ¬ okarray(r, byte_type, st) | A User Theorem |
| okbar-putbar-01 | ⊦ r ≠ r1 ∧ ¬ okbytearray(r, putByteArray(bytes, r1, i, st)) → ¬ okbytearray(r, st) | A User Theorem |
| okbar-putbar-02 | ⊦ r ≠ r1 ∧ okbytearray(r, st) → okbytearray(r, putByteArray(bytes, r1, i, st)) | A User Theorem |
| okbar-putbar-03 | ⊦ r ≠ r1 ∧ okarray(r, byte_type, st) → okarray(r, byte_type, putByteArray(bytes, r1, i, st)) | A User Theorem |
| okbar-putbar-04 | ⊦ okbytearray(r, st) → okbytearray(r, putByteArray(bytes, r1, st)) | A User Theorem |
| okbar-putbar-05 | ⊦ okbytearray(r, st) → okbytearray(r, putByteArray(bytes, r1, i, st)) | A User Theorem |
| okbar-putbar-same | ⊦ okbytearray(r, st) → okbytearray(r, putByteArray(bytes, r, i, st)) | A User Theorem |
| okbytearray | ⊦ okarray(r, byte_type, st) ∧ i + j ≤ st[r -- _length] .intval ∧ 0 ≤ i ∧ ¬ is_bytevalue(val) → ¬ val ∈ getarray(r, i, j, st) | A User Theorem |
| okbytearray-02 | ⊦ ¬ okarray(r, byte_type, st) → ¬ okbytearray(r, st) | A User Theorem |
| okbytearray-bad-type | ⊦ st[r -- _type] .type ≠ mkarraytype(byte_type) → ¬ okbytearray(r, st) | A User Theorem |
| okbytearray-byteval | ⊦ ¬ is_bytevalue(st[r -- i ']) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ okbytearray(r, st) | A User Theorem |
| okbytearray-getarray-length | ⊦ okbytearray(r, st) → n→i(# getbytearray(r, st)) = st[r -- _length] .intval | A User Theorem |
| okbytearray-index-in | ⊦ ¬ r -- i ' ∈ st ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ okbytearray(r, st) | A User Theorem |
| okbytearray-index-in-zero | ⊦ ¬ r -- 0 ' ∈ st ∧ okbytearray(r, st) → st[r -- _length] .intval = 0 | A User Theorem |
| okbytearray-is-byte | ⊦ okbytearray(st[r -- sks] .refval, st) ∧ 0 ≤ i ∧ i < st[r -- (sks + _length ')] .intval ∧ sks ≠ [] → is_bytevalue(st[r -- (sks + i ' ')]) | A User Theorem |
| okbytearray-isarray | ⊦ okbytearray(r, st) → is_array(r, st) | A User Theorem |
| okbytearray-isarrayref | ⊦ okbytearray(r, st) → is_arrayref(r, st[r -- _length] .intval, st) | A User Theorem |
| okbytearray-length-zero | ⊦ okbytearray(r, st) → (st[r -- _length] .intval ≤ 0 ↔ st[r -- _length] .intval = 0) | A User Theorem |
| okbytearray-not | ⊦ is_referencevalue(st[r -- i ']) ∧ 0 ≤ i ∧ i < st[r -- _length] .intval → ¬ okbytearray(r, st) | A User Theorem |
| okbytearray-put-byteval | ⊦ okbytearray(r, st) ∧ ¬ r0 -- _length ∈ rkvs → (okbytearray(r, st[((r0 -- i ') × byteval(by)) ' + rkvs]) ↔ okbytearray(r, st[rkvs])) | A User Theorem |
| okbytearray-put-byteval-01 | ⊦ okbytearray(r, st) → (¬ okbytearray(r, st[r0 -- i ', byteval(by)]) ↔ false) | A User Theorem |
| okbytearray-put-byteval-equiv | ⊦ i < 0 ∨ ¬ i < st[r -- _length] .intval ∨ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ r -- i ' ∈ st ∧ is_bytevalue(st[r -- i ']) → (okbytearray(r, st[r -- i ', byteval(by)]) ↔ okbytearray(r, st)) | A User Theorem |
| okbytearray-put-field | ⊦ fs ' ≠ _length ∧ fs ' ≠ _type → (okbytearray(r, st[r0 -- fs ', val]) ↔ okbytearray(r, st)) | A User Theorem |
| okbytearray-put-field-01 | str ≠ `*Array*', str ≠ `java.lang.Object' ⊦ okbytearray(r, st[r0 -- mkfs(((* str)) .class, ty, fieldvar) ', val]) ↔ okbytearray(r, st) | A User Theorem |
| okbytearray-put-field-02 | str ≠ `length', str ≠ `type' ⊦ okbytearray(r, st[r0 -- mkfs(class, ty, ((* str)) .field) ', val]) ↔ okbytearray(r, st) | A User Theorem |
| okbytearray-put-field-03 | ⊦ fs ' ≠ _length ∧ fs ' ≠ _type → (okbytearray(r, st[((r0 -- fs ') × val) ' + rkvs]) ↔ okbytearray(r, st[rkvs])) | A User Theorem |
| okbytearray-put-field-04 | ⊦ sk .fs ' ≠ _length ∧ sk .fs ' ≠ _type ∧ is_fskey(sk) → (okbytearray(r, st[r0 -- sk, val]) ↔ okbytearray(r, st)) | A User Theorem |
| okbytearray-subset | ⊦ okbytearray(r, st) ∧ st ⊆ st0 → okbytearray(r, st0) | A User Theorem |
| okbytearray-type | ⊦ okbytearray(r, st) → st[r -- _type] = typeval(mkarraytype(byte_type)) | A User Theorem |
| okbytearray-type-01 | ⊦ ¬ r -- _type ∈ st → ¬ okbytearray(r, st) | A User Theorem |
| okclass-01 | ⊦ okclass(refval(jvmref), class1, st) | A User Theorem |
| okclass-02 | ⊦ classof(r, class1, st) → okclass(refval(r), class1, st) | A User Theorem |
| okclass-03 | ⊦ sk ≠ _type → (okclass(val, class1, st[r0 -- sk, val0]) ↔ okclass(val, class1, st)) | A User Theorem |
| okclass-copy | ⊦ okclass(refval(r), class1, arraycopy(r1, i, r0, i0, j, st)) ↔ okclass(refval(r), class1, st) | A User Theorem |
| okclass-int | ⊦ r0 ∈ st → (okclass(refval(r0), class1, st[r -- i ', val0]) ↔ okclass(refval(r0), class1, st)) | A User Theorem |
| okclass-out | ⊦ okclass(val, class1, st[_out, val0]) ↔ okclass(val, class1, st) | A User Theorem |
| okprim-oktype | ⊦ okprimtype(val, ty) → oktype(val, ty, st) | A User Theorem |
| okreftype-02 | ⊦ okreftype(val, ty, st) → is_referencevalue(val) | A User Theorem |
| okreftype-istypeval | ⊦ r ≠ jvmref ∧ okreftype(refval(r), mkclasstype(class), st) → is_typevalue(st[r -- _type]) | A User Theorem |
| okreftype-notin | ⊦ ¬ r ∈ st → (okreftype(refval(r), ty, st) ↔ r = jvmref) | A User Theorem |
| okreftype-null | ⊦ okreftype(refval(jvmref), ty, st) | A User Theorem |
| okreftype-put | ⊦ r ≠ r1 → (okreftype(refval(r1), ty, st[r -- sk, val]) ↔ okreftype(refval(r1), ty, st)) | A User Theorem |
| okreftype-subset | ⊦ okreftype(refval(r), ty, st) ∧ st ⊆ st0 → okreftype(refval(r), ty, st0) | A User Theorem |
| okreftype-subset-01 | ⊦ st ⊆ st1 ∧ okreftype(val, ty, st) → okreftype(val, ty, st1) | A User Theorem |
| okreftype-union | ⊦ okreftype(refval(r), ty, st) → okreftype(refval(r), ty, st0 ∪ st) | A User Theorem |
| okstore-01 | r -- sk ≠ _out, r -- sk ≠ _mode, sk ≠ _type ⊦ okstore(st[r -- sk, val]) → okstore(st) | A User Theorem |
| okstore-02 | ⊦ okstore(st[r -- sk, val]) ∧ r ≠ jvmref → r -- _type ∈ st[r -- sk, val] ∧ is_typevalue(st[r -- sk, val][r -- _type]) | A User Theorem |
| okstore-03 | ⊦ okstore(st) ∧ r ≠ jvmref → (okstore(st[r -- sk, val]) ↔ ¬ ¬ (r -- _type ∈ st[r -- sk, val] ∧ is_typevalue(st[r -- sk, val][r -- _type]))) | A User Theorem |
| okstore-04 | ⊦ st[r -- _type] .type = ty ∧ okstore(st) ∧ r ∈ st ∧ r ≠ jvmref → is_typevalue(st[r -- _type]) | A User Theorem |
| okstore-05 | ⊦ st[r -- _type] .type = ty ∧ okstore(st) ∧ r ∈ st ∧ r ≠ jvmref → r -- _type ∈ st | A User Theorem |
| okstore-06 | ⊦ st[r -- _type] = val ∧ okstore(st) ∧ r ∈ st ∧ r ≠ jvmref → is_typevalue(st[r -- _type]) | A User Theorem |
| okstore-07 | ⊦ st[r -- _type] = val ∧ okstore(st) ∧ r ∈ st ∧ r ≠ jvmref → r -- _type ∈ st | A User Theorem |
| okstore-08 | ⊦ okstore(st) → jvmref ∈ st | A User Theorem |
| okstore-09 | ⊦ okstore(st) → _mode ∈ st | A User Theorem |
| okstore-10 | ⊦ okstore(st) → _out ∈ st | A User Theorem |
| okstore-11 | ⊦ r ∈ st ∧ okstore(st) ∧ r ≠ jvmref → r -- _type ∈ st | A User Theorem |
| okstore-jvmref | ⊦ okstore(st) → okstore(st[jvmref -- sk, val]) | A User Theorem |
| okstore-mode | ⊦ okstore(st) → okstore(st[_mode, val]) | A User Theorem |
| okstore-other | ⊦ r -- sk ≠ _mode ∧ r -- sk ≠ _out ∧ r ∈ st ∧ sk ≠ _type → (okstore(st[r -- sk, val]) ↔ okstore(st)) | A User Theorem |
| okstore-out | ⊦ okstore(st) → okstore(st[_out, val]) | A User Theorem |
| oktype | ⊦ sk0 ≠ _type → (oktype(val, ty, st[r -- sk0, val0]) ↔ oktype(val, ty, st)) | A User Theorem |
| oktype-01 | ⊦ ty0 ≠ void_type → (oktype(val, ty, st[r -- mkfs(class1, ty0, fieldvar0) ', val0]) ↔ oktype(val, ty, st)) | A User Theorem |
| oktype-02 | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (oktype(val, ty, st[r0 -- sk, val0]) ↔ oktype(val, ty, st)) | A User Theorem |
| oktype-03 | ⊦ oktype(initial_value(ty), ty, st) ↔ ty ≠ abstract_type | A User Theorem |
| oktype-04 | ⊦ oktype(val, ty, arraycopy(r, i, r0, i0, j, st)) ↔ oktype(val, ty, st) | A User Theorem |
| oktype-del | ⊦ oktype(val, ty, st -- r) ↔ oktype(val, ty, st) | A User Theorem |
| oktype-new | ⊦ val .refval ≠ r → (oktype(val, ty, st[r -- sk, val0]) ↔ oktype(val, ty, st)) | A User Theorem |
| oktype-okval | ⊦ oktype(val, ty, st) ↔ okval(val, ty) | A User Theorem |
| oktype-out | ⊦ oktype(val, ty, st[_out, val0]) ↔ oktype(val, ty, st) | A User Theorem |
| oktype-put-other | ⊦ oktype(val0, ty, st[r1 -- sk, val]) ↔ oktype(val0, ty, st) | A User Theorem |
| oktype-reftype | ⊦ is_reftype(ty) → (oktype(val, ty, st) ↔ is_referencevalue(val)) | A User Theorem |
| oktype-refval | ⊦ oktype(refval(r), ty, st) ↔ is_reftype(ty) ∨ ty = void_type | A User Theorem |
| oktype-rew | ⊦ oktype(val, ty, st) ↔ oktype(val, ty, st0) | A User Theorem |
| oktype-st | ⊦ ¬ oktype(val, ty, st0) → ¬ oktype(val, ty, st1) | A User Theorem |
| okval-oktype | ⊦ okval(val, ty) → oktype(val, ty, st) | A User Theorem |
| onlymod-is-update | ⊦ onlyModified(r, st0, st1) ↔ (∃ fis. st1 = update(r, fis, st0) ∧ validFields(r, fis, st0)) | A User Theorem |
| short-length | ⊦ st[r -- _length] .intval ≤ 32767 ∧ okarray(r, ty, st) → s2i(i2s(st[r -- _length] .intval)) = st[r -- _length] .intval | A User Theorem |
| short-length-01 | ⊦ st[r -- _length] .intval ≤ 32767 ∧ exactarray(r, ty, st) → s2i(i2s(st[r -- _length] .intval)) = st[r -- _length] .intval | A User Theorem |
| subset-exactarray | ⊦ st ⊆ st0 ∧ exactarray(r, ty, st) → exactarray(r, ty, st0) | A User Theorem |
| subset-len | ⊦ st[r -- _length] .intval = i ∧ st ⊆ st0 ∧ okarray(r, ty, st) → st0[r -- _length] .intval = i | A User Theorem |
| subset-len-01 | ⊦ st[r -- _length] .intval = i ∧ st ⊆ st0 ∧ exactarray(r, ty, st) → st0[r -- _length] .intval = i | A User Theorem |
| subset-okarray | ⊦ st ⊆ st0 ∧ okarray(r, ty, st) → okarray(r, ty, st0) | A User Theorem |
| subset-oktype | ⊦ oktype(val, ty, st) ∧ st ⊆ st0 → oktype(val, ty, st0) | A User Theorem |
| union-okarray | ⊦ okarray(r, ty, st) → okarray(r, ty, st0 ∪ st) | A User Theorem |
| update-at | ⊦ r ≠ r0 → (update(r0, fis, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| update-at-01 | ⊦ rk .ref ≠ r0 → (update(r0, fis, st)[rk]) = st[rk] | A User Theorem |
| update-at-notin | ⊦ ¬ sk ∈ fis → (update(r, fis, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| update-atin | ⊦ sk ∈ fis → (update(r, fis, st)[r -- sk]) = fis[sk] | A User Theorem |
| update-ex-nodups | ⊦ ∃ fis0. ¬ dups(fis0 .keys) ∧ update(r, fis, st) = update(r, fis0, st) ∧ fis0 ⊆ fis | A User Theorem |
| update-in | ⊦ r ≠ r0 → (r -- sk ∈ update(r0, fis, st) ↔ r -- sk ∈ st) | A User Theorem |
| update-in-01 | ⊦ r ≠ r0 → (r ∈ update(r0, fis, st) ↔ r ∈ st) | A User Theorem |
| update-in-02 | ⊦ r ∈ st → r ∈ update(r0, fis, st) | A User Theorem |
| update-in-03 | ⊦ r ∈ update(r0, fis, st) ↔ r ∈ st ∨ r = r0 ∧ fis ≠ [] | A User Theorem |
| update-init | ⊦ r ≠ jvmref → (initdone(class, update(r, fis, st)) ↔ initdone(class, st)) | A User Theorem |
| update-init-01 | ⊦ r ≠ jvmref → (initundone(class, update(r, fis, st)) ↔ initundone(class, st)) | A User Theorem |
| update-keyin | ⊦ ¬ sk ∈ fis → (r0 -- sk ∈ update(r, fis, st) ↔ r0 -- sk ∈ st) | A User Theorem |
| update-keyin-01 | ⊦ r -- sk ∈ update(r0, fis, st) ↔ r -- sk ∈ st ∨ r = r0 ∧ sk ∈ fis | A User Theorem |
| update-length | ⊦ validFields(r, fis, st) → (update(r, fis, st)[r0 -- _length]) = st[r0 -- _length] | A User Theorem |
| update-mode | ⊦ r ≠ jvmref → (update(r, fis, st)[_mode]) = st[_mode] | A User Theorem |
| update-newref | ⊦ r ≠ r0 → (newref(r, update(r0, fis, st)) ↔ newref(r, st)) | A User Theorem |
| update-one | ⊦ update(r, (sk × val) ', st) = st[r -- sk, val] | A User Theorem |
| update-put | ⊦ r ≠ r0 → (update(r0, fis, st)[r -- sk, val]) = update(r0, fis, st[r -- sk, val]) | A User Theorem |
| update-put-notin | ⊦ ¬ sk ∈ fis → (update(r0, fis, st)[r -- sk, val]) = update(r0, fis, st[r -- sk, val]) | A User Theorem |
| update-put-rew | ⊦ ¬ sk ∈ fis → update(r, fis, st[r -- sk, val]) = (update(r, fis, st)[r -- sk, val]) | A User Theorem |
| update-put-same | ⊦ sk ∈ fis → update(r, fis, st[r -- sk, val]) = update(r, fis, st) | A User Theorem |
| update-putfis-sw | ⊦ update(r, fis[sk, val], st) = (update(r, fis, st)[r -- sk, val]) | A User Theorem |
| update-rec-01 | ⊦ update(r, fv ' + fis, st) = (update(r, fis, st)[r -- fv .1, fv .2]) | A User Theorem |
| update-rec-02 | ⊦ fis ≠ [] → update(r, fis, st) = (update(r, fis .rest, st)[r -- fis .first .1, fis .first .2]) | A User Theorem |
| update-refs | ⊦ r ∈ st → update(r, fis, st) .refs = st .refs | A User Theorem |
| update-type | ⊦ validFields(r, fis, st) → (update(r, fis, st)[r0 -- _type]) = st[r0 -- _type] | A User Theorem |
| update-type-01 | ⊦ validFields(r, fis, st) → (r0 -- _type ∈ update(r, fis, st) ↔ r0 -- _type ∈ st) | A User Theorem |
| update-union-switch | ⊦ ¬ r ∈ st .refs → update(r, fis, st ∪ st0) = st ∪ update(r, fis, st0) | A User Theorem |
| validFields-del | ⊦ ¬ validFields(r, fis, st) → ¬ validFields(r, fis, st -- rk) | A User Theorem |
| validFields-empty | ⊦ validFields(r, [], st) | A User Theorem |
| validFields-empty-01 | ⊦ validFields(r, fis, ∅) ↔ fis = [] | A User Theorem |
| validFields-fis | ⊦ r -- fv .1 ∈ st ∧ fv .1 ≠ _type ∧ fv .1 ≠ _length ∧ ¬ fv .1 ∈ fis → (validFields(r, fis + fv ', st) ↔ validFields(r, fis, st)) | A User Theorem |
| validFields-put | ⊦ rk ∈ st → (validFields(r, fis, st[rk, val]) ↔ validFields(r, fis, st)) | A User Theorem |
| validFields-put-01 | ⊦ ¬ sk ∈ fis → (validFields(r, fis, st[r -- sk, val]) ↔ validFields(r, fis, st)) | A User Theorem |
| validFields-putfis | ⊦ validFields(r, fis[sk, val], st) ↔ validFields(r, fis, st) ∧ sk ≠ _length ∧ sk ≠ _type ∧ r -- sk ∈ st | A User Theorem |
| validFields-rec | ⊦ validFields(r, (sk × val) ' + fis, st) ↔ validFields(r, fis, st) ∧ sk ≠ _length ∧ sk ≠ _type ∧ r -- sk ∈ st ∧ ¬ sk ∈ fis | A User Theorem |
| validFields-type | ⊦ _type ∈ fis → ¬ validFields(r, fis, st) | A User Theorem |
| vals-at | ⊦ n < # fis → (fis .vals)[n] = fis[n] .2 | A User Theorem |
| vals-at-in | ⊦ sk ∈ fis → fis[sk] ∈ fis .vals | A User Theorem |
| vals-at-in-01 | ⊦ sk ∈ fis ∧ fis[sk] = val → val ∈ fis .vals | A User Theorem |
| vals-in | ⊦ val ∈ fis .vals ↔ (∃ sk. sk × val ∈ fis) | A User Theorem |
| vals-length | ⊦ # fis .vals = # fis | A User Theorem |
| vals-one | ⊦ (sk × val) ' .vals = val ' | A User Theorem |