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 square-le-one, two-le-three, square-not-neg-05, square-four, two-le-two,
• int-basic1/lf-01 is used by root-pos, le-plus, inverse-ii,
• int-basic1/ls-01 is used by square-not-neg-01, le-plus, square-not-neg-05, square-not-neg-03, inverse-ii,
• int-basic1/numlsf is used by square-le-one, square-nls,
• int-basic1/trans is used by root-pos, le-plus, inverse-ii,
• int-basic1/two-ls is used by square-le-one, square-le-one-01,

Used from specification int-mult

• int-mult/dist-lsplit is used by even, root-elim, euler-four-square-identity, two-identity, two-even, euler-four-square-identity2,
• int-mult/dist-rmerge is used by two-even,
• int-mult/dist-rsplit is used by euler-four-square-identity, two-identity, euler-four-square-identity2,
• int-mult/dist-sub-split is used by two-even,
• int-mult/one is used by even,
• int-mult/square-ex is used by square-not-neg-05,
• int-mult/square-ls is used by two-le-three, two-le-two,
• int-mult/square-one-le is used by one-01,
• int-mult/add-mult-two is used by two-plus, four-square-le-zero, two-even,
• int-mult/associativity is used by zero, root-pos, abs-01, square-not-neg-01, even, root-elim, two-mult, minus, one-01, square-not-neg-04, positive, abs, le, zero-01, two-pm, two-plus, two-ls-pospos, le-plus, square-not-neg-05, two-not-neg, euler-four-square-identity, square-le-one-01, root-le, four-square-le-zero, two-identity, square-not-neg-03, inverse-ii, two-even, two-ls, euler-four-square-identity2, two-minus, div,
• int-mult/commutativity is used by zero, root-pos, abs-01, square-not-neg-01, even, root-elim, two-mult, minus, one-01, square-not-neg-04, positive, abs, le, zero-01, two-pm, two-plus, two-ls-pospos, le-plus, square-not-neg-05, two-not-neg, euler-four-square-identity, square-le-one-01, root-le, four-square-le-zero, two-identity, square-not-neg-03, inverse-ii, two-even, two-ls, euler-four-square-identity2, two-minus, two-even-01, div,
• int-mult/dist-rsplit is used by two-plus,
• int-mult/dist-sub-split is used by two-minus,
• int-mult/eq-dist is used by even, root-elim, euler-four-square-identity, two-even,
• int-mult/eq-nonzero is used by two-mult,
• int-mult/eq-pos is used by two-even,
• 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,
• int-mult/numeq-02 is used by root-elim,
• int-mult/numsub is used by two-minus,
• int-mult/odd-even is used by two-even,
• int-mult/one is used by root-elim, two-even, two-minus,
• int-mult/square-eq is used by 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 positive, two-not-neg,
• int-mult/square-lez-01 is used by zero-01, four-square-le-zero,
• int-mult/square-ls is used by root-pos, root-elim, one-01, two-ls-pospos, le-plus, square-not-neg-05, inverse-ii, two-ls,
• int-mult/square-zero is used by two-mult,
• int-mult/two-zero is used by square-not-neg-03,
• int-mult/zero-eq is used by zero,
• int-mult/zero-ge is used by square-not-neg-01, root-elim, square-not-neg-03,
• 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,

Used from specification int-abs

