Used simplifier rules/spec theorems by specification

Used from specification nat-basic

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

Used from specification nat

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