Used simplifier rules/spec theorems by specification

Used from specification int-basic1

• int-basic1/ls-rec is used by square-le-one,
• int-basic1/forward-pos is used by two-le-two, two-le-three, square-not-neg-05, square-le-one, square-four,
• int-basic1/irref is used by root-nls,
• int-basic1/lf-01 is used by square-not-neg-05, square-not-neg-01, root-pos, le-plus, inverse-ii,
• int-basic1/lf-02 is used by square-not-neg-03,
• int-basic1/lf-03 is used by one-01,
• int-basic1/ls-01 is used by square-not-neg-05, square-not-neg-03, square-not-neg-01, le-plus, inverse-ii,
• int-basic1/numlsf is used by square-nls, square-le-one,
• int-basic1/numlslsdel-01 is used by two-le-three, square-four,
• int-basic1/trans is used by square-not-neg-05, square-not-neg-01, root-pos, le-plus, inverse-ii,
• int-basic1/two-ls is used by square-le-one-01, square-le-one,

Used from specification int-mult

• int-mult/dist-lsplit is used by two-minus, two-identity, two-even, root-elim, euler-four-square-identity2, euler-four-square-identity,
• int-mult/dist-rmerge is used by two-even,
• int-mult/dist-rsplit is used by two-identity, euler-four-square-identity2, euler-four-square-identity,
• int-mult/dist-sub-split is used by two-minus, two-even,
• int-mult/square-ex is used by square-not-neg-05,
• int-mult/square-ls is used by two-le-two, two-le-three,
• int-mult/square-one-le is used by one-01,
• int-mult/abs-eqall is used by sqrt-mult-squares,
• int-mult/add-mult-two is used by two-plus, two-even, four-square-le-zero,
• int-mult/associativity is used by zero-i, zero-01, zero, two-pm, two-plus, two-not-neg, two-mult, two-minus, two-ls-pospos, two-ls, two-le-two, two-le-three, two-identity, two-even, square-not-neg-05, square-not-neg-04, square-not-neg-03, square-not-neg-01, square-le-one-01, square-four, sqrt-mult-squares, sqrt-isSquare, root-pos, root-nls, root-le, root-elim, one-01, one, minus, le-plus, le, isSquare-zero, isSquare-square, isSquare-pos, isSquare-one, inverse-ii, four-square-le-zero, even, euler-four-square-identity2, euler-four-square-identity, div, abs-01, abs,
• int-mult/commutativity is used by zero-i, zero-01, zero, two-pm, two-plus, two-not-neg, two-mult, two-minus, two-ls-pospos, two-ls, two-le-two, two-le-three, two-identity, two-even-01, two-even, square-not-neg-05, square-not-neg-04, square-not-neg-03, square-not-neg-01, square-le-one-01, square-four, sqrt-mult-squares, sqrt-isSquare, root-pos, root-nls, root-le, root-elim, one-01, one, minus, le-plus, le, isSquare-zero, isSquare-square, isSquare-pos, isSquare-one, inverse-ii, four-square-le-zero, even, euler-four-square-identity2, euler-four-square-identity, div, abs-01, abs,
• int-mult/dist-rsplit is used by two-plus,
• int-mult/eq-dist is used by two-minus, two-identity, two-even, root-elim, euler-four-square-identity2,
• int-mult/eq-nonzero is used by two-mult,
• int-mult/eq-pos is used by two-even,
• int-mult/eq-succ-01 is used by euler-four-square-identity,
• int-mult/minus-left is used by minus,
• int-mult/mult-gt-both is used by two-ls-pospos,
• int-mult/neq-not-zero is used by two-mult, two-even, sqrt-mult-squares,
• int-mult/numeq is used by two-pm, euler-four-square-identity2, euler-four-square-identity,
• int-mult/numeq-02 is used by two-minus, root-elim,
• int-mult/numsucc is used by four-square-le-zero,
• int-mult/odd-even is used by two-even,
• int-mult/one is used by two-minus, two-even, root-elim,
• int-mult/square-eq is used by sqrt-isSquare, isSquare-square, abs-01, abs,
• int-mult/square-gez is used by one-01, inverse-ii,
• int-mult/square-le is used by le, inverse-ii,
• int-mult/square-lez is used by two-not-neg, isSquare-pos,
• int-mult/square-lez-01 is used by zero-01, four-square-le-zero,
• int-mult/square-ls is used by two-ls-pospos, two-ls, square-not-neg-05, root-pos, root-nls, root-elim, one-01, le-plus, inverse-ii,
• int-mult/square-zero is used by two-mult, isSquare-zero,
• int-mult/zero-eq is used by zero,
• int-mult/zero-ge is used by square-not-neg-03, square-not-neg-01, root-elim,
• int-mult/zero-gr is used by square-not-neg-04, square-le-one-01,
• int-mult/zero-le is used by four-square-le-zero,
• int-mult/zero-left is used by two-pm, euler-four-square-identity2, euler-four-square-identity,
• int-mult/zero-neq-01 is used by square-not-neg-03,

