Used simplifier rules/spec theorems by specification

Used from specification int-basic1

• int-basic1/elim-pred is used by zero, pot-dist-pos, one-02, notone, mod2-2pot-04, mod2-2pot-02, mod2-2pot, le-pos, eq-pos,
• int-basic1/forward-pos is used by two-mone, two-mod-01, two-mod, two-ls, two-leone, pot2-pos-01, pot2-ls-pred-01, pot2-est-div6, pot-zero-01, pot-square-est-02, pot-root-est, pot-nls, pot-lez, pot-div3-nls, ls-pos, exinpot, exin2pot, divmod2-2pot-neg, div-div-rec,
• int-basic1/irref is used by zero, pot2-ls-pred, pot2-est-mult8, pot-square-est-02, pot-pot-02, pot-dist-pos, one-02, notone, mod-pot-shift-pos, ls-pos, le-pos, le-2pot-01, le-2pot, eq-pos,
• int-basic1/lf-01 is used by pot-zero-01, pot-square-est-02, pot-root-est, pot-lez, notone, notneg-02, notneg, mod-ngez-01, mod-lsz, mod-lez, mod-add1-negneg, ls-mult-2pot, le-pos, grz, exinpot, exin2pot-neg, exin2pot, div2-2pot-neg, div-div-rec-01,
• int-basic1/lf-02 is used by pot-zero-01, pot-root-est, pot-nls, pot-lez, one-01, notneg-02, mod2-2pot-05, mod-lez, exinpot, exin2pot-neg, exin2pot, eq-pos, div-div-rec-01,
• int-basic1/lf-03 is used by one-01, notneg-02, eq-pos,
• int-basic1/ls-01 is used by pot2-succ-01, pot-square-est-02, pot-square-est, pot-nls, notone, notneg-02, mod2-pos, mod2-2pot-06, mod-two-ls, mod-two-ge-01, mod-ngez-01, mod-lsz, mod-lesame, mod-add1-pospos, mod-add1-negneg, minus-one-even, ls-pos-03, ls-pos, ls-mult-2pot, le-pos-01, le-pos, geom-mod, exinpot, exin2pot-neg, exin2pot, equal-minus-one, divmod2-2pot-neg, div-div-rec,
• int-basic1/lst-01 is used by exin2pot, equal-minus-one, eq-one, div2,
• int-basic1/minus-one is used by divmod2-2pot-neg,
• int-basic1/mone is used by notneg-02,
• int-basic1/numlsf is used by pot2-pos-04, pot2-ls-pred-01, pot-root-est,
• int-basic1/trans is used by pot-zero-01, pot-root-est, pot-lez, notone, notneg-02, notneg, mod-ngez-01, mod-lsz, mod-lez, mod-add1-negneg, ls-mult-2pot, le-pos, grz, exin2pot-neg, div2-2pot-neg, div-div-rec-01,

Used from specification int-mult

