[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Lemma dependency for Specification okfuns

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
okbytearray-put-bytevalprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05, okbytearray-01, okbar-byteval, okbytearray-put-byteval-equiv, okbar-put, okbytearray-put-byteval-01,
gfts-notprovedall subs proved gfts-not-01,
gftsprovedall subs proved gfts-put,
okbytearray-put-byteval-equivprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05, okbytearray-01, okbytearray-put-byteval-01,
gfts-not-01provedall subs proved gft-not-01, good-rec-01, good-rec, good-base,
gfts-putprovedall subs proved gft-put, good-rec-01, good-rec, good-base,
gengftsprovedall subs proved gengft, good-rec-01, good-rec, good-base,
gftprovedall subs proved good-field-def, gft-put,
gft-mode-01provedall subs proved mode-01, gft-null,
gft-notprovedall subs proved gft-not-01,
gft-out-01provedall subs proved gft-null,
gfts-allprovedall subs proved good-rec-01, good-base, gfts-in,
gfts-nullprovedall subs proved gft-null, good-rec-01, good-rec, good-base,
mode-01provedall subs proved good-field-rew,
gft-not-01provedall subs proved oktype-st, good-field, oktype, good-index, good-field-02,
gft-nullprovedall subs proved good-field-rew, good-field-def,
gft-putprovedall subs proved good-field-rew, good-field-def,
good-rec-01provedall subs proved good-field-rew, good-rec,
okbytearray-put-byteval-01provedall subs proved okbar-put-byte-same, okbar-put,
okarray-putprovedall subs proved okarray-put-08, good-field-rew,
goodfields-putbaprovedall subs proved good-field-rew,
good-field-putprovedall subs proved good-field-rew,
good-field-delprovedall subs proved good-field-rew,
gft-unionprovedall subs proved good-field-rew, good-field-def,
gft-outprovedall subs proved good-field-rew, good-field-def,
okbar-put-byte-sameprovedall subs proved okbar-put-byte-01,
good-field-rewprovedall subs proved good-field-in, good-field-def,
good-field-02provedall subs proved oktype-okval, good-field-def,
exactarray-put-01provedall subs proved exactreftype, exactarray-01, oktype-okval, good-field-def,
is_array-length-04provedall subs proved is_array-length-03,
is_array-length-06provedall subs proved is_array-length-02,
is_array-put-byteprovedall subs proved isarray-put-byte, is-real-array-def-01, is-real-array-def,
isarray-put-samefield-01provedall subs proved okarray-put-samefield-01, okarray-05, is-any-array, isarray-put-samefield,
okarray-int-putprovedall subs proved okarray-07,
okarray-put-04provedall subs proved okarray-07,
okarray-putbar-04provedall subs proved okarray-putbar-02,
okarray-putbar-05provedall subs proved okarray-putbar-same, okarray-05,
okarray-putbar-any-01provedall subs proved okarray-putbar-same-02, okarray-01, okarray-jvmref-01, okarray-refval, okarray-putba,
okbar-putbar-04provedall subs proved okbar-putbar-same, okbar-putbar-02,
okbar-putbar-05provedall subs proved okbar-putbar-same, okbar-putbar-02,
good-field-defprovedall subs proved good-field-in, good-field-in-01, good-field-index, good-field-field,
is_array-length-03provedall subs proved isarray-length-03, is-real-array-def-01,
is_array-length-02provedall subs proved isarray-length-02, is-real-array-def-01,
isarray-put-byteprovedall subs proved okbytearray-type, isarray-put-okval, isarray-put-01,
okarray-put-samefield-01provedall subs proved oktype, okreftype, okarrayNotNull, okarray-05, oktype-okval, okarray-put-samefield,
isarray-put-samefieldprovedall subs proved okarray-put-samefield, okarray-05, is-any-array,
okarray-07provedall subs proved okarray-08, okarray-05,
okarray-putbar-02provedall subs proved okbar-putbar-03, okarray-05,
okarray-putbar-sameprovedall subs proved okarray-put-01, okarray-05,
okarray-putbar-same-02provedall subs proved okarray-okarray-02, okarray-put-01, okarray-okarray-01, okarray-jvmref-01, okarray-01,
okbar-put-byte-01provedall subs proved okarray-put-01, okbytearray-01, okbar-put,
okbar-putbar-sameprovedall subs proved okarray-put-01, okbytearray-01,
okbar-putbar-02provedall subs proved okbar-putbar-01,
okbytearray-put-field-04provedall subs proved okbytearray-put-field,
okbytearray-put-field-03provedall subs proved okbytearray-put-field,
okbytearray-put-field-02provedall subs proved okbytearray-put-field,
okbytearray-put-field-01provedall subs proved okbytearray-put-field,
okarrays-put-03provedall subs proved okarrays-put-02,
okarrays-put-01provedall subs proved okarrays-put-02,
okarrays-modeprovedall subs proved mode-02, okarrays-all,
okarray-update-01provedall subs proved okarray-update, okarray-refval,
okarray-putbar-same-01provedall subs proved okarray-put-01, okarray-okarray, okarray-okarray-01, okarray-jvmref-01, okarray-01,
okarray-put-03provedall subs proved okarray-02,
okarray-int-put-02provedall subs proved okarray-08, okarray-05, intval-01,
okarray-int-put-01provedall subs proved okarray-08, okarray-05,
okarray-getbar-lenprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05, okarray-okarray-01,
okarray-byteputprovedall subs proved okarray-put-02,
isarray-length-06provedall subs proved isarray-length-02,
isarray-length-04provedall subs proved isarray-length-03,
is_array-union-disjointprovedall subs proved isarray-union-disjoint, is-real-array-def-01,
is_array-type-04provedall subs proved is_array-type-01,
is_array-type-03provedall subs proved is_array-type,
is_array-putbar-01provedall subs proved isarray-putbar, is-real-array-def,
is_array-putbarprovedall subs proved isarray-putbar, is-real-array-def-01,
is_array-put-samefield-01provedall subs proved is-real-array-def-01, is_array-put-field,
is_array-put-samefieldprovedall subs proved is_array-put-field, oktype-okval, is-real-array-def-01,
is_array-put-okvalprovedall subs proved isarray-put-okval, is-real-array-def-01,
is_array-put-jvmrefprovedall subs proved isarray-null, isarray-put-jvmref, is-real-array-def-01,
is_array-put-badfieldprovedall subs proved is_array-put-field, is-real-array-def-01,
is_array-okarray-01provedall subs proved isarray-okarray-01, is-real-array-def,
is_array-length-05provedall subs proved isarray-length-05, is-real-array-def-01,
is_array-length-01provedall subs proved isarray-length-01, is-real-array-def-01,
is_array-lenprovedall subs proved isarray-length-01, is-real-array-def-01,
getintarray-subset-01provedall subs proved getintarray-subset, is-real-array-def,
getbytearray-mkjavavaluesprovedall subs proved okbytearray-byteval, okbar-len, okbytearray-length-zero,
getbar-supersetprovedall subs proved getbar-subset,
getarray-superset-01provedall subs proved getarray-subset,
getarray-supersetprovedall subs proved getarray-subset, is-real-array-def,
getarray-subset-01provedall subs proved getarray-subset, is-real-array-def,
okbytearray-put-fieldprovedall subs proved okreftype, oktype-byte, okarrayNotNull, okarray-05, okarray-put-badfield, okarray-put-other, okbytearray-01,
okbar-putbar-01provedall subs proved okbar-putbar, okarray-05, okbytearray-01,
okbar-putprovedall subs proved okarray-put-05, okbytearray-01,
okarrays-put-02provedall subs proved okarray-put-08, okarrays-rec-01, okarrays-base,
mode-02provedall subs proved okarray-jvmref, okarray-put-07,
okarray-updateprovedall subs proved okarray-put-07, update-rec-01, update-empty,
okarray-put-01provedall subs proved okarray-put-06, okarray-put-05, okarray-05,
okbar-putbar-03provedall subs proved okbar-putbar, okarray-05,
okarray-02provedall subs proved okarray-put-07,
okarray-okarray-01provedall subs proved okreftype, okarrayNotNull, oktype-okval, okarray-len, okarray-intval-01, okarrayOfLength, okarray-05, okarray-jvmref-01, okarray-01, okarray-okarray-02, okarray-04, okarray-refval,
okarray-put-02provedall subs proved okreftype, oktype-byte, okarrayOfLength, okarray-primput, okarray-jvmref-01, okarray-01, okarray-put-07,
okarray-08provedall subs proved okreftype, oktype-int, okarray-len, okarrayNotNull, okarray-06, okarray-05,
okarray-put-samefieldprovedall subs proved okarray-put-badfield, oktype-okval,
isarray-union-disjointprovedall subs proved isarray-subset,
is_array-type-01provedall subs proved isarray-type-04, is-real-array-def-01,
is_array-typeprovedall subs proved isarray-type-03, is-real-array-def-01,
isarray-putbarprovedall subs proved isarray-put-01, oktype-byte, okreftype, okarrayNotNull, okarray-05, okbytearray-01, isarray-null, is-any-array,
isarray-put-okvalprovedall subs proved okarray-put-okval, okarray-05, isarray-type, isarray-type-05, isarray-null, is-any-array,
isarray-put-jvmrefprovedall subs proved okarray-05, isarray-put-01, is-any-array,
is_array-put-fieldprovedall subs proved isarray-put-field, is-real-array-def-01,
isarray-okarray-01provedall subs proved okarray-supertype, okarray-05, is-any-array,
isarray-length-05provedall subs proved isarray-len, isarray-null,
isarray-length-03provedall subs proved isarray-len, isarray-null,
isarray-length-02provedall subs proved isarray-len, isarray-null,
isarray-length-01provedall subs proved isarray-len,
good-field-in-01provedall subs proved good-field-index, good-field-field,
good-field-inprovedall subs proved good-field-index, good-field-field,
getintarray-subsetprovedall subs proved okarrayNotNull, okarray-subset-01, okarray-05, subset-okarray, is-any-array, isarray-lenfield,
okbytearray-length-zeroprovedall subs proved okbar-len,
getbar-subsetprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-subset-01, okarray-05, subset-okarray, okbytearray-01, okbar-lenfield, okbar-len,
getarray-subsetprovedall subs proved okreftype, okarrayNotNull, okarray-05, subset-okarray, is-any-array, isarray-lenfield, isarray-len,
gengftprovedall subs proved good-index, good-field-index, good-field-field, good-field-field-03, oktype-okval,
comp-sameprovedall subs proved intval-01, okarray-intval, okarray-05,
getarray-subset-02provedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-subset-01, subset-okarray, okarray-05, is-any-array,
good-field-subsetprovedall subs proved good-field-index, good-field-field,
is_array-lengthprovedall subs proved isarray-length, is-real-array-def-01,
is_array-putprovedall subs proved isarray-put, oktype-okval, is-real-array-def-01,
is_array-put-01provedall subs proved isarray-put-01, is-real-array-def-01,
is_array-subsetprovedall subs proved isarray-type-05, isarray-subset, is-real-array-def-01,
is_array-unionprovedall subs proved isarray-type-05, isarray-union, is-real-array-def-01,
is_array-updateprovedall subs proved is-real-array-def-01, isarray-update, update-at, is-real-array-def,
isarray-put-badfieldprovedall subs proved isarray-put-field,
keys-notinprovedall subs proved keys-notin-01,
nonnullrefs-dups-keyprovedall subs proved nonnullrefs-in-key, keys-notin-02, getkeys-one, getkeys-app, getvals-rec-01, getvals-empty, nonnullrefs-dups,
okarray-copy-01provedall subs proved okarray-put-05, oktype-byte, okreftype, okarrayNotNull, okarray-put-06, okarray-05,
okarray-outprovedall subs proved okarray-jvmref-01, okarray-01, okarray-put-07,
okarray-putbar-anyprovedall subs proved okarray-putbar-same-03, okarray-putbar-other, okarray-05,
okarray-subset-02provedall subs proved okarray-subset-01,
okarray-union-01provedall subs proved okarray-union, okarray-jvmref-01, okarray-01, okarray-union-04,
okarray-union-02provedall subs proved okarray-union, okarray-jvmref-01, okarray-01, okarray-union-04,
okarrays-notprovedall subs proved okarray-put-08, okarrays-rec-01, okarrays-base,
okarrays-putprovedall subs proved good-index, okarray-put-08, okarrays-rec-01, okarrays-base,
okbar-put-01provedall subs proved okbar-byteval, okarray-put-06, okbytearray-01,
okbytearray-getarray-lengthprovedall subs proved okbar-len,
okbytearray-index-in-zeroprovedall subs proved okbar-len, okbytearray-index-in,
okbytearray-isarrayprovedall subs proved okbytearray-02, okbytearray-type-01, okbar, okbytearray-type, is-any-array,
okbytearray-subsetprovedall subs proved okarray-subset-01, okbytearray-01,
subset-lenprovedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-subset-01, subset-okarray, okarray-05,
update-ex-nodupsprovedall subs proved update-putfis-sw, dups-fis-keys, update-rec-01, getkeys-empty, update-empty,
okarray-intvalprovedall subs proved intval-01, okarray-05,
okbytearray-bytevalprovedall subs proved okbar-byteval,
good-field-fieldprovedall subs proved good-field-field-03,
isarray-lengthprovedall subs proved isarray-length-07,
isarray-putprovedall subs proved okreftype, oktype-01, okarray-len, okarrayNotNull, okarray-put-other, okarray-05, is-any-array, oktype-okval,
isarray-type-03provedall subs proved isarray-type-02,
isarray-type-04provedall subs proved isarray-type-01,
isarray-unionprovedall subs proved union-okarray, okarray-05, is-any-array,
isarray-updateprovedall subs proved oktype-okval, okreftype, okarrayNotNull, update-at, update-in, is-any-array,
isarray-lenprovedall subs proved okarray-len, is-any-array,
okarray-supertypeprovedall subs proved okreftype, oktype-okval, okarray-len, okarrayNotNull, okarray-05,
isarray-put-fieldprovedall subs proved oktype-okval, oktype, okreftype, okarrayNotNull, is-any-array,
okarray-put-okvalprovedall subs proved okreftype, oktype-okval, oktype-put-other, okarray-len, okarrayNotNull, okarray-05,
isarray-put-01provedall subs proved okarray-put-other, is-any-array,
isarray-subsetprovedall subs proved okarray-05, subset-okarray, is-any-array,
keys-notin-01provedall subs proved keys-in-01,
nonnullrefs-in-keyprovedall subs proved keys-notin-02, getkeys-one, getkeys-app, getvals-rec-01, getvals-empty, nonnullrefs-in,
okarray-06provedall subs proved okarray-put-other,
okarray-primputprovedall subs proved oktype-st, okprim-oktype, oktype-put-other, okreftype, okarray-type, okarrayOfLength, okarray-01, okarray-jvmref-01,
okarray-putbar-same-03provedall subs proved okreftype, oktype-byte, okarray-len, okarrayNotNull, okarray-05,
okarray-okarray-02provedall subs proved okarray-05, okarray-okarray, okarray-jvmref-01, okarray-01,
okarray-union-04provedall subs proved okarray-subset,
okarray-put-07provedall subs proved okarray-jvmref-01, okarray-01, okarray-type, okarray-type-02, okarray-null, okarray-refval, oktype-okval, oktype-put-other, okreftype, okarrayOfLength,
okarray-put-08provedall subs proved oktype-okval, oktype, okreftype, okarrayOfLength,
okarray-put-05provedall subs proved okarray-put-other,
okarray-put-06provedall subs proved okreftype, oktype-byte, okarray-len, okarrayNotNull, okarray-05,
okbar-putbarprovedall subs proved okreftype, oktype-byte, okarray-len, okarrayNotNull, okarray-05,
okbarprovedall subs proved okarray-04, okbytearray-01,
okbar-lenprovedall subs proved okarray-len, okbytearray-01,
okarray-put-badfieldprovedall subs proved oktype, oktype-okval, okreftype, okarrayNotNull, okarray-05,
okarray-subset-01provedall subs proved okarray-05, subset-okarray,
dups-fis-keysprovedall subs proved keys-in-01, getkeys-one, getkeys-app, keys-put-in,
validFields-putfisprovedall subs proved keys-in, keys-put, hasKeys-all, validFields,
short-lengthprovedall subs proved okarray-len, okarray-05,
onlymod-is-updateprovedall subs proved update-rec-01, update-atin, update-at, update-keyin, update-in, update-at-notin, update-keyin-01, keys-in, hasKeys-all, validFields, validFields-del, validFields-rec, update-rec, validFields-empty, update-empty,
okbytearray-is-byteprovedall subs proved okbar-byteval,
okbytearray-bad-typeprovedall subs proved okbytearray-type,
okbar-bytes2int-sameprovedall subs proved okarray-len, okarray-05,
okbar-01provedall subs proved okarray-length-02, okbytearray-01,
okarray-union-03provedall subs proved oktype-st, subset-oktype, okarray-type, okreftype, okarray-jvmref-01, okarray-01, okarray-null, okarrayOfLength,
okarray-substoreprovedall subs proved oktype-st, subset-oktype, okreftype, okarrayOfLength,
okarray-putbar-03provedall subs proved okarray-putbar-01,
okarray-lengthprovedall subs proved okarray-len, okarray-length-02,
isarray-bytearrayprovedall subs proved okarray-type-03, okarray-05, is-any-array, okbytearray-01,
isarray-arrayrefvalprovedall subs proved isarray-okval,
is_array-typeleprovedall subs proved isarray-type, isarray-type-01, is-real-array-def-01,
is_array-reftypeprovedall subs proved isarray-reftype, is-real-array-def-01,
is_array-okbytearrayprovedall subs proved isarray-okarray, okbytearray-01, okbytearray-type, is-real-array-def-01,
is_array-okarrayprovedall subs proved isarray-okarray, okarray-type-03, is-real-array-def-01,
is_array-notin-01provedall subs proved isarray-notin-01, is-real-array-def,
is_array-notinprovedall subs proved isarray-notin, is-real-array-def-01,
is_array-length-07provedall subs proved isarray-length-07, is-real-array-def-01,
is_array-lenfieldprovedall subs proved isarray-lenfield, is-real-array-def-01,
is_array-keyinprovedall subs proved isarray-keyin, is-real-array-def-01,
is_array-isarrayrefprovedall subs proved isarray-isarrayref, is-real-array-def,
is_array-delprovedall subs proved isarray-del, is-real-array-def-01,
is_array-byte-noref-01provedall subs proved is_array-byte-noref, is-real-array-def-01,
is_array-badlengthprovedall subs proved isarray-length-07, is-real-array-def,
is_array-arrayreftypeprovedall subs proved isarray-arrayreftype, is-real-array-def,
good-field-field-02provedall subs proved good-field-field-03,
copy-sameprovedall subs proved copy-same-01,
bytevalues-eqprovedall subs proved okbytearray, okarray-05,
byteval-02provedall subs proved okbar-byteval,
byteval-01provedall subs proved byteval, okarray-05,
keys-putprovedall subs proved keys-in,
validFields-delprovedall subs proved validFields-rec, validFields-empty,
okbytearray-type-01provedall subs proved okreftype, okarrayNotNull, okarray-05, okbytearray-01,
okbytearray-index-inprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05, okbytearray-01,
okarray-subsetprovedall subs proved okreftype, okarray-jvmref-01, okarray-01, okarray-null, oktype-okval, okarrayOfLength,
okarray-unionprovedall subs proved oktype-st, okreftype, okarrayOfLength,
subset-oktypeprovedall subs proved oktype-st,
okarray-putbar-01provedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05,
okarray-type-02provedall subs proved okreftype, okarrayOfLength, okarray-jvmref-01, okarray-01,
okarray-typeprovedall subs proved okreftype, okarrayOfLength, okarray-jvmref-01, okarray-01,
okarray-okarrayprovedall subs proved okreftype, okarrayOfLength, oktype-okval, okarrayNotNull, okarray-jvmref-01, okarray-01, okarray-refval,
okarray-04provedall subs proved okarray-05,
okarray-intval-01provedall subs proved okarrayNotNull, okarray-05,
okarray-length-02provedall subs proved okarrayNotNull, okarray-05,
keys-notin-02provedall subs proved keys-in,
okarray-jvmrefprovedall subs proved okarray-jvmref-01, okarray-01,
update-inprovedall subs proved update-keyin-01,
union-okarrayprovedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05,
isarray-type-02provedall subs proved okarray-05, is-any-array,
okarray-put-otherprovedall subs proved oktype-okval, oktype-put-other, okreftype, okarrayNotNull,
oktype-01provedall subs proved oktype-okval, oktype-put-other,
okarray-lenprovedall subs proved okreftype, okarrayNotNull, okarray-05,
isarray-okvalprovedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05, is-any-array,
isarray-type-01provedall subs proved okarray-05, is-any-array,
isarray-reftypeprovedall subs proved okarray-05, is-any-array,
okbytearray-typeprovedall subs proved okreftype, okarrayNotNull, okarray-05, okbytearray-01,
okarray-type-03provedall subs proved okreftype, okarrayNotNull, okarray-05,
isarray-okarrayprovedall subs proved oktype-okval, okreftype, okarrayNotNull, is-any-array, okarray-05,
isarray-notin-01provedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05, is-any-array,
isarray-notinprovedall subs proved okarray-05, is-any-array,
isarray-keyinprovedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05, is-any-array, isarray-null,
isarray-isarrayrefprovedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05, is-any-array,
isarray-delprovedall subs proved okarray-del, is-any-array,
is_array-byte-norefprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05, is-any-array,
isarray-length-07provedall subs proved okarrayNotNull, okarray-05, is-any-array,
isarray-arrayreftypeprovedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05, is-any-array,
oktypeprovedall subs proved oktype-okval, oktype-put-other,
okbar-lenfieldprovedall subs proved okarrayNotNull, okarray-05, okbytearray-01,
isarray-lenfieldprovedall subs proved okarrayNotNull, okarray-05, is-any-array,
subset-okarrayprovedall subs proved okreftype, oktype-okval, okarrayNotNull, okarray-05,
good-field-field-03provedall subs proved good-field-field-01,
keys-in-01provedall subs proved keys-in,
copy-same-01provedall subs proved okarray-05,
intval-01provedall subs proved oktype-int, okreftype, okarrayNotNull, okarray-05,
okbytearrayprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05,
okbar-bytevalprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05, okbytearray-01,
bytevalprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05,
copy-compprovedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05,
exactarray-byteputprovedall subs proved exactarray-put-02,
exactarray-length-02provedall subs proved exactarray-length-01, exactarray-01-01, exactarray-jvmref-01,
exactarray-put-04provedall subs proved exactarray-07,
exactarray-type-02provedall subs proved exactarray-type-01, exactarray-01-01, exactarray-jvmref-01,
good-field-01provedall subs proved good-field-field-01,
instore-afterputsprovedall subs proved inst-in, instore-null, inst-single, instore-rec-03, instore-empty, instore-rec-02,
is_array-abstractprovedall subs proved okarray-05, is-any-array, is-real-array-def-01,
is_array-noreftypeprovedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05, is-any-array, is-real-array-def,
is_array-norefvalprovedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05, is-any-array, is-real-array-def,
is_array-nottypeexprovedall subs proved okarray-05, is-any-array, is-real-array-def,
is_array-primtype-01provedall subs proved oktype-okval, okreftype, okarrayNotNull, okarray-05, is-any-array,
isarray-abstractprovedall subs proved oktype-abstract, okreftype, okarrayNotNull, okarray-05, is-any-array,
isarray-okreftypeprovedall subs proved okarray-05, is-any-array, okreftype,
isarray-put-array-badindexprovedall subs proved oktype-okval, oktype-put-other, okreftype, okarrayNotNull, is-any-array,
okarray-byteprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05,
okarray-byte-01provedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05,
okarray-copyprovedall subs proved oktype-okval, oktype-04, okreftype, okarrayNotNull,
okarray-length-01provedall subs proved oktype-okval, okreftype, okarrayOfLength, okarray-jvmref-01, okarray-01,
okarray-newprovedall subs proved oktype-put-other, okreftype, okarrayOfLength, okarray-01,
okarray-new-01provedall subs proved okreftype, okarrayOfLength, okarray-jvmref-01, okarray-01,
okarray-onlymodprovedall subs proved okreftype, oktype-okval, okarrayOfLength, okarray-jvmref-01, okarray-01,
okarray-put-okval-01provedall subs proved oktype-put-other, oktype-okval, okreftype, okarrayOfLength,
okarray-type-01provedall subs proved oktype-okval, okreftype, okarrayOfLength, okarray-jvmref-01, okarray-01,
okbar-newprovedall subs proved okarray-05, okbytearray-01,
okbar-norefvalprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05, okbytearray-01,
okbytearray-isarrayrefprovedall subs proved okarrayNotNull, okarray-05, okbytearray-01,
okbytearray-notprovedall subs proved oktype-byte, okreftype, okarrayNotNull, okarray-05, okbytearray-01,
oktype-02provedall subs proved oktype-okval, oktype-put-other,
oktype-newprovedall subs proved oktype-okval, oktype-put-other,
update-in-01provedall subs proved update-in-02, update-in-03,
update-lengthprovedall subs proved validFields-rec, update-rec-01, update-empty,
update-type-01provedall subs proved validFields-type, update-keyin-01,
validFields-put-01provedall subs proved keys-in, hasKeys-put-02, validFields,
vals-at-in-01provedall subs proved vals-at-in,
keys-put-inprovedall subs proved getkeys-app, getkeys-empty, getkeys-one,
exactarray-put-02provedall subs proved exactreftype, exactarray-01-01, exactarray-jvmref-01, exactarray-null, exactarray-01,
exactarray-length-01provedall subs proved exactreftype, exactarray-01, exactarray-01-01, exactarray-jvmref-01,
exactarray-07provedall subs proved exactarray-08, exactarray-05,
exactarray-type-01provedall subs proved exactreftype, exactarray-01, exactarray-01-01, exactarray-jvmref-01,
good-field-field-01provedall subs proved oktype-okval, good-field,
inst-inprovedall subs proved instore-rec-03, instore-empty, instore-null,
inst-singleprovedall subs proved instore-empty, instore-null, instore-rec-02,
okarray-delprovedall subs proved oktype-okval, oktype-del, okreftype, okarrayNotNull,
nonnullrefs-dupsprovedall subs proved nonnullrefs-in, getvals-rec-01,
oktype-04provedall subs proved oktype-okval,
okarray-putbar-otherprovedall subs proved oktype-okval, okreftype, okarrayNotNull,
okarray-putbaprovedall subs proved oktype-okval, okreftype, okarrayOfLength, okarray-refval,
okarray-01provedall subs proved oktype-okval, okreftype, okarrayOfLength, okarray-jvmref-01,
oktype-put-otherprovedall subs proved oktype-okval,
oktype-stprovedall subs proved oktype-okval,
okarray-05provedall subs proved oktype-okval, okreftype, okarrayNotNull,
update-in-02provedall subs proved update-in-03,
update-keyin-01provedall subs proved update-keyin, update-rec-01, update-empty,
validFields-recprovedall subs proved hasKeys-one, hasKeys-app, getkeys-one, getkeys-app, validFields,
keys-inprovedall subs proved getkeys-one, getkeys-app, getkeys-empty,
vals-at-inprovedall subs proved vals-in,
validFields-putprovedall subs proved hasKeys-put-01, validFields,
validFields-fisprovedall subs proved hasKeys-one, hasKeys-app, getkeys-one, getkeys-app, validFields,
validFields-empty-01provedall subs proved hasKeys-one, hasKeys-app, getkeys-one, getkeys-app, validFields, validFields-empty,
update-typeprovedall subs proved validFields-type, update-at-notin,
update-put-sameprovedall subs proved update-put-rew, update-rec-01, update-empty,
update-put-notinprovedall subs proved update-rec-01, update-empty, update-put,
subset-len-01provedall subs proved exactreftype, exactref-in, exactarray-02, subset-exactarray, exactarray-05,
short-length-01provedall subs proved exactarray-len, exactarray-05,
oktype-reftypeprovedall subs proved oktype-okval,
okstore-modeprovedall subs proved is_javastore, okstore-11, okstore, okstore-08,
okstore-jvmrefprovedall subs proved okstore-10, okstore-09, is_javastore, okstore-11, okstore, okstore-08,
okstore-07provedall subs proved okstore-11,
okstore-05provedall subs proved okstore-11,
okreftype-unionprovedall subs proved okreftype-null, okreftype, okreftype-subset,
mode-03provedall subs proved oktype-okval,
keys-put-notinprovedall subs proved getkeys-one, getkeys-app,
keys-lengthprovedall subs proved getkeys-one, getkeys-app, getkeys-empty,
keys-emptyprovedall subs proved getkeys-one, getkeys-app, getkeys-empty,
keys-atprovedall subs proved getkeys-one, getkeys-app,
infis-notinprovedall subs proved infis-notin-01,
exactarray-type-03provedall subs proved exactreftype, exactarray-01, exactarray-01-01, exactarray-jvmref-01,
exactarray-typeprovedall subs proved exactreftype, exactarray-01, exactarray-01-01, exactarray-jvmref-01,
exactarray-putinprovedall subs proved exactreftype, exactarray-01, exactarray-01-01, exactarray-jvmref-01,
exactarray-put-06provedall subs proved exactreftype, exactarray-len, exactarray-02, exactarray-05,
exactarray-putprovedall subs proved exactreftype, exactarray-len, exactarray-02, exactarray-05,
exactarray-primputprovedall subs proved exactreftype, exactarray-01, exactarray-01-01, exactarray-jvmref-01,
exactarray-new-01provedall subs proved exactreftype, exactarray-01, exactarray-01-01, exactarray-jvmref-01,
exactarray-jvmrefprovedall subs proved exactarray-jvmref-01, exactarray-01-01,
exactarray-inprovedall subs proved exactreftype, exactarray-01, exactarray-jvmref-01, exactarray-01-01,
exactarray-copy-01provedall subs proved exactreftype, exactarray-len, exactarray-02, exactarray-05,
copy-same-02provedall subs proved copy-same-01-01,
vals-inprovedall subs proved getvals-rec-01, getvals-empty,
hasKeys-put-02provedall subs proved hasKeys-rec, hasKeys-one, hasKeys-app, hasKeys-empty,
hasKeys-put-01provedall subs proved hasKeys-rec, hasKeys-one, hasKeys-app, hasKeys-empty,
update-put-rewprovedall subs proved update-rec-01, update-empty,
update-putprovedall subs proved update-rec-01, update-empty,
update-in-03provedall subs proved update-rec-01, update-empty,
update-putfis-swprovedall subs proved update-rec, update-rec-01, update-empty, update-one,
subset-exactarrayprovedall subs proved exactreftype, exactarray-02, exactarray-05,
update-at-notinprovedall subs proved update-rec-01, update-empty,
update-keyinprovedall subs proved update-rec-01, update-empty,
okstore-09provedall subs proved is_javastore, okstore, okstore-08,
okstore-10provedall subs proved is_javastore, okstore, okstore-08,
okstore-11provedall subs proved okstore, okstore-08,
okreftype-subsetprovedall subs proved okreftype-null, okreftype,
nonnullrefs-inprovedall subs proved getvals-rec-01,
instore-nullprovedall subs proved instore-rec-03, instore-empty,
infis-notin-01provedall subs proved instore-rec-01, instore-base,
exactarray-jvmref-01provedall subs proved exactarray-01, exactarray-01-01,
exactarray-lenprovedall subs proved exactreftype, exactarray-02, exactarray-05,
exactarray-08provedall subs proved exactreftype, exactarray-02, exactarray-05,
getkeys-oneprovedall subs proved getkeys-app, getkeys-rec,
copy-same-01-01provedall subs proved exactarray-05,
oktype-okvalprovedall subs proved oktype-array, oktype-class, oktype-abstract, oktype-void, oktype-char, oktype-double, oktype-float, oktype-long, oktype-byte, oktype-short, oktype-int, oktype-bool, okval-oktype,
exactarray-04provedall subs proved exactarray-05,
exactarray-intval-01provedall subs proved exactarray-02, exactarray-05,
exactarray-lengthprovedall subs proved exactreftype, exactarray-02, exactarray-05,
exactarray-leninprovedall subs proved exactreftype, exactarray-02, exactarray-05,
exactarray-newprovedall subs proved exactreftype, exactarray-01, exactarray-01-01,
exactarray-outprovedall subs proved exactarray-null, exactarray-put-07,
exactref-putprovedall subs proved exactref-put-01,
getbar-updateprovedall subs proved update-rec-01, update-empty,
hasKeys-putprovedall subs proved hasKeys-rec, hasKeys-one, hasKeys-app, hasKeys-empty,
infis-jvmrefprovedall subs proved instore-rec-01, instore-rec, instore-base,
is_array-arraytypeprovedall subs proved isarray-type, is-real-array-def-01,
is_array-bytearrayprovedall subs proved is-real-array-def-01, is-real-array-def,
is_array-bytearray-01provedall subs proved is-real-array-def-01, is-real-array-def,
is_array-classtypeprovedall subs proved isarray-type, is-real-array-def,
is_array-del-01provedall subs proved isarray-del-01, is-real-array-def-01,
is_array-is-arrayprovedall subs proved is-real-array-def-01,
is_array-newrefprovedall subs proved isarray-newref, is-real-array-def-01,
is_array-nullprovedall subs proved isarray-null, is-real-array-def-01,
is_array-primtypeprovedall subs proved is-real-array-def-01,
is_array-type-02provedall subs proved isarray-type-05, is-real-array-def,
okarray-putbarprovedall subs proved okarray-putar,
okarrays-oneprovedall subs proved okarrays-one-01,
okclass-intprovedall subs proved okclass-01, okclass,
okreftype-notinprovedall subs proved okreftype-null, okreftype,
okreftype-putprovedall subs proved okreftype-null, okreftype,
okstore-01provedall subs proved is_javastore, okstore, okstore-08,
okstore-02provedall subs proved is_javastore, okstore, okstore-08,
okstore-04provedall subs proved okstore, okstore-08,
okstore-06provedall subs proved okstore, okstore-08,
okstore-outprovedall subs proved is_javastore, okstore, okstore-08,
update-at-01provedall subs proved update-at,
update-initprovedall subs proved update-rec-01, update-empty,
update-init-01provedall subs proved update-rec-01, update-empty,
update-newrefprovedall subs proved update-rec-01, update-empty,
update-rec-02provedall subs proved update-rec-01,
update-refsprovedall subs proved update-rec-01, update-empty,
update-union-switchprovedall subs proved update-rec-01, update-empty,
vals-atprovedall subs proved getvals-rec-01,
vals-lengthprovedall subs proved getvals-rec-01, getvals-empty,
exactarray-put-07provedall subs proved exactreftype, exactarray-01,
exactarray-nullprovedall subs proved exactarray-01,
exactarray-01-01provedall subs proved exactreftype, exactarray-01,
exactref-put-01provedall subs proved exactreftype,
gfts-inprovedall subs proved good-rec,
good-field-indexprovedall subs proved good-index,
instore-rec-01provedall subs proved instore-rec,
instore-rec-03provedall subs proved instore-rec-02,
isarray-del-01provedall subs proved is-any-array,
isarray-newrefprovedall subs proved is-any-array,
is-real-array-def-01provedall subs proved is-real-array-def,
isarray-typeprovedall subs proved is-any-array,
isarray-type-05provedall subs proved is-any-array,
isarray-nullprovedall subs proved is-any-array,
oktype-delprovedall subs proved oktype-array, oktype-class, oktype-abstract, oktype-void, oktype-char, oktype-double, oktype-float, oktype-long, oktype-byte, oktype-short, oktype-int, oktype-bool,
okprim-oktypeprovedall subs proved oktype-char, oktype-double, oktype-float, oktype-long, oktype-byte, oktype-short, oktype-int, oktype-bool,
okarray-putarprovedall subs proved oktype-byte, okreftype, okarrayOfLength,
okarray-jvmref-01provedall subs proved okarrayOfLength,
okarray-nullprovedall subs proved okarrayOfLength,
okarray-refvalprovedall subs proved okarrayOfLength,
okarrays-allprovedall subs proved okarrays-rec, okarrays-base,
okarrays-one-01provedall subs proved okarrays-base, okarrays-rec,
okarrays-rec-01provedall subs proved okarrays-rec,
okbytearray-02provedall subs proved okbytearray-01,
okclass-01provedall subs proved okclass,
okreftype-nullprovedall subs proved okreftype,
okstore-08provedall subs proved is_javastore, okstore,
okval-oktypeprovedall subs proved oktype-array, oktype-class, oktype-void, oktype-char, oktype-double, oktype-float, oktype-long, oktype-byte, oktype-short, oktype-int, oktype-bool,
update-atinprovedall subs proved update-rec, update-empty,
exactref-inprovedall subs proved exactreftype,
exactarray-05provedall subs proved exactreftype, exactarray-02,
update-atprovedall subs proved update-rec, update-empty,
update-oneprovedall subs proved update-empty, update-rec,
validFields-typeprovedall subs proved validFields,
update-rec-01provedall subs proved update-rec,
validFields-emptyprovedall subs proved hasKeys-empty, getkeys-empty, validFields,
hasKeys-allprovedall subs proved hasKeys-rec, hasKeys-empty,
hasKeys-oneprovedall subs proved hasKeys-empty, hasKeys-rec,
hasKeys-appprovedall subs proved hasKeys-rec, hasKeys-empty,
getkeys-appprovedall subs proved getkeys-rec, getkeys-empty,
getvals-rec-01provedall subs proved getvals-rec,
vals-oneprovedall subs proved getvals-empty, getvals-rec,
update-modeprovedall subs proved update-rec, update-empty,
oktype-rewprovedall subs proved oktype-array, oktype-class, oktype-abstract, oktype-void, oktype-char, oktype-double, oktype-float, oktype-long, oktype-byte, oktype-short, oktype-int, oktype-bool,
oktype-refvalprovedall subs proved oktype-array, oktype-class, oktype-abstract, oktype-void, oktype-char, oktype-double, oktype-float, oktype-long, oktype-byte, oktype-short, oktype-int, oktype-bool,
oktype-outprovedall subs proved oktype-array, oktype-class, oktype-abstract, oktype-void, oktype-char, oktype-double, oktype-float, oktype-long, oktype-byte, oktype-short, oktype-int, oktype-bool,
oktype-03provedall subs proved oktype-array, oktype-class, oktype-abstract, oktype-void, oktype-char, oktype-double, oktype-float, oktype-long, oktype-byte, oktype-short, oktype-int, oktype-bool,
okstore-otherprovedall subs proved is_javastore, okstore,
okstore-03provedall subs proved is_javastore, okstore,
okreftype-subset-01provedall subs proved okreftype,
okreftype-istypevalprovedall subs proved okreftype,
okreftype-02provedall subs proved okreftype,
okclass-outprovedall subs proved okclass,
okclass-copyprovedall subs proved okclass,
okclass-03provedall subs proved okclass,
okclass-02provedall subs proved okclass,
okarraytype-01provedall subs proved okarraytype,
okarray-novalprovedall subs proved okreftype, okarrayOfLength,
mode-02-01provedall subs proved exactreftype, exactarray-01,
modeprovedall subs proved okclass,
is_array-typeex-01provedall subs proved is-real-array-def,
is_array-typeexprovedall subs proved is-real-array-def,
is_array-notypevalprovedall subs proved is-real-array-def,
is_array-hasnoclasstype-01provedall subs proved is-real-array-def,
is_array-hasnoclasstypeprovedall subs proved is-real-array-def,
instore-oneprovedall subs proved instore-base, instore-rec,
good-oneprovedall subs proved good-base, good-rec,
getbar-update-01provedall subs proved update-rec, update-empty,
exactarray-putbarprovedall subs proved exactreftype, exactarray-01,
exactarray-putarprovedall subs proved exactreftype, exactarray-01,
exactarray-put-05provedall subs proved exactreftype, exactarray-02,
exactarray-put-03provedall subs proved exactreftype, exactarray-01,
exactarray-copyprovedall subs proved exactreftype, exactarray-02,
exactarray-06provedall subs proved exactreftype, exactarray-02,
exactarray-02-01provedall subs proved exactreftype, exactarray-01,
validFieldsaxiom
oktype-voidaxiom
oktype-classaxiom
oktype-arrayaxiom
okstoreaxiom
is_javastoreaxiom
oktype-boolaxiom
oktype-shortaxiom
oktype-longaxiom
oktype-floataxiom
oktype-doubleaxiom
oktype-charaxiom
okarraytypeaxiom
okarrays-baseaxiom
okarrays-recaxiom
okarrayOfLengthaxiom
getvals-emptyaxiom
okclassaxiom
oktype-abstractaxiom
oktype-intaxiom
instore-rec-02axiom
instore-emptyaxiom
instore-baseaxiom
instore-recaxiom
hasKeys-emptyaxiom
hasKeys-recaxiom
good-fieldaxiom
getvals-recaxiom
getkeys-emptyaxiom
getkeys-recaxiom
update-recaxiom
update-emptyaxiom
okbytearray-01axiom
is-real-array-defaxiom
is-any-arrayaxiom
good-baseaxiom
good-recaxiom
good-indexaxiom
exactarray-02axiom
exactarray-01axiom
exactreftypeaxiom
okarrayNotNullaxiom
okreftypeaxiom
oktype-byteaxiom