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