[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/add-01 is used by union-diff-distr, del-size, count-del,
nat/anti is used by difference,
nat/cancel-01 is used by diff-size, difference,
nat/elim-pred-c is used by difference, still-in-rem,
nat/elim-sub is used by diff-add-sw, diff-swap, difference,
nat/eq-01 is used by union-diff-cancel,
nat/eq-02 is used by diff-add-sw, exin, bag-rm-add-eq,
nat/eqle-one is used by difference,
nat/fle is used by union-diff-distr, diff-swap, difference,
nat/fle-01 is used by subset-smaller, diff-swap, subset-trans, difference,
nat/le-def is used by union-diff-distr, subset-plusminus, diff-add-sw, exin, subset-smaller, diff-swap, bag-rm-add-eq, subset-trans, subset-one, subset-plusplus, difference,
nat/le-ls-simp is used by union-diff-distr, subset-plusminus, subset-antisym, diff-add-sw, subset-smaller, diff-swap, subset-trans, subset-plusplus,
nat/le-one is used by difference,
nat/lels is used by subset-plusminus, subset-size, difference,
nat/lels-02 is used by differente-notin, subset-antisym, in-diff-notfirst, diff-swap,
nat/lels-03 is used by difference,
nat/lep is used by union-subset, diff-add-sw, diff-swap, union-diff-cancel, difference,
nat/lep-02 is used by union-subset-inj, subset-plusplus, difference,
nat/leprf is used by difference,
nat/ler is used by subset-refl, difference,
nat/les is used by difference,
nat/let is used by difference,
nat/lez is used by subset-size, diff-add-sw, diff-swap,
nat/lez-01 is used by subset-elem, subset-empty-size, subset-emp,
nat/ls is used by difference,
nat/ls-01 is used by diff-swap,
nat/ls-02 is used by subset-plusminus, diff-swap, difference,
nat/ls-le-simp is used by subset-plusminus, subset-size, diff-swap, subset-plusplus,
nat/not-zero is used by subset-one,
nat/sub-base is used by subset-plusminus, diff-size, exin, diff-swap, bag-rm-add-eq, del-size, count-del, in-rem-notrem, difference, still-in-rem,
nat/succ-01 is used by subset-in, subset-plusminus, subset-size, subset-smaller, difference,
nat/zero is used by difference,
nat/zero-02 is used by differente-notin, in-diff-notfirst, diff-swap, difference,

Used from specification bag-basic

bag-basic/count-insert is used by diff-add-sw, bag-rm-add-eq,
bag-basic/count-other is used by union, subset-plusminus, diff-add-sw, exin, subset-smaller, count-one, count-del, subset-one, subset-plusplus, difference,
bag-basic/extension is used by subset-antisym, diff-add-sw, exin, diff-swap, bag-rm-add-eq, some,
bag-basic/count-1 is used by in-one, count-one, subset-one,
bag-basic/count-empty is used by union, in-emp, in-one, subset-empty-size, count-one, subset-emp, some, del-notin, count-del, subset-one, difference,
bag-basic/count-other is used by union, subset-plusminus, in-one, diff-add-sw, in-add, del-notin, count-del, subset-plusplus,
bag-basic/count-same is used by subset-in, union, subset-plusminus, diff-add-sw, exin, subset-smaller, subset-empty-size, bag-rm-add-eq, in-add, del-notin, count-del, subset-plusplus, difference,
bag-basic/extension is used by union-diff-distr, union-inj, union-diff-cancel, union-ass, union-com,

Used from specification nat-basic

nat-basic/a is used by union-diff-distr, subset-in, union, subset-plusminus, union-size, diff-size, subset-size, union-subset, diff-add-sw, exin, subset-smaller, union-inj, diff-swap, in-union, union-subset-inj, union-diff-cancel, subset-empty-size, union-ass, bag-rm-add-eq, union-com, in-add, del-size, del-notin, count-del, subset-plusplus, difference, still-in-rem,
nat-basic/add-base is used by diff-add-sw, bag-rm-add-eq,
nat-basic/c is used by union-diff-distr, subset-in, union, subset-plusminus, union-size, diff-size, subset-size, union-subset, diff-add-sw, exin, subset-smaller, union-inj, diff-swap, in-union, union-subset-inj, union-diff-cancel, subset-empty-size, union-ass, bag-rm-add-eq, union-com, in-add, del-size, del-notin, count-del, subset-plusplus, difference, still-in-rem,
nat-basic/eq-01 is used by union-diff-distr, union, union-size, union-inj, union-ass, union-com, count-del, difference,
nat-basic/eq-02 is used by bag-rm-add-eq,
nat-basic/eqs is used by diff-add-sw, diff-swap,
nat-basic/f is used by union-diff-distr, subset-in, subset-plusminus, subset-antisym, subset-size, diff-add-sw, subset-smaller, in-diff-notfirst, diff-swap, subset-trans, subset-one, subset-plusplus, difference,
nat-basic/l is used by diff-swap, subset-plusplus,
nat-basic/l-01 is used by difference,
nat-basic/l-02 is used by union-diff-distr, diff-add-sw, diff-swap, difference,
nat-basic/l-05 is used by diff-swap,
nat-basic/l-07 is used by diff-swap,
nat-basic/less-zero is used by diff-swap, subset-one,
nat-basic/lf is used by diff-swap,
nat-basic/lf-01 is used by difference,
nat-basic/lf-02 is used by diff-add-sw, diff-swap, difference,
nat-basic/ls-02 is used by subset-smaller,
nat-basic/one-01 is used by subset-plusminus, exin, bag-rm-add-eq, subset-one, difference,
nat-basic/oz is used by subset-empty-size, in-add, del-notin, count-del, difference, still-in-rem,
nat-basic/refl-nat is used by difference,
nat-basic/s-04 is used by subset-plusminus, difference,
nat-basic/succ is used by diff-swap,
nat-basic/trans-nat is used by diff-swap,
nat-basic/z-01 is used by diff-swap, in-union, difference,
nat-basic/z-02 is used by union-diff-distr, union, union-size, del-size, count-del,
nat-basic/zero is used by differente-notin, diff-swap, difference,