Used simplifier rules/spec theorems by specification

Used from specification int-basic2

• int-basic2/add-c is used by square-le-04, square-ls-04,
• int-basic2/ex-oddeven is used by ex-two,
• int-basic2/lst-03 is used by square-ls-04,
• int-basic2/succ-01 is used by succ-rsplit,
• int-basic2/add-a is used by zero-ls-sub, numlsneg-03, numlsneg-02, numlsneg-01, ls-add, ls-same-06, abs-ls, numleneg-03, numleneg-02, numleneg-01, pls-neg, modlsp, numls, dist-lsplit, exdivmodpos, ls-pos, numleneg, mods-ls-04, modlep, mods-nls, square-even, modzero-06, two-le-04, modzero-05, two-le-03, eq-one-neg, two-le-02, modzero-07, two-le-01, modzero-02, modzero-01, modzero-04, modzero-03, numabs, square-le-06, square-le-05, square-le-04, mods-zero-07, square-le-03, square-le-02, eq-one, le-dist, minus-one-01, modeqp, mod-neq, numeq-03, numeq-04, numeq-01, numeq-02, modlep-04, modneqp, eq-succ-01, numle, modlep-01, modlep-02, ex-two, modlep-03, square-ex, numle-12, mult-sub-lesseq, numle-13, exdivmod, abs-ls-same-01, zero-left, odd-even, numle-01, numle-06, numle-07, three, numle-08, numle-09, numle-02, square-eq, numle-03, numle-04, numle-05, ls-add-02, ls-add-03, zero-ge-add, le-dist-02, le-dist-01, succ-rmerge, numeq, square-eq-01, square-interval, noeth-zero-ls, square-eq-02, minus-one, numdist, zero-gr-add-02, zero-gr-add-01, add-mult-two, pred-rmerge, commutativity, modeqp-02, modeqp-01, modeqp-03, numlsneg, auxexdivmod-01, zero-gr, auxexdivmod, ls-dist-02, ls-dist-01, ls-dist-06, square-zero-02, ls-dist-05, square-zero-01, ls-dist-04, ls-dist-03, mult-add-greater, two-sub, numsub, two-mone, associativity, eq-succ, square-inject, modeqp-neg, modlsp-01, modlsp-06, modlsp-05, modlsp-04, modlsp-03, modlsp-02, dist-sub-merge, eq-dist, numls-08, numls-09, one, numls-06, dist-rmerge, numls-07, numls-04, numls-05, numls-02, numls-03, numls-01, ls-sub, abs-eqall, numls-13, two-sub-01, numls-12, succ-lsplit, two-ls-04, numabs-01, two-ls-03, two-ls-02, two-ls-01, dist-sub-split, square-gez-02, square-gez-01, zero-gr-add, ls-dist, dist-rsplit, two-le, two-pred, mod-nls, square-ls-01, two-ls, mod-nle, square-ls-02, square-ls-03, square-ls-04, mult-sub-less, zero-ge-add-01, le-two, numsucc,
• int-basic2/add-c is used by zero-ls-sub, numlsneg-03, numlsneg-02, numlsneg-01, ls-add, ls-same-06, abs-ls, numleneg-03, numleneg-02, numleneg-01, pls-neg, modlsp, numls, dist-lsplit, exdivmodpos, ls-pos, numleneg, mods-ls-04, modlep, mods-nls, square-even, modzero-06, two-le-04, modzero-05, two-le-03, eq-one-neg, two-le-02, modzero-07, two-le-01, modzero-02, modzero-01, modzero-04, modzero-03, numabs, square-le-06, square-le-05, square-le-04, mods-zero-07, square-le-03, square-le-02, eq-one, le-dist, minus-one-01, modeqp, mod-neq, numeq-03, numeq-04, numeq-01, numeq-02, modlep-04, modneqp, eq-succ-01, numle, modlep-01, modlep-02, ex-two, modlep-03, square-ex, numle-12, mult-sub-lesseq, numle-13, exdivmod, abs-ls-same-01, zero-left, odd-even, numle-01, numle-06, numle-07, three, numle-08, numle-09, numle-02, square-eq, numle-03, numle-04, numle-05, ls-add-02, ls-add-03, zero-ge-add, le-dist-02, le-dist-01, succ-rmerge, numeq, square-eq-01, square-interval, noeth-zero-ls, square-eq-02, minus-one, numdist, zero-gr-add-02, zero-gr-add-01, add-mult-two, pred-rmerge, commutativity, modeqp-02, modeqp-01, modeqp-03, two-oddeq, numlsneg, auxexdivmod-01, zero-gr, auxexdivmod, ls-dist-02, ls-dist-01, ls-dist-06, square-zero-02, ls-dist-05, square-zero-01, ls-dist-04, ls-dist-03, mult-add-greater, two-sub, numsub, two-mone, associativity, eq-succ, square-inject, modeqp-neg, modlsp-01, modlsp-06, modlsp-05, modlsp-04, modlsp-03, modlsp-02, dist-sub-merge, eq-dist, numls-08, numls-09, one, numls-06, dist-rmerge, numls-07, numls-04, numls-05, numls-02, numls-03, numls-01, ls-sub, abs-eqall, numls-13, two-sub-01, numls-12, succ-lsplit, two-ls-04, numabs-01, two-ls-03, two-ls-02, two-ls-01, dist-sub-split, square-gez-02, square-gez-01, zero-gr-add, ls-dist, dist-rsplit, two-le, two-pred, mod-nls, square-ls-01, two-ls, mod-nle, square-ls-02, square-ls-03, square-ls-04, mult-sub-less, zero-ge-add-01, le-two, numsucc,
• int-basic2/add-in is used by dist-lsplit, mods-nls, square-le-05, modeqp, numeq-03, eq-succ-01, ex-two, succ-rmerge, numeq, square-eq-02, zero-gr-add-02, pred-rmerge, commutativity, modeqp-01, two-sub, numsub, associativity, eq-succ, square-inject, dist-sub-merge, eq-dist, dist-rmerge, two-sub-01, succ-lsplit, dist-sub-split, dist-rsplit, two-pred, mod-nle, square-ls-03,
• int-basic2/add-less is used by mod-neq,
• int-basic2/add-pred is used by succ-lsplit, dist-rsplit,
• int-basic2/add-zero is used by zero-ls-sub, numlsneg-03, numlsneg-02, numlsneg-01, numleneg-03, numleneg-02, numleneg-01, exdivmodpos, numleneg, modlep, square-even, modzero-06, modzero-07, modzero-02, modzero-01, modzero-03, numabs, modeqp, modlep-03, exdivmod, zero-left, noeth-zero-ls, zero-gr-add-02, modeqp-03, numlsneg, auxexdivmod-01, two-mone, modeqp-neg, modlsp-06, modlsp-03, one, numls-07, dist-rsplit, mod-nls, mod-nle,
• int-basic2/add-zero-rev is used by ls-pos, mod-neq, modlep-04, square-ex, exdivmod, numle-07, three, zero-ge-add, modeqp-01, auxexdivmod, abs-eqall,
• int-basic2/eq is used by modeqp, numeq-04, ex-two, modlep-03, modlsp-03,
• int-basic2/ls is used by ls-add, ls-same-06, mods-ls-04, square-le-03, square-le-02, mod-neq, modlep-03, mult-sub-lesseq, exdivmod, abs-ls-same-01, zero-ge-add, square-interval, noeth-zero-ls, modeqp-01, auxexdivmod, square-zero-01, ls-dist-03, mult-add-greater, modlsp-03, numls-13, numabs-01, square-gez-02, square-ls-01, zero-ge-add-01,
• int-basic2/ls-01 is used by ls-pos, modzero-02, modzero-01, modzero-03, square-le-04, mod-neq, modlep-04, modneqp, modlep-01, modlep-03, ls-add-02, ls-add-03, zero-ge-add, square-eq-01, square-interval, zero-gr-add-02, modeqp-01, auxexdivmod, ls-dist-02, ls-dist-01, square-inject, modlsp-01, modlsp-03, numls-08, numls-04, numls-05, numls-02, numls-03, numls-01, two-ls-04, two-ls-03, two-ls-02, two-ls-01, ls-dist, two-ls, square-ls-02,
• int-basic2/ls-02 is used by ls-add, numls, modzero-05, modzero-04, modlep-04, modlep-03, exdivmod, abs-ls-same-01, square-interval, zero-gr-add-01, modeqp-01, ls-dist-04, modlsp-03, numls-09, ls-sub, numls-12,
• int-basic2/lst-01 is used by modlsp,
• int-basic2/lst-04 is used by modzero-05, modzero-04,
• int-basic2/mone-03 is used by modzero-05, modzero-04, minus-one,
• int-basic2/neq is used by numls-07,
• int-basic2/num-between is used by mods-nls,
• int-basic2/pred is used by dist-rsplit,
• int-basic2/succ-01 is used by square-one-le, abs-ls, pls-neg, ls-pos, modzero, modzero-02, modzero-03, square-le-02, modeqp, mod-neq, modlep-04, modlep-03, square-ex, exdivmod, zero-left, three, zero-ge-add, noeth-zero-ls, commutativity, modeqp-01, auxexdivmod, associativity, modlsp-03, succ-lsplit, numabs-01, dist-rsplit, zero-ge-add-02,
• int-basic2/zero-01 is used by modzero-07, modlep-03, modlsp-03,
• int-basic2/zero-02 is used by square-ex,

