[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 is used by square-ls, mod-nle, square-ls-04, square-ls-05,
nat/fle-01 is used by modls-01, square-ls,
nat/le-def is used by le2-04, square-le-03, square-le-02, mult-le-01, ls-02,
nat/let is used by square-less,
nat/pls is used by twoeqf, twoeqf-01, twoeqf-03, nonumsimp-twonle,
nat/add-01 is used by modeq,
nat/add-num-01 is used by square-even, two-succ-03,
nat/add-num-03 is used by square-interval,
nat/add-num-04 is used by four-01, square-two, three, threeeq,
nat/anti is used by addle-01, le, mod-nle-01, mult-eq-succ-01, mult-le-01, le-04, mod-neq-02, sqls, two-succ-06,
nat/cancel-01 is used by dist-sub-02,
nat/elim-pred-c is used by modp, dist-sub-01, dist-sub-02, modeq, numeral-30, numeral-32, numeral-35, numeral-36, numeral-20, numeral-21, numeral-27, numeral-28, numeral-23, numeral-24, numeral-25, numeral-26, eq, numeral-19, square-ls, le-same,
nat/elim-sub is used by dist-sub-03, dist-sub-04, numeral-11, numeral-16, numeral-18, numeral-12, numeral-15, numeral-05, numeral-06, numeral-07, numeral-08, numeral-01, numeral-03, numeral-04, numeral-09,
nat/eq is used by twoeqf-03,
nat/eq-01 is used by dist-sub-01, dist-sub-03, dist-sub-04,
nat/eq-02 is used by modeq, numeral-25, numeral-19, le-same,
nat/eqle-one is used by mult-eq-succ, mod-neq-03,
nat/fle is used by mult-le-01, square-interval, modls, mod-nls, mod-nle, square-ls-04, sqr-09, ls-10,
nat/fle-01 is used by four-01, sqle-02, modls-03, mult-le-01, le-05, square-interval, le-same,
nat/l-num-04 is used by threels,
nat/l-num-05 is used by four-01,
nat/l-num-06 is used by modp, square-ls,
nat/le-add is used by mod-nle-01, numeral-32, numeral-15, le-same,
nat/le-def is used by coef-05, sqr, le-rew, modp, two-03, le2-04, le2-03, twoeqf-02, le, two-les-01, square-le-03, square-le-02, sqle-02, sqle-01, modls-03, mult-le-01, modeq, square-two, le-02, le-01, mult-le, numeral-29, numeral-25, numeral-10, numeral-19, twole-02, square-le, leone, sqle, square-ls, addle, le-succ, modls, sqr-06, coef-22, ls-02, ls-09, square-ls-04, square-ls-05, le-same, sqr-08, square-less,
nat/le-ls-simp is used by coef-05, le2-04, twoeqf-02, nonumsimp-twonle, square-le-02, mod-neq, modls-02, mult-le-01, square-two, square-interval, square-inject, square-le, square-ls, sqls, le-succ, modls, ls-06, square-ls-04, square-ls-05, le-same, square-less,
nat/le-num-01 is used by sqr-07,
nat/le-num-05 is used by square-two, three,
nat/le-one is used by leone,
nat/lels is used by coef-03, twoeqf, sqp, addle-01, four-01, le2-04, twoeqf-02, twoeqf-01, twoeqf-03, le, mod-nle-01, modls-01, modls-02, modls-03, mult-eq-succ-01, square-two, three, square-interval, numeral-10, numeral-17, mod-neq-02, mod-neq-03, square-ls, sqls, two-succ-06, le-succ, modls, sqr-03, sqr-01, ls-02, ls-05, ls-04, ls-06, ls-01, square-ls-04, square-ls-05, square-less,
nat/lels-02 is used by mult-eq-succ, four, modls, mod-nle,
nat/lels-03 is used by modls-02, dist-sub-03, mult-eq-succ-01, numeral-11, numeral-16, numeral-18, numeral-12, numeral-15, mod-neq-03, numeral-05, numeral-06, numeral-07, numeral-08, numeral-01, numeral-03, numeral-04, numeral-09, modls, mod-nls, square-ls-05,
nat/lep is used by mod-neq, square-inject,
nat/lep-02 is used by modp, modls-03, square-interval, numeral-35, numeral-20, numeral-23, numeral-26, numeral-16, mod-neq-03, square-inject, numeral-03, numeral-04, numeral-09, leone, square-ls, square-ls-05,
nat/ler is used by mod-nle-01, mult-eq-succ-01, mod-nle,
nat/les is used by mod-neq-03,
nat/let is used by sqle-02, mult-le-01, square-two, le-04, square-interval, le-succ, ls-01, sqr-09,
nat/lez is used by mult-le-01, le-05, le-04, leone,
nat/lez-01 is used by le, mult-le-01, square-two, le-04, numeral-15, leq-mult2, coef-22, ls-06, ls-09,
nat/ls is used by modp, modls-03, square-ls,
nat/ls-le-simp is used by coef-03, le-rew, modp, le2-04, square-le-03, le-succ, modls, ls-02, square-ls-05, square-less,
nat/not-zero is used by mult-le-01, square-two, le-succ, coef-22, sqr-08,
nat/one-01 is used by three, sqr-07,
nat/one-02 is used by sqp, mult-le-01, square-two, le-04, mult-le, leone, sqls, sqr-03, sqr-01, ls-04, sqr-08,
nat/pred-03 is used by modp, modeq, square-ls, le-same,
nat/prop-07 is used by numeral-07, numeral-01,
nat/succ-01 is used by coef-18, coef-12, square-interval, numeral-10, numeral-17, leone, sqr-02, ls-01, sqr-07,
nat/zero-01 is used by le,
nat/zero-02 is used by dist-sub,

Used from specification nat-basic

nat-basic/addex is used by modls-03,
nat-basic/ex-oddeven is used by ex-two,
nat-basic/lf is used by sqls,
nat-basic/one-04 is used by square-one,
nat-basic/trans-Nat is used by ls-06, mod-nle, square-less,
nat-basic/a is used by coef-08, coef-06, coef-07, coef-04, coef-05, coef-02, coef-03, coef-01, threels, nonumsimp-addls-01, twoeqf, succ-01, coef-18, coef-16, sqp, addle-01, coef-11, coef-12, coef-21, zero-01, rsucc, zero-03, four-01, zero-05, lssucc-01, mult-a, twols-01, mult-c, modp, two-03, two-02, le2-04, dist, twoeqf-02, square-even, twoeqf-01, twoeqf-03, nonumsimp-twonle, le, two-les-01, square-even-01, one-01, rdist, mod-nle-01, dist-merge, square-le-01, mod-neq, dist-sub-01, modls-01, nonumsimp-twols, dist-sub-02, dist-sub-03, modls-03, ex-two, dist-sub-04, mult-eq-succ, mult-eq-succ-02, mult-eq-succ-01, square-one, mult-le-01, modeq, square-two, nonumsimp-eqsucc, three, nonumsimp-twole, square-eq, eq-01, le-03, numeral-30, square-eq-01, le-01, square-interval, numeral-32, numeral-33, square-eq-03, nonumsimp-twoeq-01, numeral-35, numeral-36, mod-neq-01, numeral-20, numeral-21, nonumsimp-twoeq, numeral-27, numeral-28, numeral-29, numeral-23, numeral-24, numeral-25, numeral-26, nonumsimp-mod-neq-05, nonumsimp-succ, nonumsimp-mod-neq, succ-merge, numeral-10, numeral-11, numeral-16, numeral-17, numeral-18, eq, numeral-19, numeral-12, numeral-15, lssucc, mod-neq-02, mod-neq-03, square-inject, mod-neq-04, mod-neq-05, zero, numeral-05, numeral-06, numeral-07, numeral-08, numeral-01, threeeq, numeral-03, numeral-04, numeral-09, square-le, succ, leone, one, sqle, square-ls, addle, leq-mult2, two-succ-04, two-succ-05, two-succ-03, sqls, two-succ-06, rsucc-01, le-succ, modls, sqr-03, coef-22, sqr-02, ls-07, ls-08, ls-01, square-ls-01, nonumsimp-lstwo, modeq-01, mod-nle, square-ls-02, square-ls-04, square-ls-05, le-same, sqr-08, sqr-07, sqr-09,
nat-basic/add-base is used by coef-08, coef-06, coef-07, coef-04, succ-01, addle-01, modp, two-03, twoeqf-02, square-even, le, rdist, mod-nle-01, modls-03, modeq, nonumsimp-mod-neq-05, mod-neq-05, zero, leone, two-succ-06, ls-08, modeq-01, square-ls-05,
nat-basic/c is used by coef-08, coef-06, coef-07, coef-04, coef-05, coef-02, coef-03, coef-01, threels, nonumsimp-addls-01, twoeqf, succ-01, coef-18, coef-16, sqp, addle-01, coef-11, coef-12, coef-21, zero-01, rsucc, zero-03, four-01, zero-05, lssucc-01, mult-a, twols-01, mult-c, modp, two-03, two-02, le2-04, dist, twoeqf-02, square-even, twoeqf-01, twoeqf-03, nonumsimp-twonle, le, two-les-01, square-even-01, one-01, rdist, mod-nle-01, dist-merge, square-le-01, mod-neq, dist-sub-01, modls-01, nonumsimp-twols, dist-sub-02, dist-sub-03, modls-03, ex-two, dist-sub-04, mult-eq-succ, mult-eq-succ-02, mult-eq-succ-01, square-one, mult-le-01, modeq, square-two, nonumsimp-eqsucc, three, nonumsimp-twole, square-eq, eq-01, le-03, numeral-30, square-eq-01, le-01, square-interval, numeral-32, numeral-33, square-eq-03, nonumsimp-twoeq-01, numeral-35, numeral-36, mod-neq-01, numeral-20, numeral-21, nonumsimp-twoeq, numeral-27, numeral-28, numeral-29, numeral-23, numeral-24, numeral-25, numeral-26, nonumsimp-mod-neq-05, nonumsimp-succ, nonumsimp-mod-neq, succ-merge, numeral-10, numeral-11, numeral-16, numeral-17, numeral-18, eq, numeral-19, numeral-12, numeral-15, lssucc, mod-neq-02, mod-neq-03, square-inject, mod-neq-04, mod-neq-05, zero, numeral-05, numeral-06, numeral-07, numeral-08, numeral-01, threeeq, numeral-03, numeral-04, numeral-09, square-le, succ, leone, one, sqle, square-ls, addle, leq-mult2, two-succ-04, two-succ-05, two-succ-03, sqls, two-succ-06, rsucc-01, le-succ, modls, sqr-03, coef-22, sqr-02, ls-07, ls-08, ls-01, square-ls-01, nonumsimp-lstwo, modeq-01, mod-nle, square-ls-02, square-ls-04, square-ls-05, le-same, sqr-08, sqr-07, sqr-09,
nat-basic/eq-01 is used by mult-a, mult-c, dist, twoeqf-02, rdist, ex-two, mult-eq-succ, modeq, nonumsimp-eqsucc, square-eq-01, nonumsimp-twoeq, numeral-25, nonumsimp-mod-neq-05, eq, numeral-19, square-inject, numeral-07, numeral-01, one, rsucc-01,
nat-basic/eq-02 is used by addle-01, zero-03, mult-eq-succ-01, modeq, numeral-28, nonumsimp-mod-neq-05, mod-neq-02, numeral-08, two-succ-06,
nat-basic/f is used by twoeqf, succ-01, addle-01, four-01, modp, two-03, le2-04, ls, twoeqf-02, twoeqf-01, twoeqf-03, nonumsimp-twonle, le, mod-nle-01, square-le-02, sqle-02, sqle-01, mod-neq, dist-sub-03, modls-03, mult-eq-succ, mult-eq-succ-01, mult-le-01, modeq, three, square-eq, le-05, square-interval, square-eq-03, mult-le, numeral-10, numeral-11, numeral-16, numeral-17, numeral-18, numeral-12, numeral-15, mod-neq-02, mod-neq-03, numeral-05, numeral-06, numeral-08, numeral-03, numeral-04, numeral-09, leone, sqle, square-ls, sqls, two-succ-06, le-succ, modls, sqr-03, sqr-01, ls-04, ls-07, ls-06, ls-08, mod-nls, ls-01, modeq-01, mod-nle, square-ls-04, square-ls-05, le-same, sqr-08, sqr-09, square-less, ls-10,
nat-basic/l is used by nonumsimp-addls-01, lssucc-01, nonumsimp-twonle, nonumsimp-twols, square-interval, numeral-36, mod-neq-01, numeral-21, numeral-27, numeral-24, numeral-10, numeral-11, numeral-17, numeral-18, lssucc, square-inject, numeral-05, numeral-06, square-ls, mod-nle, square-ls-04, square-ls-05,
nat-basic/l-01 is used by twols-01, numeral-30, numeral-12, ls-07,
nat-basic/l-02 is used by square-interval, mod-neq-03, le-succ, modls, ls-08, square-ls-04, le-same,
nat-basic/l-04 is used by coef-03, square-ls, square-ls-05,
nat-basic/l-05 is used by modeq,
nat-basic/l-06 is used by mod-neq-03,
nat-basic/less-zero is used by addle-01, twoeqf-02, le, numeral-10, numeral-17, two-succ-06, ls-07,
nat-basic/lf is used by mod-neq-03, sqle, mod-nle, sqr-08,
nat-basic/lf-01 is used by twoeqf, twoeqf-01, mod-neq, mult-eq-succ-01, square-eq, square-eq-03, mod-neq-03, sqle, mod-nle,
nat-basic/lf-02 is used by twoeqf, twoeqf-01, mod-neq, mult-eq-succ-01, modeq, square-eq, square-eq-03, mod-neq-03, modls, ls-06, modeq-01,
nat-basic/ls-02 is used by twoeqf, twoeqf-01, mod-neq, modls-03, square-eq, square-interval, square-eq-03, mod-neq-03, square-ls, le-succ, modls, mod-nle,
nat-basic/neq-01 is used by two-03, square-eq, square-eq-03,
nat-basic/neq-04 is used by square-interval,
nat-basic/nls-fst is used by sqls, ls-08,
nat-basic/one is used by neqone, threels, succ-01, twols-01, mult-eq-succ-02, ls2-03, mult-le-01, mult-le, sqls, le-succ, sqr-03, sqr-06, sqr-02, coef-23, sqr-01, ls-04, ls-07, sqr-08,
nat-basic/one-01 is used by modp, two-03, modls-03, mult-eq-succ, modeq, numeral-25, numeral-19, sqle, square-ls, coef-22, square-ls-01, le-same, sqr-07,
nat-basic/one-03 is used by four-01, three,
nat-basic/one-04 is used by one-01,
nat-basic/one-05 is used by one-01,
nat-basic/one-06 is used by threels, zero-03, twols-01, ls-07,
nat-basic/oz is used by threels, zero-01, four-01, twols-01, modp, modeq, three, eq-01, le-03, numeral-10, numeral-17, eq, mod-neq-05, leone, square-ls, ls-07, ls-08,
nat-basic/refl-Nat is used by le, mod-neq-01, mod-neq-03, mod-neq-05, leone, ls-04, ls-01, le-same,
nat-basic/s-04 is used by addle-01, coef-11, coef-21, twoeqf-02, twoeqf-03, mod-neq, square-interval, numeral-10, numeral-17, mod-neq-03, square-inject, mod-neq-05, two-succ-06, ls-01, square-ls-02, square-ls-04,
nat-basic/succ is used by threels, addle-01, zero-01, rsucc, zero-03, four-01, mult-a, twols-01, mult-c, modp, dist, twoeqf-02, one-01, rdist, modls-03, modeq, three, eq-01, le-03, nonumsimp-mod-neq-05, numeral-10, numeral-17, eq, mod-neq-03, zero, threeeq, leone, one, sqle, square-ls, sqls, two-succ-06, rsucc-02, rsucc-01, ls-07, ls-08, ls-01, mod-nle, sqr-08, sqr-07,
nat-basic/trans-Nat is used by mod-neq-03, sqle, sqr-08,
nat-basic/twols-02 is used by two-03, mult-le-01, square-two, le-succ, sqr-08,
nat-basic/z-01 is used by coef-16, addle-01, zero-01, zero-05, mult-eq-succ, modeq, nonumsimp-twole, nonumsimp-mod-neq-05, eq, mod-neq-02, square-ls, leq-mult2, two-succ-06, coef-22, le-same,
nat-basic/z-02 is used by le-same,
nat-basic/zero is used by succ-01, two-03, ls-03-num, mod-nle-01, modls-03, mod-neq-05, square-ls, ls-03, ls-06, ls-01,