[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 min-ls, bmin-size,
nat/le-def is used by min-ls, bmin-size-02, bmin-size,
nat/lels is used by min-ls, bmin-size,
nat/ls-02 is used by min-ls, bmin-size,

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 min-delmin, min-del, max-del-01, ls-rm, butmin-ins, butmin-in, bmin-sub-05, bmin-nin-01, bmin-nin, bmin-intempty, bmin-in-03, bmin-in-01, bmin-f, bmin-bneq, bmax-in-02, bmax-in-01, bmax-in,
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 bminmin, bmin-eq,
set-union/del-addeq-05 is used by butmin-ins-01, butmin-ins, bmin-one, bmin-bneq, bmax-one,
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 min-ls, max-del, bmin-one, bmin-bneq, bmax-one,
set-union/del-e-02 is used by minmax-01, minmax, min-delmin-01, min-delmin, min-del-01, max-del, bmin-one-03, bmin-one-02, bmin-one-01, bmin-min, bmin-in-04, bmin-del-04, bmin-del-03, bmin-bneq, bmin-bls, bmin-bin, bmax-shift, bmax-one-01, bmax-empty, bm-shift,
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 min-ls, bmin-size-02, bmin-size-01, bmin-size,
set-union/delsw-02 is used by bmin-del-02, bmin-del-01, bmax-shift,
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 one-min, bmin-del-04, bmax-max, bm-shift,
set-union/sub-del-01 is used by bmin-sub-04,
set-union/sub-del-02 is used by min-delmin-01, min-delmin, max-del, bmin-sub-03, bmin-bin,
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 min-union, maxunion,
set-union/unadd is used by min-union,
set-union/unc is used by min-union, maxunion,
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 size-lsleq, size-gtleq, minmax-03, minmax-02, min-union, min-two-02, min-two-01, min-two, min-sub-01, min-q, min-one, min-intempty, min-insert, min-ins-04, min-ins-03, min-ins-02, min-ins-01, min-delmin-01, min-delmin, min-del, maxunion, max-subset, max-q, max-one, max-ifins, max-del-01, max-del, max-bmin, ls-rm, ls-add, is-min, butmin-ins-01, butmin-ins, bmin-two-02, bmin-two-01, bmin-sub-05, bmin-sub-02, bmin-sub-01, bmin-one-03, bmin-one-01, bmin-one, bmin-min, bmin-intempty, bmin-in-04, bmin-del-04, bmin-del-03, bmin-bneq, bmin-bls, bmin-bin, bmax-shift, bmax-one-01, bmax-one, bmax-min, bm-shift,
weakord/tord/lel is used by size-gtleq, min-union, min-ins-02,
weakord/tord/leq-trans is used by minmax-03, min-union, min-intempty, min-ins-01, min-delmin, max-ifins, ls-rm, ls-add, bmin-sub-05, bmin-sub-02, bmin-sub-01, bmin-intempty, bmin-in-04, bmin-bls,
weakord/tord/ls-le is used by min-rec, butmin-ins,
weakord/tord/nen is used by min-union, min-two-02, bmin-bneq,
weakord/tord/nll is used by min-union, max-q, max-ifins,
weakord/tord/transitivity is used by min-union, min-two-01, min-two, min-insert, min-ins-03, min-ins-02, max-ifins, butmin-ins, bmin-two-02, bmin-two-01,

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

Used from specification tord

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

Used from specification nat-basic

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