[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,
Used simplifier rules/spec theorems by specification
- infset-union/ext
is used by
ext,
- infset-union/ext
is used by
del-in-03,
int-inse,
del-feq,
del-neq-02,
int-c,
del-e-02,
une-01,
subsub-del,
unidem,
int-idem,
del,
del-feq-01,
unc,
sub-ade,
diff-del,
unsub-union-01,
union-rewone,
del-d-01,
sub-union,
del-addeq-01,
one-min,
diff-e-01,
sub-union-01,
delete-insert,
indef,
del-in,
undel-06,
del-addeq-04,
insdel-sub,
diff-empty,
sub-ade-02,
sub-del-03,
una,
del-del-one,
int-empty-01,
delsw-01,
diff-add-del,
diff-idem,
uneq,
union-sub,
diff-int-01,
unadd-01,
diff-rc,
unsubdel-01,
del-d,
del-feq-02,
int-inserte,
int-del-rew,
int-a,
delsw,
int-ins,
delsw-02,
diff-e,
int-eq,
undel-01,
unall,
del-addeq-02,
int-notempty-01,
del-neq-01,
intdel-empty,
intu-empty,
del-addeq-05,
del-two,
undel-04,
sub-del-04,
une,
del-e-01,
del-addeq,
sub-ade-03,
union-sub-01,
int-empty-02,
int-empty,
sub-del-01,
del-eq,
intexin,
union-difference,
sub-del,
int-e,
del-e,
diff-int,
int-notempty,
unadd,
undel-05,
selsub-diff,
undel-02,
undel,
unsubsub,
diff-union-03,
sub-ade-01,
- infset-basic/Subset
is used by
unsubdel,
- infset-basic/In-empty
is used by
diff-supset-empty,
int-inse,
del-feq,
del-e-02,
une-01,
subsub-del,
sub-ade,
diff-del,
unsub-union-01,
sub-union,
diff-e-01,
sub-union-01,
subset-is-union,
rem-inter-empty3,
insdel-sub,
diff-empty,
sub-ade-02,
unsubdel,
sub-del-03,
int-empty-01,
diff-idem,
uneq,
diff-int-01,
int-inserte,
int-ins,
diff-e,
int-eq,
unall,
empty-intersection-diff,
int-notempty-01,
intersect-empty-rem,
inter-empty-diff,
del-neq-01,
subseteq-inter-empty-empty,
intdel-empty,
intu-empty,
del-two,
sub-del-04,
une,
del-e-01,
del-addeq,
sub-ade-03,
union-sub-01,
int-empty-02,
int-empty,
sub-del-01,
del-eq,
intexin,
union-difference,
sub-del,
int-e,
union-sub-rem-inter-empty,
del-e,
diff-int,
int-notempty,
selsub-diff,
unsubsub,
sub-ade-01,
- infset-basic/In-insert
is used by
sub-union-03,
subseteq-rem-del,
k-delete-rec,
int-inse,
del-feq,
del-neq-02,
diff-del-02,
intersection-shift,
intersection-insert,
del-feq-01,
sub-ade,
union-subset-05,
del-addin,
union-subset-02,
del-addeq-01,
sub-union-01,
delete-insert,
indef,
del-addeq-04,
equal-add-in,
insdel-sub,
sub-ade-02,
sub-union-04,
intersect-add-rem,
diff-add-del,
delsw-suc,
unadd-01,
diff-del-plus-1,
rem-union-ins,
del-feq-02,
int-inserte,
delsw,
int-ins,
k-intersect-rec1,
unsubins-01,
del-addeq-02,
delete-shift,
int-notempty-01,
sub-union-02,
del-addin-01,
del-neq-01,
unsubins,
del-addeq-05,
del-two,
del-addeq,
union-one,
sub-ade-03,
int-empty,
union-subset-04,
sub-union-05,
diff-del-plus-2,
add-rem-sub,
diff-one,
del-e,
int-notempty,
unadd,
del-addeq-06,
delete-subset,
union-rem-add,
sub-ade-01,
diff-subset-01,
- infset-basic/Subset
is used by
sub-union-03,
subseteq-rem-del,
diff-del-02,
sub-del-05,
subsub-del,
diff-subset,
subset-union-left-rem,
sub-del-02,
sub-ade,
union-subset-05,
unsub-union-01,
union-subset-02,
subset-del,
sub-union,
sub-union-01,
union-subset,
subset-is-union,
insdel-sub,
sub-ade-02,
sub-del-03,
sub-union-04,
uneq,
int-subs01,
int-eq,
unsub,
unsubins-01,
union-subset-03,
sub-union-02,
inter-empty-diff,
unsubins,
subseteq-inter-empty-empty,
diff-del-01,
sub-del-04,
sub-ade-03,
union-sub-01,
union-subset-04,
sub-del-01,
sub-union-05,
union-difference,
sub-del,
diff-sub,
union-subset-01,
diff-one,
union-sub-rem-inter-empty,
selsub-diff,
delete-subset,
unsubsub,
sub-ade-01,
diff-subset-01,
- infset-basic/eq
is used by
del,
indef,
diff-del-plus-1,
diff-del-plus-2,
- infset-basic/eq-03
is used by
uninsert,
del-addeq-03,
- infset-basic/in
is used by
intersection-insert,
diff-del-plus-1,
diff-del-plus-2,
- infset-basic/in-02
is used by
add-inter-rem,
intersect-add-rem,
diff-del-plus-2,
add-rem-sub,
del-e,
- infset-basic/in-03
is used by
diff-del-plus-2,
- infset-basic/in-04
is used by
del-e-02,
del-del-one,
one-in,
del-two,
diff-one,
- infset-basic/ne-01
is used by
int-inse,
ext,
del-feq,
del-e-02,
une-01,
subsub-del,
sub-ade,
diff-del,
unsub-union-01,
sub-union,
sub-union-01,
insdel-sub,
diff-empty,
sub-ade-02,
uninsubdel,
unsubdel,
sub-del-03,
int-empty-01,
uneq,
unsubdel-01,
int-inserte,
int-ins,
int-eq,
unall,
int-notempty-01,
intdel-empty,
intu-empty,
del-two,
sub-del-04,
del-addeq,
sub-ade-03,
union-sub-01,
int-empty-02,
int-empty,
sub-del-01,
del-eq,
intexin,
union-difference,
sub-del,
del-e,
int-notempty,
selsub-diff,
unsubsub,
sub-ade-01,
- infset-basic/sub-in
is used by
uninsubdel,
unsubdel,
unsubdel-01,