[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-dup

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:
rm-allsizeprovedall subs proved rm-in-01, rm-rm-02, rm-notin-01, rm-in-03, rm-size-02, rm-size, rmdup-n, rmdup-y, rm-empty, rmdup-e,
dups-rmdup-size-equivprovedall subs proved rmdup-n, rm-size-not, rmdup-y, rec, e-01, rmdup-e, rm-eq,
rm-size-notprovedall subs proved rm-size-le,
rm-rm-02provedall subs proved rm-in-05, rm-in-04, rm-in-01, rm-in-03, rmdup-n, rmdup-y, rm-rm,
dups-eqsize-extprovedall subs proved dups-eqsize,
rm-rmprovedall subs proved rm-nodups, rm-eq,
rm-size-leprovedall subs proved rm-size-05,
rm-notin-01provedall subs proved f-01, rm-nodups, rm-in-02,
dups-eqsizeprovedall subs proved dups-lesize,
rm-size-in-01provedall subs proved rm-in, rm-nodups, dups-eqsize-01,
rm-size-03provedall subs proved rm-in-01, rm-in, rm-nodups, dups-lesize, rm-empty,
inapp-01provedall subs proved in-03-01,
dups-firstoc-rewprovedall subs proved app-05, f-01, rec, e-01, in-04-01,
dups-switchprovedall subs proved dups-sw,
dups-eqsize-02provedall subs proved f-01, dups-eqsize-01, d, rec, e-01,
last-01provedall subs proved app-03, one-01,
in-09provedall subs proved in-01-02, f,
rm-size-inprovedall subs proved rm-in-01, rm-in, rm-nodups, dups-eqsize-01,
aaprovedall subs proved sym, app-03, app-02,
rm-size-04provedall subs proved rm-in, rm-nodups, dups-lesize, rm-empty,
lastocprovedall subs proved cons, app-02, first, app-03, cons-01, sym, in, disjoint, first-01,
in-01-02provedall subs proved f-01,
app-03provedall subs proved app-02, sym,
rm-size-05provedall subs proved rmdup-n, rmdup-y, rm-one, rm-empty,
dups-swprovedall subs proved f-01, rec,
in-04-01provedall subs proved f-01,
in-03-01provedall subs proved f-01,
dups-lesizeprovedall subs proved f-01, rec,
dups-eqsize-01provedall subs proved f-01, rec,
rm-nodupsprovedall subs proved rm-in-02, rec, rmdup-n, rmdup-y, e-01, rmdup-e,
nprovedall subs proved f,
in-05-01provedall subs proved f-01,
eqprovedall subs proved rec, f-01,
l-03provedall subs proved f,
cons-04provedall subs proved one-01, app-02, sym,
a-01provedall subs proved f-01,
firstocprovedall subs proved cons, sym, in, e,
two-03provedall subs proved f-01, e-01,
inappprovedall subs proved f-01,
in-02-01provedall subs proved f-01,
in-06-01provedall subs proved f,
in-07provedall subs proved f,
eq-01provedall subs proved rec, f-01,
l-01provedall subs proved f,
rm-emptyprovedall subs proved rmdup-n, rmdup-y, rm-one, rmdup-e,
rm-in-02provedall subs proved rm-in, rmdup-e,
symprovedall subs proved cons-02, first-01, disjoint, cons-01, e, dis-empty,
fprovedall subs proved l, l-02, rec, e-01, c,
f-01provedall subs proved rec, d,
rmdup-lastprovedall subs proved rm-ifrec, rmdup-n, rmdup-y, rm-in-05, rmdup-e, rm-one,
k-dupsprovedall subs proved rec, e-01, dups-rest, dups-in,
rm-notinprovedall subs proved rm-in, rmdup-e,
l-02provedall subs proved app-05,
dprovedall subs proved app-01-02, rec,
dups-inprovedall subs proved c-01,
dups-restprovedall subs proved app-01-02,
rm-inprovedall subs proved rm-in-01, rm-in-03,
cons-01provedall subs proved one-01, app-02, first-01,
cons-02provedall subs proved first, first-01, one-01, app-02, dis-empty,
rm-oneprovedall subs proved c, rm-eq,
rm-size-01provedall subs proved rm-size, rm-size-02, rm-in-05, rm-in-04, rm-ifrec,
rm-rm-01provedall subs proved rm-in-04, rm-in-01, rm-in-03, rmdup-n, rm-in-05, rmdup-y, rmdup-e,
lastprovedall subs proved app-02, one-01,
app-01provedall subs proved app-02,
dups-appexprovedall subs proved in-06, rec, e-01,
aprovedall subs proved rec, e-01, app-01-02,
dups-01provedall subs proved app-01-02, adjoin-notin, rec, adjoin-in,
appprovedall subs proved one-01, app-02, e,
lprovedall subs proved rec,
app-05provedall subs proved rec, e-01,
consprovedall subs proved in, first,
app-01-02provedall subs proved rec,
in-06provedall subs proved rec,
c-01provedall subs proved rec,
app-02provedall subs proved first, in, e,
rm-in-01provedall subs proved rm-ifrec, rmdup-e,
rm-size-02provedall subs proved rm-ifrec, rmdup-y,
rm-sizeprovedall subs proved rm-ifrec, rmdup-n,
rm-eqprovedall subs proved rmdup-n, rec, rmdup-e,
finprovedall subs proved rec,
two-01provedall subs proved rec, c,
one-03provedall subs proved c,
cons-03provedall subs proved in, disjoint,
two-02provedall subs proved rec,
twoprovedall subs proved rec, c,
e-01provedall subs proved dups,
firstprovedall subs proved disjoint,
inprovedall subs proved disjoint,
dis-emptyprovedall subs proved disjoint,
eprovedall subs proved disjoint,
first-01provedall subs proved disjoint,
one-01provedall subs proved disjoint,
rm-in-03provedall subs proved rmdup-n, rmdup-y,
rm-ifrecprovedall subs proved rmdup-n, rmdup-y,
rm-in-04provedall subs proved rmdup-n, rmdup-y,
rm-in-05provedall subs proved rmdup-n, rmdup-y,
recprovedall subs proved dups,
cprovedall subs proved dups,
empty-01provedall subs proved adjoin-notin, adjoin-in,
oneprovedall subs proved disjoint,
in-08provedall subs proved adjoin-notin, adjoin-in,
dupsaxiom
adjoin-inaxiom
adjoin-notinaxiom
rmdup-eaxiom
rmdup-yaxiom
rmdup-naxiom
disjointaxiom