[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-ls-attach, ordls-append, ordered-append-second, ordered-append,
ordls-appendprovedall subs proved ls-e, ordered-append,
ordered-attachprovedall subs proved ls-o, ordered-append,
ordered-append-secondprovedall subs proved ls-e, ordered-append,
ordered-appendprovedall 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,
ordered-last2provedall subs proved ols-two, ordered-append-split2,
ole-last-01provedall subs proved ole-last,
ordered-last1provedall subs proved ordered-append-split2,
ordered-nodupprovedall subs proved orderedls-le, ordered-append-split2,
orderedle-twolastprovedall subs proved app, ole-last,
ole-lastprovedall subs proved le-o, le-r, ole-in, ole-rec, app-02, app, app-01, cons-02, ole-two,
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,
orderedle-allprovedall subs proved orderedle-ls, cons-02, le-o, ole-rec, le-e,
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,
insperm-01provedall subs proved insperm,
orderedls-ls-attachprovedall subs proved orderedls-ls, ols-rec,
app-02provedall subs proved app-01, cons-02, app,
orderedCombined-Two-Listsprovedall subs proved ols-rec, ls-r, ls-o, cons,
ols-twoprovedall subs proved ls-o, ols-rec,
orderedls-le-attachprovedall subs proved orderedls-ls, ols-rec,
orderedle-lsprovedall subs proved cons-02, ole-in,
orderedle-appendprovedall subs proved k-le-r, app, le-r, le-o, cons-02, le-e,
ordered-append-firstprovedall subs proved ls-r, ls-o, ols-rec, ls-e,
orderedls-eqprovedall subs proved orderedls-le,
ordered-shorter-sublistprovedall subs proved ordered-prefix,
del1provedall subs proved orderedls-ls, ls-o, ols-rec, cons, ls-e,
oleprovedall subs proved ole-01,
orderedls-allprovedall subs proved orderedls-ls, ls-o, ols-rec, ls-e,
ins-less-firstprovedall subs proved ins-n, app-01, cons-02,
sort-possibleprovedall subs proved del1-02, in-04, len, ole-01, le-e,
insperm-03provedall subs proved insperm,
insperm-02provedall subs proved ins-y, ins-n, insperm, ins-e,
ordered-postfixprovedall subs proved le-r, k-le-r, le-e, le-o, ole-rec, app-01, cons-02,
inspermprovedall subs proved del1-02, in-04,
ole-inprovedall subs proved le-r, cons-02,
ole-01provedall subs proved cons-02, le-r, ins-y, empty, ole-rec, ins-n, le-o, ins-e, le-e,
ordered-prefixprovedall subs proved k-le-r, cons-02, le-e,
ols-recprovedall subs proved ls-r, cons,
orderedls-leprovedall subs proved orderedls-ls, ls-r,
app-01provedall subs proved cons-02,
appprovedall subs proved le-r, le-o, ole-rec, le-e,
del1-01-02provedall subs proved ole-rec, ins-y, ins-n, cons-02, ins-e,
k-ls-rprovedall subs proved ls-r, cons, ls-o, ls-e,
cons-03provedall subs proved ins-y, le-r, ins-e, cons-02,
eqprovedall subs proved ins-rec, ins-y, empty, ins-n, ins-e,
ins-one-02provedall subs proved ins-one, ins-y,
sameprovedall subs proved ins-y, ins-y-01,
restprovedall subs proved cons,
one-02provedall subs proved ins-one, ins-one-01,
ins-less-lastprovedall subs proved ins-y, ins-n, ins-e, ins-one-01,
rest-01provedall subs proved cons-02,
del1-01provedall subs proved le-r, le-o, ole-rec, cons-02, le-e,
ins-one-01provedall subs proved ins-y,
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,
ins-y-01provedall subs proved ins-n, ins-y,
ole-twoprovedall subs proved le-o, le-r,
ins-oneprovedall subs proved ins-e, ins-n,
emptyprovedall subs proved ins-y, ins-n, ins-e,
ins-recprovedall subs proved ins-n,
k-le-rprovedall subs proved le-r, le-o, le-e,
orderedls-lsprovedall subs proved ls-r,
consprovedall subs proved ls-r, ls-e, ls-o,
cons-02provedall subs proved le-r, le-e, le-o,
ole-recprovedall subs proved le-r,
ins-yesprovedall subs proved ins-y,
szle1-orderedlsprovedall subs proved ls-o, ls-e,
szle1-orderedleprovedall subs proved le-o, le-e,
exprovedall subs proved ins-n, ins-y, ins-e,
in-01-02provedall subs proved ins-y, ins-n, ins-e,
ls-raxiom
ls-eaxiom
ls-oaxiom
le-eaxiom
le-oaxiom
le-raxiom
ins-eaxiom
ins-naxiom
ins-yaxiom