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: |
|---|---|---|
| intssize-empty | ⊦ ints#([]) = 0 | An Axiom |
| intssize-rec | ⊦ ints#(i ' + ints) = 1 + i→n(i) + ints#(ints) | An Axiom |
| countrefs_one | ⊦ # ints ≤ 1 → countrefs2(ints) = 0 | An Axiom |
| countrefs_more_le0 | ⊦ # ints > 1 ∧ ints .first ≤ 0 → countrefs2(ints) = 0 | An Axiom |
| countrefs_more_gr0 | ⊦ # ints > 1 ∧ ints .first > 0 → countrefs2(ints) = ints .first + ints .first * countrefs2(ints .rest) | An Axiom |
| addarraymultlist_zero | ⊦ # ints = 0 → addarraymultlist(r, ty, st, refs, ints, ints0, i) = st | An Axiom |
| addarraymultlist_one_0 | ⊦ # ints = 1 ∧ ints .first ≤ 0 → addarraymultlist(r, ty, st, refs, ints, ints0, i) = (st[r -- _type, typeval(mktype_from_dims(ty, n→i(# ints) + i))][r -- _length, intval(ints0 .first)]) | An Axiom |
| addarraymultlist_one_not_0 | ⊦ # ints = 1 ∧ ints .first > 0 → addarraymultlist(r, ty, st, refs, ints, ints0, i) = addarray(r, mktype_from_dims(ty, i), ints0 .first, st) | An Axiom |
| addarraymultlist_more_0 | ⊦ # ints > 1 ∧ ints .first ≤ 0 → addarraymultlist(r, ty, st, refs, ints, ints0, i) = (st[r -- _type, typeval(mktype_from_dims(ty, n→i(# ints) + i))][r -- _length, intval(ints0 .first)]) | An Axiom |
| addarraymultlist_more_2 | ⊦ # ints > 1 ∧ ints .first ≥ 1 + 1 → addarraymultlist(r, ty, st, refs, ints, ints0, i) = addarraymultlist (refs .first, ty, addarraymultlist (r, ty, st[r -- (ints .first - 1) ', refval(refs .first)][r -- _type, typeval(mktype_from_dims(ty, i + n→i(# ints)))] [r -- _length, intval(ints0 .first) ], refs .rest, (ints .first - 1) + ints .rest, ints0, i), restn(i→n(countrefs2((ints .first - 1) + ints .rest)), refs .rest), ints .rest, ints0 .rest, i) | An Axiom |
| addarraymultlist_more_1 | ⊦ # ints > 1 ∧ ints .first = 1 → addarraymultlist(r, ty, st, refs, ints, ints0, i) = addarraymultlist (refs .first, ty, st[r -- (ints .first - 1) ', refval(refs .first)][r -- _type, typeval(mktype_from_dims(ty, i + n→i(# ints)))][r -- _length, intval(ints0 .first)], refs .rest, ints .rest, ints0 .rest, i) | An Axiom |
| addarraymult | ⊦ addarraymult(r, ty, st, refs, ints, i) = addarraymultlist(r, ty, st, refs, ints, ints, i) | An Axiom |
| addmultiarrays-rec | ⊦ i > 0 ∧ # ints > 1 → addmultiarrays(refs, i, acc, ty, ints, st) = addmultiarrays (firstn(# refs - i→n(countrefs(ints .rest)), refs), i - 1, lastn(i→n(countrefs(ints .rest)), refs) .first + acc, ty, ints, addmultiarrays(lastn(i→n(countrefs(ints .rest)), refs), ints .rest .first, [], ty, ints .rest, st)) | An Axiom |
| addmultiarrays-done | ⊦ i = 0 ∧ # ints > 1 → addmultiarrays(refs, i, acc, ty, ints, st) = addarray(refs .first, mktype_from_dims(ty, n→i(# ints) - 1), mkjavavalues(acc), st) | An Axiom |
| addmultiarrays-base | ⊦ # ints = 1 → addmultiarrays(refs, i, acc, ty, ints, st) = addarray(refs .first, ty, ints .first, st) | An Axiom |
| getdims-rec | ⊦ 0 < j → getdims(j ' + ints) = j ' + getdims(ints) | An Axiom |
| getdims-zero | ⊦ j ≤ 0 → getdims(j ' + ints) = 0 ' | An Axiom |
| getdims-empty | ⊦ getdims([]) = [] | An Axiom |
| countdims-rec | ⊦ 0 < j → countdims(j ' + ints, i) = countdims(ints, i) | An Axiom |
| countdims-zero | ⊦ j ≤ 0 → countdims(j ' + ints, i) = i + n→i(# ints) | An Axiom |
| countdims-empty | ⊦ countdims([], i) = i | An Axiom |
| countrefs-rec | ⊦ # ints > 1 ∧ ints .first > 0 → countrefs(ints) = 1 + ints .first * countrefs(ints .rest) | An Axiom |
| countrefs-zero-01 | ⊦ # ints > 1 ∧ ints .first ≤ 0 → countrefs(ints) = 1 | An Axiom |
| countrefs-base | ⊦ # ints ≤ 1 → countrefs(ints) = 1 | An Axiom |
| addarrays-empty | ⊦ ints = [] ∨ n→i(# refs) ≠ countrefs(ints) ∨ ¬ posints(ints) → addarrays(refs, ty, ints, i, st) = st | An Axiom |
| addarrays-def | ⊦ ints ≠ [] ∧ n→i(# refs) = countrefs(ints) ∧ posints(ints) → addarrays(refs, ty, ints, i, st) = addmultiarrays(refs, ints .first, [], mktype_from_dims(ty, countdims(ints, i)), getdims(ints), st) | An Axiom |
| addarrays-at-other | ⊦ ¬ r ∈ refs ∧ # refs = i→n(countrefs(ints)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) → (addarrays(refs, ty, ints, i, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| addarrays-at-other-01 | ⊦ r ∈ st ∧ posints(ints) → (addarrays(newref_list(i→n(countrefs(ints)), st), ty, ints, i, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| addarrays-auto-22 | ⊦ addarrays(refs, ty, 2 ' + 2 ', 0, st) = ((# refs = 3 ⊃ addarray (refs .first, mkarraytype(ty), refval(refs .rest .first) ' + refval(refs[2]) ', addarray(refs[1], ty, 2, addarray(refs .rest .rest .first, ty, 2, st))) ; st ) ) | A User Theorem |
| addarrays-case | ⊦ addarrays(refs, ty, ints, i, st) = (((ints ≠ [] ∧ n→i(# refs) = countrefs(ints) ∧ posints(ints)) ⊃ addmultiarrays(refs, ints .first, [], mktype_from_dims(ty, countdims(ints, i)), getdims(ints), st) ; st ) ) | A User Theorem |
| addarrays-fieldat | ⊦ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type → (addarrays(refs, ty, ints, i, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| addarrays-fieldin | ⊦ is_fskey(sk) ∧ sk ≠ _length ∧ sk ≠ _type → (r -- sk ∈ addarrays(refs, ty, ints, i, st) ↔ r -- sk ∈ st) | A User Theorem |
| addarrays-initdone | ⊦ initdone(class, addarrays(refs, ty, ints, i, st)) ↔ initdone(class, st) | A User Theorem |
| addarrays-jvmref | ⊦ jvmref -- sk ∈ addarrays(newref_list(i→n(countrefs(ints)), st), ty, ints, i, st) ↔ jvmref -- sk ∈ st | A User Theorem |
| addarrays-length | ⊦ posints(ints) ∧ ints ≠ [] ∧ 0 ≤ i ∧ n→i(# (r ' + refs)) = countrefs(ints) ∧ is_newref_list(r ' + refs, st) → (addarrays(r ' + refs, ty, ints, i, st)[r -- _length]) = intval(ints .first) | A User Theorem |
| addarrays-length-01 | posints(ints), ints ≠ [] ⊦ 1 + n→i(# refs) = countrefs(ints) ∧ newref(r, st) ∧ is_newref_list(refs, st) ∧ ¬ r ∈ refs → (addarrays(r ' + refs, ty, ints, 0, st)[r -- _length]) = intval(ints .first) | A User Theorem |
| addarrays-mode | ⊦ (addarrays(refs, ty, ints, i, st)[_mode]) = st[_mode] | A User Theorem |
| addarrays-mode-01 | ⊦ _mode ∈ addarrays(refs, ty, ints, i, st) ↔ _mode ∈ st | A User Theorem |
| addarrays-one | ⊦ 0 ≤ i → addarrays(r ', ty, i ', j, st) = addarray(r, mktype_from_dims(ty, countdims(i ', j)), i, st) | A User Theorem |
| addarrays-one-01 | 0 ≤ i ⊦ addarrays(r ', ty, ((* i)) ', (* j), st) = addarray(r, mktype_from_dims(ty, countdims(i ', j)), i, st) | A User Theorem |
| addarrays-out | ⊦ (addarrays(refs, ty, ints, i, st)[_out]) = st[_out] | A User Theorem |
| addarrays-refin | ⊦ ¬ r ∈ refs → (r -- sk ∈ addarrays(refs, ty, ints, i, st) ↔ r -- sk ∈ st) | A User Theorem |
| addarrays-refin-01 | ⊦ rk ∈ st → rk ∈ addarrays(refs, ty, ints, i, st) | A User Theorem |
| addarrays-subset | ⊦ is_newref_list(refs, st) ∧ 0 ≤ i → st ⊆ addarrays(refs, ty, ints, i, st) | A User Theorem |
| addarrays-type | ⊦ posints(ints) ∧ ints ≠ [] ∧ 0 ≤ i ∧ n→i(# (r ' + refs)) = countrefs(ints) ∧ is_newref_list(r ' + refs, st) → (addarrays(r ' + refs, ty, ints, i, st)[r -- _type]) = typeval(mktype_from_dims(ty, n→i(# getdims(ints)) + countdims(ints, i))) | A User Theorem |
| addarrays-type-01 | posints(ints), ints ≠ [] ⊦ 1 + n→i(# refs) = countrefs(ints) ∧ newref(r, st) ∧ is_newref_list(refs, st) ∧ ¬ r ∈ refs → (addarrays(r ' + refs, ty, ints, 0, st)[r -- _type]) = typeval(mktype_from_dims(ty, n→i(# getdims(ints)) + countdims(ints, 0))) | A User Theorem |
| addarrays-typein | ⊦ r ∈ refs ∧ # refs = i→n(countrefs(ints)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) → (addarrays(refs, ty, ints, i, st)[r -- _type]) ≠ typeval(mkclasstype(class)) | A User Theorem |
| addarrays-typein-01 | ⊦ r ∈ refs ∧ # refs = i→n(countrefs(ints)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) → r -- _type ∈ addarrays(refs, ty, ints, i, st) ∧ is_typevalue(addarrays(refs, ty, ints, i, st)[r -- _type]) ∧ is_arraytype((addarrays(refs, ty, ints, i, st)[r -- _type]) .type) | A User Theorem |
| addarrays-typein-02 | ⊦ r ∈ refs ∧ # refs = i→n(countrefs(ints)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) → r -- _type ∈ addarrays(refs, ty, ints, i, st) | A User Theorem |
| addmultiarrays-base-01 | ⊦ addmultiarrays(refs, i, acc, ty, j ', st) = addarray(refs .first, ty, j, st) | A User Theorem |
| addmultidim_empty | ⊦ addarraymultlist(r, ty, st, refs, [], [], i) = st | A User Theorem |
| countdims-notneg | ⊦ 0 ≤ i → ¬ countdims(ints, i) < 0 | A User Theorem |
| countdims-one | ⊦ countdims(1 ' + ints, i) = countdims(ints, i) | A User Theorem |
| countdims-one-01 | ⊦ countdims(1 ', i) = i | A User Theorem |
| countdims-one-02 | 0 < i ⊦ countdims(((* i)) ', j) = j | A User Theorem |
| countdims-one-03 | ⊦ 0 < i → countdims(i ', j) = j | A User Theorem |
| countdims-zero-01 | ⊦ countdims(0 ' + ints, i) = i + n→i(# ints) | A User Theorem |
| countdims-zero-02 | ⊦ countdims(0 ', i) = i | A User Theorem |
| countdims-zero-03 | ⊦ 0 < i → countdims(ints, i) ≠ 0 | A User Theorem |
| countdims-zero-04 | ⊦ 0 < i → ¬ countdims(ints, i) ≤ 0 | A User Theorem |
| countmore2 | 0 < i ⊦ countrefs2(i ' + i0 ' + ints) = i + i * countrefs2(i0 ' + ints) | A User Theorem |
| countrefs-abs | ⊦ abs(countrefs(ints)) = countrefs(ints) | A User Theorem |
| countrefs-auto | ⊦ countrefs(2 ' + 2 ') = 3 | A User Theorem |
| countrefs-empty | ⊦ countrefs([]) = 1 | A User Theorem |
| countrefs-getdims | ⊦ countrefs(getdims(ints)) = countrefs(ints) | A User Theorem |
| countrefs-getdims-01 | ⊦ countrefs(i ' + getdims(ints)) = countrefs(i ' + ints) | A User Theorem |
| countrefs-i2n | ⊦ 0 ≤ i2 → i→n(1 + (i2 + 1) * countrefs(ints)) = 1 + i→n(i2 + 1) * i→n(countrefs(ints)) | A User Theorem |
| countrefs-i2n-01 | ⊦ 0 ≤ i → i→n(1 + countrefs(ints) * i) = 1 + i→n(countrefs(ints)) * i→n(i) | A User Theorem |
| countrefs-i2n-02 | ⊦ 0 < i → i→n(1 + countrefs(ints) * i) = 1 + i→n(countrefs(ints)) * i→n(i) | A User Theorem |
| countrefs-inrefs | ⊦ # refs = n + m ∧ ¬ r ∈ refs → ¬ r ∈ firstn(n, refs) | A User Theorem |
| countrefs-lastn | ⊦ # refs2 = i→n(countrefs(i1 ' + ints1)) * i→n(i2) + i→n(countrefs(i1 ' + ints1)) ∧ lastn(i→n(countrefs(i1 ' + ints1)), r1 ' + refs2) = r0 ' + refs1 ∧ 0 ≤ i2 → ¬ # refs2 ≤ # refs1 | A User Theorem |
| countrefs-lastn-01 | ⊦ ¬ r0 ∈ refs ∧ # refs = 2 + n * m + m0 → lastn(1 + n * m, refs) ≠ r0 ' + refs1 | A User Theorem |
| countrefs-lastn-02 | ⊦ r ∈ refs1 ∧ ¬ r ∈ refs ∧ # refs = 2 + n * m + m0 → lastn(1 + n * m, refs) ≠ r0 ' + refs1 | A User Theorem |
| countrefs-lastn-03 | ⊦ 1 + # refs1 ≠ n ∧ # refs2 = n * m + n → lastn(n, r1 ' + refs2) ≠ r0 ' + refs1 | A User Theorem |
| countrefs-le | ⊦ # refs = i→n(countrefs(i ' + ints)) ∧ 0 < i → ¬ # refs ≤ # refs - i→n(countrefs(ints)) | A User Theorem |
| countrefs-le-01 | ⊦ # refs = i→n(countrefs((i + 1) ' + ints)) ∧ 0 ≤ i → ¬ # refs ≤ # refs - i→n(countrefs(ints)) | A User Theorem |
| countrefs-le-02 | ⊦ 0 < i ∧ ints ≠ [] → ¬ countrefs(i ' + ints) ≤ countrefs(ints) | A User Theorem |
| countrefs-le-03 | ⊦ # refs = i→n(countrefs((i2 + 1) ' + i1 ' + ints1)) ∧ 0 ≤ i2 → ¬ # refs ≤ # refs - i→n(countrefs(i1 ' + ints1)) | A User Theorem |
| countrefs-ls | ⊦ 0 < i → ¬ countrefs(i ' + ints) < countrefs(ints) | A User Theorem |
| countrefs-not-zero | ⊦ ¬ countrefs(ints) < 0 | A User Theorem |
| countrefs-not-zero-01 | ⊦ countrefs(ints) ≠ 0 | A User Theorem |
| countrefs-one | ⊦ countrefs(i ') = 1 | A User Theorem |
| countrefs-rec-01 | ⊦ 0 ≤ i → countrefs((i + 1) ' + i0 ' + ints) = 1 + (i + 1) * countrefs(i0 ' + ints) | A User Theorem |
| countrefs-rec-02 | ⊦ 0 ≤ i2 → i→n(countrefs(i2 ' + i1 ' + ints1)) = i→n(countrefs(i1 ' + ints1)) * i→n(i2) + 1 | A User Theorem |
| countrefs-zero | ⊦ countrefs(0 ' + ints) = 1 | A User Theorem |
| countrefs2 | ⊦ ints ≠ [] ∧ 0 ≤ i → countrefs2((i + 1) ' + ints) = i + 1 + (i + 1) * countrefs2(ints) | A User Theorem |
| countrefs2-01 | ⊦ ints ≠ [] ∧ 1 ≤ i → countrefs2(i ' + ints) = i + i * countrefs2(ints) | A User Theorem |
| countrefs2-02 | ⊦ ints ≠ [] ∧ 0 < i → countrefs2(i ' + ints) = i + i * countrefs2(ints) | A User Theorem |
| countrefs2-03 | ⊦ i→n(countrefs2(ints) + 1) = i→n(countrefs2(ints)) + 1 | A User Theorem |
| countrefs2-empty | ⊦ countrefs2([]) = 0 | A User Theorem |
| countrefs2-not-mone | ⊦ countrefs2(ints) ≠ (~1) | A User Theorem |
| countrefs2-one | ⊦ ints ≠ [] → countrefs2(1 ' + ints) = 1 + countrefs2(ints) | A User Theorem |
| countrefs2-one-01 | ⊦ countrefs2(i ') = 0 | A User Theorem |
| countrefs2-pos | ⊦ ¬ countrefs2(ints) < 0 | A User Theorem |
| countrefs2-pos-01 | ⊦ ¬ countrefs2(ints) + 1 < 0 | A User Theorem |
| countrefs2-two | 0 < i ⊦ countrefs2(i ' + j ') = i | A User Theorem |
| countrefs2-zero | ⊦ countrefs2(0 ' + ints) = 0 | A User Theorem |
| endfinallymode | ⊦ (addarrays(refs, ty, ints, i, st)[_endfinallymode]) = st[_endfinallymode] | A User Theorem |
| endfinallymode-01 | ⊦ _endfinallymode ∈ addarrays(refs, ty, ints, i, st) ↔ _endfinallymode ∈ st | A User Theorem |
| getcountdims | ⊦ n→i(# getdims(ints)) + countdims(ints, i) = n→i(# ints) + i | A User Theorem |
| getdims-empty-01 | ⊦ getdims(ints) = [] ↔ ints = [] | A User Theorem |
| getdims-posints | ⊦ posints(ints) → posints(getdims(ints)) | A User Theorem |
| getdims-posints-01 | ⊦ ¬ posints(getdims(ints)) ↔ false | A User Theorem |
| getdims-zero-01 | ⊦ getdims(0 ' + ints) = 0 ' | A User Theorem |
| getdims-zero-02 | ⊦ getdims(0 ') = 0 ' | A User Theorem |
| getdims-zero-03 | ⊦ getdims(1 ' + ints) = 1 ' + getdims(ints) | A User Theorem |
| getdims-zero-04 | ⊦ 0 ≤ i → getdims(i ') = i ' | A User Theorem |
| getdims-zeroin | ⊦ ints ≠ [] → ¬ 0 ∈ getdims(ints) .butlast | A User Theorem |
| getdims-zeroin-01 | ⊦ 0 < i → ¬ 0 ∈ (i ' + getdims(ints)) .butlast | A User Theorem |
| multg-at-ref | r ≠ r0, ¬ r0 ∈ refs, i→n(countrefs2(ints)) ≤ # refs ⊦ (addarraymultlist(r, ty, st, refs, ints, ints0, i)[r0 -- sk]) = st[r0 -- sk] | A User Theorem |
| multi-at-other | ⊦ ¬ r ∈ refs ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → (addmultiarrays(refs, i, acc, ty, ints, st)[r -- sk]) = st[r -- sk] | A User Theorem |
| multi-field | ⊦ fs ' ≠ _type ∧ fs ' ≠ _length ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → (addmultiarrays(refs, i, acc, ty, ints, st)[r -- fs ']) = st[r -- fs '] | A User Theorem |
| multi-fieldin | ⊦ fs ' ≠ _type ∧ fs ' ≠ _length ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → (r -- fs ' ∈ addmultiarrays(refs, i, acc, ty, ints, st) ↔ r -- fs ' ∈ st) | A User Theorem |
| multi-first-type-in | ⊦ r ∈ refs ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → r -- _type ∈ addmultiarrays(refs, i, acc, ty, ints, st) | A User Theorem |
| multi-in-other | ⊦ ¬ r ∈ refs ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → (r -- sk ∈ addmultiarrays(refs, i, acc, ty, ints, st) ↔ r -- sk ∈ st) | A User Theorem |
| multi-isarrayref | ⊦ r ∈ refs ∧ n→i(# acc) + i = ints .first ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → is_arrayref(r, (addmultiarrays(refs, i, acc, ty, ints, st)[r -- _length]) .intval, addmultiarrays(refs, i, acc, ty, ints, st)) | A User Theorem |
| multi-isarrayref-01 | ⊦ ¬ r ∈ refs ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → (is_arrayref(r, i, addmultiarrays(refs, i, acc, ty, ints, st)) ↔ is_arrayref(r, i, st)) | A User Theorem |
| multi-isarrayref-notin | ⊦ ¬ r ∈ refs ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → (is_arrayref(r, j, addmultiarrays(refs, i, acc, ty, ints, st)) ↔ is_arrayref(r, j, st)) | A User Theorem |
| multi-length-first | ⊦ # refs + 1 = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first ∧ n→i(# acc) + i = ints .first → (addmultiarrays(r ' + refs, i, acc, ty, ints, st)[r -- _length]) = intval(ints .first) | A User Theorem |
| multi-lengthin | ⊦ r ∈ refs ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → r -- _length ∈ addmultiarrays(refs, i, acc, ty, ints, st) ∧ is_integervalue(addmultiarrays(refs, i, acc, ty, ints, st)[r -- _length]) ∧ 0 ≤ (addmultiarrays(refs, i, acc, ty, ints, st)[r -- _length]) .intval | A User Theorem |
| multi-mode | ⊦ (addarraymultlist(r, ty, st, refs, ints, ints0, i)[_mode]) = st[_mode] | A User Theorem |
| multi-mode-01 | ⊦ (addarraymult(r, ty, st, refs, ints, i)[_mode]) = st[_mode] | A User Theorem |
| multi-newref | ⊦ ¬ r ∈ refs ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → (newref(r, addmultiarrays(refs, i, acc, ty, ints, st)) ↔ newref(r, st)) | A User Theorem |
| multi-newrefs | ⊦ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first ∧ list2set(refs) ∩ list2set(refs0) = ∅ → (is_newref_list(refs0, addmultiarrays(refs, i, acc, ty, ints, st)) ↔ is_newref_list(refs0, st)) | A User Theorem |
| multi-refin | ⊦ rk ∈ st ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → rk ∈ addmultiarrays(refs, i, acc, ty, ints, st) | A User Theorem |
| multi-refin-other | ⊦ ¬ r ∈ refs ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → (r ∈ addmultiarrays(refs, i, acc, ty, ints, st) ↔ r ∈ st) | A User Theorem |
| multi-subset | ⊦ is_newref_list(refs, st) ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → st ⊆ addmultiarrays(refs, i, acc, ty, ints, st) | A User Theorem |
| multi-type-first | ⊦ # refs + 1 = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → (addmultiarrays(r ' + refs, i, acc, ty, ints, st)[r -- _type]) = typeval(mktype_from_dims(ty, n→i(# ints))) | A User Theorem |
| multi-typein | ⊦ r ∈ refs ∧ # refs = i→n(countrefs(i ' + ints .rest)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ ¬ 0 ∈ ints .butlast ∧ i ≤ ints .first → r -- _type ∈ addmultiarrays(refs, i, acc, ty, ints, st) ∧ is_typevalue(addmultiarrays(refs, i, acc, ty, ints, st)[r -- _type]) ∧ is_arraytype((addmultiarrays(refs, i, acc, ty, ints, st)[r -- _type]) .type) | A User Theorem |
| nouninit-addarrays | ⊦ newref_list(i→n(countrefs(ints)), st) = r ' + refs ∧ ty1 = mktype_from_dims(ty, i + n→i(n)) ∧ ints ≠ [] ∧ 0 ≤ i ∧ posints(ints) ∧ n = # ints - 1 → (nouninit(claset, addarrays(r ' + refs, ty, ints, i, st)) ↔ nouninit(claset, st)) | A User Theorem |