[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 bag-union

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:
subset-exdiffprovedall subs proved union-diff-cancel, union-diff-distr, union-com, union-ass, union, count-subset,
union-diff-distrprovedall subs proved count-subset, union-com, union-ass, union, difference, count-diff-subset,
union-diff-cancelprovedall subs proved union-com, union-ass, union, difference,
union-subset-injprovedall subs proved union-com, union-ass, union, count-subset,
subset-smallerprovedall subs proved count-subset, subset-plus,
in-unionprovedall subs proved union-com, union-ass, union, in,
union-sizeprovedall subs proved size-rec, union-rec, size-empty, union-com, union-ass, union-empty,
union-subsetprovedall subs proved union-com, union-ass, union, count-subset,
subset-sizeprovedall subs proved size-rec, subset-plus, size-empty, count-subset,
diff-sizeprovedall subs proved size-rec, del-rec, count-subset, subset-plus, diff-rec, size-empty, diff-empty,
union-injprovedall subs proved union-com, union-ass, union,
count-diff-subsetprovedall subs proved count-subset, difference,
subset-plusprovedall subs proved subset-in, in, exin, subset-plusplus,
union-comprovedall subs proved union-ass, union,
in-diff-notfirstprovedall subs proved in, difference,
del-sizeprovedall subs proved del-notin, size-rec, del-rec, exin, in,
diff-add-swprovedall subs proved difference, in,
diff-swapprovedall subs proved difference,
still-in-diffprovedall subs proved difference, in,
difference-notinprovedall subs proved in, difference,
exinprovedall subs proved count-del, in,
differenceprovedall subs proved count-del, del-notin, diff-rec, diff-empty,
union-assprovedall subs proved union,
still-in-remprovedall subs proved count-del, in,
subset-empty-sizeprovedall subs proved size-empty, subset-emp,
in-atprovedall subs proved in, in-add,
subset-antisymprovedall subs proved count-subset, subset-refl, subset-trans,
someprovedall subs proved in, in-emp,
bag-rm-add-eqprovedall subs proved in, count-del,
subset-plusminusprovedall subs proved count-del, count-subset,
in-oneprovedall subs proved in-emp, in-add, one,
in-rem-notremprovedall subs proved count-del, in,
subset-plusplusprovedall subs proved count-subset,
subset-inprovedall subs proved count-subset,
in-empprovedall subs proved in,
del-notinprovedall subs proved del-rec, del-empty,
subset-transprovedall subs proved count-subset,
subset-reflprovedall subs proved count-subset,
in-addprovedall subs proved in,
subset-empprovedall subs proved count-subset,
count-delprovedall subs proved del-rec, del-empty,
unionprovedall subs proved union-rec, union-empty,
subset-oneprovedall subs proved in, count-subset,
filter-countprovedall subs proved filter-add, filter-empty,
exists-defprovedall subs proved exists-rec, exists-base, in,
count-oneprovedall subs proved one,
forall-defprovedall subs proved forall-rec, forall-base, in,
diff-empty1provedall subs proved del-empty, diff-rec, diff-empty,
subset-elemprovedall subs proved in, count-subset,
del-recaxiom
del-emptyaxiom
diff-emptyaxiom
diff-recaxiom
forall-baseaxiom
forall-recaxiom
union-emptyaxiom
union-recaxiom
size-recaxiom
oneaxiom
exists-baseaxiom
exists-recaxiom
filter-emptyaxiom
filter-addaxiom
size-emptyaxiom
inaxiom
count-subsetaxiom