[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/fle-01 is used by ls-03,
nat/le-addex is used by ls-01,
nat/le-def is used by ls-succ,
nat/lels is used by square-ls-03,
nat/pls is used by two-loup-04, two-loup-07,
nat/trans-ls-le is used by square-ls-03,
nat/add-01 is used by mod-succ-02, two-ppred,
nat/add-num-03 is used by two-neq-01, two-neq-02,
nat/add-num-04 is used by div-two-mult,
nat/anti is used by two-loup-11,
nat/cancel-01 is used by mod-once,
nat/elim-pred-c is used by div-two-mult, two-loup-04, two-loup-02,
nat/elim-sub is used by rec, mod-rec, rax,
nat/eq is used by leq-modsucc,
nat/eq-01 is used by mod-rew,
nat/eq-02 is used by two-loup-01,
nat/eqle-one is used by leq-modsucc, ls-03,
nat/fle is used by le-01, leq-modsucc, ls, two-loup-02, two-loup-08, two-loup-12, ls-03,
nat/fle-01 is used by le-01, mult-ls-01, mult-ls, le, two-loup-11, ls-03, ls-02, ls-01,
nat/l-num-01 is used by two-loup-02,
nat/l-num-04 is used by two-loup-02,
nat/l-num-05 is used by square-nle-01-01,
nat/le-add is used by le-div-to-mult,
nat/le-def is used by square-interval, square-nle-01, mod-le-01, mod-le-02, mod-le-03, le-div-to-mult, two-loup-01, le, mod-le, mod-once, two-loup-07, mod-neq, le-succ, two-ls-01, two-le, ls-01, cond,
nat/le-ls-simp is used by le-01, square-interval, mod-le-03, le-div-to-mult, two-loup-07, two-loup-12, two-loup-11, square-ls-03,
nat/le-one is used by mod-nls,
nat/lels is used by square-interval, mult-ls-01, mod-le-04, add, mult-ls, ls, mod-ls, two-loup-04, two-loup-02, two-loup-08, two-loup-07, two-loup-12, two-loup-11, two-ls-03, two-padd, ls-03, ls-02, square-ls-03,
nat/lels-02 is used by modulo-between-equal2, modulo-between-equal3, one-01, one,
nat/lels-03 is used by square-nle-01-01,
nat/lep is used by square-inject,
nat/lep-02 is used by square-nle-01-01, le-div-to-mult, mod-once, square-ls-03,
nat/ler is used by mod-le-04,
nat/let is used by mult-ls-01, mod-le-04, ls-02, square-ls-03,
nat/lez-01 is used by square-nle-01, zero, ls, ls-01,
nat/ls-01 is used by mod-neq,
nat/ls-le-simp is used by mult-ls-01, div-le-01, div-le, two-loup-12, two-loup-13, two-padd, ls-03, cond-01, two-loup, square-ls-03,
nat/succ-01 is used by square-nle-01-01, square-ls-03,

Used from specification nat-mult

nat-mult/dist is used by square-interval, le-div-to-mult, square-inject, mod-by6, ls-01, two-neq-02, square-ls-03,
nat-mult/mult-c is used by div-succ,
nat-mult/square-inject is used by square-inject,
nat-mult/square-interval is used by square-interval,
nat-mult/square-ls is used by square-ls-02,
nat-mult/coef-01 is used by mod-by6,
nat-mult/coef-04 is used by square-inject,
nat-mult/coef-08 is used by ls-03,
nat-mult/coef-18 is used by square-ls-03,
nat-mult/coef-21 is used by le-01, square-interval, mult-ls-01, mult-ls, modulo-between-equal, ls-03, ls-02,
nat-mult/dist is used by two-loup-04, two-loup-02,
nat-mult/eq is used by mult-div, exmult, modex,
nat-mult/le is used by mult-ls-01,
nat-mult/le-05 is used by zero-01,
nat-mult/le-num is used by square-interval, two-le-03,
nat-mult/leone is used by div-le-01, div-le, two-le-01, one, two-ls-03,
nat-mult/ls is used by modulo-between-equal, two-loup-04,
nat-mult/ls-01 is used by mod-eq-01,
nat-mult/ls-02 is used by le-01, ls-03,
nat-mult/ls-08 is used by mod-eq-01, square-nls, two-ls-02, two-ls,
nat-mult/mod-neq-01 is used by ls,
nat-mult/mod-neq-03 is used by mod-succ-04,
nat-mult/modeq is used by mod-succ-01, two-ppred, two-loup-09,
nat-mult/modeq-01 is used by two-mdiv2-02, div-mult, two-loup-09,
nat-mult/modls is used by le-div-to-mult, two-loup-07,
nat-mult/mult-a is used by div-two-mult, le-01, square-interval, square-nle-01, mult-ls-01, two-mdiv2-02, two-mdiv2-03, div-add, square-nle-01-01, mod-le-03, le-div-to-mult, two-twosucc-02, zero-01, mod2-succ, mod-mod, two-odd, div-le-01, div-elim, mult-div, nummult-eq, ls-even, mod-succ-01, mod-succ-05, mod-succ-04, mod-zero, div-le, square-inject, mult-ls, div-succ, zero, two-peq, ls, square-even, div-mult, two-eq, modulo-between-equal, mod-mod-01, mod-by6, two-loup-01, two-ppred, two-le-03, le, two-le-02, div-succ-01, two-le-01, mod-eq-01, square-even-01, square-even-02, one-01, square-even-03, mult-01, mult-02, mod-once, one, two-loup-04, two-loup-02, two-loup-09, two-loup-08, square-ls, two-loup-07, two-loup-06, modsucc-neq, two-loup-12, two-loup-11, two-loup-10, div-two-add, two-zero-01-01, exmult, two-loup-13, square-nls, le-succ, two-ls-04, two-ls-03, two-ls-05, two-ls-02, two-padd, ls-03, ls-02, mod-succ, mod-eq-mod-plus-1, cond-01, ls-01, two-neq-01, mod-mult, mod-eq, square-ls-01, two-neq-02, two-loup, two-ls, square-ls-02, mod-one, square-ls-03, cond, two-neq, modex, mult,
nat-mult/mult-c is used by div-two-mult, le-01, square-interval, square-nle-01, mult-ls-01, two-mdiv2-02, two-mdiv2-03, div-add, square-nle-01-01, mod-le-03, le-div-to-mult, two-twosucc-02, zero-01, mod2-succ, mod-mod, two-odd, div-le-01, div-elim, mult-div, nummult-eq, ls-even, mod-succ-01, mod-succ-05, mod-succ-04, mod-zero, div-le, square-inject, mult-ls, div-succ, zero, two-peq, ls, square-even, div-mult, two-eq, modulo-between-equal, mod-mod-01, mod-by6, two-loup-01, two-ppred, two-le-03, le, two-le-02, div-succ-01, two-le-01, mod-eq-01, square-even-01, square-even-02, one-01, square-even-03, mult-01, mult-02, mod-once, one, two-loup-05, two-loup-04, two-loup-02, two-loup-09, two-loup-08, square-ls, two-loup-07, two-loup-06, modsucc-neq, two-loup-12, two-loup-11, two-loup-10, div-two-add, two-zero-01-01, exmult, two-loup-13, square-nls, le-succ, two-ls-04, two-ls-03, two-ls-05, two-ls-02, two-padd, ls-03, ls-02, mod-succ, mod-eq-mod-plus-1, cond-01, ls-01, two-two-01, two-neq-01, mod-mult, mod-eq, square-ls-01, two-neq-02, two-loup, two-ls, square-ls-02, mod-one, square-ls-03, cond, two-neq, modex, mult,
nat-mult/nonumsimp-succ is used by mod-succ,
nat-mult/numeral-01 is used by mod-by6,
nat-mult/numeral-19 is used by two-peq, mod-by6, two-loup-09, two-loup-11, two-loup-10,
nat-mult/numeral-24 is used by ls-03,
nat-mult/numeral-26 is used by two-padd,
nat-mult/numeral-28 is used by two-eq, two-neq-01, two-neq-02, two-neq,
nat-mult/one is used by mod-succ-04, mod-zero, two-peq, two-eq, one-01, two-loup-09, modsucc-neq, two-loup-11, two-loup-10, two-padd, ls-03, two-neq-01, two-neq-02, mod-one, two-neq,
nat-mult/one-01 is used by modsucc-neq,
nat-mult/rdist is used by mod-by6,
nat-mult/rsucc-02 is used by le-01, square-interval, square-nle-01, mult-ls-01, square-nle-01-01, mod-le-03, le-div-to-mult, square-inject, mult-ls, div-succ, square-even, mod-by6, two-ppred, square-even-01, square-even-02, one-01, square-even-03, mod-once, one, square-ls, square-nls, le-succ, ls-03, ls-02, two-neq-01, mod-mult, square-ls-01, two-neq-02, square-ls-02, square-ls-03, mult,
nat-mult/square-even-01 is used by square-nle-01, square-even, square-nls,
nat-mult/square-two is used by square-nle-01,
nat-mult/succ is used by square-inject, mod-by6,
nat-mult/succ-01 is used by mod-succ-04, mod-eq-mod-plus-1,
nat-mult/two-02 is used by two-peq, mod-by6, two-loup-05, two-loup-04, two-loup-02, two-loup-09, two-loup-07, two-loup-11, two-loup-10, ls-03,
nat-mult/two-ls-01 is used by two-ls-04, two-ls-05,
nat-mult/two-one-01 is used by two-ppred, two-zero-01-01,
nat-mult/two-zero-01 is used by square-nle-01, two-loup-04, two-loup-08, two-loup-07,
nat-mult/twoeqf is used by two-loup-12, two-loup-11, two-loup-13, square-nls, two-loup,
nat-mult/twoeqf-01 is used by two-loup-08, two-loup-06, two-loup-12, square-nls,
nat-mult/twoeqf-02 is used by two-loup-12, two-loup-11, two-loup-13, two-loup,
nat-mult/twoeqf-03 is used by two-loup-08, two-loup-06, two-loup-12,
nat-mult/zero is used by nummult-eq, mod-succ-01, mod-succ-04, modulo-between-equal, mod-mod-01, mod-eq-01, mod-eq-mod-plus-1, mod-mult, mod-eq, mult,
nat-mult/zero-01 is used by mod-eq-01,
nat-mult/zero-02 is used by square-inject,
nat-mult/zero-06 is used by le-01, mod-mod, zero, mod-mod-01, le, one, two-zero-01-01, le-succ, ls-03, cond-01, ls-01, cond,

Used from specification nat-basic

nat-basic/a is used by square-inj,
nat-basic/addex is used by le-div-to-mult,
nat-basic/less is used by two-loup-02,
nat-basic/lstwo is used by two-zero-01-01, square-nls,
nat-basic/pls is used by two-loup-05,
nat-basic/twols-02 is used by square-nle-01,
nat-basic/a is used by div-two-mult, le-01, square-interval, square-nle-01, leq-modsucc, mult-ls-01, two-mdiv2-02, two-mdiv2-03, mod-ls-01, mod-ls-02, div-add, mod-le-01, square-nle-01-01, mod-le-03, le-div-to-mult, two-twosucc-02, mod2-succ, two-odd, div-elim, mod-mult-01, add, mod-succ-03, mod-succ-02, mod-succ-01, div-one, mod-succ-06, mod-succ-05, mod-succ-04, mod-zero, square-inject, mult-ls, div-succ, rec, two-peq, ls, square-even, div-mult, two-eq, modulo-between-equal, mod-mod-01, mod-by6, two-loup-01, two-ppred, modulo-between-equal2, div-succ-01, modulo-between-equal3, mod-eq-01, square-even-01, square-even-02, one-01, square-even-03, mod-once, one, two-loup-05, two-loup-04, two-loup-02, two-loup-09, two-loup-08, square-ls, two-loup-07, two-loup-06, modsucc-neq, two-loup-12, two-loup-11, two-loup-10, mod-rew, div-two-add, mod-rec, modsucc-less, two-zero-01-01, mod-neq, two-loup-13, square-nls, le-succ, two-ls-02, two-padd, two-ls-01, ls-03, ls-02, rax, mod-succ, mod-eq-mod-plus-1, mod-nls, ls-01, two-neq-01, mod-mult, mod-eq, square-ls-01, two-neq-02, two-loup, two-ls, two-rec, square-ls-02, mod-one, square-ls-03, cond, two-neq, modex, mult, two-three,
nat-basic/add-base is used by square-nle-01, leq-modsucc, two-mdiv2-03, le-div-to-mult, div-elim, mod-mult-01, mod-succ-02, mod-succ-04, modulo-between-equal, two-ppred, mod-eq-01, two-loup-08, two-loup-06, two-loup-12, two-loup-11, two-zero-01-01, two-loup-13, square-nls, mod-eq-mod-plus-1, mod-mult, mod-eq, two-loup, modex, mult,
nat-basic/between is used by two-loup-02, ls-03,
nat-basic/c is used by div-two-mult, le-01, square-interval, square-nle-01, leq-modsucc, mult-ls-01, two-mdiv2-02, two-mdiv2-03, mod-ls-01, mod-ls-02, div-add, mod-le-01, square-nle-01-01, mod-le-03, le-div-to-mult, two-twosucc-02, mod2-succ, two-odd, div-elim, mod-mult-01, add, mod-succ-03, mod-succ-02, mod-succ-01, div-one, mod-succ-06, mod-succ-05, mod-succ-04, mod-zero, square-inject, mult-ls, div-succ, rec, two-peq, ls, square-even, div-mult, two-eq, modulo-between-equal, mod-mod-01, mod-by6, two-loup-01, two-ppred, modulo-between-equal2, div-succ-01, modulo-between-equal3, mod-eq-01, square-even-01, square-even-02, one-01, square-even-03, mod-once, one, two-loup-05, two-loup-04, two-loup-02, two-loup-09, two-loup-08, square-ls, two-loup-07, two-loup-06, modsucc-neq, two-loup-12, two-loup-11, two-loup-10, mod-rew, div-two-add, mod-rec, modsucc-less, two-zero-01-01, mod-neq, two-loup-13, square-nls, le-succ, two-ls-02, two-padd, two-ls-01, ls-03, ls-02, rax, mod-succ, mod-eq-mod-plus-1, mod-nls, ls-01, two-two-01, two-neq-01, mod-mult, mod-eq, square-ls-01, two-neq-02, two-loup, two-ls, two-rec, square-ls-02, mod-one, square-ls-03, cond, two-neq, modex, mult, two-three,
nat-basic/eq-01 is used by leq-modsucc, div-add, two-twosucc-02, div-elim, mod-succ-02, mod-succ-01, square-inject, div-succ, rec, mod-by6, two-ppred, mod-eq-01, two-loup-09, modsucc-neq, two-loup-10, div-two-add, mod-eq-mod-plus-1, two-rec, square-ls-03, mult,
nat-basic/eq-02 is used by mod-zero, div-succ-01, mod-eq-01, two-loup-09, mod-one,
nat-basic/eqs is used by rax,
nat-basic/f is used by le-01, square-nle-01, leq-modsucc, mult-ls-01, mod-ls-03, mod-ls-01, mod-ls-02, square-nle-01-01, mod-le-03, le-div-to-mult, zero-01, div-le-01, div-elim, add, mod-succ-01, mod-succ-05, mod-succ-04, div-le, mult-ls, two-peq, ls, modulo-between-equal, two-loup-01, mod-eq-02, two-ppred, le, div-succ-01, mod-eq-01, two-loup-05, two-loup-04, two-loup-02, two-loup-09, two-loup-08, two-loup-07, two-loup-06, modsucc-neq, nummult-le-01, two-loup-12, two-loup-11, mod-same, two-loup-10, modsucc-less, two-zero-01-01, two-loup-13, square-nls, le-succ, two-ls-02, ls-03, ls-02, mod-eq-mod-plus-1, cond-01, mod-nls, ls-01, mod-eq, two-neq-02, two-loup, two-ls, square-ls-03, cond, modex,
nat-basic/l is used by le-01, mod-le-03, modulo-between-equal, two-loup-05, two-loup-04, two-loup-02, square-ls, two-loup-10, ls-03, square-ls-03,
nat-basic/l-01 is used by le-01, leq-modsucc, add, modulo-between-equal, one, two-loup-10, ls-03,
nat-basic/l-02 is used by mod-ls-01, mod-ls-02, two-loup-04, two-loup-12, modsucc-less, le-succ, ls-01, cond,
nat-basic/l-05 is used by two-peq, two-loup-08, two-loup-07, two-loup-06,
nat-basic/l-06 is used by two-loup-05,
nat-basic/less-zero is used by nummult-le-03, nummult-ls-03, nummult-ls-01, mod-succ-04, mod-eq-01, nummult-le-01, mod-eq-mod-plus-1,
nat-basic/lf is used by mod-succ-05, mod-succ-04, modulo-between-equal, two-loup-05, two-loup-04, two-loup-08, two-loup-07, two-loup-06, modsucc-less, square-nls, ls-03, two-loup,
nat-basic/lf-01 is used by leq-modsucc, two-loup-01, two-loup-05, two-loup-04, two-loup-02, modsucc-neq, mod-same,
nat-basic/lf-02 is used by mod-le-03, mod-succ-04, two-peq, two-loup-01, mod-eq-01, two-loup-04, two-loup-07, two-loup-11, mod-same, cond,
nat-basic/ls-02 is used by mod-ls-03, modulo-between-equal, one-01, two-loup-04, two-loup-03, two-loup-08, two-loup-06, two-loup-12, two-loup-13, two-loup,
nat-basic/neq-04 is used by one-01,
nat-basic/nls-fst is used by mod-succ-04, two-loup-01, two-loup-07,
nat-basic/one is used by square-nle-01, div-one, modulo-between-equal, two-loup-02, two-loup-10,
nat-basic/one-01 is used by square-nle-01-01, two-loup-01, one, modsucc-neq, mod-neq,
nat-basic/one-02 is used by mod-one-01,
nat-basic/one-03 is used by two-peq, two-ppred, two-loup-08,
nat-basic/one-04 is used by modsucc-neq,
nat-basic/one-06 is used by div-one, two-zero-01-01,
nat-basic/oz is used by div-two-mult, leq-modsucc, le-div-to-mult, mod-succ-02, div-one, mod-succ-06, div-succ, two-ppred, two-loup-04, two-loup-02, two-zero-01-01, le-succ, mod-succ,
nat-basic/refl-Nat is used by le-01, mult-ls-01, mult-ls, div-succ, two-loup-07, two-loup-11, mod-neq, ls-03, ls-02,
nat-basic/s-04 is used by le-01, square-interval, mult-ls-01, add, mult-ls, div-succ, modulo-between-equal, two-loup-02, two-loup-11, mod-neq, le-succ, ls-03, ls-02, square-ls-01, square-ls-03,
nat-basic/succ is used by le-01, leq-modsucc, mult-ls-01, mod-le-03, le-div-to-mult, mod-succ-02, mod-succ-05, mod-succ-04, mult-ls, modulo-between-equal, mod-by6, two-ppred, one-01, one, two-loup-05, two-loup-08, two-loup-07, two-loup-06, modsucc-less, square-nls, ls-03, ls-02, mod-mult, two-loup, mult,
nat-basic/succ-03 is used by leq-modsucc, add, mod-succ-01, two-loup-01, div-succ-01, two-loup-04, two-loup-02, two-loup-11, two-loup-10, modsucc-less,
nat-basic/trans-Nat is used by mod-succ-05, mod-succ-04, modulo-between-equal, two-loup-05, two-loup-04, two-loup-02, two-loup-08, two-loup-07, two-loup-06, modsucc-less, square-nls, ls-03, two-loup,
nat-basic/twols is used by two-loup-01, two-loup-04, two-loup-02,
nat-basic/twols-02 is used by square-nle-01, mod2-succ, square-even, two-ppred, two-loup-02, two-loup-09, two-loup-08, two-loup-06, two-loup-12, two-loup-11, two-loup-10, two-odd-01, two-loup-13, two-loup,
nat-basic/z-01 is used by square-nle-01, le-div-to-mult, mod-succ-02, div-succ, two-eq, mod-mod-01, le-succ, two-neq-01, two-neq-02, two-neq,
nat-basic/z-02 is used by two-loup-04, two-loup-02, two-loup-08,
nat-basic/zero is used by nummult-le-03, nummult-ls-03, nummult-ls-01, mod-succ-04, two-loup-01, mod-eq-01, mod-zero-01, nummult-le-01, modsucc-less, modex,