• int-abs/abs-one-01 is used by two-le-three, two-le-two,
• 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 root-elim, two-identity, two-even,
• int-abs/abs-01 is used by abs,
• int-abs/abs-04 is used by root-elim, inverse-ii,
• int-abs/abs-05 is used by root-pos,
• int-abs/abs-06 is used by two-le-three, two-le-two,
• 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, 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/forward-le-01 is used by square-le-one, square-not-neg, root-elim, root-nls, two-ls-pospos, square-not-neg-05, root-le, square-nls, four-square-le-zero,
• int-abs/forward-le-02 is used by square-not-neg-01, square-not-neg, two-not-neg, square-nls,
• int-abs/forward-le-04 is used by square-not-neg-02, four-square-le-zero, square-not-neg-03,
• int-abs/forward-le-05 is used by square-not-neg-01, square-le-one, root-elim, square-not-neg-04, root-nls, two-le-three, square-not-neg-02, square-not-neg-05, square-le-one-01, root-le, square-nls, square-four, four-square-le-zero, square-not-neg-03, two-le-two,
• int-abs/forward-lele is used by root-elim, four-square-le-zero,
• int-abs/forward-lels is used by root-pos, square-le-one, root-elim, one-01, root-nls, square-not-neg-02, square-not-neg-05, root-le, square-nls, square-four, four-square-le-zero, square-not-neg-03, inverse-ii,
• int-abs/forward-lsle is used by root-pos, square-not-neg, root-abs, le-plus, square-nls,
• int-abs/ge-def is used by positive,
• int-abs/le-def is used by root-pos, square-not-neg-01, square-le-one, root-abs, two-le-three, le-plus, square-not-neg-05, root-le, square-nls, four-square-le-zero, square-not-neg-03, two-le-two,
• int-abs/lels is used by square-le-one, le-plus,
• int-abs/lels-02 is used by square-three, square-not-neg-02, square-two, inverse-ii,
• int-abs/lels-03 is used by square-not-neg, root-abs, le-plus, square-nls,
• int-abs/lenls is used by square-le-one, root-nls,
• 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 root-elim, square-not-neg-05, four-square-le-zero, inverse-ii,
• int-abs/lsone is used by square-three, square-two,
• int-abs/mone-06 is used by root-pos, root-elim, square-nls,
• 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-le-one, square-nls,
• 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-three, two-le-two,
• int-abs/sub-add is used by two-even, two-minus,
• int-abs/sub-add-01 is used by euler-four-square-identity, euler-four-square-identity2, two-minus,
• int-abs/sub-eq is used by euler-four-square-identity, two-even, euler-four-square-identity2, two-minus,
• 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 euler-four-square-identity, two-even, euler-four-square-identity2,
• int-abs/sub-sub-04 is used by two-minus,
• int-abs/succ-02 is used by root-elim, square-not-neg-05, square-nls, inverse-ii,
• int-abs/zero-gels-01 is used by square-not-neg, square-nls,
• int-abs/zero-gels-04 is used by square-le-one, square-not-neg, root-elim, root-nls, square-not-neg-05, square-nls, four-square-le-zero,

Used from specification int-basic2

• int-basic2/add-a is used by euler-four-square-identity2,
• int-basic2/add-c is used by euler-four-square-identity2,
• int-basic2/add-in is used by euler-four-square-identity2,
• int-basic2/add-a is used by root-pos, even, square-le-one, root-elim, two-pm, two-plus, le-plus, square-not-neg-05, euler-four-square-identity, square-nls, four-square-le-zero, two-identity, inverse-ii, two-even, euler-four-square-identity2, two-minus, two-even-01,
• int-basic2/add-c is used by root-pos, even, square-le-one, root-elim, two-pm, two-plus, le-plus, square-not-neg-05, euler-four-square-identity, square-nls, four-square-le-zero, two-identity, inverse-ii, two-even, euler-four-square-identity2, two-minus, two-even-01,
• int-basic2/add-in is used by even, root-elim, two-pm, two-plus, euler-four-square-identity, two-identity, two-even, euler-four-square-identity2, two-minus,
• int-basic2/add-zero is used by root-elim, four-square-le-zero,
• 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/num-between is used by two-le-three, two-le-two,
• int-basic2/succ-01 is used by root-pos, square-le-one, root-elim, one-01, root-nls, square-not-neg-05, square-nls, square-four, 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 even, two-even,
• int-div/modex is used by even, 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-not is used by even,
• int-div/mod-two-02 is used by two-even,
• int-div/mod-zero-num is used by even,
• int-div/nummult-ls is used by square-le-one-01,
• int-div/two-even is used by two-even-01,