Used from specification int-abs

• int-abs/abs-one-01 is used by two-le-two, two-le-three,
• int-abs/absle is used by le-plus,
• int-abs/notle-pos is used by four-square-le-zero,
• int-abs/Abs-neg is used by le-plus,
• int-abs/Sub-def is used by two-identity, two-even, root-elim,
• int-abs/abs-01 is used by sqrt-isSquare, abs,
• int-abs/abs-04 is used by sqrt-estimate, root-elim, inverse-ii,
• int-abs/abs-05 is used by root-pos,
• int-abs/abs-06 is used by two-le-two, two-le-three,
• int-abs/abs-07 is used by sqrt-mult-squares,
• int-abs/abs-16 is used by square-not-neg-05,
• int-abs/abs-17 is used by square-not-neg-05,
• int-abs/abs-18 is used by root-abs,
• int-abs/absle is used by two-ls-pospos, sqrt-estimate, le-plus, inverse-ii,
• int-abs/absls-06 is used by inverse-ii,
• int-abs/anti is used by square-not-neg-02, four-square-le-zero,
• int-abs/bet-01 is used by square-not-neg-05,
• int-abs/elim-sub is used by two-minus,
• int-abs/forward-le-01 is used by two-ls-pospos, square-not-neg-05, square-not-neg-03, square-not-neg, square-nls, square-le-one, sqrt-estimate, root-nls, root-le, root-elim, four-square-le-zero,
• int-abs/forward-le-02 is used by two-not-neg, square-not-neg-01, square-not-neg, square-nls, sqrt-estimate, isSquare-pos,
• int-abs/forward-le-04 is used by square-not-neg-03, square-not-neg-02, four-square-le-zero,
• int-abs/forward-le-05 is used by two-le-two, two-le-three, square-not-neg-05, square-not-neg-04, square-not-neg-03, square-not-neg-02, square-not-neg-01, square-nls, square-le-one-01, square-le-one, square-four, sqrt-estimate, root-nls, root-le, root-elim, four-square-le-zero,
• int-abs/forward-lele is used by root-elim, four-square-le-zero,
• int-abs/forward-lels is used by two-le-two, two-le-three, square-not-neg-05, square-not-neg-03, square-not-neg-02, square-nls, square-le-one, square-four, sqrt-estimate, root-pos, root-nls, root-le, root-elim, one-01, inverse-ii, four-square-le-zero,
• int-abs/forward-lsle is used by square-not-neg, square-nls, sqrt-estimate, root-pos, le-plus,
• int-abs/ge-def is used by positive,
• int-abs/lels is used by square-not-neg-04, square-le-one-01, square-le-one, le-plus,
• int-abs/lels-01 is used by two-le-two, two-le-three, square-not-neg-05, square-not-neg-03, square-not-neg-01, square-nls, square-le-one, sqrt-estimate, root-pos, root-le, root-abs, le-plus, isSquare-pos, four-square-le-zero,
• int-abs/lels-02 is used by square-two, square-three, square-not-neg-02, sqrt-estimate, inverse-ii,
• int-abs/lels-03 is used by square-not-neg-04, square-not-neg, square-nls, square-le-one-01, le-plus,
• int-abs/lenls is used by square-le-one,
• int-abs/lep is used by root-elim,
• int-abs/lep-01 is used by le-plus, four-square-le-zero,
• int-abs/ler is used by square-not-neg-05, root-elim, inverse-ii, four-square-le-zero,
• int-abs/lsone is used by square-two, square-three, one-01,
• int-abs/mone-06 is used by square-nls, root-pos, root-elim,
• int-abs/neg-02 is used by minus,
• int-abs/neg-06 is used by le-plus,
• int-abs/negle-13 is used by le-plus,
• int-abs/numle-02 is used by square-nls, square-le-one,
• int-abs/numlef-01 is used by root-pos,
• int-abs/numlelsdel is used by square-le-one,
• int-abs/numls-02 is used by square-le-one, root-elim,
• int-abs/numls-03 is used by inverse-ii,
• int-abs/numlsf-01 is used by one-01,
• int-abs/numlsledel is used by two-le-two, two-le-three,
• int-abs/sub-add is used by two-even,
• int-abs/sub-add-01 is used by two-minus, euler-four-square-identity2, euler-four-square-identity,
• int-abs/sub-eq is used by two-minus, two-even, euler-four-square-identity2, euler-four-square-identity,
• int-abs/sub-le is used by root-elim,
• int-abs/sub-le-01 is used by root-elim,
• int-abs/sub-ls-01 is used by root-pos,
• int-abs/sub-sub is used by two-even, euler-four-square-identity2, euler-four-square-identity,
• int-abs/succ-02 is used by square-not-neg-05, square-nls, sqrt-estimate, root-elim, inverse-ii,
• int-abs/zero-gels-01 is used by square-not-neg, sqrt-estimate,
• int-abs/zero-gels-04 is used by square-not-neg-05, square-not-neg, square-nls, square-le-one, root-nls, root-elim, four-square-le-zero,

