[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, zero-gr-01, zero-ge-add-02, square-le,
real-abs/forward-lele is used by square-le, pnls-posneg, pnls-pos, pnls-negpos, ple-pos-better, ple-pos,
real-abs/forward-lels is used by mult-gt-both,
real-abs/forward-lsle is used by pls-pos, pls-neg,
real-abs/gr-def is used by le-pos, le-neg,
real-abs/le-def is used by square-le-04, invmult-ge-pos, invmult-ge-neg, inv-ge-pos, inv-ge-neg,
real-abs/lele-add-notgr is used by square-ls-04, square-ls-02,
real-abs/lels is used by zero-neq-01, zero-ge-add-02, square-le-04, square-le, pnls-posneg, pnls-pos, pnls-negpos, ple-pos, invmult-gr-pos, invmult-gr-neg, inv-gr-pos, inv-gr-neg,
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 square-le, pnle-neg,
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 square-le-04, le-same-06,
real-abs/abs-add is used by abs-ite,
real-abs/abs-one is used by square-ls-one, square-le-one, square-gr-one, square-ge-one, square-eq-one,
real-abs/absle is used by square-ls-02, square-le-04,
real-abs/antr is used by zero-ls-03, zero-gr-01, square-le-04, square-le, pnle-pos, pls-neg, ls-pos, ls-neg, le-same-02, invmult-ls-pos, abs-ls-same,
real-abs/forward-le is used by ls-two-02,
real-abs/forward-le-01 is used by square-ls-02, square-le-04, square-interval, square-gr-one, ls-two,
real-abs/forward-le-05 is used by zero-ge-add-02, square-ls-one, square-ls-02, square-le-04, square-le, square-interval, square-eq-01, pnle-pos, mult-gt-both, mods-ls, ls-two-01,
real-abs/forward-lele is used by zero-gr-add-01, square-zero-01a, square-zero-01, square-ls-one, square-le-one, square-le, square-interval-01, square-interval, square-ge-one, pnls-posneg, pnls-pos, pnls-negpos, pnle-pos, pls-neg, ple-pos-better, abs-ls-same,
real-abs/forward-lels is used by zero-gr-add-01, zero-gr-03, square-zero-01a, square-zero-01, square-ls-one, square-ls-01, square-le-one, square-le, square-interval-01, square-interval, square-gr-one, square-ge-one, pnls-neg, pnle-neg, pls-pos-02, pls-neg, ple-neg, ls-pos-02, est-nle, abs-ls-same,
real-abs/forward-lsle is used by zero-ls-02, zero-gr-add-01, zero-gr-01, zero-ge-add-02, zero-ge-add-01, square-zero-02, square-zero-01a, square-zero-01, square-ls-one, square-ls-03a, square-le-one, square-le-05a, square-le-03, square-le, square-interval, square-gr-one, square-ge-one, square-eq-02, pls-pos-01, pls-pos, ple-pos, mult-pos, ls-two-01, ls-two, ls-same-05, le-same-01, abs-ls-same,
real-abs/gr-def is used by zero-neq-01, zero-gr-01, square-lez, ls-pos, ls-neg, le-pos, le-neg,
real-abs/le-def is used by zero-le-case, zero-le-03, zero-le-02, zero-le-01, zero-ge-case, zero-ge-add-02, zero-ge-add-01, zero-ge-03, zero-ge-02, zero-ge-01, twice-le-zero, square-zero-02, square-zero-01a, square-zero-01, square-ls-03a, square-le-one, square-le-05a, square-le-04, square-le-03, square-le, square-interval-01, square-interval, square-gez-01, square-gez, square-ge-one, square-eq-02, pzero-ls, pnls-posneg, pnls-pos, pnls-negpos, pnle-pos, pls-pos, pls-neg, ple-pos-better, ple-pos, ple-neg, mult-gt-both, ls-two-03, ls-two-01, le-same-04, le-same-02, le-same-01, le-same, le-pos, le-neg, le-abs, invmult-le-pos-add, invmult-le-pos, invmult-le-neg-add, invmult-le-neg, invmult-ge-pos, invmult-ge-neg, inv-le-pos, inv-le-neg, inv-ge-pos, inv-ge-neg, est-nle, abs-le-one-multiple,
real-abs/le-num is used by twice-le-zero, square-interval, ls-two,
real-abs/lels is used by zero-ls-case, zero-ls-03, zero-ls-02, zero-ls-01, zero-gr-case, zero-gr-03, zero-gr-02, zero-gr-01, zero-ge-add-02, twice-ls-zero, square-minus, square-ls-one, square-ls-02, square-ls-01, square-ls, square-lez, square-le-one, square-le-04, square-le, square-interval-01, square-interval, square-gr-one, square-ge-one, square-eq, square-abs, pzero-ls, pzero-gr, pls-pos-02, pls-pos-01, pls-pos, pls-neg, noeth-zero-ls, mult-pos, mult-gt-one, mult-gt-both, mods-ls, ls-two-02, ls-two, ls-same-05, ls-pos-02, ls-pos, ls-neg, le-same-02, le-neg, invmult-ls-pos-add, invmult-ls-pos, invmult-ls-neg-add, invmult-ls-neg, invmult-le-pos-add, invmult-le-neg-add, invmult-gr-pos, invmult-gr-neg, invmult-ge-pos, invmult-ge-neg, inv-ls-pos, inv-ls-neg, inv-gr-pos, inv-gr-neg, inv-ge-pos, inv-ge-neg, abs-not-neg, abs-ls-same, abs-ls-one-multiple, abs-ls-multiple-one, abs-eqall,
real-abs/lels-02 is used by zero-neq-01, zero-ls-case, zero-ls-02, zero-le-case, zero-le-03, zero-le-02, zero-gr-case, zero-gr-03, zero-gr-02, zero-gr-01, zero-ge-case, zero-ge-03, zero-ge-02, square-zero-02, square-zero-01, square-le, square-eq, pnls-posneg, pnls-pos, pnls-negpos, pnle-pos, pls-pos-02, pls-pos-01, ple-pos-better, mult-gt-both, le-same-02, est-nle, abs-not-neg, abs-eqall,
real-abs/lels-03 is used by zero-ls-case, zero-ls-02, zero-le-03, zero-le-02, zero-le-01, zero-gr-case, zero-gr-03, zero-gr-02, zero-ge-add-02, zero-ge-03, zero-ge-02, zero-ge-01, square-ls-one, square-ls, square-lez-01, square-le-05a, square-le, square-interval-01, square-gr-one, square-ge-one, square-eq, pzero-ls, pnle-pos, pnle-neg, noeth-zero-ls, mult-gt-one, mods-ls, ls-same-05, le-same-05, le-same-04, le-same-01, le-pos, le-neg, le-abs, invmult-ls-pos-add, invmult-ls-pos, invmult-ls-neg-add, invmult-ls-neg, invmult-le-pos-add, invmult-le-neg-add, invmult-gr-pos, invmult-gr-neg, invmult-ge-pos, invmult-ge-neg, inv-ls-pos, inv-ls-neg, inv-gr-pos, inv-gr-neg, inv-ge-pos, inv-ge-neg, abs-not-neg, abs-ls-same, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple,
real-abs/lenls is used by zero-le-01, zero-gr-add-01, zero-gr-03, zero-gr-01, zero-ge-add-01, zero-ge-01, square-zero-01a, square-zero-01, square-lez, square-le-one, square-le-04, square-le, square-interval-01, square-interval, square-gr-one, square-abs, pzero-ls, pzero-gr, pnls-posneg, pnls-pos, pnls-negpos, pnls-neg, pls-pos-02, pls-pos-01, pls-pos, ple-pos-better, ple-pos, ple-neg, mult-pos, ls-pos, ls-neg, le-same-04, le-same-01, le-same, le-pos, le-neg, le-abs, invmult-le-pos-add, invmult-le-pos, invmult-le-neg-add, invmult-le-neg, invmult-ge-pos, invmult-ge-neg, inv-ls-neg, inv-le-pos, inv-le-neg, inv-ge-pos, inv-ge-neg, est-nle, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple, abs-eqall,
real-abs/lep is used by num-distr-le1, ls-dist-06,
real-abs/lep-01 is used by square-zero-01a, square-ls-one, square-le, square-interval, square-ge-one, num-distr-le2, num-distr-add-le2, ls-dist-05, abs-ls-same,
real-abs/lep-02 is used by square-interval, num-distr-addboth-le2, num-distr-addboth-le1, num-distr-add-le1, le-dist-02, le-dist-01, le-dist,
real-abs/ler is used by zero-ls-02, zero-gr-03, zero-gr-02, zero-gr-01, zero-ge-add-02, square-lez-01, square-le, pls-neg, ls-pos, le-same-05, le-same-02, invmult-ls-pos,
real-abs/lsle-add-notge is used by square-le-04,
real-abs/negle-07 is used by square-le, square-ge-one, abs-ls-same,
real-abs/negle-13 is used by zero-le-01, square-le-one, square-le, square-gr-one, le-same-05, le-same-04, le-abs, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple,
real-abs/notle-pos is used by mods-ls,
real-abs/sub-le is used by invmult-le-neg-add, invmult-ge-pos-add, invmult-ge-neg-add,
real-abs/sub-le-01 is used by square-le, le-same-05, le-same-04, le-abs, invmult-le-pos-add, invmult-ge-neg-add, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple,
real-abs/zero-gels is used by square-ls-03a,
real-abs/zero-gels-01 is used by zero-ls-02, zero-gr-add-01, zero-gr-01, zero-ge-add-02, zero-ge-add-01, square-le, square-interval, square-eq-02, pzero-ls, pzero-gr, mult-pos,
real-abs/zero-gels-03 is used by square-le, square-interval,
real-abs/zero-gels-04 is used by square-le, pnls-posneg, pnls-negpos,
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-lez-01, square-eq-01, mult-pos,
real-basic/eqint-add is used by num-distr-ls2, num-distr-ls1, num-distr-le2, num-distr-le1, num-distr-eq2, num-distr-eq1, num-distr-addboth-ls2, num-distr-addboth-ls1, num-distr-addboth-le2, num-distr-addboth-le1, num-distr-addboth-eq2, num-distr-addboth-eq1, num-distr-add-ls2, num-distr-add-ls1, num-distr-add-le2, num-distr-add-le1, num-distr-add-eq2, num-distr-add-eq1, num-distr,
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 square-le, ple-neg, mods-zero-07,
real-basic/trans-lem3 is used by pnls-neg,
real-basic/add-assoc is used by zero-left, zero-le-01, zero-gr-add-01, zero-ge-add-02, zero-ge-add-01, two-sub-05, two-sub-04, two-sub-03, two-sub-02, two-sub-01, two-sub, 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, twice-le-zero, succ-rsplit, succ-rmerge, succ-lsplit, square-zero-02, square-zero-01a, square-zero-01, square-ls-one, square-ls-04a, square-ls-04, square-ls-03a, square-ls-03, square-ls-02, square-ls-01, square-le-one, square-le-05a, square-le-05, square-le-04, square-le-03, square-le, square-interval-01, square-interval, square-gr-one, square-ge-one, square-eq-one, square-eq-03, square-eq-02, square-eq-01, num-distr-ls2, num-distr-ls1, num-distr-le2, num-distr-le1, num-distr-eq2, num-distr-eq1, num-distr-addboth-ls2, num-distr-addboth-ls1, num-distr-addboth-le2, num-distr-addboth-le1, num-distr-addboth-eq2, num-distr-addboth-eq1, num-distr-add-ls2, num-distr-add-ls1, num-distr-add-le2, num-distr-add-le1, num-distr-add-eq2, num-distr-add-eq1, num-distr, mult-zero, mult-add-greater, mods-zero-07, mods-ls, minus-one, minus-left, ls-pos-02, ls-pos, ls-neg, 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, le-same-05, le-same-04, le-pos, le-neg, le-dist-02, le-dist-01, le-dist, le-abs, invmult-ls-pos-add, invmult-ls-neg-add, invmult-le-pos-add, invmult-le-neg-add, invmult-gr-pos-add, invmult-gr-neg-add, invmult-ge-pos-add, invmult-ge-neg-add, inv-mult-add-eq, eq-succ-01, eq-succ, eq-nonzero, eq-dist, add-mult-two, abs-ls-same, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple, abs-ite, abs-eqall,
real-basic/add-comm is used by zero-left, zero-le-01, zero-gr-add-01, zero-ge-add-02, zero-ge-add-01, two-sub-05, two-sub-04, two-sub-03, two-sub-02, two-sub-01, two-sub, 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, twice-le-zero, succ-rsplit, succ-rmerge, succ-lsplit, square-zero-02, square-zero-01a, square-zero-01, square-ls-one, square-ls-04a, square-ls-04, square-ls-03a, square-ls-03, square-ls-02, square-ls-01, square-le-one, square-le-05a, square-le-05, square-le-04, square-le-03, square-le, square-interval-01, square-interval, square-gr-one, square-ge-one, square-eq-one, square-eq-03, square-eq-02, square-eq-01, num-distr-ls2, num-distr-ls1, num-distr-le2, num-distr-le1, num-distr-eq2, num-distr-eq1, num-distr-addboth-ls2, num-distr-addboth-ls1, num-distr-addboth-le2, num-distr-addboth-le1, num-distr-addboth-eq2, num-distr-addboth-eq1, num-distr-add-ls2, num-distr-add-ls1, num-distr-add-le2, num-distr-add-le1, num-distr-add-eq2, num-distr-add-eq1, num-distr, mult-zero, mult-add-greater, mods-zero-07, mods-ls, minus-one, minus-left, ls-pos-02, ls-pos, ls-neg, 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, le-same-05, le-same-04, le-pos, le-neg, le-dist-02, le-dist-01, le-dist, le-abs, invmult-ls-pos-add, invmult-ls-neg-add, invmult-le-pos-add, invmult-le-neg-add, invmult-gr-pos-add, invmult-gr-neg-add, invmult-ge-pos-add, invmult-ge-neg-add, inv-mult-add-eq, eq-succ-01, eq-succ, eq-nonzero, eq-dist, add-mult-two, abs-ls-same, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple, abs-ite, abs-eqall,
real-basic/add-in is used by two-sub-05, succ-rsplit, succ-rmerge, succ-lsplit, square-eq-02, num-distr-addboth-eq2, num-distr-addboth-eq1, num-distr-add-eq1, num-distr, eq-succ-01, eq-succ, eq-dist, add-mult-two,
real-basic/add-less is used by square-le, ls-dist-04,
real-basic/add-zero is used by zero-le-01, two-sub-04, two-sub-03, 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, square-le, le-same-05, le-same-04, le-abs, inv-mult-add-eq, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple, abs-eqall,
real-basic/bls-01 is used by zero-neq-01, zero-ls-01, zero-le-case, zero-gr-01, zero-ge-case, zero-ge-add-02, zero-eq, square-lez, square-le-one, square-le-04, square-le, square-gr-one, square-eq-01, square-eq, square-abs, pzero-ls, pzero-gr, pnls-neg, pnle-pos, pls-neg, mult-gt-both, mult-add-greater, ls-pos, ls-neg, le-same-05, le-same-04, le-same-02, le-abs, invmult-ls-pos, abs-not-neg, abs-ls-same, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple, abs-eqall,
real-basic/blst is used by square-le-04,
real-basic/blst-01 is used by zero-le-case, zero-ge-case, zero-eq, le-same-05, le-same-04, le-abs, inv-eq, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple, abs-eqall,
real-basic/blst-02 is used by square-zero, square-eq, mult-pos, invmult-ls-pos,
real-basic/double-neg is used by zero-le-01, zero-gr-01, square-lez, square-le, ls-neg, le-neg, 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 two-sub-05, two-sub-04, two-sub-03, two-sub-02, two-ls-02, twice-le-zero, square-zero-01a, square-zero-01, square-ls-04a, square-ls-04, square-ls-03a, square-ls-03, square-le-05a, square-le-05, square-interval-01, square-interval, square-eq-03, square-eq-02, mult-zero, mods-zero-07,
real-basic/eqint-num is used by zero-neq-01, zero-neq, zero-left, zero-eq, square-zero, square-eq-one, posint-factor, neq-not-zero-01, neq-not-zero, minus-one, minus-left, le-abs, inv-twice, inv-mult, inv-eq, eq-same, eq-nonzero-int, eq-nonzero, abs-ite, abs-eqall,
real-basic/irref is used by square-le, square-gr-one, square-ge-one, square-eq, ls-pos, ls-neg, invmult-ls-pos, abs-ls-same,
real-basic/less-add-cancel-l is used by square-zero-02, square-zero-01a, square-le-04, square-interval-01, square-interval, num-distr-addboth-ls2, num-distr-addboth-ls1, num-distr-add-ls1, ls-dist-02, ls-dist-01, ls-dist, ls-add-03, ls-add-02,
real-basic/lf-02 is used by zero-neq-01, zero-neq, zero-ls-03, square-le, square-eq, pzero-ls, pzero-gr, pls-neg, mult-pos, mods-zero-07, minus-one, invmult-ls-pos, eq-same-03, eq-same-02, abs-ls-same,
real-basic/lf-03 is used by zero-neq-01, zero-ls-03, zero-eq, square-le, square-eq, pzero-ls, pzero-gr, pls-neg, invmult-ls-pos, eq-same-03, eq-same-02,
real-basic/ls is used by zero-ge-add-01, square-zero-02, square-zero-01a, square-zero-01, square-ls-03a, square-ls-01, square-le-one, square-le-05a, square-le-03, square-le, square-interval, square-gr-one, square-eq-02, num-distr-ls2, num-distr-add-ls2, mult-add-greater, ls-dist-03,
real-basic/ls-02 is used by zero-gr-add-01, square-zero-01a, square-le, square-interval-01, square-interval, num-distr-ls1, mods-zero-07, minus-one, ls-pos-02, ls-dist-04, abs-ls-same,
real-basic/ls-num is used by zero-ls-03, zero-ls-02, zero-le-case, zero-gr-03, zero-gr-02, zero-gr-01, zero-ge-case, zero-ge-add-02, twice-ls-zero, square-zero-02, square-zero-01a, square-zero-01, square-zero, square-minus, square-ls-one, square-ls-03a, square-le-one, square-le-05a, square-interval, square-gr-one, square-ge-one, square-eq-02, pzero-ls, pzero-gr, mods-zero-07, minus-one, ls-two-03, ls-two-02, ls-two-01, ls-same-05, ls-posint, ls-negint, ls-forward, le-same-04, le-same-01, le-posint, le-negint, le-abs, invmult-ls-pos, eq-same-03, eq-same-02, eq-pos, eq-neg, abs-ls-same, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple,
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 square-zero-01, square-eq-one, minus-one,
real-basic/neg is used by abs-eqall,
real-basic/neg-01 is used by le-same-04, le-abs, abs-ls-one-multiple, abs-ls-multiple-one, abs-le-one-multiple,
real-basic/neg-02 is used by zero-neq-01, zero-neq, zero-le-01, zero-gr-01, square-lez, square-le, ls-neg, le-neg,
real-basic/neg-05 is used by square-minus, abs-not-neg,
real-basic/neg-09 is used by square-le, ls-pos, ls-neg, le-pos, le-neg, abs-ls-same,
real-basic/neg-10 is used by zero-neq, square-le, le-abs,
real-basic/neg-12 is used by minus-one-01,
real-basic/neg-add is used by two-sub-05, ls-neg, le-neg,
real-basic/neg-zero is used by square-minus,
real-basic/negadd-eq is used by two-sub,
real-basic/negeq is used by square-eq-one, posint-factor, minus-one, minus-left, abs-ite, abs-eqall,
real-basic/negl-ls is used by square-ls-one, square-le, square-ge-one, ls-pos-02, abs-ls-same,
real-basic/negladd-ls is used by invmult-ls-neg-add, invmult-gr-pos-add, invmult-gr-neg-add,
real-basic/negr-ls is used by square-le, square-gr-one,
real-basic/negradd-ls is used by invmult-ls-pos-add, invmult-gr-neg-add,
real-basic/sub-eq is used by two-sub-05, two-sub-04, two-sub-02, two-sub-01, two-sub, inv-mult-add-eq, abs-eqall,
real-basic/sub-eq-01 is used by zero-left, minus-left, inv-mult-add-eq, eq-nonzero,
real-basic/trans is used by zero-neq-01, zero-ls-03, zero-gr-add-01, zero-gr-01, zero-ge-add-02, square-zero-02, square-ls-one, square-le, square-interval, square-ge-one, pzero-ls, pnls-neg, pnle-neg, pls-pos, pls-neg, ple-neg, mult-pos, ls-two-03, ls-two-02, ls-same-05, ls-pos-02, le-same-02, le-same-01, abs-not-neg, abs-ls-same,
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-ls2, num-distr-ls1, num-distr-le2, num-distr-le1, num-distr-eq2, num-distr-eq1, num-distr-addboth-ls2, num-distr-addboth-ls1, num-distr-addboth-le2, num-distr-addboth-le1, num-distr-addboth-eq2, num-distr-addboth-eq1, num-distr-add-ls2, num-distr-add-ls1, num-distr-add-le2, num-distr-add-le1, num-distr-add-eq2, num-distr-add-eq1,
int-abs/forward-le-01 is used by num-distr-ls1, num-distr-le1, num-distr-eq1, num-distr-addboth-ls1, num-distr-addboth-le1, num-distr-addboth-eq1, num-distr-add-ls1, num-distr-add-le1, num-distr-add-eq1,
int-abs/forward-le-02 is used by posint-factor,
int-abs/forward-le-05 is used by num-distr-ls2, num-distr-le2, num-distr-eq2, num-distr-addboth-ls2, num-distr-addboth-le2, num-distr-addboth-eq2, num-distr-add-ls2, num-distr-add-le2, num-distr-add-eq2, ls-posint, le-posint,
int-abs/gr-def is used by ls-posint, le-posint,
int-abs/lels is used by ls-posint, le-posint,
int-abs/lels-03 is used by ls-posint, le-posint,
int-abs/lep is used by num-distr-ls1, num-distr-le1, num-distr-eq1, num-distr-addboth-ls1, num-distr-addboth-le1, num-distr-addboth-eq1, num-distr-add-ls1, num-distr-add-le1, num-distr-add-eq1,
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-ls1, num-distr-le1, num-distr-eq1, num-distr-addboth-ls1, num-distr-addboth-le1, num-distr-addboth-eq1, num-distr-add-ls1, num-distr-add-le1, num-distr-add-eq1,