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