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

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:
lookup-sevenprovedall subs proved lookup-six, lookup-rec,
lookup-put-rkvs-diff-03provedall subs proved lookup-put-rkvs-01, put-refkeyvalues-rec,
lookup-put-rkvs-diff-02provedall subs proved lookup-put-rkvs-01, put-refkeyvalues-rec,
lookup-put-rkvs-diff-01provedall subs proved lookup-put-rkvs-01, put-refkeyvalues-rec,
lookup-put-rkvs-diffprovedall subs proved lookup-put-rkvs-01, put-refkeyvalues-rec,
initdone-put-rkvsprovedall subs proved initundone-01, initdone-01, initundone, lookup-put-rkvs-notin, in-put-rkvs, initerror, initdone,
init-put-rkvs-01provedall subs proved lookup-put-rkvs-notin, initundone-01, initdone-01, initundone, in-put-rkvs, initerror, initdone, init-existing,
in-put-rkvs-modeprovedall subs proved in-put-rkvs, put-refkeyvalues-rec,
in-put-rkvs-01provedall subs proved in-put-rkvs, put-refkeyvalues-rec,
lookup-sixprovedall subs proved lookup-five, lookup-rec,
lookup-put-rkvs-01provedall subs proved put-rkvs-absorb, put-rkvs-switch,
in-put-rkvsprovedall subs proved put-rkvs-absorb, put-rkvs-switch, put-rkvs-one-01, put-rkvs-append, put-refkeyvalues-empty,
init-put-rkvsprovedall subs proved init-put-notnull, put-rkvs-absorb, put-rkvs-switch, put-refkeyvalues-rec,
initdone-at-type-02provedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, init-put-19, put-one, put-last-rec,
lookup-put-rkvs-modeprovedall subs proved put-rkvs-absorb, put-rkvs-switch, put-refkeyvalues-rec,
newrefs-butlastprovedall subs proved newrefs-last-01, newrefs-butlast-01,
put-rkvs-absorb-01provedall subs proved put-rkvs-absorb, put-refkeyvalues-rec,
init-put-19provedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, initdone-06,
lookup-fiveprovedall subs proved lookup-four, lookup-rec,
newrefs-last-01provedall subs proved newref-02, newrefs-new, instore-02, newref-new, newrefs-empty, newrefs-rec-01, newrefs-succ, newrefs-zero, newrefs-one-01,
put-rkvs-absorbprovedall subs proved put-rkvs-switch, put-rkvs-one, put-rkvs-append, put-refkeyvalues-empty, put-rkvs-last,
put-rkvs-switch-02provedall subs proved put-rkvs-switch,
put-rkvs-switch-01provedall subs proved put-rkvs-switch, put-refkeyvalues-rec,
newrefs-lastprovedall subs proved newrefs-empty, newrefs-new,
newreflist-dupsprovedall subs proved newreflist-dups-01,
newref-newref-notinprovedall subs proved newref-newref, newref-in-01,
lookup-supersetprovedall subs proved lookup-subset-01,
initdone-at-type-05provedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, init-put-22, put-one, put-last-rec,
initdone-at-type-04provedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, init-put-21, put-one, put-last-rec,
initdone-at-type-03provedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, init-put-20, put-one, put-last-rec,
initdone-at-type-01provedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, init-put-18, put-one, put-last-rec,
initdone-at-typeprovedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, init-put-17, put-one, put-last-rec,
init-put-field-07provedall subs proved init-put-field-01,
init-put-field-06provedall subs proved init-put-field-01,
init-put-field-05provedall subs proved init-put-field-01,
init-put-field-04provedall subs proved init-put-field-01,
init-put-field-03provedall subs proved init-put-field-01,
init-put-field-02provedall subs proved init-put-field-01,
exists-twonewprovedall subs proved instore-01, newref, maxref-exists-01,
exists-fournewprovedall subs proved instore-01, newref, maxref-exists-01,
del-refs-sizeprovedall subs proved del-subset-del, in-empty, instore-01, instore, del-notin-01,
newrefs-newprovedall subs proved instore-01, newrefsnew, newref, newrefs-succ, newrefs-zero,
newreflist-dups-01provedall subs proved instore-02, newrefs-in, newrefs-succ, newrefs-zero,
newref-newrefprovedall subs proved newrefsnew, new-insert, newref-fun,
lookup-subset-01provedall subs proved lookup-empty, lookup-subset,
lookup-fourprovedall subs proved lookup-three, lookup-rec,
init-put-22provedall subs proved initundone-01, initdone-01, initundone, init-put-16, initerror, initdone,
init-put-21provedall subs proved initundone-01, initdone-01, initundone, init-put-15, initerror, initdone,
init-put-20provedall subs proved initundone-01, initdone-01, initundone, init-put-14, initerror, initdone,
init-put-18provedall subs proved initundone-01, initdone-01, initundone, init-put-09, initerror, initdone,
init-put-17provedall subs proved initundone-01, initdone-01, initundone, init-put-07, initerror, initdone,
init-put-notnullprovedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, init-put, init-existing,
init-put-field-01provedall subs proved init-put-field, put-one, put-last-rec,
initdone-06provedall subs proved initundone-01, initdone-01, initundone, init-put-13, initerror, initdone,
put-rkvs-switchprovedall subs proved put-rkvs-one, put-rkvs-append, put-refkeyvalues-empty, put-rkvs-last,
maxref-exists-01provedall subs proved maxref-exists,
del-notin-01provedall subs proved instore-01, look-del, in-del,
del-subset-delprovedall subs proved look-del, in-del,
at-put-first-03provedall subs proved lookup-one, at-put-first-01,
at-put-first-05provedall subs proved at-put-first-04, lookup-one,
at-put-first-06provedall subs proved at-put-first-04,
at-put-keys-04provedall subs proved at-put-keys,
at-put-last-other-01provedall subs proved at-put-last-other, at-put-keys-01,
at-put-sameprovedall subs proved at-put-keys-02, lookup-rec-01, put-rec-01, lookup-one, put-one,
at-put-same-01provedall subs proved at-put-same-02,
del-notinprovedall subs proved in-del, instore,
del-putprovedall subs proved in-del-01, look-del, in-del,
del-put-switchprovedall subs proved look-del, in-del-01, in-del,
del-subsetprovedall subs proved look-del, in-del,
del-switchprovedall subs proved in-del-01, look-del, in-del,
in-mode-putprovedall subs proved put-one, in-put,
init-03provedall subs proved init-01,
init-endfmodeprovedall subs proved initundone-01, initdone-01, initundone, init-endfmode-01, initerror, init-endfmode-02, initdone, init-put-04,
init-put-indexprovedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, initdone-02, init-existing,
init-uninitprovedall subs proved init-uninit-01,
initdone-05provedall subs proved initundone-05, initerror-05, initdone-01,
lookup-put-keys-01provedall subs proved lookup-one, lookup-put-keys,
lookup-put-keys-02provedall subs proved lookup-put-keys,
mode-put-sks-array-01provedall subs proved mode-put-sks-array, put-storerefs,
newref-delprovedall subs proved instore-01, in-del, newref,
newref-del-01provedall subs proved in-del, newref, newjvmref,
newref-existsprovedall subs proved instore-01, newref, maxref-exists,
newref-newreflist-subsetprovedall subs proved stsubset-new, newref-newref-subset, newref, newrefs-succ, newrefs-rec-01, newrefs-zero,
newref-notin-01provedall subs proved ref-in, newref-subset,
newref-put-inprovedall subs proved instore-01, ref-in, newref-same,
newref-subset-01provedall subs proved subset-newref,
newref-subset-02provedall subs proved subset-newref,
newreflist-null-01provedall subs proved newreflist-null,
newrefs-firstprovedall subs proved newrefsnew, newrefs-succ,
newrefs-new-01provedall subs proved newref-new, instore-01, newrefs-null, newref-jvmref, instore, instore-02, newrefs-in, newref, newref-02, list_ok, newrefsnew, newrefs-rec, newrefs-succ, newrefs-base, newrefs-zero,
newrefs-restprovedall subs proved instore-02, newrefs-in, newrefs-succ,
newrefs-threeprovedall subs proved instore-02, newref-new, instore-01, newref-notin, newref-in, instore, newref-jvmref, newref-def, newrefs-one-01, newrefs-rec-01, newrefsnew,
newrefs-twoprovedall subs proved instore-02, newref-new, newref-in, instore-01, instore, newref-jvmref, newref-def, newrefs-one-01, newrefs-rec-01, newrefsnew,
put-sks-fs-array-01provedall subs proved put-sks-fs-array, put-storerefs,
refin-delprovedall subs proved instore-01, look-del, in-del, instore, deleteref,
subset-deleteprovedall subs proved instore-01, in-del, delete-at,
at-put-first-01provedall subs proved at-put-other-02, lookup-rec-01,
at-put-first-04provedall subs proved lookup-rec-01, put-two,
at-put-keysprovedall subs proved at-put-keys-01,
at-put-last-otherprovedall subs proved lookup-rec-01, lookup-one, put-one, put-rec-01, at-put-keys-01,
at-put-keys-02provedall subs proved at-put-keys-01,
at-put-same-02provedall subs proved put-last-rec,
in-putprovedall subs proved lookup-rec-01, put-rec-01, put-two, lookup-one,
init-01provedall subs proved initundone-01, init, initdone-01,
init-endfmode-01provedall subs proved initundone, initundone-01, init-05,
init-put-04provedall subs proved initundone-01, initdone-01, initundone, initerror, initdone,
init-put-07provedall subs proved initundone, initundone-01, init-05,
init-put-09provedall subs proved initundone, initundone-01, init-05,
init-put-14provedall subs proved initundone, initundone-01, init-05,
init-put-15provedall subs proved initundone, initundone-01, init-05,
init-put-16provedall subs proved initundone, initundone-01, init-05,
init-put-fieldprovedall subs proved instore-01, init-def,
initdone-02provedall subs proved initundone-01, initundone-02, initerror-01, initerror-02, initdone-01,
init-putprovedall subs proved initundone-01, init-put-01, initerror-01, init-put-02, initdone-01,
init-uninit-01provedall subs proved init-def, uninit-def,
initundone-05provedall subs proved initerror-01, initdone-01, init-04, initundone-01,
initerror-05provedall subs proved initundone-01, initdone-01, init-04, instore-01, initerror-01,
init-put-13provedall subs proved initundone, initundone-01, init-05,
lookup-put-rkvs-notinprovedall subs proved put-rkvs-one-01, put-rkvs-append, put-refkeyvalues-empty,
lookup-threeprovedall subs proved lookup-two, lookup-rec,
lookup-put-keysprovedall subs proved at-put-keys-01, lookup-rec-01,
lookup-subsetprovedall subs proved lookup-rec-01, instore-01, instore-one, lookup-one, instore-rec-01,
mode-put-sks-arrayprovedall subs proved put-one, put-last-rec,
maxref-existsprovedall subs proved instore-02, instore,
newref-newref-subsetprovedall subs proved newref-jvmref, newref-def, newref-in, subset-notin,
ref-inprovedall subs proved instore-02,
subset-newrefprovedall subs proved subset-notin, newref-def, newref-01,
newreflist-nullprovedall subs proved newrefs-null,
newrefs-inprovedall subs proved instore-02, newref-in, newrefs-succ, newrefs-zero,
newrefsnewprovedall subs proved newref-in, newref-jvmref, newref-def,
put-rkvs-lastprovedall subs proved put-rkvs-one, put-rkvs-append,
put-sks-fs-arrayprovedall subs proved put-one, put-last-rec,
in-delprovedall subs proved in-del-01,
subset-instoreprovedall subs proved subset-notin,
refinprovedall subs proved instore-02,
put-rkvs-list-02provedall subs proved put-rkvs-one, put-rkvs-append,
put-list-intro-01provedall subs proved put-one, lookup-empty, put-last-rec,
put-last-rec-betterprovedall subs proved lookup-empty, put-one, put-last-rec,
normal-lookup-02provedall subs proved normalmode, normal, normal-return, newref,
normal-lookup-01provedall subs proved normalmode, normal, normal-return,
normal-lookupprovedall subs proved normal-return, normal-out,
newrefs-jvmrefprovedall subs proved newjvmref, newrefs-rec,
newrefs-01provedall subs proved newrefs-rec, newrefs-one, newref,
newref-put-in-01provedall subs proved instore-02, newref-subset, newref-jvmref, newref-def,
newref-put-01provedall subs proved newref-notin,
newref-putprovedall subs proved newref, newref-02,
newref-emptyprovedall subs proved newref, newjvmref,
new-insert-01provedall subs proved newref, newref-02,
mode-at-type-05provedall subs proved put-one, put-last-rec,
mode-at-type-04provedall subs proved put-one, put-last-rec,
mode-at-type-03provedall subs proved put-one, put-last-rec,
mode-at-type-02provedall subs proved put-one, put-last-rec,
mode-at-type-01provedall subs proved put-one, put-last-rec,
mode-at-typeprovedall subs proved put-one, put-last-rec,
lookup-sk-list-appendprovedall subs proved lookup-one, lookup-append,
lookup-put-rkvsprovedall subs proved put-rkvs-one-01, put-rkvs-append, put-refkeyvalues-empty, put-refkeyvalues-rec,
lookup-put-otherprovedall subs proved lookup-put-ex-first,
lookup-list-list-appendprovedall subs proved lookup-empty, lookup-append,
lookup-list-intro-06provedall subs proved lookup-list-intro-05,
lookup-list-intro-04provedall subs proved lookup-list-intro-02,
lookup-list-intro-03provedall subs proved lookup-list-intro-01,
lookup-list-introprovedall subs proved lookup-two,
lookup-list-butlastprovedall subs proved lookup-empty, lookup-one, lookup-last-rec,
initdone-04provedall subs proved initundone-01, initundone-04, initerror-01, initerror-04, initdone-01,
initdone-03provedall subs proved initundone-01, initundone-03, initerror-01, initerror-03, initdone-01,
initP-putprovedall subs proved initundone-01, initerror, initdone-01, initdoneP,
init-totalprovedall subs proved instore-01, initundone-01, initdone-01, initerror, initundone,
init-put-shortprovedall subs proved instore-01, initundone-01, initdone-01, initundone, initerror, initdone,
init-put-nonvoidprovedall subs proved initundone-01, initdone-01, initundone, initerror, initdone, init-existing,
init-put-24provedall subs proved instore-01, initundone-01, initdone-01, initundone, initerror, init-put-08, initdone,
init-put-23provedall subs proved instore-01, init-def,
init-put-12provedall subs proved initundone-01, initerror-01, initdone-01,
init-put-06provedall subs proved instore-01, init-def,
init-put-03provedall subs proved initundone-01, initdone-01, initundone, initerror, init-put-08, initdone,
init-outprovedall subs proved initundone-01, init-out-01, initerror-01, init-out-02, initdone-01,
init-mode-03provedall subs proved initundone-01, init-mode-04, initerror-01, init-mode-05, initdone-01,
init-done-01provedall subs proved instore-01, initundone-01, initdone-01, initundone, initerror, initdone,
init-doneprovedall subs proved initundone-01, initerror, initdone-01,
in-put-sameprovedall subs proved put-two,
in-put-keys-02provedall subs proved in-put-keys,
in-put-keys-01provedall subs proved in-put-keys,
in-list-subsetprovedall subs proved instore-01, instore-rec-01, instore-one,
in-list-putprovedall subs proved instore-rec-01, instore-one,
at-put-same-04provedall subs proved put-two,
at-put-other-03provedall subs proved at-put-other-02,
at-put-other-01provedall subs proved at-put-other-02, lookup-one, lookup-rec-01, lookup-storerefs,
at-put-keys-05provedall subs proved at-put-keys-01,
at-put-keys-03provedall subs proved at-put-keys-01,
at-put-first-rec-04provedall subs proved at-put-first-rec,
at-put-first-rec-03provedall subs proved lookup-one, at-put-first-rec,
at-put-first-rec-02provedall subs proved at-put-first-rec,
at-put-first-rec-01provedall subs proved lookup-one, at-put-first-rec,
at-put-first-02provedall subs proved lookup-two,
delete-atprovedall subs proved look-del,
normal-returnprovedall subs proved normal,
newref-newprovedall subs proved newref-in,
newrefs-butlast-01provedall subs proved newrefs-empty, newrefs-rec-01, newrefs-succ, newrefs-one-01, newrefs-zero,
newrefs-recprovedall subs proved instore-01, newref, list_ok,
newrefs-nullprovedall subs proved newref-jvmref, newrefs-succ, newrefs-zero,
newref-notinprovedall subs proved newref-in, instore-01,
newref-subsetprovedall subs proved newref-in,
stsubset-newprovedall subs proved instore-01, newref,
subset-notinprovedall subs proved instore-01, instore,
newref-defprovedall subs proved instore-01, instore, newref,
newref-in-01provedall subs proved instore-01, instore, newref,
new-insertprovedall subs proved instore-01, newref,
newjvmrefprovedall subs proved newref-01,
newref-02provedall subs proved instore-01, newref,
instore-02provedall subs proved instore-01, instore,
lookup-put-ex-firstprovedall subs proved lookup-one, lookup-rec-01, lookup-empty,
lookup-appendprovedall subs proved lookup-rec-01, lookup-one,
lookup-list-intro-05provedall subs proved lookup-rec-01,
lookup-list-intro-02provedall subs proved lookup-rec-01, lookup-one,
lookup-list-intro-01provedall subs proved lookup-rec-01, lookup-one,
lookup-last-recprovedall subs proved lookup-one, lookup-rec-01,
initerror-04provedall subs proved instore-01, initerror,
initundone-04provedall subs proved instore-01, initundone, initundone-01,
initerror-03provedall subs proved initerror-01,
initundone-03provedall subs proved initundone-01,
initerror-02provedall subs proved initerror-01,
initundone-02provedall subs proved initundone-01,
uninit-defprovedall subs proved instore-01, initundone-01, uninit,
init-defprovedall subs proved instore-01, initundone, initerror, initdone, init-04,
init-put-01provedall subs proved initundone-01,
init-out-01provedall subs proved initundone, initundone-01,
init-mode-04provedall subs proved initundone, initundone-01,
init-05provedall subs proved initundone, initundone-01,
init-endfmode-02provedall subs proved init-06,
initdone-01provedall subs proved initundone-01, initerror-01, initdone,
initprovedall subs proved instore-01, initundone-01, initerror-01,
put-rkvs-appendprovedall subs proved put-rkvs-rec, put-refkeyvalues-empty,
put-rkvs-one-01provedall subs proved put-rkvs-one,
in-put-keysprovedall subs proved put-rec-01, put-one,
instore-rec-01provedall subs proved instore-rec, instore-two, instore-one,
in-del-01provedall subs proved instore-01, look-del, deleteref,
put-last-recprovedall subs proved lookup-rec-01, lookup-one, put-one, put-rec-01,
at-put-keys-01provedall subs proved put-rec-01, put-one,
at-put-first-recprovedall subs proved lookup-rec-01,
put-twoprovedall subs proved put-one, put-rec-01,
lookup-twoprovedall subs proved lookup-one, lookup-rec-01,
at-put-other-02provedall subs proved lookup-one, lookup-rec-01,
at-put-firstprovedall subs proved lookup-rec-01, lookup-storerefs,
at-put-otherprovedall subs proved lookup-rec-01, lookup-storerefs,
in-butminprovedall subs proved in-empty, instore-01, instore,
in-butmin-01provedall subs proved instore-01, instore,
indelprovedall subs proved instore-01, instore,
init-put-05provedall subs proved initerror, init-put-08,
init-put-11provedall subs proved initundone-01,
lookup-list-put-exprovedall subs proved lookup-one, lookup-rec-01, lookup-empty,
lookup-rec-refvalprovedall subs proved lookup-empty, lookup-one, lookup-rec-01,
mode-delprovedall subs proved look-del,
mode-notinprovedall subs proved instore-01,
new-mode-01provedall subs proved instore-01, newref,
new-outprovedall subs proved instore-01, newref,
newref-03provedall subs proved instore-01, newref, instore,
newref-in-02provedall subs proved instore-01, newref,
newref-in-03provedall subs proved instore-01, instore, newref,
normal-throwprovedall subs proved normal,
put-list-introprovedall subs proved put-one, put-rec-01,
put-put-first-01provedall subs proved put-rec-01,
put-put-switchprovedall subs proved put-one, put-rec-01,
put-rkvs-listprovedall subs proved put-rkvs-one, put-refkeyvalues-rec,
subset-put-notinprovedall subs proved instore-01,
uninit-01provedall subs proved initundone-01, uninit, initundone, initerror, initdone,
uninit-02provedall subs proved initundone-01, uninit, instore-01, initerror,
uninit-03provedall subs proved initundone-01, uninit, initundone,
in-emptyprovedall subs proved instore,
init-06provedall subs proved initerror,
init-mode-05provedall subs proved initerror,
init-out-02provedall subs proved initerror,
init-put-02provedall subs proved initerror,
init-put-08provedall subs proved initerror,
initerror-01provedall subs proved initerror,
instore-twoprovedall subs proved instore-rec, instore-one,
newref-sameprovedall subs proved maxref-ok, maxref-empty, newref-fun,
newrefs-oneprovedall subs proved newref, list_ok,
newrefs-emptyprovedall subs proved newrefs-succ, newrefs-zero,
newrefs-baseprovedall subs proved list_ok,
newrefs-one-01provedall subs proved newrefs-zero, newrefs-succ,
newrefs-rec-01provedall subs proved newrefs-succ,
newref-inprovedall subs proved maxref-ok, maxref-empty, newref-fun,
newref-jvmrefprovedall subs proved maxref-empty, newref-fun,
normal-outprovedall subs proved normalmode,
normalprovedall subs proved normalmode,
lookup-rec-01provedall subs proved lookup-rec,
put-rkvs-recprovedall subs proved put-refkeyvalues-rec,
put-rkvs-oneprovedall subs proved put-refkeyvalues-empty, put-refkeyvalues-rec,
put-rec-01provedall subs proved put-rec,
look-delprovedall subs proved deleteref,
newref-01provedall subs proved newref,
instore-01provedall subs proved instore,
initundone-01provedall subs proved initundone,
put-rkvs-list-01provedall subs proved put-refkeyvalues-rec,
newrefs-lengthprovedall subs proved newrefs-succ, newrefs-zero,
newrefs-lastnprovedall subs proved newref, list_ok,
newrefs-firstnprovedall subs proved newref, list_ok,
newrefsprovedall subs proved newref, list_ok,
new-modeprovedall subs proved newref,
mode-01provedall subs proved instore,
initdone-uninitprovedall subs proved initundone, initerror, initdone,
init-put-10provedall subs proved initerror,
init-errorprovedall subs proved initerror,
init-02provedall subs proved initundone, initdone, initerror,
in-minprovedall subs proved instore,
uninitaxiom
put-recaxiom
normalmodeaxiom
list_okaxiom
newrefs-zeroaxiom
newrefs-succaxiom
newref-funaxiom
maxref-emptyaxiom
maxref-okaxiom
put-storerefsaxiom
lookup-emptyaxiom
lookup-recaxiom
instore-recaxiom
initdonePaxiom
init-existingaxiom
init-04axiom
initerroraxiom
initdoneaxiom
initundoneaxiom
put-refkeyvalues-recaxiom
put-refkeyvalues-emptyaxiom
instore-oneaxiom
deleterefaxiom
newrefaxiom
instoreaxiom
put-oneaxiom
lookup-oneaxiom
lookup-storerefsaxiom