• int-mult/associativity is used by pot-add-min, div-div-rec,
• int-mult/commutativity is used by twopot-mone-div, pot-square-est-div6, pot-root-est, mod2-2pot, div-div-rec,
• int-mult/dist-lsplit is used by pot2-est-mult8, pot-square-est-02, pot-square-est-01, pot-root-est, pot-pot-02, pot-mod-add-zero, pot-add-min, div-div-rec,
• int-mult/dist-rsplit is used by div-div-rec,
• int-mult/dist-sub-merge is used by geom-mod,
• int-mult/dist-sub-split is used by pot-mod-add-zero,
• int-mult/eq-nonzero-01 is used by eq-pos,
• int-mult/le-pos-01 is used by le-pos,
• int-mult/ls-pos is used by pot2-est-div6,
• int-mult/ls-pos-01 is used by ls-2pot-01,
• int-mult/ls-same-01 is used by ls-2pot,
• int-mult/ls-same-04 is used by ls-mult-2pot,
• int-mult/ls-same-06 is used by ls-same,
• int-mult/minus-left is used by geom-mod, div2-2pot-neg,
• int-mult/modeqp-copied is used by le-2pot-succ,
• int-mult/modlep is used by exin2pot,
• int-mult/modlep-02 is used by exin2pot,
• int-mult/modlep-03 is used by le-2pot-01,
• int-mult/modlsp-01 is used by le-2pot-01,
• int-mult/modlsp-02 is used by le-2pot,
• int-mult/one is used by pot-square-est-02,
• int-mult/one-01 is used by div-div-rec,
• int-mult/pnle-pos is used by le-pos-01,
• int-mult/pnls-pos is used by ls-pos-02,
• int-mult/Mult-zero is used by zero-01, eq-pos, divmod2-2pot-neg, div-div-rec,
• int-mult/add-mult-two is used by sqrt-10pot, pot2-succ-01, pot2-succ, pot2-add, pot-square-est-02, pot-root-est, minus-odd, isSquare-10pot, abs-2pot,
• int-mult/associativity is used by zero-01, zero, twopot-mone-div, square-nls, square-mod-four, pred-le, pot2-succ, pot2-subls, pot2-suble, pot2-pos-05, pot2-pos-04, pot2-pos-03, pot2-pos-02, pot2-mod2-zero, pot2-ls-pred-01, pot2-le-pred, pot2-est-mult8, pot2-est-div6, pot2-div2, pot2-add, pot-sub-dist, pot-square-est-02, pot-square-est-01, pot-square-05, pot-square-04, pot-square-03, pot-square-01, pot-square, pot-root-est, pot-pot-02, pot-pot-01, pot-pot, pot-mod-zero, pot-mod-add-zero, pot-div3-nls, pot-div, pot-dist-pos, pot-add-min, one-02, one, notone, notneg, mod2-2pot-04, mod2-2pot-03, mod2-2pot-01, mod-two-ge-01, mod-same, mod-pot-shift-pos, mod-next-square, mod-add1-pospos, mod-add1-negneg, mod-2pot, minus-square-01, minus-square, minus-one-odd, minus-one-even, minus-odd, ls-same, ls-mult-2pot, le-same, le-pos, le-2pot-succ, le-2pot-01, le-2pot, geom-mod, exinpot, exin2pot-neg, exin2pot, equal-minus-one, eqone-01, eq2, eq-pos, divmod2-2pot-neg, div2-2pot-neg, div2-2pot-04, div2-2pot-03, div2-2pot-02, div2, div-twopot, div-div-rec, add-eq2pot, abs-2pot,
• int-mult/commutativity is used by zero-01, zero, twopot-mone-div, square-nls, square-mod-four, pred-le, pot2-succ, pot2-subls, pot2-suble, pot2-pos-05, pot2-pos-04, pot2-pos-03, pot2-pos-02, pot2-mod2-zero, pot2-ls-pred-01, pot2-le-pred, pot2-est-mult8, pot2-est-div6, pot2-div2, pot2-add, pot-sub-dist, pot-square-est-02, pot-square-est-01, pot-square-05, pot-square-04, pot-square-03, pot-square-01, pot-square, pot-root-est, pot-pot-02, pot-pot-01, pot-pot, pot-mod-zero, pot-mod-add-zero, pot-div3-nls, pot-div, pot-dist-pos, pot-add-min, one-02, one, notone, notneg, mod2-2pot-04, mod2-2pot-03, mod2-2pot-02, mod2-2pot-01, mod-two-ge-01, mod-same, mod-pot-shift-pos, mod-next-square, mod-add1-pospos, mod-add1-negneg, mod-2pot, minus-square-01, minus-square, minus-one-odd, minus-one-even, minus-odd, ls-same, ls-mult-2pot, ls-2pot, le-same, le-pos, le-2pot-succ, le-2pot-01, le-2pot, geom-mod, exinpot, exin2pot-neg, exin2pot, equal-minus-one, eqone-01, eq2, eq-pos, divmod2-2pot-neg, div2-2pot-neg, div2-2pot-04, div2-2pot-03, div2-2pot-02, div2-2pot-01, div2, div-twopot, div-div-rec, add-eq2pot-01, add-eq2pot, abs-2pot,
• int-mult/dist-rmerge is used by pot-square-est-02, geom-mod, div-div-rec,
• int-mult/eq-dist is used by pot2-est-div6, add-eq2pot,
• int-mult/eq-neg is used by div2-2pot-04,
• int-mult/eq-nonzero is used by pot-add-min,
• int-mult/eq-one is used by eqone-01, eq-pos,
• int-mult/eq-one-neg is used by equal-minus-one,
• int-mult/eq-pos is used by twopot-mone-div, pot2-succ, pot2-est-mult8, pot2-add, pot-square-est-02, mod-two-ge-01,
• int-mult/eq-same-02 is used by eq2,
• int-mult/eq-succ is used by pot-square-est-02, pot-square-est-01,
• int-mult/le-dist-01 is used by pot2-est-div6,
• int-mult/le-one is used by notone, le-pos,
• int-mult/le-pos is used by pot-square-est-02, pot-square-est-01, exinpot,
• int-mult/le-same-01 is used by exinpot,
• int-mult/ls-add-02 is used by pot-root-est,
• int-mult/ls-dist is used by pot2-est-div6,
• int-mult/ls-dist-03 is used by div-div-rec,
• int-mult/ls-pos is used by pot2-est-div6, pot-square-est-02, pot-div3-nls, exinpot,
• int-mult/ls-same-01 is used by exinpot, exin2pot,
• int-mult/ls-same-05 is used by notone,
• int-mult/minus-left is used by minus-square-01, minus-square, minus-odd, div2-2pot-neg,
• int-mult/minus-one-01 is used by geom-mod, div-div-rec,
• int-mult/minus-one-02 is used by pred-le, pot2-le-pred, minus-one-odd, add-eq2pot,
• int-mult/mods-ls-04 is used by le-2pot-01, le-2pot, exin2pot,
• int-mult/modzero is used by pot-root-est,
• int-mult/neq-not-zero is used by pot-pot-02, pot-add-min,
• int-mult/numeq-02 is used by pot-square-est-01,
• int-mult/numle-07 is used by pred-le,
• int-mult/numle-08 is used by pot2-suble,
• int-mult/numle-09 is used by exin2pot-neg,
• int-mult/numle-10 is used by pot-square-est-01,
• int-mult/numle-12 is used by le-same,
• int-mult/numle-13 is used by div-div-rec,
• int-mult/numls is used by pot2-est-div6,
• int-mult/numls-03 is used by pot2-est-mult8, pot-square-est-02,
• int-mult/numls-04 is used by exin2pot-neg,
• int-mult/numls-05 is used by pot-square-est-01,
• int-mult/numls-06 is used by pot-square-est-02,
• int-mult/numls-07 is used by pot2-le-pred,
• int-mult/numls-08 is used by pot2-subls, pot2-ls-pred-01,
• int-mult/numls-09 is used by exin2pot,
• int-mult/numls-10 is used by pot-square-est-01,
• int-mult/one is used by pot2-subls, pot2-suble, pot2-ls-pred-01, pot2-est-mult8, pot-square-est-01, pot-root-est, pot-pot-02, pot-dist-pos, pot-add-min, one-02, one, mod-two-ge-01, mod-pot-shift-pos, ls-same, le-same, geom-mod, exinpot, exin2pot-neg, exin2pot, divmod2-2pot-neg, div-div-rec, add-eq2pot,
• int-mult/square-eq is used by pot-square-05,
• int-mult/square-gez is used by pot-root-est,
• int-mult/succ-rmerge is used by pot2-est-div6, pot-square-est-02, mod-two-ge-01, div-div-rec,
• int-mult/zero-eq is used by zero,
• int-mult/zero-ge is used by pot2-pos-03, pot-root-est, mod-add1-pospos, minus-one-odd, minus-odd,
• int-mult/zero-ge-02 is used by pot-square-est-02, pot-root-est, pot-pot-02, mod2-2pot-04, div2-2pot-03,
• int-mult/zero-ge-add is used by pot2-est-div6, mod2-2pot-01, le-2pot-01, le-2pot, exin2pot,
• int-mult/zero-gr is used by pot2-est-div6, minus-one-even, le-2pot, exinpot, exin2pot-neg, exin2pot, div-div-rec,
• int-mult/zero-gr-03 is used by div-div-rec,
• int-mult/zero-le is used by le-pos,
• int-mult/zero-left is used by pot-sub-dist, pot-pot-02, pot-mod-add-zero,
• int-mult/zero-ls is used by pot2-pos-04, pot2-pos-03, pot2-pos-02, mod-add1-negneg, div-div-rec,
• int-mult/zero-ls-01 is used by divmod2-2pot-neg,
• int-mult/zero-ls-02 is used by notneg,
• int-mult/zero-ls-03 is used by divmod2-2pot-neg,
• int-mult/zero-neq-01 is used by abs-2pot,

