[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/q-add is used by oex,
nat-basic/a is used by zero, meven-02, max-a, modd-02, div2-even, eo-01, eo, odd-div2, two-02, min-distr, odd-add, eo-02, div2-odd-01, odd-mult, oe-01, max-distr, even-add, zero-01, otwo-02, div2-elim-01, meven-03, modd-03, oe-02, pot2-odd-02, two-03, otwo-03, zero-02, div2-odd, even-div2, pot2-even-02, even-mult, ozero, div2-elim, odd, oex, one, plus,
nat-basic/add-base is used by pot2-odd-02,
nat-basic/c is used by zero, meven-02, max-a, modd-02, div2-even, eo-01, eo, odd-div2, two-02, min-distr, odd-add, eo-02, div2-odd-01, odd-mult, oe-01, max-distr, even-add, zero-01, otwo-02, div2-elim-01, meven-03, modd-03, oe-02, pot2-odd-02, two-03, otwo-03, zero-02, div2-odd, even-div2, pot2-even-02, even-mult, ozero, div2-elim, odd, oex, one, plus,
nat-basic/eq-01 is used by odd-div2, two-02, min-distr, odd-add, odd-mult, max-distr, even-add, oe-02, pot2-odd-02, even-mult, div2-elim, oex, plus,
nat-basic/f is used by max-a, min-ls-self2, zero-01, min-c, min-ls-both, max-c, min-a,
nat-basic/l is used by min-distr, max-distr,
nat-basic/l-02 is used by max-a,
nat-basic/less-zero is used by min-zero2,
nat-basic/lf is used by max-a, min-a,
nat-basic/ls-02 is used by max-a, min-distr, max-distr, min-ls-self2, min-c, max-c, min-a,
nat-basic/lstwo is used by pot2-odd-02,
nat-basic/neq-01 is used by max-a,
nat-basic/one-01 is used by odd,
nat-basic/one-03 is used by two-03,
nat-basic/oz is used by eo-02, otwo-02, two-03,
nat-basic/refl-nat is used by max-a, min-ls-self2, min-ls-both,
nat-basic/succ is used by max-a, two-03, oex,
nat-basic/trans-nat is used by max-a, min-a,
nat-basic/z-01 is used by two-02,

Used from specification nat

nat/add-num-01 is used by eo-02, even-add, otwo-02,
nat/add-num-04 is used by otwo-03,
nat/elim-pred-c is used by two-02, eo-02, otwo-02,
nat/elim-sub is used by odd-add, odd-mult, even-add, even-mult, plus,
nat/fle is used by max-a, min-a,
nat/le-add is used by two-03,
nat/le-def is used by odd-add, odd-mult, even-add, even-mult, plus,
nat/lels is used by max-a, min-distr, max-distr, min-c, max-c, min-a,
nat/lels-02 is used by max-a, min-distr, max-distr, min-c, odd, max-c, min-a,
nat/lep is used by odd-add, odd-mult, even-add, even-mult,
nat/let is used by max-a,
nat/ls-le-simp is used by max-a, min-a,

Used from specification nat-mult

nat-mult/dist is used by odd-add, odd-mult, even-add, even-mult,
nat-mult/two-succ-06 is used by plus,
nat-mult/coef-04 is used by odd-add, even-add, plus,
nat-mult/coef-17 is used by two-02, eo-02, otwo-02,
nat-mult/dist is used by two-02, eo-02, otwo-02, two-03, plus,
nat-mult/le2-02 is used by zero-02,
nat-mult/ls-01 is used by zero-01,
nat-mult/mult-a is used by zero, meven-02, modd-02, div2-even, odd-div2, two-02, odd-add, eo-02, div2-odd-01, odd-mult, even-add, zero-01, otwo-02, div2-elim-01, meven-03, modd-03, pot2-odd-02, two-03, otwo-03, zero-02, div2-odd, even-div2, pot2-even-02, even-mult, ozero, div2-elim, odd, oex, one, plus,
nat-mult/mult-c is used by zero, meven-02, modd-02, div2-even, odd-div2, two-02, odd-add, eo-02, div2-odd-01, odd-mult, even-add, zero-01, otwo-02, div2-elim-01, meven-03, modd-03, pot2-odd-02, two-03, otwo-03, zero-02, div2-odd, even-div2, pot2-even-02, even-mult, ozero, div2-elim, odd, oex, one, plus,
nat-mult/one-01 is used by one,
nat-mult/rsucc-02 is used by odd-add, odd-mult, even-add, even-mult,
nat-mult/two-02 is used by zero, meven-02, div2-even, eo-01, eo, odd-div2, two-02, odd-add, eo-02, div2-odd-01, odd-mult, oe-01, even-add, zero-01, otwo-02, div2-elim-01, meven-03, modd-03, oe-02, pot2-odd-02, two-03, otwo-03, zero-02, div2-odd, even-div2, pot2-even-02, even-mult, ozero, div2-elim, odd, oex, one, plus,
nat-mult/two-one-01 is used by otwo-03,
nat-mult/two-succ-05 is used by meven-02, odd-add, odd-mult, even-add, meven-03, modd-03, pot2-odd-02, even-mult, oex,
nat-mult/two-succ-06 is used by odd-add, odd-mult, even-add, even-mult, plus,
nat-mult/two-zero-01 is used by zero, zero-01, two-03, zero-02, ozero, odd,
nat-mult/twoeq is used by two-03,
nat-mult/zero-02 is used by div2-elim-01,

Used from specification nat-div

nat-div/div-elim is used by pot2-odd-02,
nat-div/two-mdiv2-02 is used by div2-even, odd-div2, even-add, div2-elim-01, pot2-odd-02, even-div2, pot2-even-02,
nat-div/two-mdiv2-03 is used by odd-div2, even-div2, div2-elim,
nat-div/two-rec is used by odd-div2,