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

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:
eqdefprovedall subs proved del1-01-01, del1-01, app-01, cons-02,
sort-possibleprovedall subs proved del1-02, in-04, len, ole, le-e,
oleprovedall subs proved ole-01,
del1-01-01provedall subs proved orderedle-ls, le-r, app-01, del1-01, cons-02,
ole-last-01provedall subs proved ole-last,
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,
ordered-shorter-sublistprovedall subs proved ordered-prefix,
app-02provedall subs proved app-01, cons-02, app,
orderedle-allprovedall subs proved orderedle-ls, app-01, cons-02, le-o, ole-rec, le-e,
ole-01provedall subs proved app-01, cons-02, le-r, ins-y, empty, ole-rec, ins-n, le-o, ins-e, le-e,
appprovedall subs proved le-r, le-o, ole-rec, le-e,
ordered-prefixprovedall subs proved k-le-r, app-01, cons-02, le-e,
orderedle-lsprovedall subs proved cons-02, ole-in,
del1-01provedall subs proved le-r, le-o, ole-rec, app-01, cons-02, le-e,
ole-lastprovedall subs proved le-o, le-r, ole-in, ole-rec, app-01, cons-02, ole-two,
ordered-appendprovedall subs proved k-le-r, le-r, le-o, app-01, cons-02, le-e,
ins-less-firstprovedall subs proved cons-03, ins-y, ins-n, app-01, cons-02,
del1-01-02provedall subs proved ole-rec, ins-y, eq, ins-n, app-01, cons-02, ins-e,
ordered-postfixprovedall subs proved le-r, k-le-r, le-e, le-o, ole-rec, app-01, cons-02,
ins2provedall subs proved sw,
perm-insprovedall subs proved del1-02, in-04, insperm-01,
insperm-01provedall subs proved insperm,
swprovedall subs proved ins-y-01, ins-y, ins-n, ins-one-02, ins-one-01, ins-one, ins-e,
cons-03provedall subs proved ins-y, le-r, ins-e, app-01, cons-02,
ole-inprovedall subs proved le-r, app-01, cons-02,
k-le-rprovedall subs proved le-r, app-01, le-o, le-e,
ole-recprovedall subs proved le-r, app-01,
del1provedall subs proved orderedls-ls, ls-o, ols-rec, cons, ls-e,
insperm-02provedall subs proved ins-y, ins-n, insperm, ins-e,
one-02provedall subs proved ins-one-02, ins-one-01,
orderedls-allprovedall subs proved orderedls-ls, ls-o, ols-rec, ls-e,
insperm-03provedall subs proved insperm,
rest-01provedall subs proved app-01,
eqprovedall subs proved in-04, ins-rec, ins-y, empty, ins-n, ins-e,
inspermprovedall subs proved del1-02, in-04,
ins-one-02provedall subs proved ins-one, ins-y,
ols-recprovedall subs proved ls-r, cons,
app-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,
lenprovedall 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,
ins-oneprovedall subs proved ins-e, ins-n,
ins-one-01provedall subs proved ins-y,
ins-y-01provedall subs proved ins-n, ins-y,
emptyprovedall subs proved ins-y, ins-n, ins-e,
ins-recprovedall subs proved ins-n,
in-04provedall subs proved ins-y, ins-n, ins-e,
consprovedall subs proved ls-r, ls-e, ls-o,
orderedls-lsprovedall subs proved ls-r,
cons-02provedall subs proved le-r, le-e, le-o,
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,
ls-raxiom
ins-eaxiom
ins-naxiom
ins-yaxiom
ls-eaxiom
ls-oaxiom
le-eaxiom
le-oaxiom
le-raxiom