[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 set-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:
union-size-01provedall subs proved unc, una, union-sizele-01,
union-sizele-01provedall subs proved union-sizele, unadd-01,
union-sizeleprovedall subs proved union-sub, union-size, unc, una, union-sizeeq,
union-sizeeqprovedall subs proved union-sub, unc, una, unrax,
union-size-not-less-02provedall subs proved union-size-not-less-01,
union-size-02provedall subs proved del-in, une-01, Union, del-size, unc, una, undel-03,
union-rem-unchdgprovedall subs proved del-in, undel, unin, del-in-03, unc, una, undel-03,
subset-is-unionprovedall subs proved int-empty, unadd, Intersect, del-e-02, int-del-rew, uninsert, delete-insert, undel-03, Delete, Union, insdel-sub, int-c, int-a, int-e, une-01, unc, una, unsub,
union-subprovedall subs proved unc, una, union-sub-01,
union-size-not-less-01provedall subs proved union-size-le,
undel-03provedall subs proved unc, una, undel-01,
union-subsetprovedall subs proved union-subset-01, unc, una,
union-size-not-lessprovedall subs proved union-size-le,
union-size-ls-inprovedall subs proved Intersect, int-c, int-a, intersection-size, union-size-03,
union-differenceprovedall subs proved Difference, unrax, unc, una, diff-union-01,
union-diff-union-sameprovedall subs proved union-diff, unc, una, unrax, Difference,
union-subset-01provedall subs proved unc, una, unrax,
union-sub-01provedall subs proved unc, una, uneq,
union-sizeprovedall subs proved unc, una, Union,
union-size-leprovedall subs proved uninsert, Union, unadd, unc, una, une,
union-size-03provedall subs proved uninsert, Intersect, intersection-shift, intersection-size, intersection-insert, Union, unadd, int-c, int-a, int-e, unc, una, une,
diff-union-01provedall subs proved Difference, unc, una, unrax,
union-diffprovedall subs proved unc, una, Union, Difference,
undel-01provedall subs proved Delete, unrax, del-in-03, unc, una, undel,
unsubdelprovedall subs proved Delete, unrax, unc, una, undel-04,
union-subset-05provedall subs proved unc, una, unrax,
union-subset-04provedall subs proved unc, una, unrax,
union-subset-03provedall subs proved unc, una, unrax,
union-subset-02provedall subs proved unc, una, unrax,
union-size-insertprovedall subs proved unc, una, Union,
union-rewoneprovedall subs proved unc, una, une, unadd, One,
union-rem-addprovedall subs proved Delete, unrax, unindel, unc, una,
union-oneprovedall subs proved unc, una, une, unadd, One,
union-inter-inter-unionprovedall subs proved int-c, int-a, unc, una, unrax, Intersect,
subset-union-left-remprovedall subs proved unc, una, unsub, unsub-union-01,
sub-union-05provedall subs proved unc, una, Union,
sub-union-04provedall subs proved unc, una, Union,
sub-union-03provedall subs proved unc, una, Union,
sub-union-02provedall subs proved unc, una, Union,
sub-union-01provedall subs proved unc, una, Union,
sub-unionprovedall subs proved unc, una, Union,
size-unionprovedall subs proved Union, unrax, unadd-01, unc, una, une, int-c, int-a, Intersect,
rem-union-insprovedall subs proved del-in, Delete, unrax, unindel, unc, una, uninsert,
k-union-rec2provedall subs proved unc, una, unadd,
k-union-rec1provedall subs proved unc, una, uninsert, unadd,
k-union-baseprovedall subs proved unc, una, une,
intu-emptyprovedall subs proved unc, una, unrax, int-c, int-a, Intersect,
diff-union-03provedall subs proved Difference, unc, una, unrax,
diff-union-02provedall subs proved unin, Difference, unc, una, unrax,
diff-unionprovedall subs proved Difference, unc, una, unrax,
diff-supset-emptyprovedall subs proved unc, una, unrax, Difference,
diff-subsetprovedall subs proved unc, una, Union, Difference,
diff-int-01provedall subs proved unc, una, Union, Difference, int-c, int-a, Intersect,
undel-04provedall subs proved una, Delete, unrax,
uneqprovedall subs proved una, unrax,
intersection-sizeprovedall subs proved Intersect, intersection-insert, intersection-shift, int-c, int-a, int-e,
undelprovedall subs proved una, Delete, unrax,
unsub-union-01provedall subs proved una, unrax,
unsubprovedall subs proved una, unrax,
une-01provedall subs proved una, unrax,
unadd-01provedall subs proved una, unrax,
unaddprovedall subs proved una, unrax,
uneprovedall subs proved una, unrax,
uncprovedall subs proved una, unrax,
unsubsubprovedall subs proved una, unrax,
unsubins-01provedall subs proved una, unrax,
unsubinsprovedall subs proved una, unrax,
unsubdel-01provedall subs proved una, Delete, unrax,
unidemprovedall subs proved una, unrax,
undel-06provedall subs proved una, Delete, unrax,
undel-02provedall subs proved una, unrax, Delete,
unallprovedall subs proved una, unrax,
intersect-empty-remprovedall subs proved int-c, int-a, intdel-empty,
int-empty-oneprovedall subs proved int-e, intersection-insert, int-c, int-a, int-inserte,
empty-intersection-diffprovedall subs proved int-empty-02, int-c, int-a, Difference,
del-three-01provedall subs proved del-size-02,
add-inter-remprovedall subs proved intersection-insert, Delete, del-in, int-c, int-a, Intersect, del-neq,
int-del-rewprovedall subs proved int-c, int-a, Delete, Intersect,
intersection-shiftprovedall subs proved int-c, int-a, Intersect,
intdel-emptyprovedall subs proved Delete, int-c, int-a, Intersect,
int-empty-02provedall subs proved int-c, int-a, Intersect,
unaprovedall subs proved unrax,
del-size-02provedall subs proved Delete, del-in, del-size,
intersection-insertprovedall subs proved int-c, int-a, Intersect,
subseteq-inter-empty-emptyprovedall subs proved int-c, int-a, Intersect,
size-del-leqprovedall subs proved del-in, del-size,
rem-inter-empty3provedall subs proved Difference, int-c, int-a, Intersect,
k-intersect-rec2provedall subs proved del-in, Delete, int-c, int-a, Intersect,
k-intersect-rec1provedall subs proved Delete, int-c, int-a, Intersect,
k-intersect-baseprovedall subs proved int-c, int-a, int-e,
intersect-add-remprovedall subs proved int-c, int-a, Delete, Intersect,
int-subs01provedall subs proved int-c, int-a, Intersect,
int-notempty-01provedall subs proved Delete, int-inserte, int-c, int-a, Intersect,
int-notemptyprovedall subs proved int-inserte, int-c, int-a, Intersect,
int-insprovedall subs proved int-c, int-a, Intersect,
int-empty-01provedall subs proved int-c, int-a, Intersect,
diff-sub-sizeprovedall subs proved del-in, Difference, del-size, diff-add-del, diff-e,
diff-intprovedall subs proved Difference, int-c, int-a, Intersect,
diff-add-del-01provedall subs proved Difference, del-in-03, diff-add-del,
del-threeprovedall subs proved del-in, del-size, Delete,
del-size-01provedall subs proved del-size,
int-emptyprovedall subs proved int-a, Intersect,
uninsertprovedall subs proved unin-01,
int-inserteprovedall subs proved int-a, Intersect,
int-eprovedall subs proved int-a, Intersect,
unraxprovedall subs proved unin-01, unin,
del-in-03provedall subs proved del-in, Delete,
del-sizeprovedall subs proved del-in, del-addeq-05,
int-cprovedall subs proved int-a, Intersect,
undel-05provedall subs proved del-in,
subset-delprovedall subs proved sub-del-04, del-in,
one-minprovedall subs proved del-e-01, del-addeq-05,
k-diff-rec2provedall subs proved diff-del-minus-3, diff-del-minus,
intexinprovedall subs proved int-a, Intersect,
int-inseprovedall subs proved int-a, Intersect,
int-idemprovedall subs proved int-a, Intersect,
int-eqprovedall subs proved int-a, Intersect,
diff-delprovedall subs proved Delete, del-in, diff-del-minus-3, Difference, diff-del-minus,
del-addinprovedall subs proved del-addin-01,
del-addeq-02provedall subs proved Delete, del-addin-01,
unin-01provedall subs proved Union,
insdel-subprovedall subs proved Delete,
delete-insertprovedall subs proved Delete,
del-e-02provedall subs proved Delete,
sub-del-04provedall subs proved Delete,
unindelprovedall subs proved Delete, Union,
del-e-01provedall subs proved Delete,
uninprovedall subs proved Union,
diff-eprovedall subs proved Difference,
diff-del-minusprovedall subs proved Delete, Difference,
diff-del-minus-3provedall subs proved Delete, Difference,
diff-add-delprovedall subs proved Difference, Delete,
del-addeq-05provedall subs proved Delete,
del-addin-01provedall subs proved Delete,
int-aprovedall subs proved Intersect,
del-inprovedall subs proved Delete,
union-delprovedall subs proved Delete, Union,
uninsubdelprovedall subs proved Delete, Union,
subsub-delprovedall subs proved Delete,
subseteq-rem-delprovedall subs proved Delete, Difference,
sub-del-05provedall subs proved Delete,
sub-del-03provedall subs proved Delete,
sub-del-02provedall subs proved Delete,
sub-del-01provedall subs proved Delete,
sub-delprovedall subs proved Delete,
sub-ade-03provedall subs proved Delete,
sub-ade-02provedall subs proved Delete,
sub-ade-01provedall subs proved Delete,
sub-adeprovedall subs proved Delete,
size-eq-extprovedall subs proved size-eq,
selsub-diffprovedall subs proved Difference,
one-inprovedall subs proved One,
k-diff-rec1provedall subs proved Delete, Difference,
k-delete-recprovedall subs proved Delete,
equal-add-inprovedall subs proved Delete,
diff-subset-01provedall subs proved Delete, Difference,
diff-subprovedall subs proved Difference,
diff-rcprovedall subs proved Difference,
diff-oneprovedall subs proved Difference,
diff-ninprovedall subs proved Difference,
diff-idemprovedall subs proved Difference,
diff-emptyprovedall subs proved Difference,
diff-e-01provedall subs proved Difference,
diff-diff-rightprovedall subs proved Difference,
diff-del-plus-2provedall subs proved Difference,
diff-del-plus-1provedall subs proved Difference,
diff-del-minus-2provedall subs proved Delete, Difference,
diff-del-02provedall subs proved Delete, Difference,
diff-del-01provedall subs proved Difference, Delete,
delsw-02provedall subs proved Delete,
delsw-01provedall subs proved Delete,
delswprovedall subs proved Delete,
delete-subsetprovedall subs proved Delete,
delete-shiftprovedall subs proved Delete,
del-twoprovedall subs proved Delete,
del-notinprovedall subs proved Delete,
del-neq-02provedall subs proved Delete,
del-neq-01provedall subs proved Delete,
del-neprovedall subs proved Delete,
del-in-02provedall subs proved Delete,
del-in-01provedall subs proved Delete,
del-feq-02provedall subs proved Delete,
del-feq-01provedall subs proved Delete,
del-feqprovedall subs proved Delete,
del-eqprovedall subs proved Delete,
del-eprovedall subs proved Delete,
del-del-oneprovedall subs proved Delete,
del-d-01provedall subs proved Delete,
del-dprovedall subs proved Delete,
del-addeq-06provedall subs proved Delete,
del-addeq-04provedall subs proved Delete,
del-addeq-03provedall subs proved Delete,
del-addeq-01provedall subs proved Delete,
del-addeqprovedall subs proved Delete,
size-eqprovedall subs proved
Oneaxiom
Unionaxiom
Differenceaxiom
del-neqprovedall subs proved
Intersectaxiom
Deleteaxiom