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

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:
inapp-09provedall subs proved a, inapp-11, in-17, in-append, inapp-13, in-15, in-14, inapp-08,
neq-04provedall subs proved a, in-15, inapp-11,
inapp-11provedall subs proved in-17, in-empty, app, inapp-12, lastdiv, a, in-append, in-15,
inexprovedall subs proved app-06, e-02, app, lastdiv, a, in-17, in-append, in-15, in-16,
isin-01provedall subs proved neq-05, app-06, app, lastdiv, inapp-02, inapp-10, in-empty, c-06, Nil, a, in-append, in-15, in-14, in-16,
lastprovedall subs proved a, in-14, in-15, ni, inapp-07, in-empty,
neq-03provedall subs proved neq, app-06, app, lastdiv, a, in-append, in-15, in-16,
neq-06provedall subs proved neq-02, app-06, app, lastdiv, c-06, Nil, a, in-append, in-15, in-14, in-16,
neq-07provedall subs proved in-rec, c-06, inapp-02, in-01, in-14, in-06, c, neq-02, Nil, e-02, app-06, app, lastdiv, a, in-17, in-append, in-15, in-16,
neq-09provedall subs proved a, neq-01,
twoprovedall subs proved e-02, in-16, in-17, e, eq-04, inapp-02, e-01, c, c-05, app-06, a, in-append, in-15, in-14, app-07, app, Nil,
neq-01provedall subs proved in-17, c-06, inapp-02, in-01, in-append, in-14, in-06, c, a, neq-02, Nil,
inapp-07provedall subs proved in-rec, c, c-06, c-03, Nil, a, in-17, in-append, in-15, in-14, ni,
neq-05provedall subs proved a, neq-02, e-02, inapp-04, in-17, in-append, in-14,
in-16provedall subs proved a, app-06, app, in-15, ni,
inapp-12provedall subs proved in-17, e-02, app-06, lastdiv, a, ni, in-append, in-15,
inapp-01provedall subs proved a, inapp-03,
inapp-05provedall subs proved c, inapp-03, in-rec, c-06, Nil, a, inapp-02, in-append, in-14,
inapp-06provedall subs proved in-17, neq, inapp-02, in-append, c, c-06, Nil, neq-02, isin, in-14, a,
inapp-13provedall subs proved e-01, e-02, app-06, c-05, app, lastdiv, inapp-08, c-03, Nil, a, in-17, in-append, in-15, in-14,
neq-02provedall subs proved neq, c, c-06, Nil, a, inapp-02, in-append, in-14,
inapp-03provedall subs proved in-17, c-06, in-01, in-append, in-14, c, in-06, in-empty, inapp-02, Nil, a,
niprovedall subs proved app-06, lastdiv, a, in-append, in-15,
firstoc-rewprovedall subs proved firstoc, a, neq,
inappprovedall subs proved app-01, in-17, c-08, e-01, c-07, first, rest, first-app, e-02, e, app-02, firsteq, inapp-02, in-append, in-14, c, in-06, in-empty, inapp-04, Nil, a,
inapp-14provedall subs proved app-06, neq, lastdiv, a, in-append, in-15, app-03, app,
inex-01provedall subs proved c, in-rec, c-06, Nil, a, inapp-02, in-append, in-14,
lastdiv-rewprovedall subs proved lastdiv, a, e-02,
lastdivprovedall subs proved c-04, Nil, e-02, app-07, app, c, a, e-01,
inapp-04provedall subs proved a, c-06, Nil, isin, in-14, app-07,
inapp-02provedall subs proved in-rec, c, in-empty, c-06, a, in-append, in-14, app-07, Nil,
firstocprovedall subs proved app-08, in-rec, app-07, Nil, c, a, in-17, in-append, in-empty,
app-09provedall subs proved a, e, app-02, app-05, c,
in-last-restprovedall subs proved a, in-17, in-append, rest-01,
not-less-appendprovedall subs proved app-05, less-append, c, e-01, a, Nil,
unequalprovedall subs proved app-07, Nil, len, app-01, app-08, e, c, a, len-05,
firsteqprovedall subs proved c-06, c, a, in-append, in-14, app-03, fr,
rest-01provedall subs proved a, app-03, c-07, c,
app-07provedall subs proved a, c-04, app-03,
app-05provedall subs proved c-05, app-03, c, app, a, Nil,
c-01provedall subs proved a, app-03, c,
c-02provedall subs proved c-06, c, a, in-append, in-14, app-03, fr,
firsteq-01provedall subs proved c, e-01, c-06, a, in-append, in-14, app-03, fr,
inex-03provedall subs proved a, app-03,
app-03provedall subs proved app-06, c, a, app,
eqprovedall subs proved a, app-06, in-15, in-14,
eq-02provedall subs proved a, app-06, in-15, in-14,
eq-03provedall subs proved a, app-06,
k-Inprovedall subs proved in-09, in-empty, in-08, in-07,
last-01provedall subs proved a, in-14, in-15, inapp-08, in-empty,
len-06provedall subs proved a, len, len-01,
len-01provedall subs proved c-06, in-rec, in-append, in-14, c, len-02, len, a, Nil,
in-09provedall subs proved a, in-01, c, e-01, in-empty, in-08,
inapp-10provedall subs proved a, in-17, in-append, in-15, in-14,
inapp-08provedall subs proved in-rec, c, e-01, c-06, a, in-17, in-append, in-15, in-14,
isinprovedall subs proved neq, c-06, c, a, in-append, in-14,
first-appprovedall subs proved c-06, in-empty, in-append, in-14, c, a, Nil, app-02,
app-06provedall subs proved c-06, e-02, c-03, in-14, c, c-05, Nil, a, in-17, in-append, in-15,
append-size-lessprovedall subs proved c-06, in-rec, len-05, e-01, in-append, in-14, c, len-02, len, Nil, a,
eq-01provedall subs proved c, c-06, Nil, a, in-17, in-append, in-14,
first-02provedall subs proved c-06, Nil, c-03, in-15, e-02, in-17, in-append, in-14, c, a, e-03,
in-append0-not-leftprovedall subs proved in-06, c, e-01, c-06, a, in-append, in-14, in-empty,
lastoc-rewprovedall subs proved lastoc, a, neq,
lasttwoprovedall subs proved a, in-append, in-13, lastoc,
len-03provedall subs proved len-02, len, in-rec, c, in-empty, c-06, Nil, a, in-append, in-14,
len-04provedall subs proved c, len-05, len, in-empty, c-06, Nil, a, in-rec, in-append, in-14,
len-last-restprovedall subs proved len-02, len, in-17, in-append, in-14, in-15, c, a, e-02,
lastocprovedall subs proved app-08, Nil, in-append, in-13, c, a, in-rec, in-empty,
in-07provedall subs proved a, in-06, c, e-01,
in-08provedall subs proved a, in-06, c, e-01, in-empty,
in-01provedall subs proved a, in-06, in-10,
in-14provedall subs proved a, in-06,
inprovedall subs proved a, in-06,
in-defprovedall subs proved in-13, app-01, Nil, in-rec, in-empty, a, neq, c,
eq-04provedall subs proved e-02, e-01, c, c-05, c-04, a, app, Nil,
in-13provedall subs proved a, in-17, in-append,
in-10provedall subs proved a, in-17, in-append,
in-06provedall subs proved a, in-17, in-append,
neqprovedall subs proved a, in-17, in-append,
in-15provedall subs proved a, in-17, in-append,
if-inprovedall subs proved a, in-17, in-append,
some-elementprovedall subs proved a, in-17, in-append, c, e-01, in-empty,
split-restprovedall subs proved a, len, split-first,
split-firstprovedall subs proved c, len-02, len, a, Nil,
e-03provedall subs proved a, e-01, app-02,
in-17provedall subs proved in-empty, a, app, in-rec,
e-02provedall subs proved a, e, app-02,
c-05provedall subs proved e, app-02, c-03, c, c-04, a, Nil,
app-04provedall subs proved app-01, c, Nil, a, app,
constrrewprovedall subs proved c-04, a, app, c,
e-04provedall subs proved a, len,
firstrestprovedall subs proved c, a, e, app-02,
in-11provedall subs proved a, in-append,
in-12provedall subs proved a, in-append,
inex-02provedall subs proved a, app-08,
oneprovedall subs proved c-03, c, in-rec, app-02, in-empty, a, Nil,
one-01provedall subs proved app-02, c-03, c, a, Nil, c-04,
oneinprovedall subs proved in-empty, in-rec, c-03, e-01, e, a, app, c,
app-08provedall subs proved a, app-01,
lenprovedall subs proved len-05, c, a, Nil,
app-02provedall subs proved e-01, c, a, Nil,
in-appendprovedall subs proved in-rec, c, a, Nil, in-empty,
appprovedall subs proved app-01, c, a, Nil,
Noassocprovedall subs proved a,
c-09provedall subs proved a, fr,
elim-firstprovedall subs proved fr, a, e-01,
eq-05provedall subs proved a, c-06,
first-01provedall subs proved a, c-08, c,
insprovedall subs proved a,
ins-01provedall subs proved a,
k-Last-baseprovedall subs proved c-04, a, Nil, Last,
k-Last-recprovedall subs proved a, app-01, c, Last,
k-Twoprovedall subs proved a, app-01, c, Two,
longest-common-prefixprovedall subs proved c-08, e-01, app-01, c, a, Nil,
rewlemprovedall subs proved a,
less-appendprovedall subs proved c,
len-05provedall subs proved c,
aprovedall subs proved Cons, app-01, Nil,
restprovedall subs proved One,
firstprovedall subs proved One,
c-07provedall subs proved Nil, Cons, One,
c-08provedall subs proved Nil, Cons, One,
frprovedall subs proved Nil, Cons, One,
len-02provedall subs proved One,
eprovedall subs proved One,
c-04provedall subs proved One,
c-03provedall subs proved Nil, Cons, One,
c-06provedall subs proved Nil, Cons, One,
e-01provedall subs proved Nil, Cons, One,
cprovedall subs proved Nil, Cons, One,
app-01provedall subs proved Cons, Nil,
Twoaxiom
Lastaxiom
in-emptyaxiom
Oneaxiom
in-recaxiom
Nilaxiom
Consaxiom