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

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:
multi-newrefsprovedall subs proved multi-newref,
addarrays-typein-02provedall subs proved addarrays-typein-01,
addarrays-typeinprovedall subs proved addarrays-typein-01,
multi-newrefprovedall subs proved multi-refin-other,
addarrays-typein-01provedall subs proved countrefs-getdims-01, getdims-zeroin-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, getdims-posints-01, getdims-empty-01, multi-typein, countrefs-abs, addarrays-def,
addarrays-at-other-01provedall subs proved countrefs-i2n-02, getdims-zeroin, countrefs-getdims, getdims-empty, countdims-empty, countrefs-rec, countdims-rec, countrefs-one, getdims-zero, countdims-zero, countrefs-zero, getdims-rec, getdims-posints-01, getdims-empty-01, multi-at-other, countrefs-abs, addarrays-def, addarrays-empty, countrefs-empty, addarrays-at-other,
addarrays-initdoneprovedall subs proved addarrays-fieldat, addarrays-fieldin,
addarrays-jvmrefprovedall subs proved addarrays-refin,
addarrays-mode-01provedall subs proved addarrays-refin-01, addarrays-fieldin,
addarrays-subsetprovedall subs proved countrefs-not-zero, addarrays-empty, addarrays-at-other, addarrays-refin-01,
endfinallymode-01provedall subs proved addarrays-refin-01, addarrays-fieldin,
multi-first-type-inprovedall subs proved multi-typein,
multi-isarrayrefprovedall subs proved countrefs-one, countrefs-zero, countrefs-lastn-03, countrefs-lastn, multi-isarrayref-notin, multi-at-other, countrefs-rec-02, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
nouninit-addarraysprovedall subs proved addarrays-at-other, addarrays-refin,
addarrays-fieldatprovedall subs proved countrefs-getdims-01, getdims-zeroin-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, getdims-posints-01, getdims-empty-01, multi-field, addarrays-def, addarrays-empty,
addarrays-refin-01provedall subs proved countrefs-getdims-01, getdims-zeroin-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, getdims-posints-01, getdims-empty-01, multi-refin, addarrays-def, addarrays-empty,
addarrays-fieldinprovedall subs proved countrefs-getdims-01, getdims-zeroin-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, getdims-posints-01, getdims-empty-01, multi-fieldin, addarrays-def, addarrays-empty,
multi-typeinprovedall subs proved countrefs-one, countrefs-zero, multi-at-other, multi-refin, countrefs-lastn-03, countrefs-lastn, countrefs-rec-02, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
multi-isarrayref-notinprovedall subs proved multi-in-other,
multi-refin-otherprovedall subs proved multi-in-other,
addarrays-at-otherprovedall subs proved countrefs-i2n-02, getdims-zeroin, countrefs-i2n-01, countrefs-getdims, getdims-empty, countdims-empty, countrefs-rec, countdims-rec, countrefs-one, getdims-zero, countdims-zero, countrefs-zero, getdims-rec, getdims-posints-01, getdims-empty-01, multi-at-other, countrefs-abs, addarrays-def,
addarrays-refinprovedall subs proved countrefs-getdims-01, getdims-zeroin-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, getdims-posints-01, getdims-empty-01, multi-in-other, addarrays-def, addarrays-empty,
multi-subsetprovedall subs proved multi-at-other, multi-refin,
multi-lengthinprovedall subs proved countrefs-one, countrefs-zero, multi-at-other, multi-refin, countrefs-lastn-03, countrefs-lastn, countrefs-rec-02, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
multi-isarrayref-01provedall subs proved multi-in-other,
endfinallymodeprovedall subs proved getdims-zeroin-01, countrefs-getdims-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, countrefs-not-zero, getdims-posints-01, getdims-empty-01, multi-field, addarrays-def, addarrays-empty,
countrefs-le-03provedall subs proved countrefs-le-01,
addarrays-type-01provedall subs proved addarrays-type,
addarrays-outprovedall subs proved getdims-zeroin-01, countrefs-getdims-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, getdims-posints-01, getdims-empty-01, multi-field, addarrays-def, addarrays-empty,
addarrays-modeprovedall subs proved getdims-zeroin-01, countrefs-getdims-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, countrefs-not-zero, getdims-posints-01, getdims-empty-01, multi-field, addarrays-def, addarrays-empty,
addarrays-length-01provedall subs proved addarrays-length,
countrefs-le-01provedall subs proved countrefs-le,
addarrays-typeprovedall subs proved countdims-notneg, countrefs-getdims-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, getdims-zeroin, getdims-posints, getdims-empty-01, multi-type-first, addarrays-def, addarrays-empty,
multi-refinprovedall subs proved countrefs-zero, countrefs-lastn-03, countrefs-lastn, countrefs-rec-02, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
multi-in-otherprovedall subs proved countrefs-one, countrefs-zero, countrefs-lastn-03, countrefs-lastn, countrefs-rec-02, countrefs-inrefs, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
addarrays-lengthprovedall subs proved countrefs-getdims-01, getdims-zeroin-01, countdims-rec, countdims-zero, countrefs-zero, getdims-zero, getdims-rec, getdims-posints-01, getdims-empty-01, multi-length-first, addarrays-def, addarrays-empty,
multi-fieldinprovedall subs proved countrefs-one, countrefs-zero, countrefs-lastn-03, countrefs-lastn, countrefs-rec-02, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
multi-fieldprovedall subs proved countrefs-one, countrefs-zero, countrefs-lastn-03, countrefs-lastn, countrefs-rec-02, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
multi-at-otherprovedall subs proved countrefs-lastn-02, countrefs-lastn-01, countrefs-i2n-02, countrefs-i2n-01, countrefs-zero, countrefs-one, countrefs-rec, countrefs-lastn, countrefs-inrefs, countrefs-rec-02, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
addarrays-one-01provedall subs proved addarrays-one,
multg-at-refprovedall subs proved countrefs2-pos-01, countrefs2-not-mone, countrefs2-pos, countrefs2-02, addarraymultlist_zero, countrefs2-empty, intssize-rec, addarraymultlist_more_1, countrefs2-03, countrefs2-01, addarraymultlist_more_2, addarraymultlist_more_0, addarraymultlist_one_not_0, addarraymultlist_one_0,
multi-length-firstprovedall subs proved countrefs-zero, countrefs-rec-02, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
addarrays-oneprovedall subs proved addmultiarrays-base, getdims-zero-04, countrefs-one, addarrays-def,
multi-type-firstprovedall subs proved countrefs-one, countrefs-zero, countrefs-rec-02, countrefs-not-zero-01, countrefs-i2n, countrefs-rec-01, addmultiarrays-rec, addmultiarrays-done, addmultiarrays-base,
countrefs-leprovedall subs proved countrefs-ls, countrefs-not-zero, countrefs-not-zero-01,
getdims-zeroin-01provedall subs proved getdims-zeroin, getdims-empty, getdims-empty-01,
countrefs-getdims-01provedall subs proved countrefs-one, countrefs-getdims, countrefs-rec, countrefs-zero-01, getdims-empty-01, countrefs-base,
countrefs2-pos-01provedall subs proved countrefs2-pos,
countrefs2-not-moneprovedall subs proved countrefs2-pos,
countrefs2-03provedall subs proved countrefs2-pos,
countrefs-i2n-02provedall subs proved countrefs-i2n-01,
countrefs-lastnprovedall subs proved countrefs-not-zero-01,
multi-mode-01provedall subs proved multi-mode, addarraymult,
addarrays-auto-22provedall subs proved addarrays-empty, addmultiarrays-done, addmultiarrays-base, addmultiarrays-rec, getdims-zero-04, getdims-rec, countdims-one-02, countdims-rec, countrefs-one, countrefs-rec, addarrays-def,
multi-modeprovedall subs proved countrefs2-02, intssize-rec, addarraymultlist_zero, addarraymultlist_more_1, addarraymultlist_more_2, addarraymultlist_more_0, addarraymultlist_one_not_0, addarraymultlist_one_0,
countrefs-i2nprovedall subs proved countrefs-not-zero,
countrefs-rec-02provedall subs proved countrefs-not-zero, countrefs-zero, countrefs-rec,
countrefs2-posprovedall subs proved countrefs_more_le0, countrefs_more_gr0, countrefs2-01, countrefs2-one-01, countrefs2-02, countrefs2-empty,
countrefs-lsprovedall subs proved countrefs-not-zero, countrefs-rec, countrefs-zero-01, countrefs-base,
countrefs-not-zero-01provedall subs proved countrefs-not-zero, countrefs-rec, countrefs-zero-01, countrefs-base, countrefs-empty,
getdims-posintsprovedall subs proved getdims-zero-01, getdims-rec, getdims-empty,
countdims-one-02provedall subs proved countdims-one-03,
getdims-zero-04provedall subs proved getdims-zero-02, getdims-empty, getdims-rec,
countrefs-absprovedall subs proved countrefs-not-zero,
countrefs-getdimsprovedall subs proved getdims-empty-01, countrefs-rec, countrefs-zero-01, countrefs-one, getdims-zero, getdims-rec, countrefs-empty, getdims-empty,
countrefs-i2n-01provedall subs proved countrefs-not-zero,
getdims-zeroinprovedall subs proved getdims-empty, getdims-zero, getdims-rec, getdims-empty-01,
countrefs-autoprovedall subs proved countrefs-one, countrefs-rec,
countrefs-le-02provedall subs proved countrefs-not-zero, countrefs-rec,
countrefs2-oneprovedall subs proved countrefs2-02,
countrefs2-twoprovedall subs proved countrefs2-one-01, countrefs_more_gr0,
countrefs2-zeroprovedall subs proved countrefs2-one-01, countrefs_more_le0,
countdims-notnegprovedall subs proved countdims-zero, countdims-rec, countdims-empty,
countdims-one-03provedall subs proved countdims-empty, countdims-rec,
countrefs-emptyprovedall subs proved countrefs-base,
countrefs2-one-01provedall subs proved countrefs_one,
countrefs-not-zeroprovedall subs proved countrefs-rec, countrefs-zero-01, countrefs-base,
getdims-posints-01provedall subs proved getdims-zero, getdims-rec, getdims-empty,
getdims-zero-01provedall subs proved getdims-zero,
getdims-zero-02provedall subs proved getdims-zero,
getdims-empty-01provedall subs proved getdims-zero, getdims-rec, getdims-empty,
countrefs2-emptyprovedall subs proved countrefs_one,
countrefs2-01provedall subs proved countrefs_more_gr0,
countrefs2-02provedall subs proved countrefs_more_gr0,
countrefs-oneprovedall subs proved countrefs-base,
countrefs-zeroprovedall subs proved countrefs-zero-01, countrefs-base,
countrefs-rec-01provedall subs proved countrefs-rec,
getdims-zero-03provedall subs proved getdims-rec,
getcountdimsprovedall subs proved getdims-rec, countdims-zero, getdims-zero, countdims-rec, getdims-empty, countdims-empty,
countrefs2provedall subs proved countrefs_more_gr0,
countmore2provedall subs proved countrefs_more_gr0,
countdims-zero-04provedall subs proved countdims-zero, countdims-rec, countdims-empty,
countdims-zero-03provedall subs proved countdims-zero, countdims-rec, countdims-empty,
countdims-zero-02provedall subs proved countdims-zero,
countdims-zero-01provedall subs proved countdims-zero,
countdims-one-01provedall subs proved countdims-empty, countdims-rec,
countdims-oneprovedall subs proved countdims-rec,
addmultidim_emptyprovedall subs proved addarraymultlist_zero,
addmultiarrays-base-01provedall subs proved addmultiarrays-base,
addarrays-caseprovedall subs proved addarrays-empty, addarrays-def,
addarraymultaxiom
countrefs-lastn-03provedall subs proved
countrefs-inrefsprovedall subs proved
countrefs-lastn-01provedall subs proved
countrefs-lastn-02provedall subs proved
addarraymultlist_one_0axiom
addarraymultlist_one_not_0axiom
addarraymultlist_more_0axiom
addarraymultlist_more_2axiom
addarraymultlist_more_1axiom
intssize-recaxiom
countrefs_more_le0axiom
countrefs_oneaxiom
countrefs-zero-01axiom
countrefs-baseaxiom
countrefs_more_gr0axiom
addarraymultlist_zeroaxiom
addmultiarrays-recaxiom
addmultiarrays-baseaxiom
addmultiarrays-doneaxiom
addarrays-emptyaxiom
addarrays-defaxiom
getdims-recaxiom
countdims-zeroaxiom
getdims-zeroaxiom
countdims-recaxiom
countrefs-recaxiom
countdims-emptyaxiom
getdims-emptyaxiom