Used from specification int-square

• int-square/Sqrt-def is used by pot-root-est,
• int-square/Square-def is used by square-nls, pot-root-est,
• int-square/inverse-ii is used by sqrt-10pot,
• int-square/isSquare-def is used by isSquare-10pot,
• int-square/root-elim is used by pot-root-est,
• int-square/root-le is used by pot-root-est,
• int-square/even is used by odd-square, even-square,
• int-square/square-nls is used by square-nls,
• int-square/square-not-neg-03 is used by pot-root-est,
• int-square/square-not-neg-04 is used by pot-root-est,

Used from specification nat

• nat/le-ls-simp is used by lemon2pot-02, lemon2pot-01,
• nat/lels-01 is used by lemon2pot-02, lemon2pot-01,
• nat/lez-01 is used by lemon2pot-02, lemon2pot-01,
• nat/ls-01 is used by pot-square-est-02, lemon2pot-02, lemon2pot-01,
• nat/ls-03 is used by lemon2pot-01,
• nat/pred-03 is used by pot-square-est-02,

Used from specification int-abs

• int-abs/Abs-neg is used by one-01, le-pos, equal-minus-one, div-div-rec,
• int-abs/Abs-pos is used by abs-2pot,
• int-abs/add-shift is used by pot-mod-add-zero,
• int-abs/forward-lele is used by pot-root-est,
• int-abs/forward-lels is used by pot2-est-div6,
• int-abs/forward-lsle is used by ls-mult-2pot,
• int-abs/le-add is used by pot2-est-div6,
• int-abs/le-def is used by le-pos, le-2pot-succ, exin2pot,
• int-abs/lstwo is used by div-div-rec,
• int-abs/minus-sub is used by geom-mod,
• int-abs/neg-02 is used by geom-mod,
• int-abs/numadd is used by div-div-rec,
• int-abs/rew-eqzero is used by exin2pot-neg,
• int-abs/sub-add-01 is used by divmod2-2pot-neg, div-div-rec,
• int-abs/sub-eq-01 is used by div-div-rec,
• int-abs/sub-minus is used by geom-mod,
• int-abs/sub-shift is used by div-div-rec,
• int-abs/zero-gels is used by pot2-pos-04, pot2-pos-02,
• int-abs/zero-gels-02 is used by pot2-pos-03, div-div-rec,
• int-abs/zero-gs is used by pot-square-est-02,
• int-abs/Abs-neg is used by notneg-02,
• int-abs/Abs-pos is used by equal-minus-one, div-div-rec,
• int-abs/Sub-def is used by twopot-mone-div, pot-square-est-02, pot-mod-zero, pot-add-min, mod-two-ge-01, geom-mod, exin2pot-neg, div-div-rec-01, div-div-rec, add-eq2pot,
• int-abs/abs is used by pot-square-est-02, eq-pos,
• int-abs/abs-03 is used by sqrt-10pot, isSquare-10pot, div2-2pot-neg, div-div-rec,
• int-abs/abs-06 is used by pot2-le-pred, div2-2pot-neg,
• int-abs/abs-07 is used by div-div-rec,
• int-abs/abs-08 is used by two-minus, pot2-ls-pred-01, pot-zero-01, pot-square-est-01, pot-lez, pot-add-min, ls-pos-02, grz, equal-minus-one, eq2, divmod2-2pot-neg, div2-2pot-neg, abs-2pot,
• int-abs/abs-16 is used by pot-zero-01, pot-lez, grz, exin2pot, equal-minus-one,
• int-abs/abs-18 is used by sqrt-10pot,
• int-abs/abs-neg is used by equal-minus-one,
• int-abs/absle is used by zero, pot2-est-mult8, pot-pot-02, pot-dist-pos, one-02, notone, mod-pot-shift-pos, le-pos, le-2pot-01, le-2pot, exin2pot, eq-pos,
• int-abs/anti is used by zero, twopot-mone-div, two-leone, pot2-pos-01, pot2-ls-pred-01, pot2-le-pred, pot2-est-mult8, pot2-est-div6, pot-sub-dist, pot-square-est-01, pot-pot-02, pot-dist-pos, one-02, one-01, notone, notneg-01, notneg, mod-two-ge-01, mod-pot-shift-pos, ls-pos-02, ls-pos, le-pos-01, le-pos, le-2pot-01, le-2pot, exinpot, exin2pot-neg, exin2pot, equal-minus-one, eq2, eq-pos, div-div-rec,
• int-abs/bet is used by two-ls, pot-zero-01, pot-square-est-02, pot-nls, notneg, mod-pot-shift-pos, exinpot, equal-minus-one, divmod2-2pot-neg, div-div-rec-01,
• int-abs/bet-01 is used by pot-nls,
• int-abs/elim-sub is used by twopot-mone-div, square-mod-four, pred-le, pot2-est-mult8, pot2-est-div6, pot2-div2, pot2-add, pot-sub-dist, pot-square-est-02, pot-square-est-01, pot-pot-02, pot-mod-add-zero, pot-div3-nls, pot-div, mod-two-ge-01, mod-pot-shift-pos, ls-same, ls-pos-02, ls-mult-2pot, le-same, le-pos-01, le-2pot-succ, geom-mod, equal-minus-one, divmod2-2pot, div2-2pot-03, div2-2pot-02, div2, div-twopot, add-eq2pot-01, add-eq2pot,
• int-abs/forward-le is used by pot2-est-div6, pot-square-est-div6, pot-square-est, pot-root-est, pot-div3-nls, le-pos, exinpot,
• int-abs/forward-le-01 is used by zero, twopot-mone-div, two-ls, succ, pot2-est-mult8, pot2-est-div6, pot-zero-01, pot-sub-dist, pot-square-est-div6, pot-square-est-02, pot-square-est-01, pot-square-est, pot-square-02, pot-root-est, pot-pot-03, pot-pot-02, pot-nls, pot-mod-zero, pot-mod-add-zero, pot-eq-sub, pot-div3-nls, pot-div, pot-add-min, notneg-01, notneg, mod2-pos, mod2-2pot-06, mod2-2pot-05, mod2-2pot-04, mod2-2pot-02, mod2-2pot, mod-two-ls-01, mod-two-ls, mod-two-ge-01, mod-pot-shift-pos, mod-ngez, mod-lsz, mod-lez, mod-add1-pospos, minus-square, minus-one-odd, minus-odd, ls-same, ls-pos-03, ls-pos-02, ls-pos, ls-mult-2pot, ls-2pot-01, ls-2pot, lemon2pot, le-pos-01, le-pos, le-2pot-01, le-2pot, geom-mod, exinpot, exin2pot-neg, exin2pot, equal-minus-one, divmod2-2pot-neg, div2-2pot-02, div2-2pot-01, div2-2pot, div-twopot, div-div-rec, add-eq2pot-01, add-eq2pot,
• int-abs/forward-le-02 is used by zero-02, two-minus, pot2-pos-04, pot2-pos-03, pot2-pos-02, pot2-ls-pred-01, pot2-le-pred, pot-zero-01, pot-square-est-02, pot-square-est-01, pot-root-est, pot-lez, pot-add-min, notneg, mod2-pos, mod-two-ls-01, mod-ngez-01, mod-ngez, mod-lsz, mod-add1-negneg, ls-pos-02, ls-mult-2pot, le-pos, grz, exin2pot-neg, equal-minus-one, eq2, divmod2-2pot-neg, div2-2pot-neg, div-twopot, div-div-rec-01, div-div-rec, add-eq2pot,
• int-abs/forward-le-04 is used by two-mone, two-leone, pot2-pos-01, pot2-ls-pred-01, pot2-le-pred, notneg-01, le-pos, grz, exin2pot-neg, equal-minus-one, eq2, divmod2-2pot-neg, div-div-rec,
• int-abs/forward-le-05 is used by zero, twopot-mone-div, two-mone, two-mod-01, two-mod, two-ls, two-leone, pred-le, pot2-subls, pot2-suble, pot2-pos-01, pot2-mod2-zero, pot2-ls-pred-01, pot2-est-mult8, pot2-est-div6, pot2-div2, pot-zero-01, pot-square-est-02, pot-root-est, pot-pot-02, pot-nls, pot-mod-zero, pot-mod-add-zero, pot-lez, pot-eq-sub, pot-div3-nls, pot-div, notneg-01, notneg, mod2-2pot-06, mod2-2pot-05, mod2-2pot-04, mod2-2pot-02, mod2-2pot, mod-two-ge-01, mod-same, mod-pot-shift-pos, mod-ngez-01, mod-lsz, mod-lez, mod-lesame, mod-add1-pospos, mod-add1-negneg, minus-one-odd, minus-one-even, minus-odd, ls-same, ls-pos-03, ls-pos, ls-mult-2pot, le-same, le-pos-01, le-2pot-succ, grz, geom-mod, exinpot, exin2pot-neg, exin2pot, equal-minus-one, eqone, divmod2-2pot-neg, div2-2pot-neg, div2-2pot-02, div-div-rec-01, div-div-rec,
• int-abs/forward-lele is used by twopot-mone-div, pot2-est-div6, pot-square-est-02, pot-square-est-01, pot-root-est, pot-dist-pos, notone, notneg-01, mod-two-ls-01, ls-pos-02, lemon2pot, le-pos, le-2pot-01, exinpot, exin2pot-neg, divmod2-2pot-neg, div-div-rec,
• int-abs/forward-lels is used by pot2-est-div6, pot-root-est, pot-div3-nls, pot-dist-pos, notone, notneg-02, notneg-01, mod2-2pot-01, mod-two-ls-01, mod-two-ls, mod-two-ge-01, ls-pos, le-pos, le-2pot-01, le-2pot, grz, exin2pot-neg, exin2pot, divmod2-2pot-neg, div-div-rec,
• int-abs/forward-lsle is used by two-mone, pot2-ls-pred-01, pot2-est-mult8, pot2-est-div6, pot-zero-01, pot-square-est-02, pot-root-est, pot-add-min, notneg, mod2-pos, mod2-2pot-05, mod-two-ls-01, mod-ngez, mod-lsz, mod-lez, ls-pos-02, ls-mult-2pot, lemon2pot-02, lemon2pot-01, lemon2pot, le-pos, le-2pot-succ, le-2pot-01, exinpot, exin2pot-neg, exin2pot, divmod2-2pot-neg, div-twopot, div-div-rec, add-eq2pot,
• int-abs/lels is used by zero, twopot-mone-div, two-mod-01, two-ls, pot2-pos-03, pot2-pos-01, pot2-ls-pred-01, pot2-ls-pred, pot2-le-pred, pot2-est-mult8, pot2-est-div6, pot-zero-01, pot-sub-dist, pot-square-est-02, pot-square-est-01, pot-root-est, pot-pot-02, pot-nls, pot-dist-pos, one-02, one-01, notone, notneg-01, notneg, mod2-2pot-01, mod-two-ge-01, mod-pot-shift-pos, ls-pos-03, ls-pos-02, ls-pos, ls-mult-2pot, le-pos-01, le-pos, le-2pot-01, grz, geom-mod, exinpot, exin2pot-neg, exin2pot, equal-minus-one, eq2, eq-pos, divmod2-2pot-neg, div-div-rec-01, div-div-rec, abs-2pot,
• int-abs/lels-01 is used by two-leone, sqrt-10pot, pot2-succ-01, pot2-pos-04, pot2-pos-03, pot2-pos-02, pot2-ls-pred, pot2-le-pred, pot2-est-mult8, pot2-est-div6, pot-square-est-div6, pot-square-est-02, pot-square-est-01, pot-square-est, pot-root-est, pot-nls, pot-lez, pot-div3-nls, pot-add-min, notone, notneg-02, notneg, mod2-pos, mod2-2pot-06, mod2-2pot-05, mod2-2pot-04, mod2-2pot-01, mod-two-ls-01, mod-two-ls, mod-two-ge-01, mod-ngez-01, mod-lsz, mod-lez, mod-lesame, mod-add1-pospos, mod-add1-negneg, minus-one-even, ls-pos-03, ls-pos-02, ls-pos-01, ls-pos, ls-mult-2pot, lemon2pot-02, lemon2pot-01, lemon2pot, le-pos-01, le-pos, le-2pot-succ, le-2pot-01, le-2pot, grz, exinpot, exin2pot-neg, exin2pot, equal-minus-one, divmod2-2pot-neg, div2-2pot-04, div2-2pot-03, div2, div-twopot, div-div-rec, add-eq2pot,
• int-abs/lels-02 is used by pot2-le-pred, pot-square-est-01, pot-mod-add-zero, pot-lez, notneg-01, notneg, mod2-pos, mod2-2pot-05, mod2-2pot-04, mod2-2pot-01, mod-pot-shift-pos, mod-lez, le-pos, geom-mod, exin2pot, equal-minus-one, eqone, eq-pos, eq-one, divmod2-2pot-neg,
• int-abs/lels-03 is used by two-mod-01, two-ls, pot2-pos-03, pot2-pos-01, pot-square-est-02, pot-square-est-01, pot-root-est, pot-nls, ls-pos-03, le-pos-01, le-pos, le-2pot-01, le-2pot, exinpot, exin2pot, equal-minus-one, div2, add-eq2pot,
• int-abs/lels-04 is used by pot-dist-pos, mod2-2pot-01, le-2pot-01, le-2pot, exin2pot, div2-2pot-03, div-div-rec,
• int-abs/lenls is used by two-zero, two-lez, pot2-est-mult8, pot2-est-div6, pot-square-est-01, pot-root-est, pot-mod-zero, pot-eq-sub, pot-div3-nls, pot-div, pot-add-min, mod-two-ls-01, ls-pos, lemon2pot, le-pos-01, le-pos, exin2pot, add-eq2pot,
• int-abs/leone is used by twopot-mone-div, two-mod-01, pot2-est-div6, pot-square-est-02, pot-square-est-01, notone, mod2-2pot-01, mod-two-ls-01, mod-two-ge-01, ls-pos-02, le-pos-01, le-pos, geom-mod, exinpot, eq-pos, divmod2-2pot-neg,
• int-abs/lep is used by pot-sub-dist, pot-div, add-eq2pot-01, add-eq2pot,
• int-abs/lep-01 is used by ls-mult-2pot,
• int-abs/ler is used by notneg-02, ls-pos, exinpot, exin2pot-neg,
• int-abs/les is used by le-2pot-succ,
• int-abs/lsone is used by two-mone, two-leone, pot2-pos-01, pot2-le-pred, pot-zero-01, pot-nls, le-pos, exin2pot, divmod2-2pot-neg, div-div-rec, 2pot-leone,
• int-abs/lstwo-01 is used by mod2-2pot-01,
• int-abs/minus-02 is used by geom-mod,
• int-abs/minus-add is used by minus-one-odd, div-div-rec-01, div-div-rec,
• int-abs/minus-sub is used by geom-mod, equal-minus-one, div-div-rec,
• int-abs/mone-05 is used by le-pos, divmod2-2pot-neg, div-div-rec,
• int-abs/mone-06 is used by zero, twopot-mone-div, succ, pred-le, pot2-est-mult8, pot2-est-div6, pot2-div2, pot2-add, pot-square-est-02, pot-square-est-01, pot-pot-02, pot-mod-add-zero, pot-div3-nls, notone, notneg, mod2-2pot-04, mod2-2pot-02, mod2-2pot-01, mod2-2pot, mod-two-ge-01, mod-pot-shift-pos, minus-one-odd, minus-odd, ls-same, ls-pos-02, le-same, le-pos-01, le-pos, le-2pot-succ, le-2pot-01, le-2pot, geom-mod, exin2pot, equal-minus-one, eq-pos, divmod2-2pot, div2-2pot-03, div2-2pot-02, div2,
• int-abs/mone-08 is used by pot-square-est-01, ls-pos-02, equal-minus-one, div-div-rec,
• int-abs/neg is used by zero-02, two-minus, pot2-ls-pred-01, pot2-le-pred, one-01, le-pos, exin2pot-neg, equal-minus-one, eqone-02, eq2,
• int-abs/neg-02 is used by minus-square-01, minus-square, equal-minus-one, div2-2pot-neg,
• int-abs/neg-03 is used by equal-minus-one,
• int-abs/neg-05 is used by exin2pot-neg, equal-minus-one, div2-2pot-neg,
• int-abs/neg-06 is used by one-01, notneg-02, le-pos, equal-minus-one, div-div-rec,
• int-abs/neg-07 is used by exin2pot-neg, equal-minus-one,
• int-abs/neg-10 is used by equal-minus-one,
• int-abs/neg-12 is used by div2-2pot-neg,
• int-abs/neg-13 is used by exin2pot-neg, divmod2-2pot-neg, div2-2pot-neg, div-div-rec,
• int-abs/neg-15 is used by minus-odd, geom-mod, exin2pot-neg, equal-minus-one, div2-2pot-neg, div-div-rec,
• int-abs/negeq is used by minus-one-odd, minus-odd, equal-minus-one, div-div-rec, add-eq2pot, abs-2pot,
• int-abs/negle-07 is used by two-minus, pred-le, pot-zero-01, notneg-02, exin2pot-neg,
• int-abs/negle-13 is used by exin2pot-neg, equal-minus-one,
• int-abs/numadd-01 is used by one-03, mod-two-ls-01, mod-pot-shift-pos, geom-mod, equal-minus-one, eq-pos, div2, div-div-rec, add-eq2pot,
• int-abs/numle-02 is used by pot2-pos-04, pot2-est-mult8, pot2-est-div6, pot-square-est-div6, pot-square-est-01, pot-pot-02, pot-div3-nls, ls-pos-02, le-pos-01, le-pos, exinpot, equal-minus-one, eq-pos, add-eq2pot-01,
• int-abs/numle-03 is used by pot2-est-div6, le-pos, divmod2-2pot-neg, div-div-rec,
• int-abs/numlef-01 is used by notone, notneg, mod2-2pot-01, mod-two-ge-01, le-pos, eq-pos,
• int-abs/numleledel is used by pot2-ls-pred-01, equal-minus-one,
• int-abs/numleledel-01 is used by pot2-est-mult8, pot2-est-div6, pot-square-est-div6, pot-square-est-01, pot-root-est, pot-pot-02, ls-pos-02, le-pos-01, le-pos, exinpot, exin2pot-neg, add-eq2pot-01,
• int-abs/numlelsdel is used by le-2pot-01, le-2pot,
• int-abs/numlelsdel-01 is used by pot2-ls-pred-01, pot-zero-01, pot-square-est-02, ls-pos, exinpot,
• int-abs/numls-02 is used by zero, twopot-mone-div, succ, pred-le, pot2-est-mult8, pot2-est-div6, pot2-div2, pot2-add, pot-square-est-02, pot-square-est-01, pot-pot-02, pot-mod-add-zero, pot-div3-nls, notone, mod2-2pot-04, mod2-2pot-02, mod2-2pot-01, mod2-2pot, mod-pot-shift-pos, minus-one-odd, minus-odd, ls-same, ls-pos-02, le-same, le-pos-01, le-pos, le-2pot-succ, le-2pot-01, le-2pot, geom-mod, exin2pot, equal-minus-one, eq-pos, divmod2-2pot-neg, divmod2-2pot, div2-2pot-03, div2-2pot-02, div2,
• int-abs/numls-03 is used by pot2-ls-pred-01, pot2-est-mult8, pot-zero-01, pot-square-est-02, pot-root-est, equal-minus-one, div2, div-div-rec,
• int-abs/numlsf-02 is used by notone, notneg, mod2-2pot-01, mod-two-ge-01, le-pos, eq-pos,
• int-abs/numlsledel is used by pot2-est-div6,
• int-abs/numlsledel-01 is used by pot2-est-div6, le-pos,
• int-abs/numsub is used by divmod2-2pot-neg, div-div-rec-01, div-div-rec, add-eq2pot-01,
• int-abs/sub-add is used by geom-mod, add-eq2pot-01,
• int-abs/sub-add-01 is used by geom-mod, divmod2-2pot-neg, div-div-rec,
• int-abs/sub-eq is used by twopot-mone-div, pot2-succ-01, pot2-succ, pot2-le-pred, mod-two-ls-01, mod-two-ge-01, minus-one-odd, minus-odd, geom-mod, equal-minus-one, eq2, div-div-rec, add-eq2pot,
• int-abs/sub-eq-01 is used by pot2-le-pred, geom-mod, equal-minus-one, divmod2-2pot-neg, div-div-rec-01,
• int-abs/sub-le is used by twopot-mone-div, div-div-rec,
• int-abs/sub-le-01 is used by twopot-mone-div, two-mod-01, pot2-ls-pred, pot-square-est-01, pot-mod-zero, pot-add-min, mod-two-ls-01, ls-pos-02, le-pos-01, geom-mod, exinpot, exin2pot-neg, divmod2-2pot-neg, div-div-rec,
• int-abs/sub-ls is used by two-mone, pot2-le-pred, mod-two-ls-01, exinpot, exin2pot-neg, divmod2-2pot-neg, div2-2pot-neg, div-div-rec,
• int-abs/sub-ls-01 is used by pot2-ls-pred-01, pot2-le-pred, pot-square-est-02, le-pos-01, exinpot, exin2pot-neg, divmod2-2pot-neg, div-div-rec-01,
• int-abs/sub-pred is used by twopot-mone-div, two-mone, two-mod-01, pot2-subls, pot2-suble, pot2-mod2-zero, pot2-ls-pred-01, pot2-le-pred, pot2-est-mult8, pot2-est-div6, pot-pot-02, pot-mod-add-zero, pot-div3-nls, notneg, mod-same, mod-pot-shift-pos, exin2pot-neg, equal-minus-one, eq2,
• int-abs/sub-sub is used by mod-two-ge-01,
• int-abs/sub-sub-03 is used by pot-add-min, div-div-rec,
• int-abs/sub-sub-04 is used by geom-mod, div-div-rec-01, div-div-rec,
• int-abs/subneg is used by equal-minus-one,
• int-abs/subsub is used by equal-minus-one,
• int-abs/succ-01 is used by pot2-ls-pred, pot2-le-pred-01, pot2-est-div6, le-pos, exinpot,
• int-abs/succ-02 is used by pot2-pos-05, pot2-est-div6, pot-square-est-01, pot-root-est, pot-dist-pos, one-02, notone, notneg-02, mod-two-ls-01, exinpot,
• int-abs/zero-gels is used by pot2-est-mult8,
• int-abs/zero-gels-01 is used by zero-02, two-minus, pot2-pos-04, pot2-pos-03, pot2-pos-02, pot2-ls-pred-01, pot-zero-01, pot-square-est-02, pot-root-est, pot-add-min, notneg, mod2-pos, mod-two-ls-01, mod-ngez-01, mod-ngez, mod-add1-negneg, ls-same, ls-mult-2pot, le-pos, exin2pot-neg, equal-minus-one, eqone-02, eq2, divmod2-2pot-neg, div-twopot, div-div-rec-01, div-div-rec, add-eq2pot,
• int-abs/zero-gels-03 is used by two-minus, pot2-ls-pred-01, pot2-le-pred, pot-zero-01, pot-add-min, notneg, ls-mult-2pot, le-pos, equal-minus-one, eq2, div-div-rec,
• int-abs/zero-gels-04 is used by two-ls, two-le-01, succ, pot2-pos, pot2-le-pred-01, pot2-le-pred, pot2-est-mult8, pot2-est-div6, pot-zero-01, pot-sub-dist, pot-square-est-02, pot-square-est-01, pot-square-02, pot-root-est, pot-pot-03, pot-pot-02, pot-mod-zero, pot-div, pot-add-min, notneg-01, mod2-2pot-06, mod2-2pot-02, mod2-2pot, mod-two-ls-01, mod-ngez, mod-lsz, mod-add1-pospos, minus-one-odd, minus-odd, ls-pos-03, ls-pos-02, ls-pos, ls-mult-2pot, ls-2pot-01, ls-2pot, le-same, le-pos-01, le-2pot-01, exinpot, exin2pot-neg, exin2pot, divmod2-2pot-neg, div2-2pot-01, div2-2pot, div-twopot, div-div-rec, add-eq2pot-01, add-eq2pot,
• int-abs/zero-gs is used by exin2pot,

