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