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