Used simplifier rules/spec theorems by specification

Used from specification int-basic1

• int-basic1/lst-01 is used by abs-sub-01, le-three,
• int-basic1/irref is used by absls-01, les, abs-sub-02, lepr, succ-02, absls-05, num-between, abs-succ, ler, absls-06, abs-le-succ,
• int-basic1/lf-01 is used by le-three, abs-14, abs-11, zero-not, abs-05, succ-02, absls-02, absone-01, abs-15, int-simp-04, abs-ls, sub-less, absls-03,
• int-basic1/lf-02 is used by absa, abs-neg, zero-not, absls-02, absone-01,
• int-basic1/lf-04 is used by numlsledel-01, le-add-01, transrew-01, absp, numlslsdel, numlsf-02, forward-le-05, forward-le-02, zero-gels-04, numlslsdel-01, forward-lels, numlelsdel-01, zero-gels-01, int-simp-08, int-simp-11, abs-14, zero-not, forward-le-03, forward-lsle, abs-ls-01, le-add-02, forward-lele, numleledel, numlslsdel-02, mone-07, abssub-01, abs-ls-02, absls-02, transrew, abs-15, abs-06, numlelsdel, int-add-pos-01, int-add-pos, forward-le-04, forward-le, forward-le-01, numlsledel, abs-ls, numleledel-01, sub-less, numlslsdel-03, notle-pos, abs-le-succ,
• int-basic1/lf-07 is used by numlsledel-01, transrew-01, numlslsdel, numlsf-02, le-add-07, forward-le-05, forward-le-02, le-add-04, zero-gels-04, numlslsdel-01, forward-lels, numlelsdel-01, zero-gels-01, int-simp-11, abs-14, le-add-05, zero-not, forward-le-03, abs-ls-04, forward-lsle, le-add-08, ple-01, int-simp-06, forward-lele, numleledel, numlslsdel-02, zero-gs, abssub-01, abs-ls-02, transrew, abs-15, abs-06, numlelsdel, abs-succ, le-add-06, int-add-pos-01, int-add-pos, forward-le-04, le-add-03, forward-le, forward-le-01, abssub-05, zero-ge, numlsledel, abs-ls, numleledel-01, numlslsdel-03, absls-03, abs-19,
• int-basic1/lf-08 is used by numlsledel-01, transrew-01, absa, numlslsdel, forward-le-05, forward-le-02, zero-gels-04, numlslsdel-01, forward-lels, numlelsdel-01, zero-gels-01, estimate-add1-lsle-right, absls-04, mone-06, zero-not, forward-le-03, forward-lsle, ple-01, succ-02, forward-lele, numleledel, numlslsdel-02, estimate-add2-lsle-left, abs-ls-02, lsone, transrew, pls-01, numlelsdel, int-add-pos-01, int-add-pos, estimate-add2-lsle-right, forward-le-04, forward-le, forward-le-01, estimate-add1-lsle-left, numlsledel, int-simp-10, discard-add2-lels-left, numleledel-01, numlslsdel-03,
• int-basic1/ls-01 is used by abs-16, le-add-07, lels-02, abs-sub-01, le-three, absls, int-simp-08, abs-one-01, abs-ls-04, le-add-08, int-simp-06, abs-ls-02, absls-02, absone-01, abssub-02, abs-06, numlsf-01, int-simp-04, sub-less, int-simp-01,
• int-basic1/lst is used by zero-gels, abs-17, zero-gels-02, absls-02, numlsf-01, zero-gels-03,
• int-basic1/lst-01 is used by abseq, lels-02, le-three, le-rec, les, abs-one-01, anti, absone, mone-07, abs-ls-02, mone-04, absone-01, num-between, abs-06, abs-succ, zeroone, lstwo-01, mone-08,
• int-basic1/lst-02 is used by absa, absls-04, ple-01, absls-02, one-03,
• int-basic1/minus-one is used by abs-sub-01, absone-01,
• int-basic1/numlslsdel is used by le-three,
• int-basic1/pred is used by sub-pred,
• int-basic1/trans is used by abs-14, abs-11, zero-not, abs-05, succ-02, absls-02, absone-01, abs-15, int-simp-04, abs-ls, sub-less, absls-03,
• int-basic1/two-ls is used by lstwo-01,

Used from specification int-basic2

