[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 real-abs

real-abs/antr is used by zero-neq-01, square-le, zero-gr-01, zero-ge-add-02,
real-abs/forward-lele is used by pnls-negpos, pnls-posneg, ple-pos-better, ple-pos, pnls-pos, square-le,
real-abs/forward-lels is used by mult-gt-both,
real-abs/forward-lsle is used by pls-neg, pls-pos,
real-abs/gr-def is used by le-pos, le-neg,
real-abs/le-def is used by inv-ge-pos, square-le-04, invmult-ge-neg, inv-ge-neg, invmult-ge-pos,
real-abs/lele-add-notgr is used by square-ls-02, square-ls-04,
real-abs/lels is used by invmult-gr-pos, square-le-04, pnls-negpos, pnls-posneg, inv-gr-neg, zero-neq-01, ple-pos, invmult-gr-neg, pnls-pos, square-le, inv-gr-pos, zero-ge-add-02,
real-abs/lsls-add-notge is used by square-ls-02,
real-abs/sub-le-01 is used by invmult-le-pos-add, invmult-le-neg-add,
real-abs/transrew is used by pnle-neg, square-le,
real-abs/transrew-01 is used by pnle-pos,
real-abs/zero-gs is used by square-gez-01,
real-abs/Abs-pos is used by abs-ite,
real-abs/abs-02 is used by le-same-05,
real-abs/abs-16 is used by le-same-06, square-le-04,
real-abs/abs-add is used by abs-ite,
real-abs/abs-one is used by square-ls-one, square-le-one, square-ge-one, square-gr-one, square-eq-one,
real-abs/absle is used by square-le-04, square-ls-02,
real-abs/antr is used by pls-neg, le-same-02, ls-pos, zero-ls-03, square-le-04, ls-neg, abs-ls-same, invmult-ls-pos, square-le, zero-gr-01, pnle-pos,
real-abs/forward-le is used by ls-two-02,
real-abs/forward-le-01 is used by ls-two, square-le-04, square-gr-one, square-ls-02,
real-abs/forward-le-05 is used by square-ls-one, square-le-04, square-eq-01, square-le, mult-gt-both, pnle-pos, ls-two-01, square-ls-02, zero-ge-add-02, mods-ls,
real-abs/forward-lele is used by square-interval-01, pls-neg, square-ls-one, square-le-one, square-ge-one, pnls-negpos, pnls-posneg, square-interval, ple-pos-better, zero-gr-add-01, square-zero-01a, abs-ls-same, square-zero-01, pnls-pos, square-le, pnle-pos,
real-abs/forward-lels is used by square-interval-01, pnls-neg, pnle-neg, pls-neg, ls-pos-02, square-ls-one, pls-pos-02, square-le-one, square-ge-one, ple-neg, square-interval, zero-gr-add-01, square-zero-01a, abs-ls-same, square-gr-one, square-zero-01, square-le, est-nle, square-ls-01, zero-gr-03,
real-abs/forward-lsle is used by ls-same-05, square-ls-one, le-same-01, pls-pos-01, ls-two, zero-ls-02, square-le-one, square-ge-one, square-le-03, square-interval, square-eq-02, mult-pos, zero-gr-add-01, ple-pos, square-zero-01a, abs-ls-same, square-gr-one, square-zero-02, square-zero-01, square-le, zero-gr-01, square-ls-03a, ls-two-01, square-le-05a, pls-pos, zero-ge-add-01, zero-ge-add-02,
real-abs/gr-def is used by square-lez, le-pos, ls-pos, ls-neg, zero-neq-01, le-neg, zero-gr-01,
real-abs/le-def is used by square-interval-01, invmult-le-pos-add, le-pos, le-abs, zero-ge-case, pls-neg, le-same-04, le-same-01, le-same-02, square-le-one, invmult-le-neg, square-ge-one, inv-ge-pos, square-le-04, square-le-03, zero-ge-01, invmult-le-neg-add, pzero-ls, zero-ge-02, zero-ge-03, zero-le-case, inv-le-neg, pnls-negpos, invmult-ge-neg, pnls-posneg, ple-neg, square-interval, square-eq-02, ple-pos-better, inv-le-pos, ple-pos, square-zero-01a, le-neg, invmult-le-pos, square-zero-02, square-zero-01, pnls-pos, abs-le-one-multiple, square-le, zero-le-01, zero-le-02, zero-le-03, inv-ge-neg, invmult-ge-pos, twice-le-zero, mult-gt-both, square-ls-03a, square-gez-01, est-nle, square-gez, pnle-pos, ls-two-03, ls-two-01, le-same, square-le-05a, pls-pos, zero-ge-add-01, zero-ge-add-02,
real-abs/le-num is used by ls-two, square-interval, twice-le-zero,
real-abs/lels is used by square-interval-01, square-lez, invmult-le-pos-add, ls-same-05, abs-not-neg, invmult-ls-neg, pls-neg, ls-pos-02, square-ls-one, le-same-02, pls-pos-01, pls-pos-02, ls-pos, ls-two, zero-ls-03, zero-ls-02, zero-ls-01, invmult-ls-pos-add, square-le-one, abs-ls-multiple-one, invmult-gr-pos, square-ge-one, inv-ge-pos, square-le-04, invmult-ls-neg-add, invmult-le-neg-add, pzero-ls, twice-ls-zero, square-abs, inv-ls-neg, invmult-ge-neg, square-eq, zero-gr-case, ls-neg, square-interval, noeth-zero-ls, mult-pos, inv-ls-pos, inv-gr-neg, pzero-gr, invmult-gr-neg, le-neg, abs-ls-same, square-gr-one, invmult-ls-pos, square-minus, square-le, zero-gr-01, zero-gr-02, square-ls, inv-ge-neg, mult-gt-one, invmult-ge-pos, zero-ls-case, abs-eqall, mult-gt-both, inv-gr-pos, square-ls-01, ls-two-02, abs-ls-one-multiple, square-ls-02, pls-pos, zero-ge-add-02, mods-ls, zero-gr-03,
real-abs/lels-02 is used by zero-ge-case, abs-not-neg, le-same-02, pls-pos-01, pls-pos-02, zero-ls-02, zero-ge-02, zero-ge-03, zero-le-case, pnls-negpos, square-eq, pnls-posneg, zero-gr-case, ple-pos-better, zero-neq-01, square-zero-02, square-zero-01, pnls-pos, square-le, zero-gr-01, zero-gr-02, zero-le-02, zero-le-03, zero-ls-case, abs-eqall, mult-gt-both, est-nle, pnle-pos, zero-gr-03,
real-abs/lels-03 is used by square-interval-01, invmult-le-pos-add, le-pos, le-abs, ls-same-05, abs-not-neg, invmult-ls-neg, pnle-neg, square-ls-one, le-same-05, le-same-04, le-same-01, zero-ls-02, invmult-ls-pos-add, abs-ls-multiple-one, invmult-gr-pos, square-ge-one, inv-ge-pos, invmult-ls-neg-add, zero-ge-01, invmult-le-neg-add, pzero-ls, zero-ge-02, zero-ge-03, inv-ls-neg, invmult-ge-neg, square-eq, zero-gr-case, noeth-zero-ls, inv-ls-pos, inv-gr-neg, invmult-gr-neg, le-neg, abs-ls-same, square-gr-one, abs-le-one-multiple, square-lez-01, square-le, zero-gr-02, zero-le-01, zero-le-02, zero-le-03, square-ls, inv-ge-neg, mult-gt-one, invmult-ge-pos, zero-ls-case, inv-gr-pos, pnle-pos, abs-ls-one-multiple, square-le-05a, zero-ge-add-02, mods-ls, zero-gr-03,
real-abs/lenls is used by square-interval-01, square-lez, invmult-le-pos-add, le-pos, pnls-neg, le-abs, le-same-04, le-same-01, pls-pos-01, pls-pos-02, ls-pos, square-le-one, abs-ls-multiple-one, invmult-le-neg, inv-ge-pos, square-le-04, zero-ge-01, invmult-le-neg-add, pzero-ls, square-abs, inv-ls-neg, inv-le-neg, pnls-negpos, invmult-ge-neg, pnls-posneg, ple-neg, ls-neg, square-interval, ple-pos-better, mult-pos, inv-le-pos, zero-gr-add-01, ple-pos, square-zero-01a, pzero-gr, le-neg, invmult-le-pos, square-gr-one, square-zero-01, pnls-pos, abs-le-one-multiple, square-le, zero-gr-01, zero-le-01, inv-ge-neg, invmult-ge-pos, abs-eqall, est-nle, abs-ls-one-multiple, le-same, pls-pos, zero-ge-add-01, zero-gr-03,
real-abs/lep is used by ls-dist-06, num-distr-le1,
real-abs/lep-01 is used by square-ls-one, num-distr-add-le2, square-ge-one, square-interval, square-zero-01a, abs-ls-same, ls-dist-05, square-le, num-distr-le2,
real-abs/lep-02 is used by num-distr-add-le1, le-dist, le-dist-02, le-dist-01, square-interval, num-distr-addboth-le1, num-distr-addboth-le2,
real-abs/ler is used by pls-neg, le-same-05, le-same-02, ls-pos, square-lez-01, invmult-ls-pos, square-le, zero-gr-01, zero-gr-03,
real-abs/lsle-add-notge is used by square-le-04,
real-abs/negle-07 is used by square-ge-one, abs-ls-same, square-le,
real-abs/negle-13 is used by le-abs, le-same-05, le-same-04, square-le-one, abs-ls-multiple-one, square-gr-one, abs-le-one-multiple, square-le, zero-le-01, abs-ls-one-multiple,
real-abs/notle-pos is used by mods-ls,
real-abs/sub-le is used by invmult-ge-neg-add, invmult-le-neg-add, invmult-ge-pos-add,
real-abs/sub-le-01 is used by invmult-le-pos-add, le-abs, le-same-05, le-same-04, abs-ls-multiple-one, invmult-ge-neg-add, abs-le-one-multiple, square-le, abs-ls-one-multiple,
real-abs/zero-gels is used by square-ls-03a,
real-abs/zero-gels-01 is used by zero-ls-02, pzero-ls, square-eq-02, zero-gr-add-01, pzero-gr, square-le, zero-gr-01, zero-ge-add-01, zero-ge-add-02,
real-abs/zero-gels-03 is used by square-interval, square-le,
real-abs/zero-gels-04 is used by pnls-negpos, pnls-posneg, square-le,
real-abs/zero-gs is used by square-zero-02,

Used from specification real-basic

real-basic/add-assoc is used by square-le-05,
real-basic/add-zero is used by mult-zero,
real-basic/blst-01 is used by square-zero, square-eq-01, mult-pos, square-lez-01,
real-basic/eqint-add is used by num-distr-add-le2, num-distr-add-le1, num-distr-add-ls2, num-distr-add-ls1, num-distr, num-distr-eq2, num-distr-eq1, num-distr-ls2, num-distr-ls1, num-distr-addboth-eq2, num-distr-addboth-eq1, num-distr-addboth-le1, num-distr-addboth-le2, num-distr-add-eq2, num-distr-add-eq1, num-distr-addboth-ls1, num-distr-addboth-ls2, num-distr-le2, num-distr-le1,
real-basic/eqint-neg is used by two-sub,
real-basic/neg-09 is used by le-pos, le-neg,
real-basic/negeq is used by square-le,
real-basic/negradd-ls is used by invmult-ls-pos-add, invmult-ls-neg-add,
real-basic/trans-lem is used by mods-zero-07, ple-neg, square-le,
real-basic/trans-lem3 is used by pnls-neg,
real-basic/add-assoc is used by square-interval-01, mult-zero, invmult-le-pos-add, le-pos, le-abs, ls-pos-02, square-ls-one, le-same-05, le-same-04, num-distr-add-le2, num-distr-add-le1, ls-pos, succ-rsplit, num-distr-add-ls2, num-distr-add-ls1, invmult-ls-pos-add, square-le-one, abs-ls-multiple-one, minus-left, two-le-04, two-le-03, two-le-02, two-le-01, square-ge-one, square-le-05, square-le-04, mods-zero-07, square-le-03, invmult-ls-neg-add, invmult-ge-neg-add, le-dist, invmult-le-neg-add, num-distr, eq-succ-01, num-distr-eq2, num-distr-eq1, ls-add-02, ls-add-03, le-dist-02, le-dist-01, ls-neg, succ-rmerge, square-eq-01, square-interval, square-eq-02, minus-one, square-eq-03, invmult-ge-pos-add, zero-gr-add-01, add-mult-two, num-distr-ls2, invmult-gr-neg-add, num-distr-ls1, square-zero-01a, le-neg, inv-mult-add-eq, ls-dist-02, ls-dist-01, eq-nonzero, abs-ls-same, ls-dist-06, square-gr-one, square-zero-02, ls-dist-05, square-zero-01, ls-dist-04, ls-dist-03, mult-add-greater, two-sub, abs-le-one-multiple, num-distr-addboth-eq2, num-distr-addboth-eq1, eq-succ, invmult-gr-pos-add, square-le, eq-dist, zero-le-01, num-distr-addboth-le1, num-distr-addboth-le2, square-eq-one, two-sub-04, two-sub-05, abs-ite, two-sub-02, two-sub-03, square-ls-04a, abs-eqall, two-sub-01, twice-le-zero, succ-lsplit, two-ls-04, two-ls-03, num-distr-add-eq2, square-ls-03a, two-ls-02, two-ls-01, num-distr-add-eq1, ls-dist, two-le, square-ls-01, two-ls, num-distr-addboth-ls1, abs-ls-one-multiple, num-distr-addboth-ls2, square-ls-02, square-ls-03, square-ls-04, square-le-05a, num-distr-le2, zero-ge-add-01, num-distr-le1, zero-ge-add-02, mods-ls,
real-basic/add-comm is used by square-interval-01, mult-zero, invmult-le-pos-add, le-pos, le-abs, ls-pos-02, square-ls-one, le-same-05, le-same-04, num-distr-add-le2, num-distr-add-le1, ls-pos, succ-rsplit, num-distr-add-ls2, num-distr-add-ls1, invmult-ls-pos-add, square-le-one, abs-ls-multiple-one, minus-left, two-le-04, two-le-03, two-le-02, two-le-01, square-ge-one, square-le-05, square-le-04, mods-zero-07, square-le-03, invmult-ls-neg-add, invmult-ge-neg-add, le-dist, invmult-le-neg-add, num-distr, eq-succ-01, num-distr-eq2, num-distr-eq1, ls-add-02, ls-add-03, le-dist-02, le-dist-01, ls-neg, succ-rmerge, square-eq-01, square-interval, square-eq-02, minus-one, square-eq-03, invmult-ge-pos-add, zero-gr-add-01, add-mult-two, num-distr-ls2, invmult-gr-neg-add, num-distr-ls1, square-zero-01a, le-neg, inv-mult-add-eq, ls-dist-02, ls-dist-01, eq-nonzero, abs-ls-same, ls-dist-06, square-gr-one, square-zero-02, ls-dist-05, square-zero-01, ls-dist-04, ls-dist-03, mult-add-greater, two-sub, abs-le-one-multiple, num-distr-addboth-eq2, num-distr-addboth-eq1, eq-succ, invmult-gr-pos-add, square-le, eq-dist, zero-le-01, num-distr-addboth-le1, num-distr-addboth-le2, square-eq-one, two-sub-04, two-sub-05, abs-ite, two-sub-02, two-sub-03, square-ls-04a, abs-eqall, two-sub-01, twice-le-zero, succ-lsplit, two-ls-04, two-ls-03, num-distr-add-eq2, square-ls-03a, two-ls-02, two-ls-01, num-distr-add-eq1, ls-dist, two-le, square-ls-01, two-ls, num-distr-addboth-ls1, abs-ls-one-multiple, num-distr-addboth-ls2, square-ls-02, square-ls-03, square-ls-04, square-le-05a, num-distr-le2, zero-ge-add-01, num-distr-le1, zero-ge-add-02, mods-ls,
real-basic/add-in is used by succ-rsplit, num-distr, eq-succ-01, succ-rmerge, square-eq-02, add-mult-two, num-distr-addboth-eq2, num-distr-addboth-eq1, eq-succ, eq-dist, two-sub-05, succ-lsplit, num-distr-add-eq1,
real-basic/add-less is used by ls-dist-04, square-le,
real-basic/add-zero is used by le-abs, le-same-05, le-same-04, abs-ls-multiple-one, two-le-04, two-le-03, two-le-02, two-le-01, inv-mult-add-eq, abs-le-one-multiple, square-le, zero-le-01, two-sub-04, two-sub-03, abs-eqall, two-ls-04, two-ls-03, two-ls-02, two-ls-01, two-le, two-ls, abs-ls-one-multiple,
real-basic/bls-01 is used by square-lez, pnls-neg, le-abs, zero-ge-case, abs-not-neg, pls-neg, le-same-05, le-same-04, le-same-02, ls-pos, zero-ls-01, square-le-one, abs-ls-multiple-one, zero-eq, square-le-04, pzero-ls, square-abs, zero-le-case, square-eq, ls-neg, square-eq-01, zero-neq-01, pzero-gr, abs-ls-same, square-gr-one, mult-add-greater, abs-le-one-multiple, invmult-ls-pos, square-le, zero-gr-01, abs-eqall, mult-gt-both, pnle-pos, abs-ls-one-multiple, zero-ge-add-02,
real-basic/blst is used by square-le-04,
real-basic/blst-01 is used by le-abs, zero-ge-case, le-same-05, le-same-04, abs-ls-multiple-one, zero-eq, inv-eq, zero-le-case, abs-le-one-multiple, abs-eqall, abs-ls-one-multiple,
real-basic/blst-02 is used by square-eq, square-zero, mult-pos, invmult-ls-pos,
real-basic/double-neg is used by square-lez, ls-neg, le-neg, square-le, zero-gr-01, zero-le-01, abs-eqneg,
real-basic/eq is used by num-distr-eq2, num-distr-eq1, num-distr-add-eq2,
real-basic/eqint-add is used by square-interval-01, mult-zero, square-le-05, mods-zero-07, square-interval, square-eq-02, square-eq-03, square-zero-01a, square-zero-01, two-sub-04, two-sub-05, two-sub-02, two-sub-03, square-ls-04a, twice-le-zero, square-ls-03a, two-ls-02, square-ls-03, square-ls-04, square-le-05a,
real-basic/eqint-num is used by posint-factor, le-abs, inv-mult, neq-not-zero-01, eq-nonzero-int, minus-left, zero-eq, inv-eq, square-zero, minus-one, zero-neq-01, eq-same, eq-nonzero, square-eq-one, abs-ite, abs-eqall, zero-neq, inv-twice, neq-not-zero,
real-basic/irref is used by ls-pos, square-ge-one, square-eq, ls-neg, abs-ls-same, square-gr-one, invmult-ls-pos, square-le,
real-basic/less-add-cancel-l is used by square-interval-01, num-distr-add-ls1, square-le-04, ls-add-02, ls-add-03, square-interval, square-zero-01a, ls-dist-02, ls-dist-01, square-zero-02, ls-dist, num-distr-addboth-ls1, num-distr-addboth-ls2,
real-basic/lf-02 is used by pls-neg, zero-ls-03, mods-zero-07, pzero-ls, square-eq, minus-one, mult-pos, zero-neq-01, pzero-gr, abs-ls-same, invmult-ls-pos, square-le, eq-same-03, eq-same-02, zero-neq,
real-basic/lf-03 is used by pls-neg, zero-ls-03, zero-eq, pzero-ls, square-eq, zero-neq-01, pzero-gr, invmult-ls-pos, square-le, eq-same-03, eq-same-02,
real-basic/ls is used by num-distr-add-ls2, square-le-one, square-le-03, square-interval, square-eq-02, num-distr-ls2, square-zero-01a, square-gr-one, square-zero-02, square-zero-01, ls-dist-03, mult-add-greater, square-le, square-ls-03a, square-ls-01, square-le-05a, zero-ge-add-01,
real-basic/ls-02 is used by square-interval-01, ls-pos-02, mods-zero-07, square-interval, minus-one, zero-gr-add-01, num-distr-ls1, square-zero-01a, abs-ls-same, ls-dist-04, square-le,
real-basic/ls-num is used by le-abs, ls-same-05, zero-ge-case, square-ls-one, le-same-04, le-same-01, zero-ls-03, zero-ls-02, square-le-one, abs-ls-multiple-one, ls-negint, le-negint, ls-forward, square-ge-one, le-posint, mods-zero-07, pzero-ls, twice-ls-zero, zero-le-case, eq-pos, square-zero, square-interval, square-eq-02, minus-one, square-zero-01a, pzero-gr, ls-posint, abs-ls-same, square-gr-one, square-zero-02, square-zero-01, abs-le-one-multiple, invmult-ls-pos, square-minus, zero-gr-01, zero-gr-02, eq-same-03, eq-same-02, eq-neg, square-ls-03a, ls-two-03, ls-two-02, ls-two-01, abs-ls-one-multiple, square-le-05a, zero-ge-add-02, zero-gr-03,
real-basic/lsls-add-noteq is used by square-eq-01,
real-basic/lsnum-addboth1 is used by square-interval,
real-basic/lsnum-addboth2 is used by square-zero-01,
real-basic/mone-03 is used by minus-one, square-zero-01, square-eq-one,
real-basic/neg is used by abs-eqall,
real-basic/neg-01 is used by le-abs, le-same-04, abs-ls-multiple-one, abs-le-one-multiple, abs-ls-one-multiple,
real-basic/neg-02 is used by square-lez, ls-neg, zero-neq-01, le-neg, square-le, zero-gr-01, zero-le-01, zero-neq,
real-basic/neg-05 is used by abs-not-neg, square-minus,
real-basic/neg-09 is used by le-pos, ls-pos, ls-neg, le-neg, abs-ls-same, square-le,
real-basic/neg-10 is used by le-abs, square-le, zero-neq,
real-basic/neg-12 is used by minus-one-01,
real-basic/neg-add is used by ls-neg, le-neg, two-sub-05,
real-basic/neg-zero is used by square-minus,
real-basic/negadd-eq is used by two-sub,
real-basic/negeq is used by posint-factor, minus-left, minus-one, square-eq-one, abs-ite, abs-eqall,
real-basic/negl-ls is used by ls-pos-02, square-ls-one, square-ge-one, abs-ls-same, square-le,
real-basic/negladd-ls is used by invmult-ls-neg-add, invmult-gr-neg-add, invmult-gr-pos-add,
real-basic/negr-ls is used by square-gr-one, square-le,
real-basic/negradd-ls is used by invmult-ls-pos-add, invmult-gr-neg-add,
real-basic/sub-eq is used by inv-mult-add-eq, two-sub, two-sub-04, two-sub-05, two-sub-02, abs-eqall, two-sub-01,
real-basic/sub-eq-01 is used by minus-left, inv-mult-add-eq, eq-nonzero,
real-basic/trans is used by pnls-neg, ls-same-05, abs-not-neg, pnle-neg, pls-neg, ls-pos-02, square-ls-one, le-same-01, le-same-02, zero-ls-03, square-ge-one, pzero-ls, ple-neg, square-interval, mult-pos, zero-gr-add-01, zero-neq-01, abs-ls-same, square-zero-02, square-le, zero-gr-01, ls-two-03, ls-two-02, pls-pos, zero-ge-add-02,
real-basic/zero-01 is used by square-le,
real-basic/zero-07 is used by abs-eqall,

Used from specification int-basic2

Used from specification int-abs

int-abs/elim-sub is used by num-distr-add-le2, num-distr-add-le1, num-distr-add-ls2, num-distr-add-ls1, num-distr-eq2, num-distr-eq1, num-distr-ls2, num-distr-ls1, num-distr-addboth-eq2, num-distr-addboth-eq1, num-distr-addboth-le1, num-distr-addboth-le2, num-distr-add-eq2, num-distr-add-eq1, num-distr-addboth-ls1, num-distr-addboth-ls2, num-distr-le2, num-distr-le1,
int-abs/forward-le-01 is used by num-distr-add-le1, num-distr-add-ls1, num-distr-eq1, num-distr-ls1, num-distr-addboth-eq1, num-distr-addboth-le1, num-distr-add-eq1, num-distr-addboth-ls1, num-distr-le1,
int-abs/forward-le-02 is used by posint-factor,
int-abs/forward-le-05 is used by num-distr-add-le2, num-distr-add-ls2, le-posint, num-distr-eq2, num-distr-ls2, ls-posint, num-distr-addboth-eq2, num-distr-addboth-le2, num-distr-add-eq2, num-distr-addboth-ls2, num-distr-le2,
int-abs/gr-def is used by le-posint, ls-posint,
int-abs/lels is used by le-posint, ls-posint,
int-abs/lels-03 is used by le-posint, ls-posint,
int-abs/lep is used by num-distr-add-le1, num-distr-add-ls1, num-distr-eq1, num-distr-ls1, num-distr-addboth-eq1, num-distr-addboth-le1, num-distr-add-eq1, num-distr-addboth-ls1, num-distr-le1,
int-abs/neg-03 is used by posint-factor,
int-abs/zero-gels-01 is used by posint-factor, ls-negint, le-negint,
int-abs/zero-gels-04 is used by num-distr-add-le1, num-distr-add-ls1, num-distr-eq1, num-distr-ls1, num-distr-addboth-eq1, num-distr-addboth-le1, num-distr-add-eq1, num-distr-addboth-ls1, num-distr-le1,