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