[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,
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-04provedall subs proved a, in-15, inapp-11,
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,
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-11provedall subs proved in-17, in-empty, app, inapp-12, lastdiv, a, in-append, in-15,
inapp-01provedall subs proved a, inapp-03,
inapp-05provedall subs proved c, inapp-03, in-rec, c-06, Nil, a,
neq-05provedall subs proved a, neq-02, e-02, inapp-04, in-17, in-append, in-14,
inapp-12provedall subs proved a, in-append, e-02, app-06, lastdiv,
inapp-13provedall subs proved in-17, in-append, e-01, e-02, app-06, c-05, app, lastdiv, a, c-03, Nil,
inapp-03provedall subs proved c-06, 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, app-03, app,
inexprovedall subs proved a, app-06, e-02, app, lastdiv,
lastdiv-rewprovedall subs proved lastdiv, a, e-02,
neq-03provedall subs proved a, neq, app-06, app, lastdiv,
neq-06provedall subs proved neq-02, app-06, app, lastdiv, a, c-06, Nil,
neq-07provedall subs proved c-06, in-06, c, neq-02, Nil, a, e-02, app-06, app, lastdiv,
lastdivprovedall subs proved c-04, Nil, e-02, app-07, app, c, a, e-01,
inapp-04provedall subs proved a, c-06, Nil, isin, app-07,
inapp-02provedall subs proved in-rec, c, in-empty, c-06, a, 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,
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,
neq-09provedall subs proved a, neq-01,
not-less-appendprovedall subs proved app-05, less-append, c, e, app-02, a, Nil,
neq-01provedall subs proved c-06, in-06, c, a, neq-02, Nil,
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,
firsteqprovedall subs proved c-06, c, a, 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,
append-size-lessprovedall subs proved c-06, in-rec, len-05, e-01, in-append, in-14, c, len-02, len, Nil, a,
c-01provedall subs proved a, app-03, c,
c-02provedall subs proved c-06, c, a, app-03, fr,
firsteq-01provedall subs proved e-01, c, c-06, a, app-03, fr,
inapp-06provedall subs proved neq, c, c-06, Nil, neq-02, isin, a,
inex-03provedall subs proved a, app-03,
lastoc-rewprovedall subs proved lastoc, a, neq,
lasttwoprovedall subs proved a, in-append, in-13, lastoc,
len-04provedall subs proved c, len-02, 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,
neq-02provedall subs proved neq, c, a, c-06, Nil,
isinprovedall subs proved a, neq, c-06, c,
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,
app-03provedall subs proved app-06, c, a, app,
eqprovedall subs proved a, app-06,
eq-02provedall subs proved a, app-06,
eq-03provedall subs proved a, app-06,
inprovedall subs proved a, in-06,
in-append0-not-leftprovedall subs proved a, in-06, c, e-01, c-06, in-empty,
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-15provedall 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,
app-06provedall subs proved c-06, e-02, c-03, c, a, c-05, Nil,
first-02provedall subs proved c-03, Nil, c-06, e-02, c, a, e-03,
if-inprovedall subs proved a, in-17, in-append,
map-int-appendprovedall subs proved map-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,
map-appendprovedall subs proved app-08, c, map-rec, a, Nil, map-base,
first-appprovedall subs proved c-06, in-empty, c, a, Nil, app-02,
in-17provedall subs proved in-empty, a, app, in-rec,
e-03provedall subs proved a, e-01, app-02,
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,
len-03provedall subs proved len, c, a, c-06, Nil,
map-emptyprovedall subs proved a, e, app-02, c, map-rec, map-base,
map-oneprovedall subs proved a, app, c, map-base, map-rec,
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,
unequalprovedall subs proved c-06, Nil, len, app-01, app-08, e, c, a, len-05,
app-08provedall subs proved a, app-01,
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,
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-01provedall subs proved c, a, c-06, Nil,
eq-05provedall subs proved a, c-06,
first-01provedall subs proved a, c-08, c,
inex-01provedall subs proved c, a, c-06, Nil,
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,
map-inprovedall subs proved a, in-rec, c, map-rec, in-empty, map-base,
map-sizeprovedall subs proved a, len-05, c, map-rec, map-base,
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,
map-baseaxiom
map-recaxiom
Twoaxiom
Lastaxiom
in-emptyaxiom
Oneaxiom
in-recaxiom
Nilaxiom
Consaxiom