Used simplifier rules/spec theorems by specification

Used from specification int-basic1

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

Used from specification int-basic2

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