[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification int-basic1

int-basic1/trans is used by square-nls-01, nls-mult-div,
int-basic1/two-ls is used by div-div-pred-01,
int-basic1/forward-pos is used by zero-07, square-nle, prod-div-less, one-04, nummult-modls-01, nummult-modls, nummult-modle-01, nummult-modle, nls-mult-div, mult-05, mult-03, modmod-add2-posneg-neg, modeq-neg-02, mod-zero-one, mod-zero-09, mod-zero-06, mod-zero-05, mod-two-05, mod-succ, mod-sub-02, mod-pred-neg-01, mod-pred-02, mod-nls-05, mod-nls-04, mod-nls-01, mod-nls, mod-mod-less, mod-le-num, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-zero, mod-add-01, letwo, less-mult-div-01, leone-two, estimate-01, div-zero-ngr, div-zero-01, div-sum-ls-01, div-sum-ls, div-mult-two-nls-01, div-mult-three-nls, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-ls, div-le-modnotzero, div-eq-zero-01, div-eq-zero, div-add1-posneg-pos-01, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ-neg, div-add-succ, div-add-nosucc-neg, div-add-nosucc,
int-basic1/irref is used by square-nls, square-nle, prod-div-less, nls-mult-div, modmod-pos, mod-zero-06, mod-rec-01, mod-neq, mod-lsz-01, mod-ls-zero, mod-ls-same-02, mod-ls-same-01, mod-gez, mod-div-ls, ls-even-01, estimate-01, diveq-pos, div-sum-ls, div-mult-two-nls-01, div-ls-zero, div-ls-mone, div-ls-modnotzero, div-le-same-neg, div-est-nle-pos, div-add-nosucc, div-abs,
int-basic1/lf-01 is used by zero-07, zero-05, zero-04, zero-03, zero-02, sub-ls-01, square-nle, square-interval, prod-div-less, one-neg, nummult-modls-01, nummult-modls, nummult-modle-01, nummult-modle, nummult-ls-01, nummult-le-03, nummult-le-01, mult-ls-01, mult-ls, mult-05, mult-03, modmod-mult-07, modmod-mult-04, modmod-mult-03, modmod-mult-02, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add, modeq-pos-03, mod-zero-one, mod-zero-ls, mod-zero-09, mod-zero-06, mod-zero-05, mod-zero-02, mod-zero-01, mod-twoodd-03, mod-succ-01, mod-sub-02, mod-pred-neg-01, mod-nls-05, mod-nls-04, mod-nls-02, mod-nls-01, mod-nle-02, mod-ngr, mod-ngez-01, mod-mod-less, mod-lsz, mod-ls-zero, mod-ls-same-01, mod-lezero, mod-le-num, mod-grz-02, mod-grz-01, mod-grz, mod-by6, mod-add-zero, mod-add-pos, mod-add-neg, lsfc-02, lsf-02, ls-even-01, ls-02, less-mult-div-01, estimate-01, diveq-neg, div2-nls-03, div2-nls-02, div2-nls-01, div-zero-nls, div-zero-ngr-01, div-zero-ngr, div-zero-02, div-zero-01, div-twoodd-05, div-twoodd-03, div-sum-ls-01, div-ngr-zero, div-nearer-zero, div-mult-nls-zero, div-mult-01, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-ls, div-lezero, div-le-same-neg, div-le-pos, div-le-modnotzero, div-est-num, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-elim2, div-elim-pospos, div-elim-negpos, div-div-pred-01, div-div-pred, div-div, div-addthree-rew, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ-neg, div-add-succ, div-add-pos, div-add-nosucc-neg, div-add-neg, abs-shift,
int-basic1/lf-02 is used by square-nls, square-nle, square-interval, nummult-ls, nummult-le-02, nummult-le-01, modmod-mult-07, modmod-ma-01, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg, modmod-add-if, modex, modeven-neg, mod-zero-02, mod-twoodd-03, mod-twoodd, mod-two-pred-01, mod-rec-01, mod-pred-01, mod-nls-04, mod-ngr, mod-ngez-01, mod-lsz-01, mod-ls-zero, mod-ls-same-01, mod-gez, mod-by6, mod-add-zero, mod-add-neg, ls-even-01, ls-03, ls-02, ls, less-mult-div-01, leone-two, exeven, even-not, estimate-01, diveq-pos, div2-notzero, div2-nls-02, div2-nls, div-zero-02, div-twoodd-03, div-two-intro, div-nls-01, div-minus255-256-01, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-le-same-neg, div-eq-zero-01, div-eq-same-01, div-div-pred-01, div-div-pred, div-div, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-nosucc-neg, div-add-neg,
int-basic1/lf-03 is used by nummult-le-01, mod-twoodd, mod-mult, mod-add-pos, mod-add-neg, div-add-pos, div-add-neg,
int-basic1/ls-01 is used by zero-05, zero-03, two-add-square-01, sub-ls, prod-div-less, mult-03, modmod-mult-09, modmod-mult-03, modmod-mult-01, modmod-add2-negpos-pos-01, modmod-add-case, modmod-add-01, modex, modeven-pos, modeq-pos-01, modeq-neg-02, mod2-add-neg, mod-zero-one, mod-zero-ls, mod-zero-06, mod-two-06, mod-pred-neg, mod-nls-06, mod-nls-04, mod-nls-02, mod-nls-01, mod-neq, mod-lsz, mod-ls-same-02, mod-ls-same-01, mod-le-num, mod-div-ls, mod-by6, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-zero, mod-add-neg, ls-succ, ls-even-01, ls, less-mult-div-01, leone-two, le-abs-numerator, div2-nls-03, div2-nls-02, div2-nls-01, div2-nls, div-zero-02, div-two-intro, div-sum-ls-01, div-same, div-nls-01, div-nearer-zero, div-mult-three-nls, div-mult-three, div-mult-neg, div-mult-01, div-ls-02, div-le-same, div-le-pos, div-est-denom-pos, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-eq-same, div-elim2, div-elim, div-div, div-add1-posneg-pos-01, div-add1-negpos-neg-01, div-add-succ, div-add-neg, abs-shift,
int-basic1/lst is used by div-mult-three-nls,
int-basic1/lst-01 is used by zero-05, zero, square-interval, modmod-mult-09, modmod-mult-05, modmod-mult-03, modmod-mult-01, modmod-add-law, modmod-add-01, modex, mod-zero-one, mod-zero-06, mod-succ-01, mod-pred-neg, mod-nls-06, mod-nls-04, mod-neq, mod-lsz-01, mod-ls-zero, mod-ls-same-02, mod-ls-same-01, mod-grz-01, mod-div-zero, mod-div-ls, le-abs-numerator, div2-zero, div-twoodd-06, div-two-intro, div-same, div-nearer-zero, div-mult-three-nls, div-mult-01, div-ls-zero, div-ls-02, div-eq-zero-01, div-eq-same-01, div-eq-same, div-div, div-add1-negpos-neg-02, abs-shift, abs,
int-basic1/minus-one is used by modex-odd-neg, modeven-neg-01, modeven-neg, mod2-neg-odd, mod2-add-neg, mod-two-pred-01, letwozero, even-not-ex, div2-zero, div2-notzero, div2-nls-02, div2-nls, div2-add-neg, div-two-intro, div-div-pred-01, div-div-pred,
int-basic1/numlsf is used by mod-succ-01, mod-pred-neg-01, mod-pred-neg, mod-pred-02, div2-notzero, div-nearer-zero, div-ls-mone, div-elim-negpos, div-div-pred-01, div-div-pred,
int-basic1/numlslsdel is used by square-nle, ls-even-01, div-div-pred-01, div-div-pred,
int-basic1/numlslsdel-01 is used by mod-sub-02, div-mult-three-nls,
int-basic1/trans is used by zero-07, zero-05, zero-04, zero-03, zero-02, sub-ls-01, square-interval, prod-div-less, one-neg, nummult-modls-01, nummult-modls, nummult-modle-01, nummult-modle, nummult-ls-01, nummult-le-03, nummult-le-01, mult-ls-01, mult-ls, mult-05, mult-03, modmod-mult-07, modmod-mult-04, modmod-mult-03, modmod-mult-02, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add, modeq-pos-03, mod-zero-one, mod-zero-ls, mod-zero-09, mod-zero-06, mod-zero-05, mod-zero-02, mod-zero-01, mod-twoodd-03, mod-succ-01, mod-sub-02, mod-pred-neg-01, mod-nls-05, mod-nls-04, mod-nls-02, mod-nls-01, mod-nle-02, mod-ngr, mod-ngez-01, mod-lsz, mod-ls-zero, mod-ls-same-01, mod-lezero, mod-le-num, mod-grz-02, mod-grz-01, mod-grz, mod-by6, mod-add-pos, mod-add-neg, lsfc-02, lsf-02, ls-even-01, ls-02, less-mult-div-01, estimate-01, diveq-neg, div2-nls-03, div2-nls-02, div2-nls-01, div-zero-nls, div-zero-ngr-01, div-zero-ngr, div-zero-02, div-zero-01, div-twoodd-05, div-twoodd-03, div-ngr-zero, div-nearer-zero, div-mult-nls-zero, div-mult-01, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-lezero, div-le-same-neg, div-le-pos, div-est-num, div-eq-zero-01, div-eq-same-01, div-elim2, div-elim-pospos, div-elim-negpos, div-div-pred, div-div, div-addthree-rew, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ-neg, div-add-pos, div-add-nosucc-neg, div-add-neg, abs-shift,
int-basic1/two-ls is used by square-nls, square-nle, square-even, mod-zero-one, mod-two-06, even-not-ex, div-two-zero, div-two-intro, div-shift-two,

Used from specification int-mult

int-mult/add-mult-two is used by mod-zero-one,
int-mult/commutativity is used by two-mult, square-nls, square-nle, modmod-mult-04, modeq-pos-03, modeq-pos-02, mod-add-pos, mod-add-neg, div-twoodd-07, div-twoodd-04, div-twoodd-02, div-shift-two, div-ls-modnotzero, div-div, div-add-pos, div-add-neg,
int-mult/dist-lsplit is used by square-inject, mult-split-mod, modmod-mult, modby6-help, mod-shift, less-mult-div-01, le-abs-numerator, even-mult, even-add, div2one-01, div-sum-ls, div-shift-two, div-mult-shift-holds, div-ls-mone, div-div-pred-01, div-addthree-rew, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-01, div-add-both,
int-mult/dist-rsplit is used by square-interval, modby6-help, mod-div-ls, div-sum-ls, div-mult-two-nls-01, div-div-pred,
int-mult/dist-sub-split is used by square-inject, mult-03,
int-mult/ls-pos is used by square-nls, square-nle,
int-mult/ls-pos-01 is used by div-mult-three-nls,
int-mult/ls-same-06 is used by div-ls-same,
int-mult/minus-left is used by modmod-mult-07, div-twoodd-07, div-twoodd-04, div-twoodd-02, div-two-intro,
int-mult/mod-neq is used by modmod-pos,
int-mult/modeqp-01 is used by modeq-neg, mod-add1-posneg-neg, mod-add-01, diveq-neg, div-div-pred,
int-mult/modeqp-02 is used by div-elim-posneg,
int-mult/modeqp-03 is used by div-elim-negneg,
int-mult/modeqp-copied is used by one-neg, mult-02, modmod-add, modeq-neg-02, mod-succ-01, mod-rec, mod-pred-neg-01, mod-pred-neg, mod-pred-02, mod-add1-posneg-pos, mod-add1-negpos-neg, div-rec, div-mult-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-01,
int-mult/modlep is used by nummult-ls, diveq-pos,
int-mult/modlep-01 is used by nummult-le-02, nummult-le, mult-ls,
int-mult/modlep-02 is used by nummult-ls-03, nummult-le-03, nummult-le-01, mult-ls-01, div-mult-nle-est, div-le-modnotzero,
int-mult/modlep-03 is used by ls-01, leone-two, div-le-pos, div-est-num, div-est-nls,
int-mult/modlep-04 is used by div-le-pos, div-est-num,
int-mult/modlsp is used by modmod-pos, estimate-01, div-mult-nls-est-01, div-le-modnotzero,
int-mult/modlsp-01 is used by nummult-ls-03, nummult-ls-01, nummult-le-03, nummult-le-01,
int-mult/modlsp-02 is used by nummult-le, num-ls, diveq-pos, div-mult-nls-est, div-ls, div-est-nle-pos,
int-mult/modneqp is used by prod-div-less, ls, div-est-denom-pos,
int-mult/mods-eq is used by div-mult-two-nls-01,
int-mult/mods-ls-02 is used by mult-02,
int-mult/numeq-04 is used by div-eq-same-01,
int-mult/numle-12 is used by div-le-same-neg, div-eq-zero-01,
int-mult/numls-02 is used by nummult-ls-02,
int-mult/numls-13 is used by modmod-add-law-pos, mod-add1-posneg-pos, mod-add1-negpos-neg,
int-mult/square-inject is used by square-inject,
int-mult/square-interval is used by square-interval,
int-mult/succ-lsplit is used by div-eq-zero-01,
int-mult/succ-rmerge is used by mod-div-ls,
int-mult/zero-ls is used by modmod-ma, mod-by6,
int-mult/Mult-zero is used by one-neg, nls-mult-div, modmod-pos, modmod-add-04, mod-pred-03, mod-ls-same-02, mod-add-neg, mod-add-01, div-shift-two, div-mult-two-nls-01,
int-mult/abs-eqall is used by div-twoodd-07, div-twoodd-05, div-two-intro, div-nearer-zero, div-div-pred,
int-mult/add-mult-two is used by modmod-add-law-pos, modmod-add-case, modeq-neg-02, modby6-help, mod-zero-one, mod-zero-06, mod-add1-posneg-pos, mod-add1-negpos-neg, div2-nls-02, div2-nls, div2-nle-02, div-mult-two-nls-01, div-ls-mone, div-add1-posneg-pos-01, div-add1-negpos-neg-01, abs-shift-01, abs-shift,
int-mult/associativity is used by zero-06, zero-04, zero, two-odd, two-mult-01, two-mult, two-even, two-add-square, square-nls-02, square-nls-01, square-nls, square-nle-02, square-nle-01, square-nle, square-ls, square-interval, square-inject, square-even-01, square-even, quad-div-less, prod-div-less-01, prod-div-less, one-neg, one-01, one, nummult-modls-01, nummult-modls, nummult-modle-01, nummult-modle, nummult-ls-03, nummult-ls-02-01, nummult-ls-02, nummult-ls-01-01, nummult-ls-01, nummult-ls, nummult-le-03, nummult-le-02, nummult-le-01, nummult-le, nummult-eq-01, nummult-eq, num-ls, nls-mult-div, mult-split-mod-02, mult-split-mod, mult-ls-01, mult-ls, mult-div-switch, mult-05, mult-04, mult-03, mult-02, mult-01, mult, modmod-pos, modmod-mult-08, modmod-mult-07, modmod-mult-06, modmod-mult-05, modmod-mult-04, modmod-mult-03, modmod-mult-02, modmod-mult, modmod-ma-negpos-neg, modmod-ma-01, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-law-pos, modmod-add-case, modmod-add-04, modmod-add, modmod, modex-odd-neg-01, modex-odd-neg, modex-odd, modex, modeven-pos, modeven-neg-01, modeven-neg, modeq-pos-04, modeq-pos-03, modeq-pos-02, modeq-pos-01, modeq-pos, modeq-neg-02, modeq-neg, modby6-help, mod2-add-neg, mod-zero-one, mod-zero-num, mod-zero-07, mod-zero-06, mod-zero-05, mod-zero-04, mod-zero-03, mod-zero-01, mod-twoodd-03, mod-twoodd-02, mod-twoodd-01, mod-twoodd, mod-twoeven, mod-two-pred-02, mod-two-pred-01, mod-two-pred, mod-two-04, mod-two-03, mod-two-02, mod-succ-02, mod-succ-01, mod-sub-02, mod-shift, mod-same, mod-rew, mod-rec, mod-pred-neg-01, mod-pred-neg, mod-pred-03, mod-pred-02, mod-nls-05, mod-nle, mod-next-square, mod-neg-01, mod-neg, mod-mult-pos-02, mod-mult-pos-01, mod-mult-pos, mod-mult-neg-03, mod-mult-neg-02, mod-mult-neg-01, mod-mult-neg, mod-mult-04, mod-mult-03, mod-mult-02, mod-mult-01, mod-mult, mod-mod-less, mod-ls-same-02, mod-ls-same-01, mod-ls-same, mod-div-ls, mod-by6, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-zero, mod-add-pos, mod-add-neg, mod-add-both-zero, mod-add-01, ls-same-pos-02, ls-same-pos, ls-even-01, ls-even, ls-02, ls-01, ls, less-mult-div-02, less-mult-div-01, less-mult-div, leone-two, le-norest, le-abs-numerator, is-div, exodd, exeven, even-or-succ-even, even-not-ex, even-not, even-mult, even-add, estimate-01, diveq-pos, div2zero, div2one-01, div2one, div2-zero, div2-odd-01, div2-odd, div2-notzero, div2-nls-02, div2-nls, div2-nle-02, div2-neg-odd, div2-neg-01, div2-add-neg, div-zero-01, div-zero, div-twoodd-07, div-twoodd-06, div-twoodd-05, div-twoodd-04, div-twoodd-03, div-twoodd-02, div-twoodd-01, div-twoodd, div-two-zero-01, div-two-intro, div-two-01, div-two, div-sum-ls, div-sub-01, div-sub, div-shift-two, div-rec, div-ngr-zero, div-nearer-zero, div-mult-two-nls-01, div-mult-two-nls, div-mult-three-nls, div-mult-three, div-mult-shift-holds, div-mult-rew-01, div-mult-rew, div-mult-pos-rew, div-mult-pos-03, div-mult-pos-02, div-mult-pos-01, div-mult-pos, div-mult-num, div-mult-nls-zero, div-mult-nls-est-01, div-mult-nls-est, div-mult-nle-est, div-mult-neg, div-mult-ls-pos, div-mult-ls, div-mult-le-01, div-mult-le, div-mult-03, div-mult-02, div-mult-01, div-mult, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-pos-better, div-ls-mone, div-ls-modzero, div-ls, div-lezero, div-le-same-neg, div-le-same, div-le-pos, div-le-modzero-01, div-le-modzero, div-le-modnotzero, div-est-num, div-est-nls, div-est-nle-pos, div-est-denom-pos, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-eq-same, div-elim3, div-elim2, div-elim1, div-elim-pospos, div-elim-posneg, div-elim-pos, div-elim-negpos, div-elim-negneg, div-elim-divides, div-div-switch, div-div-pred-01, div-div-pred, div-div-pos, div-div, div-am-rew, div-addthree-rew, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-01, div-add-succ, div-add-pos, div-add-nosucc, div-add-neg, div-add-both, add-div-mult, abs-shift-01, abs-shift, abs-03, abs,
int-mult/commutativity is used by zero-06, zero-04, zero, two-odd, two-mult-01, two-mult, two-even, two-add-square, square-nls-02, square-nls-01, square-nls, square-nle-02, square-nle-01, square-nle, square-ls, square-interval, square-inject, square-even-01, square-even, quad-div-less, prod-div-less-01, prod-div-less, one-neg, one-01, one, nummult-modls-01, nummult-modls, nummult-modle-01, nummult-modle, nummult-ls-03, nummult-ls-02-01, nummult-ls-02, nummult-ls-01-01, nummult-ls-01, nummult-ls, nummult-le-03, nummult-le-02, nummult-le-01, nummult-le, nummult-eq-01, nummult-eq, num-ls, nls-mult-div, mult-split-mod-02, mult-split-mod, mult-ls-01, mult-ls, mult-div-switch, mult-05, mult-04, mult-03, mult-02, mult-01, mult, modmod-pos, modmod-mult-08, modmod-mult-07, modmod-mult-06, modmod-mult-05, modmod-mult-04, modmod-mult-03, modmod-mult-02, modmod-mult, modmod-ma-negpos-neg, modmod-ma-01, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-law-pos, modmod-add-case, modmod-add-04, modmod-add, modmod, modex-odd-neg-01, modex-odd-neg, modex-odd, modex, modeven-pos, modeven-neg-01, modeven-neg, modeq-pos-04, modeq-pos-03, modeq-pos-02, modeq-pos-01, modeq-pos, modeq-neg-02, modeq-neg, modby6-help, mod2-add-neg, mod-zero-one, mod-zero-num, mod-zero-07, mod-zero-06, mod-zero-05, mod-zero-04, mod-zero-03, mod-zero-01, mod-twoodd-03, mod-twoodd-02, mod-twoodd-01, mod-twoodd, mod-twoeven, mod-two-pred-02, mod-two-pred-01, mod-two-pred, mod-two-04, mod-two-03, mod-two-02, mod-succ-02, mod-succ-01, mod-sub-02, mod-shift, mod-same, mod-rew, mod-rec, mod-pred-neg-01, mod-pred-neg, mod-pred-03, mod-pred-02, mod-nls-05, mod-nle, mod-next-square, mod-neg-01, mod-neg, mod-mult-pos-02, mod-mult-pos-01, mod-mult-pos, mod-mult-neg-03, mod-mult-neg-02, mod-mult-neg-01, mod-mult-neg, mod-mult-04, mod-mult-03, mod-mult-02, mod-mult-01, mod-mult, mod-mod-less, mod-ls-same-02, mod-ls-same-01, mod-ls-same, mod-div-ls, mod-by6, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-zero, mod-add-pos, mod-add-neg, mod-add-both-zero, mod-add-01, ls-same-pos-02, ls-same-pos, ls-even-01, ls-even, ls-02, ls-01, ls, less-mult-div-02, less-mult-div-01, less-mult-div, leone-two, le-norest, le-abs-numerator, is-div, exodd, exeven, even-or-succ-even, even-not-ex, even-not, even-mult, even-add, estimate-01, diveq-pos, div2zero, div2one-01, div2one, div2-zero, div2-odd-01, div2-odd, div2-notzero, div2-nls-02, div2-nls, div2-nle-02, div2-neg-odd, div2-neg-01, div2-add-neg, div-zero-01, div-zero, div-twoodd-07, div-twoodd-06, div-twoodd-05, div-twoodd-04, div-twoodd-03, div-twoodd-02, div-twoodd-01, div-twoodd, div-two-zero-01, div-two-intro, div-two-01, div-two, div-sum-ls, div-sub-01, div-sub, div-shift-two, div-rec, div-ngr-zero, div-nearer-zero, div-mult-two-nls-01, div-mult-two-nls, div-mult-three-nls, div-mult-three, div-mult-shift-holds, div-mult-rew-01, div-mult-rew, div-mult-pos-rew, div-mult-pos-03, div-mult-pos-02, div-mult-pos-01, div-mult-pos, div-mult-num, div-mult-nls-zero, div-mult-nls-est-01, div-mult-nls-est, div-mult-nle-est, div-mult-neg, div-mult-ls-pos, div-mult-ls, div-mult-le-01, div-mult-le, div-mult-03, div-mult-02, div-mult-01, div-mult, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-pos-better, div-ls-mone, div-ls-modzero, div-ls, div-lezero, div-le-same-neg, div-le-same, div-le-pos, div-le-modzero-01, div-le-modzero, div-le-modnotzero, div-est-num, div-est-nls, div-est-nle-pos, div-est-denom-pos, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-eq-same, div-elim3, div-elim2, div-elim1, div-elim-pospos, div-elim-posneg, div-elim-pos, div-elim-negpos, div-elim-negneg, div-elim-divides, div-div-switch, div-div-pred-01, div-div-pred, div-div-pos, div-div, div-am-rew, div-addthree-rew, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-01, div-add-succ, div-add-pos, div-add-nosucc, div-add-neg, div-add-both, add-div-mult, abs-shift-01, abs-shift, abs-03, abs,
int-mult/dist-rmerge is used by zero-04, two-add-square, mult-02, modmod-mult-04, modmod-add-zero, modmod-add-04, modeq-pos-03, modeq-pos-02, modeq-neg-02, modeq-neg, mod2-add-neg, mod-twoodd, mod-mult-pos-01, mod-mult-neg-02, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-pos, mod-add-neg, mod-add-both-zero, div2-add-neg, div-sum-ls, div-sub, div-mult-two-nls-01, div-mult-02, div-add1-negpos-pos, div-add-pos, div-add-neg,
int-mult/dist-sub-merge is used by mod-mult-02, mod-mult, div-sub-01,
int-mult/eq-dist is used by nummult-ls, nummult-le-02, modmod-pos, modmod-ma-negpos-neg, modby6-help, mod-twoodd-03, even-mult, even-add, div-twoodd-07, div-twoodd-05, div-mult-ls, div-minus-onediff, div-am-rew, div-add1-posneg-pos-01, div-add1-negpos-neg-01,
int-mult/eq-neg is used by modmod-mult-07, modex,
int-mult/eq-nonzero is used by nummult-eq-01, modmod-pos, mod-mult-02,
int-mult/eq-one is used by mod-twoodd-02, div-minus-onediff-01,
int-mult/eq-pos is used by two-odd, mult-03, modex-odd-neg-01, modex-odd-neg, modex-odd, modex, modeq-pos, mod-twoodd-03, mod-twoodd, mod-twoeven, mod-mult-neg-01, mod-mult-03, mod-mult-01, mod-mult, exodd, exeven, even-not-ex, even-mult, div2-nls-02, div2-nls, div2-nle-02, div-two-intro, div-mult-two-nls-01,
int-mult/eq-succ is used by nummult-ls, nummult-le-02, div-mult-two-nls-01, div-minus-onediff-01, div-div-pred, div-add1-posneg-pos-01, div-add1-negpos-neg-01,
int-mult/eq-succ-01 is used by modeq-neg-02, mod-add1-posneg-pos, mod-add1-negpos-neg, div-mult-two-nls-01,
int-mult/le-pos is used by nummult-modle-01, nummult-modle, modmod-pos, le-norest, estimate-01,
int-mult/le-pos-01 is used by square-interval,
int-mult/le-same is used by div-mult-three-nls,
int-mult/le-same-02 is used by modex,
int-mult/le-same-03 is used by div-ls-same,
int-mult/le-two is used by div2-nls-02,
int-mult/ls-add is used by modmod-add2-posneg-neg, modeq-pos-03, mod-zero-07, mod-zero-03, mod-succ-01, mod-pred-neg-01, mod-nle, mod-ls-same-01, ls, div-zero, div-minus-onediff, div-ls-zero, div-ls-mone, div-le-pos, div-eq-zero, div-add1-posneg-pos-01, div-add1-negpos-neg-01,
int-mult/ls-add-02 is used by mod-ls-same-01, div-le-same-neg, div-add1-negpos-neg-01,
int-mult/ls-add-03 is used by mod-ls-same-01, div-add1-posneg-pos-01,
int-mult/ls-dist is used by nummult-ls-03,
int-mult/ls-dist-01 is used by div-shift-two,
int-mult/ls-dist-02 is used by less-mult-div-01, div-le-same-neg,
int-mult/ls-dist-03 is used by square-interval, nummult-ls-03, mod-mult-neg-02, mod-add-01,
int-mult/ls-dist-04 is used by div-eq-zero-01,
int-mult/ls-forward is used by square-nls, square-nle, mod-add-01, ls-01, estimate-01, div-sum-ls,
int-mult/ls-pos is used by square-nls, square-nle, square-interval, prod-div-less, nummult-modls-01, nummult-modls, nummult-ls-03, modeq-pos-03, modeq-neg-02, mod2-add-neg, mod-sub-02, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-neg, ls-01, is-div, estimate-01, diveq-pos, div-sum-ls, div-mult-two-nls-01, div-mult-three-nls, div-mult-02, div-ls-modzero, div-le-modzero, div-add-neg,
int-mult/ls-same is used by nummult-ls-01, nummult-le-03, mult-ls, modmod-add2-posneg-neg, modeq-pos-03, mod-pred-neg-01, mod-mult, mod-add-neg, mod-add-01, div-nearer-zero, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-mone, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-01, div-add-neg,
int-mult/ls-same-01 is used by mod-sub-02, mod-mod-less, div-mult-two-nls-01,
int-mult/ls-same-03 is used by mod-ls-same-01, le-abs-numerator, div-minus-onediff-01, div-eq-zero-01, div-elim-posneg, div-div-pred-01,
int-mult/ls-two-02 is used by ls-even-01,
int-mult/ls-two-03 is used by ls-even-01,
int-mult/minus-left is used by zero, one-neg, mult-01, modmod-mult-07, modmod-mult-05, modmod-mult-03, modmod-mult-02, mod-zero-06, mod-twoodd-03, mod-neg-01, mod-neg, mod-mult-neg, ls-even-01, div2-odd-01, div2-neg-odd, div-twoodd-07, div-twoodd-04, div-twoodd-03, div-twoodd-02, div-two-intro, div-nearer-zero, div-mult-neg, div-mult-01, div-ls-mone, div-elim3, div-elim2, div-elim1, div-div,
int-mult/minus-one-01 is used by mod-ls-same-02,
int-mult/minus-one-02 is used by mod-zero-06, mod-div-ls, div-ls-mone,
int-mult/mod-neq is used by modex-odd-neg,
int-mult/mod-nle is used by div-le-same,
int-mult/mods-eq is used by div2-nls-02, div2-nls, div2-nle-02,
int-mult/mods-ls-04 is used by prod-div-less, nummult-ls, nummult-le-02, nummult-le, num-ls, diveq-pos, div-mult-two-nls-01, div-mult-nls-est, div-ls, div-est-nle-pos,
int-mult/modzero is used by mod-zero-05, mod-by6, div-zero-01, div-lezero, div-add-neg,
int-mult/modzero-02 is used by nummult-ls-01, nummult-le-03, mult-ls, modmod-add2-posneg-neg-01, modeven-neg, even-not, div-twoodd-07, div-ngr-zero, div-ls-zero, div-ls-same, div-ls-mone, div-le-pos, div-est-num, div-eq-zero-01, div-add1-negpos-neg-01,
int-mult/modzero-03 is used by zero-04, modmod-pos, div-le-same-neg, div-elim-pospos,
int-mult/modzero-04 is used by zero-06, div-elim-negneg, abs,
int-mult/modzero-05 is used by le-abs-numerator,
int-mult/neq-two is used by mod2-add-neg, div-div-pred,
int-mult/numdist is used by modby6-help,
int-mult/numeq is used by square-inject, modby6-help,
int-mult/numeq-01 is used by div-shift-two,
int-mult/numeq-02 is used by modmod-add-law-pos,
int-mult/numle-03 is used by div-ls-mone,
int-mult/numle-05 is used by div-add1-posneg-pos-01, div-add1-negpos-neg-01,
int-mult/numle-10 is used by square-nls, square-nle, div2-nls,
int-mult/numle-12 is used by div2-neg-01,
int-mult/numls-01 is used by div-mult-two-nls-01,
int-mult/numls-03 is used by square-interval, div2-nle-02, div-ls-mone,
int-mult/numls-04 is used by div2-nls-02, div-div-pred-01, div-div-pred,
int-mult/numls-05 is used by div2-nls,
int-mult/numls-06 is used by div-div-pred-01,
int-mult/numls-07 is used by div-mult-three-nls,
int-mult/numls-08 is used by div2-nls-02, div-ls-mone,
int-mult/numls-10 is used by div2-nls, div2-nle-02, div-ls-mone,
int-mult/numls-12 is used by leone-two, div-div-pred,
int-mult/numsub is used by modmod-add-law-pos, div-ls-mone,
int-mult/numsucc is used by modmod-add-law-pos, modby6-help,
int-mult/odd-even is used by modeven-neg, mod-two-pred-01, even-not-ex,
int-mult/one is used by square-interval, one-01, one, nummult-ls, nummult-le-02, mult-05, mult-03, modmod-add-law-pos, modmod, modby6-help, mod-same, mod-ls-same-02, mod-ls-same-01, mod-div-ls, mod-add1-posneg-pos, mod-add1-negpos-neg, leone-two, le-abs-numerator, even-mult, div2-nls-02, div2-nls, div2-nle-02, div2-neg-01, div2-add-neg, div-sub, div-shift-two, div-mult-03, div-minus-onediff, div-ls-mone, div-le-same-neg, div-div-pred-01, div-div-pred, div-add1-posneg-pos-01, div-add1-negpos-neg-01,
int-mult/one-01 is used by square-nls, square-nle, one-neg, leone-two, div-shift-two, div-mult-three-nls, div-ls-same,
int-mult/pred-rmerge is used by mod-ls-same-02,
int-mult/square-eq is used by abs-03,
int-mult/square-even is used by square-nls, square-nle, square-inject, square-even,
int-mult/square-gez is used by mod-by6,
int-mult/square-ls-02 is used by square-ls,
int-mult/square-ls-04 is used by square-interval,
int-mult/square-zero-01 is used by square-interval,
int-mult/square-zero-02 is used by square-inject,
int-mult/succ-rmerge is used by nummult-ls-03, nummult-le-01, modex-odd-neg-01, modex-odd-neg, modeq-pos-01, modeq-neg-02, mod-succ-02, mod-rec, mod-pred-03, mod-pred-02, mod-next-square, mod-mult-neg-02, mod-ls-same-02, mod-ls-same, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-01, even-not-ex, div-shift-two, div-rec, div-mult-two-nls-01, div-mult-three-nls,
int-mult/two-ls is used by square-nls, square-nle,
int-mult/two-oddeq is used by modex-odd-neg,
int-mult/two-sub-01 is used by div-ls-mone,
int-mult/two-zero is used by mod-twoodd,
int-mult/zero-eq is used by mult-split-mod, modmod-pos, mod-mult-02, mod-mult, mod-add-01, div-eq-same-01, div-div, div-am-rew,
int-mult/zero-ge is used by square-nle, prod-div-less, nummult-ls, nummult-le-02, mult-split-mod, mult-ls-01, modmod-pos, modmod-mult, modmod-ma-negpos-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-neg, modmod-add-04, modex, modeven-pos, mod2-add-neg, mod-twoodd-02, mod-shift, mod-mult-pos, mod-ls-same-02, mod-by6, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add-pos, le-norest, exeven, even-not, div2-nls-02, div2-nls, div2-nle-02, div2-add-neg, div-two-intro, div-mult-two-nls-01, div-mult-three-nls, div-mult-shift-holds, div-mult-pos-01, div-mult-nle-est, div-mult-ls, div-mult-le-01, div-mult-02, div-minus-onediff-01, div-ls-mone, div-le-modnotzero, div-am-rew, div-addthree-rew, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add-succ, div-add-pos, div-add-nosucc, add-div-mult,
int-mult/zero-ge-01 is used by mult-split-mod, modex, div-mult-shift-holds,
int-mult/zero-ge-02 is used by two-add-square, square-nls, square-ls, square-even, mult-split-mod, modmod-mult, modmod-ma-negpos-neg, modmod-ma-01, modmod-ma, mod-shift, mod-by6, div-mult-shift-holds, div-mult-ls, div-am-rew,
int-mult/zero-ge-add is used by zero-04, nummult-ls-02, nummult-ls, nummult-le-02, nummult-le, num-ls, mult-split-mod, mult-ls-01, mult-ls, mult-02, modmod-pos, modmod-mult-04, modmod-mult, modmod-ma-negpos-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-04, modmod-add, modex-odd-neg, modeq-pos-02, modeq-pos, mod-zero-03, mod-succ-01, mod-shift, mod-rec, mod-pred-03, mod-pred-02, mod-nls-05, mod-mult-pos-01, mod-div-ls, mod-add1-posneg-pos, mod-add1-negpos-pos, mod-add-zero, mod-add-pos, ls-02, ls-01, ls, leone-two, exodd, even-or-succ-even, even-not-ex, diveq-pos, div-zero, div-twoodd, div-two-zero-01, div-shift-two, div-rec, div-mult-two-nls-01, div-mult-shift-holds, div-mult-nls-est-01, div-mult-nls-est, div-mult-nle-est, div-mult-ls, div-mult-02, div-ls-same, div-ls, div-le-same, div-le-pos, div-est-num, div-est-nls, div-est-nle-pos, div-est-denom-pos, div-eq-zero, div-eq-same-01, div-elim-pos, div-div-pos, div-am-rew, div-addthree-rew, div-add1-posneg-pos-01, div-add1-negpos-pos, div-add-pos, add-div-mult,
int-mult/zero-ge-add-01 is used by square-inject, modex-odd, mod-twoodd-01, div2-nle-02, div-two-intro, div-shift-two, div-am-rew,
int-mult/zero-gr is used by two-odd, square-nls, square-nle, square-interval, nummult-ls-02, num-ls, mult-02, modmod-pos, modmod-mult-04, modmod-add2-posneg-pos, modmod-add2-negpos-pos-01, modeq-pos-04, modeq-pos-03, mod2-add-neg, mod-zero-01, mod-two-03, mod-sub-02, mod-rec, mod-mod-less, mod-ls-same-01, mod-add1-posneg-pos, mod-add-zero, mod-add-01, ls-same-pos-02, ls-same-pos, less-mult-div-01, is-div, estimate-01, div-two-intro, div-nearer-zero, div-mult-two-nls-01, div-mult-nls-est, div-mult-02, div-ls-mone, div-ls, div-lezero, div-est-nle-pos, div-eq-same-01, div-div-pred, div-add1-posneg-pos-01,
int-mult/zero-gr-01 is used by mod-zero-06, mod-ls-same-01, div-nearer-zero, div-mult-three-nls,
int-mult/zero-gr-02 is used by square-interval, le-abs-numerator,
int-mult/zero-gr-add is used by mod-zero-05, div-zero-01, div-ngr-zero, div-ls-zero, div-eq-zero-01,
int-mult/zero-gr-add-01 is used by mod-ls-same-02, div-eq-zero-01,
int-mult/zero-le is used by nummult-modle-01, mod-nle, ls, div2-odd-01, div-ls-mone,
int-mult/zero-le-01 is used by zero,
int-mult/zero-left is used by square-inject, nummult-modls-01, nummult-modle-01, nummult-eq, mult-split-mod, mult-01, modmod-mult-03, modmod-mult, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-neg, modeq-pos-04, modeq-pos, mod-zero-one, mod-zero-04, mod-sub-02, mod-shift, mod-nle, mod-mult-pos, mod-mult-neg, mod-div-ls, less-mult-div-01, less-mult-div, div-ngr-zero, div-nearer-zero, div-mult-shift-holds, div-mult-pos-01, div-mult-neg, div-mult-ls, div-mult-01, div-minus-onediff, div-ls-zero, div-ls-modzero, div-le-same-neg, div-eq-zero-01, div-eq-zero, div-elim3, div-elim2, div-elim1, div-div-switch, div-div-pred-01, div-am-rew, div-addthree-rew, div-add-succ, add-div-mult,
int-mult/zero-ls is used by nummult-modls-01, nummult-ls-03, nummult-ls-01, nummult-le-03, nummult-le-01, mult-ls, modmod-mult-04, modmod-ma-negpos-neg, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add, modex, modeven-neg, modeq-neg-02, mod-succ-01, mod-pred-neg, mod-pred-02, mod-ls-same-02, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-zero, mod-add-neg, ls-even-01, less-mult-div-01, exeven, even-not, div2-nls-02, div2-add-neg, div-twoodd-07, div-twoodd-04, div-twoodd-02, div-two-intro, div-nearer-zero, div-minus-onediff-01, div-minus-onediff, div-ls-same, div-ls-mone, div-le-pos, div-div-pred-01, div-div-pred, div-add1-negpos-pos, div-add1-negpos-neg-01, div-add-neg,
int-mult/zero-ls-01 is used by modex, mod-ls-same-02, mod-ls-same-01, le-abs-numerator, div-nearer-zero, div-eq-zero-01,
int-mult/zero-ls-02 is used by modmod-ma-negpos-neg, div-mult-nls-zero,
int-mult/zero-neq is used by modmod-mult-05, div-mult-01, div-div,
int-mult/zero-neq-01 is used by modmod-mult-03, modmod-add-law-pos, modmod-add-case, mod-zero-07, mod-zero-05, mod-zero-03, mod-twoodd-03, mod-add-zero, less-mult-div-01, div-twoodd-07, div-twoodd-05, div-twoodd-04, div-twoodd-03, div-twoodd-02, div-two-intro, div-mult-01, div-div-pred, div-div, abs-shift-01, abs-shift,

Used from specification int-abs

int-abs/Abs-neg is used by one-neg, modex-odd-neg, mod-two-pred-01, mod-ls-same-01, mod-div-zero, mod-add1-negpos-neg, div2-nls-02, div2-nls, div-nearer-zero, div-ls-zero, div-ls-mone, abs-shift-01, abs-shift,
int-abs/Abs-pos is used by mod-nls-04, mod-abs, abs-shift-01, abs-shift, abs,
int-abs/abs-08 is used by div-div,
int-abs/add-rew is used by nummult-ls-03,
int-abs/add-shift is used by nummult-ls-03,
int-abs/ex-le-add is used by less-mult-div-01,
int-abs/forward-lele is used by square-nle-02,
int-abs/forward-lsle is used by square-nls, square-nle,
int-abs/gr-def is used by mod-add-zero,
int-abs/le-def is used by nummult-le-01, modex, mod-ls-same-02, mod-ls-same-01, ls-even-01, div-sum-ls, div-ls-zero, div-le-modzero-01, div-le-modzero, div-le-modnotzero-01,
int-abs/le-rec is used by mod-nls-04,
int-abs/lels is used by nummult-ls-03, ls-even-01, div-ls-same,
int-abs/lels-04 is used by div-ls-same,
int-abs/minus-02 is used by div-twoodd-01,
int-abs/mone-07 is used by div2-add-neg,
int-abs/neg-06 is used by mod-div-zero,
int-abs/neg-13 is used by mod-ls-same-02,
int-abs/numadd is used by square-inject,
int-abs/numadd-01 is used by div2-add-neg, div-div-pred-01,
int-abs/numle-02 is used by mod-div-zero,
int-abs/ple-03 is used by div-add1-posneg-pos-01, div-add1-negpos-neg-01,
int-abs/ple-04 is used by div-ls-same,
int-abs/rew-eqzero is used by mod-neq-01,
int-abs/zero-ge-01 is used by div-div-pred-01,
int-abs/zero-gs is used by le-abs-numerator,
int-abs/Abs-pos is used by modex-odd-neg, mod-two-pred-01, mod-ls-same-01, mod-div-zero, mod-add1-negpos-neg, div2-nls-02, div2-nls, div-nls-01, div-nearer-zero, div-ls-zero, div-ls-mone, div-eq-zero-01, div-div-pred-01, div-div, abs-shift-01, abs-shift,
int-abs/Sub-def is used by two-odd, two-mult-01, nummult-ls-03, nummult-le-01, mult-03, modmod-add2-posneg-neg-01, modmod-add-if, modmod-add-case, modex-odd-neg-01, modeq-pos-01, mod-twoodd-03, mod-two-pred-02, mod-sub-01, mod-sub, mod-nls-04, mod-mult-neg-01, mod-by6, minus-add, even-not-ex, div2-odd-01, div2-nls-02, div2-nls, div2-nle-02, div2-add-neg, div-twoodd-03, div-two-intro, div-sub-01, div-sub, div-rec-01, div-minus255-256, div-minus-onediff, div-add1-posneg-pos-02, div-add-succ-neg, div-add-succ, div-add-nosucc-neg,
int-abs/abs-01 is used by div-abs, abs-02, abs-01,
int-abs/abs-03 is used by le-abs-numerator, div-zero-nls-01, div-div-pred, div-div,
int-abs/abs-05 is used by div2-add-neg, div-minus-onediff,
int-abs/abs-06 is used by one-neg, mod-nls-04, mod-mult-neg-02, le-abs-numerator, div-zero-nls-01, div-zero-02, div-two-intro, div-eq-zero-01, div-elim2, div-elim-negpos, div-div-pred-01, div-div-pred, div-div, abs-div10-le,
int-abs/abs-07 is used by div-nearer-zero, div-div, div-abs, abs-shift, abs-01, abs,
int-abs/abs-08 is used by one, mult-01, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add-if, modmod-add-case, modex, modeven-neg-01, modeven-neg, modeq-pos-03, modeq-pos-01, modeq-neg-02, mod2-neg-odd, mod2-add-neg, mod-zero-06, mod-zero-05, mod-pred-neg-01, mod-pred-neg, mod-nls-06, mod-nls-04, mod-nls-03, mod-nle-02, mod-mult-neg-02, mod-mult-neg, mod-lsz, mod-ls-same-02, mod-ls-same-01, mod-lezero, mod-grz-01, mod-div-zero, mod-add1-posneg-pos, mod-add-01, mod-abs, ls-even-01, letwozero, le-abs-numerator, exeven, even-not-ex, div2-zero, div2-notzero, div2-add-neg, div-zero-ngr-01, div-zero-02, div-zero-01, div-twoodd-07, div-two-intro, div-nls-01, div-ngr-zero, div-mult-neg, div-minus255-256-01, div-minus-onediff-01, div-minus-onediff, div-ls-same, div-eq-zero-01, div-eq-same-01, div-elim2, div-elim1, div-elim-posneg, div-elim-negpos, div-div-pred-01, div-div-pred, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-nosucc-neg, abs-shift-01, abs-shift, abs-intro, abs,
int-abs/abs-16 is used by nls-mult-div, modmod-pos, modmod-add2-posneg-neg-01, modmod-add2-negpos-pos-01, modmod-add-if, modmod-add-case, modeq-neg-02, mod-zero-ls, mod-zero-09, mod-sub-01, mod-nls-06, mod-ls-same-02, mod-ls-same-01, mod-div-zero, mod-add1-negpos-neg, div-twoodd-05, div-nearer-zero, div-minus-onediff-01, div-minus-onediff, div-le-modnotzero, div-eq-zero-01, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-nosucc-neg, abs-shift, abs-intro,
int-abs/abs-18 is used by abs,
int-abs/abs-neg is used by mod-sub-01, mod-mult-neg-01,
int-abs/abs-one-01 is used by one-pos,
int-abs/abs-zero is used by mod2-add-neg, div-le-same-neg, div-div-pred,
int-abs/abseq is used by abs,
int-abs/absle is used by nummult-le-02, nummult-le, num-ls, mult-ls-01, mult-ls, modmod-pos, mod-mult-pos, mod-mult-neg-01, ls-01, leone-two, le-abs-numerator, diveq-pos, div-zero-02, div-mult-nls-est, div-mult-nle-est, div-ls, div-le-pos, div-est-num, div-est-nls, div-est-nle-pos, abs-intro,
int-abs/absls is used by mod-zero-05, le-abs-numerator, diveq-neg, div-elim2, div-elim-negpos,
int-abs/absls-01 is used by mod-zero-05, mod-nls-06, mod-ls-same-02,
int-abs/absls-03 is used by one-neg,
int-abs/absls-06 is used by one-neg, mod-mult-neg-02, div-zero-02,
int-abs/anti is used by two-add-square, square-nls-02, square-nle, square-interval, prod-div-less, nummult-ls-01, nummult-le-03, nummult-le, num-ls, mult-split-mod, modmod-add2-posneg-pos, modmod-add2-posneg-neg, modex-odd-neg, mod-two-pred-01, mod-succ-01, mod-sub-01, mod-nle, mod-next-square, mod-ls-same-02, mod-ls-same-01, mod-add1-negpos-neg, mod-add-neg, mod-add-01, ls-even-01, ls, less-mult-div-01, div2-nls-02, div2-nls, div-nls-01, div-ngr-zero, div-mult-shift-holds, div-mult-nls-est, div-ls-zero, div-ls-mone, div-ls, div-le-same-neg, div-le-pos, div-le-modnotzero, div-est-nle-pos, div-eq-zero-01, div-eq-same-01, div-div-pred-01, div-add1-negpos-neg-02,
int-abs/bet is used by one-neg, mod-zero-one, leone-two, div-mult-three-nls, div-minus-onediff-01, div-ls-same, div-add1-posneg-pos-02,
int-abs/bet-01 is used by square-nls, square-nle-01, square-nle, div-ls-mone,
int-abs/elim-sub is used by sub-ls-01, nummult-ls-03, nummult-ls, nummult-le-02, modex-odd-neg-01, mod-rec-01, mod-rec, mod-pred-neg-01, mod-pred-neg, mod-pred-02, mod-pred-01, mod-pred, mod-ls-same-02, mod-by6, even-add, div2-notzero, div2-add-neg, div-two-intro, div-rec, div-minus-onediff-01, div-minus-onediff, div-le-same-neg, div-eq-zero-01, div-eq-same-01, div-div-pred-01, div-div-pred, div-add1-posneg-pos-02, div-add-nosucc,
int-abs/forward-le is used by square-nle, prod-div-less, modmod-add2-negpos-pos-01, modmod-add-if, modeq-pos-04, mod-sub-01, mod-rec, mod-nls-04, mod-nle-01, mod-mult-neg-02, mod-ls-same-01, mod-div-ls, lsf-02, lsf-01, ls, less-mult-div-01, div2-nle-02, div-sum-ls, div-rec, div-mult-two-nls-01, div-mult-three-nls, div-ls, div-lezero, div-le-same, div-eq-zero-01, div-elim2, div-elim-negpos, div-div-pred, div-add1-posneg-pos-01,
int-abs/forward-le-01 is used by square-nls-02, square-nls-01, square-nls, square-nle-02, square-nle-01, square-nle, square-ls-01, square-ls, square-interval, square-inject, square-even, prod-div-less, one-neg, nummult-ls-02, nummult-ls, nummult-le-02, nummult-le, num-ls, nls-mult-div, mult-split-mod, mult-ls-01, mult-ls, mult, modmod-pos, modmod-mult-07, modmod-mult-02, modmod-mult, modmod-ma-negpos-neg, modmod-ma-01, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-04, modmod-add-01, modmod-add, modex-odd-neg, modeq-pos, modeq-neg-02, mod2-add-neg, mod-zero-one, mod-zero-07, mod-zero-06, mod-zero-02, mod-zero-01, mod-twoodd-02, mod-twoodd-01, mod-succ-02, mod-succ-01, mod-sub-02, mod-sub-01, mod-shift, mod-rec-01, mod-rec, mod-pred-04, mod-pred-03, mod-pred-02, mod-pred-01, mod-nls-05, mod-nls-04, mod-nls-03, mod-nle-01, mod-nle, mod-mult-pos-01, mod-mult-pos, mod-mod-less, mod-ls-same-02, mod-ls-same-01, mod-div-zero, mod-div-ls, mod-by6, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-zero, mod-add, lsfc-02, lsf-01, ls-same-pos-02, ls-same-pos-01, ls-same-pos, ls-even-01, ls-03, ls-02, ls-01, ls, less-mult-div-01, leone-two, le-norest, le-abs-numerator, is-div, exodd, even-or-succ-even, even-not-ex, estimate-01, diveq-pos, div2-nls-02, div2-nls, div2-nle-02, div2-neg, div2-add-neg, div-zero-nls, div-zero-ngr-01, div-zero-05, div-zero-02, div-twoodd-06, div-twoodd-05, div-two-intro, div-sum-ls, div-shift-two, div-rec, div-nls, div-nle, div-nearer-zero, div-mult-two-nls-01, div-mult-three-nls, div-mult-shift-holds, div-mult-pos-01, div-mult-nls-zero, div-mult-nls-est-01, div-mult-nls-est, div-mult-nle-est, div-mult-ls, div-mult-le-01, div-mult-01, div-ls-zero, div-ls-same, div-ls-pos-mon, div-ls-mone, div-ls-modzero, div-ls-modnotzero, div-ls-02, div-ls, div-lezero, div-le-same-neg, div-le-pos, div-le-modzero-01, div-le-modnotzero-01, div-le-modnotzero, div-est-num, div-est-nls, div-est-nle-pos, div-est-denom-pos, div-eq-zero-01, div-eq-same-01, div-elim1, div-elim-pospos, div-elim-posneg, div-elim-pos, div-elim-negneg, div-div-pred-01, div-div-pred, div-div-pos, div-div, div-am-rew, div-addthree-rew, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ, div-add-nosucc, add-div-mult, abs-shift-01, abs-shift, abs,
int-abs/forward-le-02 is used by zero-06, zero-05, zero-03, zero-02, sub-ls-01, square-nls-01, square-interval, one-neg, one, nummult-ls-03, nummult-ls-01, nummult-le-03, mult-ls-01, mult-ls, modmod-mult-09, modmod-mult-07, modmod-mult-05, modmod-mult-03, modmod-mult-02, modmod-mult-01, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-03, modmod-add-01, modex-odd-neg-01, modex-odd-neg, modex-odd, modex, modeven-neg-01, modeven-neg, modeq-neg-02, modeq-neg, mod2-neg-odd, mod2-add-neg, mod-zero-one, mod-zero-ls, mod-zero-06, mod-zero-05, mod-zero-01, mod-twoodd-03, mod-two-pred-02, mod-two-pred-01, mod-rec-01, mod-pred-neg-01, mod-pred-neg, mod-not-less, mod-nls-06, mod-nls-04, mod-nls-02, mod-nle-02, mod-next-square, mod-mult-neg-02, mod-lsz-01, mod-lsz, mod-ls-zero, mod-ls-same-02, mod-ls-same-01, mod-lezero, mod-grz-02, mod-grz-01, mod-grz, mod-gez, mod-div-zero, mod-by6, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-01, lsfc-02, lsf-02, ls-even-01, ls-02, less-mult-div-01, leone-two, le-abs-numerator, exeven, even-not-ex, even-not, diveq-neg, div2-odd-01, div2-notzero, div2-nls-02, div2-nls, div2-neg-odd, div2-add-neg, div-zero-nls-01, div-zero-nls, div-zero-ngr-01, div-zero-ngr, div-zero-02, div-zero-01, div-twoodd-07, div-twoodd-05, div-twoodd-03, div-two-intro, div-same, div-rec-01, div-nls-01, div-ngr-zero, div-nearer-zero, div-mult-nls-zero, div-mult-01, div-minus255-256-01, div-minus255-256, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-lezero, div-le-same-neg, div-le-pos, div-est-num, div-eq-zero-01, div-eq-same-01, div-elim3, div-elim2, div-elim1, div-elim-pospos, div-elim-posneg, div-elim-negpos, div-elim-negneg, div-div-pred-01, div-div-pred, div-div, div-addthree-rew, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ-neg, div-add-nosucc-neg, abs-shift-01, abs-shift, abs,
int-abs/forward-le-03 is used by div2-neg, div-div-pred-01,
int-abs/forward-le-04 is used by square-nls-02, square-nle-02, square-interval, nummult-ls-03, nummult-ls-01, nummult-ls, nummult-le-03, nummult-le-02, mult-ls-01, mult-ls, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add-zero, modmod-add-if, modmod-add-case, modmod-add-03, modmod-add-02, modex-odd-neg-01, modex-odd-neg, modeven-neg, modeq-neg-02, modeq-neg, mod2-add-neg, mod-zero-05, mod-two-pred-01, mod-pred-neg-01, mod-pred-neg, mod-nls-04, mod-nls, mod-nle-02, mod-next-square, mod-mult-neg-02, mod-mult-neg, mod-ls-same-02, mod-ls-same-01, mod-lezero, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-neg, mod-add-01, ls-even-01, ls, less-mult-div-01, le-abs-numerator, exeven, even-not-ex, diveq-neg, div2-nls-02, div2-nls, div2-neg, div2-add-neg, div-zero-01, div-two-intro, div-nls-01, div-ngr-zero, div-mult-nls-zero, div-mult-neg, div-minus255-256-01, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-lezero, div-le-same-neg, div-le-pos, div-est-num, div-eq-zero-01, div-eq-same-01, div-elim2, div-elim-posneg, div-elim-negpos, div-elim-negneg, div-div-pred-01, div-div-pred, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-nosucc-neg,
int-abs/forward-le-05 is used by zero-07, zero-05, zero-03, zero-02, two-odd, sub-ls-01, sub-ls, square-nls, square-nle, square-interval, square-inject, square-even, prod-div-less, pdiv-ls, one-pos, one-04, nummult-modls-01, nummult-modls, nummult-modle-01, nummult-modle, nummult-ls-03, nummult-ls-02, nummult-ls-01, nummult-ls, nummult-le-03, nummult-le-02, nummult-le, num-ls, nls-mult-div, mult-split-mod, mult-ls-01, mult-ls, mult-05, mult-03, mult, modmod-pos, modmod-mult-07, modmod-mult-03, modmod-mult-02, modmod-mult, modmod-ma-negpos-neg, modmod-ma-01, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-law-pos, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-04, modex-odd-neg, modeven-pos, modeq-pos-04, modeq-pos, modeq-neg-02, modeq-neg, mod2-add-neg, mod-zero-one, mod-zero-ls, mod-zero-09, mod-zero-07, mod-zero-06, mod-zero-05, mod-zero-02, mod-zero-01, mod-twoodd-03, mod-twoodd-02, mod-twoodd-01, mod-two-06, mod-two-05, mod-two-03, mod-succ-02, mod-succ-01, mod-succ, mod-sub-02, mod-sub-01, mod-shift, mod-rec, mod-pred-neg-01, mod-pred-neg, mod-pred-04, mod-pred-03, mod-pred-02, mod-pred-01, mod-pred, mod-nls-05, mod-nls-04, mod-nls-02, mod-nls-01, mod-nls, mod-nle-02, mod-nle-01, mod-nle, mod-ngr, mod-ngez-01, mod-next-square, mod-mult-pos-01, mod-mult-pos, mod-mult-neg-02, mod-mult-neg, mod-mod-less, mod-lsz, mod-ls-zero, mod-ls-same-02, mod-ls-same-01, mod-lezero, mod-les, mod-le-num, mod-grz-02, mod-grz-01, mod-grz, mod-div-ls, mod-by6, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-zero, mod-add-01, mod-add, lsfc-02, lsfc-01, lsf-02, lsf-01, lsf, ls-succ, ls-same-pos-02, ls-same-pos-01, ls-same-pos, ls-even-01, ls-03, ls-02, ls-01, ls, letwo, less-mult-div-01, leone-two, le-norest, le-abs-numerator, is-div, even-not-ex, estimate-01, diveq-pos, diveq-neg, div2one, div2-nls-02, div2-nls, div2-nle-02, div-zero-nls, div-zero-ngr-01, div-zero-ngr, div-zero-02, div-zero-01, div-twoodd-05, div-twoodd-03, div-two-intro, div-sum-ls-01, div-sum-ls, div-shift-two, div-rec, div-nls, div-nle, div-ngr-zero, div-nearer-zero, div-mult-two-nls-01, div-mult-three-nls, div-mult-shift-holds, div-mult-pos-01, div-mult-nls-zero, div-mult-nls-est-01, div-mult-nls-est, div-mult-nle-est, div-mult-neg, div-mult-ls, div-mult-le-01, div-mult-01, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-pos-mon, div-ls-mone, div-ls-modzero, div-ls-modnotzero, div-ls-02, div-ls, div-lezero, div-le-same-neg, div-le-same, div-le-pos, div-le-modzero-01, div-le-modzero, div-le-modnotzero-01, div-le-modnotzero, div-est-num, div-est-nls, div-est-nle-pos, div-est-denom-pos, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-elim2, div-elim-pospos, div-elim-pos, div-elim-negpos, div-elim, div-div-pred, div-div-pos, div-div, div-am-rew, div-addthree-rew, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ-neg, div-add-succ, div-add-nosucc-neg, div-add-nosucc, add-div-mult, abs-shift,
int-abs/forward-lele is used by zero-04, square-nls-02, square-nle-02, square-interval, nummult-ls, nummult-le-02, mult-ls-01, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add-if, modmod-add-case, modex-odd-neg, modeq-pos-03, modeq-neg-02, mod2-add-neg, mod-nls-04, mod-nle-01, mod-ls-same-02, mod-ls-same-01, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-neg, mod-add-neg, ls-even-01, ls-01, ls, le-abs-numerator, estimate-01, diveq-pos, div2-neg-01, div2-neg, div2-add-neg, div-sum-ls, div-mult-nls-zero, div-mult-nle-est, div-ls-zero, div-ls-pos-mon, div-ls-mone, div-ls, div-lezero, div-le-same-neg, div-est-nls, div-eq-same-01, div-elim-posneg, div-elim-negneg, div-div-pred-01, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-neg,
int-abs/forward-lels is used by zero-04, sub-ls, square-nle, square-interval, one-neg, nummult-ls-03, nummult-ls-02, nummult-ls-01, nummult-ls, nummult-le-03, nummult-le-02, nummult-le-01, nls-mult-div, mult-ls-01, mult-ls, mult-02, modmod-mult-04, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add-zero, modmod-add-if, modmod-add-case, modmod-add, modeq-pos-03, modeq-pos-02, modeq-neg-02, modeq-neg, mod2-add-neg, mod-zero-05, mod-zero-01, mod-sub-02, mod-rec-01, mod-pred-neg-01, mod-pred-neg, mod-not-less, mod-nls-06, mod-nls-05, mod-nls-04, mod-nls-03, mod-nls-01, mod-nle-02, mod-mult-neg-02, mod-mult-neg, mod-ls-same-02, mod-ls-same-01, mod-lezero, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-neg, mod-add-pos, mod-add-neg, mod-add-01, ls-same-pos-02, ls-even-01, ls-02, ls-01, ls, less-mult-div-01, leone-two, le-abs-numerator, is-div, estimate-01, diveq-pos, diveq-neg, div2-nls, div2-nle-02, div2-neg-01, div-zero-05, div-zero-02, div-zero-01, div-rec-01, div-nls-01, div-nls, div-nle, div-ngr-zero, div-nearer-zero, div-mult-three-nls, div-mult-nls-zero, div-mult-nls-est, div-mult-nle-est, div-mult-neg, div-mult-02, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-pos-mon, div-ls-mone, div-ls, div-lezero, div-le-same-neg, div-le-pos, div-est-num, div-eq-zero-01, div-eq-same-01, div-elim2, div-elim-negpos, div-div-pred, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-pos, div-add-nosucc-neg, div-add-neg,
int-abs/forward-lsle is used by zero-04, square-nls-01, square-nle, square-interval, pdiv-ls, one-neg, nummult-ls-03, nummult-ls-02, nummult-le-01, num-ls, modmod-mult-07, modmod-mult-04, modmod-mult-02, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-01, modmod-add, modeq-pos-03, modeq-neg-02, mod2-add-neg, mod-zero-one, mod-zero-ls, mod-zero-06, mod-zero-05, mod-zero-02, mod-zero-01, mod-succ-01, mod-rec-01, mod-rec, mod-pred-02, mod-nls-05, mod-nls-04, mod-nls-02, mod-nls-01, mod-mult-neg-02, mod-ls-same-02, mod-ls-same-01, mod-ls-same, mod-les, mod-div-zero, mod-div-ls, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-zero, mod-add-pos, mod-add-neg, lsfc-02, lsf-02, ls-even-01, ls-02, ls-01, ls, letwo, less-mult-div-01, le-abs-numerator, diveq-neg, div2-nls-02, div2-nls, div2-nle-02, div2-neg-01, div2-add-neg, div-zero-nls, div-zero-ngr-01, div-zero-02, div-two-intro, div-sum-ls, div-nle, div-nearer-zero, div-mult-two-nls-01, div-mult-three-nls, div-mult-nls-zero, div-mult-nls-est, div-mult-01, div-minus-onediff-01, div-ls-same, div-ls, div-lezero, div-le-same-neg, div-le-pos, div-est-num, div-est-nle-pos, div-est-denom-pos, div-eq-zero-01, div-eq-same-01, div-elim2, div-elim1, div-elim-pospos, div-elim-posneg, div-elim-negpos, div-elim-negneg, div-div-pred-01, div-div-pred, div-div, div-addthree-rew, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-pos, div-add-neg, abs-shift,
int-abs/ge-def is used by mod-zero-one, mod-add-zero,
int-abs/gr-def is used by mod-zero-one, mod-less, mod-add-zero,
int-abs/int-add-pos-01 is used by one-neg,
int-abs/int-simp-06 is used by square-nls,
int-abs/int-simp-07 is used by square-nle,
int-abs/le-add is used by nummult-ls-03,
int-abs/le-add-03 is used by square-nle-01,
int-abs/lels is used by zero-04, zero-01, two-add-square, sub-ls, square-nls-02, square-nls, square-nle, square-interval, prod-div-less, pdiv-ls, one-pos, one-neg, nummult-ls-03, nummult-ls-02-01, nummult-ls-02, nummult-ls-01-01, nummult-ls-01, nummult-ls, nummult-le-02, nummult-le-01, num-ls, mult-ls-01, mult-ls, mult-02, modmod-pos, modmod-mult-07, modmod-mult-02, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-02, modmod-add2-posneg-neg, modmod-add2-negpos-pos-02, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-04, modex-odd-neg, modex, modeq-neg-02, mod2-add-neg, mod-zero-one, mod-zero-09, mod-zero-05, mod-two-pred-01, mod-sub-01, mod-pred-neg-01, mod-pred-neg, mod-pred-03, mod-pred-02, mod-nls-04, mod-nle-02, mod-next-square, mod-mult-pos, mod-mult-neg-02, mod-mult-neg, mod-lsz-01, mod-lsz, mod-ls-zero, mod-ls-same-02, mod-ls-same-01, mod-ls-same, mod-less-01, mod-div-zero, mod-div-ls, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-zero, mod-add-neg, mod-add-01, lsfc-02, lsfc-01, lsf-02, lsf-01, lsf, ls-same-pos-01, ls-even-01, ls-02, ls, less-mult-div-01, less-mult-div, leone-two, le-abs-numerator, estimate-01, diveq-neg, div2-nls-02, div2-nls, div2-neg, div-zero-06, div-zero-02, div-twoodd-07, div-twoodd-05, div-two-intro, div-sum-ls-01, div-sum-ls, div-shift-two, div-nls-01, div-nls, div-ngr-zero, div-nearer-zero, div-mult-two-nls-01, div-mult-three-nls, div-mult-three, div-mult-nls-est, div-mult-neg, div-mult-ls-pos, div-mult-01, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-pos-mon, div-ls-pos-better, div-ls-mone, div-ls-modzero, div-ls-01, div-ls, div-lezero, div-le-modzero-01, div-le-modnotzero, div-est-num, div-est-nls, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-elim2, div-elim-negpos, div-div-pred-01, div-div-pred, div-div, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-neg, abs-shift-01, abs-shift, abs,
int-abs/lels-01 is used by zero-07, zero-06, zero-05, zero-04, zero-03, zero-02, two-add-square-01, sub-ls-01, square-nls, square-nle, square-interval, square-inject, square-even-01, prod-div-less, pos, one, nummult-ls-03, nummult-le-03, nummult-le, mult-03, modmod-mult-07, modmod-mult-04, modmod-mult-03, modmod-mult-02, modmod-ma, modmod-add2-posneg-pos, modmod-add2-negpos-pos-01, modmod-add-zero, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-04, modmod-add-03, modmod-add, modex-odd-neg, modex-odd, modex, modeven-pos, modeq-pos-01, modeq-neg-02, mod2-add-neg, mod-zero-one, mod-zero-ls, mod-zero-05, mod-zero-02, mod-zero, mod-two-06, mod-succ-01, mod-pred-neg, mod-pred-02, mod-nls-06, mod-nls-05, mod-nls-02, mod-nls-01, mod-ngr, mod-ngez-01, mod-next-square, mod-neq, mod-mult-pos-01, mod-mult-neg-02, mod-ls-same-02, mod-les, mod-le-num, mod-le-01, mod-le, mod-gez, mod-div-ls, mod-by6, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-pos, ls-succ, ls-same-pos, ls-even-01, ls-03, ls-01, ls, leone-two, le-abs-numerator, exeven, even-not-ex, even-not, div2-nls-03, div2-nls-02, div2-nls-01, div2-nls, div2-nle-02, div2-add-neg, div-zero-02, div-two-zero-01, div-two-intro, div-sum-ls-01, div-sum-ls, div-nearer-zero, div-mult-nls-est-01, div-mult-nle-est, div-mult-le, div-minus-onediff-01, div-ls-mone, div-lezero, div-le-same, div-le-pos, div-le-modzero, div-le-modnotzero, div-est-num, div-est-nle-pos, div-est-denom-pos, div-eq-zero, div-eq-same, div-elim-pospos, div-elim-negpos, div-elim-negneg, div-elim, div-div-pred, div-addthree-rew, div-add1-posneg-pos-01, div-add1-negpos-neg-01, div-add-succ, div-add-pos, div-add-nosucc, add-div-mult, abs,
int-abs/lels-02 is used by zero, square-nls, square-nle, square-interval, square-even, one-neg, one, nummult-le-01, nls-mult-div, modmod-pos, modeven-neg-01, modeven-neg, modeq-pos-03, modeq-neg-02, mod2-neg-odd, mod2-add-neg, mod-zero-07, mod-zero-05, mod-zero-03, mod-zero-02, mod-two-06, mod-pred-neg-01, mod-pred-neg, mod-pred-02, mod-ngr, mod-ngez-01, mod-neq, mod-mult-neg-02, mod-ls-same-02, mod-ls-same-01, mod-lezero, mod-gez, mod-by6, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-zero, mod-add-01, ls-03, ls-02, ls-01, le-abs-numerator, is-div, even-not-ex, diveq-pos, div2-zero, div2-add-neg, div-zero-01, div-zero, div-two-intro, div-sum-ls, div-shift-two, div-ngr-zero, div-mult-three-nls, div-mult-le-01, div-minus-onediff, div-ls-modnotzero, div-ls, div-le-same-neg, div-le-modnotzero, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-elim2, div-elim-negpos, div-div-pred-01, div-div-pred, div-add1-posneg-pos-01, div-add1-negpos-neg-01, div-add-succ, abs-shift-01,
int-abs/lels-03 is used by zero-07, zero-05, zero-03, zero-02, square-nls, square-interval, prod-div-less, one, nummult-ls, nummult-le-03, nummult-le-02, nummult-le-01, nummult-le, mult-ls-01, mult-ls, modmod-pos, modmod-mult-07, modmod-add2-posneg-neg-02, modmod-add2-negpos-pos-02, modmod-add-if3, modmod-add-case, modeq-pos-04, mod-zero-one, mod-zero-09, mod-zero-07, mod-zero-03, mod-succ-01, mod-pred-neg, mod-neq, mod-mult-pos, mod-mult, mod-ls-same-02, mod-ls-same-01, mod-grz-02, mod-grz-01, mod-grz, mod-div-ls, mod-add-zero, ls-same-pos-02, ls-same-pos, ls-even-01, ls-02, ls-01, less-mult-div-01, less-mult-div, le-abs-numerator, is-div, estimate-01, div2-nls-02, div2-nls, div2-add-neg, div-zero-nls, div-zero-ngr-01, div-zero-ngr, div-zero-06, div-zero-02, div-zero, div-twoodd-05, div-sum-ls, div-shift-two, div-ngr-zero, div-nearer-zero, div-mult-three-nls, div-mult-nls-est-01, div-mult-nle-est, div-mult-le-01, div-minus-onediff-01, div-ls-zero, div-ls-same, div-ls-mone, div-ls-modzero, div-ls-02, div-ls, div-le-pos, div-le-modnotzero, div-est-num, div-est-nls, div-eq-zero-01, div-eq-zero, div-elim3, div-elim2, div-div-pred-01, div-div-pred, div-add1-posneg-pos-01, div-add1-negpos-neg-02, div-add1-negpos-neg-01,
int-abs/lels-04 is used by nummult-le-01, modmod-mult-04, modmod-add-04, modmod-add, modex-odd-neg, mod-mult-neg-02, mod-ls-same-02, mod-ls-same, mod-add-pos, mod-add-01, div2-neg-01, div-sum-ls, div-shift-two, div-add-pos,
int-abs/lenls is used by square-interval, pdiv-ls, nummult-ls-03, nummult-ls-02, nummult-ls-01, nummult-ls, nummult-le-03, nummult-le-02, nummult-le, num-ls, mult-split-mod, mult-01, modmod-ma-negpos-neg, modmod-add2-posneg-pos, modmod-add2-negpos-pos-01, modmod-add-if3, modmod-add-if, modex, modeq-pos, modeq-neg-02, mod-zero-one, mod-zero-06, mod-succ-01, mod-pred-neg-01, mod-pred-neg, mod-pred-02, mod-not-less, mod-nls-05, mod-nls-04, mod-nle-02, mod-mult-pos, mod-mult-neg, mod-ls-same-01, mod-lezero, mod-les, mod-div-zero, mod-div-ls, mod-add1-posneg-pos, mod-add1-negpos-neg, lsfc-02, lsfc-01, lsf-02, lsf-01, lsf, ls-same-pos-01, ls-01, less-mult-div-01, le-abs-numerator, div2-nle-02, div-sum-ls-01, div-nls-01, div-nls, div-nle, div-mult-shift-holds, div-mult-nls-zero, div-mult-nls-est, div-mult-neg, div-ls-zero, div-ls-pos-mon, div-ls, div-lezero, div-le-pos, div-le-modzero, div-eq-zero-01, div-elim3, div-elim2, div-elim1, div-elim-pospos, div-elim-pos, div-elim-negpos, div-div-pred-01, div-div-pred, div-am-rew, div-addthree-rew, div-add1-posneg-pos-01, div-add1-posneg-neg, add-div-mult,
int-abs/leone is used by two-add-square, one-neg, nummult-ls-03, nummult-ls, nummult-le-02, mult-03, mult-02, modex, mod2-add-neg, mod-two-03, mod-by6, leone-two, div-add-succ, div-add-nosucc,
int-abs/lep is used by zero-04, sub-ls-01, square-inject, mod-rec-01, mod-rec, mod-ls-same-02, mod-add, div-rec, div-add-neg,
int-abs/lep-01 is used by square-nle-02, square-interval, mod-nle, mod-add1-negpos-neg, ls-even-01, ls, div-mult-le-01, div-ls-mone, div-le-modnotzero, div-add1-negpos-neg-01,
int-abs/lep-02 is used by modmod-add2-posneg-neg-01, mod-div-ls,
int-abs/ler is used by square-interval, prod-div-less, nummult-ls-03, nummult-ls-01, nummult-le-03, nummult-le-01, modmod-pos, mod-sub-02, mod-nle, mod-div-ls, ls-03, ls-02, is-div, diveq-pos, div-same, div-mult-le-01, div-ls-01, div-le-same, div-le-modnotzero, div-est-nle-pos,
int-abs/les is used by nummult-ls-03, nummult-le-01, mod-pred-03, mod-pred-02, diveq-pos,
int-abs/lsone is used by zero-05, square-interval, one-neg, nummult-ls-03, nummult-ls-01, nummult-le-03, nummult-le-01, mult-ls, modmod-add2-posneg-neg, modeq-pos-03, mod-two-pred-01, mod-pred-neg-01, mod-pred-neg, mod-nls-04, mod-nls, mod-mult, mod-ls-same-01, mod-add-neg, le-abs-numerator, even-not-ex, div2-nls-02, div-twoodd-03, div-twoodd-01, div-two-intro, div-nearer-zero, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-eq-zero-01, div-elim-posneg, div-div-pred-01, div-div-pred, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-neg,
int-abs/lstwo is used by square-inject, modex-odd-neg, mod-twoodd-02, div2-nls-02, div2-nls, div2-nle-02, div-shift-two,
int-abs/lstwo-01 is used by square-nls, square-nle,
int-abs/minus-02 is used by mod-two-pred-02, mod-nls-04, div-twoodd-03,
int-abs/minus-add is used by mod2-add-neg, mod-ls-same-02, even-not-ex, div2one-01, div2-nls-02, div2-nls, div-two-intro, div-ls-mone, div-div-pred-01, div-div-pred,
int-abs/minus-ass is used by mod-add1-posneg-pos, mod-add1-negpos-neg,
int-abs/minus-neg is used by div-add-succ-neg, div-add-nosucc-neg,
int-abs/minus-sub is used by mod-twoodd-03, div2-neg-odd, div-add-succ-neg, div-add-nosucc-neg,
int-abs/mone-05 is used by modex-odd-neg-01, modex-odd-neg, modeven-neg, mod-twoodd-03, mod-pred-neg-01, mod-pred-neg, ls-even-01, exeven, div2-add-neg, div-div-pred-01, div-div-pred,
int-abs/mone-06 is used by square-nls, square-nle, square-interval, one-neg, one, nummult-ls, nummult-le-02, mult-02, mod2-add-neg, mod-sub-02, mod-pred-neg, mod-pred-02, mod-pred-01, mod-pred, mod-nls-05, mod-ls-same-02, mod-ls-same-01, mod-div-ls, mod-by6, mod-add-01, le-abs-numerator, is-div, diveq-pos, div2-add-neg, div-twoodd-05, div-ls-same, div-ls-mone, div-le-same-neg, div-eq-zero-01, div-eq-same-01,
int-abs/mone-08 is used by one-neg, mod-ls-same-02, mod-by6, div-twoodd-07, div-twoodd-05, div-two-zero-01, div-minus-onediff, div-ls-mone,
int-abs/neg is used by zero-02, zero, modmod-mult-09, modmod-mult-05, modmod-mult-03, modmod-mult-01, modmod-add-law, modmod-add-01, modex, mod-rec-01, mod-nls-06, le-abs-numerator, div-zero-02, div-twoodd-07, div-twoodd-04, div-twoodd-02, div-two-intro, div-rec-01, div-nls-01, div-nearer-zero, div-mult-01, div-elim3, div-elim2, div-elim1, div-add-succ-neg,
int-abs/neg-01 is used by zero-05, lsf-02, ls-even-01, div-nearer-zero, div-elim3,
int-abs/neg-02 is used by zero, num-neg-01, num-neg, modnum-neg, modmod-mult-07, modmod-mult-02, mod-zero-06, mod-neg, mod-mult-neg, le-abs-numerator, div2-neg-odd, div-twoodd-07, div-twoodd-04, div-twoodd-03, div-twoodd-02, div-twoodd-01, div-two-intro, div-rec-01, div-nearer-zero, div-mult-neg, div-mult-01, div-elim3, div-elim1, div-div, div-add-nosucc-neg, abs-intro,
int-abs/neg-03 is used by mod-rec-01, minus-add, div2-odd-01, div-mone, div-ls-mone, abs-shift-01, abs-shift,
int-abs/neg-05 is used by zero-07, modeq-pos-04, mod-zero-06, mod-sub-01, le-abs-numerator, div-nls-01, div-nearer-zero, div-mult-neg, div-ls-mone, div-elim2,
int-abs/neg-06 is used by one-neg, modex-odd-neg, modeq-pos-04, mod-two-pred-01, mod-ls-same-01, mod-div-zero, mod-add1-negpos-neg, div2-nls-02, div2-nls, div-nearer-zero, div-ls-zero, div-ls-mone, abs-shift-01, abs-shift,
int-abs/neg-07 is used by one-neg, mult-01, mod-zero-06, mod-nls-04, mod-mult-neg-02, mod-ls-same-02, mod-ls-same-01, mod-div-zero, ls-even-01, le-abs-numerator, div-zero-ngr-01, div-zero-02, div-twoodd-07, div-nls-01, div-eq-zero-01, div-elim2, div-elim1, div-elim-posneg, div-elim-negpos,
int-abs/neg-10 is used by modmod-mult-03, modeq-pos-04, mod-rec-01, mod-neq-01, mod-neg, ls-even-01, div-zero-02, div-twoodd-07, div-twoodd-05, div-twoodd-01, div-two-intro, div-rec-01, div-nearer-zero, div-mult-01, div-elim3, div-div, div-add-succ-neg, div-add-nosucc-neg, abs-intro,
int-abs/neg-11 is used by modmod-add-02, mod-mult-neg, le-abs-numerator, div-nls-01, div-mult-neg, div-ls-mone, div-elim3, div-elim2,
int-abs/neg-12 is used by neg-01, neg, modmod-mult-03, modmod-mult-02, modmod-add-02, mod-sub-01, mod-sub, mod-pred-neg-01, mod-pred-neg, div-nearer-zero, div-mult-01, div-mone-01, div-elim3, div-elim2, div-elim1, div-div,
int-abs/neg-13 is used by one, modmod-add2-posneg-neg, modex-odd-neg, modeven-neg-01, modeven-neg, modeq-pos-03, modeq-pos-01, modeq-neg-02, mod2-neg-odd, mod2-add-neg, mod-zero-05, mod-two-pred-01, mod-pred-neg-01, mod-pred-neg, mod-nls-04, mod-nle-02, mod-mult-neg, mod-lsz, mod-ls-same-02, mod-ls-same-01, mod-lezero, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-01, ls-even-01, letwozero, even-not-ex, div2-zero, div2-notzero, div2-nls-02, div2-nls, div2-add-neg, div-zero-02, div-zero-01, div-two-intro, div-ngr-zero, div-mult-neg, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-eq-zero-01, div-elim2, div-elim-negpos, div-div-pred-01, div-div-pred, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-01,
int-abs/neg-15 is used by zero-07, one-neg, mult-01, modmod-add-law, modex, modeq-pos-04, mod-zero-06, mod-twoodd-03, mod-two-pred-02, mod-sub-01, mod-sub, mod-rec-01, mod-pred-neg-01, mod-pred-neg, mod-nls-04, mod-nls, mod-mult-neg-01, mod-ls-same-02, mod-div-zero, mod-div-ls, minus-add, ls-02, le-abs-numerator, div2-odd-01, div2-neg-odd, div-twoodd-03, div-twoodd-01, div-rec-01, div-nls-01, div-ls-mone, div-eq-zero-01, div-div, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-01, div-add-succ-neg, div-add-nosucc-neg, abs,
int-abs/negeq is used by mult-01, modex, mod2-add-neg, mod-zero-06, mod-sub-01, mod-sub, mod-rec-01, mod-neg-01, mod-mult-neg-01, mod-ls-same-02, mod-ls-same-01, div2-odd-01, div-twoodd-03, div-twoodd-01, div-mone, div-elim3, div-elim2, div-div-pred-01, div-div, div-add-nosucc-neg, abs-shift-01, abs-shift, abs,
int-abs/negle-07 is used by zero-05, zero-02, modmod-mult-07, modmod-mult-03, modmod-mult-02, modmod-add2-posneg-neg-01, modmod-add-if, modmod-add-case, modmod-add-02, modeven-neg, mod-twoodd-03, mod-sub, mod-pred-neg-01, mod-pred-neg, mod-nls-03, mod-nle-02, mod-mult-neg-02, mod-mult-neg, mod-grz-01, mod-add-01, lsf-02, ls-even-01, ls-02, le-abs-numerator, exeven, div2-odd-01, div-twoodd-03, div-twoodd-01, div-nls-01, div-nearer-zero, div-mult-neg, div-mult-01, div-minus255-256-01, div-minus-onediff-01, div-elim3, div-elim2, div-elim-negpos, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-nosucc-neg,
int-abs/negle-13 is used by zero-07, modex, mod2-add-neg, mod-zero-06, mod-rec-01, mod-nls-06, mod-mult-neg-01, mod-div-zero, ls-02, le-abs-numerator, div2-add-neg, div-rec-01, div-nls-01, div-eq-same-01, div-add1-posneg-pos-01, div-add1-negpos-neg-01,
int-abs/num-between is used by div-div-pred-01,
int-abs/numadd is used by nummult-ls, nummult-le-02, modex-odd, modby6-help, mod-pred, exodd, even-mult, div2one-01, div-minus-onediff-01, div-minus-onediff, div-add1-posneg-pos-02, div-add1-negpos-neg-02, div-add-succ-neg, div-add-succ, div-add-nosucc-neg, div-add-nosucc,
int-abs/numadd-01 is used by square-nls, square-nle, modex, mod-zero-06, mod-two-01, mod-succ-02, mod-pred-04, mod-pred-03, mod-next-square, mod-ls-same-02, mod-ls-same-01, mod-div-ls, mod-add-01, div2-add-neg, div-mone, div-le-same-neg, div-eq-zero-01, div-eq-same-01, div-div-pred-01, div-div-pred, div-add-nosucc,
int-abs/numle-02 is used by square-nls, square-nle-01, square-nle, square-ls-02, square-ls-01, square-ls, square-even, nummult-ls, nummult-le-02, mod-succ-01, mod-pred-03, mod-pred-02, mod-nls-06, mod-ls-same-02, mod-by6, diveq-pos, div2-add-neg,
int-abs/numle-03 is used by modex-odd-neg-01, modex-odd-neg, modeven-neg, mod-twoodd-03, mod-pred-neg-01, mod-pred-neg, ls-even-01, leone-two, exeven, div2-neg, div2-add-neg, div-minus255-256-01, div-div-pred-01, div-div-pred,
int-abs/numlef-01 is used by one-neg, mult-02,
int-abs/numleledel is used by mod-pred-neg, ls-even-01, leone-two,
int-abs/numleledel-01 is used by square-nls, square-nle-01, square-nle, square-ls-02, square-ls-01, square-ls, square-even, nummult-ls, mod-succ-01, mod-pred-03, mod-pred-02, mod-nls-06, mod-by6, div-two-zero-01,
int-abs/numlelsdel is used by square-nls, square-nle, mult-ls, leone-two, div-nearer-zero, div-mult-three-nls, div-eq-zero-01, div-div-pred,
int-abs/numlelsdel-01 is used by one-lez, div-add1-negpos-neg-02, div-add-succ-neg, div-add-nosucc-neg,
int-abs/numls-01 is used by div-le-same-neg, div-eq-zero-01, div-eq-same-01,
int-abs/numls-02 is used by square-nls, square-nle, square-interval, one, nummult-ls, nummult-le-02, modex-odd-neg, modeven-neg-01, modeven-neg, mod2-neg-odd, mod2-add-neg, mod-two-pred-01, mod-sub-02, mod-pred-neg, mod-pred-02, mod-pred-01, mod-pred, mod-nls-05, mod-ls-same-02, mod-ls-same-01, mod-div-ls, mod-by6, mod-add-01, letwozero, leone-two, le-abs-numerator, is-div, even-not-ex, div2-zero, div2-notzero, div2-nls-02, div2-nls, div2-add-neg, div-two-intro, div-mult-three-nls, div-ls-same, div-le-same-neg, div-eq-zero-01, div-eq-same-01, div-div-pred-01, div-div-pred, div-add-nosucc,
int-abs/numls-03 is used by zero-05, square-nle-01, square-interval, one-neg, nummult-ls-03, nummult-ls-01, nummult-le-03, nummult-le-01, mult-ls, modmod-mult-03, modmod-mult-02, modmod-add2-posneg-pos, modmod-add-if, modmod-add-case, mod-pred-neg-01, mod-pred-neg, mod-nls-04, mod-nls-02, mod-lsz, mod-ls-same-01, mod-add-01, lsf-02, ls-even-01, ls-02, div2-notzero, div-twoodd-07, div-twoodd-05, div-nearer-zero, div-mult-01, div-minus-onediff-01, div-minus-onediff, div-ls-mone, div-eq-zero-01, div-elim2, div-elim-negpos, div-div-pred-01, div-div-pred, div-add1-negpos-neg-02, div-add1-negpos-neg-01,
int-abs/numlsf-01 is used by modeq-pos-03,
int-abs/numlsf-02 is used by one-neg, mult-02,
int-abs/numlsledel is used by modex-odd-neg, mod-two-pred-01, leone-two, div2-nls-02, div2-nls, div-div-pred-01,
int-abs/numlslsdel-03 is used by div-ngr-zero,
int-abs/numsub is used by two-add-square, div-minus-onediff-01, div-div-pred-01, div-div-pred, div-add1-negpos-neg-02, div-add-nosucc-neg, div-add-nosucc,
int-abs/one-03 is used by mod-nls-04,
int-abs/sub-add is used by mod-add,
int-abs/sub-add-01 is used by two-add-square, square-inject, mult-03, modmod-add-law-pos, modeq-neg-02, mod-zero-06, mod-zero-01, mod-pred-neg-01, mod-pred-neg, mod-neg-01, mod-add1-posneg-pos, mod-add1-negpos-neg, div2-nls-02, div-mult-two-nls-01, div-minus-onediff-01, div-ls-mone, div-div-pred-01, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ-neg, div-add-succ, div-add-nosucc-neg, div-add-nosucc,
int-abs/sub-add-05 is used by div2-nls-02,
int-abs/sub-add-06 is used by mult-03,
int-abs/sub-add-09 is used by mod-rec-01,
int-abs/sub-eq is used by two-odd, two-mult-01, square-inject, one-neg, nummult-ls-03, nummult-ls, nummult-le-02, nummult-le-01, mult-05, mult-03, modmod-add2-negpos-pos-01, modmod-add-law-pos, modmod-add-law, modmod-add-if3, modmod-add-if, modmod-add-case, modex-odd-neg-01, modex-odd-neg, modeq-pos-04, modeq-pos, modeq-neg-02, mod2-add-neg, mod-twoodd-03, mod-twoodd, mod-two-pred-02, mod-two-pred-01, mod-sub-02, mod-sub-01, mod-sub, mod-rew, mod-pred-neg-01, mod-pred-neg, mod-pred-04, mod-pred-03, mod-pred-02, mod-nls-04, mod-neg, mod-mult-neg-01, mod-mult-02, mod-mult, mod-add1-posneg-pos, mod-add1-negpos-neg, minus-add, even-not-ex, divmult, div2one-01, div2-odd-01, div2-nls-02, div2-nls, div2-nle-02, div-twoodd-07, div-twoodd-05, div-twoodd-03, div-two-intro, div-sub-01, div-sub, div-rec-01, div-mult-two-nls-01, div-mult-rew-01, div-minus255-256, div-minus-onediff-01, div-minus-onediff, div-ls-mone, div-div-pred-01, div-div-pred, div-div, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-01, div-add-succ-neg, div-add-succ, div-add-nosucc-neg, abs,
int-abs/sub-le is used by mod-nls-04, mod-ls-same-02, div2-nls-02, div2-nls, div-eq-zero-01, div-div-pred-01, div-add1-posneg-pos-01, div-add1-negpos-neg-01,
int-abs/sub-le-01 is used by zero-07, two-add-square, square-inject, nummult-ls-03, nummult-ls, nummult-le-02, nummult-le-01, mult-03, modex, modeq-pos-04, modeq-neg-02, mod2-add-neg, mod-two-03, mod-rec-01, mod-pred-neg, mod-nls-04, mod-ls-same, mod-div-zero, mod-div-ls, mod-by6, mod-add1-posneg-pos, mod-add1-negpos-neg, ls-02, le-abs-numerator, div2-nle-02, div-rec-01, div-mult-two-nls-01, div-ls-mone, div-add1-posneg-pos-01, div-add1-negpos-neg-01, div-add-succ, div-add-nosucc,
int-abs/sub-ls is used by sub-ls, nummult-ls-03, nummult-le-01, mult-03, modeq-neg-02, mod-zero-06, mod-zero-01, mod-two-pred-01, mod-pred-neg, mod-nls-04, mod-nls, mod-div-ls, mod-add1-posneg-pos, mod-add1-negpos-neg, even-not-ex, div2-nls-02, div2-nls, div2-nle-02, div2-add-neg, div-twoodd-03, div-twoodd-01, div-two-intro, div-sum-ls, div-shift-two, div-nls-01, div-mult-two-nls-01, div-minus-onediff, div-ls-same, div-ls-mone, div-div-pred-01, div-div-pred, div-add1-posneg-pos-01, div-add1-negpos-neg-01, div-add-succ,
int-abs/sub-ls-01 is used by nummult-ls-03, nummult-ls-02, mod-nls-04, mod-nls, mod-ls-same, div2-nls-02, div-ls-mone, div-eq-zero-01,
int-abs/sub-minus is used by mod-rec-01, mod-neg-01, div-rec-01,
int-abs/sub-pred is used by mod-by6,
int-abs/sub-sub is used by mult-03, modmod-add-law-pos, modeq-neg-02, mod-add1-posneg-pos, mod-add1-negpos-neg, div-add1-posneg-pos-01, div-add1-negpos-neg-01, div-add-succ-neg, div-add-nosucc-neg,
int-abs/sub-sub-03 is used by one-01, mod-same, mod-neg-01, mod-mult-04, div-same,
int-abs/sub-sub-04 is used by div-minus-onediff-01, div-minus-onediff, div-add1-posneg-pos-02, div-add-succ-neg, div-add-nosucc-neg,
int-abs/sub-zero-01 is used by mult-01, modmod-add-if, mod-sub-01, mod-rec-01, div-rec-01,
int-abs/subneg is used by modmod-add-law,
int-abs/subsub is used by mod-twoodd-03, div2-add-neg, div-minus-onediff,
int-abs/succ-01 is used by square-nls, square-nle, nummult-ls-03, nummult-ls, nummult-le-02, nummult-le-01, div2-nls,
int-abs/succ-02 is used by square-ls-01, square-interval, nummult-ls-03, nummult-ls, nummult-le-01, mod-succ-01, mod-sub-02, mod-pred-02, mod-nls-04, mod-div-ls, is-div, diveq-pos, div2-nls-02, div2-nls, div-sum-ls, div-mult-three-nls, div-le-same-neg, div-eq-zero-01, div-eq-same-01, div-add-succ, div-add-nosucc,
int-abs/zero-ge-01 is used by modmod-add-if3, div2-add-neg, add-div-mult,
int-abs/zero-gels is used by mod-ls-same-02, mod-add1-posneg-pos, div-minus-onediff-01, div-eq-zero-01, div-eq-same-01,
int-abs/zero-gels-01 is used by zero-06, zero-05, zero-02, zero, square-nls-01, square-interval, one-neg, one, nummult-ls-03-01, nummult-ls-03, nummult-ls-01-01, nummult-ls-01, nummult-le-03-01, nummult-le-03, nummult-le-01-01, mult-ls-01, mult-ls, mult-01, modmod-mult-09, modmod-mult-07, modmod-mult-05, modmod-mult-03, modmod-mult-02, modmod-mult-01, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-law, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-01, modex-odd, modex, modeven-neg-01, modeven-neg, modeq-neg-02, modeq-neg, mod2-neg-odd, mod2-add-neg, mod-zero-one, mod-zero-06, mod-zero-05, mod-zero-01, mod-twoodd-03, mod-rec-01, mod-pred-neg-01, mod-pred-neg, mod-not-less, mod-nls-06, mod-nls-04, mod-nle-02, mod-neq, mod-mult-neg-02, mod-lsz, mod-ls-same-02, mod-ls-same-01, mod-lezero, mod-grz-02, mod-grz-01, mod-grz, mod-div-zero, mod-by6, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-01, lsfc-02, lsf-02, ls-even-01, ls-02, less-mult-div-01, le-abs-numerator, exeven, even-not-ex, even-not, diveq-neg, div2-zero, div2-notzero, div2-nls-02, div2-nls, div2-add-neg, div-zero-nls, div-zero-ngr-01, div-zero-ngr, div-zero-02, div-zero-01, div-twoodd-07, div-twoodd-04, div-twoodd-02, div-two-intro, div-same, div-rec-01, div-nls-01, div-ngr-zero, div-nearer-zero, div-mult-nls-zero, div-mult-01, div-minus255-256-01, div-minus255-256, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-lezero, div-le-same-neg, div-le-pos, div-est-num, div-eq-zero-01, div-eq-same-01, div-eq-same, div-elim3, div-elim2, div-elim1, div-elim-pospos, div-elim-posneg, div-elim-negpos, div-elim-negneg, div-div-pred-01, div-div-pred, div-div, div-addthree-rew, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ-neg, div-add-nosucc-neg, abs-shift, abs,
int-abs/zero-gels-02 is used by zero-01, ls-even-01, abs,
int-abs/zero-gels-03 is used by zero-05, nummult-ls-01, nummult-le-03, mult-ls, modmod-mult-07, modmod-mult-03, modmod-mult-02, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add-if, modmod-add-case, modmod-add-03, modeven-neg, mod-zero-06, mod-two-pred-01, mod-sub, mod-pred-neg, mod-not-less, mod-nls-03, mod-nle-02, mod-neq, mod-mult-neg, mod-lsz, mod-ls-same-02, mod-ls-same-01, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-01, lsf-02, ls-even-01, ls-02, ls, leone-two, le-abs-numerator, exeven, div2-odd-01, div2-notzero, div2-nls-02, div2-nls, div-zero-02, div-twoodd-03, div-twoodd-01, div-rec-01, div-nls-01, div-ngr-zero, div-nearer-zero, div-mult-neg, div-mult-01, div-minus255-256-01, div-minus-onediff-01, div-ls-zero, div-ls-same, div-ls-mone, div-le-same-neg, div-le-pos, div-est-num, div-eq-zero-01, div-eq-same-01, div-elim2, div-elim-negpos, div-div-pred-01, div-div-pred, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-01, div-add-nosucc-neg,
int-abs/zero-gels-04 is used by square-nls-02, square-nls, square-nle-02, square-nle, square-ls-01, square-inject, nummult-ls-04, nummult-ls-02-01, nummult-ls-02, nummult-ls, nummult-le-04, nummult-le-02-01, nummult-le, num-ls, mult-split-mod, mult-ls-01, mult-ls, mult-02, mult-01, modmod-pos, modmod-mult-07, modmod-mult-02, modmod-mult, modmod-ma-negpos-neg, modmod-ma-01, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-04, modmod-add-02, modmod-add-01, modmod-add, modex-odd-neg, modex-odd, modeq-pos, modeq-neg-02, mod2-add-neg, mod-zero-07, mod-zero-06, mod-zero-03, mod-zero-01, mod-twoodd-02, mod-twoodd-01, mod-succ-01, mod-sub-02, mod-sub-01, mod-shift, mod-rec, mod-pred-neg-01, mod-pred-neg, mod-pred-04, mod-pred-03, mod-pred-02, mod-nls-05, mod-nle, mod-mult-pos-01, mod-mult-pos, mod-mult-neg-01, mod-mult-neg, mod-ls-same-02, mod-ls-same-01, mod-div-zero, mod-div-ls, mod-by6, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-neg, mod-add-zero, mod-add, ls-same-pos-02, ls-same-pos-01, ls-same-pos, ls-even-01, ls-03, ls-02, ls-01, ls, leone-two, le-norest, le-abs-numerator, is-div, exodd, even-not-ex, diveq-pos, div2-nls-02, div2-nls, div2-add-neg, div-zero-nls, div-zero-ngr-01, div-zero-05, div-zero, div-twoodd-06, div-twoodd-02, div-two-zero-01, div-two-intro, div-shift-two, div-rec, div-nearer-zero, div-mult-two-nls-01, div-mult-shift-holds, div-mult-pos-01, div-mult-nls-est-01, div-mult-nls-est, div-mult-nle-est, div-mult-neg, div-mult-ls, div-mult-le-01, div-mult-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-pos-mon, div-ls-pos-better, div-ls-mone, div-ls-modnotzero, div-ls-01, div-ls, div-lezero, div-le-same-neg, div-le-same, div-le-pos, div-le-modzero-01, div-le-modnotzero-01, div-le-modnotzero, div-est-num, div-est-nls, div-est-nle-pos, div-est-denom-pos, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-elim2, div-elim1, div-elim-pospos, div-elim-posneg, div-elim-pos, div-elim-negneg, div-div-pred-01, div-div-pred, div-div-pos, div-am-rew, div-addthree-rew, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ, div-add-nosucc, add-div-mult,
int-abs/zero-gs is used by square-inject, modmod-add-if3, modmod-add-04, mod-mult-pos-01, div-mult-three-nls, div-addthree-rew, add-div-mult,

Used from specification int-basic2

int-basic2/add-a is used by add-div-mult,
int-basic2/add-c is used by mult-split-mod, modmod-add-law-pos, modmod-add-04, mod-shift, mod-mult-pos, div-sum-ls, div-shift-two, div-mult-three-nls,
int-basic2/add-zero is used by prod-div-less,
int-basic2/ex-ls-add is used by less-mult-div-01, div-ls-mone,
int-basic2/ls is used by modeq-neg-02,
int-basic2/nls is used by div-sum-ls,
int-basic2/pls is used by mod-zero-one,
int-basic2/pls-01 is used by mod-zero-one,
int-basic2/plst is used by div-mult-three-nls,
int-basic2/zero-03 is used by mod-add-zero,
int-basic2/zero-04 is used by div-eq-same-01,
int-basic2/zero-06 is used by less-mult-div-01,
int-basic2/add-a is used by zero-07, zero-06, zero-05, zero-04, zero-02, two-odd, two-mult-01, two-add-square, three, sub-ls-01, sub-ls, square-nls-02, square-nls-01, square-nls, square-nle-02, square-nle-01, square-nle, square-ls-02, square-ls-01, square-ls, square-interval, square-inject, square-even-02, square-even-01, square-even, prod-div-less, one-neg, one, nummult-modls, nummult-modle, nummult-ls-03, nummult-ls-02, nummult-ls-01, nummult-ls, nummult-le-03, nummult-le-02, nummult-le-01, nummult-le, num-ls, mult-split-mod-02, mult-split-mod, mult-ls-01, mult-ls, mult-03, mult-02, mult-01, mult, modmod-pos, modmod-mult-07, modmod-mult-04, modmod-mult-03, modmod-mult-02, modmod-mult, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-02, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-02, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-law-pos, modmod-add-law, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-04, modmod-add-02, modmod-add, modex-odd-neg-01, modex-odd-neg, modex-odd, modex, modeven-pos, modeven-neg-01, modeven-neg, modeq-pos-04, modeq-pos-03, modeq-pos-02, modeq-pos-01, modeq-pos, modeq-neg-02, modeq-neg, modby6-help, mod62, mod53, mod2-neg-odd, mod2-add-neg, mod-zero-one, mod-zero-07, mod-zero-06, mod-zero-05, mod-zero-03, mod-zero-01, mod-twoodd-03, mod-twoodd-02, mod-twoodd-01, mod-twoodd, mod-two-pred-02, mod-two-pred-01, mod-two-04, mod-two-03, mod-two-01, mod-three, mod-succ-02, mod-succ-01, mod-succ, mod-sub-02, mod-sub-01, mod-sub, mod-shift, mod-rew, mod-rec-01, mod-rec, mod-pred-neg-01, mod-pred-neg, mod-pred-04, mod-pred-03, mod-pred-02, mod-pred-01, mod-pred, mod-nls-06, mod-nls-05, mod-nls-04, mod-nls-02, mod-nls, mod-nle-02, mod-nle, mod-next-square, mod-neg-01, mod-neg, mod-mult-pos-02, mod-mult-pos-01, mod-mult-pos, mod-mult-neg-03, mod-mult-neg-02, mod-mult-neg-01, mod-mult-neg, mod-mult-02, mod-mult, mod-lsz, mod-ls-same-02, mod-ls-same-01, mod-ls-same, mod-lezero, mod-le, mod-four, mod-div-zero, mod-div-ls, mod-by6, mod-add1-pospos, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add1-negneg, mod-add-zero, mod-add-pos, mod-add-neg, mod-add-both-zero, mod-add-01, mod-add, minus-add, lsf-02, ls-succ, ls-even-01, ls-02, ls-01, ls, letwozero, less-mult-div-01, leone-two, le-norest, le-abs-numerator, is-div, exodd, exeven, even-or-succ-even, even-not-ex, even-not, even-mult, even-add, divmult, diveq-pos, div53, div2one-01, div2one, div2-zero, div2-odd-01, div2-odd, div2-notzero, div2-nls-02, div2-nls, div2-nle-02, div2-neg-odd, div2-neg-01, div2-neg, div2-add-neg, div-zero-02, div-zero-01, div-zero, div-twoodd-07, div-twoodd-06, div-twoodd-05, div-twoodd-03, div-twoodd-01, div-twoodd, div-two-zero-01, div-two-intro, div-two, div-sum-ls-01, div-sum-ls, div-sub-01, div-sub, div-shift-two, div-same, div-rec-01, div-rec, div-nls-01, div-ngr-zero, div-nearer-zero, div-mult-two-nls-01, div-mult-three-nls, div-mult-three, div-mult-shift-holds, div-mult-rew-01, div-mult-rew, div-mult-pos-rew, div-mult-pos-03, div-mult-pos-02, div-mult-pos-01, div-mult-pos, div-mult-nls-zero, div-mult-nls-est-01, div-mult-nls-est, div-mult-nle-est, div-mult-neg, div-mult-ls, div-mult-le-01, div-mult-02, div-mult-01, div-mone, div-minus255-256-01, div-minus255-256, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-ls, div-lezero, div-le-same-neg, div-le-same, div-le-pos, div-le-modnotzero, div-est-num, div-est-nls, div-est-nle-pos, div-est-denom-pos, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-eq-same, div-elim3, div-elim2, div-elim1, div-elim-pospos, div-elim-posneg, div-elim-pos, div-elim-negpos, div-elim-negneg, div-elim-divides, div-div-pred-01, div-div-pred, div-div-pos, div-div, div-am-rew, div-addthree-rew, div-add1-pospos, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-pos, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add1-negpos-neg, div-add1-negneg, div-add-succ-neg, div-add-succ, div-add-rew, div-add-pos, div-add-nosucc-neg, div-add-nosucc, div-add-neg, div-add-both, add-div-mult, abs-shift-01, abs-shift, abs,
int-basic2/add-c is used by zero-07, zero-06, zero-05, zero-04, zero-02, two-odd, two-mult-01, two-add-square, three, sub-ls-01, sub-ls, square-nls-02, square-nls-01, square-nls, square-nle-02, square-nle-01, square-nle, square-ls-02, square-ls-01, square-ls, square-interval, square-inject, square-even-02, square-even-01, square-even, prod-div-less, one-neg, one, nummult-modls, nummult-modle, nummult-ls-03, nummult-ls-02, nummult-ls-01, nummult-ls, nummult-le-03, nummult-le-02, nummult-le-01, nummult-le, num-ls, mult-split-mod-02, mult-split-mod, mult-ls-01, mult-ls, mult-03, mult-02, mult-01, mult, modmod-pos, modmod-mult-07, modmod-mult-04, modmod-mult-03, modmod-mult-02, modmod-mult, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-02, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-02, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-zero, modmod-add-law-pos, modmod-add-law, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-04, modmod-add-03, modmod-add-02, modmod-add, modex-odd-neg-01, modex-odd-neg, modex-odd, modex, modeven-pos, modeven-neg-01, modeven-neg, modeq-pos-04, modeq-pos-03, modeq-pos-02, modeq-pos-01, modeq-pos, modeq-neg-02, modeq-neg, modby6-help, mod62, mod53, mod2-neg-odd, mod2-add-neg, mod-zero-one, mod-zero-07, mod-zero-06, mod-zero-05, mod-zero-03, mod-zero-01, mod-twoodd-03, mod-twoodd-02, mod-twoodd-01, mod-twoodd, mod-two-pred-02, mod-two-pred-01, mod-two-04, mod-two-03, mod-two-01, mod-three, mod-succ-02, mod-succ-01, mod-succ, mod-sub-02, mod-sub-01, mod-sub, mod-shift, mod-rew, mod-rec-01, mod-rec, mod-pred-neg-01, mod-pred-neg, mod-pred-04, mod-pred-03, mod-pred-02, mod-pred-01, mod-pred, mod-nls-06, mod-nls-05, mod-nls-04, mod-nls-02, mod-nls, mod-nle-02, mod-nle, mod-next-square, mod-neg-01, mod-neg, mod-mult-pos-02, mod-mult-pos-01, mod-mult-pos, mod-mult-neg-03, mod-mult-neg-02, mod-mult-neg-01, mod-mult-neg, mod-mult-02, mod-mult, mod-lsz, mod-ls-same-02, mod-ls-same-01, mod-ls-same, mod-lezero, mod-le, mod-four, mod-div-zero, mod-div-ls, mod-by6, mod-add1-pospos, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add1-negneg, mod-add-zero, mod-add-pos, mod-add-neg, mod-add-both-zero, mod-add-01, mod-add, minus-add, lsf-02, ls-succ, ls-even-01, ls-02, ls-01, ls, letwozero, less-mult-div-01, leone-two, le-norest, le-abs-numerator, is-div, exodd, exeven, even-or-succ-even, even-not-ex, even-not, even-mult, even-add, divmult, diveq-pos, div53, div2one-01, div2one, div2-zero, div2-odd-01, div2-odd, div2-notzero, div2-nls-02, div2-nls, div2-nle-02, div2-neg-odd, div2-neg-01, div2-neg, div2-add-neg, div-zero-02, div-zero-01, div-zero, div-twoodd-07, div-twoodd-06, div-twoodd-05, div-twoodd-03, div-twoodd-01, div-twoodd, div-two-zero-01, div-two-intro, div-two, div-sum-ls-01, div-sum-ls, div-sub-01, div-sub, div-shift-two, div-same, div-rec-01, div-rec, div-nls-01, div-ngr-zero, div-nearer-zero, div-mult-two-nls-01, div-mult-three-nls, div-mult-three, div-mult-shift-holds, div-mult-rew-01, div-mult-rew, div-mult-pos-rew, div-mult-pos-03, div-mult-pos-02, div-mult-pos-01, div-mult-pos, div-mult-nls-zero, div-mult-nls-est-01, div-mult-nls-est, div-mult-nle-est, div-mult-neg, div-mult-ls, div-mult-le-01, div-mult-02, div-mult-01, div-mone, div-minus255-256-01, div-minus255-256, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-ls, div-lezero, div-le-same-neg, div-le-same, div-le-pos, div-le-modnotzero, div-est-num, div-est-nls, div-est-nle-pos, div-est-denom-pos, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-eq-same, div-elim3, div-elim2, div-elim1, div-elim-pospos, div-elim-posneg, div-elim-pos, div-elim-negpos, div-elim-negneg, div-elim-divides, div-div-pred-01, div-div-pred, div-div-pos, div-div, div-am-rew, div-addthree-rew, div-add1-pospos, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-pos, div-add1-posneg-neg, div-add1-negpos-pos, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add1-negpos-neg, div-add1-negneg, div-add-succ-neg, div-add-succ, div-add-rew, div-add-pos, div-add-nosucc-neg, div-add-nosucc, div-add-neg, div-add-both, add-div-mult, abs-shift-01, abs-shift, abs,
int-basic2/add-in is used by square-inject, nummult-ls-03, nummult-ls, nummult-le-02, nummult-le-01, mult-split-mod-02, mult-split-mod, modmod-pos, modmod-ma-negpos-neg, modmod-add-law-pos, modmod-add-if, modeq-pos, modeq-neg-02, mod-twoodd, mod-pred-neg, mod-mult-neg, mod-add1-posneg-pos, mod-add1-negpos-neg, even-not-ex, div2-add-neg, div-shift-two, div-mult-pos-rew, div-mult-pos-03, div-mult-pos-01, div-mult-neg, div-minus-onediff-01, div-minus-onediff, div-am-rew, div-addthree-rew, div-add1-pospos, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-pos, div-add1-negpos-pos, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add1-negpos-neg, div-add1-negneg, div-add-succ, div-add-both, add-div-mult,
int-basic2/add-less is used by mult-03, modmod-add2-posneg-neg, mod2-add-neg, mod-zero-05, mod-pred-neg-01, mod-pred-neg, mod-nls-04, mod-nle-02, mod-add1-posneg-pos, div-zero-01, div-minus-onediff, div-ls-zero, div-ls-mone, div-eq-zero-01, div-elim2, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-01,
int-basic2/add-zero is used by one-neg, nummult-ls-03, nummult-le-01, modmod-pos, modmod-add-04, modex-odd-neg, modeq-neg-02, mod2-add-neg, mod-pred-neg, mod-pred-02, mod-ls-same-02, mod-ls-same, mod-add1-posneg-pos, mod-add1-posneg-neg, mod-add1-negpos-pos, mod-add1-negpos-neg, mod-add-pos, mod-add-neg, mod-add-01, le-abs-numerator, even-not-ex, div2-add-neg, div-shift-two, div-mult-two-nls-01, div-add1-negpos-pos, div-add-pos, div-add-neg,
int-basic2/add-zero-rev is used by zero-07, zero-05, zero-02, square-nls-02, square-nls, square-nle, square-interval, square-inject, nummult-modls, nummult-modle, nummult-ls-02, nummult-ls, nummult-le-02, mult-split-mod, mult-03, mult-01, modmod-mult-07, modmod-mult-03, modmod-mult-02, modmod-mult, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-neg, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add-02, modex-odd, modex, modeven-pos, modeven-neg-01, modeven-neg, modeq-pos-04, modeq-pos, modby6-help, mod-zero-06, mod-zero-01, mod-twoodd-02, mod-sub, mod-shift, mod-rec-01, mod-pred-neg-01, mod-pred, mod-nls-06, mod-nls-04, mod-nls, mod-nle, mod-mult-pos, mod-mult-neg-01, mod-mult-neg, mod-div-zero, mod-div-ls, mod-add-zero, lsf-02, ls-even-01, ls-02, less-mult-div-01, le-norest, exodd, exeven, even-mult, divmult, div2-zero, div2-odd-01, div2-odd, div2-notzero, div2-nls-02, div2-nls, div2-nle-02, div-twoodd-03, div-twoodd-01, div-rec-01, div-nls-01, div-ngr-zero, div-nearer-zero, div-mult-shift-holds, div-mult-pos-02, div-mult-pos-01, div-mult-neg, div-mult-01, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-le-same-neg, div-eq-zero-01, div-eq-zero, div-eq-same-01, div-elim3, div-elim2, div-elim1, div-elim-divides, div-div-pred-01, div-div-pred, div-div, div-am-rew, div-addthree-rew, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ-neg, div-add-succ, div-add-nosucc-neg, div-add-nosucc, add-div-mult, abs,
int-basic2/eq is used by one, mult-split-mod, modmod-add2-negpos-pos-01, modmod-add-law-pos, modmod-add-if3, modmod-add-case, modeq-neg-02, mod-zero-07, mod-zero-05, mod-zero-03, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-01, less-mult-div-01, div-two-intro, div-rec-01, div-mult-pos-01, div-minus-onediff-01, div-minus-onediff, div-eq-same, div-elim-divides, div-div-pred-01, div-am-rew, div-addthree-rew, div-add1-posneg-pos-01, div-add1-negpos-neg-01, div-add-succ, div-add-nosucc,
int-basic2/ls is used by zero-04, sub-ls, square-nls-01, one-neg, nummult-ls, nummult-le-02, modmod-mult-04, modmod-ma-negpos-neg, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-neg, modmod-add-if3, modmod-add-if, modmod-add-case, modmod-add, modeq-pos-01, modeq-neg-02, mod-zero-06, mod-succ-01, mod-pred-neg-01, mod-pred-neg, mod-pred-02, mod-nls-04, mod-nle-02, mod-mult-neg-02, mod-mult-neg, mod-lsz, mod-ls-same-02, mod-ls-same-01, mod-lezero, mod-add1-posneg-neg, mod-add1-negpos-neg, mod-add-pos, mod-add-01, ls-succ, ls-even-01, less-mult-div-01, le-abs-numerator, div2-nls-02, div2-nle-02, div-zero-02, div-shift-two, div-mult-nls-zero, div-mult-neg, div-mult-ls, div-minus-onediff-01, div-ls-zero, div-ls-same, div-ls-mone, div-le-same-neg, div-le-pos, div-eq-zero-01, div-elim2, div-elim-posneg, div-elim-negpos, div-div-pred-01, div-addthree-rew, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-pos, div-add-nosucc-neg,
int-basic2/ls-01 is used by zero-04, modmod-ma-negpos-neg, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add-if, modmod-add-case, modmod-add, modeq-pos-03, modeq-neg-02, mod2-add-neg, mod-zero-06, mod-zero-05, mod-rec-01, mod-pred-neg-01, mod-nls-04, mod-nle-02, mod-ls-same-02, mod-ls-same-01, mod-add1-posneg-pos, mod-add1-negpos-neg, mod-add-neg, mod-add-01, ls-01, less-mult-div-01, le-abs-numerator, div-zero-02, div-zero-01, div-shift-two, div-mult-two-nls-01, div-mult-three-nls, div-minus-onediff, div-ls-zero, div-ls-mone, div-le-same-neg, div-eq-zero-01, div-elim-posneg, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-01, div-add-neg,
int-basic2/ls-02 is used by zero-04, nummult-ls-03, nummult-ls-01, nummult-le-03, nummult-le-01, modmod-add2-posneg-pos, modmod-add2-negpos-pos-01, modeq-pos-03, mod-zero-05, mod-rec, mod-mult-neg-02, mod-ls-same-01, mod-add1-posneg-pos, mod-add-neg, mod-add-01, less-mult-div-01, le-abs-numerator, div2-neg-01, div-zero-02, div-zero-01, div-ngr-zero, div-ls-zero, div-ls-mone, div-lezero, div-eq-zero-01, div-eq-same-01, div-div-pred, div-add1-posneg-pos-01, div-add-neg,
int-basic2/ls-add-both is used by square-ls-02, modmod-add2-negpos-pos-01, mod-zero-05, div-zero-01, div-eq-zero-01, div-add1-negpos-neg-01,
int-basic2/lst-03 is used by zero-04, nummult-ls-01, nummult-le-03, nummult-le-01, mult-ls-01, mult-ls, modmod-ma-negpos-neg, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-negpos-pos-01, modmod-add2-negpos-neg, modmod-add-if, mod-zero-05, mod-pred-neg-01, mod-nle-02, mod-ls-same-01, div-zero-01, div-ngr-zero, div-minus-onediff, div-ls-same, div-le-same-neg, div-le-pos, div-est-num, div-eq-same-01, div-elim2, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-01,
int-basic2/lst-04 is used by zero-05, nummult-ls-01, nummult-le-03, nummult-le-01, mult-ls, modmod-add2-posneg-neg, mod-zero-06, mod-pred-neg-01, mod-nls-04, mod-nls-02, div-nearer-zero, div-ls-mone, div-eq-zero-01, div-add1-posneg-pos-01, div-add1-negpos-neg-01,
int-basic2/nls is used by square-ls-02,
int-basic2/num-between is used by one, leone-two, div2-nle-01, div-mult-three-nls,
int-basic2/succ-01 is used by zero-05, zero-04, zero-03, zero-02, sub-ls-01, square-interval, one-neg, nummult-ls-01, nummult-le-03, nummult-le-01, mult-ls-01, mult-ls, modmod-mult-07, modmod-mult-03, modmod-mult-02, modmod-ma-negpos-neg, modmod-ma, modmod-add2-posneg-pos, modmod-add2-posneg-neg-01, modmod-add2-posneg-neg, modmod-add2-negpos-pos-01, modmod-add2-negpos-pos, modmod-add2-negpos-neg, modmod-add-if3, modmod-add-if, modmod-add-case, modeq-pos-03, mod-zero-one, mod-zero-ls, mod-zero-06, mod-zero-05, mod-zero-01, mod-twoodd-03, mod-succ-01, mod-sub-02, mod-pred-neg-01, mod-nls-05, mod-nls-04, mod-nls-02, mod-nle-02, mod-lsz, mod-ls-zero, mod-ls-same-01, mod-lezero, mod-le-num, mod-grz-02, mod-grz-01, mod-grz, mod-by6, mod-add-neg, lsfc-02, lsf-02, ls-same-pos-01, ls-even-01, ls-02, less-mult-div-01, is-div, estimate-01, diveq-pos, diveq-neg, div2-nls-03, div2-nls-02, div2-nls-01, div-zero-nls, div-zero-ngr-01, div-zero-ngr, div-zero-02, div-zero-01, div-ngr-zero, div-nearer-zero, div-mult-nls-zero, div-mult-01, div-minus-onediff-01, div-minus-onediff, div-ls-zero, div-ls-same, div-ls-mone, div-lezero, div-le-same-neg, div-le-pos, div-est-num, div-eq-zero-01, div-eq-same-01, div-elim2, div-elim-pospos, div-elim-negpos, div-div-pred, div-div, div-addthree-rew, div-add1-posneg-pos-02, div-add1-posneg-pos-01, div-add1-posneg-neg, div-add1-negpos-neg-02, div-add1-negpos-neg-01, div-add-succ-neg, div-add-nosucc-neg, div-add-neg, abs-shift,
int-basic2/zero-01 is used by one-neg, div2-nls, div-elim2, div-elim-negpos,
int-basic2/zero-02 is used by square-interval, mod-sub-02, mod-pred-neg-01, mod-by6, ls-succ, less-mult-div-01, div-sum-ls-01, div-mult-three-nls, div-minus-onediff, div-ls-mone, div-add-nosucc,