[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 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, subset-exdiff, in-union, in-add, exin, difference, diff-swap, diff-size, diff-add-sw, del-size, del-notin, count-del, bag-rm-add-eq,
nat-basic/add-base is used by union-size, union-diff-distr, union, diff-add-sw, del-size, count-del, bag-rm-add-eq,
nat-basic/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, subset-exdiff, in-union, in-add, exin, difference, diff-swap, diff-size, diff-add-sw, del-size, del-notin, count-del, bag-rm-add-eq,
nat-basic/eq-01 is used by union-size, union-inj, union-com, union-ass, union, count-del, bag-rm-add-eq,
nat-basic/eqs is used by diff-swap, diff-add-sw,
nat-basic/f is used by 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-swap, diff-add-sw,
nat-basic/l is used by subset-plusplus, diff-swap,
nat-basic/l-02 is used by union-diff-distr, subset-smaller, diff-swap, diff-add-sw,
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 subset-one, difference, diff-swap, bag-rm-add-eq,
nat-basic/lf is used by diff-swap,
nat-basic/lf-01 is used by difference,
nat-basic/lf-02 is used by diff-swap, diff-add-sw,
nat-basic/ls-02 is used by diff-add-sw,
nat-basic/one-01 is used by subset-plusminus, subset-one, exin, difference, bag-rm-add-eq,
nat-basic/oz is used by difference, del-size, count-del,
nat-basic/s-04 is used by subset-plusminus,
nat-basic/succ is used by diff-swap,
nat-basic/trans-Nat is used by diff-swap,
nat-basic/z-01 is used by in-union, in-add, diff-swap, del-notin,
nat-basic/zero is used by difference-notin, diff-swap,

Used from specification nat

nat/add-01 is used by del-size, count-del,
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-swap, 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, diff-swap,
nat/fle-01 is used by subset-trans, diff-swap,
nat/le-def is used by union-diff-distr, subset-trans, subset-smaller, subset-plusplus, subset-plusminus, subset-one, exin, difference, diff-swap, diff-add-sw, bag-rm-add-eq,
nat/le-ls-simp is used by union-diff-distr, subset-plusminus, diff-swap,
nat/lels is used by subset-size, subset-plusminus,
nat/lels-02 is used by subset-antisym, still-in-diff, in-diff-notfirst, difference-notin, diff-swap, diff-add-sw,
nat/lep is used by union-subset, union-diff-distr, union-diff-cancel, subset-exdiff, diff-swap, 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, difference, diff-swap, diff-add-sw,
nat/lez-01 is used by subset-emp, subset-elem, difference,
nat/ls-01 is used by subset-plusminus, diff-swap,
nat/ls-02 is used by subset-plusminus, difference, diff-swap,
nat/ls-le-simp is used by subset-trans, subset-smaller, subset-size, subset-plusplus, subset-plusminus, subset-antisym, diff-swap,
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-swap, diff-size, diff-add-sw, del-size, count-del, bag-rm-add-eq,
nat/succ-01 is used by subset-size, subset-plusminus, subset-in, difference,
nat/zero-02 is used by still-in-diff, in-diff-notfirst, difference-notin, diff-swap, 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 union-diff-distr, subset-antisym, some, exin, diff-swap, diff-add-sw, bag-rm-add-eq,
bag-basic/count-1 is used by subset-one, count-one,
bag-basic/count-empty is used by union, subset-size, subset-one, subset-emp, some, in-emp, difference, del-notin, count-one, count-del,
bag-basic/count-other is used by union, subset-plusplus, subset-plusminus, in-add, diff-add-sw, del-notin, 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, del-notin, count-del, bag-rm-add-eq,
bag-basic/extension is used by union-inj, union-diff-cancel, union-com, union-ass, subset-emp,
bag-basic/insert-inj is used by subset-plus, del-notin,