Used simplifier rules/spec theorems by specification

Used from specification nat-basic2

• nat-basic2/a is used by le-sum,
• nat-basic2/addex is used by le-addex, le-add-02, le-add-01, eq-add2n-1-eq-le,
• nat-basic2/c is used by le-sum,
• nat-basic2/pls is used by pls,
• nat-basic2/succ is used by num-01,
• nat-basic2/a is used by zero-01, zero, succ-05, succ-04, succ-02, succ-01, succ, sub-succ, sub-same, sub-ls-rew, sub-ls, sub-le-rew, sub-add-01, sub-add, shift-01, rec, prop-07, prop-06, prop-05, prop-04, prop-02, prop, pred-03, pred-02, pred-01, pred, pls, one-01, num-02, num-01, neq-add1, neq-01, ls-pred, ls-add-not-03, ls-add-not-02, ls-add-not-01, ls-add-not, ls-07, ls-06, ls-04, ls-03, ls-02, ls-01, ls, less-03, less-02, less-01, less, les, leprf, lepr, lep-02, lep-01, lep, lels-04, le-sum, le-one, le-num-06, le-num-03, le-num-02, le-num-01, le-addex, le-add-02, le-add-01, le-add, le, l-num-06, l-num-03, l-num-02, l-num-01, eqle-one, eq-pred-01, eq-pred, eq-add2n-1-eq-le, eq-03, eq-02, eq-01, eq, elim-sub, elim-pred-c, cancel-01, add-sub-less, add-num-04, add-num-03, add-num-02, add-num-01, add-ls-right2-le, add-le-right2-ls, add-03, add-02, add-01, add,
• nat-basic2/add-base is used by zero-01, shift-01, neq-01, ls-add-not-01, less-03, less, lep-02, lep-01, le-sum, le-add, elim-sub,
• nat-basic2/c is used by zero-01, zero, succ-05, succ-04, succ-02, succ-01, succ, sub-succ, sub-same, sub-ls-rew, sub-ls, sub-le-rew, sub-add-01, sub-add, shift-01, shift, rec, prop-07, prop-06, prop-05, prop-04, prop-02, prop, pred-03, pred-02, pred-01, pred, pls, one-01, num-02, num-01, neq-add1, neq-01, ls-pred, ls-add-not-03, ls-add-not-02, ls-add-not-01, ls-add-not, ls-07, ls-06, ls-04, ls-03, ls-02, ls-01, ls, less-03, less-02, less-01, less, les, leprf, lepr, lep-02, lep-01, lep, lels-04, le-sum, le-one, le-num-06, le-num-03, le-num-02, le-num-01, le-addex, le-add-02, le-add-01, le-add, le, l-num-06, l-num-03, l-num-02, l-num-01, eqle-one, eq-pred-01, eq-pred, eq-add2n-1-eq-le, eq-03, eq-02, eq-01, eq, elim-sub, elim-pred-c, cancel-01, add-sub-less, add-num-04, add-num-03, add-num-02, add-num-01, add-ls-right2-le, add-le-right2-ls, add-03, add-02, add-01, add,
• nat-basic2/eq is used by zero, neq-add1, less-03, less, le-addex, eq-add2n-1-eq-le,
• nat-basic2/eq-01 is used by sub-succ, sub-same, sub-add, rec, prop-05, prop-02, num-02, neq-01, le-addex, le-add-02, eq-add2n-1-eq-le, eq-02, eq-01, elim-sub, cancel-01, add-sub-less, add-03, add,
• nat-basic2/even-02 is used by add-02,
• nat-basic2/l is used by succ-05, sub-ls-rew, sub-ls, pls, neq-01, ls-add-not, ls-07, ls-04, ls-01, ls, less-03, less-02, less, lep-02, lels-04, le-sum, l-num-02, l-num-01,
• nat-basic2/l-01 is used by ls-06, less,
• nat-basic2/l-02 is used by sub-succ, sub-same, prop-04, pls, ls-pred, ls-add-not, lep, lels-04, le-sum, eq-01, add-sub-less, add-num-03, add-01,
• nat-basic2/l-03 is used by add-02,
• nat-basic2/l-04 is used by ls-add-not-03, ls-add-not-02, ls-add-not-01, ls-add-not,
• nat-basic2/l-05 is used by succ-05, sub-ls, ls-pred, le-num-03, l-num-06,
• nat-basic2/nls-fst is used by le-num-06, l-num-03,
• nat-basic2/one-03 is used by one-01,
• nat-basic2/oz is used by succ-05, pred-03, pred-02, pred, one-01, neq-add1, le-sum, le-num-06, l-num-03,
• nat-basic2/pls is used by le-sum,
• nat-basic2/pred is used by pred-03, num-01,
• nat-basic2/s is used by succ-02, succ-01, pred, ls-pred, les, le-sum, le-one, le-num-06, l-num-03,
• nat-basic2/succ is used by succ-05, sub-ls, shift-01, rax, pred-03, one-01, num-02, num-01, neq-01, ls-pred, less, lep-02, lep-01, le-sum, le-num-06, le-num-03, l-num-06, l-num-03, elim-sub,
• nat-basic2/z-01 is used by one-01, le-addex, le-add-02, le-add-01, eq-add2n-1-eq-le,

Used from specification nat-basic1

• nat-basic1/lf-07 is used by fle,
• nat-basic1/elim-pred-c is used by pred-03,
• nat-basic1/f is used by zero-01, trans-ls-le, trans-le-ls, trans-le-le, succ-05, sub-succ, sub-ls-rew, sub-ls, prop, pred, pls, neq-01, ls-pred, ls-add-not-03, ls-add-not-02, ls-add-not-01, ls-add-not, let, less-03, less, lels-04, le-sum, le-one, le-num-06, le-num-03, le-num-01, le-ls-simp, le-addex, le-add-02, le-add-01, l-num-06, l-num-03, l-num-02, fle-01, fle, eq-add2n-1-eq-le, elim-sub, cancel-01, add-sub-less, add-ls-right2-le, add-le-right2-ls, add-01, add,
• nat-basic1/lf is used by succ-05, sub-ls, ls-pred, less, le-one, le-num-03, l-num-06, elim-sub,
• nat-basic1/lf-01 is used by neq-01, fle, add,
• nat-basic1/ls-02 is used by lels-03, le-rec, fle,
• nat-basic1/ls-03 is used by anti,
• nat-basic1/neq-01 is used by lels-02,
• nat-basic1/one is used by succ-05, less,
• nat-basic1/one-01 is used by one-02, one-01, leprf, lepr,
• nat-basic1/ref-1 is used by zero-01, zero, sub-ls, ls-06, ler, leprf, lepr, le-sum, le-ls-simp, eq, elim-sub,
• nat-basic1/trans-1 is used by succ-05, sub-ls, ls-pred, le-one, le-num-03, l-num-06, elim-sub,
• nat-basic1/zero is used by not-zero, ls-05,
• nat-basic1/zero-01 is used by lez-01, lez,