Used simplifier rules/spec theorems by specification

Used from specification int-basic2

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

Used from specification int-basic1

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