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