Used from specification int-min

• int-min/Min-right is used by pot-add-min,
• int-min/even-def-mod is used by even-square,
• int-min/odd-def is used by minus-odd,
• int-min/odd-def-mod is used by odd-square,
• int-min/Min-left is used by pot-add-min,
• int-min/min-03 is used by pot-add-min,
• int-min/min-a is used by pot-add-min,
• int-min/min-c is used by pot-add-min,
• int-min/not-even-mod2 is used by even-square,

Used from specification nat-basic2

• nat-basic2/a is used by zero, pot2-est-mult8, pot-square-est-02, pot-pot-02, pot-dist-pos, one-02, notone, mod-pot-shift-pos, lemon2pot-02, lemon2pot-01, le-pos, eq-pos,
• nat-basic2/c is used by zero, pot2-est-mult8, pot-square-est-02, pot-pot-02, pot-dist-pos, one-02, notone, mod-pot-shift-pos, lemon2pot-02, lemon2pot-01, le-pos, eq-pos,
• nat-basic2/s is used by zero, pot2-est-mult8, pot-square-est-02, pot-pot-02, pot-dist-pos, one-02, notone, mod-pot-shift-pos, lemon2pot-02, lemon2pot-01, le-pos, eq-pos,

Used from specification intnat

• intnat/abs-pred is used by twopot-mone-div, pot-square-est-01, ls-pos-02, le-pos-01, geom-mod, exinpot,
• intnat/labs is used by zero, pot2-est-mult8, pot-square-est-02, pot-pot-02, pot-dist-pos, one-02, notone, mod-pot-shift-pos, le-pos, exin2pot, eq-pos,
• intnat/le is used by lemon2pot-01,
• intnat/nat2int is used by lemon2pot-02, lemon2pot-01,
• intnat/nat2int-04 is used by lemon2pot-02, lemon2pot-01,
• intnat/nat2int-08 is used by twolezero, two-zero-01,
• intnat/num-i2n-le-02 is used by pot-square-est-02,
• intnat/rax-01 is used by pot-square-est-02,
• intnat/rax-04 is used by zero, pot2-est-mult8, pot-pot-02, pot-dist-pos, one-02, notone, mod-pot-shift-pos, le-pos, eq-pos,

