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