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