Used from specification nat-mult

• nat-mult/ls-02 is used by lemon2pot-02, lemon2pot-01,
• nat-mult/mult-a is used by lemon2pot-02, lemon2pot-01,
• nat-mult/mult-c is used by lemon2pot-02, lemon2pot-01,
• nat-mult/zero is used by lemon2pot-02, lemon2pot-01,
• nat-mult/zero-06 is used by lemon2pot-02, lemon2pot-01,

Used from specification int-basic2

• int-basic2/add-a is used by pot2-est-div6, div-div-rec,
• int-basic2/add-c is used by pot2-est-div6, divmod2-2pot-neg, div-div-rec,
• int-basic2/add-a is used by zero, twopot-mone-div, two-mone, two-mod-01, two-minus, succ, square-mod-four, sqrt-10pot, pred-le, pot2-succ-01, pot2-succ, pot2-subls, pot2-suble, pot2-pos-05, pot2-pos-04, pot2-ls-pred-01, pot2-ls-pred, pot2-le-pred-01, pot2-le-pred, pot2-est-mult8, pot2-est-div6, pot2-div2, pot2-add, pot-zero-01, pot-sub-dist, pot-square-est-div6, pot-square-est-02, pot-square-est-01, pot-root-est, pot-pot-02, pot-mod-zero, pot-mod-add-zero, pot-div3-nls, pot-div, pot-dist-pos, pot-add-min, one-03, one-02, notone, notneg-02, mod2-2pot-04, mod2-2pot-02, mod2-2pot-01, mod2-2pot, mod-two-ls-01, mod-two-ge-01, mod-pot-shift-pos, mod-next-square, minus-one-odd, minus-odd, ls-same, ls-pos-02, ls-mult-2pot, lemon2pot-02, le-same, le-pos-01, le-pos, le-2pot-succ, le-2pot-01, le-2pot, isSquare-10pot, geom-mod, exinpot, exin2pot-neg, exin2pot, equal-minus-one, eq2, eq-pos, divmod2-2pot-neg, divmod2-2pot, div2-2pot-neg, div2-2pot-03, div2-2pot-02, div2-2pot-01, div2-2pot, div2, div-twopot, div-div-rec-01, div-div-rec, add-eq2pot-01, add-eq2pot, abs-2pot,
• int-basic2/add-c is used by zero, twopot-mone-div, two-mone, two-mod-01, two-minus, succ, square-mod-four, sqrt-10pot, pred-le, pot2-succ-01, pot2-succ, pot2-subls, pot2-suble, pot2-pos-05, pot2-pos-04, pot2-ls-pred-01, pot2-ls-pred, pot2-le-pred-01, pot2-le-pred, pot2-est-mult8, pot2-est-div6, pot2-div2, pot2-add, pot-zero-01, pot-sub-dist, pot-square-est-div6, pot-square-est-02, pot-square-est-01, pot-root-est, pot-pot-02, pot-mod-zero, pot-mod-add-zero, pot-div3-nls, pot-div, pot-dist-pos, pot-add-min, one-03, one-02, notone, notneg-02, mod2-2pot-04, mod2-2pot-02, mod2-2pot-01, mod2-2pot, mod-two-ls-01, mod-two-ge-01, mod-pot-shift-pos, mod-next-square, minus-one-odd, minus-odd, ls-same, ls-pos-02, ls-mult-2pot, lemon2pot-02, le-same, le-pos-01, le-pos, le-2pot-succ, le-2pot-01, le-2pot, isSquare-10pot, geom-mod, exinpot, exin2pot-neg, exin2pot, equal-minus-one, eq2, eq-pos, divmod2-2pot-neg, divmod2-2pot, div2-2pot-neg, div2-2pot-03, div2-2pot-02, div2-2pot-01, div2-2pot, div2, div-twopot, div-div-rec-01, div-div-rec, add-eq2pot-01, add-eq2pot, abs-2pot,
• int-basic2/add-in is used by pot-square-est-02, pot-dist-pos, pot-add-min, mod-two-ge-01, eq-pos, div-div-rec,
• int-basic2/add-zero is used by pot2-est-div6, pot-dist-pos, notneg-02, mod2-2pot-01, le-2pot-succ, geom-mod, divmod2-2pot-neg, div-div-rec,
• int-basic2/add-zero-rev is used by two-minus, pred-le, pot-zero-01, pot-mod-zero, pot-mod-add-zero, pot-add-min, minus-odd, exin2pot-neg, div-div-rec-01, add-eq2pot-01,
• int-basic2/ls is used by pot2-le-pred, pot-dist-pos, le-2pot-succ, div-twopot, add-eq2pot,
• int-basic2/ls-01 is used by lemon2pot-02, le-2pot-01, exin2pot-neg,
• int-basic2/ls-02 is used by mod-two-ge-01, ls-mult-2pot, exin2pot-neg, div-div-rec,
• int-basic2/mone-02 is used by equal-minus-one,
• int-basic2/mone-03 is used by notneg-02,
• int-basic2/num-between is used by pot2-est-div6, ls-mult-2pot, le-2pot-01,
• int-basic2/pred is used by succ, mod2-2pot-01, minus-odd, le-2pot-01, le-2pot, exin2pot, div2-2pot-03, div2,
• int-basic2/succ-01 is used by zero, pot-zero-01, pot-square-est-02, pot-root-est, pot-lez, pot-dist-pos, one-02, notone, notneg-02, mod2-2pot-04, mod2-2pot-02, mod2-2pot, mod-ngez-01, mod-lsz, mod-add1-negneg, ls-mult-2pot, le-pos, exin2pot-neg, eq-pos, div2-2pot-neg,
• int-basic2/zero-02 is used by pot-div3-nls,