• int-basic2/ex-ls-add is used by int-simp-08, int-simp-06, int-simp-03, int-simp-04, int-simp-10, int-simp-01,
• int-basic2/pls-02 is used by le-add-01,
• int-basic2/add-a is used by abs-sub, le-add-01, sub-ls, absa, ttwo, abs-01, abseq, sub-add-09, minus-five, neg-08, neg-14, abs-neg, succ-01, pls, numlsf, sub-sub-02, numlsf-02, le-add-07, abssub-03, estimate-add1-ls-right, lep, neg-11, abs-sub-01, numls-01, negone, sub-add-06, minus-four, num-subadd, le-add-04, absls, zero-eq, numadd, int-simp-02, minus-02, minus, le-rec, sub-add-03, absneg-01, absls-01, k-sub-rec2, le-rew-succ, sub-ls-01, sub-pred, les, ple-03, mone-03, int-simp-08, abs-one-01, int-simp-11, estimate-add2-ls-right, sub-minus, int-simp-05, sub-sub-03, abssub, sub-zero, abs-08, estimate-add1-lsle-right, sub-same, numlef-01, numabsneg, neg-12, absls-04, abs-sub-02, sub-shift, lepr, neg-06, absone, abs-11, le-add-05, zero-not, abs-add, abs-05, abs-ls-04, sub-add-04, absneg-02, neg-03, abs-17, le-add, sub-shift-second, negadd, add-rew, ple-04, add-shift, subsub, le-add-02, ple, abssub-04, le-add-08, subneg, neg-15, sub-sub, ple-01, estimate-add2-ls-left, int-simp-06, succ-02, minus-rew, minus-sub, neg-09, sub-add-01, ls-rew-succ, sub-add-07, absls-05, minus-gr, abs-two, mone-07, int-simp-03, estimate-add2-lsle-left, sub-same-01, zero-gs, abssub-01, absneg, abs-ls-02, int-simp-09, zero-ge-01, sub-ls-02, absls-02, estimate-add1-le-left, mone-04, elim-sub, num-eq-shift, add-pos-ge, absone-01, abs-21, mone-neg, ex-le-add, mone-01, neg-01, minus-three, sub-sub-04, pls-01, sub-zero-01, abs-09, num-between, abssub-02, lep-01, abs-06, abs-12, abs-succ, le-add-06, le-sub-same, int-add-pos-01, int-add-pos, sub-sub-01, estimate-add2-lsle-right, minus-neg, numadd-01, sub-eq, estimate-add1-le-right, le-add-03, neg-10, one-03, abs-18, minus-01, sub-add, sub-add-05, ler, estimate-add1-lsle-left, k-sub-rec1, sub-add-02, abssub-05, ple-02, int-add-same-pos, zero-ge, numsub, neg, int-simp-07, int-simp-04, int-simp-10, discard-add2-lels-left, abs-ls, sub-less, sub-add-08, estimate-add2-le-left, neg-add, absls-06, abs-07, lep-02, notle-pos, abs-le-succ, minus-add, absls-03, estimate-add1-ls-left, numlef, int-simp-01, abs-10, absone-02, neg-05, numle-01, abs-ls-03, estimate-add2-le-right, abs-04,
• int-basic2/add-c is used by abs-sub, rew-eqzero-01, le-add-01, sub-ls, absa, ttwo, abs-01, abseq, sub-add-09, minus-five, neg-08, neg-14, abs-neg, succ-01, pls, numlsf, sub-sub-02, numlsf-02, le-add-07, abssub-03, estimate-add1-ls-right, lep, neg-11, abs-sub-01, numls-01, negone, sub-add-06, minus-four, num-subadd, le-add-04, absls, zero-eq, numadd, int-simp-02, minus-02, minus, le-rec, sub-add-03, absneg-01, absls-01, k-sub-rec2, le-rew-succ, sub-ls-01, sub-pred, les, sub-le-01, ple-03, mone-03, int-simp-08, abs-one-01, int-simp-11, estimate-add2-ls-right, sub-minus, int-simp-05, sub-sub-03, abssub, abs-14, sub-zero, abs-08, estimate-add1-lsle-right, numle-02, sub-same, numlef-01, numabsneg, neg-12, absls-04, abs-sub-02, sub-shift, lepr, neg-06, sub-le, absone, abs-11, le-add-05, zero-not, abs-add, abs-05, abs-ls-04, sub-add-04, absneg-02, neg-03, abs-17, le-add, sub-shift-second, negadd, add-rew, ple-04, add-shift, subsub, le-add-02, ple, abssub-04, le-add-08, subneg, neg-15, sub-sub, ple-01, estimate-add2-ls-left, int-simp-06, succ-02, minus-rew, minus-sub, neg-09, sub-add-01, ls-rew-succ, sub-add-07, absls-05, numls-02, minus-gr, abs-two, mone-07, int-simp-03, estimate-add2-lsle-left, sub-same-01, zero-gs, abssub-01, absneg, abs-ls-02, int-simp-09, zero-ge-01, sub-ls-02, absls-02, estimate-add1-le-left, mone-04, elim-sub, num-eq-shift, add-pos-ge, absone-01, abs-21, mone-neg, ex-le-add, mone-01, neg-01, minus-three, sub-sub-04, abs-15, pls-01, sub-zero-01, abs-09, num-between, neg-13, abssub-02, lep-01, abs-06, abs-12, abs-succ, le-add-06, le-sub-same, int-add-pos-01, int-add-pos, sub-sub-01, estimate-add2-lsle-right, minus-neg, numadd-01, sub-eq, estimate-add1-le-right, le-add-03, neg-10, one-03, abs-18, minus-01, sub-add, sub-add-05, ler, estimate-add1-lsle-left, k-sub-rec1, sub-add-02, abssub-05, ple-02, int-add-same-pos, zero-ge, numsub, neg, int-simp-07, int-simp-04, int-simp-10, discard-add2-lels-left, abs-ls, sub-less, sub-add-08, estimate-add2-le-left, neg-add, negeq, absls-06, abs-07, lep-02, notle-pos, abs-le-succ, minus-add, absls-03, estimate-add1-ls-left, numlef, int-simp-01, abs-10, absone-02, neg-05, numle-01, abs-ls-03, estimate-add2-le-right, abs-04,
• int-basic2/add-in is used by abs-sub-01, sub-shift, sub-shift-second, subneg, sub-add-01, int-simp-03, sub-add, abssub-05, numsub, minus-add, int-simp-01,
• int-basic2/add-less is used by ple-01, succ-02, int-simp-03, int-add-same-pos, int-simp-10, discard-add2-lels-left,
• int-basic2/add-zero-rev is used by absa, sub-add-09, neg-08, sub-sub-02, absls, minus, sub-add-03, sub-pred, les, sub-minus, sub-sub-03, abssub, sub-zero, neg-12, sub-add-04, ple-01, succ-02, minus-sub, neg-09, sub-add-07, minus-gr, abs-ls-02, absls-02, absone-01, abs-21, ex-le-add, mone-01, neg-01, sub-zero-01, num-between, abssub-02, abs-06, abs-succ, neg-10, one-03, sub-add-05, ler, k-sub-rec1, sub-add-02, neg, abs-ls, sub-add-08, abs-07, neg-05, abs-04,
• int-basic2/ls is used by le-add-01, absa, le-add-07, lep, le-add-04, int-simp-08, absls-04, le-add-05, abs-ls-04, le-add-02, le-add-08, ple-01, int-simp-06, zero-gs, abs-ls-02, add-pos-ge, ex-le-add, le-add-06, le-add-03, abssub-05, zero-ge, int-simp-04, sub-less, notle-pos, absls-03, int-simp-01, abs-ls-03,
• int-basic2/ls-01 is used by abs-sub, sub-ls, sub-ls-01, int-simp-08, int-simp-11, zero-not, le-add, int-simp-06, int-simp-04, int-simp-10, absls-03,
• int-basic2/ls-02 is used by abs-neg, abs-sub-01, zero-not, lep-01, int-add-pos-01, int-add-pos, absls-03,
• int-basic2/ls-add-both is used by sub-ls, sub-ls-01, estimate-add1-lsle-right, ple-01, estimate-add2-lsle-left, pls-01, estimate-add2-lsle-right, estimate-add1-lsle-left,
• int-basic2/ls-zero is used by absls-01,
• int-basic2/lst-02 is used by pls, estimate-add1-ls-right, ple-03, estimate-add2-ls-right, zero-not, estimate-add1-le-left, estimate-add2-le-left,
• int-basic2/lst-03 is used by ple-04, estimate-add2-ls-left, estimate-add1-le-right, estimate-add1-ls-left, estimate-add2-le-right,
• int-basic2/neq-01 is used by zero-not,
• int-basic2/nls is used by ttwo, ple, ple-01, int-simp-07,
• int-basic2/not-zero-pos is used by abseq,
• int-basic2/num-between is used by le-three, mone-06, lsone,
• int-basic2/succ-01 is used by k-sub-rec2, sub-pred, abs-11, zero-not, ple-01, succ-02, ler, k-sub-rec1, int-simp-04, abs-ls, absls-03,
• int-basic2/ttwo is used by ttwo,
• int-basic2/zero is used by abs-21, abs-18,
• int-basic2/zero-01 is used by zero-gs, zero-ge-01, zero-ge, absls-06,
• int-basic2/zero-06 is used by abs-neg, zero-eq, zero-not, abs-21,
• int-basic2/zero-07 is used by abseq, neg-14,