[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

Used from specification nat

nat/eq-02 is used by bmin-size-02,
nat/le-add is used by bmin-size, min-ls,
nat/le-def is used by bmin-size-02, bmin-size, min-ls,
nat/lels is used by bmin-size, min-ls,
nat/ls-02 is used by bmin-size, min-ls,

Used from specification set-union

set-union/del-addeq-03 is used by butmin-ins,
set-union/delsw is used by butmin-ins,
set-union/Delete is used by bmin-nin, bmin-f, min-delmin, bmax-in, bmax-in-02, bmax-in-01, bmin-sub-05, butmin-ins, bmin-nin-01, ls-rm, min-del, bmin-bneq, butmin-in, bmin-intempty, max-del-01, bmin-in-03, bmin-in-01,
set-union/Difference is used by diff-min,
set-union/Intersect is used by min-intempty, bmin-intempty,
set-union/Union is used by maxunion,
set-union/del-addeq-02 is used by bmin-eq, bminmin,
set-union/del-addeq-05 is used by bmax-one, butmin-ins-01, butmin-ins, bmin-one, bmin-bneq,
set-union/del-addeq-06 is used by bmin-two-01,
set-union/del-d is used by bmin-del,
set-union/del-d-01 is used by bmin-del-01,
set-union/del-e-01 is used by bmax-one, bmin-one, bmin-bneq, max-del, min-ls,
set-union/del-e-02 is used by min-delmin-01, bmin-bin, min-delmin, bmax-empty, bmax-shift, bmax-one-01, bmin-bls, bmin-one-01, bmin-one-02, bmin-one-03, bmin-del-04, bmin-del-03, bmin-min, bmin-bneq, minmax, min-del-01, minmax-01, max-del, bm-shift, bmin-in-04,
set-union/del-eq is used by butmin-ins, bmin-eq-01,
set-union/del-in is used by bmin-one-02,
set-union/del-in-03 is used by butmin-ins-01, bmin-two-01,
set-union/del-neq-02 is used by butmin-ins,
set-union/del-size is used by bmin-size-02, bmin-size-01, bmin-size, min-ls,
set-union/delsw-02 is used by bmax-shift, bmin-del-02, bmin-del-01,
set-union/int-a is used by min-intempty, bmin-intempty,
set-union/int-c is used by min-intempty, bmin-intempty,
set-union/one-min is used by bmax-max, one-min, bmin-del-04, bm-shift,
set-union/sub-del-01 is used by bmin-sub-04,
set-union/sub-del-02 is used by min-delmin-01, bmin-bin, min-delmin, bmin-sub-03, max-del,
set-union/sub-del-03 is used by bmin-sub, bmin-in-04,
set-union/sub-del-04 is used by bmin-sub-04,
set-union/una is used by maxunion, min-union,
set-union/unadd is used by min-union,
set-union/unc is used by maxunion, min-union,
set-union/une is used by min-union,
set-union/une-01 is used by min-union,

Used from specification weakord

weakord/tord/irreflexivity is used by max-bmin, ls-add, min-delmin-01, min-sub-01, bmin-bin, size-gtleq, min-intempty, min-two-01, max-subset, min-two-02, is-min, bmax-min, min-delmin, bmax-one, butmin-ins-01, bmin-sub-05, butmin-ins, min-insert, bmin-sub-02, bmin-sub-01, min-q, bmax-shift, maxunion, ls-rm, max-q, bmax-one-01, min-union, min-del, bmin-bls, bmin-one-01, bmin-one-03, size-lsleq, max-one, bmin-one, bmin-del-04, bmin-del-03, bmin-min, min-one, bmin-two-02, bmin-bneq, max-ifins, minmax-02, minmax-03, min-ins-04, min-ins-03, min-ins-02, max-del, min-ins-01, bmin-intempty, max-del-01, bmin-two-01, min-two, bm-shift, bmin-in-04,
weakord/tord/lel is used by size-gtleq, min-union, min-ins-02,
weakord/tord/leq-trans is used by ls-add, min-intempty, min-delmin, bmin-sub-05, bmin-sub-02, bmin-sub-01, ls-rm, min-union, bmin-bls, max-ifins, minmax-03, min-ins-01, bmin-intempty, bmin-in-04,
weakord/tord/ls-le is used by min-rec, butmin-ins,
weakord/tord/nen is used by min-two-02, min-union, bmin-bneq,
weakord/tord/nll is used by max-q, min-union, max-ifins,
weakord/tord/transitivity is used by min-two-01, butmin-ins, min-insert, min-union, bmin-two-02, max-ifins, min-ins-03, min-ins-02, bmin-two-01, min-two,

Used from specification set-basic

set-basic/Extension is used by min-intempty, bmin-intempty,
set-basic/Size-insert is used by min-delmin,
set-basic/Subset is used by bmin-sub-05,
set-basic/size-one-03 is used by min-one-01, max-one-01,
set-basic/size-two is used by size-two,
set-basic/size-two-03 is used by minmax-03,
set-basic/size-two-05 is used by min-two-02,
set-basic/sw is used by min-two-01, bmin-two-02,
set-basic/In-empty is used by min-intempty, min-inn, ls-emptyset, bmin-intempty, bmin-in-03,
set-basic/In-insert is used by ls-add, min-two-02, min-insert, max-ifins, bmin-two, min-ins-02, min-ins-01, min-two,
set-basic/Size-empty is used by min-delmin, bmax-one-01, bmin-one-03, bmin-size, min-ls,
set-basic/eq is used by min-delmin, butmin-ins, min-ins-04,
set-basic/eq-03 is used by butmin-ins, min-ins-05,
set-basic/eq-04 is used by bmin-two-04, bmin-two-08,
set-basic/eqtwo is used by min-two-02,
set-basic/eqtwo-01 is used by min-two-02, bmin-two-04, bmin-two-08,
set-basic/in is used by min-ins-02,
set-basic/in-02 is used by min-two-02,
set-basic/in-03 is used by size-gtleq, size-lsleq,
set-basic/in-04 is used by min-two-02, max-one, min-one, bmin-two, bmin-two-01, min-two,
set-basic/in-06 is used by bmin-bin, min-delmin, bmax-max, bmin-one-01, bmin-one-02, bmin-del-04, bmin-bneq, bm-shift,
set-basic/ne is used by bmin-eq, min-two-02, bmax-one, butmin-ins-01, butmin-ins, min-insert, min-union, bmin-one, bmin-two-07, max-del, bmin-two-01,
set-basic/ne-01 is used by ls-add, min-delmin-01, min-sub-01, bmin-bin, min-intempty, max-subset, min-two-02, is-min, diff-min, bmax-one, butmin-ins-01, bmax-in, bmin-sub-05, butmin-ins, min-insert, ins-inbutmins, bmin-sub-02, bmin-sub-01, min-q, min-less, bmin-in, bmax-shift, max-gr, bmin-eq-01, maxunion, ls-rm, max-q, max-subset-01, bmax-one-01, min-del, bmin-bls, bmin-one-01, bmin-one-02, bmin-one-03, bmin-one, bmin-del-04, bmin-del-03, bmin-min, bmin-bneq, max-ifins, minmax, minmax-02, minmax-01, min-ins-04, min-ins-03, min-sub, min-ins-02, min-ins-01, bmin-intempty, max-del-01, bmin-in-04, bmin-in-01,
set-basic/one-in is used by minmax, minmax-01,
set-basic/one-size is used by bmax-max, bmax-empty, bmin-one-02, bmin-del-04, minmax, minmax-01, bm-shift,
set-basic/size-ins is used by size-gtleq, size-lsleq,
set-basic/size-one-01 is used by bmin-bin, min-union, bmin-one-01, bmin-bneq,
set-basic/size-one-02 is used by minmax, minmax-01,
set-basic/size-two-01 is used by min-two-02,
set-basic/size-zero is used by max-bmin, min-rec, bmax-min, min-delmin, bmax-max, min-union, minmax-03, bmin-intempty, bm-shift,
set-basic/size-zero-01 is used by bmin-eq, max-bmin, ls-add, min-delmin-01, min-sub-01, bmin-bin, min-intempty, min-rec, bmin-size-02, bmin-size-01, max-subset, bminmin, min-two-02, min-inc, is-min, min-inn, bmax-min, min-delmin, diff-min, bmax-one, bmax-max, butmin-ins-01, max-in, bmin-sub-05, butmin-ins, min-insert, bmin-sub-02, bmin-sub-01, bmax-empty, min-q, bmax-shift, max-gr, bmin-eq-01, maxunion, ls-rm, max-q, max-subset-01, bmax-one-01, min-union, min-del, bmin-bls, bmin-one-01, bmin-one-02, bmin-one-03, bmin-one, bmin-del-04, bmin-del-03, bmin-min, bmin-bneq, max-ifins, minmax, minmax-02, minmax-01, minmax-04, minmax-03, min-ins-04, min-ins-03, min-sub, min-ins-02, min-ins-01, bmin-size, min-ls, bmin-intempty, max-del-01, bm-shift, bmin-in-04,
set-basic/size-zero-02 is used by min-union,
set-basic/sub-add is used by bmin-sub-02,
set-basic/sub-add-03 is used by bmin-sub-01,
set-basic/sub-e is used by bmin-sub-02, bmin-sub-01, min-sub,
set-basic/sub-in is used by min-sub-01, max-subset, diff-min, bmin-sub-05, max-subset-01, min-sub, bmin-in-04,
set-basic/two is used by min-two-02,

Used from specification tord

tord/seq is used by min-rec, minmax-03, min-ins-04,
tord/sls is used by min-sub-01, min-two-02, is-min, bmin-sub-05, min-insert, bmin-sub-02, bmin-sub-01, min-q, min-less, max-q, min-union, bmin-two-04, bmin-two-05, bmin-two-07, bmin-two-08, bmin-two, bmin-intempty, bmin-in-01,

Used from specification nat-basic

nat-basic/a is used by size-gtleq, bmin-size-02, size-lsleq, bmin-size, min-ls,
nat-basic/c is used by size-gtleq, bmin-size-02, size-lsleq, bmin-size, min-ls,
nat-basic/less-zero is used by bmin-size,
nat-basic/one is used by max-bmin, bmax-min, min-delmin, bmax-max, bmin-bls, minmax-02, minmax-03, bm-shift,
nat-basic/one-01 is used by bmin-size-02, bmin-size, min-ls,