Used from specification nat-basic1

• nat-basic1/f is used by lemon2pot-01,
• nat-basic1/one-01 is used by lemon2pot-02, lemon2pot-01,

Used from specification int-div

• int-div/Div-left is used by div2-2pot-neg,
• int-div/div-add-neg is used by divmod2-2pot-neg,
• int-div/div-div-pos is used by div2-2pot-01, div2-2pot,
• int-div/div-mult-03 is used by pot-sub-dist,
• int-div/div-mult-neg is used by div-div-rec,
• int-div/div-mult-nle-est is used by pot-root-est,
• int-div/div-rec is used by equal-minus-one,
• int-div/div-two-01 is used by twopot-mone-div,
• int-div/div-zero is used by two-minus, pot-zero-01, div-twopot,
• int-div/div-zero-02 is used by equal-minus-one,
• int-div/div2-nle-01 is used by exin2pot,
• int-div/div2-odd is used by div2-2pot-03,
• int-div/ls-03 is used by pot-root-est,
• int-div/mod-add-neg is used by divmod2-2pot-neg,
• int-div/mod-add1-negneg is used by mod-add1-negneg,
• int-div/mod-add1-pospos is used by mod-add1-pospos,
• int-div/mod-les is used by mod-lesame,
• int-div/mod-neg is used by geom-mod,
• int-div/mod-ngez is used by mod-ngez-01, mod-ngez,
• int-div/mod-rew is used by mod-two-ge-01,
• int-div/mod-two-03 is used by two-mod-01,
• int-div/mod-two-04 is used by mod2-2pot-04,
• int-div/mod-twoodd is used by mod2-2pot-01,
• int-div/mod-twoodd-02 is used by mod2-2pot-02,
• int-div/mod-zero-03 is used by mod-two-ls-01, mod-two-ls,
• int-div/mod-zero-06 is used by mod-lsz,
• int-div/modex is used by pot-mod-add-zero, minus-one-even, geom-mod,
• int-div/modex-odd is used by minus-one-odd,
• int-div/modmod-law-mult is used by mod-pot-shift-pos,
• int-div/modmod-mult-03 is used by mod2-2pot,
• int-div/mult-05 is used by mod-two-ge-01,
• int-div/num-neg-01 is used by equal-minus-one,
• int-div/nummult-eq-01 is used by pot-eq-sub,
• int-div/one-03 is used by mod-pot-shift-pos,
• int-div/one-04 is used by pot2-ls-pred-01, pot2-le-pred, le-pos, eq2,
• int-div/two-mult is used by twopot-mone-div,
• int-div/abs is used by exin2pot,
• int-div/div-div-num is used by pot-root-est,
• int-div/div-elim-negpos is used by divmod2-2pot-neg, div-div-rec,
• int-div/div-elim-pos is used by mod2-2pot-01, le-2pot-01, le-2pot, exin2pot,
• int-div/div-elim-pospos is used by pot2-est-div6,
• int-div/div-eq-zero is used by pot-zero-01,
• int-div/div-ls-zero is used by divmod2-2pot-neg,
• int-div/div-mult-01 is used by twopot-mone-div, div-div-rec,
• int-div/div-mult-03 is used by pot-div, mod2-2pot-01, div2-2pot-03, div-twopot, div-div-rec,
• int-div/div-mult-le is used by pot-root-est,
• int-div/div-mult-num-01 is used by pot2-div2, div2-2pot-02, div2,
• int-div/div-mult-three-nls is used by pot-div3-nls,
• int-div/div-same is used by div-div-rec,
• int-div/div-two is used by mod2-2pot-01,
• int-div/div-two-zero-01 is used by pot-root-est,
• int-div/div2-nle is used by exin2pot,
• int-div/div2-zero is used by div2,
• int-div/even-mult is used by mod-2pot,
• int-div/lsfc-01 is used by pot-div3-nls,
• int-div/mod-ls-same-01 is used by mod2-pos, mod-lsz,
• int-div/mod-mult-02 is used by mod2-2pot-01,
• int-div/mod-mult-04 is used by pot-mod-zero, pot-mod-add-zero, mod-same, mod-add1-pospos, mod-add1-negneg, geom-mod,
• int-div/mod-neg-01 is used by equal-minus-one,
• int-div/mod-next-square is used by mod-next-square,
• int-div/mod-one is used by mod2-pos, mod-lsz,
• int-div/mod-two-02 is used by pot2-mod2-zero, div2-2pot-03,
• int-div/mod-two-06 is used by equal-minus-one,
• int-div/mod-zero-04 is used by mod-pot-shift-pos, geom-mod,
• int-div/mod-zero-09 is used by mod2-pos, mod-lsz,
• int-div/mod2-neg-odd is used by equal-minus-one,
• int-div/modmod is used by mod-pot-shift-pos,
• int-div/neg is used by equal-minus-one,
• int-div/neg-01 is used by div-div-rec,
• int-div/num-ls is used by pot-root-est, le-2pot,
• int-div/nummult-le is used by pot-square-est-01,
• int-div/nummult-le-02 is used by pot-root-est,
• int-div/nummult-ls is used by div-div-rec,
• int-div/nummult-ls-02 is used by exin2pot-neg, exin2pot,
• int-div/nummult-modle is used by pot2-est-mult8, pot2-est-div6,
• int-div/nummult-modls-01 is used by pot2-est-mult8,
• int-div/one is used by twopot-mone-div, pot2-div2, mod-two-ge-01, div2-2pot-02, div2, div-div-rec-01,
• int-div/one-01 is used by mod-pot-shift-pos,
• int-div/one-02 is used by twopot-mone-div, one-01,
• int-div/one-04 is used by equal-minus-one,
• int-div/one-neg is used by notneg-02,
• int-div/one-pos is used by pot-lez, grz,
• int-div/pos is used by pot-root-est,
• int-div/zero is used by twopot-mone-div, equal-minus-one,
• int-div/zero-03 is used by pot-square-est-div6, pot-root-est,