[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 perm-shift-two, perm-shift-one, mkbag-update-out-of-bound, mkbag-update, mkbag-size, index-in-mkbag, in-mkbag-del-two, in-mkbag-del, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one, count-del-same,
nat-basic/add-base is used by count-mkbag-greater-two, count-mkbag-greater-one, count-del-same,
nat-basic/c is used by perm-shift-two, perm-shift-one, mkbag-update-out-of-bound, mkbag-update, mkbag-size, index-in-mkbag, in-mkbag-del-two, in-mkbag-del, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one, count-del-same,
nat-basic/eq-01 is used by perm-shift-two, mkbag-size,
nat-basic/eq-02 is used by perm-shift-two, perm-shift-one,
nat-basic/f is used by perm-swap, perm-shift-two, perm-shift-one, mkbag-update-out-of-bound, mkbag-update, mkbag-del-add-content-two, mkbag-del-add-content, index-in-mkbag, in-mkbag-del-two, in-mkbag-del, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,
nat-basic/l is used by perm-shift-two,
nat-basic/less-1 is used by mkbag-update, index-in-mkbag, count-mkbag-non-zero,
nat-basic/lf is used by count-mkbag-greater-two, count-mkbag-greater-one,
nat-basic/lf-01 is used by in-mkbag-del-two, count-mkbag-greater-two,
nat-basic/lf-02 is used by mkbag-update, in-mkbag-del-two, count-mkbag-greater-two,
nat-basic/ls-02 is used by in-mkbag-del-two,
nat-basic/nls-fst is used by perm-shift-two, perm-shift-one,
nat-basic/one is used by in-mkbag-del-two, in-mkbag-del, count-mkbag-greater-two, count-mkbag-greater-one,
nat-basic/one-01 is used by count-mkbag-greater-one,
nat-basic/one-06 is used by count-mkbag-greater-one,
nat-basic/oz is used by in-mkbag-del-two, count-del-same,
nat-basic/ref is used by mkbag-update-out-of-bound,
nat-basic/s-04 is used by mkbag-update, index-in-mkbag, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,
nat-basic/succ is used by mkbag-update-out-of-bound, mkbag-update, mkbag-size, index-in-mkbag, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,
nat-basic/trans is used by count-mkbag-greater-one,
nat-basic/twols-02 is used by count-mkbag-greater-two,
nat-basic/z-01 is used by count-mkbag-non-zero,

Used from specification bag-union

bag-union/count-del is used by count-del-same, count-del-other,
bag-union/in is used by in-mkbag-del-two, in-mkbag-del,
bag-union/bag-rm-add-eq is used by bag-del-add,
bag-union/del-empty is used by mkbag-update,
bag-union/del-notin is used by count-del-same,
bag-union/del-rec is used by perm-swap, perm-shift-two, perm-shift-one, mkbag-update,
bag-union/in-add is used by index-in-mkbag,
bag-union/size-empty is used by mkbag-size,
bag-union/size-rec is used by mkbag-size,

Used from specification nat

nat/anti is used by count-mkbag-greater-two,
nat/add-01 is used by count-del-same,
nat/add-num-04 is used by count-mkbag-greater-two,
nat/anti is used by mkbag-update, index-in-mkbag, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,
nat/elim-pred-c is used by in-mkbag-del-two, in-mkbag-del, count-del-same,
nat/fle is used by perm-shift-two, mkbag-del-add-content-two, mkbag-del-add-content, in-mkbag-del-two, in-mkbag-del, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,
nat/fle-01 is used by mkbag-del-add-content, count-mkbag-greater-one,
nat/ge is used by count-mkbag-greater-one,
nat/gr-def is used by in-mkbag-del-two, in-mkbag-del, count-mkbag-greater-two, count-mkbag-greater-one,
nat/l-num-05 is used by count-mkbag-greater-one,
nat/le-def is used by perm-shift-two, count-mkbag-greater-one,
nat/le-ls-simp is used by mkbag-del-add-content,
nat/lels is used by perm-swap, perm-shift-two, perm-shift-one, mkbag-update, mkbag-del-add-content, index-in-mkbag, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,
nat/lels-02 is used by mkbag-update, count-mkbag-greater-two, count-mkbag-greater-one,
nat/lels-03 is used by mkbag-update-out-of-bound, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,
nat/ler is used by perm-swap, perm-shift-two, perm-shift-one, count-mkbag-greater-two, count-mkbag-greater-one,
nat/let is used by mkbag-del-add-content,
nat/lez is used by count-mkbag-non-zero,
nat/ls-le-simp is used by perm-swap, perm-shift-two, perm-shift-one,
nat/not-zero is used by count-mkbag-greater-two,
nat/sub-base is used by in-mkbag-del-two, in-mkbag-del, count-del-same, count-del-other,
nat/succ-01 is used by mkbag-update-out-of-bound, count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,

Used from specification bag-basic

bag-basic/count-insert is used by count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,
bag-basic/extension is used by bag-swap-del,
bag-basic/bag-add2-eq-elim is used by perm-shift-two, perm-shift-one, mkbag-update, bag-swap-add,
bag-basic/count-empty is used by count-mkbag-non-zero, count-mkbag-greater-two, count-mkbag-greater-one,
bag-basic/insert-inj is used by mkbag-update-out-of-bound, mkbag-update,
bag-basic/insert-nonempty is used by mkbag-update,

Used from specification array

array/Put-other is used by mkbag-update,
array/Put-other is used by perm-swap,
array/Put-same is used by mkbag-update,
array/Size-put is used by perm-swap, perm-shift-two, perm-shift-one,
array/cngetput is used by perm-shift-two, perm-shift-one, mkbag-update-out-of-bound, mkbag-update,
array/ngp-06 is used by mkbag-update,
array/put-same-content is used by mkbag-update,
array/putgetinv is used by perm-swap,