Used simplifier rules/spec theorems by specification

Used from specification real-basic

• real-basic/add-assoc is used by le-add-08, le-add-06,
• real-basic/add-comm is used by le-add-07, le-add-06,
• real-basic/eqint-add is used by lenum-addboth2, lenum-addboth1, lenum-add4, lenum-add3, lenum-add2, lenum-add1,
• real-basic/ex-ls-add is used by ple-01, lsls-add-notge, lels-add-notgr, lels-add-notge, lels-add-noteq, le-add-08, le-add-07, le-add-06, le-add-05, le-add-04,
• real-basic/add-assoc is used by zero-not, zero-gs, zero-ge-01, zero-ge, zero-eq, ttwo, sub-le-01, sub-le, real-simp-11, real-add-same-pos, real-add-pos-01, real-add-pos, pls-01, pls, ple-04, ple-03, ple-02, ple-01, ple, notle-pos, not-mtwo, not-mone, mone-neg, lsls-add-notge, lsle-add-notgr, lsle-add-notge, lsle-add-noteq, lep-02, lep-01, lep, lenum-addboth2, lenum-addboth1, lenum-add4, lenum-add3, lenum-add2, lenum-add1, lels-add-notgr, lels-add-notge, lels-add-noteq, lele-add-notgr, le-add-08, le-add-07, le-add-06, le-add-05, le-add-04, le-add-03, le-add, 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, discard-add2-lels-left, abssub-04, abssub-02, abssub-01, abssub, absp-01, absp, absneg-01, absls-06, absls-05, absls-04, absls-03, absls-02, absls-01, abseq, absa, abs-two, abs-sub, abs-one, abs-neg, abs-ls-04, abs-ls-03, abs-ls-02, abs-ls-01, abs-ls, abs-le-succ, abs-add, abs-21, abs-18, abs-17, abs-12, abs-10, abs-09, abs-04, abs,
• real-basic/add-comm is used by zero-not, zero-gs, zero-ge-01, zero-ge, zero-eq, ttwo, sub-le-01, sub-le, real-simp-11, real-add-same-pos, real-add-pos-01, real-add-pos, pls-01, pls, ple-04, ple-03, ple-02, ple-01, ple, notle-pos, not-mtwo, not-mone, negle-13, mone-neg, lsls-add-notge, lsle-add-notgr, lsle-add-notge, lsle-add-noteq, lep-02, lep-01, lep, lenum-addboth2, lenum-addboth1, lenum-add4, lenum-add3, lenum-add2, lenum-add1, lels-add-notgr, lels-add-notge, lels-add-noteq, lele-add-notgr, le-add-08, le-add-07, le-add-06, le-add-05, le-add-04, le-add-03, le-add, 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, discard-add2-lels-left, abssub-04, abssub-02, abssub-01, abssub, absp-01, absp, absneg-01, absls-06, absls-05, absls-04, absls-03, absls-02, absls-01, abseq, absa, abs-two, abs-sub, abs-one, abs-neg, abs-ls-04, abs-ls-03, abs-ls-02, abs-ls-01, abs-ls, abs-le-succ, abs-add, abs-21, abs-18, abs-17, abs-12, abs-10, abs-09, abs-04, abs,
• real-basic/add-in is used by lels-add-noteq, abs-09,
• real-basic/add-less is used by zero-not, real-add-same-pos, ple-01, lenum-add2, lels-add-notge, lels-add-noteq, discard-add2-lels-left,
• real-basic/add-zero is used by ex-le-add, abssub-04, abssub-02, abssub-01, abssub, absp-01, absls-02, absa, abs-sub, abs-ls-02, abs-le-succ, abs-21,
• real-basic/bls-01 is used by lsls-add-notge, lels-add-notgr, lels-02, abssub-02, absls-05, absls-02, absls, abs-neg, abs-ls-04, abs-17, abs-16, abs-06,
• real-basic/blst is used by zero-gels-03, zero-gels-02, zero-gels, absls-02,
• real-basic/blst-01 is used by lels-02, antr, absp-01, abseq, abs-ls-02, abs-06,
• real-basic/blst-02 is used by absls-05, absls-02, absa, abs-le-succ,
• real-basic/double-neg is used by absls-05, absls-04, abs-neg, abs-ls-03,
• real-basic/eqint-add is used by zero-eq, not-mtwo, absa, abs-two, abs-one,
• real-basic/eqint-num is used by zero-eq, abseq, absa, abs-one, abs-mone, abs-add, abs-21, abs-07, abs-02,
• real-basic/forward-any-lsle is used by zero-not, zero-gs, zero-gels-04, zero-gels-01, zero-ge, transrew-01, transrew, real-simp-11, real-add-pos-01, real-add-pos, pls-01, notle-pos, not-mtwo, not-mone, lels-add-notgr, le-add-08, le-add-03, 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, absp-01, absp, absls-04, absls-03, absls, abs-neg, abs-ls-04, abs-ls-02, abs-ls-01, abs-ls, abs-le-succ, abs-19, abs-15, abs-14, abs-06, abs-04,
• real-basic/irref is used by ler, absp-01, absls-06, absls-01, abs-sub, abs-ls-02,
• real-basic/less-add-cancel-l is used by zero-not, real-simp-11, pls-01, ple-01, not-mtwo, not-mone, lsls-add-notge, lenum-addboth2, lenum-addboth1, lenum-add4, lenum-add1, lels-add-notgr, lels-add-notge, le-add, estimate-add2-lsle-right, estimate-add2-lsle-left, estimate-add1-lsle-right, estimate-add1-lsle-left, abs-le-succ,
• real-basic/lf-02 is used by zero-not, not-mtwo, not-mone, absls-02, absa,
• real-basic/lf-03 is used by zero-not, absls-02,
• real-basic/lf-04 is used by zero-not, zero-gs, zero-gels-04, zero-gels-01, zero-ge, transrew-01, transrew, real-simp-11, real-add-pos-01, real-add-pos, pls-01, notle-pos, lsls-add-notge, le-add-08, le-add-07, le-add-06, le-add-05, le-add-04, le-add-03, 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, absp-01, absp, absls-05, absls-04, absls, abs-neg, abs-ls-02, abs-ls-01, abs-ls, abs-15, abs-14, abs-10, abs-09, abs-06,
• real-basic/lf-08 is used by zero-not, zero-gels-04, zero-gels-01, transrew-01, transrew, real-add-pos-01, real-add-pos, pls-01, ple-01, lels-add-notge, le-add-08, le-add-07, le-add-06, le-add-05, le-add-04, 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, absp-01, absls-05, absa, abs-ls-02, abs-le-succ, abs-10,
• real-basic/ls is used by zero-not, zero-gs, zero-ge, notle-pos, not-mtwo, not-mone, lsls-add-notge, lep, lenum-add3, lels-add-notgr, le-add-08, le-add-07, le-add-06, le-add-05, le-add-04, le-add-03, ex-le-add, abssub-01, absls-04, absls-03, absa, abs-sub, abs-ls-04, abs-ls-03, abs-le-succ, abs-17, abs-04,
• real-basic/ls-02 is used by zero-not, real-add-pos-01, real-add-pos, not-mtwo, not-mone, lep-01, lenum-add2, le-add-08, le-add-07, le-add-06, le-add-05, le-add-04, absp-01, absls-05, abs-ls-02, abs-le-succ, abs-10,
• real-basic/ls-num is used by zero-not, not-mtwo, not-mone, le-num, betweenlsle-zero-one, betweenlels-zero-one, abssub-01, absls-05, absls-04, absls-03, abs-zero, abs-two, abs-one, abs-le-succ, abs-17, abs-10, abs-09, abs-06, abs-04, abs,
• real-basic/ls-zero is used by absls-01, abs-le-succ,
• real-basic/lst-01 is used by zero-not,
• real-basic/lst-02 is used by zero-not, pls, ple-03, estimate-add2-ls-right, estimate-add2-le-left, estimate-add1-ls-right, estimate-add1-le-left,
• real-basic/lst-03 is used by ple-04, estimate-add2-ls-left, estimate-add2-le-right, estimate-add1-ls-left, estimate-add1-le-right,
• real-basic/lst-04 is used by zero-not,
• real-basic/mone-02 is used by not-mtwo,
• real-basic/mone-03 is used by not-mone, abs-le-succ,
• real-basic/neg-02 is used by absls-02, abs-le-succ, abs-06,
• real-basic/neg-05 is used by minus-gr, absls, abs-neg,
• real-basic/neg-08 is used by ex-le-add, absp-01, absls-05, absls-04, abs-sub, abs-ls-03, abs-ls-02,
• real-basic/neg-09 is used by absls-02, abs-ls,
• real-basic/neg-10 is used by abs-07,
• real-basic/neg-12 is used by absneg-02, abs-01,
• real-basic/neg-add is used by absls-05, absls-04, absa, abs-ls-03, abs-le-succ,
• real-basic/negadd-eq is used by not-mtwo,
• real-basic/negeq is used by not-mone, absneg-01, absa, abs-one, abs-neg, abs-21, abs-18, abs,
• real-basic/negl-ls is used by zero-not, negle-07, absls-02, absls-01, abs-ls-04, abs-ls, abs-le-succ, abs-15, abs-14, abs-10,
• real-basic/negladd-ls is used by sub-le-01, absp-01, absls-05, abs-ls-02,
• real-basic/negr-ls is used by zero-not, negle-13, absls-06, absls-03, abs-le-succ,
• real-basic/negradd-ls is used by sub-le, absls-05, absls-04, abs-ls-03, abs-le-succ,
• real-basic/neq-01 is used by zero-not,
• real-basic/nls is used by ttwo, ple, lele-add-notgr,
• real-basic/not-zero-pos is used by abseq,
• real-basic/sub-eq is used by absp-01, absa, abs-ls-02, abs-21,
• real-basic/sub-eq-01 is used by ex-le-add, abssub-04, absp-01, absls-05, abseq, absa, abs-sub, abs-ls-02, abs-le-succ, abs-add, abs-21,
• real-basic/trans is used by zero-not, le-add-08, abssub-01, absp, absls-05, absls-02, abs-sub, abs-ls-01, abs-ls, abs-17, abs-15, abs-14, abs-11, abs-10, abs,
• real-basic/ttwo is used by ttwo,
• real-basic/zero is used by abs-21, abs-18, abs,
• real-basic/zero-01 is used by zero-gs, zero-ge-01, zero-ge, absls-06,
• real-basic/zero-02 is used by le-add-08, le-add-07,
• real-basic/zero-03 is used by le-add-06, le-add-05, le-add-04,
• real-basic/zero-06 is used by zero-not, zero-eq, abs-21,
• real-basic/zero-07 is used by abseq,

