[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:
unsubdel-01provedall subs proved ext, unc, una, union-sub, undel-03,
union-delprovedall subs proved unrax, undel, del-rax, unc, una, undel-03,
undel-03provedall subs proved unc, una, undel-01,
union-subprovedall subs proved ext, unc, una, union-sub-01,
undel-01provedall subs proved Delete, del-rax, ext, unrax, del-in-03, unc, una, undel,
union-rewoneprovedall subs proved ext, unc, una, une, unadd, One,
union-oneprovedall subs proved unc, una, une, unadd, One,
union-sub-01provedall subs proved ext, unc, una, subdef, uneq,
uneprovedall subs proved unc, una, uneq,
undelprovedall subs proved del-rax, unrax, unindel, unc, una, ext,
union-differenceprovedall subs proved subdef, Difference, unrax, unc, una, diff-union-01, ext,
unidemprovedall subs proved unc, una, subdef, uneq,
int-notempty-01provedall subs proved int-inserte, del-rax, int-ins, int-c, int-a, int-rax, ext,
int-notemptyprovedall subs proved int-inserte, int-ins, int-c, int-a, int-rax, ext,
unaddprovedall subs proved ext, unc, una, unadd-01,
diff-union-01provedall subs proved Difference, unrax, unc, una, unin,
uneqprovedall subs proved subdef, unrax, unc, una, unin, ext,
unindelprovedall subs proved unin-01, unc, una, del-rax, unrax,
int-inserteprovedall subs proved int-c, int-a, int-rax, ext, int-ins,
unsubdelprovedall subs proved ext, del-rax, unrax, unc, una, undel-04, subdef,
uninsertprovedall subs proved unc, una, unin-01,
undel-02provedall subs proved ext, unc, una, undel-04,
unallprovedall subs proved unin, unc, una, unrax, ext,
int-inseprovedall subs proved int-c, int-a, int-ins,
int-idemprovedall subs proved int-c, int-a, subdef, int-eq,
int-emptyprovedall subs proved int-ins, int-c, int-a, int-rax, ext,
int-eprovedall subs proved int-c, int-a, int-eq,
diff-union-02provedall subs proved unin, Difference, unc, una, unrax,
diff-unionprovedall subs proved Difference, unrax, unc, una, unin,
unin-01provedall subs proved unc, una, unrax,
undel-04provedall subs proved Delete, unc, una, del-rax, unrax, ext,
unadd-01provedall subs proved unc, una, unrax, ext,
int-insprovedall subs proved int-c, int-a, int-rax, ext,
int-eqprovedall subs proved Intersect, subdef, int-c, int-a, int-rax, ext,
uninprovedall subs proved unc, una, unrax,
unsubsubprovedall subs proved ext, unc, una, unrax, subdef,
unsubins-01provedall subs proved unc, una, unrax, subdef,
unsubinsprovedall subs proved unc, una, unrax, subdef,
unsub-union-01provedall subs proved ext, unc, una, unrax, subdef,
unsubprovedall subs proved unc, una, unrax, subdef,
union-diffprovedall subs proved unc, una, unrax, Difference,
une-01provedall subs proved unc, una, unrax, ext,
undel-06provedall subs proved unc, una, del-rax, unrax, ext,
sub-union-05provedall subs proved unc, una, unrax, subdef,
sub-union-04provedall subs proved unc, una, unrax, subdef,
sub-union-03provedall subs proved unc, una, unrax, subdef,
sub-union-02provedall subs proved unc, una, unrax, subdef,
sub-union-01provedall subs proved ext, unc, una, unrax, subdef,
sub-unionprovedall subs proved ext, unc, una, unrax, subdef,
one-minprovedall subs proved ext, del-e-01, del-addeq-05,
intu-emptyprovedall subs proved unc, una, unrax, int-c, int-a, int-rax,
intexinprovedall subs proved int-c, int-a, int-rax, ext,
intdel-emptyprovedall subs proved del-rax, int-c, int-a, int-rax, ext,
int-subs01provedall subs proved int-c, int-a, int-rax, subdef,
int-empty-02provedall subs proved int-c, int-a, int-rax, ext,
int-empty-01provedall subs proved int-c, int-a, int-rax, ext,
int-del-rewprovedall subs proved Delete, Intersect, int-c, int-a, del-rax, int-rax, ext,
indefprovedall subs proved del-rax, ext, del-addeq-02,
diff-union-03provedall subs proved Difference, unc, una, unrax, ext,
diff-subsetprovedall subs proved unc, una, unrax, Difference, subdef,
diff-int-01provedall subs proved unc, una, unrax, Difference, int-c, int-a, int-rax, ext,
diff-intprovedall subs proved Difference, int-c, int-a, int-rax, ext,
diff-add-del-01provedall subs proved Difference, del-in-03, diff-add-del,
del-del-oneprovedall subs proved del-in-03,
del-dprovedall subs proved del-rax, del-in-03,
delprovedall subs proved del-rax, ext, del-addeq-02,
del-e-01provedall subs proved del-e-02,
uncprovedall subs proved una, unrax, ext,
int-cprovedall subs proved Intersect, int-a, int-rax, ext,
del-in-03provedall subs proved del-in, del-rax, ext,
del-addeq-02provedall subs proved ext, delete-insert,
undel-05provedall subs proved ext, del-in,
subset-delprovedall subs proved del-in, del-rax, subdef,
sub-del-01provedall subs proved sub-del-04, subdef,
delsw-01provedall subs proved delsw-02,
del-addinprovedall subs proved del-addin-01,
del-addeq-04provedall subs proved ext, del-in, del-addeq-05,
del-addeq-03provedall subs proved del-in-01,
sub-del-04provedall subs proved ext, del-rax, subdef,
unaprovedall subs proved unrax, ext,
int-aprovedall subs proved Intersect, int-rax, ext,
diff-add-delprovedall subs proved Difference, del-rax, ext,
delsw-02provedall subs proved Delete, del-rax, ext,
del-e-02provedall subs proved del-rax, ext,
del-addin-01provedall subs proved del-rax,
del-addeq-05provedall subs proved Delete, del-rax, ext,
del-inprovedall subs proved Delete, del-rax, ext,
del-in-01provedall subs proved del-rax, Delete,
delete-insertprovedall subs proved Delete, del-rax, ext,
uninsubdelprovedall subs proved del-rax, Union,
subsub-delprovedall subs proved ext, del-rax, subdef,
sub-del-05provedall subs proved Delete, del-rax, subdef,
sub-del-03provedall subs proved ext, del-rax, subdef,
sub-del-02provedall subs proved del-rax, subdef,
sub-delprovedall subs proved ext, Delete, del-rax, subdef,
sub-ade-03provedall subs proved ext, del-rax, subdef,
sub-ade-02provedall subs proved ext, del-rax, subdef,
sub-ade-01provedall subs proved ext, del-rax, subdef,
sub-adeprovedall subs proved ext, del-rax, subdef,
selsub-diffprovedall subs proved Difference, subdef, ext,
insdel-subprovedall subs proved ext, del-rax, subdef,
equal-add-inprovedall subs proved del-rax, ext,
diff-subset-01provedall subs proved Difference, del-rax, subdef,
diff-subprovedall subs proved Difference, subdef,
diff-oneprovedall subs proved Difference, subdef,
diff-del-02provedall subs proved Difference, Delete, subdef,
diff-del-01provedall subs proved Difference, Delete, subdef,
diff-delprovedall subs proved del-rax, Delete, Difference, ext,
delswprovedall subs proved Delete, del-rax, ext,
delete-subsetprovedall subs proved del-rax, subdef,
del-twoprovedall subs proved del-rax, ext,
del-neq-02provedall subs proved del-rax, ext,
del-neq-01provedall subs proved del-rax, ext,
del-feq-02provedall subs proved del-rax, ext,
del-feq-01provedall subs proved del-rax, ext,
del-feqprovedall subs proved del-rax, ext,
del-eqprovedall subs proved del-rax, ext,
del-eprovedall subs proved del-rax, ext,
del-d-01provedall subs proved Delete, del-rax, ext,
del-addeq-06provedall subs proved Delete, del-rax, ext,
del-addeq-01provedall subs proved Delete, del-rax, ext,
del-addeqprovedall subs proved del-rax, ext,
unraxprovedall subs proved Union,
int-raxprovedall subs proved Intersect,
subdefprovedall subs proved ext,
del-raxprovedall subs proved Delete,
one-inprovedall subs proved One,
diff-rcprovedall subs proved Difference, ext,
diff-ninprovedall subs proved Difference,
diff-idemprovedall subs proved Difference, ext,
diff-emptyprovedall subs proved Difference, ext,
diff-e-01provedall subs proved Difference, ext,
diff-eprovedall subs proved Difference, ext,
del-notinprovedall subs proved Delete,
del-in-02provedall subs proved Delete,
Unionaxiom
Oneaxiom
Intersectaxiom
Differenceaxiom
Deleteaxiom
extprovedall subs proved