[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 unique-elems-rem-notin, unique-elems-add, max-subseteq, max-rem-notsame, max-in-ls, in-rec, bag-rem-subseteq, bag-rem-empty, bag-count-addtwice, bag-add-rev, bag-add-rem-same,
nat-basic/add-base is used by unique-elems-add, max-rem-notsame, bag-add-rev, bag-add-rem-same,
nat-basic/c is used by unique-elems-rem-notin, unique-elems-add, max-subseteq, max-rem-notsame, max-in-ls, in-rec, bag-rem-subseteq, bag-rem-empty, bag-count-addtwice, bag-add-rev, bag-add-rem-same,
nat-basic/eq-01 is used by bag-add-rev, bag-add-rem-same,
nat-basic/eq-02 is used by bag-add-rem-same,
nat-basic/f is used by max-subseteq, max-rem-notsame, max-rem-ls, max-in-ls, max-in-bag, max-add-smaller, bag-rem-subseteq, bag-rem-notmax,
nat-basic/l-02 is used by bag-rem-subseteq,
nat-basic/l-05 is used by max-in-ls,
nat-basic/lf is used by max-subseteq, max-rem-notsame, max-in-ls,
nat-basic/lf-01 is used by max-rem-notsame, max-in-ls, bag-rem-notmax,
nat-basic/lf-02 is used by max-rem-notsame, max-in-ls,
nat-basic/ls-02 is used by max-subseteq, max-rem-notsame, max-in-ls, max-add-bigger,
nat-basic/neq-01 is used by max-rem-notsame,
nat-basic/nls-fst is used by max-subseteq,
nat-basic/one is used by unique-elems-subset, unique-elems-add,
nat-basic/one-01 is used by bag-rem-subseteq, bag-add-rem-same,
nat-basic/one-03 is used by unique-elems-add, max-rem-notsame,
nat-basic/one-06 is used by max-rem-notsame,
nat-basic/oz is used by unique-elems-rem-notin,
nat-basic/ref is used by max-subseteq, max-rem-notsame, max-add-smaller, max-add-one-different, bag-rem-subseteq,
nat-basic/succ is used by max-subseteq, max-rem-notsame, max-in-ls,
nat-basic/trans is used by max-subseteq, max-rem-notsame, max-in-ls,
nat-basic/z-01 is used by max-rem-notsame, in-rec, bag-add-rem-same,

Used from specification bag-union

bag-union/nat-bag/count-del is used by unique-elems-rem-notin, bag-rem-subseteq, bag-rem-empty, bag-add-rem-same,
bag-union/nat-bag/count-subset is used by unique-elems-subset, bag-rem-subseteq,
bag-union/nat-bag/diff-rec is used by bag-diff-one,
bag-union/nat-bag/difference is used by bag-diff-empty,
bag-union/nat-bag/in is used by unique-elems-rem-notin, unique-elems-add, in-rec, bag-remadd-in, bag-in-single, bag-add-rem-same,
bag-union/nat-bag/one is used by bag-union-one, bag-single-max, bag-diff-one,
bag-union/nat-bag/bag-rm-add-eq is used by bag-remadd-in,
bag-union/nat-bag/del-empty is used by max-rem-notsame, bag-remadd-in, bag-rem-notmax, bag-add-rem-same,
bag-union/nat-bag/del-notin is used by max-rem-notsame, bag-remadd-in, bag-add-rem-same,
bag-union/nat-bag/del-rec is used by max-rem-notsame, bag-remadd-in, bag-rem-notmax, bag-rem-empty, bag-add-rem-same,
bag-union/nat-bag/diff-empty is used by bag-diff-one,
bag-union/nat-bag/in-add is used by max-in-ls, max-in-bag, bag-remadd-in,
bag-union/nat-bag/in-at is used by unique-elems-addtwice, bag-remadd-in,
bag-union/nat-bag/in-emp is used by max-in-ls, max-in-bag, bag-remadd-in, bag-empty-notin,
bag-union/nat-bag/in-rem-notrem is used by unique-elems-rem-notin,
bag-union/nat-bag/subset-emp is used by max-subseteq,
bag-union/nat-bag/subset-plus is used by max-subseteq,
bag-union/nat-bag/union-ass is used by bag-union-one,
bag-union/nat-bag/union-com is used by bag-union-one,
bag-union/nat-bag/union-empty is used by bag-union-one,
bag-union/nat-bag/union-rec is used by bag-union-one,

Used from specification nat

nat/add-num-03 is used by bag-count-addtwice,
nat/elim-pred-c is used by unique-elems-rem-notin, bag-rem-empty,
nat/eq-02 is used by bag-add-rem-same,
nat/fle-01 is used by max-subseteq, max-rem-notsame, max-in-ls, bag-rem-notmax,
nat/gr-def is used by max-subseteq, max-rem-notsame, max-rec-simp, max-in-ls, max-in-bag, max-add-smaller, max-add-one-different, max-add-bigger, bag-rem-notmax,
nat/le-def is used by unique-elems-subset, unique-elems-add, bag-rem-subseteq, bag-add-rem-same,
nat/le-ls-simp is used by max-rem-notsame,
nat/lels is used by max-subseteq, max-rem-notsame, max-in-ls, bag-rem-notmax,
nat/ler is used by max-rem-notsame, bag-diff-empty,
nat/let is used by unique-elems-subset,
nat/ls is used by bag-rem-subseteq,
nat/one-01 is used by unique-elems-rem-notin, unique-elems-add,
nat/one-02 is used by unique-elems-subset, unique-elems-add,
nat/sub-base is used by unique-elems-rem-notin, bag-rem-subseteq, bag-rem-empty, bag-add-rem-same,
nat/zero is used by bag-diff-empty,

Used from specification bag-basic

bag-basic/nat-bag/count-insert is used by unique-elems-add, max-rem-notsame, bag-add-rev, bag-add-rem-same,
bag-basic/nat-bag/extension is used by bag-rem-empty, bag-diff-empty, bag-add-rev, bag-add-rem-same,
bag-basic/nat-bag/bag-add2-eq-elim is used by bag-remadd-in,
bag-basic/nat-bag/count-1 is used by max-rem-notsame, bag-rem-empty, bag-in-single, bag-add-rem-same,
bag-basic/nat-bag/count-empty is used by unique-elems-empty, max-rem-notsame, bag-rem-empty, bag-in-single, bag-diff-empty, bag-add-rem-same,
bag-basic/nat-bag/count-other is used by max-rem-notsame, in-rec, bag-rem-empty, bag-in-single, bag-add-rev, bag-add-rem-same,
bag-basic/nat-bag/count-same is used by unique-elems-add, max-rem-notsame, in-rec, bag-count-addtwice, bag-add-rev, bag-add-rem-same,
bag-basic/nat-bag/insert-inj is used by bag-union-one, bag-remadd-in,
bag-basic/nat-bag/insert-nonempty is used by max-subseteq, max-rem-notsame, max-in-bag, bag-rem-notmax, bag-add-nonempty,