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: |
|---|---|---|
| getArray-zero | ⊦ j ≤ 0 → getarray(r, i, j, st) = [] | An Axiom |
| getArray-one | ⊦ getarray(r, i, 1, st) = st[r -- i '] ' | An Axiom |
| getArray-rec | ⊦ 1 < j → getarray(r, i, j, st) = getarray(r, i, j - 1, st) + st[r -- (i + j - 1) '] | An Axiom |
| getArray-all | ⊦ getarray(r, st) = getarray(r, 0, st[r -- _length] .intval, st) | An Axiom |
| getArrayv-all | ⊦ getarrayv(r, st) = getarrayv(r, 0, st[r -- _length] .intval, st) | An Axiom |
| getArrayv-rec | ⊦ 1 < j → getarrayv(r, i, j, st) = getarrayv(r, i, j - 1, st) ++ st[r -- (i + j - 1) '] | An Axiom |
| getArrayv-one | ⊦ getarrayv(r, i, 1, st) = st[r -- i '] | An Axiom |
| getArrayv-zero | ⊦ j ≤ 0 → getarrayv(r, i, j, st) = noval | An Axiom |
| arrayCopy-rec | ⊦ 0 < j → arraycopy(r1, i1, r2, i2, j, st) = arraycopy(r1, i1, r2, i2, j - 1, st[r2 -- (i2 + j - 1) ', st[r1 -- (i1 + j - 1) ']]) | An Axiom |
| arrayCopy-base | ⊦ j ≤ 0 → arraycopy(r1, i1, r2, i2, j, st) = st | An Axiom |
| arrayComp | ⊦ arraycomp(r1, i1, r2, i2, j, st) ↔ (∀ i. 0 ≤ i ∧ i < j → st[r1 -- (i1 + i) '] = st[r2 -- (i2 + i) ']) | An Axiom |
| is_arrayref | ⊦ is_arrayref(r, i, st) ↔ (∀ j. 0 ≤ j ∧ j < i → r -- j ' ∈ st) | An Axiom |
| getByteArray | ⊦ getbytearray(r, i, j, st) = bytevalues(getarray(r, i, j, st)) | An Axiom |
| getByteArray-all | ⊦ getbytearray(r, st) = getbytearray(r, 0, st[r -- _length] .intval, st) | An Axiom |
| putByteArray | ⊦ putByteArray(bytes, r, i, st) = putArray(mkjavavalues(bytes), r, i, st) | An Axiom |
| putByteArray-all | ⊦ putByteArray(bytes, r, st) = putByteArray(bytes, r, 0, st) | An Axiom |
| putArray-rec | ⊦ putArray(val ' + vals, r, i, st) = (putArray(vals, r, i + 1, st)[r -- i ', val]) | An Axiom |
| putArray-empty | ⊦ putArray([], r, i, st) = st | An Axiom |
| putArray-all | ⊦ putArray(vals, r, st) = putArray(vals, r, 0, st) | An Axiom |
| getintarray | ⊦ getintarray(r, i, j, st) = intvalues(getarray(r, i, j, st)) | An Axiom |
| getintarray-def | ⊦ getintarray(r, st) = getintarray(r, 0, st[r -- _length] .intval, st) | An Axiom |
| Comp-get | ⊦ ¬ arraycomp(r1, i1, r2, i2, j, st) → getarray(r1, i1, j, st) ≠ getarray(r2, i2, j, st) | A User Theorem |
| Comp-get-01 | ⊦ getarray(r1, i1, j, st) ≠ getarray(r2, i2, j, st) → ¬ arraycomp(r1, i1, r2, i2, j, st) | A User Theorem |
| Comp-get-02 | ⊦ arraycomp(r1, i1, r2, i2, j, st) ↔ getarray(r1, i1, j, st) = getarray(r2, i2, j, st) | A User Theorem |
| arrayComp-01 | ⊦ arraycomp(r1, i1, r2, i2, j, st) ∧ 0 < j → (arraycomp(r1, i1, r2, i2, j + 1, st) ↔ st[r1 -- (i1 + j) '] = st[r2 -- (i2 + j) ']) | A User Theorem |
| arrayComp-02 | ⊦ arraycomp(r1, i1, r2, i2, j, st) ∧ 0 ≤ j → (arraycomp(r1, i1, r2, i2, j + 1, st) ↔ st[r1 -- (i1 + j) '] = st[r2 -- (i2 + j) ']) | A User Theorem |
| arrayComp-03 | ⊦ arraycomp(r1, i1, r2, i2, j + j0, st) ∧ 0 < j ∧ 0 < j0 → (st[r1 -- (i1 + j0) '] = st[r2 -- (i2 + j0) '] ↔ true) | A User Theorem |
| arrayComp-04 | ⊦ arraycomp(r1, i1, r2, i2, j + j0, st) ∧ 0 < j ∧ 0 ≤ j0 → (st[r1 -- (i1 + j0) '] = st[r2 -- (i2 + j0) '] ↔ true) | A User Theorem |
| arrayComp-05 | ⊦ arraycomp(r1, i1, r2, i2, j + j0, st) ∧ 0 < j ∧ 0 ≤ j0 → (st[r1 -- (i1 + j0) '] .byteval = st[r2 -- (i2 + j0) '] .byteval ↔ true) | A User Theorem |
| arrayComp-06 | ⊦ arraycomp(r1, i1, r2, i2, 0, st) | A User Theorem |
| arrayComp-07 | ⊦ arraycomp(r1, i1, r2, i2, j, st) ∧ j0 < j ∧ 0 ≤ j0 → (st[r1 -- (i1 + j0) '] = st[r2 -- (i2 + j0) '] ↔ true) | A User Theorem |
| arrayComp-08 | ⊦ arraycomp(r1, i1, r2, i2, j, st) ∧ j0 < j ∧ 0 ≤ j0 → (st[r1 -- (i1 + j0) '] .byteval = st[r2 -- (i2 + j0) '] .byteval ↔ true) | A User Theorem |
| arrayref | ⊦ is_arrayref(r, i, st[r0 -- fs ', val]) ↔ is_arrayref(r, i, st) | A User Theorem |
| arrayref-01 | ⊦ is_arrayref(r, i, st[r0 -- _length, val]) ↔ is_arrayref(r, i, st) | A User Theorem |
| arrayref-02 | ⊦ is_fskey(sk) → (is_arrayref(r, i, st[r0 -- sk, val]) ↔ is_arrayref(r, i, st)) | A User Theorem |
| at=get | ⊦ 0 ≤ i ∧ i < j → st[r -- i '] = (getarray(r, 0, j, st)[i→n(i)]) | A User Theorem |
| at=get-offset | ⊦ i0 ≤ i ∧ i < j + i0 ∧ 0 ≤ i0 → st[r -- i '] = (getarray(r, i0, j, st)[i→n(i - i0)]) | A User Theorem |
| bar-at | ⊦ n→i(n) < j → (getbytearray(r, i, j, st)[n]) = st[r -- (i + n→i(n)) '] .byteval | A User Theorem |
| bar-at-01 | ⊦ n→i(n) < st[r -- _length] .intval → (getbytearray(r, st)[n]) = st[r -- n→i(n) '] .byteval | A User Theorem |
| bar-empty | ⊦ j < 0 → getbytearray(r, i, j, st) = [] | A User Theorem |
| bar-empty-01 | ⊦ getbytearray(r, i, 0, st) = [] | A User Theorem |
| bar-eq-sub | i0 ≤ i, i + j ≤ i0 + j0 ⊦ getbytearray(r, (* i0), (* j0), st) = getbytearray(r0, (* i0), (* j0), st0) → (getbytearray(r, i, j, st) ≠ getbytearray(r0, i, j, st0) ↔ false) | A User Theorem |
| bar-firstn | ⊦ n→i(n) ≤ j → firstn(n, getbytearray(r, i, j, st)) = getbytearray(r, i, n→i(n), st) | A User Theorem |
| bar-len | ⊦ j ≤ 1 → getbytearray(r, i, j, st) ≠ by ' + by0 ' + bytes | A User Theorem |
| bar-len-01 | ⊦ n < 2 → getbytearray(r, i, n→i(n), st) ≠ by ' + by0 ' + bytes | A User Theorem |
| bar-len-02 | ⊦ 0 ≤ j → # getbytearray(r, i, j, st) = i→n(j) | A User Theorem |
| bar-len-03 | ⊦ # getbytearray(r, i, n→i(m), st) = m | A User Theorem |
| bar-length | ⊦ ¬ st[r -- _length] .intval < 0 → # getbytearray(r, st) = i→n(st[r -- _length] .intval) | A User Theorem |
| bar-neq | ⊦ getbytearray(r, i, j, st) ≠ getbytearray(r0, i0, j, st0) ∧ 0 ≤ j ∧ j ≤ j0 → getbytearray(r, i, j0, st) ≠ getbytearray(r0, i0, j0, st0) | A User Theorem |
| bar-neq-same | ⊦ getbytearray(r, i, j, st) ≠ getbytearray(r0, i, j, st0) ∧ 0 ≤ j ∧ j ≤ j0 → getbytearray(r, i, j0, st) ≠ getbytearray(r0, i, j0, st0) | A User Theorem |
| bar-neq-soffset | ⊦ getbytearray(r, i, j, st) ≠ getbytearray(r0, i, j, st0) ∧ i0 ≤ i ∧ i + j ≤ i0 + j0 → getbytearray(r, i0, j0, st) ≠ getbytearray(r0, i0, j0, st0) | A User Theorem |
| bar-restn | ⊦ n→i(n) ≤ j ∧ 0 ≤ i → restn(n, getbytearray(r, i, j, st)) = getbytearray(r, i + n→i(n), j - n→i(n), st) | A User Theorem |
| bar-sublist | ⊦ n→i(m) + n→i(n) ≤ j → sublist(m, n, getbytearray(r, i, j, st)) = getbytearray(r, i + n→i(m), n→i(n), st) | A User Theorem |
| bar-zero | ⊦ getbytearray(r, st) = [] ↔ st[r -- _length] .intval ≤ 0 | A User Theorem |
| bytevalues | ⊦ bytevalues(vals + vals0) = bytevalues(vals) + bytevalues(vals0) | A User Theorem |
| comp-copy | ⊦ 0 ≤ i ∧ 0 ≤ j ∧ i + j ≤ j0 → arraycomp(r0, i, r, i, j, arraycopy(r0, 0, r, 0, j0, st)) | A User Theorem |
| comp-negative | ⊦ arraycomp(r1, i1, r2, i2, ~ 1, st) | A User Theorem |
| comp-next | ⊦ arraycomp(r1, i1, r2, i2, i, st0) ∧ r1 ≠ r2 → arraycomp(r1, i1, r2, i2, i + 1, st0[r2 -- (i2 + i) ', st0[r1 -- (i1 + i) ']]) | A User Theorem |
| comp-same | i2 < i1, i + i4 * (i1 - i2) < i3, 0 ≤ i2, 0 ≤ i4, 0 ≤ j0, j0 ≤ i4, 0 ≤ i, ∀ j. 0 ≤ j ∧ j < i3 → st[r -- (i1 + j) '] = st[r -- (i2 + j) '] ⊦ st[r -- (i1 + i + j0 * (i1 - i2)) '] = st[r -- (i1 + i) '] | A User Theorem |
| copy-arref | ⊦ r1 ≠ r0 → (is_arrayref(r1, i1, arraycopy(r, i, r0, i0, j, st)) ↔ is_arrayref(r1, i1, st)) | A User Theorem |
| copy-at | ⊦ r1 ≠ r0 → (arraycopy(r, i, r0, i0, j, st)[r1 -- sk]) = st[r1 -- sk] | A User Theorem |
| copy-at-01 | ⊦ 0 ≤ i ∧ i < j0 ∧ 0 < j → (arraycopy(r, 0, r0, 0, j * j0, st)[r0 -- (i * j) ']) = st[r -- (i * j) '] | A User Theorem |
| copy-atfield | ⊦ (arraycopy(r1, i1, r2, i2, j, st)[r -- fs ']) = st[r -- fs '] | A User Theorem |
| copy-bet-bet | ⊦ i0 < i ∧ i < i0 + j ∧ i0 ≤ j0 ∧ j0 < i0 + j → (arraycopy(r, i, r, i0, j, st)[r -- j0 ']) = st[r -- (i + j - (i0 + j - j0 + 1) % (i - i0) + 1) '] | A User Theorem |
| copy-bet-low | ⊦ i ≤ i0 ∧ i0 ≤ j0 ∧ j0 < i0 + j → (arraycopy(r, i, r, i0, j, st)[r -- j0 ']) = st[r -- ((j0 - i0) + i) '] | A User Theorem |
| copy-bet-up | ⊦ i0 + j ≤ i ∧ i0 ≤ j0 ∧ j0 < i0 + j → (arraycopy(r, i, r, i0, j, st)[r -- j0 ']) = st[r -- ((j0 - i0) + i) '] | A User Theorem |
| copy-between | ⊦ r ≠ r0 ∧ i0 ≤ j0 ∧ j0 < i0 + j → (arraycopy(r, i, r0, i0, j, st)[r0 -- j0 ']) = st[r -- ((j0 - i0) + i) '] | A User Theorem |
| copy-ident | ⊦ (arraycopy(r, i, r, i, j, st)[r -- j0 ']) = st[r -- j0 '] | A User Theorem |
| copy-in | ⊦ r1 ≠ r0 → (r1 -- sk ∈ arraycopy(r, i, r0, i0, j, st) ↔ r1 -- sk ∈ st) | A User Theorem |
| copy-in-01 | ⊦ r1 ≠ r0 → (r1 ∈ arraycopy(r, i, r0, i0, j, st) ↔ r1 ∈ st) | A User Theorem |
| copy-in-02 | ⊦ r ∈ st → r ∈ arraycopy(r1, i1, r2, i2, j, st) | A User Theorem |
| copy-in-between | ⊦ i0 ≤ j0 ∧ j0 < i0 + j → r0 -- j0 ' ∈ arraycopy(r, i, r0, i0, j, st) | A User Theorem |
| copy-in-lower | ⊦ j0 < i0 → (r0 -- j0 ' ∈ arraycopy(r, i, r0, i0, j, st) ↔ r0 -- j0 ' ∈ st) | A User Theorem |
| copy-in-upper | ⊦ i0 + j ≤ j0 → (r0 -- j0 ' ∈ arraycopy(r, i, r0, i0, j, st) ↔ r0 -- j0 ' ∈ st) | A User Theorem |
| copy-in-upper-01 | ⊦ r0 -- (i0 + j) ' ∈ arraycopy(r, i, r0, i0, j, st) ↔ r0 -- (i0 + j) ' ∈ st | A User Theorem |
| copy-infs | ⊦ r -- fs ' ∈ arraycopy(r1, i1, r2, i2, j, st) ↔ r -- fs ' ∈ st | A User Theorem |
| copy-init | ⊦ initdone(class1, arraycopy(r, i, r0, i0, j, st)) ↔ initdone(class1, st) | A User Theorem |
| copy-init-01 | ⊦ initundone(class1, arraycopy(r, i, r0, i0, j, st)) ↔ initundone(class1, st) | A User Theorem |
| copy-init-02 | ⊦ initerror(class1, arraycopy(r, i, r0, i0, j, st)) ↔ initerror(class1, st) | A User Theorem |
| copy-length | ⊦ (arraycopy(r1, i1, r2, i2, j, st)[r -- _length]) = st[r -- _length] | A User Theorem |
| copy-length-02 | ⊦ r -- _length ∈ arraycopy(r1, i1, r2, i2, j, st) ↔ r -- _length ∈ st | A User Theorem |
| copy-lower | ⊦ j0 < i0 → (arraycopy(r, i, r0, i0, j, st)[r0 -- j0 ']) = st[r0 -- j0 '] | A User Theorem |
| copy-mode | ⊦ (arraycopy(r1, i1, r2, i2, j, st)[_mode]) = st[_mode] | A User Theorem |
| copy-mode-01 | ⊦ _mode ∈ arraycopy(r, i, r0, i0, j, st) ↔ _mode ∈ st | A User Theorem |
| copy-new | ⊦ r1 ≠ r0 → (newref(r1, arraycopy(r, i, r0, i0, j, st)) ↔ newref(r1, st)) | A User Theorem |
| copy-ref | ⊦ r1 ≠ r0 → (reftypep(refval(r1), arraycopy(r, i, r0, i0, j, st)) ↔ reftypep(refval(r1), st)) | A User Theorem |
| copy-succ | ⊦ 0 ≤ j ∧ r ≠ r0 → (arraycopy(r, i, r0, i0, j, st)[r0 -- (i0 + j) ', st[r -- (i + j) ']]) = arraycopy(r, i, r0, i0, j + 1, st) | A User Theorem |
| copy-type | ⊦ r -- _type ∈ arraycopy(r1, i1, r2, i2, j, st) ↔ r -- _type ∈ st | A User Theorem |
| copy-type-01 | ⊦ (arraycopy(r1, i1, r2, i2, j, st)[r -- _type]) = st[r -- _type] | A User Theorem |
| copy-upper | ⊦ i0 + j ≤ j0 → (arraycopy(r, i, r0, i0, j, st)[r0 -- j0 ']) = st[r0 -- j0 '] | A User Theorem |
| copy-upper-01 | ⊦ (arraycopy(r, i, r0, i0, j, st)[r0 -- (i0 + j) ']) = st[r0 -- (i0 + j) '] | A User Theorem |
| copy-zero | ⊦ arraycopy(r1, i1, r2, i2, 0, st) = st | A User Theorem |
| extension | ⊦ getbytearray(r, i, j, st) = getbytearray(r0, i0, j0, st0) ↔ j ≤ 0 ∧ j0 ≤ 0 ∨ 0 ≤ j ∧ j = j0 ∧ (∀ j1. 0 ≤ j1 ∧ j1 < j → st[r -- (i + j1) '] .byteval = st0[r0 -- (i0 + j1) '] .byteval) | A User Theorem |
| extension-01 | ⊦ getbytearray(r, st) = getbytearray(r0, st0) ↔ st[r -- _length] .intval ≤ 0 ∧ st0[r0 -- _length] .intval ≤ 0 ∨ 0 ≤ st[r -- _length] .intval ∧ st[r -- _length] .intval = st0[r0 -- _length] .intval ∧ (∀ j1. 0 ≤ j1 ∧ j1 < st[r -- _length] .intval → st[r -- j1 '] .byteval = st0[r0 -- j1 '] .byteval) | A User Theorem |
| get-alleq | ⊦ getarray(r, i, j, st) = getarray(r0, i0, j, st0) ↔ (∀ j0. 0 ≤ j0 ∧ j0 < j → st[r -- (i + j0) '] = st0[r0 -- (i0 + j0) ']) | A User Theorem |
| get-ateq | ⊦ getarray(r, i, j, st) = getarray(r0, i, j, st0) ∧ i ≤ j0 ∧ j0 < i + j → (st[r -- j0 '] ≠ st0[r0 -- j0 '] ↔ false) | A User Theorem |
| get-ateq-01 | ⊦ getarray(r, i, j, st) = getarray(r0, i, j, st0) ∧ i ≤ j0 ∧ j0 < i + j → (st[r -- j0 '] .byteval ≠ st0[r0 -- j0 '] .byteval ↔ false) | A User Theorem |
| get-del | ⊦ r ≠ r0 → getarray(r, st -- r0) = getarray(r, st) | A User Theorem |
| get-del-01 | ⊦ r ≠ r0 → getarray(r, i, j, st -- r0) = getarray(r, i, j, st) | A User Theorem |
| get-empty | ⊦ getarray(r, i, j, st) = [] ↔ j ≤ 0 | A User Theorem |
| get-eqex | r ≠ r0 ⊦ getarray(r, st0) = vals ∧ eqex(st, st0, r0) → getarray(r, st) = vals | A User Theorem |
| get-eqex-01 | r ≠ r0 ⊦ getarray(r, st0) ≠ vals ∧ eqex(st, st0, r0) → getarray(r, st) ≠ vals | A User Theorem |
| get-eqex-02 | r ≠ r0 ⊦ getarray(r, i, j, st0) = vals ∧ eqex(st, st0, r0) → getarray(r, i, j, st) = vals | A User Theorem |
| get-eqex-03 | r ≠ r0 ⊦ getarray(r, i, j, st0) ≠ vals ∧ eqex(st, st0, r0) → getarray(r, i, j, st) ≠ vals | A User Theorem |
| get-first | ⊦ 0 < j → getarray(r, i, j, st) .first = st[r -- i '] | A User Theorem |
| get-get | ⊦ n→i(n) < j → (getarray(r, i, j, st)[n]) = st[r -- (i + n→i(n)) '] | A User Theorem |
| get-length | ⊦ 0 < j → # getarray(r, i, j, st) = i→n(j) | A User Theorem |
| get-length-01 | ⊦ 0 ≤ j → # getarray(r, i, j, st) = i→n(j) | A User Theorem |
| get-length-02 | ⊦ j < 0 → # getarray(r, i, j, st) = 0 | A User Theorem |
| get-length-03 | ⊦ j ≤ 0 → # getarray(r, i, j, st) = 0 | A User Theorem |
| get-length-04 | ⊦ n→i(m) < j → # getarray(r, i, j, st) = i→n(j) | A User Theorem |
| get-put | ⊦ fs ' ≠ _length → getbytearray(r, st[r0 -- fs ', val]) = getbytearray(r, st) | A User Theorem |
| get-put-01 | ⊦ getbytearray(r, i, j, st[r0 -- fs ', val]) = getbytearray(r, i, j, st) | A User Theorem |
| get-put-02 | ⊦ rk .key ≠ _length ∧ is_fskey(rk .key) → getbytearray(r, st[rk, val]) = getbytearray(r, st) | A User Theorem |
| get-put-03 | ⊦ rk .key ≠ _length ∧ is_fskey(rk .key) → getbytearray(r, i, j, st[rk, val]) = getbytearray(r, i, j, st) | A User Theorem |
| get-put-04 | ⊦ getbytearray(r, i, j, st[r0 -- mkfs(class, ty, `initstate' .field) ', val]) = getbytearray(r, i, j, st) | A User Theorem |
| get-put-05 | ⊦ getbytearray(r, st[r0 -- mkfs(class, ty, `initstate' .field) ', val]) = getbytearray(r, st) | A User Theorem |
| get-puteq | ⊦ getarray(r, i, j, st) = getarray(r0, i, j, st0) ∧ getarray(r, i, j, st[r -- sk, val]) ≠ getarray(r0, i, j, st0[r0 -- sk, val0]) → val ≠ val0 | A User Theorem |
| get-rec-01 | ⊦ 0 < j → getarray(r, i, j, st) = st[r -- i '] ' + getarray(r, i + 1, j - 1, st) | A User Theorem |
| get-rest | ⊦ 0 < j → getarray(r, i, j, st) .rest = getarray(r, i + 1, j - 1, st) | A User Theorem |
| get-rest-01 | ⊦ n→i(m) < j → getarray(r, i, j, st) .rest = getarray(r, i + 1, j - 1, st) | A User Theorem |
| get-sublist | ⊦ n→i(m) + n→i(n) ≤ j → sublist(m, n, getarray(r, i, j, st)) = getarray(r, i + n→i(m), n→i(n), st) | A User Theorem |
| get-zero | ⊦ getarray(r, i, 0, st) = [] | A User Theorem |
| getArray-rec-01 | ⊦ 0 < j → getarray(r, i, j, st) = getarray(r, i, j - 1, st) + st[r -- (i + j - 1) '] | A User Theorem |
| getByteArray-put | ⊦ r1 ≠ r → getbytearray(r1, st[r -- sk, val]) = getbytearray(r1, st) | A User Theorem |
| getByteArray-put-01 | ⊦ r1 ≠ rk .ref → getbytearray(r1, st[rk, val]) = getbytearray(r1, st) | A User Theorem |
| getar-at | ⊦ is_bytevalue(getarray(r, i, j, st)[n]) ∧ n→i(n) < j → (getarray(r, i, j, st)[n]) = byteval(getbytearray(r, i, j, st)[n]) | A User Theorem |
| getar-putbar | ⊦ r ≠ r1 → getarray(r, putByteArray(bytes, r1, st)) = getarray(r, st) | A User Theorem |
| getar-putbar-01 | ⊦ r ≠ r1 → getarray(r, putByteArray(bytes, r1, i, st)) = getarray(r, st) | A User Theorem |
| getarray-copy | r ≠ r2 ⊦ getarray(r, arraycopy(r1, i1, r2, i2, j, st)) = getarray(r, st) | A User Theorem |
| getarray-copy-01 | r ≠ r2 ⊦ getarray(r, i, j, arraycopy(r1, i1, r2, i2, j, st)) = getarray(r, i, j, st) | A User Theorem |
| getarray-copy-02 | r ≠ r2 ⊦ getarray(r, i, j, arraycopy(r1, i1, r2, i2, j0, st)) = getarray(r, i, j, st) | A User Theorem |
| getarray-get | ⊦ n < # getarray(r, st) → (getarray(r, st)[n]) = st[r -- n→i(n) '] | A User Theorem |
| getarray-in | ⊦ val ∈ getarray(r, st) ↔ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ st[r -- i '] = val) | A User Theorem |
| getarray-in-01 | ⊦ 0 < i1 → (val ∈ getarray(r, i0, i1, st) ↔ (∃ i. i0 ≤ i ∧ i < i0 + i1 ∧ st[r -- i '] = val)) | A User Theorem |
| getarray-length | ⊦ 0 ≤ st[r -- _length] .intval → # getarray(r, st) = i→n(st[r -- _length] .intval) | A User Theorem |
| getarray-length-01 | ⊦ 0 ≤ st[r -- _length] .intval ∧ getarray(r, 0, st[r -- _length] .intval, st) = vals → # vals = i→n(st[r -- _length] .intval) | A User Theorem |
| getarray-offset | j0 ≤ j, 0 ≤ j0 ⊦ getarray(r, i, j, st) = getarray(r, i, j0, st) + getarray(r, i + j0, j - j0, st) | A User Theorem |
| getarray-offset-01 | 2 ≤ j ⊦ getarray(r, i, j, st) = getarray(r, i, 2, st) + getarray(r, i + 2, j - 2, st) | A User Theorem |
| getarray-offset-02 | 0 < j ⊦ getarray(r, i, j, st) = st[r -- i '] ' + getarray(r, i + 1, j - 1, st) | A User Theorem |
| getarray-put | ⊦ i0 < i → getarray(r, i, j, st[r -- i0 ', val]) = getarray(r, i, j, st) | A User Theorem |
| getarray-put-01 | ⊦ i0 < i ∨ i + j ≤ i0 → getarray(r, i, j, st[r -- i0 ', val]) = getarray(r, i, j, st) | A User Theorem |
| getarray-put-02 | ⊦ r ≠ r0 → getarray(r, i, j, st[r0 -- sk, val]) = getarray(r, i, j, st) | A User Theorem |
| getarray-put-03 | ⊦ getarray(r, i, j, st[r0 -- fs ', val]) = getarray(r, i, j, st) | A User Theorem |
| getarray-put-04 | ⊦ is_fskey(sk) → getarray(r, i, j, st[r0 -- sk, val]) = getarray(r, i, j, st) | A User Theorem |
| getarray-put-05 | ⊦ i0 < i ∨ i + j ≤ i0 → getarray(r, i, j, st[r0 -- i0 ', val]) = getarray(r, i, j, st) | A User Theorem |
| getarray-put-06 | ⊦ fs ' ≠ _type ∧ fs ' ≠ _length → getarray(r, st[r0 -- fs ', val]) = getarray(r, st) | A User Theorem |
| getarray-put-07 | ⊦ r ≠ r0 ∨ fs ' ≠ _type ∧ fs ' ≠ _length → getarray(r, st[r0 -- fs ', val]) = getarray(r, st) | A User Theorem |
| getarray-put-other | ⊦ r ≠ r0 → getarray(r, st[r0 -- sk, val]) = getarray(r, st) | A User Theorem |
| getarray-put=set | ⊦ i ≤ i0 ∧ i0 < i + j → getarray(r, i, j, st[r -- i0 ', val]) = (getarray(r, i, j, st)[i→n(i0 - i), val]) | A User Theorem |
| getarray-putbar | ⊦ r ≠ r1 → getarray(r, i, j, putByteArray(bytes, r1, st)) = getarray(r, i, j, st) | A User Theorem |
| getarray-putbar-01 | ⊦ r ≠ r1 → getarray(r, i, j, putByteArray(bytes, r1, i0, st)) = getarray(r, i, j, st) | A User Theorem |
| getarray-subset | ⊦ st ⊆ st0 ∧ is_arrayref(r, i + j, st) ∧ 0 ≤ i → getarray(r, i, j, st) = getarray(r, i, j, st0) | A User Theorem |
| getarray-superset | ⊦ st ⊆ st0 ∧ is_arrayref(r, i + j, st) ∧ 0 ≤ i → getarray(r, i, j, st0) = getarray(r, i, j, st) | A User Theorem |
| getarray-union | ⊦ ¬ r ∈ st → getarray(r, i, j, st ∪ st0) = getarray(r, i, j, st0) | A User Theorem |
| getarray-union-01 | ⊦ r -- _length ∈ st ∧ 0 < st[r -- _length] .intval ∧ (∀ i1. 0 ≤ i1 ∧ i1 < st[r -- _length] .intval → r -- i1 ' ∈ st) → getarray(r, 0, st[r -- _length] .intval, st0 ∪ st) = getarray(r, 0, st[r -- _length] .intval, st) | A User Theorem |
| getarray-union-02 | ⊦ r -- _length ∈ st ∧ 0 < j ∧ j ≤ st[r -- _length] .intval ∧ (∀ i1. 0 ≤ i1 ∧ i1 < j → r -- i1 ' ∈ st) → getarray(r, 0, j, st0 ∪ st) = getarray(r, 0, j, st) | A User Theorem |
| getarray-union-03 | ⊦ r -- _length ∈ st ∧ 0 ≤ i ∧ j ≤ st[r -- _length] .intval - i ∧ (∀ i1. i ≤ i1 ∧ i1 < i + j → r -- i1 ' ∈ st) → getarray(r, i, j, st0 ∪ st) = getarray(r, i, j, st) | A User Theorem |
| getarray=getbytearray | ⊦ is_bytelist(getarray(r, i, j, st)) → getarray(r, i, j, st) = mkjavavalues(getbytearray(r, i, j, st)) | A User Theorem |
| getba-eq | ⊦ (∀ i0. i1 ≤ i0 ∧ i0 < i1 + i → st[r -- i0 '] = st[r1 -- i0 ']) ∧ 0 ≤ i ∧ 0 ≤ i1 → getbytearray(r, i1, i, st) = getbytearray(r1, i1, i, st) | A User Theorem |
| getba-neq | ⊦ st1[r -- i '] .byteval ≠ st1[r1 -- i '] .byteval ∧ 0 ≤ i ∧ i < st1[r -- _length] .intval ∧ st1[r1 -- _length] .intval = st1[r -- _length] .intval → getbytearray(r, st1) ≠ getbytearray(r1, st1) | A User Theorem |
| getba-neq-01 | ⊦ st1[r -- i1 '] .byteval ≠ st1[r1 -- i1 '] .byteval ∧ 0 ≤ i ∧ i ≤ i1 ∧ i1 < i + j ∧ 0 < j → getbytearray(r, i, j, st1) ≠ getbytearray(r1, i, j, st1) | A User Theorem |
| getbar-2rec | ⊦ 2 ≤ j → getbytearray(r, i, j, st) = st[r -- i '] .byteval ' + st[r -- (i + 1) '] .byteval ' + getbytearray(r, i + 2, j - 2, st) | A User Theorem |
| getbar-3rec | ⊦ 3 ≤ j → getbytearray(r, i, j, st) = st[r -- i '] .byteval ' + st[r -- (i + 1) '] .byteval ' + st[r -- (i + 2) '] .byteval ' + getbytearray(r, i + 3, j - 3, st) | A User Theorem |
| getbar-5rec | ⊦ 5 ≤ j → getbytearray(r, i, j, st) = st[r -- i '] .byteval ' + st[r -- (i + 1) '] .byteval ' + st[r -- (i + 2) '] .byteval ' + st[r -- (i + 3) '] .byteval ' + st[r -- (i + 4) '] .byteval ' + getbytearray(r, i + 5, j - 5, st) | A User Theorem |
| getbar-anyrec | ⊦ 0 ≤ j0 ∧ j0 ≤ j → getbytearray(r, i, j, st) = getbytearray(r, i, j0, st) + getbytearray(r, i + j0, j - j0, st) | A User Theorem |
| getbar-appeq | ⊦ 0 ≤ j → ( getbytearray(r, i, j, st) + bytes = getbytearray(r0, i0, j, st) + bytes0 ↔ getbytearray(r, i, j, st) = getbytearray(r0, i0, j, st) ∧ bytes = bytes0) | A User Theorem |
| getbar-appeq-01 | 0 ≤ j ⊦ getbytearray(r, i, (* j), st) + bytes = getbytearray(r0, i0, j, st) + bytes0 ↔ getbytearray(r, i, j, st) = getbytearray(r0, i0, j, st) ∧ bytes = bytes0 | A User Theorem |
| getbar-lastrec | ⊦ 0 < j → getbytearray(r, i, j, st) = getbytearray(r, i, j - 1, st) + st[r -- (i + j - 1) '] .byteval | A User Theorem |
| getbar-len | ⊦ 0 ≤ st[r -- _length] .intval → n→i(# getbytearray(r, st)) = st[r -- _length] .intval | A User Theorem |
| getbar-len-01 | ⊦ st[r -- _length] .intval < 0 → # getbytearray(r, st) = 0 | A User Theorem |
| getbar-len-02 | ⊦ i ≤ j → # getbytearray(r, i0, j - i, st) = i→n(j - i) | A User Theorem |
| getbar-len-03 | ⊦ 0 ≤ st[r -- _length] .intval → # getbytearray(r, st) = i→n(st[r -- _length] .intval) | A User Theorem |
| getbar-length | 0 ≤ i ⊦ st[r -- _length] .intval = ((* i)) → # getbytearray(r, st) = i→n(st[r -- _length] .intval) | A User Theorem |
| getbar-length-01 | j0 ≤ j1 ⊦ ((* j1)) ≤ j → # getbytearray(r, i, j - ((* j0)), st) = i→n(j - j0) | A User Theorem |
| getbar-mod | ⊦ onlyModified(r, st, st0) ∧ r ≠ r0 → getbytearray(r0, st) = getbytearray(r0, st0) | A User Theorem |
| getbar-mod-01 | ⊦ onlyModified(r, st, st0) ∧ r ≠ r0 → getbytearray(r0, i, j, st) = getbytearray(r0, i, j, st0) | A User Theorem |
| getbar-mode | ⊦ getbytearray(r, st[_mode, val]) = getbytearray(r, st) | A User Theorem |
| getbar-one | ⊦ getbytearray(r, i, 1, st) = st[r -- i '] .byteval ' | A User Theorem |
| getbar-put | ⊦ rk .ref ≠ r ∨ rk .ref = r ∧ (is_fskey(rk .key) ∨ rk .key .index < i ∨ i + j ≤ rk .key .index) → getbytearray(r, i, j, st[rk, val]) = getbytearray(r, i, j, st) | A User Theorem |
| getbar-put-01 | ⊦ fs ' ≠ _length → getbytearray(r, st[r0 -- (sks + fs ' '), val]) = getbytearray(r, st) | A User Theorem |
| getbar-put-02 | ⊦ getbytearray(r, 0, j, st[r0 -- j ', val]) = getbytearray(r, 0, j, st) | A User Theorem |
| getbar-put-03 | str ≠ `*Array*' ⊦ getbytearray(r, st[r0 -- (sks + mkfs(((* str)) .class, ty, fieldvar) ' '), val]) = getbytearray(r, st) | A User Theorem |
| getbar-put-04 | str ≠ `*Array*' ⊦ getbytearray(r, st[r0 -- mkfs(((* str)) .class, ty, fieldvar) ', val]) = getbytearray(r, st) | A User Theorem |
| getbar-put-lower | ⊦ i0 < i → getbytearray(r, i, j, st[r0 -- i0 ', val]) = getbytearray(r, i, j, st) | A User Theorem |
| getbar-put-other | ⊦ i0 < i ∨ i + j ≤ i0 → getbytearray(r, i, j, st[r0 -- i0 ', val]) = getbytearray(r, i, j, st) | A User Theorem |
| getbar-putbar | ⊦ r ≠ r1 → getbytearray(r, putByteArray(bytes, r1, st)) = getbytearray(r, st) | A User Theorem |
| getbar-putbar-01 | ⊦ st[r -- _length] .intval = n→i(# bytes) ∧ st = putByteArray(bytes, r, st0) → getbytearray(r, st) = bytes | A User Theorem |
| getbar-putbar-same | ⊦ n→i(# bytes) = st[r -- _length] .intval → getbytearray(r, putByteArray(bytes, r, st)) = bytes | A User Theorem |
| getbar-putbar-same-01 | ⊦ getbytearray(r, i, n→i(# bytes), putByteArray(bytes, r, i, st)) = bytes | A User Theorem |
| getbar-rec | ⊦ 0 < j → getbytearray(r, i, j, st) = st[r -- i '] .byteval + getbytearray(r, i + 1, j - 1, st) | A User Theorem |
| getbar-ref | ⊦ r ≠ r0 → getbytearray(r, i, j, st[r0 -- sk, val]) = getbytearray(r, i, j, st) | A User Theorem |
| getbar-restn | ⊦ n→i(n) ≤ st[r -- _length] .intval → # restn(n, getbytearray(r, st)) = i→n(st[r -- _length] .intval - n→i(n)) | A User Theorem |
| getbar-restn-01 | ⊦ n→i(n) ≤ st[r -- _length] .intval → restn(n, getbytearray(r, st)) = getbytearray(r, n→i(n), st[r -- _length] .intval - n→i(n), st) | A User Theorem |
| getbar-restn-02 | n→i(n) ≤ st[r -- _length] .intval ⊦ # restn((* n), getbytearray(r, st)) = i→n(st[r -- _length] .intval - n→i(n)) | A User Theorem |
| getbar-restn-03 | n→i(n) ≤ st[r -- _length] .intval ⊦ restn((* n), getbytearray(r, st)) = getbytearray(r, n→i(n), st[r -- _length] .intval - n→i(n), st) | A User Theorem |
| getbar-restn-04 | 0 ≤ i ∧ 0 ≤ j ∧ n→i(n) ≤ j ⊦ restn((* n), mkjavavalues(getbytearray(r, i, j, st))) = mkjavavalues(getbytearray(r, n→i(n) + i, j - n→i(n), st)) | A User Theorem |
| getbar-union | ⊦ st .refs ∩ st0 .refs = ∅ ∧ r ∈ st0 → getbytearray(r, st ∪ st0) = getbytearray(r, st0) | A User Theorem |
| getbar-union-01 | ⊦ ¬ r ∈ st → getbytearray(r, st ∪ st0) = getbytearray(r, st0) | A User Theorem |
| getbar-union-02 | ⊦ st .refs ∩ st0 .refs = ∅ ∧ r ∈ st0 → getbytearray(r, i, j, st ∪ st0) = getbytearray(r, i, j, st0) | A User Theorem |
| getbar-union-03 | ⊦ ¬ r ∈ st → getbytearray(r, i, j, st ∪ st0) = getbytearray(r, i, j, st0) | A User Theorem |
| getbyte-putbyte | ⊦ st[r -- _length] .intval = n→i(# bytes) → getbytearray(r, putByteArray(bytes, r, 0, st)) = bytes | A User Theorem |
| getbytearray-length-zero | ⊦ st[r -- _length] .intval = 0 → getbytearray(r, st) = [] | A User Theorem |
| getbytearray-one | ⊦ st[r -- _length] .intval = 1 → getbytearray(r, st) = st[r -- 0 '] .byteval ' | A User Theorem |
| getbytearray-put | ⊦ r ≠ r0 ∨ fs ' ≠ _type ∧ fs ' ≠ _length → getbytearray(r, st[r0 -- fs ', val]) = getbytearray(r, st) | A User Theorem |
| getbytearray-put-index-length | ⊦ # getbytearray(r, st[r0 -- i ', val]) = # getbytearray(r, st) | A User Theorem |
| getbytearray-putbar-length | ⊦ # getbytearray(r, putByteArray(bytes, r0, i, st)) = # getbytearray(r, st) | A User Theorem |
| getbytearray-subset | ⊦ st ⊆ st0 ∧ is_arrayref(r, i + j, st) ∧ 0 ≤ i → getbytearray(r, i, j, st) = getbytearray(r, i, j, st0) | A User Theorem |
| getintarray-at | ⊦ n < # getintarray(r, i, j, st) → (getintarray(r, i, j, st)[n]) = st[r -- (i + n→i(n)) '] .intval | A User Theorem |
| getintarray-empty | ⊦ getintarray(r, i, 0, st) = [] | A User Theorem |
| getintarray-empty-01 | ⊦ j < 0 → getintarray(r, i, j, st) = [] | A User Theorem |
| getintarray-empty-02 | ⊦ getintarray(r, i, j, st) = [] ↔ j ≤ 0 | A User Theorem |
| getintarray-in | ⊦ i ∈ getintarray(r, st) ↔ (∃ j. i = st[r -- j '] .intval ∧ 0 ≤ j ∧ j < st[r -- _length] .intval) | A User Theorem |
| getintarray-in-01 | ⊦ 0 ≤ i ∧ i < st[r -- _length] .intval → (¬ st[r -- i '] .intval ∈ getintarray(r, st) ↔ false) | A User Theorem |
| getintarray-in-02 | ⊦ i ∈ getintarray(r, i0, j, st) ↔ (∃ j0. i = st[r -- (i0 + j0) '] .intval ∧ 0 ≤ j0 ∧ j0 < j) | A User Theorem |
| getintarray-length | ⊦ 0 ≤ j → # getintarray(r, i, j, st) = i→n(j) | A User Theorem |
| getintarray-length-01 | ⊦ 0 ≤ st[r -- _length] .intval → # getintarray(r, st) = i→n(st[r -- _length] .intval) | A User Theorem |
| getintarray-length-rew | ⊦ j = st[r -- _length] .intval → getintarray(r, 0, j, st) = getintarray(r, st) | A User Theorem |
| getintarray-max-len | ⊦ max(getintarray(r, 0, st[r -- _length] .intval, st)) ≠ max(getintarray(r, st)) ↔ false | A User Theorem |
| getintarray-max-rec | ⊦ max(getintarray(r, 0, i, st)) < st[r -- i '] .intval ∧ 0 < i → max(getintarray(r, 0, i + 1, st)) = st[r -- i '] .intval | A User Theorem |
| getintarray-max-rec-01 | ⊦ st[r -- i '] .intval ≤ max(getintarray(r, 0, i, st)) ∧ 0 < i → max(getintarray(r, 0, i + 1, st)) = max(getintarray(r, 0, i, st)) | A User Theorem |
| getintarray-one | ⊦ getintarray(r, 0, 1, st) = st[r -- 0 '] .intval ' | A User Theorem |
| getintarray-put-lower | ⊦ j0 < i → getintarray(r, i, j, st[r -- j0 ', val]) = getintarray(r, i, j, st) | A User Theorem |
| getintarray-put-other | ⊦ r ≠ r0 → getintarray(r, i, j, st[r0 -- sk, val]) = getintarray(r, i, j, st) | A User Theorem |
| getintarray-put-other-01 | ⊦ r ≠ r0 → getintarray(r, st[r0 -- sk, val]) = getintarray(r, st) | A User Theorem |
| getintarray-put-other-02 | ⊦ i < 0 ∨ st[r -- _length] .intval < i → getintarray(r, st[r -- i ', val]) = getintarray(r, st) | A User Theorem |
| getintarray-put-other-03 | ⊦ j0 < i ∨ i + j ≤ j0 → getintarray(r, i, j, st[r -- j0 ', val]) = getintarray(r, i, j, st) | A User Theorem |
| getintarray-put-upper | ⊦ i + j ≤ j0 → getintarray(r, i, j, st[r -- j0 ', val]) = getintarray(r, i, j, st) | A User Theorem |
| getintarray-put-upper-01 | ⊦ j ≤ j0 → getintarray(r, 0, j, st[r -- j0 ', val]) = getintarray(r, 0, j, st) | A User Theorem |
| getintarray-put-upper-02 | ⊦ getintarray(r, 0, j - 1, st[r -- j ', val]) = getintarray(r, 0, j - 1, st) | A User Theorem |
| getintarray-rec-first | ⊦ 0 < j → getintarray(r, i, j, st) = st[r -- i '] .intval + getintarray(r, i + 1, j - 1, st) | A User Theorem |
| getintarray-rec-last | ⊦ 0 < j → getintarray(r, i, j, st) = getintarray(r, i, j - 1, st) + st[r -- (i + j - 1) '] .intval | A User Theorem |
| getintarray-subset | ⊦ st ⊆ st0 ∧ is_arrayref(r, st[r -- _length] .intval, st) ∧ r -- _length ∈ st → getintarray(r, st) = getintarray(r, st0) | A User Theorem |
| getintarray-subset-01 | ⊦ st ⊆ st0 ∧ is_arrayref(r, i + j, st) ∧ 0 ≤ i → getintarray(r, i, j, st) = getintarray(r, i, j, st0) | A User Theorem |
| getintarray-zero | ⊦ st[r -- _length] .intval = 0 → getintarray(r, st) = [] | A User Theorem |
| is_arrayref-01 | ⊦ is_arrayref(r, i, st[_out, val]) ↔ is_arrayref(r, i, st) | A User Theorem |
| is_arrayref-02 | ⊦ is_arrayref(r, i, st[_mode, val]) ↔ is_arrayref(r, i, st) | A User Theorem |
| is_arrayref-03 | ⊦ is_arrayref(r, i, st) → is_arrayref(r, i, st[r -- j ', val]) | A User Theorem |
| isarray | ⊦ r ≠ r0 → (is_arrayref(r, i, st[r0 -- sk, val0]) ↔ is_arrayref(r, i, st)) | A User Theorem |
| isarray-01 | ⊦ i < 0 → is_arrayref(r, i, st) | A User Theorem |
| isarray-02 | ⊦ i ≤ j → (is_arrayref(r, i, st[r0 -- j ', val]) ↔ is_arrayref(r, i, st)) | A User Theorem |
| isarray-03 | ⊦ is_arrayref(r, 1, st) ↔ r -- 0 ' ∈ st | A User Theorem |
| isarrayref-del | ⊦ r ≠ r0 → (is_arrayref(r0, i, st -- r) ↔ is_arrayref(r0, i, st)) | A User Theorem |
| isarrayref-mod | ⊦ ¬ is_arrayref(r, i, st0) ∧ onlyModified(r0, st, st0) ∧ r ≠ r0 → ¬ is_arrayref(r, i, st) | A User Theorem |
| isarrayref-put | ⊦ is_fskey(rk .key) → (is_arrayref(r, i, st[rk, val]) ↔ is_arrayref(r, i, st)) | A User Theorem |
| isarrayref-putbar-other | ⊦ r ≠ r1 → (is_arrayref(r, i0, putByteArray(bytes, r1, i, st)) ↔ is_arrayref(r, i0, st)) | A User Theorem |
| pubBar-init | ⊦ initdone(class, putByteArray(bytes, r, i, st)) ↔ initdone(class, st) | A User Theorem |
| putAr-get-other | ⊦ 0 ≤ i ∧ i→n(i) + # vals ≤ i→n(j) → (putArray(vals, r, i, st)[r -- j ']) = st[r -- j '] | A User Theorem |
| putAr-get-other-01 | ⊦ 0 ≤ i ∧ i→n(i) + # vals ≤ i→n(j) → (putArray(vals, r, i, st)[r1 -- j ']) = st[r1 -- j '] | A User Theorem |
| putAr-lastrec | ⊦ putArray(vals + val ', r, i, st) = putArray(vals, r, i, st[r -- (i + n→i(# vals)) ', val]) | A User Theorem |
| putArray-append | ⊦ putArray(vals + vals0, r, i, st) = putArray(vals, r, i, putArray(vals0, r, i + n→i(# vals), st)) | A User Theorem |
| putArray-at | ⊦ is_fskey(sk) → (putArray(vals, r, i, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| putArray-at-in | ⊦ i ≤ j ∧ j < i + n→i(# vals) → (putArray(vals, r, i, st)[r -- j ']) = vals[i→n(j - i)] | A User Theorem |
| putArray-in | ⊦ rk ∈ putArray(vals, r, i, st) ↔ rk ∈ st ∨ rk .ref = r ∧ is_indexkey(rk .key) ∧ i ≤ rk .key .index ∧ rk .key .index < i + n→i(# vals) | A User Theorem |
| putArray-one | ⊦ putArray(val ', r, j, st) = st[r -- j ', val] | A User Theorem |
| putArray-put | ⊦ 0 ≤ j ∧ i = n→i(# vals) → (putArray(vals, r, j, st)[r -- (j + i) ', val]) = putArray(vals + val, r, j, st) | A User Theorem |
| putArray-put-switch | ⊦ 0 ≤ j ∧ 0 ≤ i ∧ i + n→i(# vals) ≤ j → putArray(vals, r, i, st[r -- j ', val]) = (putArray(vals, r, i, st)[r -- j ', val]) | A User Theorem |
| putArray-put-switch-01 | ⊦ putArray(vals, r, i, st[r0 -- fs ', val]) = (putArray(vals, r, i, st)[r0 -- fs ', val]) | A User Theorem |
| putArray-put-switch-02 | ⊦ is_fskey(sk) ∨ r0 ≠ r → putArray(vals, r, i, st[r0 -- sk, val]) = (putArray(vals, r, i, st)[r0 -- sk, val]) | A User Theorem |
| putBar-at | ⊦ is_fskey(sk) → (putByteArray(bytes, r, i, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| putBar-at-fskey | ⊦ is_fskey(sk) → (putByteArray(bytes, r, i, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| putBar-at-len | ⊦ (putByteArray(bytes, r, i, st)[r0 -- _length]) = st[r0 -- _length] | A User Theorem |
| putBar-at-mode | ⊦ (putByteArray(bytes, r, i, st)[_mode]) = st[_mode] | A User Theorem |
| putBar-at-type | ⊦ (putByteArray(bytes, r, i, st)[r0 -- _type]) = st[r0 -- _type] | A User Theorem |
| putBar-empty | ⊦ putByteArray([], r, i, st) = st | A User Theorem |
| putBar-in | ⊦ rk ∈ putByteArray(bytes, r, i, st) ↔ rk ∈ st ∨ rk .ref = r ∧ is_indexkey(rk .key) ∧ i ≤ rk .key .index ∧ rk .key .index < i + n→i(# bytes) | A User Theorem |
| putBar-lastrec | ⊦ putByteArray(bytes + by ', r, i, st) = putByteArray(bytes, r, i, st[r -- (i + n→i(# bytes)) ', byteval(by)]) | A User Theorem |
| putBar-one | ⊦ putByteArray(by ', r, i, st) = st[r -- i ', byteval(by)] | A User Theorem |
| putBar-rec | ⊦ bytes ≠ [] → putByteArray(bytes, r, i, st) = (putByteArray(bytes .rest, r, i + 1, st)[r -- i ', byteval(bytes .first)]) | A User Theorem |
| putBar-rew | ⊦ j < i ∨ i + n→i(# bytes) ≤ j → (putByteArray(bytes, r, i, st)[r -- j ', val]) = putByteArray(bytes, r, i, st[r -- j ', val]) | A User Theorem |
| putBar-rew-01 | ⊦ putByteArray(bytes, r, i, st[r0 -- fs ', val]) = (putByteArray(bytes, r, i, st)[r0 -- fs ', val]) | A User Theorem |
| putBar-unrec | ⊦ j = i - 1 ∧ is_bytevalue(val) → (putByteArray(bytes, r, i, st)[r -- j ', val]) = putByteArray(val .byteval ' + bytes, r, i - 1, st) | A User Theorem |
| putByteArray-append | ⊦ 0 ≤ i ∧ 0 ≤ j ∧ j + n→i(# bytes0) = i → putByteArray(bytes, r, i, putByteArray(bytes0, r, j, st)) = putByteArray(bytes0 + bytes, r, j, st) | A User Theorem |
| putByteArray-put-switch | ⊦ 0 ≤ j ∧ 0 ≤ i ∧ j < i → putByteArray(bytes, r, i, st[r -- j ', byteval(by)]) = (putByteArray(bytes, r, i, st)[r -- j ', byteval(by)]) | A User Theorem |
| putByteArray-put-switch-01 | ⊦ 0 ≤ j ∧ 0 ≤ i ∧ j + 1 = i → putByteArray(bytes, r, i, st[r -- j ', byteval(by)]) = putByteArray(by + bytes, r, j, st) | A User Theorem |
| putar-at | ⊦ j ≤ i ∧ i < n→i(# vals) + j → (putArray(vals, r, j, st)[r -- i ']) = vals[i→n(i - j)] | A User Theorem |
| putar-atfs | ⊦ (putArray(vals, r, j, st)[r0 -- fs ']) = st[r0 -- fs '] | A User Theorem |
| putar-atother | ⊦ i < j ∨ n→i(# vals) + j ≤ i → (putArray(vals, r, j, st)[r0 -- i ']) = st[r0 -- i '] | A User Theorem |
| putar-atref | ⊦ r ≠ r0 → (putArray(vals, r, j, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| putar-getar | ⊦ j = n→i(# vals) → getarray(r, i, j, putArray(vals, r, i, st)) = vals | A User Theorem |
| putar-getar-01 | ⊦ r ≠ r0 → getarray(r, i, j, putArray(vals, r0, i, st)) = getarray(r, i, j, st) | A User Theorem |
| putar-getar-02 | ⊦ r ≠ r0 → getarray(r, i, j, putArray(vals, r0, i0, st)) = getarray(r, i, j, st) | A User Theorem |
| putar-in | ⊦ r1 ∈ putArray(vals, r0, i0, st) ↔ r1 ∈ st ∨ r1 = r0 ∧ vals ≠ [] | A User Theorem |
| putar-in-01 | ⊦ rk ∈ st → rk ∈ putArray(vals, r, i, st) | A User Theorem |
| putar-in-02 | ⊦ r -- j ' ∈ putArray(vals, r, i, st) ↔ r -- j ' ∈ st ∨ i ≤ j ∧ j < i + n→i(# vals) | A User Theorem |
| putar-infs | ⊦ r0 -- fs ' ∈ putArray(vals, r, j, st) ↔ r0 -- fs ' ∈ st | A User Theorem |
| putar-inother | ⊦ i < j ∨ n→i(# vals) + j ≤ i → (r0 -- i ' ∈ putArray(vals, r, j, st) ↔ r0 -- i ' ∈ st) | A User Theorem |
| putar-inref | ⊦ r ≠ r0 → (r0 -- sk ∈ putArray(vals, r, j, st) ↔ r0 -- sk ∈ st) | A User Theorem |
| putar-rew | ⊦ rk .ref ≠ r ∨ is_fskey(rk .key) ∨ rk .key .index < j ∨ n→i(# vals) + j ≤ rk .key .index → (putArray(vals, r, j, st)[rk, val]) = putArray(vals, r, j, st[rk, val]) | A User Theorem |
| putarray-field | ⊦ is_fskey(sk) → (putArray(vals, r, i, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| putarray-length | ⊦ (putArray(vals, r, i, st)[r0 -- _length]) = st[r0 -- _length] | A User Theorem |
| putarray-mode | ⊦ (putArray(vals, r, i, st)[_mode]) = st[_mode] | A User Theorem |
| putarray-subset-new | ⊦ ¬ r ∈ st → (st ⊆ putArray(vals, r, st0) ↔ st ⊆ st0) | A User Theorem |
| putarray-subset-new-01 | ⊦ ¬ r ∈ st → (st ⊆ putArray(vals, r, i, st0) ↔ st ⊆ st0) | A User Theorem |
| putarray-type | ⊦ (putArray(vals, r, i, st)[r0 -- _type]) = st[r0 -- _type] | A User Theorem |
| putbar-atfs | ⊦ (putByteArray(bytes, r, st)[r0 -- fs ']) = st[r0 -- fs '] | A User Theorem |
| putbar-atfs-01 | ⊦ (putByteArray(bytes, r, j, st)[r0 -- fs ']) = st[r0 -- fs '] | A User Theorem |
| putbar-atother | ⊦ i < 0 ∨ n→i(# bytes) ≤ i → (putByteArray(bytes, r, st)[r0 -- i ']) = st[r0 -- i '] | A User Theorem |
| putbar-atother-01 | ⊦ i < j ∨ n→i(# bytes) + j ≤ i → (putByteArray(bytes, r, j, st)[r0 -- i ']) = st[r0 -- i '] | A User Theorem |
| putbar-atref | ⊦ r ≠ r0 → (putByteArray(bytes, r, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| putbar-atref-01 | ⊦ r ≠ r0 → (putByteArray(bytes, r, j, st)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| putbar-byte | ⊦ i ≤ j ∧ j < i + n→i(# bytes) → (putByteArray(bytes, r, i, st)[r -- j ']) = byteval(bytes[i→n(j - i)]) | A User Theorem |
| putbar-getbar | ⊦ j = n→i(# bytes) → getbytearray(r, i, j, putByteArray(bytes, r, i, st)) = bytes | A User Theorem |
| putbar-getbar-01 | ⊦ r ≠ r0 → getbytearray(r, i, j, putByteArray(bytes, r0, i, st)) = getbytearray(r, i, j, st) | A User Theorem |
| putbar-getbar-02 | ⊦ r ≠ r0 → getbytearray(r, i, j, putByteArray(bytes, r0, i0, st)) = getbytearray(r, i, j, st) | A User Theorem |
| putbar-getbar-03 | ⊦ r ≠ r0 → getbytearray(r, putByteArray(bytes, r0, i0, st)) = getbytearray(r, st) | A User Theorem |
| putbar-getbar-le | ⊦ j ≤ n→i(# bytes) ∧ 0 ≤ j → getbytearray(r, i, j, putByteArray(bytes, r, i, st)) = firstn(i→n(j), bytes) | A User Theorem |
| putbar-in | ⊦ r1 ∈ putByteArray(bytes, r0, i0, st) ↔ r1 ∈ st ∨ r1 = r0 ∧ bytes ≠ [] | A User Theorem |
| putbar-in-01 | ⊦ rk ∈ st → rk ∈ putByteArray(bytes, r, i, st) | A User Theorem |
| putbar-in-02 | ⊦ r -- j ' ∈ putByteArray(bytes, r, i, st) ↔ r -- j ' ∈ st ∨ i ≤ j ∧ j < i + n→i(# bytes) | A User Theorem |
| putbar-infs | ⊦ r0 -- fs ' ∈ putByteArray(bytes, r, j, st) ↔ r0 -- fs ' ∈ st | A User Theorem |
| putbar-infs-01 | ⊦ r0 -- fs ' ∈ putByteArray(bytes, r, st) ↔ r0 -- fs ' ∈ st | A User Theorem |
| putbar-inother | ⊦ i < j ∨ n→i(# bytes) + j ≤ i → (r0 -- i ' ∈ putByteArray(bytes, r, j, st) ↔ r0 -- i ' ∈ st) | A User Theorem |
| putbar-inother-01 | ⊦ i < 0 ∨ n→i(# bytes) ≤ i → (r0 -- i ' ∈ putByteArray(bytes, r, st) ↔ r0 -- i ' ∈ st) | A User Theorem |
| putbar-inref | ⊦ r ≠ r0 → (r0 -- sk ∈ putByteArray(bytes, r, j, st) ↔ r0 -- sk ∈ st) | A User Theorem |
| putbar-inref-01 | ⊦ r ≠ r0 → (r0 -- sk ∈ putByteArray(bytes, r, st) ↔ r0 -- sk ∈ st) | A User Theorem |
| putbar-len | ⊦ (putByteArray(bytes, r, st)[r1 -- _length]) = st[r1 -- _length] | A User Theorem |
| putbar-len-01 | ⊦ (putByteArray(bytes, r, i, st)[r1 -- _length]) = st[r1 -- _length] | A User Theorem |
| putbar-override | ⊦ 0 ≤ j ∧ 0 ≤ j0 ∧ j ≤ j0 ∧ j0 + n→i(# bytes0) ≤ j + n→i(# bytes) → putByteArray(bytes, r1, j, putByteArray(bytes0, r1, j0, st)) = putByteArray(bytes, r1, j, st) | A User Theorem |
| putbar-put-mode | ⊦ (putByteArray(bytes, r, st)[_mode]) = st[_mode] | A User Theorem |
| putbar-put-override | ⊦ 0 ≤ j ∧ bytes ≠ [] ∧ j ≤ i ∧ i < j + n→i(# bytes) → putByteArray(bytes, r, j, st[r -- i ', byteval(by)]) = putByteArray(bytes, r, j, st) | A User Theorem |
| putbar-refval | ⊦ st[r1 -- i0 '] ≠ refval(r0) → (putByteArray(bytes, r1, i, st)[r1 -- i0 ']) ≠ refval(r0) | A User Theorem |
| putbytearray-in | ⊦ r -- _type ∈ putByteArray(bytes, r0, i, st) ↔ r -- _type ∈ st | A User Theorem |
| putbytearray-init | ⊦ init(str, putByteArray(bytes, r, i, st)) ↔ init(str, st) | A User Theorem |
| putbytearray-subset-new | ⊦ ¬ r ∈ st → (st ⊆ putByteArray(bytes, r, st0) ↔ st ⊆ st0) | A User Theorem |
| putbytearray-subset-new-01 | ⊦ ¬ r ∈ st → (st ⊆ putByteArray(bytes, r, i, st0) ↔ st ⊆ st0) | A User Theorem |
| stsub-copy | ⊦ newref(r0, st) → (st ⊆ arraycopy(r, i, r0, i0, j, st0) ↔ st ⊆ st0) | A User Theorem |
| sublist-getbar | ⊦ n→i(n) + n→i(n0) ≤ st[r -- _length] .intval → sublist(n, n0, getbytearray(r, st)) = getbytearray(r, n→i(n), n→i(n0), st) | A User Theorem |