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: |
|---|---|---|
| addarray-def | ⊦ addarray(r, ty, i, st) = addarray(r, initial_value(ty), i, st[r -- _type, typeval(mkarraytype(ty))][r -- _length, intval(i)]) | An Axiom |
| addarray-base | ⊦ i ≤ 0 → addarray(r, val, i, st) = st | An Axiom |
| addarray-rec | ⊦ i > 0 → addarray(r, val, i, st) = (addarray(r, val, i - 1, st)[r -- (i - 1) ', val]) | An Axiom |
| addarrayinit-def | ⊦ addarray(r, ty, vals, st) = addarray(r, vals, 0, st[r -- _type, typeval(mkarraytype(ty))][r -- _length, intval(n→i(# vals))]) | An Axiom |
| addarrayinit-base | ⊦ addarray(r, [], i, st) = st | An Axiom |
| addarrayinit-rec | ⊦ addarray(r, val ' + vals, i, st) = (addarray(r, vals, i + 1, st)[r -- i ', val]) | An Axiom |
| addbytearray | ⊦ addarray(r, ty, bytes, st) = addarray(r, ty, mkjavavalues(bytes), st) | An Axiom |
| addbytearray-ints | ⊦ addbytearray(r, ints, st) = addarray(r, byte_type, mkjavavalues(is2bs(ints)), st) | An Axiom |
| 1dim | ⊦ addarray(r, val, 0, st) = st | A User Theorem |
| 1dim-01 | ⊦ 0 ≤ i → addarray(r, val, i + 1, st) = (addarray(r, val, i, st)[r -- i ', val]) | A User Theorem |
| add-at | ⊦ rk .ref ≠ r → (addarray(r, val, i, st)[rk]) = st[rk] | A User Theorem |
| add-at-01 | ⊦ rk .ref ≠ r → (addarray(r, ty, vals, st)[rk]) = st[rk] | A User Theorem |
| add-at-02 | ⊦ rk .ref ≠ r → (addarray(r, ty, i, st)[rk]) = st[rk] | A User Theorem |
| add-at-03 | ⊦ rk .ref ≠ r → (addarray(r, vals, i, st)[rk]) = st[rk] | A User Theorem |
| add-at-04 | ⊦ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type → (addarray(r, ty, vals, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| add-at-05 | ⊦ is_fskey(sk) → (addarray(r, val, i, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| add-at-gr | ⊦ n→i(# vals) ≤ i → (addarray(r, ty, vals, st)[r -- i ']) = st[r -- i '] | A User Theorem |
| add-at-neg | ⊦ i < 0 → (addarray(r, ty, vals, st)[r -- i ']) = st[r -- i '] | A User Theorem |
| add-at-ok | ⊦ 0 ≤ i ∧ i < n→i(# vals) → (addarray(r, ty, vals, st)[r -- i ']) = vals[i→n(i)] | A User Theorem |
| add-at-ok-01 | 0 ≤ i, i < n→i(# vals) ⊦ (addarray(r, ty, vals, st)[r -- ((* i)) ']) = vals[i→n(i)] | A User Theorem |
| add-at-other | ⊦ r ≠ r0 ∨ r = r0 ∧ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type ∨ r = r0 ∧ is_indexkey(sk) ∧ (sk .index < 0 ∨ n→i(# vals) ≤ sk .index) → (addarray(r, ty, vals, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| add-at-other-index | ⊦ i < 0 ∨ n→i(# vals) ≤ i → (addarray(r, ty, vals, st)[r -- i ']) = st[r -- i '] | A User Theorem |
| add-gft | ⊦ r ≠ r0 → (goodfieldandtype(r0, sk, addarray(r, ty, vals, st)) ↔ goodfieldandtype(r0, sk, st)) | A User Theorem |
| add-in | ⊦ r -- _type ∈ addarray(r, ty, vals, st) | A User Theorem |
| add-in-fskey | ⊦ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type → (r -- sk ∈ addarray(r, ty, vals, st) ↔ r -- sk ∈ st) | A User Theorem |
| add-in-other | ⊦ r ≠ r0 ∨ r = r0 ∧ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type ∨ r = r0 ∧ is_indexkey(sk) ∧ (sk .index < 0 ∨ n→i(# vals) ≤ sk .index) → (r0 -- sk ∈ addarray(r, ty, vals, st) ↔ r0 -- sk ∈ st) | A User Theorem |
| add-in-other-index | ⊦ i < 0 ∨ n→i(# vals) ≤ i → (r -- i ' ∈ addarray(r, ty, vals, st) ↔ r -- i ' ∈ st) | A User Theorem |
| add-init | ⊦ initerror(class, addarray(r, ty, i, st)) ↔ initerror(class, st) | A User Theorem |
| add-isobj | ⊦ r ≠ r0 → (is_obj(r0, class, sks, addarray(r, ty, vals, st)) ↔ is_obj(r0, class, sks, st)) | A User Theorem |
| add-lastrec | ⊦ vals ≠ [] → addarray(r, ty, vals, st) = (addarray(r, ty, vals .butlast, st)[r -- n→i((# vals) -1) ', vals .last][r -- _length, intval(n→i(# vals))]) | A User Theorem |
| add-okarray | ⊦ r ≠ val .refval → (okarray(val, ty0, i, addarray(r, ty, vals, st)) ↔ okarray(val, ty0, i, st)) | A User Theorem |
| add-put-switch | ⊦ is_fskey(sk) ∨ r ≠ r0 → addarray(r, val, i, st[r0 -- sk, val0]) = (addarray(r, val, i, st)[r0 -- sk, val0]) | A User Theorem |
| add-refs | ⊦ addarray(r, ty, vals, st) .refs = st .refs ++ r | A User Theorem |
| addarray-addaray | ⊦ 0 ≤ i → addarray(r, ty, i, st) = addarray(r, ty, mklist(initial_value(ty), i→n(i)), st) | A User Theorem |
| addarray-at-newref | ⊦ newref(r, st) ∧ r0 ∈ st → (addarray(r, ty, vals, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| addarray-at-other | m < n ⊦ ¬ r ∈ refs ∧ # refs = ((* n)) → (addarray(r, ty, vals, st)[refs[(* m)] -- sk]) = st[refs[m] -- sk] | A User Theorem |
| addarray-both-subset | ⊦ ¬ addarray(r, byte_type, vals, st0) ⊆ addarray(r, byte_type, vals, st1) → ¬ st0 ⊆ st1 | A User Theorem |
| addarray-both-subset-01 | ⊦ st0 ⊆ st1 → addarray(r, byte_type, vals, st0) ⊆ addarray(r, byte_type, vals, st1) | A User Theorem |
| addarray-getintarray-other | ⊦ r ≠ r0 → getintarray(r, addarray(r0, ty, i0, st)) = getintarray(r, st) | A User Theorem |
| addarray-getintarray-other-01 | ⊦ r ≠ r0 → getintarray(r, i, j, addarray(r0, ty, i0, st)) = getintarray(r, i, j, st) | A User Theorem |
| addarray-identity | ⊦ is_array(r, st) ∧ st[r -- _type] .type = mkarraytype(ty) ∧ getarray(r, st) = vals → addarray(r, ty, vals, st) = st | A User Theorem |
| addarray-init | ⊦ init(addarray(r, ty, vals, st)) ↔ init(st) | A User Theorem |
| addarray-init-01 | ⊦ init(addarray(r, ty, i, st)) ↔ init(st) | A User Theorem |
| addarray-init-02 | ⊦ init(str, addarray(r, ty, i, st)) ↔ init(str, st) | A User Theorem |
| addarray-is-putarray | ⊦ 0 ≤ i → addarray(r, val, i, st) = putArray(mklist(val, i→n(i)), r, 0, st) | A User Theorem |
| addarray-is-putarray-01 | ⊦ addarray(r, vals, i, st) = putArray(vals, r, i, st) | A User Theorem |
| addarray-lastrec | ⊦ vals ≠ [] → addarray(r, vals, i, st) = (addarray(r, vals .butlast, i, st)[r -- (i + n→i(# vals) - 1) ', vals .last]) | A User Theorem |
| addarray-length-in | ⊦ r -- _length ∈ addarray(r0, ty, vals, st) ↔ r = r0 ∨ r -- _length ∈ st | A User Theorem |
| addarray-mklist | ⊦ 0 ≤ j → addarray(r, mklist(initial_value(byte_type), i→n(j)), 0, st) = addarray(r, initial_value(byte_type), j, st) | A User Theorem |
| addarray-mklist-01 | ⊦ 0 ≤ i ∧ 0 ≤ j → addarray(r, mklist(initial_value(byte_type), i→n(j)), i, addarray(r, mklist(initial_value(byte_type), i→n(i)), 0, st)) = addarray(r, initial_value(byte_type), j + i, st) | A User Theorem |
| addarray-mklist-02 | ⊦ addarray(r, mklist(val, n), 0, st) = addarray(r, val, n→i(n), st) | A User Theorem |
| addarray-mklist-03 | ⊦ addarray(r, mklist(val, n), n→i(m), addarray(r, mklist(val, m), 0, st)) = addarray(r, val, n→i(n) + n→i(m), st) | A User Theorem |
| addarray-mklist-04 | ⊦ 0 ≤ i → addarray(r, mklist(val, n), i, addarray(r, mklist(val, i→n(i)), 0, st)) = addarray(r, val, n→i(n) + i, st) | A User Theorem |
| addarray-mklist-05 | ⊦ addarray(r, ty, mklist(initial_value(ty), n), st) = (addarray(r, initial_value(ty), n→i(n), st)[r -- _type, typeval(mkarraytype(ty))][r -- _length, intval(n→i(n))]) | A User Theorem |
| addarray-mode | ⊦ r ≠ jvmref → (_mode ∈ addarray(r, ty, vals, st) ↔ _mode ∈ st) | A User Theorem |
| addarray-negative | ⊦ i < 0 → ¬ is_array(r, addarray(r, ty, i, st)) | A User Theorem |
| addarray-nouninit | ⊦ nouninit(claset, addarray(r, ty, i, st)) ↔ nouninit(claset, st) | A User Theorem |
| addarray-nouninit-01 | ⊦ nouninit(claset, addarray(r, ty, vals, st)) ↔ nouninit(claset, st) | A User Theorem |
| addarray-put | ⊦ rk .ref ≠ r → addarray(r, ty, vals, st[rk, val]) = (addarray(r, ty, vals, st)[rk, val]) | A User Theorem |
| addarray-put-01 | ⊦ 0 ≤ i ∧ 0 ≤ j ∧ j < i → (addarray(r, ty, i, st)[r -- j ', val]) = addarray(r, ty, ((j = 0 ⊃ []; mklist(initial_value(ty), i→n(j)))) + (val + mklist(initial_value(ty), i→n(i - j + 1))), st) | A User Theorem |
| addarray-refs | ⊦ addarray(r, ty, i, st) .refs = st .refs ++ r | A User Theorem |
| addarray-subset | ⊦ newref(r, st) → (¬ st ⊆ addarray(r, ty, vals, st) ↔ false) | A User Theorem |
| addbar-addobj-switch | ⊦ r ≠ r0 → addbytearray(r, ints, addobj(r0, class, fis, st)) = addobj(r0, class, fis, addbytearray(r, ints, st)) | A User Theorem |
| addbar-addobj-switch-01 | ⊦ r ≠ r0 → addobj(r0, class, fis, addbytearray(r, ints, st)) = addbytearray(r, ints, addobj(r0, class, fis, st)) | A User Theorem |
| addbar-get | ⊦ r ≠ r0 → (addbytearray(r0, ints, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| addbar-in | ⊦ r ≠ r0 → (r -- sk ∈ addbytearray(r0, ints, st) ↔ r -- sk ∈ st) | A User Theorem |
| addbar-in-01 | ⊦ r ∈ addbytearray(r0, ints, st) ↔ r = r0 ∨ r ∈ st | A User Theorem |
| addbar-init | ⊦ initdone(class, addbytearray(r, ints, st)) ↔ initdone(class, st) | A User Theorem |
| addbar-init-01 | ⊦ initundone(class, addbytearray(r, ints, st)) ↔ initundone(class, st) | A User Theorem |
| addbar-length | ⊦ (addbytearray(r, ints, st)[r -- _length]) = intval(n→i(# ints)) | A User Theorem |
| addbar-length-01 | ⊦ r -- _length ∈ addbytearray(r, ints, st) | A User Theorem |
| addbar-mode | ⊦ (addbytearray(r, ints, st)[_mode]) = st[_mode] | A User Theorem |
| addbar-newref | ⊦ newref(r, addbytearray(r0, ints, st)) ↔ r ≠ r0 ∧ newref(r, st) | A User Theorem |
| addbar-okarray | ⊦ r ≠ val .refval → (okarray(val, ty0, i, addbytearray(r, ints, st)) ↔ okarray(val, ty0, i, st)) | A User Theorem |
| addbar-okarray-01 | ⊦ i = n→i(# ints) ∧ r ≠ jvmref → okarray(refval(r), byte_type, i, addbytearray(r, ints, st)) | A User Theorem |
| addbar-okarray-02 | ⊦ r ≠ r0 → (okarray(refval(r0), ty0, i, addbytearray(r, ints, st)) ↔ okarray(refval(r0), ty0, i, st)) | A User Theorem |
| addbar-okarray-03 | ⊦ r ≠ jvmref → (okarray(refval(r), byte_type, i, addbytearray(r, ints, st)) ↔ i = n→i(# ints)) | A User Theorem |
| addbar-putrew | ⊦ r ≠ r0 → (addbytearray(r, ints, st)[r0 -- sk, val]) = addbytearray(r, ints, st[r0 -- sk, val]) | A User Theorem |
| addbar-refs | ⊦ addbytearray(r, ints, st) .refs = st .refs ++ r | A User Theorem |
| addbar-refval | ⊦ 0 ≤ i ∧ i < n→i(# ints) → ¬ is_referencevalue(addbytearray(r, ints, st)[r -- i ']) | A User Theorem |
| addbar-refval-01 | ⊦ 0 ≤ i ∧ i < n→i(# ints) → is_bytevalue(addbytearray(r, ints, st)[r -- i ']) | A User Theorem |
| addbar-type | ⊦ (addbytearray(r, ints, st)[r -- _type]) = typeval(mkarraytype(byte_type)) | A User Theorem |
| addbar-type-01 | ⊦ r -- _type ∈ addbytearray(r, ints, st) | A User Theorem |
| addbytearray-rew | ⊦ is_bytelist(vals) → addarray(r, byte_type, vals, st) = addbytearray(r, bs2is(bytevalues(vals)), st) | A User Theorem |
| addobj-addarray-switch | ⊦ r ≠ r0 → addobj(r, class, fis, addarray(r0, ty, vals, st)) = addarray(r0, ty, vals, addobj(r, class, fis, st)) | A User Theorem |
| at-1dim | ⊦ 0 ≤ j ∧ j < i → (addarray(r, ty, i, st)[r -- j ']) = initial_value(ty) | A User Theorem |
| at-1dim-01 | ⊦ 0 ≤ j ∧ j < i → (addarray(r, val, i, st)[r -- j ']) = val | A User Theorem |
| at-1dim-other | ⊦ r ≠ r0 ∨ r = r0 ∧ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type ∨ r = r0 ∧ is_indexkey(sk) ∧ (sk .index < 0 ∨ j ≤ sk .index) → (addarray(r, ty, j, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| at-1dim-other-index | ⊦ i < 0 ∨ j ≤ i → (addarray(r, ty, j, st)[r -- i ']) = st[r -- i '] | A User Theorem |
| at-1dim-other-index-01 | ⊦ i < 0 ∨ j ≤ i → (addarray(r, val, j, st)[r -- i ']) = st[r -- i '] | A User Theorem |
| at-field-1dim | ⊦ is_fskey(sk) ∧ sk ≠ _type ∧ sk ≠ _length → (addarray(r, ty, i, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| at-init | ⊦ is_fskey(sk) → (addarray(r, vals, j, st[r -- sk, val])[r -- i ']) = (addarray(r, vals, j, st)[r -- i ']) | A User Theorem |
| at-init-01 | ⊦ (addarray(r, vals, j, st[r -- _type, val])[r -- i ']) = (addarray(r, vals, j, st)[r -- i ']) | A User Theorem |
| at-init-02 | ⊦ (addarray(r, vals, j, st[r -- _length, val])[r -- i ']) = (addarray(r, vals, j, st)[r -- i ']) | A User Theorem |
| at-statfield | ⊦ r ≠ jvmref → (addarray(r, ty, vals, st)[sk]) = st[sk] | A User Theorem |
| at-statfield-01 | ⊦ newref(r, st) → (addarray(r, ty, vals, st)[sk]) = st[sk] | A User Theorem |
| atinit | ⊦ (addarray(r, ty, val ' + val0 ' + val1 ', st)[r -- 2 ']) = val1 | A User Theorem |
| atint20-1dim | ⊦ (addarray(r, int_type, 1 + 1, st)[r -- 0 ']) = intval(0) | A User Theorem |
| atint21-1dim | ⊦ (addarray(r, int_type, 1 + 1, st)[r -- 1 ']) = intval(0) | A User Theorem |
| atone-1dim | ⊦ (addarray(r, ty, 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1, st)[r -- 1 ']) = initial_value(ty) | A User Theorem |
| class-1dim | ⊦ r ≠ r0 → (classof(r0, class1, addarray(r, ty, i, st)) ↔ classof(r0, class1, st)) | A User Theorem |
| class-init | ⊦ r ≠ r0 → (classof(r0, class1, addarray(r, ty, vals, st)) ↔ classof(r0, class1, st)) | A User Theorem |
| endfinallymode | ⊦ (addarray(newref(st), ty, vals, st)[_endfinallymode]) = st[_endfinallymode] | A User Theorem |
| endfinallymode-01 | ⊦ (addarray(newref(st), ty, i, st)[_endfinallymode]) = st[_endfinallymode] | A User Theorem |
| get-add | ⊦ getbytearray(r, addarray(r, byte_type, vals, st)) = bytevalues(vals) | A User Theorem |
| get-add-01 | ⊦ getarray(r, 0, n→i(# vals), addarray(r, ty, vals, st)) = vals | A User Theorem |
| get-add-02 | ⊦ 0 ≤ i ∧ 0 ≤ j ∧ i + j ≤ n→i(# vals) → getarray(r, i, j, addarray(r, ty, vals, st)) = sublist(i→n(i), i→n(j), vals) | A User Theorem |
| getBar-2-put | ⊦ getbytearray(r, addarray(r, byte_type, 2, st)[r -- 0 ', byteval(by)][r -- 1 ', byteval(by0)]) = by ' + by0 ' | A User Theorem |
| getarray-addarray | ⊦ getarray(r, addarray(r, ty, vals, st)) = vals | A User Theorem |
| getarray-addarray-01 | ⊦ r ≠ r0 → getarray(r, addarray(r0, ty, vals, st)) = getarray(r, st) | A User Theorem |
| getarray-addarray-02 | ⊦ 0 ≤ i → getarray(r, 0, i, addarray(r, int_type, i, st)) = mklist(intval(0), i→n(i)) | A User Theorem |
| getarray-addarray-03 | ⊦ 0 ≤ i → getarray(r, 0, i, addarray(r, val, i, st)) = mklist(val, i→n(i)) | A User Theorem |
| getarray-addarray-04 | ⊦ 0 ≤ i ∧ i ≤ j → getarray(r, 0, i, addarray(r, int_type, j, st)) = mklist(intval(0), i→n(i)) | A User Theorem |
| getarray-addarray-05 | ⊦ 0 ≤ i ∧ i ≤ j → getarray(r, 0, i, addarray(r, val, j, st)) = mklist(val, i→n(i)) | A User Theorem |
| getarray-addarray-06 | ⊦ 0 ≤ i → getarray(r, addarray(r, ty, i, st)) = mklist(initial_value(ty), i→n(i)) | A User Theorem |
| getarray-addarray-other | ⊦ r ≠ r0 → getarray(r, i, j, addarray(r0, ty, i0, st)) = getarray(r, i, j, st) | A User Theorem |
| getarray-addarray-other-01 | ⊦ r ≠ r0 → getarray(r, i, j, addarray(r0, ty, vals, st)) = getarray(r, i, j, st) | A User Theorem |
| getbar-add | ⊦ r ≠ r0 → getbytearray(r, addarray(r0, ty, vals, st)) = getbytearray(r, st) | A User Theorem |
| getbar-add-01 | ⊦ r ≠ r0 → getbytearray(r, i, j, addarray(r0, ty, vals, st)) = getbytearray(r, i, j, st) | A User Theorem |
| getbar-add-02 | ⊦ r ≠ r0 → getbytearray(r, addarray(r0, ty, i, st)) = getbytearray(r, st) | A User Theorem |
| getbar-add-03 | ⊦ r ≠ r0 → getbytearray(r, i, j, addarray(r0, ty, i0, st)) = getbytearray(r, i, j, st) | A User Theorem |
| getbar-addbar | ⊦ r ≠ r0 → getbytearray(r, addbytearray(r0, ints, st)) = getbytearray(r, st) | A User Theorem |
| getbar-addbar-01 | ⊦ getbytearray(r, addbytearray(r, ints, st)) = is2bs(ints) | A User Theorem |
| getbar-addbar-02 | ⊦ 0 ≤ i ∧ 0 ≤ j ∧ i→n(i) + i→n(j) < # ints → getbytearray(r, i, j, addbytearray(r, ints, st)) = is2bs(sublist(i→n(i), i→n(j), ints)) | A User Theorem |
| getbytearray-addarray-this | ⊦ 0 ≤ i → getbytearray(r, addarray(r, byte_type, i, st)) = mklist(i2b(0), i→n(i)) | A User Theorem |
| getintarray-addarray | ⊦ 0 ≤ i → getintarray(r, 0, i, addarray(r, int_type, i, st)) = mklist(0, i→n(i)) | A User Theorem |
| getintarray-addarray-01 | ⊦ 0 ≤ i ∧ i ≤ j → getintarray(r, 0, i, addarray(r, int_type, j, st)) = mklist(0, i→n(i)) | A User Theorem |
| in-1dim | ⊦ r ≠ r0 → ((r -- sk) × val ∈ addarray(r0, ty, i, st) ↔ (r -- sk) × val ∈ st) | A User Theorem |
| in-1dim-01 | ⊦ r ≠ r0 → (r -- sk ∈ addarray(r0, ty, i, st) ↔ r -- sk ∈ st) | A User Theorem |
| in-1dim-02 | ⊦ r ≠ r0 → (r -- sk ∈ addarray(r0, val, i, st) ↔ r -- sk ∈ st) | A User Theorem |
| in-1dim-03 | ⊦ r ≠ r0 → (r ∈ addarray(r0, ty0, i, st) ↔ r ∈ st) | A User Theorem |
| in-1dim-04 | ⊦ r ≠ r0 → (r ∈ addarray(r0, val, i, st) ↔ r ∈ st) | A User Theorem |
| in-1dim-05 | ⊦ r ∈ addarray(r, ty0, i, st) | A User Theorem |
| in-1dim-06 | ⊦ r ∈ st → r ∈ addarray(r0, ty0, i, st) | A User Theorem |
| in-1dim-07 | ⊦ r -- fs ' ∈ addarray(r0, val, i, st) ↔ r -- fs ' ∈ st | A User Theorem |
| in-1dim-08 | ⊦ r -- _type ∈ addarray(r0, val, i, st) ↔ r -- _type ∈ st | A User Theorem |
| in-1dim-09 | ⊦ r ∈ st → r ∈ addarray(r0, val, i, st) | A User Theorem |
| in-1dim-10 | ⊦ r ∈ addarray(r, val, i, st) ↔ 0 < i ∨ r ∈ st | A User Theorem |
| in-1dim-11 | class1 ≠ `*Array*' .class, class1 ≠ `java.lang.Object' .class ⊦ r -- mkfs(class1, ty, fieldvar) ' ∈ addarray(r0, ty0, i, st) ↔ r -- mkfs(class1, ty, fieldvar) ' ∈ st | A User Theorem |
| in-1dim-12 | fs ' ≠ _type, fs ' ≠ _length ⊦ r -- fs ' ∈ addarray(r0, ty, i, st) ↔ r -- fs ' ∈ st | A User Theorem |
| in-1dim-13 | ⊦ rk ∈ st → rk ∈ addarray(r, val, i, st) | A User Theorem |
| in-1dim-14 | ⊦ rk ∈ st → rk ∈ addarray(r, ty, i, st) | A User Theorem |
| in-1dim-15 | ⊦ 0 ≤ j ∧ j < i → r -- j ' ∈ addarray(r, val, i, st) | A User Theorem |
| in-1dim-16 | ⊦ 0 ≤ j ∧ j < i → r -- j ' ∈ addarray(r, ty, i, st) | A User Theorem |
| in-1dim-17 | ⊦ is_fskey(sk) → (r -- sk ∈ addarray(r0, val, i, st) ↔ r -- sk ∈ st) | A User Theorem |
| in-1dim-fskey | ⊦ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type → (r -- sk ∈ addarray(r, ty, i, st) ↔ r -- sk ∈ st) | A User Theorem |
| in-1dim-other | ⊦ r ≠ r0 ∨ r = r0 ∧ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type ∨ r = r0 ∧ is_indexkey(sk) ∧ (sk .index < 0 ∨ j ≤ sk .index) → (r0 -- sk ∈ addarray(r, ty, j, st) ↔ r0 -- sk ∈ st) | A User Theorem |
| in-1dim-other-index | ⊦ i < 0 ∨ j ≤ i → (r -- i ' ∈ addarray(r, ty, j, st) ↔ r -- i ' ∈ st) | A User Theorem |
| in-1dim-other-index-01 | ⊦ i < 0 ∨ j ≤ i → (r -- i ' ∈ addarray(r, val, j, st) ↔ r -- i ' ∈ st) | A User Theorem |
| in-1init | ⊦ r ≠ r0 → (r ∈ addarray(r0, ty0, vals, st) ↔ r ∈ st) | A User Theorem |
| in-1init-01 | ⊦ r ≠ r0 → (r ∈ addarray(r0, vals, j, st) ↔ r ∈ st) | A User Theorem |
| in-1init-02 | ⊦ r ∈ addarray(r, ty0, vals, st) | A User Theorem |
| in-1init-03 | ⊦ r ∈ st → r ∈ addarray(r0, vals, j, st) | A User Theorem |
| in-1init-04 | ⊦ r ∈ st → r ∈ addarray(r0, ty0, vals, st) | A User Theorem |
| in-1init-05 | ⊦ r ∈ addarray(r, vals, j, st) ↔ vals ≠ [] ∨ r ∈ st | A User Theorem |
| in-1init-06 | ⊦ r ∈ addarray(r0, ty0, vals, st) ↔ r = r0 ∨ r ∈ st | A User Theorem |
| in-add | ⊦ r -- j ' ∈ addarray(r, ty, vals, st) ↔ r -- j ' ∈ st ∨ 0 ≤ j ∧ j < n→i(# vals) | A User Theorem |
| in-init | ⊦ r ≠ r0 → ((r -- sk) × val ∈ addarray(r0, ty, vals, st) ↔ (r -- sk) × val ∈ st) | A User Theorem |
| in-init-01 | ⊦ r ≠ r0 → (r -- sk ∈ addarray(r0, ty, vals, st) ↔ r -- sk ∈ st) | A User Theorem |
| in-init-02 | ⊦ r ≠ r0 → (r -- sk ∈ addarray(r0, vals, j, st) ↔ r -- sk ∈ st) | A User Theorem |
| in-init-03 | ⊦ r -- fs ' ∈ addarray(r0, vals, j, st) ↔ r -- fs ' ∈ st | A User Theorem |
| in-init-04 | ⊦ r -- _type ∈ addarray(r0, vals, j, st) ↔ r -- _type ∈ st | A User Theorem |
| in-init-05 | class1 ≠ `*Array*' .class, class1 ≠ `java.lang.Object' .class ⊦ r -- mkfs(class1, ty, fieldvar) ' ∈ addarray(r0, ty0, vals, st) ↔ r -- mkfs(class1, ty, fieldvar) ' ∈ st | A User Theorem |
| in-init-06 | fs ' ≠ _type, fs ' ≠ _length ⊦ r -- fs ' ∈ addarray(r0, ty, vals, st) ↔ r -- fs ' ∈ st | A User Theorem |
| in-init-08 | ⊦ rk ∈ st → rk ∈ addarray(r, vals, j, st) | A User Theorem |
| in-init-09 | ⊦ rk ∈ st → rk ∈ addarray(r, ty, vals, st) | A User Theorem |
| init-1dim | ⊦ initdone(class1, addarray(r, ty, i, st)) ↔ initdone(class1, st) | A User Theorem |
| init-1dim-01 | ⊦ initundone(class1, addarray(r, ty, i, st)) ↔ initundone(class1, st) | A User Theorem |
| init-1dim-02 | ⊦ initerror(class1, addarray(r, ty, i, st)) ↔ initerror(class1, st) | A User Theorem |
| init-1dim-03 | ⊦ initdone(class1, addarray(r, val, i, st)) ↔ initdone(class1, st) | A User Theorem |
| init-1dim-04 | ⊦ initundone(class1, addarray(r, val, i, st)) ↔ initundone(class1, st) | A User Theorem |
| init-1dim-05 | ⊦ initerror(class1, addarray(r, val, i, st)) ↔ initerror(class1, st) | A User Theorem |
| init-1init | ⊦ initdone(class1, addarray(r, vals, j, st)) ↔ initdone(class1, st) | A User Theorem |
| init-1init-01 | ⊦ initundone(class1, addarray(r, vals, j, st)) ↔ initundone(class1, st) | A User Theorem |
| init-1init-02 | ⊦ initerror(class1, addarray(r, vals, j, st)) ↔ initerror(class1, st) | A User Theorem |
| init-1init-03 | ⊦ initdone(class1, addarray(r, ty, vals, st)) ↔ initdone(class1, st) | A User Theorem |
| init-1init-04 | ⊦ initundone(class1, addarray(r, ty, vals, st)) ↔ initundone(class1, st) | A User Theorem |
| init-1init-05 | ⊦ initerror(class1, addarray(r, ty, vals, st)) ↔ initerror(class1, st) | A User Theorem |
| init-addarray | ⊦ init(str, addarray(r, ty, vals, st)) ↔ init(str, st) | A User Theorem |
| init-at | ⊦ 0 ≤ i ∧ i < n→i(# vals) → (addarray(r, vals, 0, st)[r -- i ']) = vals[i→n(i)] | A User Theorem |
| init-at-01 | ⊦ j ≤ i ∧ i < j + n→i(# vals) → (addarray(r, vals, j, st)[r -- i ']) = vals[i→n(i - j)] | A User Theorem |
| init-last | ⊦ addarray(r, vals + val ', i, st) = (addarray(r, vals, i, st)[r -- (i + n→i(# vals)) ', val]) | A User Theorem |
| init-switch | ⊦ is_fskey(sk) → addarray(r, vals, i, st[r0 -- sk, val]) = (addarray(r, vals, i, st)[r0 -- sk, val]) | A User Theorem |
| is_array-1dim | ⊦ r ≠ r0 → (is_arrayref(r, i, addarray(r0, ty0, i0, st)) ↔ is_arrayref(r, i, st)) | A User Theorem |
| is_array-1dim-01 | ⊦ r ≠ r0 → (is_arrayref(r, i, addarray(r0, val0, i0, st)) ↔ is_arrayref(r, i, st)) | A User Theorem |
| is_array-addarray | ⊦ is_array(str, r, addarray(r, ty, i, st)) ↔ ¬ ¬ (type∃(str, ty) ∧ 0 ≤ i ∧ r ≠ jvmref ∧ ty .jtelemtype ≠ void_type ∧ ty .jtelemtype ≠ abstract_type) | A User Theorem |
| is_array-addarray-01 | ⊦ ¬ is_referencevalue(val) ∧ val ∈ vals → ¬ is_array(str, r, addarray(r, mkclasstype(class), vals, st)) | A User Theorem |
| is_array-addarray-any | ⊦ ty .jtelemtype ≠ void_type ∧ ty .jtelemtype ≠ abstract_type ∧ type∃(str, ty) ∧ (∀ val. val ∈ vals → okval(val, ty)) ∧ r ≠ jvmref → is_array(str, r, addarray(r, ty, vals, st)) | A User Theorem |
| is_array-addarray-byte | ⊦ is_array(str, r, addarray(r, byte_type, mkjavavalues(bytes), st)) ↔ r ≠ jvmref | A User Theorem |
| is_array-addarray-prim | ⊦ is_primtype(ty) ∧ (∀ val. val ∈ vals → okprimtype(val, ty)) ∧ r ≠ jvmref → is_array(str, r, addarray(r, ty, vals, st)) | A User Theorem |
| is_array-init | ⊦ r ≠ r0 → (is_arrayref(r, i, addarray(r0, ty0, vals, st)) ↔ is_arrayref(r, i, st)) | A User Theorem |
| is_array-init-01 | ⊦ r ≠ r0 → (is_arrayref(r, i, addarray(r0, vals, j, st)) ↔ is_arrayref(r, i, st)) | A User Theorem |
| is_array-other-addarray | ⊦ r ≠ r0 → (is_array(str, r, addarray(r0, ty0, vals, st)) ↔ is_array(str, r, st)) | A User Theorem |
| is_obj-addarray | ⊦ r ≠ r0 → (is_obj(str, r, addarray(r0, ty0, vals, st)) ↔ is_obj(str, r, st)) | A User Theorem |
| is_obj-addarray-01 | ⊦ ¬ is_obj(str, r, addarray(r, ty, i, st)) | A User Theorem |
| is_obj-addarray-02 | ⊦ ¬ is_obj(str, r, addarray(r, ty, vals, st)) | A User Theorem |
| isarray-1dim | ⊦ is_arrayref(r, i, addarray(r, ty, i, st)) | A User Theorem |
| isarray-add | ⊦ r ≠ jvmref ∧ 0 ≤ i ∧ ty ≠ abstract_type → is_array(r, addarray(r, ty, i, st)) | A User Theorem |
| isarray-addarray | ⊦ (∀ j. 0 ≤ j ∧ j < n→i(# vals) → oktype(vals[i→n(j)], ty, st)) ∧ r ≠ jvmref → is_array(r, addarray(r, ty, vals, st)) | A User Theorem |
| isarray-addarray-01 | ⊦ r1 ≠ r0 → (is_array(r1, addarray(r0, ty, vals, st)) ↔ is_array(r1, st)) | A User Theorem |
| isarray-addarray-02 | ⊦ r ≠ jvmref → is_array(r, addarray(r, byte_type, mkjavavalues(bytes), st)) | A User Theorem |
| isarray-addarray-other | ⊦ r ≠ r0 ∧ is_array(r, st) → is_array(r, addarray(r0, ty0, vals, st)) | A User Theorem |
| isarray-init-01 | ⊦ i < n→i(# vals) → is_arrayref(r, i, addarray(r, ty, vals, st)) | A User Theorem |
| isarray-init-02 | ⊦ i ≤ n→i(# vals) → is_arrayref(r, i, addarray(r, ty, vals, st)) | A User Theorem |
| isobj-addarray | ⊦ r1 ≠ r0 → (is_obj(r1, addarray(r0, ty, vals, st)) ↔ is_obj(r1, st)) | A User Theorem |
| isobj-addarray-01 | ⊦ ¬ is_obj(r, addarray(r, ty, i, st)) | A User Theorem |
| isobj-addarray-other | ⊦ r ≠ r0 ∧ is_obj(r, st) → is_obj(r, addarray(r0, ty0, vals, st)) | A User Theorem |
| isobj-addarray-other-01 | ⊦ r ≠ r0 ∧ is_obj(r, class, st) → is_obj(r, class, addarray(r0, ty0, vals, st)) | A User Theorem |
| isobj-addbar | ⊦ r ≠ r0 → (is_obj(r, class, sks, addbytearray(r0, ints, st)) ↔ is_obj(r, class, sks, st)) | A User Theorem |
| length-1dim | ⊦ (addarray(r, ty, i, st)[r -- _length]) = intval(i) | A User Theorem |
| length-1dim-01 | ⊦ (addarray(r, val, i, st)[r -- _length]) = st[r -- _length] | A User Theorem |
| length-1dim-02 | ⊦ r -- _length ∈ addarray(r, ty, i, st) | A User Theorem |
| length-1init | ⊦ (addarray(r, vals, j, st)[r -- _length]) = st[r -- _length] | A User Theorem |
| length-1init-01 | ⊦ (addarray(r, ty, vals, st)[r -- _length]) = intval(n→i(# vals)) | A User Theorem |
| length-init | ⊦ r -- _length ∈ addarray(r, ty, vals, st) | A User Theorem |
| lookup-1dim | ⊦ r ≠ r0 → (addarray(r, ty, i, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| lookup-1dim-01 | ⊦ r ≠ r0 → (addarray(r, val, i, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| lookup-1dim-02 | ⊦ newref(r, st0) → (addarray(r, ty, i, st)[jvmref -- sk]) = st[jvmref -- sk] | A User Theorem |
| lookup-1dim-03 | fs ' ≠ _type, fs ' ≠ _length ⊦ (addarray(r0, ty, i, st)[r -- fs ']) = st[r -- fs '] | A User Theorem |
| lookup-1dim-04 | ⊦ (addarray(r0, val, i, st)[r -- fs ']) = st[r -- fs '] | A User Theorem |
| lookup-1dim-05 | class1 ≠ `*Array*' .class, class1 ≠ `java.lang.Object' .class ⊦ (addarray(r0, ty0, i, st)[r -- mkfs(class1, ty, fieldvar) ']) = st[r -- mkfs(class1, ty, fieldvar) '] | A User Theorem |
| lookup-1dim-06 | ⊦ newref(r, st) ∧ r0 ∈ st → (addarray(r, ty, i, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| lookup-1init | ⊦ r ≠ r0 → (addarray(r, ty, vals, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| lookup-1init-01 | ⊦ r ≠ r0 → (addarray(r, vals, j, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| lookup-1init-02 | ⊦ newref(r, st0) → (addarray(r, ty, vals, st)[jvmref -- sk]) = st[jvmref -- sk] | A User Theorem |
| lookup-init | fs ' ≠ _type, fs ' ≠ _length ⊦ (addarray(r0, ty, vals, st)[r -- fs ']) = st[r -- fs '] | A User Theorem |
| lookup-init-01 | ⊦ (addarray(r0, vals, j, st)[r -- fs ']) = st[r -- fs '] | A User Theorem |
| lookup-init-02 | class1 ≠ `*Array*' .class, class1 ≠ `java.lang.Object' .class ⊦ (addarray(r0, ty0, vals, st)[r -- mkfs(class1, ty, fieldvar) ']) = st[r -- mkfs(class1, ty, fieldvar) '] | A User Theorem |
| mode | ⊦ _mode ∈ addarray(r, ty, i, st) ↔ _mode ∈ st | A User Theorem |
| mode-1dim | ⊦ (addarray(r, ty, i, st)[_mode]) = st[_mode] | A User Theorem |
| mode-1dim-01 | ⊦ (addarray(r, val, i, st)[_mode]) = st[_mode] | A User Theorem |
| mode-1init | ⊦ (addarray(r, vals, j, st)[_mode]) = st[_mode] | A User Theorem |
| mode-1init-01 | ⊦ (addarray(r, ty, vals, st)[_mode]) = st[_mode] | A User Theorem |
| move-initvals | ⊦ 0 ≤ i ∧ i→n(i) < # vals → (addarray(r, ty, vals, st)[r -- i ', val]) = addarray(r, ty, vals[i→n(i), val], st) | A User Theorem |
| move-initvals-01 | ⊦ (addarray(r, ty, val ' + vals, st)[r -- 0 ', val0]) = addarray(r, ty, val0 ' + vals, st) | A User Theorem |
| move-initvals-02 | ⊦ (addarray(r, ty, val ' + val0 ' + vals, st)[r -- 1 ', val1]) = addarray(r, ty, val ' + val1 ' + vals, st) | A User Theorem |
| move-initvals-03 | ⊦ (addarray(r, ty, val ' + val0 ', st)[r -- 1 ', val1]) = addarray(r, ty, val ' + val1 ', st) | A User Theorem |
| newref-1dim | ⊦ newref(r0, addarray(r, ty, i, st)) ↔ r ≠ r0 ∧ newref(r0, st) | A User Theorem |
| newref-1dim-01 | ⊦ 0 < i → (newref(r0, addarray(r, val, i, st)) ↔ r ≠ r0 ∧ newref(r0, st)) | A User Theorem |
| newref-1dim-02 | ⊦ i ≤ 0 → (newref(r0, addarray(r, val, i, st)) ↔ newref(r0, st)) | A User Theorem |
| newref-1init | ⊦ vals ≠ [] → (newref(r0, addarray(r, vals, j, st)) ↔ r ≠ r0 ∧ newref(r0, st)) | A User Theorem |
| newref-1init-01 | ⊦ newref(r0, addarray(r, ty, vals, st)) ↔ r ≠ r0 ∧ newref(r0, st) | A User Theorem |
| num-at-1dim | 0 ≤ j, j < i ⊦ (addarray(r, ty, (* i), st)[r -- ((* j)) ']) = initial_value(ty) | A User Theorem |
| okarray | ⊦ r ≠ jvmref ∧ ty ≠ abstract_type → (okarray(r, ty, addarray(r, ty, i, st)) ↔ 0 ≤ i) | A User Theorem |
| okarray-01 | ⊦ r ≠ r0 → (okarray(r, int_type, addarray(r0, ty0, i, st)) ↔ okarray(r, int_type, st)) | A User Theorem |
| okarray-02 | ⊦ r ≠ r0 → (okarray(r, byte_type, addarray(r0, ty, i, st)) ↔ okarray(r, byte_type, st)) | A User Theorem |
| okarray-03 | ⊦ newref(r0, st) ∧ r ∈ st → (okarray(r, byte_type, addarray(r0, ty, i, st)) ↔ okarray(r, byte_type, st)) | A User Theorem |
| okarray-04 | ⊦ is_bytelist(vals) ∧ r ≠ jvmref → okarray(r, byte_type, addarray(r, byte_type, vals, st)) | A User Theorem |
| okarray-05 | ⊦ r ≠ jvmref → okarray(r, byte_type, addarray(r, byte_type, mkjavavalues(bytes), st)) | A User Theorem |
| okarray-06 | ⊦ newref(r0, st) ∧ r ∈ st → (okarray(r, byte_type, addarray(r0, ty, vals, st)) ↔ okarray(r, byte_type, st)) | A User Theorem |
| okarray-1dim | ⊦ r ≠ r0 → (okarray(refval(r), byte_type, i, addarray(r0, ty0, i0, st)) ↔ okarray(refval(r), byte_type, i, st)) | A User Theorem |
| okarray-1dim-01 | ⊦ r ≠ r0 → (okarray(refval(r), short_type, i, addarray(r0, ty0, i0, st)) ↔ okarray(refval(r), short_type, i, st)) | A User Theorem |
| okarray-1dim-02 | ⊦ r ≠ r0 → (okarray(refval(r), int_type, i, addarray(r0, ty0, i0, st)) ↔ okarray(refval(r), int_type, i, st)) | A User Theorem |
| okarray-1dim-03 | ⊦ r ≠ r0 → (okarray(refval(r), boolean_type, i, addarray(r0, ty0, i0, st)) ↔ okarray(refval(r), boolean_type, i, st)) | A User Theorem |
| okarray-1dim-04 | ⊦ 0 ≤ i ∧ r ≠ jvmref ∧ ty ≠ abstract_type → okarray(refval(r), ty, i, addarray(r, ty, i, st)) | A User Theorem |
| okarray-1dim-basic | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) ∧ r ≠ r0 → (okarray(refval(r), ty, i, addarray(r0, ty0, i0, st)) ↔ okarray(refval(r), ty, i, st)) | A User Theorem |
| okarray-1dim-basic-01 | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) ∧ r ≠ r0 → (okarray(refval(r), ty, i, addarray(r0, val0, i0, st)) ↔ okarray(refval(r), ty, i, st)) | A User Theorem |
| okarray-abstract | ⊦ r ≠ jvmref → (okarray(r, abstract_type, addarray(r, abstract_type, i, st)) ↔ i = 0) | A User Theorem |
| okarray-addarray | ⊦ okarray(r, ty, addarray(r, ty, vals, st)) ↔ r ≠ jvmref ∧ (∀ val. val ∈ vals → okval(val, ty)) | A User Theorem |
| okarray-addarray-lenput-primtype | ⊦ 0 < i ∧ r ≠ jvmref ∧ i ≤ n→i(# vals) ∧ (∀ val. val ∈ vals → okval(val, ty)) → okarray(r, ty, addarray(r, ty, vals, st)[r -- _length, intval(i)]) | A User Theorem |
| okarray-addarray-other | ⊦ okarray(r, ty, st) ∧ r ≠ r0 → okarray(r, ty, addarray(r0, ty0, vals, st)) | A User Theorem |
| okarray-copy | ⊦ okarray(r0, byte_type, st) ∧ r ≠ jvmref → okarray(r, byte_type, arraycopy(r0, 0, r, 0, st[r0 -- _length] .intval, addarray(r, byte_type, st[r0 -- _length] .intval, st))) | A User Theorem |
| okarray-init | ⊦ r ≠ r0 → (okarray(refval(r), byte_type, i, addarray(r0, ty0, vals, st)) ↔ okarray(refval(r), byte_type, i, st)) | A User Theorem |
| okarray-init-01 | ⊦ r ≠ r0 → (okarray(refval(r), short_type, i, addarray(r0, ty0, vals, st)) ↔ okarray(refval(r), short_type, i, st)) | A User Theorem |
| okarray-init-02 | ⊦ r ≠ r0 → (okarray(refval(r), int_type, i, addarray(r0, ty0, vals, st)) ↔ okarray(refval(r), int_type, i, st)) | A User Theorem |
| okarray-init-03 | ⊦ r ≠ r0 → (okarray(refval(r), boolean_type, i, addarray(r0, ty0, vals, st)) ↔ okarray(refval(r), boolean_type, i, st)) | A User Theorem |
| okarray-init-04 | ⊦ okarray(refval(r), byte_type, i + 1, addarray(r, byte_type, vals + byteval(by) ', st)) ↔ okarray(refval(r), byte_type, i, addarray(r, byte_type, vals, st)) | A User Theorem |
| okarray-init-05 | ⊦ r ≠ jvmref → okarray(refval(r), byte_type, 1, addarray(r, byte_type, byteval(by) ', st)) | A User Theorem |
| okarray-init-07 | ⊦ newref(r, st) → (okarray(refval(r), byte_type, i, addarray(r, byte_type, vals, st)) ↔ n→i(# vals) = i ∧ is_bytelist(vals)) | A User Theorem |
| okarray-init-basic | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) ∧ r ≠ r0 → (okarray(refval(r), ty, i, addarray(r0, ty0, vals, st)) ↔ okarray(refval(r), ty, i, st)) | A User Theorem |
| okarray-init-basic-01 | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) ∧ r ≠ r0 → (okarray(refval(r), ty, i, addarray(r0, vals, j, st)) ↔ okarray(refval(r), ty, i, st)) | A User Theorem |
| okarray-putarray-addarray-put | ⊦ (∀ val. val ∈ vals ∨ val ∈ vals0 → is_bytevalue(val)) ∧ 0 ≤ i ∧ 0 ≤ j ∧ j ≤ n→i(# vals) + i ∧ i ≤ n→i(# vals0) ∧ r ≠ jvmref → okarray(r, byte_type, putArray(vals, r, i, addarray(r, byte_type, vals0, st))[r -- _length, intval(j)]) | A User Theorem |
| okbar-addarray | ⊦ bytes ≠ [] ∧ r0 ≠ jvmref → okbytearray(r0, addarray(r0, byte_type, mkjavavalues(bytes), st0)) | A User Theorem |
| okbytearray-addarray | ⊦ okbytearray(r, addarray(r, byte_type, mkjavavalues(bytes), st)) ↔ r ≠ jvmref | A User Theorem |
| okbytearray-addarray-01 | ⊦ okbytearray(r, addarray(r, byte_type, vals, st)) ↔ r ≠ jvmref ∧ (∀ val. val ∈ vals → is_bytevalue(val)) | A User Theorem |
| okbytearray-addarray-02 | ⊦ okbytearray(r, addarray(r, byte_type, mklist(byteval(by), n), st)) ↔ r ≠ jvmref | A User Theorem |
| okbytearray-this | ⊦ r ≠ jvmref → (okbytearray(r, addarray(r, byte_type, i, st)) ↔ 0 ≤ i) | A User Theorem |
| okclass-1dim | ⊦ r ≠ r0 → (okclass(refval(r0), class1, addarray(r, ty, i, st)) ↔ okclass(refval(r0), class1, st)) | A User Theorem |
| okclass-init | ⊦ r ≠ r0 → (okclass(refval(r0), class1, addarray(r, ty, vals, st)) ↔ okclass(refval(r0), class1, st)) | A User Theorem |
| okreftype-1dim | ⊦ r ≠ r0 → (okreftype(refval(r), ty, addarray(r0, ty0, i, st)) ↔ okreftype(refval(r), ty, st)) | A User Theorem |
| okreftype-1dim-01 | ⊦ r ≠ r0 → (okreftype(refval(r), ty, addarray(r0, val, i, st)) ↔ okreftype(refval(r), ty, st)) | A User Theorem |
| okreftype-1dim-02 | ⊦ okreftype(refval(r), mkarraytype(ty), addarray(r, ty, i, st)) | A User Theorem |
| okreftype-init | ⊦ r ≠ r0 → (okreftype(refval(r), ty, addarray(r0, ty0, vals, st)) ↔ okreftype(refval(r), ty, st)) | A User Theorem |
| okreftype-init-01 | ⊦ r ≠ r0 → (okreftype(refval(r), ty, addarray(r0, vals, j, st)) ↔ okreftype(refval(r), ty, st)) | A User Theorem |
| okreftype-init-02 | ⊦ okreftype(refval(r), mkarraytype(ty), addarray(r, ty, vals, st)) | A User Theorem |
| oktype-1dim-basic | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (oktype(val, ty, addarray(r0, ty0, i0, st)) ↔ oktype(val, ty, st)) | A User Theorem |
| oktype-1dim-basic-01 | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (oktype(val, ty, addarray(r0, val0, i0, st)) ↔ oktype(val, ty, st)) | A User Theorem |
| oktype-addarray | ⊦ oktype(val, ty, st) → oktype(val, ty, addarray(r0, ty0, vals, st)) | A User Theorem |
| oktype-init-basic | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (oktype(val, ty, addarray(r0, ty0, vals, st)) ↔ oktype(val, ty, st)) | A User Theorem |
| oktype-init-basic-01 | ⊦ ¬ is_classtype(ty) ∧ ¬ is_arraytype(ty) → (oktype(val, ty, addarray(r0, vals, j, st)) ↔ oktype(val, ty, st)) | A User Theorem |
| one-1init | ⊦ (addarray(r, ty, val ' + val0 ', st)[r -- 1 ']) = val0 | A User Theorem |
| one-1init-01 | ⊦ (addarray(r, val ' + val0 ', j, st)[r -- (j + 1) ']) = val0 | A User Theorem |
| one-1init-01-01 | ⊦ (addarray(r, val ' + val0 ' + vals, j, st)[r -- (j + 1) ']) = val0 | A User Theorem |
| one-1init-02 | ⊦ (addarray(r, ty, val ' + val0 ' + vals, st)[r -- 1 ']) = val0 | A User Theorem |
| one-init | ⊦ addarray(r, val ', j, st) = st[r -- j ', val] | A User Theorem |
| out-1dim | ⊦ (addarray(r, ty, i, st)[_out]) = st[_out] | A User Theorem |
| out-1dim-01 | ⊦ (addarray(r, val, i, st)[_out]) = st[_out] | A User Theorem |
| out-1init | ⊦ (addarray(r, vals, j, st)[_out]) = st[_out] | A User Theorem |
| out-1init-01 | ⊦ (addarray(r, ty, vals, st)[_out]) = st[_out] | A User Theorem |
| putByteArray-vals-addarray | ⊦ 0 ≤ j ∧ j ≤ i ∧ i = n→i(# bytes) + j → putByteArray(bytes, r, j, addarray(r, byte_type, i, st)) = addarray(r, byte_type, mklist(initial_value(byte_type), i→n(j)) + mkjavavalues(bytes), st) | A User Theorem |
| putByteArray-vals-addarray-01 | ⊦ 0 ≤ j ∧ j ≤ i ∧ 0 ≤ i1 ∧ i = j + n→i(# bytes) + i1 → putByteArray(bytes, r, j, addarray(r, byte_type, i, st)) = addarray(r, byte_type, mklist(initial_value(byte_type), i→n(j)) + mkjavavalues(bytes) + mklist(initial_value(byte_type), i→n(i1)), st) | A User Theorem |
| putarray-add-butlast | ⊦ i = n→i(# vals) + 1 → putArray(vals, r, 0, addarray(r, ty, i, st)) = addarray(r, ty, vals + initial_value(ty), st) | A User Theorem |
| putarray-add-same | ⊦ i = n→i(# vals) → putArray(vals, r, addarray(r, ty, i, st)) = addarray(r, ty, vals, st) | A User Theorem |
| putarray-add-same-01 | ⊦ i = n→i(# vals) → putArray(vals, r, 0, addarray(r, ty, i, st)) = addarray(r, ty, vals, st) | A User Theorem |
| putarray-add-same-02 | ⊦ i = n→i(# vals) ∧ val = initial_value(ty) → putArray(vals, r, 0, addarray(r, val, i, st)) = addarray(r, vals, 0, st) | A User Theorem |
| putarray-addarray | ⊦ 0 ≤ j ∧ j ≤ i ∧ i ≤ j + n→i(# vals) → putArray(vals, r, j, addarray(r, val, i, st)) = addarray(r, mklist(val, i→n(j)) + vals, 0, st) | A User Theorem |
| putarray-addarray-01 | ⊦ 0 ≤ i ∧ 0 ≤ j ∧ i ≤ j → putArray(vals, r, i, addarray(r, ty, j, st)) = (addarray (r, ty, mklist(initial_value(ty), i→n(i)) + vals + ((j - i + n→i(# vals) > 0 ⊃ mklist(initial_value(ty), i→n(j - i + n→i(# vals))); [])), st) [r -- _length, intval(j) ] ) | A User Theorem |
| putarray-addarray-one | ⊦ i = n→i(# vals) + 1 ∧ is_reftype(ty) → putArray(vals, r, 1, addarray(r, ty, i, st)) = addarray(r, ty, refval(jvmref) ' + vals, st) | A User Theorem |
| putarray-addarray-override | ⊦ 0 ≤ i ∧ i + n→i(# vals) ≤ n→i(# vals0) → putArray(vals, r, i, addarray(r, ty, vals0, st)) = addarray(r, ty, firstn(i→n(i), vals0) + vals + restn(i→n(i) + # vals, vals0), st) | A User Theorem |
| putbytearray-addarray-override | ⊦ n→i(# vals0) = i ∧ # vals1 = # bytes → putByteArray(bytes, r, i, addarray(r, byte_type, vals0 + vals1, st)) = addarray(r, byte_type, vals0 + mkjavavalues(bytes), st) | A User Theorem |
| shift-1dim | ⊦ r ≠ r0 → (addarray(r, ty, i, st)[r0 -- sk, val]) = addarray(r, ty, i, st[r0 -- sk, val]) | A User Theorem |
| shift-1dim-01 | ⊦ r ≠ r0 → (addarray(r, val0, i, st)[r0 -- sk, val]) = addarray(r, val0, i, st[r0 -- sk, val]) | A User Theorem |
| shift-1dim-02 | ⊦ r ≠ r0 ∧ r0 ≠ jvmref → (addarray(r, ty, i, st)[r0 -- sk, val]) = addarray(r, ty, i, st[r0 -- sk, val]) | A User Theorem |
| shift-1init | ⊦ r ≠ r0 → (addarray(r, ty, vals, st)[r0 -- sk, val]) = addarray(r, ty, vals, st[r0 -- sk, val]) | A User Theorem |
| shift-1init-01 | ⊦ r ≠ r0 → (addarray(r, vals, j, st)[r0 -- sk, val]) = addarray(r, vals, j, st[r0 -- sk, val]) | A User Theorem |
| shift-1init-02 | ⊦ r ≠ r0 ∧ r0 ≠ jvmref → (addarray(r, ty, vals, st)[r0 -- sk, val]) = addarray(r, ty, vals, st[r0 -- sk, val]) | A User Theorem |
| store-1init | ⊦ j ≤ i ∧ i < j + n→i(# vals) → ((addarray(r, vals, j, st)[r -- i ']) = (addarray(r, vals, j, st0)[r -- i ']) ↔ true) | A User Theorem |
| stsubset | ⊦ newref(r, st) → st ⊆ addarray(r, ty, i, st) | A User Theorem |
| stsubset-01 | ⊦ newref(r, st) ∧ newref(r0, st) → st ⊆ addarray(r, ty, i, addobj(r0, class1, fis, st)) | A User Theorem |
| stsubset-02 | ⊦ newref(r, st) ∧ newref(r0, st) → st ⊆ (addarray(r, ty, i, addobj(r0, class1, fis, st))[r -- sk, val]) | A User Theorem |
| stsubset-03 | ⊦ newref(r, st) → (st ⊆ addarray(r, ty, i, st0) ↔ st ⊆ st0) | A User Theorem |
| subset-addarray | ⊦ st ⊆ st0 ∧ newref(r, st0) → st ⊆ addarray(r, ty, vals, st0) | A User Theorem |
| subset-addarray-01 | ⊦ newref(r, st0) ∧ newref(r, st) → (st ⊆ addarray(r, ty, vals, st0) ↔ st ⊆ st0) | A User Theorem |
| subset-putarray-addarray-newref | ⊦ newref(r, st) → st ⊆ putArray(vals0, r, i, addarray(r, ty, vals, st)) | A User Theorem |
| subset-putarray2-addarray-newref | ⊦ newref(r, st) → st ⊆ putArray(vals0, r, i, putArray(vals1, r, j, addarray(r, ty, vals, st))) | A User Theorem |
| subset-putarray2-put-addarray-newref | ⊦ newref(r, st) → st ⊆ (putArray(vals0, r, i, putArray(vals1, r, j, addarray(r, ty, vals, st)))[r -- i0 ', val]) | A User Theorem |
| subset-putarray2-put-addarray-newref-01 | ⊦ newref(r, st) → st ⊆ (putArray(vals0, r, i, putArray(vals1, r, j, addarray(r, ty, i1, st)))[r -- i0 ', val]) | A User Theorem |
| subset-putarray2-put-addarray-newref-01-01 | ⊦ st ⊆ st1 ∧ newref(r, st) → st ⊆ (putArray(vals0, r, i, putArray(vals1, r, j, addarray(r, ty, i1, st1)))[r -- i0 ', val]) | A User Theorem |
| succ-1init | ⊦ 0 < i ∧ i ≤ n→i(# vals) → (addarray(r, ty, val + vals, st)[r -- i ']) = (addarray(r, ty, vals, st)[r -- (i - 1) ']) | A User Theorem |
| switch-addarray-addclass | ⊦ r ≠ jvmref → addarray(r, ty, i, addclass(class, fis, st)) = addclass(class, fis, addarray(r, ty, i, st)) | A User Theorem |
| switch-addarray-addclass-01 | ⊦ r ≠ jvmref → addarray(r, val, i, addclass(class, fis, st)) = addclass(class, fis, addarray(r, val, i, st)) | A User Theorem |
| switch-addarray-addobj | ⊦ r ≠ r0 → addarray(r, ty, i, addobj(r0, class, fis, st)) = addobj(r0, class, fis, addarray(r, ty, i, st)) | A User Theorem |
| switch-addarray-addobj-01 | ⊦ r ≠ r0 → addarray(r, initial_value(ty), i1, addobj(r0, class, fis, st)[r -- _type, typeval(mkarraytype(ty))][r -- _length, intval(i)]) = addobj(r0, class, fis, addarray(r, initial_value(ty), i1, st[r -- _type, typeval(mkarraytype(ty))][r -- _length, intval(i)])) | A User Theorem |
| switch-array | ⊦ r ≠ r0 → addarray(r, ty, vals, addarray(r0, ty0, vals0, st)) = addarray(r0, ty0, vals0, addarray(r, ty, vals, st)) | A User Theorem |
| switch-class | ⊦ r ≠ jvmref → addarray(r, ty, vals, addclass(class, fis, st)) = addclass(class, fis, addarray(r, ty, vals, st)) | A User Theorem |
| switch-class-01 | ⊦ addarray(r, vals, i, addclass(class, fis, st)) = addclass(class, fis, addarray(r, vals, i, st)) | A User Theorem |
| switch-obj | ⊦ r ≠ r0 → addarray(r, ty, vals, addobj(r0, class, fis, st)) = addobj(r0, class, fis, addarray(r, ty, vals, st)) | A User Theorem |
| switch-obj-01 | ⊦ r ≠ r0 → addarray(r, vals, i, addobj(r0, class, fis, st)) = addobj(r0, class, fis, addarray(r, vals, i, st)) | A User Theorem |
| type-1dim | ⊦ (addarray(r, ty, i, st)[r -- _type]) = typeval(mkarraytype(ty)) | A User Theorem |
| type-1dim-01 | ⊦ (addarray(r, val, i, st)[r -- _type]) = st[r -- _type] | A User Theorem |
| type-1init | ⊦ (addarray(r, ty, vals, st)[r -- _type]) = typeval(mkarraytype(ty)) | A User Theorem |
| type-1init-01 | ⊦ (addarray(r, vals, j, st)[r -- _type]) = st[r -- _type] | A User Theorem |
| type-in | ⊦ r -- _type ∈ addarray(r, ty, i, st) | A User Theorem |
| union-addarray-rew | ⊦ newref(r, st ∪ st0) → addarray(r, ty, vals, st ∪ st0) = st ∪ addarray(r, ty, vals, st0) | A User Theorem |
| validref-addarray | ⊦ r1 ≠ r0 → (is_valid_ref(r1, addarray(r0, ty, vals, st)) ↔ is_valid_ref(r1, st)) | A User Theorem |
| zero-1init | ⊦ (addarray(r, ty, val + vals, st)[r -- 0 ']) = val | A User Theorem |
| zero-1init-02 | ⊦ (addarray(r, ty, val ', st)[r -- 0 ']) = val | A User Theorem |
| zero-1init-05 | ⊦ (addarray(r, ty, val ' + vals, st)[r -- 0 ']) = val | A User Theorem |