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

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:
orderedls-append2-splitprovedall subs proved ordered-append-split1,
ordered-last3provedall subs proved orderedls-le-attach, ordered-append-split1,
ordered-append-split1provedall subs proved orderedls-twolast, ls-r, ls-o, cons, ordered-append-split2,
orderedls-twolastprovedall subs proved ordered-attach,
ordered-ordered-subset-orderedprovedall subs proved orderedls-le, ordered-append-second, ordered-append-split2, ordered-append,
ordered-sublist2provedall subs proved orderedls-le, ordered-append-second, ordered-append,
ordered-append-secondprovedall subs proved ls-e, ordered-append,
ordered-attachprovedall subs proved ls-o, ordered-append,
ordls-appendprovedall subs proved ls-e, ordered-append,
ordered-appendprovedall subs proved ordered-append-split2,
ole-last-01provedall subs proved ole-last,
orderedle-twolastprovedall subs proved app, ole-last,
ordered-last2provedall subs proved ols-two, ordered-append-split2,
ordered-nodupprovedall subs proved orderedls-le, ordered-append-split2,
ordered-last1provedall subs proved ordered-append-split2,
ordered-sublistprovedall subs proved ordered-append-first, ordered-append-split2,
ordle-appendprovedall subs proved orderedle-append2-split, app, orderedle-append, app-01, cons-02,
orderedle-append2-splitprovedall subs proved le-r, app, orderedle-append, cons-02, app-01,
ordered-append-split2provedall subs proved ols-rec, ls-r, ordered-append-first, orderedCombined-Two-Lists,
ole-lastprovedall subs proved le-o, le-r, ole-in, ole-rec, app-02, app, app-01, cons-02, ole-two,
orderedls-eq-attachprovedall subs proved orderedls-le-attach,
ordered-ex-divide-lsleprovedall subs proved orderedle-ls, app-01, cons-02, le-e,
ordered-ex-divide-lelsprovedall subs proved orderedle-ls, app-01, cons-02, le-e,
perm-insprovedall subs proved del1-02, in-04, insperm-01,
orderedle-allprovedall subs proved orderedle-ls, cons-02, le-o, ole-rec, le-e,
insperm-01provedall subs proved insperm,
orderedle-appendprovedall subs proved k-le-r, app, le-r, le-o, cons-02, le-e,
orderedCombined-Two-Listsprovedall subs proved ols-rec, ls-r, ls-o, cons,
ordered-append-firstprovedall subs proved ls-r, ls-o, ols-rec, ls-e,
orderedle-lsprovedall subs proved cons-02, ole-in,
ols-twoprovedall subs proved ls-o, ols-rec,
app-02provedall subs proved app-01, cons-02, app,
orderedls-le-attachprovedall subs proved orderedls-ls, ols-rec,
del1provedall subs proved orderedls-ls, ls-o, ols-rec, cons, ls-e,
insperm-02provedall subs proved ins-y, ins-n, insperm, ins-e,
orderedls-ls-attachprovedall subs proved orderedls-ls, ols-rec,
ins-less-firstprovedall subs proved ins-n, app-01, cons-02,
sort-possibleprovedall subs proved del1-02, in-04, len, ole-01, le-e,
orderedls-eqprovedall subs proved orderedls-le,
orderedls-allprovedall subs proved orderedls-ls, ls-o, ols-rec, ls-e,
insperm-03provedall subs proved insperm,
ordered-shorter-sublistprovedall subs proved ordered-prefix,
oleprovedall subs proved ole-01,
ordered-prefixprovedall subs proved k-le-r, cons-02, le-e,
orderedls-leprovedall subs proved orderedls-ls, ls-r,
ole-01provedall subs proved cons-02, le-r, ins-y, empty, ole-rec, ins-n, le-o, ins-e, le-e,
app-01provedall subs proved cons-02,
ole-inprovedall subs proved le-r, cons-02,
appprovedall subs proved le-r, le-o, ole-rec, le-e,
inspermprovedall subs proved del1-02, in-04,
ols-recprovedall subs proved ls-r, cons,
del1-01provedall subs proved le-r, le-o, ole-rec, cons-02, le-e,
eqprovedall subs proved ins-rec, ins-y, empty, ins-n, ins-e,
del1-01-02provedall subs proved ole-rec, ins-y, ins-n, cons-02, ins-e,
ordered-postfixprovedall subs proved le-r, k-le-r, le-e, le-o, ole-rec, cons-02,
cons-03provedall subs proved ins-y, le-r, ins-e, cons-02,
one-02provedall subs proved ins-one, ins-one-01,
rest-01provedall subs proved cons-02,
ins-less-lastprovedall subs proved ins-y, ins-n, ins-e, ins-one-01,
sameprovedall subs proved ins-y, ins-y-01,
restprovedall subs proved cons,
k-ls-rprovedall subs proved ls-r, cons, ls-o, ls-e,
ins-one-02provedall subs proved ins-one, ins-y,
ins-y-01provedall subs proved ins-n, ins-y,
ins-one-01provedall subs proved ins-y,
ins-oneprovedall subs proved ins-e, ins-n,
lenprovedall subs proved ins-y, ins-n, ins-e,
in-04provedall subs proved ins-y, ins-n, ins-e,
del1-02provedall subs proved ins-y, ins-n, ins-e,
ole-twoprovedall subs proved le-o, le-r,
emptyprovedall subs proved ins-y, ins-n, ins-e,
ins-recprovedall subs proved ins-n,
consprovedall subs proved ls-r, ls-e, ls-o,
k-le-rprovedall subs proved le-r, le-o, le-e,
orderedls-lsprovedall subs proved ls-r,
cons-02provedall subs proved le-r, le-e, le-o,
ole-recprovedall subs proved le-r,
szle1-orderedlsprovedall subs proved ls-o, ls-e,
in-01-02provedall subs proved ins-y, ins-n, ins-e,
ins-yesprovedall subs proved ins-y,
exprovedall subs proved ins-n, ins-y, ins-e,
szle1-orderedleprovedall subs proved le-o, le-e,
ins-eaxiom
ins-naxiom
ins-yaxiom
ls-eaxiom
ls-oaxiom
ls-raxiom
le-eaxiom
le-oaxiom
le-raxiom