[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,
app-02provedall subs proved app-01, cons-02, app,
ole-last-01provedall subs proved ole-last,
ordered-ex-divide-lelsprovedall subs proved orderedle-ls, app-01, cons-02, le-e,
ordered-ex-divide-lsleprovedall subs proved orderedle-ls, app-01, cons-02, le-e,
ordered-ordered-subset-orderedprovedall subs proved ordered-sublist2,
ordered-shorter-sublistprovedall subs proved ordered-prefix,
orderedle-allprovedall subs proved orderedle-ls, app-01, cons-02, le-o, ole-rec, le-e,
ordered-prefixprovedall subs proved k-le-r, app-01, cons-02, le-e,
ordered-sublist2provedall subs proved orderedls-le, ordered-append-split2, ordered-append-first, ordered-append-second, ordered-append,
ole-lastprovedall subs proved le-o, le-r, ole-in, ole-rec, app-01, cons-02, ole-two,
ole-01provedall subs proved app-01, cons-02, le-r, ins-y, empty, ole-rec, ins-n, le-o, ins-e, le-e,
del1-01provedall subs proved le-r, le-o, ole-rec, app-01, cons-02, le-e,
orderedle-lsprovedall subs proved cons-02, ole-in,
appprovedall subs proved le-r, le-o, ole-rec, le-e,
del1-01-02provedall subs proved ole-rec, ins-y, eq, ins-n, app-01, cons-02, ins-e,
ins-less-firstprovedall subs proved cons-03, ins-y, ins-n, app-01, cons-02,
ins2provedall subs proved sw,
ordered-cant-contain-same-element-twiceprovedall subs proved orderedls-le, ordered-append-split1,
ordered-last2provedall subs proved ordered-attach,
ordered-last3provedall subs proved orderedls-le-attach, ordered-append-split2,
ordered-postfixprovedall subs proved le-r, k-le-r, le-e, le-o, ole-rec, app-01, cons-02,
ordered-sublistprovedall subs proved ordered-append-first, ordered-append-split2,
ordered-two-same-elements-not-orderedprovedall subs proved orderedls-eq-attach,
orderedle-appendprovedall subs proved k-le-r, le-r, le-o, app-01, cons-02, le-e,
perm-insprovedall subs proved del1-02, in-04, insperm-01,
insperm-01provedall subs proved insperm,
orderedls-eq-attachprovedall subs proved orderedls-le-attach,
ordered-append-secondprovedall subs proved ls-e, ordered-append,
ordered-append-firstprovedall subs proved ls-e, ordered-append,
k-le-rprovedall subs proved le-r, app-01, le-o, le-e,
ordered-append-split2provedall subs proved ordered-append,
ordered-attachprovedall subs proved ls-o, ordered-append,
ordered-append-split1provedall subs proved ls-r, ls-o, cons, ordered-append,
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,
del1provedall subs proved orderedls-ls, ls-o, ols-rec, cons, ls-e,
insperm-02provedall subs proved ins-y, ins-n, insperm, ins-e,
insperm-03provedall subs proved insperm,
one-02provedall subs proved ins-one-02, ins-one-01,
ordered-last1provedall subs proved ls-r, ordered-append,
orderedCombined-Two-Listsprovedall subs proved ordered-append,
orderedls-allprovedall subs proved orderedls-ls, ls-o, ols-rec, ls-e,
orderedls-eqprovedall subs proved orderedls-le,
orderedls-ls-attachprovedall subs proved orderedls-le-attach,
rest-01provedall subs proved app-01,
orderedls-le-attachprovedall subs proved ls-r, ols-two,
orderedls-leprovedall subs proved orderedls-ls, ls-r,
ordered-appendprovedall subs proved ls-r, ls-o, cons,
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,
ins-less-lastprovedall subs proved ins-y, ins-n, ins-e, ins-one-01,
k-ls-rprovedall subs proved ls-r, cons, ls-o, ls-e,
restprovedall subs proved cons,
sameprovedall subs proved ins-y, ins-y-01,
lenprovedall subs proved ins-y, ins-n, ins-e,
ins-y-01provedall subs proved ins-n, ins-y,
ols-twoprovedall subs proved ls-o, ls-r,
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,
cons-02provedall subs proved le-r, le-e, le-o,
exprovedall subs proved ins-n, ins-y, ins-e,
in-01-02provedall subs proved ins-y, ins-n, ins-e,
ins-yesprovedall subs proved ins-y,
szle1-orderedleprovedall subs proved le-o, le-e,
szle1-orderedlsprovedall subs proved ls-o, ls-e,
ins-naxiom
ins-eaxiom
ins-yaxiom
ls-oaxiom
ls-eaxiom
ls-raxiom
le-eaxiom
le-oaxiom
le-raxiom