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