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