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

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

Used from specification nat-basic2

• nat-basic2/a is used by union-subset-inj, union-subset, union-size, union-inj, union-diff-distr, union-diff-cancel, union-com, union-ass, union, subset-smaller, subset-size, subset-plusplus, subset-plusminus, subset-in, in-union, in-add, exin, difference, diff-size, diff-add-sw, del-size, count-del, bag-rm-add-eq,
• nat-basic2/add-base is used by union-size, union, diff-add-sw, del-size, count-del, bag-rm-add-eq,
• nat-basic2/c is used by union-subset-inj, union-subset, union-size, union-inj, union-diff-distr, union-diff-cancel, union-com, union-ass, union, subset-smaller, subset-size, subset-plusplus, subset-plusminus, subset-in, in-union, in-add, exin, difference, diff-size, diff-add-sw, del-size, count-del, bag-rm-add-eq,
• nat-basic2/eq-01 is used by union-size, union-inj, union-diff-distr, union-com, union-ass, union, count-del, bag-rm-add-eq,
• nat-basic2/eqs is used by union-diff-distr, diff-add-sw,
• nat-basic2/l is used by subset-plusplus, difference,
• nat-basic2/l-02 is used by union-diff-distr, subset-smaller, diff-add-sw,
• nat-basic2/oz is used by subset-plusplus, subset-plusminus, del-size, count-del,
• nat-basic2/s is used by subset-plusminus,
• nat-basic2/z-01 is used by in-union, in-add,

Used from specification nat-basic1

• nat-basic1/f is used by union-subset-inj, union-diff-distr, subset-trans, subset-smaller, subset-size, subset-plusplus, subset-plusminus, subset-one, subset-in, subset-antisym, still-in-diff, in-diff-notfirst, difference, diff-add-sw,
• nat-basic1/lf-01 is used by subset-in, still-in-diff, in-diff-notfirst, difference,
• nat-basic1/lf-02 is used by diff-add-sw,
• nat-basic1/ls-02 is used by diff-add-sw,
• nat-basic1/one-01 is used by subset-plusminus, subset-one, exin, difference, bag-rm-add-eq,
• nat-basic1/ref-1 is used by subset-smaller,
• nat-basic1/zero is used by differente-notin, difference,
• nat-basic1/zero-01 is used by subset-one, bag-rm-add-eq,