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

Used from specification int-abs

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

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