Used from specification int-basic2

• int-basic2/add-a is used by zero-eq, not-mtwo, lenum-addboth2, lenum-addboth1, lenum-add4, lenum-add3, lenum-add2, lenum-add1, absa, abs-two, abs-one,
• int-basic2/add-c is used by zero-eq, not-mtwo, lenum-addboth2, lenum-addboth1, lenum-add4, lenum-add3, lenum-add2, lenum-add1, absa, abs-two, abs-one,
• int-basic2/ls-02 is used by lenum-addboth2, lenum-addboth1, lenum-add4, lenum-add3, lenum-add2, lenum-add1,

Used from specification int-abs

• int-abs/bet-01 is used by betweenlele-zero-one,
• int-abs/elim-sub is used by lenum-addboth2, lenum-addboth1, lenum-add4, lenum-add3, lenum-add2, lenum-add1,
• int-abs/forward-le-01 is used by betweenlele-zero-one,
• int-abs/forward-le-05 is used by lenum-addboth2, lenum-addboth1, lenum-add4, lenum-add3, lenum-add2, lenum-add1, betweenlele-zero-one,
• int-abs/le-def is used by le-num, betweenlele-zero-one,
• int-abs/lels-02 is used by betweenlsle-zero-one, betweenlels-zero-one, betweenlele-zero-one,
• int-abs/lels-03 is used by betweenlels-zero-one,
• int-abs/lenls is used by le-num, betweenlsle-zero-one,
• int-abs/lsone is used by betweenlsle-zero-one, betweenlels-zero-one,
• int-abs/zero-gels-04 is used by betweenlele-zero-one,