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

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/delsw-01 is used by bmin-del-04,
set-union/subdef is used by bmin-sub-05,
set-union/Delete is used by min-del, max-del-01, butmin-ins, butmin-in, bmin-sub-05, bmin-nin-01, bmin-nin, bmin-in-03, bmin-f, bmax-in-02, bmax-in-01, bmax-in,
set-union/Difference is used by diff-min,
set-union/del-addeq-05 is used by butmin-ins-01, butmin-ins, bmin-one, 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, bmax-one,
set-union/del-e-02 is used by minmax-01, minmax, min-delmin-01, min-delmin, min-del-01, max-del, butminempty-sizeone, 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-01 is used by bmin-in-01,
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-rax is used by min-delmin, min-del, max-del-01, ls-rm, bmin-sub-05, bmin-in-03, bmin-bneq, bmax-in,
set-union/del-size is used by bmin-size-02, bmin-size-01,
set-union/delete-insert is used by bminmin, bmin-eq,
set-union/delsw-02 is used by bmin-del-02, 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/int-empty-02 is used by min-intempty,
set-union/intersect-empty-rem is used by bmin-intempty,
set-union/one-min is used by one-min, min-delmin, bmin-del-04, bmin-bneq, bmin-bin, bmax-max, bm-shift,
set-union/size-del-leq is used by min-ls,
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 maxunion,
set-union/unc is used by maxunion,
set-union/unin-01 is used by maxunion,

Used from specification set-basic

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-ins, min-inn, ls-emptyset, emptyset-ls, bmin-in-03,
set-basic/Size-empty is used by min-ls, bmin-size, bmin-one-03, bmax-one-01,
set-basic/add is used by min-insert, bmin-two,
set-basic/eq is used by min-ins-04, butmin-ins-01, 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-01 is used by min-two-02, bmin-two-08, bmin-two-04,
set-basic/in is used by min-ins-02, min-ins-01, max-ifins,
set-basic/in-02 is used by min-two-02, min-insert,
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-del-04, bmin-bneq, bmin-bin, bmax-max, bm-shift,
set-basic/ne is used by 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, 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, 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, bmin-min, bmin-in-04, bmin-in-01, bmin-in, bmin-eq-01, bmin-del-04, bmin-bneq, bmin-bls, bmin-bin, bmax-one-01, bmax-one, bmax-in,
set-basic/one-in is used by minmax-01,
set-basic/one-size is used by minmax-01, minmax, min-delmin, butminempty-sizeone, bmin-one-02, bmin-one-01, bmin-del-04, bmin-bneq, bmin-bin, bmax-max, bmax-empty, bm-shift,
set-basic/rax is used by min-two-02, min-two, min-ins-02, min-ins-01, max-ifins, ls-add,
set-basic/size-one-02 is used by minmax-01,
set-basic/size-two-01 is used by min-two-02,
set-basic/size-zero is used by minmax-03, min-delmin, max-bmin, bmax-min, bmax-max, bm-shift,
set-basic/size-zero-01 is used by minmax-04, minmax-03, minmax-02, minmax-01, minmax, min-two-02, min-sub-01, min-sub, min-q, min-intempty, min-insert, min-ins-04, min-ins-03, min-ins-02, min-ins-01, min-inn, 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, diff-min, butminempty-sizeone, butmin-ins-01, butmin-ins, bmin-sub-05, bmin-sub-02, bmin-sub-01, bmin-size-02, bmin-size-01, bmin-one-03, bmin-one-02, bmin-one-01, bmin-one, bmin-min, bmin-in-04, bmin-eq-01, bmin-del-04, bmin-bneq, bmin-bls, bmin-bin, bmax-one-01, bmax-one, bmax-min, bmax-max, bmax-empty, bm-shift,
set-basic/sub-add-03 is used by bmin-sub-02, bmin-sub-01,
set-basic/sub-e is used by min-sub,
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/sub-one-02 is used by bmin-sub-02, bmin-sub-01,
set-basic/two is used by min-two-02,

Used from specification nat-basic2

nat-basic2/a is used by bmin-size-02,
nat-basic2/c is used by bmin-size-02,

Used from specification oelem

oelem/irreflexivity is used by minmax-03, minmax-02, min-two-02, min-two-01, min-two, min-sub-01, min-q, min-one, 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, 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, bmin-min, bmin-in-04, bmin-del-04, bmin-bneq, bmin-bls, bmin-bin, bmax-one-01, bmax-one, bmax-min, bm-shift,
oelem/lel is used by minmax-02, max-ifins, butmin-ins,
oelem/ls-le is used by min-two-02, min-two, butmin-ins,
oelem/nen is used by min-ins-04, min-delmin, bmin-sub-05,
oelem/nll is used by max-q, max-ifins,
oelem/nnn is used by minmax-03, min-ins-01, ls-rm, ls-add, bmin-sub-05, bmin-sub-02, bmin-sub-01, bmin-in-04,
oelem/seq is used by minmax-03, min-ins-04,
oelem/sls is used by min-two-02, min-sub-01, min-q, min-less, min-insert, max-q, bmin-two-08, bmin-two-07, bmin-two-05, bmin-two-04, bmin-two, bmin-sub-05, bmin-sub-02, bmin-sub-01, bmin-one-02, bmin-in-01,
oelem/transitivity is used by 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 nat-basic1

nat-basic1/one is used by minmax-03, min-delmin, max-bmin, bmax-min, bmax-max, bm-shift,
nat-basic1/one-01 is used by bmin-size-02,
nat-basic1/one-02 is used by minmax-03, minmax-02, bmin-bls,
nat-basic1/zero-01 is used by bmin-size,

Used from specification oset

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