Used simplifier rules/spec theorems by specification

Used from specification nat

• nat/anti is used by bounded-any-postfix,
• nat/elim-sub is used by bounded-any-postfix,
• nat/eq-01 is used by bounded-any-postfix,
• nat/fle is used by limit-unique,
• nat/ge is used by monge-converges-inf, convergesto-neg-convergesto, bounded-any-postfix, limit-unique, monle-converges-sup,
• nat/le-def is used by bounded-any-postfix, limit-unique,
• nat/lels is used by bounded-any-postfix,
• nat/lels-02 is used by bounded-any-postfix,
• nat/lels-03 is used by bounded-any-postfix, limit-unique,
• nat/lep-02 is used by bounded-any-postfix,
• nat/ler is used by bounded-any-postfix, limit-unique,
• nat/let is used by bounded-any-postfix,
• nat/succ-01 is used by bounded-any-postfix,
• nat/zero-01 is used by bounded-any-postfix,

Used from specification real-multdiv

• real-multdiv/abs-ite is used by limit-unique,
• real-multdiv/commutativity is used by limit-unique,
• real-multdiv/add-mult-two is used by convergesto-neg-convergesto, limit-unique,
• real-multdiv/commutativity is used by convergesto-neg-convergesto, limit-unique, monle-converges-sup,
• real-multdiv/inv-def is used by limit-unique,
• real-multdiv/inv-le-pos is used by monle-converges-sup,
• real-multdiv/invmult-gr-pos is used by limit-unique, monle-converges-sup,
• real-multdiv/le-same is used by monle-converges-sup,
• real-multdiv/ls-posint is used by convergesto-neg-convergesto, limit-unique,
• real-multdiv/ls-same is used by monle-converges-sup,
• real-multdiv/minus-left is used by limit-unique,
• real-multdiv/mult-ass is used by convergesto-neg-convergesto, limit-unique, monle-converges-sup,
• real-multdiv/mult-one is used by limit-unique, monle-converges-sup,
• real-multdiv/zero-le is used by monle-converges-sup,
• real-multdiv/zero-left is used by limit-unique, monle-converges-sup,

Used from specification real-abs

• real-abs/Abs-neg is used by convergesto-neg-convergesto, monle-converges-sup,
• real-abs/Abs-pos is used by convergesto-neg-convergesto, monle-converges-sup,
• real-abs/abs-neg is used by monge-converges-inf,
• real-abs/antr is used by monle-converges-sup,
• real-abs/forward-lels is used by monle-boundedle-f-below-bound, monle-converges-sup,
• real-abs/forward-lsle is used by monge-converges-inf, monle-boundedle-limit-below-bound,
• real-abs/lels is used by limit-unique, monle-converges-sup,
• real-abs/lsls-add-notge is used by limit-unique,
• real-abs/Abs-pos is used by convergesto-neg-convergesto,
• real-abs/abs-06 is used by convergesto-neg-convergesto, limit-unique,
• real-abs/abssub-02 is used by convergesto-neg-convergesto, limit-unique,
• real-abs/forward-le is used by convergesto-neg-convergesto,
• real-abs/forward-lels is used by limit-unique,
• real-abs/forward-lsle is used by convergesto-neg-convergesto,
• real-abs/ge-def is used by monge-neg-monle, boundedge-neg-boundedle,
• real-abs/gr-def is used by monge-converges-inf, convergesto-neg-convergesto, limit-unique, monle-converges-sup,
• real-abs/le-def is used by monge-converges-inf, monle-boundedle-f-below-bound, monge-neg-monle, monle-boundedle-limit-below-bound, bounded-any-postfix, boundedge-neg-boundedle, monle-converges-sup, monge-limit-inf,
• real-abs/le-num is used by monle-converges-sup,
• real-abs/lels is used by monge-converges-inf, monge-boundedge-limit-above-bound, convergesto-neg-convergesto, monge-boundedge-f-above-bound, limit-unique, monle-converges-sup,
• real-abs/lels-02 is used by convergesto-neg-convergesto,
• real-abs/lels-03 is used by monge-converges-inf, monle-boundedle-f-below-bound, monge-neg-monle, monle-boundedle-limit-below-bound, convergesto-neg-convergesto, bounded-any-postfix, boundedge-neg-boundedle, limit-unique, monle-converges-sup, monge-limit-inf,
• real-abs/lenls is used by monge-boundedge-limit-above-bound, convergesto-neg-convergesto, monge-boundedge-f-above-bound, limit-unique, monle-converges-sup,
• real-abs/lep-01 is used by monle-converges-sup,
• real-abs/lep-02 is used by monle-converges-sup,
• real-abs/ler is used by monle-converges-sup,
• real-abs/negle-07 is used by monge-converges-inf, monge-limit-inf,
• real-abs/negle-13 is used by monge-converges-inf, monge-neg-monle, boundedge-neg-boundedle, monge-limit-inf,
• real-abs/sub-def is used by monge-converges-inf, convergesto-neg-convergesto, limit-unique, monle-converges-sup,
• real-abs/sub-le is used by limit-unique,
• real-abs/sub-le-01 is used by monge-converges-inf, monge-neg-monle, convergesto-neg-convergesto, boundedge-neg-boundedle, monle-converges-sup, monge-limit-inf,

