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

Used from specification bag-basic

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

Used from specification nat-basic

nat-basic/a is used by subset-in, subset-exdiff, union-diff-distr, union, subset-plusminus, union-inj, diff-size, subset-size, count-del, diff-swap, bag-rm-add-eq, del-notin, diff-add-sw, del-size, subset-plusplus, difference, exin, union-subset, forall-def, union-size, in-add, union-diff-cancel, exists-def, filter-count, in-union, union-ass, union-com, subset-smaller, union-subset-inj,
nat-basic/add-base is used by union-diff-distr, union, count-del, bag-rm-add-eq, diff-add-sw, del-size, forall-def, union-size, exists-def, filter-count,
nat-basic/c is used by subset-in, subset-exdiff, union-diff-distr, union, subset-plusminus, union-inj, diff-size, subset-size, count-del, diff-swap, bag-rm-add-eq, del-notin, diff-add-sw, del-size, subset-plusplus, difference, exin, union-subset, forall-def, union-size, in-add, union-diff-cancel, exists-def, filter-count, in-union, union-ass, union-com, subset-smaller, union-subset-inj,
nat-basic/eq-01 is used by union, union-inj, count-del, bag-rm-add-eq, union-size, filter-count, union-ass, union-com,
nat-basic/eqs is used by diff-swap, diff-add-sw,
nat-basic/f is used by subset-in, union-diff-distr, still-in-diff, subset-plusminus, subset-size, diff-swap, diff-add-sw, subset-plusplus, in-diff-notfirst, difference, subset-antisym, subset-one, subset-trans, subset-smaller,
nat-basic/l is used by diff-swap, subset-plusplus,
nat-basic/l-02 is used by union-diff-distr, diff-swap, diff-add-sw, subset-smaller,
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, bag-rm-add-eq, difference, 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-swap, diff-add-sw,
nat-basic/ls-02 is used by diff-add-sw,
nat-basic/one-01 is used by subset-plusminus, bag-rm-add-eq, difference, exin, subset-one,
nat-basic/oz is used by count-del, del-size, difference, forall-def, exists-def,
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 diff-swap, del-notin, forall-def, in-add, exists-def, in-union,
nat-basic/zero is used by difference-notin, diff-swap,