Used from specification int-basic1

• int-basic1/lsrec is used by three,
• int-basic1/elim-pred is used by ls-pos, modeqp, zero-left, commutativity, associativity, succ-lsplit, dist-rsplit,
• int-basic1/forward-pos is used by eq-one, square-ex, short-mult-max, numls-07, ls-two-03, mod-nle,
• int-basic1/irref is used by modlep, numabs, mod-neq, modneqp, square-eq, square-eq-01, auxexdivmod-01, eq-nonzero,
• int-basic1/lf-01 is used by le-one, abs-ls, pls-neg, modzero, modzero-02, modzero-03, square-le-02, square-le-01, mod-neq, modlep-04, modlep-03, exdivmod, three, zero-ge-add, modeqp-01, modlsp-03, numabs-01, pls-pos, zero-ge-add-02,
• int-basic1/lf-02 is used by modzero-05, modzero-01, modzero-04, mod-neq, three, ple-pos, eq-same-02, zero-ge-add-02,
• int-basic1/lf-03 is used by modeqp, eq-same-03,
• int-basic1/ls-01 is used by zero-ls-sub, square-lez, zero-ge-case, zero-le-two, zero-ls-01, modzero-06, modzero-05, modzero-02, modzero-01, modzero-04, modzero-03, square-le-06, square-le-04, eq-one, pzero-ls, mod-neq, modlep-03, square-ex, mult-sub-lesseq, zero-le-case, exdivmod, abs-ls-same-01, square-eq, ple-neg, zero-gr-case, zero-ge-add, square-eq-01, noeth-zero-ls, zero-gr-add-01, ple-pos, pzero-gr, zero-gr, auxexdivmod, eq-nonzero, square-zero-02, mult-add-greater, square-lez-01, modeqp-neg, modlsp-03, square-ls, zero-ls-case, mult-gt-both, zero-gr-add, ls-two-03, ls-two-02, ls-two-01, square-ls-02, square-ls-04, zero-ge-add-02,
• int-basic1/lst is used by mods-nls,
• int-basic1/lst-01 is used by square-le-06, mod-neq, modlep-03, exdivmod, abs-ls-same-01, square-eq, square-eq-01, noeth-zero-ls, eq-nonzero, square-lez-01, modlsp-03,
• int-basic1/mone is used by square-one-le,
• int-basic1/numlsf is used by mods-zero-07,
• int-basic1/numlslsdel-01 is used by short-mult-max,
• int-basic1/pred is used by modeqp, succ-lsplit,
• int-basic1/trans is used by pls-neg, modzero, modzero-02, modzero-03, square-le-02, square-le-01, mod-neq, modlep-04, modlep-03, exdivmod, zero-ge-add, modeqp-01, modlsp-03, numabs-01, pls-pos, zero-ge-add-02,
• int-basic1/two-ls is used by three,

