[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 unrax, undel, Delete, unc, una, undel-03,
undel-03provedall subs proved unc, una, undel-01,
union-subprovedall subs proved unc, una, union-sub-01,
union-differenceprovedall subs proved Difference, unrax, unc, una, diff-union-01,
union-sub-01provedall subs proved unc, una, uneq,
diff-union-01provedall subs proved Difference, unc, una, unrax,
undel-01provedall subs proved Delete, unrax, del-in-03, unc, una, undel,
unsubdelprovedall subs proved Delete, unrax, unc, una, undel-04,
union-rewoneprovedall subs proved unc, una, une, unadd, One,
union-oneprovedall subs proved unc, una, une, unadd, One,
union-diffprovedall subs proved unc, una, Union, Difference,
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,
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 Difference, unc, una, unrax,
diff-unionprovedall subs proved Difference, unc, una, unrax,
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,
unaddprovedall subs proved una, unrax,
uneprovedall subs proved una, unrax,
undelprovedall subs proved una, Delete, 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,
unsub-union-01provedall subs proved una, unrax,
unsubprovedall subs proved una, unrax,
unidemprovedall subs proved una, unrax,
une-01provedall subs proved una, unrax,
undel-06provedall subs proved una, Delete, unrax,
undel-02provedall subs proved una, unrax, Delete,
unallprovedall subs proved una, unrax,
unadd-01provedall subs proved una, unrax,
unaprovedall subs proved unrax,
intdel-emptyprovedall subs proved Delete, int-c, int-a, 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-02provedall subs proved int-c, int-a, Intersect,
int-empty-01provedall subs proved int-c, int-a, Intersect,
int-del-rewprovedall subs proved int-c, int-a, Delete, Intersect,
diff-intprovedall subs proved Difference, int-c, int-a, Intersect,
diff-add-del-01provedall subs proved Difference, del-in-03, diff-add-del,
int-inserteprovedall subs proved int-a, Intersect,
unraxprovedall subs proved unin-01, unin,
int-cprovedall subs proved int-a, Intersect,
del-in-03provedall subs proved del-in, Delete,
uninsertprovedall subs proved unin-01,
undel-05provedall subs proved del-in,
subset-delprovedall subs proved del-in, Delete,
one-minprovedall subs proved del-e-01, del-addeq-05,
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,
int-emptyprovedall subs proved int-a, Intersect,
int-eprovedall subs proved int-a, Intersect,
indefprovedall subs proved Delete, delete-insert,
del-addinprovedall subs proved del-addin-01,
del-addeq-02provedall subs proved Delete, del-addin-01,
delprovedall subs proved Delete, delete-insert,
uninprovedall subs proved Union,
unin-01provedall subs proved Union,
del-addeq-05provedall subs proved Delete,
del-e-01provedall subs proved Delete,
int-aprovedall subs proved Intersect,
diff-add-delprovedall subs proved Difference, Delete,
del-inprovedall subs proved Delete,
del-addin-01provedall subs proved Delete,
delete-insertprovedall subs proved Delete,
uninsubdelprovedall subs proved Delete, Union,
unindelprovedall subs proved Delete, Union,
subsub-delprovedall subs proved Delete,
sub-del-05provedall subs proved Delete,
sub-del-04provedall 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,
selsub-diffprovedall subs proved Difference,
one-inprovedall subs proved One,
insdel-subprovedall subs proved Delete,
equal-add-inprovedall subs proved Delete, ext,
diff-subset-01provedall subs proved Difference, Delete,
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-eprovedall subs proved Difference,
diff-del-02provedall subs proved Delete, Difference,
diff-del-01provedall subs proved Difference, Delete,
diff-delprovedall subs proved Delete, Difference,
delsw-02provedall subs proved Delete,
delsw-01provedall subs proved Delete,
delswprovedall subs proved Delete,
delete-subsetprovedall 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-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-e-02provedall 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, ext,
del-addeq-04provedall subs proved Delete,
del-addeq-03provedall subs proved Delete,
del-addeq-01provedall subs proved Delete,
del-addeqprovedall subs proved Delete,
Oneaxiom
Unionaxiom
Intersectaxiom
Differenceaxiom
extprovedall subs proved
Deleteaxiom