Used simplifier rules/spec theorems by specification

Used from specification nat

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

Used from specification nat-basic2

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

Used from specification nat-basic1

• nat-basic1/trans is used by sqls,
• nat-basic1/trans-1 is used by square-less, mod-nle, ls-06,
• nat-basic1/f is used by twoeqf-03, twoeqf-02, twoeqf-01, twoeqf, two-succ-06, three, square-ls-05, square-ls-04, square-ls, square-less, square-le-02, square-interval, square-eq-03, square-eq, sqr-09, sqr-08, sqr-03, sqr-01, sqls, sqle-02, sqle-01, sqle, numeral-18, numeral-17, numeral-16, numeral-15, numeral-12, numeral-11, numeral-10, numeral-09, numeral-08, numeral-06, numeral-05, numeral-04, numeral-03, nonumsimp-twonle, mult-le-01, mult-le, mult-eq-succ-01, mult-eq-succ, modp, modls-03, modls, modeq-01, modeq, mod-nls, mod-nle-01, mod-nle, mod-neq-03, mod-neq-02, mod-neq-01, mod-neq, ls-10, ls-08, ls-07, ls-06, ls-04, ls-01, ls, leone, le2-04, le-succ, le-same, le-05, le, four-01, dist-sub-03, addle-01,
• nat-basic1/less-1 is used by two-succ-06,
• nat-basic1/lf is used by sqr-08, sqle, mod-nle, mod-neq-03,
• nat-basic1/lf-01 is used by twoeqf-01, twoeqf, three, square-eq-03, square-eq, sqle-01, sqle, mult-eq-succ-01, modls, mod-nle, mod-neq-03, mod-neq-01, mod-neq, ls-01, four-01,
• nat-basic1/lf-02 is used by twoeqf-01, twoeqf, three, square-eq-03, square-eq, mult-eq-succ-01, modls, modeq-01, modeq, mod-nle, mod-neq-03, mod-neq-02, mod-neq-01, mod-neq, ls-06, four-01,
• nat-basic1/ls-02 is used by twoeqf-01, twoeqf, three, square-ls, square-interval, square-eq-03, square-eq, modls, mod-nle, mod-neq-03, mod-neq, le-succ,
• nat-basic1/neq-01 is used by two-03, square-eq-03, square-eq,
• nat-basic1/one is used by twols-01, threels, succ-01, sqr-08, sqr-06, sqr-03, sqr-02, sqr-01, sqls, neqone, mult-le-01, mult-le, mult-eq-succ-02, ls2-03, ls-07, ls-04, le-succ, coef-23,
• nat-basic1/one-01 is used by two-03, square-ls-01, square-ls, sqr-07, sqle, numeral-25, numeral-19, mult-eq-succ, modp, modls-03, le-same, coef-22,
• nat-basic1/ref-1 is used by modls, mod-nls, mod-nle, mod-neq-05, mod-neq-03, mod-neq-01, ls-04, ls-01, leone, le-same, le,
• nat-basic1/trans is used by mod-nls,
• nat-basic1/trans-1 is used by sqr-08, sqle, mod-nls, mod-neq-03,
• nat-basic1/twols-01 is used by two-03,
• nat-basic1/twols-02 is used by square-two, sqr-08, mult-le-01, le-succ,
• nat-basic1/z is used by two-03, modls,
• nat-basic1/zero is used by succ-01, square-ls, modp, modls-03, mod-nle-01, mod-neq-05, ls-06, ls-03-num, ls-03, ls-01,
• nat-basic1/zero-01 is used by le, addle-01,