[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-basic

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

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, bmin-size-02,
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-del, bmax-in, bmin-bneq, butmin-ins, bmin-intempty, butmin-in, bmin-in-01, min-delmin, ls-rm, bmin-f, bmax-in-01, bmax-in-02, bmin-nin-01, bmin-nin, bmin-sub-05, bmin-in-03, max-del-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 bmin-bneq, butmin-ins, butmin-ins-01, bmax-one, bmin-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 bmin-bneq, min-ls, bmax-one, max-del, bmin-one,
set-union/del-e-02 is used by bmin-one-02, bmax-shift, bmin-del-03, bmin-bneq, bmax-one-01, bmin-in-04, min-delmin, min-del-01, bmin-one-03, bmin-min, minmax-01, bmax-empty, bmin-bls, bmin-del-04, min-delmin-01, bm-shift, bmin-one-01, bmin-bin, minmax, max-del,
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 bmin-two-01, butmin-ins-01,
set-union/del-neq-02 is used by butmin-ins,
set-union/del-size is used by min-ls, bmin-size-01, bmin-size, bmin-size-02,
set-union/delsw-02 is used by bmin-del-02, bmax-shift, 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 one-min, bmin-del-04, bm-shift, bmax-max,
set-union/sub-del-01 is used by bmin-sub-04,
set-union/sub-del-02 is used by bmin-sub-03, min-delmin, min-delmin-01, bmin-bin, max-del,
set-union/sub-del-03 is used by bmin-in-04, bmin-sub,
set-union/sub-del-04 is used by bmin-sub-04,
set-union/una is used by maxunion,
set-union/unc is used by maxunion,

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

Used from specification oelem

oelem/irreflexivity is used by min-del, min-intempty, min-insert, min-q, min-two-01, bmax-shift, bmin-del-03, bmin-bneq, max-ifins, minmax-03, min-ins-03, bmax-one-01, butmin-ins, bmin-in-04, min-sub-01, bmin-intempty, max-subset, min-delmin, ls-rm, bmax-min, is-min, bmin-one-03, max-one, bmin-two-01, bmin-min, max-q, bmin-bls, min-two-02, bmin-del-04, min-delmin-01, ls-add, min-ins-04, size-gtleq, bmin-sub-01, bm-shift, min-ins-01, bmin-one-01, size-lsleq, maxunion, min-one, bmin-bin, butmin-ins-01, min-ins-02, bmin-two-02, minmax-02, bmax-one, bmin-sub-05, max-bmin, max-del-01, max-del, min-two, bmin-one, bmin-sub-02,
oelem/lel is used by size-gtleq, min-ins-02,
oelem/ls-le is used by butmin-ins,
oelem/nen is used by bmin-bneq, min-two-02,
oelem/nll is used by max-ifins, max-q,
oelem/nnn is used by min-intempty, max-ifins, minmax-03, bmin-in-04, bmin-intempty, min-delmin, ls-rm, bmin-bls, ls-add, bmin-sub-01, min-ins-01, bmin-sub-05, bmin-sub-02,
oelem/seq is used by minmax-03, min-ins-04,
oelem/sls is used by min-insert, min-q, min-sub-01, bmin-intempty, bmin-in-01, is-min, bmin-two-04, bmin-two, max-q, min-two-02, bmin-two-07, bmin-sub-01, bmin-two-08, min-less, bmin-two-05, bmin-sub-05, bmin-sub-02,
oelem/transitivity is used by min-insert, min-two-01, max-ifins, min-ins-03, butmin-ins, bmin-two-01, min-ins-02, bmin-two-02, min-two,

Used from specification oset

oset/size-two is used by size-two,