Used simplifier rules/spec theorems by specification

Used from specification int-basic1

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

Used from specification int-abs

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

Used from specification int-basic2

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