[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 ext, unrax, Delete, unc, una, 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,
int-empty-oneprovedall subs proved int-c, int-a, ext, int-e, int-ins, int-inserte,
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,
uninsertprovedall subs proved unin-01,
int-insprovedall subs proved int-c, int-a, Intersect,
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,
k-intersect-rec2provedall subs proved int-c, int-a, Intersect, Delete, ext,
unsubsubprovedall subs proved una, unrax,
undel-02provedall subs proved una, unrax, Delete,
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,
unsubinsprovedall subs proved una, unrax,
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,
unallprovedall subs proved una, unrax,
unsubins-01provedall subs proved una, unrax,
unsubprovedall subs proved una, unrax,
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,
unsubdel-01provedall subs proved una, Delete, unrax,
unadd-01provedall subs proved una, unrax,
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,
rem-inter-empty3provedall subs proved Difference, int-c, int-a, Intersect, ext,
undel-06provedall subs proved una, Delete, unrax,
unsub-union-01provedall subs proved una, unrax,
unidemprovedall subs proved una, unrax,
intersection-insertprovedall subs proved int-c, int-a, Intersect, ext,
une-01provedall subs proved una, unrax,
intersection-shiftprovedall subs proved int-c, int-a, Intersect, ext,
add-inter-remprovedall subs proved int-c, int-a, Intersect, Delete, ext,
unin-01provedall subs proved unrax,
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,
uninprovedall subs proved unrax,
int-inserteprovedall subs proved int-a, Intersect,
unindelprovedall subs proved Delete, unrax,
unaprovedall subs proved unrax,
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,
uninsubdelprovedall subs proved Delete, unrax,
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,
diff-del-minusprovedall subs proved Delete, Difference, ext,
diff-add-delprovedall subs proved Difference, Delete,
del-addin-01provedall subs proved Delete,
del-inprovedall subs proved Delete,
unraxprovedall subs proved Union,
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,
Unionaxiom
Oneaxiom
extprovedall subs proved
Intersectaxiom
Deleteaxiom
Differenceaxiom