Used from specification int-basic2

• int-basic2/add-a is used by two-pm, two-plus, two-minus, two-identity, two-even-01, two-even, square-not-neg-05, square-nls, square-le-one-01, square-le-one, square-four, sqrt-estimate, root-pos, root-nls, root-elim, le-plus, inverse-ii, four-square-le-zero, euler-four-square-identity2, euler-four-square-identity,
• int-basic2/add-c is used by two-pm, two-plus, two-minus, two-identity, two-even-01, two-even, square-not-neg-05, square-nls, square-le-one-01, square-le-one, square-four, sqrt-estimate, root-pos, root-nls, root-elim, le-plus, inverse-ii, four-square-le-zero, euler-four-square-identity2, euler-four-square-identity,
• int-basic2/add-in is used by two-pm, two-plus, two-identity, two-even, root-elim, euler-four-square-identity2, euler-four-square-identity,
• int-basic2/add-zero is used by root-elim,
• int-basic2/add-zero-rev is used by two-pm, square-not-neg-05, four-square-le-zero, euler-four-square-identity2, euler-four-square-identity,
• int-basic2/ls is used by root-pos, four-square-le-zero,
• int-basic2/ls-01 is used by le-plus, four-square-le-zero,
• int-basic2/ls-02 is used by square-not-neg-05, square-four, root-nls,
• int-basic2/num-between is used by two-le-two, two-le-three,
• int-basic2/succ-01 is used by square-not-neg-05, square-not-neg-01, square-nls, square-le-one, square-four, sqrt-estimate, root-pos, root-nls, root-elim, one-01, inverse-ii,

Used from specification int-div

• int-div/divmult is used by two-even-01,
• int-div/even-add is used by add-even,
• int-div/even-not-ex is used by two-even,
• int-div/modex is used by two-even, div,
• int-div/abs-03 is used by abs-01,
• int-div/div-mult-03 is used by div,
• int-div/div-mult-num is used by two-even,
• int-div/even-mult is used by even,
• int-div/mod-two-02 is used by two-even,
• int-div/nummult-ls is used by square-le-one-01,
• int-div/two-even is used by two-even-01,