[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 addarray

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:
validref-addarrayprovedall subs proved isarray-addarray-01, isobj-addarray,
is_obj-addarrayprovedall subs proved isobj-addarray, lookup-1init,
is_array-other-addarrayprovedall subs proved isarray-addarray-01, lookup-1init,
is_array-addarrayprovedall subs proved addarray-negative, isarray-add, type-1dim,
isobj-addarrayprovedall subs proved add-gft, in-init, lookup-1init, in-init-01, isobj-addarray-other,
isarray-addarray-01provedall subs proved is_array-init, okreftype-init, in-1init, lookup-1init, in-init-01, isarray-addarray-other,
isarray-addprovedall subs proved okarray, type-1dim, type-in,
addarray-addarayprovedall subs proved in-init-01, in-1dim-01, add-at-01, add-in-other, in-1init-02, in-init-09, in-1dim-other, add-in-fskey, in-1dim-fskey, add-at-other, add-at-ok, at-1dim, in-add, in-1dim-16, length-1init-01, length-1dim, length-init, addarray-length-in, length-1dim-02, type-1init, type-1dim, add-in, type-in, at-1dim-other, add-at-02,
addarray-put-01provedall subs proved add-at-04, at-1dim, at-1dim-other-index, add-at-other-index, length-1init-01, length-1dim, type-1init, type-1dim, at-field-1dim, lookup-1init, lookup-1dim, in-1dim-14, in-1dim-16, in-1init-02, in-1dim-other, add-in-other, in-1dim-05, in-1dim-fskey, add-in, type-in, length-init, length-1dim-02, add-in-fskey, in-init-01, in-1dim-01, add-at-ok, zero-1init-05, in-add,
is_array-addarray-byteprovedall subs proved is_array-addarray-prim,
okbytearray-thisprovedall subs proved okarray,
putarray-add-sameprovedall subs proved at-field-1dim, at-1dim, at-1dim-other, lookup-1dim, add-at-ok, type-1init, type-1dim, length-1init-01, length-1dim, add-at-other, add-in-fskey, add-in-other, in-init-01, in-add, add-in, type-in, length-init, length-1dim-02, in-1dim-other,
putarray-addarray-01provedall subs proved add-at-neg, in-1dim-other-index, in-1dim-05, in-1dim-14, in-1init-02, add-in-other, add-at-01, lookup-1init, lookup-1dim, add-at-04, at-field-1dim, in-1dim-fskey, type-1init, type-1dim, add-in, type-in, at-1dim-other-index, num-at-1dim, at-1dim, add-at-other-index, add-at-ok, in-1dim-16, in-1dim-other, in-1dim-01, in-add, add-in-fskey, in-init-01, length-1dim, length-1dim-02,
addarray-negativeprovedall subs proved length-1dim, length-1dim-02, okreftype-1dim-02, in-1dim-05, type-1dim, type-in,
is_array-addarray-primprovedall subs proved isarray-addarray, type-1init,
isarray-addarray-otherprovedall subs proved okarray-addarray-other, lookup-1init, in-init-01,
isobj-addarray-otherprovedall subs proved isobj-addarray-other-01, lookup-1init, in-init-01,
okarrayprovedall subs proved at-1dim, isarray-1dim, length-1dim, length-1dim-02, okreftype-1dim-02,
in-1dim-otherprovedall subs proved in-1dim-16, in-1dim-other-index, in-1dim-fskey, in-1dim-05, in-1dim-01, in-1dim-14,
union-addarray-rewprovedall subs proved in-init-01, addarray-at-newref, add-in-other-index, in-1init-02, in-init-09, lookup-init, in-init-06, add-in-other, add-at-ok, in-add, length-1init-01, length-init, type-1init, add-in, add-at-other, lookup-1init,
stsubset-02provedall subs proved stsubset-03,
stsubset-01provedall subs proved stsubset-03,
stsubsetprovedall subs proved stsubset-03,
putarray-addarray-overrideprovedall subs proved lookup-1init, lookup-init, type-1init, length-1init-01, add-at-other, add-at-gr, add-at-ok-01, add-at-other-index, add-at-ok, length-init, in-1init-02, in-init-09, add-in, add-in-other, in-init-06, in-add, in-init-01,
putarray-addarray-oneprovedall subs proved in-1dim-fskey, in-1dim-14, in-1dim-16, in-1dim-other-index, add-in-fskey, lookup-1init, lookup-1dim, in-init-01, in-1dim-01, add-at-04, length-1init-01, length-1dim, length-init, length-1dim-02, type-1init, type-1dim, add-in, type-in, at-field-1dim, add-at-ok, at-1dim-other-index, at-1dim, in-1dim-05, in-1init-02, zero-1init-05, add-at-other-index, in-add,
okbytearray-addarray-02provedall subs proved okbytearray-addarray-01,
okbytearray-addarrayprovedall subs proved okarray-05,
okbar-addarrayprovedall subs proved okarray-05,
okarray-init-03provedall subs proved add-okarray,
okarray-init-02provedall subs proved add-okarray,
okarray-init-01provedall subs proved add-okarray,
okarray-initprovedall subs proved add-okarray,
okarray-abstractprovedall subs proved isarray-1dim, length-1dim, length-1dim-02, okreftype-1dim-02,
okarray-1dim-basicprovedall subs proved okarray-1dim-basic-01, addarray-def,
okarray-1dim-04provedall subs proved at-1dim, isarray-1dim, length-1dim, length-1dim-02, okreftype-1dim-02,
isarray-addarray-02provedall subs proved okarray-05, type-1init, add-in,
is_obj-addarray-01provedall subs proved isobj-addarray-01, type-1dim,
is_array-addarray-anyprovedall subs proved isarray-addarray, type-1init,
getbar-addbar-01provedall subs proved get-add, addbytearray-ints,
addbar-okarray-02provedall subs proved add-okarray, addbytearray-ints,
addbar-okarrayprovedall subs proved add-okarray, addbytearray-ints,
addarray-mklistprovedall subs proved addarrayinit-base, addarray-mklist-01,
addarray-init-02provedall subs proved init-1dim,
addarray-identityprovedall subs proved in-init-01, add-in-other, in-1init-02, add-at-ok, in-add, length-1init-01, addarray-length-in, type-1init, add-in, add-at-other, add-at-01, in-init-09,
stsubset-03provedall subs proved in-1dim-14, in-1dim-01, in-1dim-05, add-at-02,
okbytearray-addarray-01provedall subs proved okarray-addarray,
okarray-1dim-basic-01provedall subs proved oktype-1dim-basic-01, is_array-1dim-01, lookup-1dim-01, in-1dim-02, okreftype-1dim-01,
isobj-addarray-other-01provedall subs proved add-gft, in-init,
okarray-addarray-otherprovedall subs proved oktype-addarray, is_array-init, lookup-1init, in-init-01, okreftype-init,
okarray-05provedall subs proved add-at-ok, isarray-init-02, length-1init-01, length-init, okreftype-init-02,
isobj-addarray-01provedall subs proved type-1dim, type-in,
isarray-addarrayprovedall subs proved oktype-addarray, isarray-init-02, isarray-init-01, add-at-ok, length-1init-01, length-init, okreftype-init-02, type-1init, add-in,
in-1dim-other-indexprovedall subs proved in-1dim-15, in-1dim-other-index-01, addarray-def, in-1dim-05, in-1dim-14,
get-addprovedall subs proved get-add-01, length-1init-01,
add-okarrayprovedall subs proved okreftype-init, lookup-1init, is_array-init, in-init,
okreftype-1dim-02provedall subs proved type-1dim, type-in,
addarray-mklist-01provedall subs proved addarray-mklist-04,
init-1dimprovedall subs proved init-1dim-03, addarray-def,
add-at-otherprovedall subs proved add-at-ok, add-at-other-index, add-at-04, lookup-1init,
in-1dim-fskeyprovedall subs proved in-1dim-17, addarray-def, in-1dim-05, in-1dim-14,
addarray-init-01provedall subs proved init-1dim-03, addarray-def,
addarray-nouninitprovedall subs proved init-1dim-01,
addbar-okarray-03provedall subs proved length-1init-01, addbytearray-ints, addbar-okarray-01,
getarray-addarrayprovedall subs proved get-add-01, length-1init-01,
newref-1dimprovedall subs proved in-1dim-01, type-in,
okarray-04provedall subs proved isarray-init-02, add-at-ok, length-1init-01, length-init, okreftype-init-02,
okarray-06provedall subs proved is_array-init, in-init-01, length-init, okreftype-init, addarray-at-newref,
okarray-addarray-lenput-primtypeprovedall subs proved add-at-ok, type-1init, add-in, isarray-init-02,
okarray-copyprovedall subs proved lookup-1dim, at-1dim, type-1dim, type-in, length-1dim, length-1dim-02,
okarray-init-04provedall subs proved isarray-init-02, add-at-ok, length-1init-01, length-init, okreftype-init-02,
okarray-init-05provedall subs proved zero-1init-02, in-add, length-1init-01, length-init, okreftype-init-02,
okarray-init-07provedall subs proved add-at-ok, isarray-init-02, length-1init-01, length-init, okreftype-init-02,
okarray-init-basicprovedall subs proved oktype-init-basic, lookup-1init, is_array-init, in-init, okreftype-init,
okclass-1dimprovedall subs proved in-1dim-03, lookup-1dim, in-1dim-01,
subset-addarray-01provedall subs proved subset-addarray, addarray-at-newref, lookup-1init, in-init-01,
zero-1initprovedall subs proved zero-1init-05,
addarray-length-inprovedall subs proved in-init-09, length-init, in-init-01,
addarray-mklist-04provedall subs proved addarray-mklist-03,
init-1dim-01provedall subs proved init-1dim-04, addarray-def,
addbar-okarray-01provedall subs proved add-at-ok-01, in-add, length-1init-01, length-init, okreftype-init-02, addbytearray-ints,
get-add-01provedall subs proved addarrayinit-def, get-add-02,
init-1dim-03provedall subs proved init-1dim-04, init-1dim-05,
isarray-init-01provedall subs proved in-add,
add-gftprovedall subs proved oktype-init-basic, lookup-1init, in-init-01,
okreftype-1dim-01provedall subs proved lookup-1dim-01, in-1dim-08,
zero-1init-02provedall subs proved add-at-ok-01,
isarray-init-02provedall subs proved in-add,
is_array-initprovedall subs proved in-init-01,
in-initprovedall subs proved lookup-1init, in-init-01,
okreftype-initprovedall subs proved lookup-1init, in-init-01,
okarray-addarrayprovedall subs proved in-add, add-at-ok, length-1init-01, length-init, okreftype-init-02,
in-1dim-03provedall subs proved in-1dim-04, addarray-def,
at-1dim-otherprovedall subs proved at-1dim, at-1dim-other-index, at-field-1dim, lookup-1dim,
type-inprovedall subs proved in-1dim-08, addarray-def,
add-at-other-indexprovedall subs proved add-at-gr, add-at-neg,
in-1dim-05provedall subs proved in-1dim-10, addarray-def,
subset-addarrayprovedall subs proved addarray-at-newref, in-init-09,
add-in-other-indexprovedall subs proved in-add,
add-in-otherprovedall subs proved in-add, add-in-fskey, in-1init-02, in-init-01, in-init-09,
zero-1init-05provedall subs proved add-at-ok-01,
subset-putarray2-put-addarray-newrefprovedall subs proved addarray-at-newref, in-init-09,
subset-putarray2-addarray-newrefprovedall subs proved addarray-at-newref, in-init-09,
subset-putarray-addarray-newrefprovedall subs proved addarray-at-newref, in-init-09,
putbytearray-addarray-overrideprovedall subs proved move-initvals,
putByteArray-vals-addarrayprovedall subs proved putarray-addarray, init-switch, addarrayinit-def, add-put-switch, addarray-def,
out-1dimprovedall subs proved out-1dim-01, addarray-def,
one-1init-02provedall subs proved add-at-ok-01,
one-1initprovedall subs proved add-at-ok-01,
okclass-initprovedall subs proved in-1init, lookup-1init, in-init-01,
okarray-putarray-addarray-putprovedall subs proved add-at-ok, type-1init, add-in, in-add,
okarray-init-basic-01provedall subs proved oktype-init-basic-01, is_array-init-01, lookup-1init-01, in-init-02, okreftype-init-01,
okarray-03provedall subs proved okarray-02,
move-initvals-03provedall subs proved move-initvals,
move-initvals-02provedall subs proved move-initvals,
move-initvals-01provedall subs proved move-initvals,
lookup-1dim-05provedall subs proved lookup-1dim-03,
isobj-addbarprovedall subs proved add-isobj, addbytearray-ints,
is_array-addarray-01provedall subs proved add-at-ok-01, length-1init-01, type-1init,
init-1dim-02provedall subs proved init-1dim-05, addarray-def,
getintarray-addarray-01provedall subs proved getarray-addarray-04,
getintarray-addarrayprovedall subs proved getarray-addarray-02,
getbytearray-addarray-thisprovedall subs proved at-1dim, length-1dim,
getbar-addbar-02provedall subs proved get-add-02, addbytearray-ints,
getbar-addbarprovedall subs proved getbar-add, addbytearray-ints,
getbar-add-02provedall subs proved getbar-add-03, lookup-1dim,
getarray-addarray-06provedall subs proved at-1dim, length-1dim,
class-initprovedall subs proved lookup-1init, in-init-01,
atinitprovedall subs proved add-at-ok-01,
addbar-refvalprovedall subs proved addbar-refval-01,
addbar-refsprovedall subs proved add-refs, addbytearray-ints,
addbar-inprovedall subs proved in-init-01, addbytearray-ints,
addarray-refsprovedall subs proved in-1dim-10, in-1dim-04, addarray-def,
addarray-both-subset-01provedall subs proved addarray-both-subset,
add-initprovedall subs proved init-1dim-05, addarray-def,
putarray-addarrayprovedall subs proved 1dim-01, addarray-lastrec, addarray-mklist-02,
out-1dim-01provedall subs proved lookup-1dim-04,
in-1dim-08provedall subs proved in-1dim-17,
is_array-init-01provedall subs proved in-init-02,
addarray-at-newrefprovedall subs proved add-at-01,
okarray-02provedall subs proved is_array-1dim, lookup-1dim, in-1dim-01, okreftype-1dim,
move-initvalsprovedall subs proved add-lastrec,
lookup-1dim-03provedall subs proved lookup-1dim-04, addarray-def,
add-isobjprovedall subs proved addarrayinit-base, addarrayinit-def, add-lastrec,
init-1dim-04provedall subs proved in-1dim-13, lookup-1dim-04, in-1dim-07,
getarray-addarray-04provedall subs proved getarray-addarray-05, add-put-switch, addarray-def,
getarray-addarray-02provedall subs proved getarray-addarray-03, add-put-switch, addarray-def,
getbar-addprovedall subs proved getbar-add-01, lookup-1init,
getbar-add-03provedall subs proved getarray-addarray-other,
get-add-02provedall subs proved init-at, at-init-01, at-init-02, addarrayinit-def,
addbar-refval-01provedall subs proved addarrayinit-def, add-lastrec, addbytearray-ints,
add-refsprovedall subs proved addarrayinit-base, addarrayinit-def, add-lastrec,
okreftype-init-02provedall subs proved type-1init, add-in,
add-at-ok-01provedall subs proved add-at-ok,
in-1dim-04provedall subs proved in-1dim-02, in-1dim-09,
in-1dim-10provedall subs proved addarray-rec, in-1dim-09, addarray-base,
at-1dim-other-indexprovedall subs proved at-1dim-01, at-1dim-other-index-01, add-put-switch, addarray-def,
addarray-mklist-03provedall subs proved addarray-lastrec, addarray-rec, addarray-mklist-02, addarrayinit-base,
addarray-both-subsetprovedall subs proved add-lastrec, addarrayinit-base, addarrayinit-def,
type-1dimprovedall subs proved type-1dim-01, addarray-def,
length-1dimprovedall subs proved length-1dim-01, addarray-def,
init-1dim-05provedall subs proved lookup-1dim-04, in-1dim-07,
add-in-fskeyprovedall subs proved addarrayinit-base, addarrayinit-def, add-lastrec, in-1init-02, in-init-09,
in-addprovedall subs proved addarrayinit-base, addarrayinit-def, add-lastrec,
in-init-01provedall subs proved in-init-02, addarrayinit-def,
add-at-negprovedall subs proved addarrayinit-base, addarrayinit-def, add-lastrec,
add-at-grprovedall subs proved addarrayinit-base, addarrayinit-def, add-lastrec,
addarray-getintarray-otherprovedall subs proved getarray-addarray-other, lookup-1dim,
addarray-getintarray-other-01provedall subs proved getarray-addarray-other,
addarray-mklist-05provedall subs proved addarray-rec, add-lastrec, addarrayinit-base, addarrayinit-def, 1dim,
addarray-modeprovedall subs proved add-lastrec, addarrayinit-base, addarrayinit-def, in-init-09,
addarray-subsetprovedall subs proved add-at-01, in-init-09,
addbar-in-01provedall subs proved in-1init-04, in-1init-02, in-1init, addbytearray-ints,
addbar-type-01provedall subs proved add-in, addbytearray-ints,
at-statfield-01provedall subs proved at-statfield,
endfinallymodeprovedall subs proved add-at-01,
endfinallymode-01provedall subs proved add-at-02,
getarray-addarray-01provedall subs proved getarray-addarray-other-01, lookup-1init,
in-1dim-06provedall subs proved in-1dim-14,
in-1dim-11provedall subs proved in-1dim-12,
in-1init-06provedall subs proved in-1init-04, in-1init-02, in-1init,
in-init-05provedall subs proved in-init-06,
modeprovedall subs proved in-1dim-12, in-1dim-14,
mode-1dimprovedall subs proved mode-1dim-01, addarray-def,
okarray-01provedall subs proved is_array-1dim, lookup-1dim, in-1dim-01, okreftype-1dim,
okarray-1dimprovedall subs proved lookup-1dim, is_array-1dim, in-1dim, okreftype-1dim,
okarray-1dim-01provedall subs proved lookup-1dim, is_array-1dim, in-1dim, okreftype-1dim,
okarray-1dim-02provedall subs proved lookup-1dim, is_array-1dim, in-1dim, okreftype-1dim,
okarray-1dim-03provedall subs proved lookup-1dim, is_array-1dim, in-1dim, okreftype-1dim,
out-1init-01provedall subs proved add-at-04,
putByteArray-vals-addarray-01provedall subs proved addarray-is-putarray-01, addarray-is-putarray, init-switch, addarrayinit-def, add-put-switch, addarray-def,
putarray-add-butlastprovedall subs proved init-switch, addarrayinit-def, putarray-add-same-02, addarray-rec, addarray-def, add-lastrec,
putarray-add-same-01provedall subs proved putarray-add-same-02, addarray-def, addarrayinit-def,
shift-1dim-02provedall subs proved shift-1dim,
subset-putarray2-put-addarray-newref-01provedall subs proved lookup-1dim, in-1dim-14,
succ-1initprovedall subs proved add-at-ok,
switch-addarray-addclassprovedall subs proved switch-addarray-addclass-01, add-put-switch, addarray-def,
switch-addarray-addobjprovedall subs proved switch-addarray-addobj-01, addarray-def,
switch-arrayprovedall subs proved shift-1init, addarrayinit-base, addarrayinit-def, add-lastrec,
at-1dim-other-index-01provedall subs proved at-1dim-01, addarray-rec, addarray-base,
at-statfieldprovedall subs proved lookup-1init,
at-init-01provedall subs proved init-switch,
at-init-02provedall subs proved init-switch,
getarray-addarray-other-01provedall subs proved lookup-1init,
getarray-addarray-05provedall subs proved 1dim, addarray-rec, getarray-addarray-03,
getbar-add-01provedall subs proved lookup-1init,
getarray-addarray-otherprovedall subs proved lookup-1dim,
in-1dim-09provedall subs proved in-1dim-13,
in-1dim-17provedall subs proved in-1dim-07,
in-1dim-other-index-01provedall subs proved in-1dim-15, addarray-rec, addarray-base, in-1dim-13,
in-1init-04provedall subs proved in-1init-03, addarrayinit-def,
length-1dim-01provedall subs proved add-at-05,
in-1dim-12provedall subs proved in-1dim-07, addarray-def,
mode-1dim-01provedall subs proved add-at-05,
is_array-1dimprovedall subs proved is_array-1dim-01, addarray-def,
okreftype-1dimprovedall subs proved lookup-1dim, in-1dim-01,
isarray-1dimprovedall subs proved in-1dim-16,
in-init-02provedall subs proved in-1init-03, addarrayinit-rec, addarrayinit-base, in-1init-01, in-init-08,
okreftype-init-01provedall subs proved lookup-1init-01, in-init-04,
lookup-1dim-04provedall subs proved add-at-05,
putarray-add-same-02provedall subs proved addarray-lastrec, addarrayinit-base, 1dim, addarray-rec,
addarray-mklist-02provedall subs proved addarray-lastrec, addarray-rec, 1dim, addarrayinit-base,
add-at-01provedall subs proved lookup-1init,
num-at-1dimprovedall subs proved at-1dim-01, addarray-def,
add-at-04provedall subs proved lookup-init,
length-1dim-02provedall subs proved in-1dim-13, addarray-def,
at-field-1dimprovedall subs proved add-at-05, addarray-def, lookup-1dim,
at-1dimprovedall subs proved at-1dim-01, addarray-def,
shift-1dimprovedall subs proved shift-1dim-01, addarray-def,
add-at-02provedall subs proved add-at, addarray-def,
in-1dim-14provedall subs proved in-1dim-13, addarray-def,
add-put-switchprovedall subs proved 1dim-01, addarray-base, addarray-rec, shift-1dim-01,
switch-addarray-addobj-01provedall subs proved shift-1dim-01, addarray-base, addarray-rec,
add-lastrecprovedall subs proved init-last, init-switch, addarrayinit-def,
type-1dim-01provedall subs proved add-at-05,
in-1init-02provedall subs proved in-1init-03, addarrayinit-def,
in-init-06provedall subs proved in-init-03, addarrayinit-def,
add-at-okprovedall subs proved init-at, addarrayinit-def,
add-inprovedall subs proved in-init-04, addarrayinit-def,
switch-classprovedall subs proved switch-class-01, init-switch, addarrayinit-def,
subset-putarray2-put-addarray-newref-01-01provedall subs proved lookup-1dim, in-1dim-01,
shift-1init-02provedall subs proved shift-1init,
lookup-init-02provedall subs proved lookup-init,
lookup-1init-02provedall subs proved lookup-1init,
lookup-1dim-06provedall subs proved lookup-1dim,
is_obj-addarray-02provedall subs proved type-1init,
init-addarrayprovedall subs proved init-1init-03,
in-1init-05provedall subs proved addarrayinit-rec, in-1init-03, addarrayinit-base,
class-1dimprovedall subs proved lookup-1dim, in-1dim-01,
atone-1dimprovedall subs proved at-1dim-01, addarray-def,
atint21-1dimprovedall subs proved at-1dim-01, addarray-def,
atint20-1dimprovedall subs proved at-1dim-01, addarray-def,
at-initprovedall subs proved init-switch,
addobj-addarray-switchprovedall subs proved switch-obj,
addbar-typeprovedall subs proved type-1init, addbytearray-ints,
addbar-putrewprovedall subs proved shift-1init, addbytearray-ints,
addbar-newrefprovedall subs proved newref-1init-01, addbytearray-ints,
addbar-modeprovedall subs proved mode-1init-01, addbytearray-ints,
addbar-length-01provedall subs proved length-init, addbytearray-ints,
addbar-lengthprovedall subs proved length-1init-01, addbytearray-ints,
addbar-init-01provedall subs proved init-1init-04, addbytearray-ints,
addbar-initprovedall subs proved init-1init-03, addbytearray-ints,
addbar-getprovedall subs proved lookup-1init, addbytearray-ints,
addbar-addobj-switch-01provedall subs proved switch-obj, addbytearray-ints,
addbar-addobj-switchprovedall subs proved switch-obj, addbytearray-ints,
addarray-putprovedall subs proved shift-1init,
addarray-nouninit-01provedall subs proved init-1init-04,
addarray-initprovedall subs proved init-1init-03,
addarray-at-otherprovedall subs proved lookup-1init,
switch-addarray-addclass-01provedall subs proved 1dim-01, addarray-base, addarray-rec,
addarray-is-putarrayprovedall subs proved 1dim, addarray-rec,
in-1dimprovedall subs proved lookup-1dim-01, in-1dim-02, addarray-def,
is_array-1dim-01provedall subs proved in-1dim-02,
in-init-03provedall subs proved addarrayinit-rec, addarrayinit-base, in-init-08,
in-1init-03provedall subs proved in-1init-01, addarrayinit-rec, addarrayinit-base,
in-1dim-07provedall subs proved addarray-base, addarray-rec, in-1dim-02,
in-1dim-13provedall subs proved in-1dim-02, addarray-base, addarray-rec,
getarray-addarray-03provedall subs proved 1dim, addarray-rec,
add-at-05provedall subs proved lookup-1dim-01, addarray-base, addarray-rec,
at-1dim-01provedall subs proved 1dim, addarray-rec,
newref-1init-01provedall subs proved addarrayinit-base, newref-1init, addarrayinit-def,
mode-1init-01provedall subs proved mode-1init, addarrayinit-def,
in-1initprovedall subs proved in-1init-01, addarrayinit-def,
switch-objprovedall subs proved switch-obj-01, addarrayinit-def,
shift-1initprovedall subs proved shift-1init-01, addarrayinit-def,
init-1init-04provedall subs proved init-1init-01, addarrayinit-def,
addarray-lastrecprovedall subs proved addarrayinit-rec, addarrayinit-base, one-init,
init-1init-03provedall subs proved init-1init, addarrayinit-def,
lookup-1dimprovedall subs proved lookup-1dim-01, addarray-def,
type-1initprovedall subs proved type-1init-01, addarrayinit-def,
length-initprovedall subs proved in-init-08, addarrayinit-def,
length-1init-01provedall subs proved length-1init, addarrayinit-def,
in-1dim-16provedall subs proved in-1dim-15, addarray-def,
in-1dim-01provedall subs proved in-1dim-02, addarray-def,
shift-1dim-01provedall subs proved 1dim-01, addarray-base, addarray-rec,
init-switchprovedall subs proved shift-1init-01, addarrayinit-rec, addarrayinit-base,
init-lastprovedall subs proved addarrayinit-rec, one-init, addarrayinit-base,
in-init-09provedall subs proved in-init-08, addarrayinit-def,
in-init-04provedall subs proved addarrayinit-rec, addarrayinit-base, in-init-08,
init-atprovedall subs proved init-at-01,
lookup-initprovedall subs proved lookup-init-01, addarrayinit-def,
add-atprovedall subs proved lookup-1dim-01,
lookup-1initprovedall subs proved lookup-1init-01, addarrayinit-def,
add-at-03provedall subs proved lookup-1init-01,
getBar-2-putprovedall subs proved 1dim, addarray-rec, addarray-def,
init-1init-05provedall subs proved init-1init-02, addarrayinit-def,
lookup-1dim-02provedall subs proved lookup-1dim-01, addarray-def,
newref-1dim-01provedall subs proved 1dim, addarray-rec,
one-1init-01provedall subs proved one-init, addarrayinit-rec,
out-1initprovedall subs proved lookup-init-01,
store-1initprovedall subs proved init-at-01,
in-1dim-15provedall subs proved addarray-rec,
in-1init-01provedall subs proved addarrayinit-rec, addarrayinit-base,
init-1initprovedall subs proved addarrayinit-rec, addarrayinit-base,
init-1init-01provedall subs proved addarrayinit-rec, addarrayinit-base,
init-1init-02provedall subs proved addarrayinit-rec, addarrayinit-base,
length-1initprovedall subs proved addarrayinit-rec, addarrayinit-base,
in-init-08provedall subs proved addarrayinit-rec, addarrayinit-base,
mode-1initprovedall subs proved addarrayinit-rec, addarrayinit-base,
newref-1initprovedall subs proved addarrayinit-base, addarrayinit-rec,
in-1dim-02provedall subs proved addarray-base, addarray-rec,
lookup-1dim-01provedall subs proved addarray-base, addarray-rec,
lookup-1init-01provedall subs proved addarrayinit-rec, addarrayinit-base,
one-initprovedall subs proved addarrayinit-base, addarrayinit-rec,
lookup-init-01provedall subs proved addarrayinit-rec, addarrayinit-base,
addarray-is-putarray-01provedall subs proved addarrayinit-rec, addarrayinit-base,
1dimprovedall subs proved addarray-base,
shift-1init-01provedall subs proved addarrayinit-rec, addarrayinit-base,
init-at-01provedall subs proved addarrayinit-rec, addarrayinit-base,
1dim-01provedall subs proved addarray-rec,
switch-class-01provedall subs proved addarrayinit-rec, addarrayinit-base,
switch-obj-01provedall subs proved addarrayinit-rec, addarrayinit-base,
type-1init-01provedall subs proved addarrayinit-rec, addarrayinit-base,
one-1init-01-01provedall subs proved addarrayinit-rec,
oktype-1dim-basicprovedall subs proved oktype-1dim-basic-01, addarray-def,
newref-1dim-02provedall subs proved addarray-base,
addbytearray-rewprovedall subs proved addbytearray-ints,
oktype-init-basic-01provedall subs proved
oktype-1dim-basic-01provedall subs proved
oktype-addarrayprovedall subs proved
addbytearray-intsaxiom
addarrayinit-recaxiom
oktype-init-basicprovedall subs proved
addarrayinit-defaxiom
addarrayinit-baseaxiom
addarray-defaxiom
addarray-recaxiom
addarray-baseaxiom