Used from specification int-abs

• int-abs/Abs-neg is used by mods-nls, modlep-04, abs-ls-same-01, modeqp-01, modeqp-03, square-gez-02,
• int-abs/Abs-pos is used by eq-one-neg, mod-neq, square-abs, modlep-03, square-eq, noeth-zero-ls, modlsp-03,
• int-abs/add-shift is used by minus-one,
• int-abs/anti is used by eq-one, abs-ls-same-01,
• int-abs/bet is used by three,
• int-abs/forward-lels is used by pls-neg, square-le-04, square-ls-02, pls-pos,
• int-abs/forward-lsle is used by square-le-04, square-ls-02,
• int-abs/le-def is used by le-one, pnle-neg, square-le-04, abs-ls-same-01, numle-07, le-neg, square-le, numls-07, pnle-pos,
• int-abs/lels is used by pnls-neg, eq-one, abs-ls-same-01, pnls-pos,
• int-abs/mone-02 is used by mods-zero-07,
• int-abs/neg-06 is used by minus-left,
• int-abs/neg-07 is used by mods-zero-07,
• int-abs/ple is used by square-gez-01,
• int-abs/rew-eqzero is used by square-one-le,
• int-abs/rew-eqzero-01 is used by modzero-08,
• int-abs/zero-ge-01 is used by modzero-07,
• int-abs/zero-gels-02 is used by square-le-06,
• int-abs/Abs-neg is used by modlep-03, square-eq, modlsp-06, modlsp-05, modlsp-04, modlsp-03, abs-eqneg,
• int-abs/Abs-pos is used by mods-nls, eq-one, modlep-04, abs-ls-same-01, modeqp-01, abs-eqall, square-gez-02,
• int-abs/Sub-def is used by exdivmodpos, modlep-03, square-ex, exdivmod, square-zero-02, two-sub, modlsp-03, two-sub-01, mod-nle,
• int-abs/abs-01 is used by modlep-04,
• int-abs/abs-03 is used by abs-not-neg, modlep-04, modlep-01, modlsp-01,
• int-abs/abs-05 is used by noeth-zero-ls,
• int-abs/abs-06 is used by le-abs, le-same-04, abs-ls-j-one, abs-le-one-j, abs-ls-one-j, square-le-02, modlep-03, abs-ls-same-01, square-eq, noeth-zero-ls, modlsp-03, square-ls,
• int-abs/abs-07 is used by abs-not-neg, square-eq,
• int-abs/abs-08 is used by abs-ls, eq-one-neg, eq-one, mod-neq, exdivmod, abs-ls-same-01, noeth-zero-ls, modeqp-02, modeqp-01, modeqp-03, modeqp-neg, abs-eqall,
• int-abs/abs-09 is used by noeth-zero-ls,
• int-abs/abs-16 is used by le-same-06, modzero-08, eq-one, mod-neq, modlep-03, square-ex, exdivmod, abs-ls-same-01, square-eq, noeth-zero-ls, zero-gr, abs-ls-same, modlsp-03, square-ls-02,
• int-abs/abs-17 is used by square-ex,
• int-abs/abs-18 is used by numabs, abs-ls-same-01, abs-eqall, numabs-01,
• int-abs/abs-neg is used by modzero-08, eq-one-neg, modlep-02, exdivmod, modlsp-06, modlsp-05, modlsp-04, modlsp-02,
• int-abs/abs-one-01 is used by square-one-le,
• int-abs/abs-zero is used by abs-ls-same,
• int-abs/abseq is used by abs-eqall,
• int-abs/absle is used by ls-add, mods-ls-04, mods-ls-02, square-le-04, modneqp, exdivmod, abs-ls-same-01, square-eq, square-ls-02, mods-ls,
• int-abs/absls is used by abs-not-neg, ls-pos-02, mod-neq, square-eq, noeth-zero-ls,
• int-abs/absls-01 is used by modlep-01, modlep-03, modlsp-01, modlsp-03,
• int-abs/abssub-02 is used by exdivmod,
• int-abs/anti is used by mods-ls-04, mods-nls, modzero-01, numabs, eq-one, modeqp, mod-neq, modlep-04, square-ex, exdivmod, abs-ls-same-01, numle-07, zero-ge-add, ple-pos-better, zero-gr-add-02, ple-pos, modeqp-01, modeqp-03, auxexdivmod-01, zero-gr, square-zero-02, pnls-pos, mult-gt-both, pnle-pos, le-two, zero-ge-add-02,
• int-abs/bet is used by ls-add, square-le-06, square-ex, auxexdivmod-01, mod-nle,
• int-abs/bet-01 is used by eq-one,
• int-abs/elim-sub is used by ls-same-06, numls, ls-pos, modeqp, numeq-03, numeq-04, numeq-01, numeq-02, numle, modlep-03, numle-12, numle-13, numle-01, numle-06, numle-08, numle-09, numle-02, numle-03, numle-04, numle-05, numeq, noeth-zero-ls, pred-rmerge, numsub, modlsp-03, dist-sub-merge, numls-08, numls-09, numls-06, numls-07, numls-04, numls-05, numls-02, numls-03, numls-01, ls-sub, numls-13, numls-12, dist-sub-split, two-pred, mod-nls,
• int-abs/forward-le is used by ls-add, short-mult-max, ls-two-02,
• int-abs/forward-le-01 is used by ls-add, modeqp-pos, pls-pos-01, pls-pos-02, ls-two, mods-ls-04, zero-ls-02, mods-nls, square-le-04, eq-one, modeqp, mod-neq, modneqp, square-ex, exdivmod, abs-ls-same-01, pnls-negpos, pnls-posneg, zero-ge-add, square-eq-01, square-interval, noeth-zero-ls, ple-pos-better, zero-gr-add-02, zero-gr-add-01, auxexdivmod-01, auxexdivmod, square-zero-02, square-zero-01, pnls-pos, short-mult-max, square-inject, modeqp-neg, zero-gr-02, numls-07, abs-eqall, mult-gt-both, numabs-01, est-nle, mod-nls, pnle-pos, ls-two-01, mod-nle, square-ls-02, zero-ge-add-01, zero-ge-add-02,
• int-abs/forward-le-02 is used by abs-ls, abs-not-neg, pls-neg, mods-nls, modzero-08, eq-one-neg, square-le-06, eq-one, mod-neq, modlep-04, exdivmod, abs-ls-same-01, numle-07, zero-ge-add, square-interval, noeth-zero-ls, zero-gr-add-02, zero-gr-add-01, modeqp-01, le-neg, eq-nonzero, square-zero-02, square-zero-01, modeqp-neg, numls-07, abs-eqall, numabs-01, zero-neq, mod-nls, ls-two-03, ls-two-02, ls-two-01, zero-ge-add-01, zero-ge-add-02,
• int-abs/forward-le-03 is used by square-zero-01,
• int-abs/forward-le-04 is used by ls-add, abs-ls, zero-ls-03, modzero-08, eq-one, modlep-04, exdivmod, abs-ls-same-01, pnls-negpos, numle-07, three, pnls-posneg, noeth-zero-ls, zero-gr-add-02, zero-gr-add-01, modeqp-01, pzero-gr, zero-gr, abs-ls-same, square-zero-02, square-zero-01, zero-le-03, mod-nle, zero-gr-03,
• int-abs/forward-le-05 is used by mult-pos-pos, le-pos, ls-add, modeqp-pos, ls-pos, mods-ls-04, mods-nls, modzero-08, square-le-06, square-le-04, eq-one, mod-neq, modlep-04, modneqp, square-ex, exdivmod, abs-ls-same-01, three, zero-ge-add, square-eq-01, noeth-zero-ls, zero-gr-add-02, zero-gr-add-01, zero-neq-01, ple-pos, modeqp-01, auxexdivmod-01, zero-gr, auxexdivmod, eq-nonzero, short-mult-max, modeqp-neg, numls-07, mult-gt-both, numabs-01, mod-nls, pnle-pos, ls-two-03, ls-two-02, ls-two-01, mod-nle, square-ls-02, square-ls-04, pls-pos, zero-ge-add-02,
• int-abs/forward-lele is used by ls-add, modzero-06, mods-zero-07, eq-one, modlep-03, square-ex, exdivmod, pnls-negpos, pnls-posneg, square-interval, zero-gr-add-02, zero-gr-add-01, square-zero-02, pnls-pos, short-mult-max, square-inject, modlsp-03, pnle-pos, mod-nle,
• int-abs/forward-lels is used by ls-add, le-one, pls-neg, modlsp, pls-pos-02, mods-ls-02, modlep, modzero-05, modzero-08, modzero-04, mods-eq, modeqp, mod-neq, modlep-04, modlep-03, square-ex, abs-ls-same-01, three, square-eq-01, square-interval, noeth-zero-ls, zero-gr-add-02, zero-gr-add-01, modeqp-01, zero-gr, auxexdivmod, modlsp-01, modlsp-03, mult-gt-both, est-nle, square-ls-01, mod-nle, mods-ls,
• int-abs/forward-lsle is used by ls-add, ls-same-05, le-one, ls-pos-02, pls-pos-01, modzero-06, modzero-05, modzero-02, modzero-01, modzero-04, modzero-03, numabs, mods-zero-07, square-le-03, square-le-01, mod-neq, modneqp, modlep-01, modlep-03, square-ex, exdivmod, pnls-negpos, pnls-posneg, zero-ge-add, square-interval, noeth-zero-ls, zero-gr-add-02, zero-gr-add-01, ple-pos, abs-ls-same, square-zero-02, square-zero-01, modeqp-neg, modlsp-06, modlsp-03, numls-07, numabs-01, square-gez-02, mod-nls, pls-pos, zero-ge-add-01, zero-ge-add-02,
• int-abs/le-add is used by zero-gr-add-02,
• int-abs/le-add-03 is used by square-ex,
• int-abs/le-def is used by square-one-le, le-pos, pnls-neg, ls-add, le-abs, zero-ge-case, le-one, modeqp-pos, modlsp, zero-le-two, le-same-04, abs-le-one-j, modlep, modzero-05, modzero-07, modzero-02, modzero-01, modzero-03, numabs, square-le-06, square-le-04, square-le-03, square-le-02, eq-one, square-le-01, zero-ge-01, zero-ge-02, zero-ge-03, mod-neq, modlep-04, modneqp, modlep-01, modlep-02, modlep-03, square-ex, mult-sub-lesseq, zero-le-case, exdivmod, abs-ls-same-01, pnls-negpos, numle-07, three, square-eq, pnls-posneg, ple-neg, zero-ge-add, square-interval, ple-pos-better, zero-gr-add-02, ple-pos, le-neg, auxexdivmod-01, auxexdivmod, square-zero-02, pnls-pos, square-inject, modeqp-neg, modlsp-01, modlsp-06, modlsp-05, modlsp-04, modlsp-03, modlsp-02, square-le, zero-le-02, zero-le-03, square-ls, abs-eqall, numabs-01, square-gez-02, square-gez-01, est-nle, square-gez, ls-two-03, ls-two-01, mod-nle, square-ls-02, zero-ge-add-01, le-two, zero-ge-add-02,
• int-abs/lels is used by zero-ls-sub, square-lez, ls-add, ls-same-05, zero-ge-case, le-one, abs-ls, pnle-neg, modeqp-pos, pls-neg, ls-pos-02, pls-pos-01, pls-pos-02, ls-two, mods-ls-01, zero-ls-03, mods-ls-04, zero-ls-02, mods-ls-03, zero-ls-01, mods-ls-02, mods-nls, modzero, modzero-06, modzero-05, modzero-02, modzero-01, modzero-04, modzero-03, numabs, square-le-06, square-le-04, mods-zero-07, eq-one, square-le-01, mod-neq, modlep-04, modneqp, modlep-03, square-ex, zero-le-case, exdivmod, abs-ls-same-01, numle-07, three, square-eq, zero-gr-case, square-interval, noeth-zero-ls, ple-pos-better, zero-gr-add-02, ple-pos, modeqp-01, modeqp-03, pzero-gr, auxexdivmod-01, zero-gr, auxexdivmod, abs-ls-same, square-zero-02, pnls-pos, short-mult-max, square-minus, square-inject, modeqp-neg, modlsp-01, modlsp-03, square-le, zero-gr-02, numls-07, square-ls, mult-gt-one, zero-ls-case, abs-eqall, mult-gt-both, square-gez-02, pnle-pos, square-ls-01, ls-two-02, square-ls-02, mult-sub-less, pls-pos, zero-ge-add-02, mods-ls, zero-gr-03,
• int-abs/lels-02 is used by zero-ge-case, le-one, zero-le-two, pls-pos-01, pls-pos-02, zero-ls-03, zero-ls-02, modlep, modzero-08, eq-one, zero-ge-02, zero-ge-03, mod-neq, modneqp, modlep-03, zero-le-case, abs-ls-same-01, pnls-negpos, three, pnls-posneg, zero-gr-case, square-interval, zero-gr-add-02, modeqp-01, modeqp-03, pzero-gr, square-lez-01, short-mult-max, modlsp-03, zero-gr-02, zero-le-02, zero-le-03, numls-07, zero-ls-case, abs-eqall, est-nle, pnle-pos, mod-nle, square-ls-04, zero-gr-03,
• int-abs/lels-03 is used by le-pos, le-one, pls-neg, modlsp, le-same-05, ls-two, mods-ls-01, zero-ls-02, mods-ls-03, mods-ls-02, modlep, modzero, modzero-06, modzero-07, modzero-02, modzero-01, modzero-03, square-le-02, eq-one, zero-ge-01, zero-ge-02, zero-ge-03, modlep-04, modneqp, exdivmod, abs-ls-same-01, zero-ge-add, square-interval, noeth-zero-ls, zero-gr-add-02, modeqp-03, le-neg, short-mult-max, modlsp-06, modlsp-05, modlsp-04, modlsp-03, square-le, zero-gr-02, zero-le-02, zero-le-03, square-ls, mult-gt-one, mult-gt-both, square-gez-02, square-gez-01, pnle-pos, square-ls-02, mult-sub-less, pls-pos, mods-ls, zero-gr-03,
• int-abs/lenls is used by le-pos, ls-add, abs-ls, pls-neg, pls-pos-01, pls-pos-02, zero-ls-03, mods-ls-04, square-le-04, zero-ge-01, mod-neq, modlep-04, modneqp, pnls-negpos, numle-07, three, pnls-posneg, zero-ge-add, square-interval, noeth-zero-ls, ple-pos-better, mult-pos, zero-gr-add-02, ple-pos, modeqp-01, le-neg, zero-gr, auxexdivmod, pnls-pos, square-inject, square-le, square-ls, numabs-01, est-nle, mod-nls, mod-nle, pls-pos, zero-ge-add-01, zero-gr-03,
• int-abs/leone is used by le-same-01, le-same-02, abs-le-one-j, eq-one, abs-ls-same-01, numle-07, three, noeth-zero-ls, auxexdivmod, square-zero-02,
• int-abs/lep is used by numle, modlep-03, square-ex, numle-12, numle-09, auxexdivmod, ls-dist-06, square-inject, modlsp-03,
• int-abs/lep-01 is used by numle-13, numle-02, square-zero-02, ls-dist-05, mod-nle, mult-sub-less,
• int-abs/lep-02 is used by modzero-06, two-le-04, two-le-03, two-le-02, two-le-01, square-le-04, le-dist, modlep-03, square-ex, numle-01, numle-06, numle-08, numle-03, numle-04, numle-05, le-dist-02, le-dist-01, square-interval, square-inject, two-le, square-ls-02,
• int-abs/ler is used by modlep, modzero-05, modzero-04, square-ex, zero-gr, mod-nle,
• int-abs/les is used by modzero-06, modzero-05, modzero-02, modzero-01, modzero-04, modzero-03, square-ex,
• int-abs/lsone is used by le-one, abs-ls-j-one, mods-zero-07, numle-07, abs-ls-same, numls-07, square-ls-04,
• int-abs/minus-add is used by square-even, eq-one-neg, noeth-zero-ls,
• int-abs/mone-05 is used by eq-one, zero-ge-add,
• int-abs/mone-06 is used by square-ex, noeth-zero-ls, zero-gr-add-02, auxexdivmod, mod-nls,
• int-abs/mone-08 is used by square-le-06, abs-ls-same-01,
• int-abs/neg is used by eq-one, mod-neq, exdivmod, ls-neg, noeth-zero-ls, zero-gr, zero-gr-01,
• int-abs/neg-01 is used by ls-neg, modeqp-neg, modlsp-06, modlsp-04,
• int-abs/neg-02 is used by eq-one, square-eq, zero-gr-01, abs-eqneg,
• int-abs/neg-03 is used by eq-one-neg, abs-ls-same-01, square-eq, minus-one,
• int-abs/neg-05 is used by square-eq, square-minus,
• int-abs/neg-06 is used by mods-nls, minus-left, modlep-04, modlep-03, abs-ls-same-01, square-eq, modeqp-01, modeqp-03, modlsp-06, modlsp-05, modlsp-04, modlsp-03, abs-eqneg, square-gez-02,
• int-abs/neg-07 is used by modzero-07, eq-one, mod-neq, modlep-03, exdivmod, modeqp-02, modeqp-03, modlsp-06, modlsp-05, modlsp-04, modlsp-03,
• int-abs/neg-11 is used by modeqp-neg, modlsp-06, modlsp-04,
• int-abs/neg-12 is used by minus-left, minus-one-02, modeqp-01, modeqp-neg,
• int-abs/neg-13 is used by abs-ls, mods-nls, mod-neq, modlep-04, modlep-03, abs-ls-same-01, noeth-zero-ls, modeqp-01, modeqp-neg, modlsp-03,
• int-abs/neg-15 is used by numlsneg-03, numlsneg-02, numlsneg-01, numleneg-03, numleneg-02, numleneg-01, numleneg, modzero-06, modzero-05, modzero-02, modzero-01, modzero-04, modzero-03, mod-neq, modlep-04, modlep-02, exdivmod, zero-ge-add, modeqp-02, modeqp-01, modeqp-03, numlsneg, modlsp-05, modlsp-02, abs-eqall,
• int-abs/negeq is used by eq-one-neg, eq-one, minus-one-01, exdivmod, square-eq, minus-one, two-mone, abs-eqall,
• int-abs/negle-07 is used by modlep-03, exdivmod, abs-ls-same-01, noeth-zero-ls, modeqp-01, modeqp-neg, modlsp-06, modlsp-03,
• int-abs/negle-13 is used by modzero-07, noeth-zero-ls, square-gez-02,
• int-abs/numadd is used by square-even, square-ex,
• int-abs/numadd-01 is used by eq-one-neg, eq-one, three, zero-ge-add, noeth-zero-ls, two-mone,
• int-abs/numle-01 is used by square-ex,
• int-abs/numle-02 is used by square-le-05, abs-ls-same-01, square-interval, square-eq-02, auxexdivmod, square-ls-03,
• int-abs/numle-03 is used by square-ex, zero-ge-add, square-zero-01,
• int-abs/numleledel is used by le-same-06, three,
• int-abs/numleledel-01 is used by square-le-05, abs-ls-same-01, square-interval, square-eq-02, auxexdivmod, square-ls-03,
• int-abs/numlelsdel is used by short-mult-max, square-ls-04,
• int-abs/numlelsdel-01 is used by three,
• int-abs/numls-01 is used by ls-pos,
• int-abs/numls-02 is used by square-ex, square-interval, noeth-zero-ls, zero-gr-add-02, auxexdivmod, mod-nls,
• int-abs/numls-03 is used by abs-ls, pls-neg, mods-nls, square-le-06, mods-zero-07, eq-one, mod-neq, three, zero-ge-add, modeqp-01, square-ls-04,
• int-abs/numsub is used by square-zero-02,
• int-abs/one-03 is used by numls-07,
• int-abs/sub-add-01 is used by modlep-04, modlep-03, exdivmod, modeqp-02, modeqp-01, modeqp-03, auxexdivmod, square-zero-02, modlsp-03, mod-nle,
• int-abs/sub-add-06 is used by two-sub,
• int-abs/sub-add-09 is used by exdivmod,
• int-abs/sub-eq is used by square-even, eq-one-neg, modeqp, modlep-03, exdivmod, noeth-zero-ls, pred-rmerge, modeqp-02, modeqp-01, modeqp-03, two-oddeq, two-sub, numsub, modlsp-03, dist-sub-merge, abs-eqall, two-sub-01, dist-sub-split, two-pred, mod-nle,
• int-abs/sub-eq-01 is used by eq-one-neg,
• int-abs/sub-le is used by numleneg-03, numleneg, modzero-06, modzero-05, modzero-04, modlep-03, mult-sub-lesseq, mod-nle,
• int-abs/sub-le-01 is used by numleneg-02, numleneg-01, exdivmodpos, modzero-02, modzero-01, modzero-03, modlep-02, square-ex, zero-ge-add, noeth-zero-ls, modeqp-03, auxexdivmod, square-zero-02, modlsp-03,
• int-abs/sub-ls is used by zero-ls-sub, numlsneg-03, exdivmodpos, mod-neq, modlep-04, square-ex, exdivmod, numle-07, noeth-zero-ls, numlsneg, mult-sub-less,
• int-abs/sub-ls-01 is used by zero-ls-sub, numlsneg-02, numlsneg-01, ls-pos, modlep-04, square-ex, exdivmod, numle-07, noeth-zero-ls, auxexdivmod, modlsp-05, modlsp-02, numls-07,
• int-abs/sub-pred is used by square-ex, noeth-zero-ls, auxexdivmod,
• int-abs/sub-sub is used by exdivmod,
• int-abs/subsub is used by exdivmod, noeth-zero-ls,
• int-abs/succ-01 is used by modlep-03, square-ex, square-interval, square-inject, modlsp-03,
• int-abs/succ-02 is used by modlsp, modzero-05, modzero-04, square-ex, square-interval, noeth-zero-ls, auxexdivmod-01, zero-gr, auxexdivmod, zero-gr-add, mod-nls, square-ls-03,
• int-abs/zero-gels is used by square-interval,
• int-abs/zero-gels-01 is used by abs-ls, pls-neg, zero-ls-03, eq-one, pzero-ls, mod-neq, modlep-04, exdivmod, zero-ge-add, noeth-zero-ls, zero-gr-add-02, modeqp-01, pzero-gr, le-neg, modeqp-neg, abs-eqall, mod-nls, zero-ge-add-01, zero-ge-add-02,
• int-abs/zero-gels-02 is used by square-ex,
• int-abs/zero-gels-03 is used by mod-neq, modlep-04, exdivmod, numle-07, modeqp-01, square-zero-01, abs-eqall,
• int-abs/zero-gels-04 is used by ls-add, abs-ls, pls-pos-01, abs-ls-j-one, mods-ls-04, square-le-04, eq-one, modeqp, mod-neq, modlep-04, modneqp, square-ex, exdivmod, pnls-negpos, numle-07, three, pnls-posneg, zero-ge-add, square-interval, noeth-zero-ls, modeqp-01, pzero-gr, zero-gr, auxexdivmod, square-inject, abs-eqall, mult-gt-both, est-nle, zero-ge-add-02,
• int-abs/zeroone is used by mods-zero-07,