Used from specification real-basic

• real-basic/add-comm is used by monle-converges-sup,
• real-basic/neg-add is used by monge-converges-inf,
• real-basic/add-assoc is used by monge-converges-inf, monge-neg-monle, convergesto-neg-convergesto, boundedge-neg-boundedle, limit-unique, monle-converges-sup, monge-limit-inf,
• real-basic/add-comm is used by monge-converges-inf, monge-neg-monle, limit-neg-limit, monge-boundedge-limit-above-bound, convergesto-neg-convergesto, boundedge-neg-boundedle, monge-boundedge-f-above-bound, limit-unique, monle-converges-sup, monge-limit-inf,
• real-basic/add-less is used by convergesto-neg-convergesto,
• real-basic/add-zero is used by monge-converges-inf, monge-neg-monle, convergesto-neg-convergesto, boundedge-neg-boundedle, limit-unique, monge-limit-inf,
• real-basic/bls-01 is used by convergesto-neg-convergesto, limit-unique,
• real-basic/blst-01 is used by limit-unique,
• real-basic/double-neg is used by monge-converges-inf, converges-neg-converges, convergesto-neg-convergesto, limit-unique, monle-converges-sup,
• real-basic/irref is used by monge-converges-inf, monle-boundedle-f-below-bound, monle-boundedle-limit-below-bound, bounded-any-postfix, limit-unique,
• real-basic/less-add-cancel-l is used by monge-converges-inf, limit-unique, monle-converges-sup, monge-limit-inf,
• real-basic/lf-03 is used by monge-converges-inf, monge-limit-inf,
• real-basic/ls-02 is used by convergesto-neg-convergesto,
• real-basic/ls-num is used by limit-unique, monle-converges-sup,
• real-basic/neg-08 is used by convergesto-neg-convergesto, limit-unique, monle-converges-sup,
• real-basic/neg-12 is used by monge-limit-inf,
• real-basic/neg-add is used by convergesto-neg-convergesto, limit-unique, monle-converges-sup,
• real-basic/negadd is used by limit-unique,
• real-basic/negeq is used by monge-converges-inf, limit-neg-limit, monge-limit-inf,
• real-basic/negl-ls is used by monge-boundedge-limit-above-bound,
• real-basic/negladd-ls is used by convergesto-neg-convergesto, limit-unique,
• real-basic/negr-ls is used by monge-boundedge-f-above-bound,
• real-basic/negradd-ls is used by convergesto-neg-convergesto, limit-unique,
• real-basic/sub-eq is used by convergesto-neg-convergesto, limit-unique,
• real-basic/sub-eq-01 is used by limit-unique,
• real-basic/sub-ls-02 is used by limit-unique,
• real-basic/trans is used by convergesto-neg-convergesto, bounded-any-postfix, limit-unique,

Used from specification nat-basic

• nat-basic/a is used by bounded-any-postfix,
• nat-basic/add-base is used by bounded-any-postfix,
• nat-basic/c is used by bounded-any-postfix,
• nat-basic/f is used by bounded-any-postfix, limit-unique,
• nat-basic/l-01 is used by bounded-any-postfix,
• nat-basic/l-02 is used by bounded-any-postfix,
• nat-basic/s-04 is used by bounded-any-postfix,
• nat-basic/succ is used by bounded-any-postfix,

Used from specification real-supinf

• real-supinf/boundedge-neg-boundedle is used by monge-converges-inf, monge-limit-inf,
• real-supinf/boundedle-def is used by monge-converges-inf, monle-boundedle-f-below-bound, monle-boundedle-limit-below-bound, bounded-any-postfix, monle-converges-sup, monge-limit-inf,
• real-supinf/inf-neg-sup is used by monge-converges-inf, monge-limit-inf,
• real-supinf/sup-lowest-upperbound is used by monle-boundedle-limit-below-bound, monle-converges-sup,
• real-supinf/sup-upperbound is used by monle-boundedle-f-below-bound, monle-converges-sup,
• real-supinf/upperbound-def is used by monge-converges-inf, monle-boundedle-f-below-bound, monle-boundedle-limit-below-bound, bounded-any-postfix, monle-converges-sup, monge-limit-inf,