Used simplifier rules/spec theorems by specification

Used from specification int-basic1

• int-basic1/forward-pos is used by test-truncate-01,
• int-basic1/irref is used by scale-neq-01, scale-le,
• int-basic1/ls-01 is used by scale-le, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, equality-any,
• int-basic1/lst-01 is used by getint-pos,
• int-basic1/numlsf is used by maxScale-not-negt,
• int-basic1/numlslsdel-01 is used by test-truncate-01,

Used from specification int-mult

• int-mult/associativity is used by maxScale-pot10-add,
• int-mult/commutativity is used by maxScale-zero-01,
• int-mult/dist-lsplit is used by maxScale-pot10-add,
• int-mult/zero-eq is used by maxScale-pot10-01, equality-any,
• int-mult/Mult-zero is used by mkDecimal-enlarge, maxScale-pot10-02, maxScale-pot10-01, equality-any, eq-zero,
• int-mult/abs-eqall is used by eq-same,
• int-mult/associativity is used by mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-add, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, getint-zero, equality-any, eq-zero, eq-same, dec2int-def-any,
• int-mult/commutativity is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-int, mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-add, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, getint-zero, equality-any, eq-zero, eq-same, dec2int-def-any,
• int-mult/eq-nonzero is used by maxScale-pot10-add, equality-any, eq-same,
• int-mult/eq-same-01 is used by equality-any,
• int-mult/le-same-04 is used by eq-same,
• int-mult/neq-not-zero is used by maxScale-pot10-add,
• int-mult/numls-09 is used by eq-same,
• int-mult/one is used by mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-add, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, getint-zero, equality-any, eq-same, dec2int-def-any,
• int-mult/zero-eq is used by maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, getint-zero, equality-any, eq-zero,
• int-mult/zero-gr is used by eq-same,
• int-mult/zero-neq-01 is used by maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10,

Used from specification nat

• nat/le-add-01 is used by eq-same,
• nat/lels is used by eq-same,

Used from specification int-pot

• int-pot/Pot-pos is used by mkDecimal-maxScale-le-int, mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, equality-any, dec2int-def-any,
• int-pot/pot-dist-pos is used by maxScale-pot10-add,
• int-pot/pot-eq-sub is used by equality-any,
• int-pot/pot-mod-add-zero is used by maxScale-pot10-add,
• int-pot/succ is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, maxScale-zero-01,
• int-pot/eq-pos is used by maxScale-pot10-add,
• int-pot/pot-zero-01 is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-int, maxScale-zero-01, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, equality-any, eq-zero, dec2int-zero, dec2int-def-any,

Used from specification int-abs

• int-abs/Abs-pos is used by mkDecimal-maxScale-le-int, mkDecimal-enlarge,
• int-abs/lels-02 is used by getint-pos-01,
• int-abs/Sub-def is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le, maxScale-pot10-add,
• int-abs/abs-01 is used by mkDecimal-scale-not-neg, mkDecimal-enlarge,
• int-abs/abs-03 is used by equality-any,
• int-abs/abs-06 is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, mkDecimal-enlarge, equality-any, eq-same, dec2int-def-any,
• int-abs/abs-07 is used by mkDecimal-scale-not-neg, mkDecimal-maxScale-le, mkDecimal-enlarge, equality-any, eq-same,
• int-abs/abs-08 is used by mkDecimal-enlarge, getint-neg-02,
• int-abs/abs-10 is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-int, dec2int-def-any,
• int-abs/abs-abs is used by scale-neq-01, scale-le, mkDecimal-reduce-scale, mkDecimal-reduce-int, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-scale, equality-any, dec2int-def-any,
• int-abs/absls is used by scale-not-neg, scale-le, mkDecimal-reduce-scale, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-enlarge, equality-any, eq-zero, dec2int-def-any,
• int-abs/abssub is used by mkDecimal-maxScale-le,
• int-abs/anti is used by mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-add, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10,
• int-abs/bet-01 is used by maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10,
• int-abs/forward-le-01 is used by mkDecimal-reduce-int, mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-add, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10,
• int-abs/forward-le-02 is used by scale-not-neg, mkDecimal-reduce-int, mkDecimal-enlarge, maxScale-pot10-add, maxScale-not-negt, getint-neg-02,
• int-abs/forward-le-03 is used by getint-neg-02,
• int-abs/forward-le-04 is used by getint-neg-02,
• int-abs/forward-le-05 is used by test-truncate-01, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, maxScale-le-zero,
• int-abs/forward-lels is used by maxScale-pot10-add,
• int-abs/forward-lsle is used by mkDecimal-enlarge, maxScale-pot10-add,
• int-abs/lels is used by test-truncate-01, scale-not-neg, scale-negate, scale-le, mkDecimal-selectors, mkDecimal-reduce-scale, mkDecimal-reduce-int, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-scale, mkDecimal-maxScale-le-int, mkDecimal-enlarge, maxScale-zero-01, maxScale-pot10-nls, maxScale-pot10-add, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, maxScale-not-negt, intvalue-mod-10, getint-zero, getint-pos, getint-neg-02, getint-neg, equality-any, dec2int-def-any,
• int-abs/lels-01 is used by scale-neq-01, scale-le, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-nle, mkDecimal-maxScale-le-int, maxScale-zero-01, maxScale-pot10-add, maxScale-le-zero, getint-neg-02, ex-mkDecimal, equality-any,
• int-abs/lels-02 is used by mkDecimal-maxScale-le, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, maxScale-le-zero, getint-pos-01, equality-any,
• int-abs/lels-03 is used by scale-neq, mkDecimal-maxScale-nle, mkDecimal-maxScale-le-scale, mkDecimal-maxScale-le-int, maxScale-pot10-add,
• int-abs/lenls is used by mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, maxScale-pot10-add, getint-neg-02, equality-any,
• int-abs/leone is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10,
• int-abs/mone-06 is used by mkDecimal-maxScale-le-int,
• int-abs/neg is used by mkDecimal-reduce-scale,
• int-abs/neg-03 is used by getint-neg,
• int-abs/neg-06 is used by mkDecimal-reduce-scale,
• int-abs/neg-10 is used by scale-negate, getint-neg,
• int-abs/neg-13 is used by getint-neg-02,
• int-abs/neg-15 is used by mkDecimal-negated,
• int-abs/negeq is used by mkDecimal-negated, getint-neg-01, getint-neg,
• int-abs/numle-03 is used by getint-neg-02,
• int-abs/numlelsdel-01 is used by getint-neg-02,
• int-abs/numls-02 is used by mkDecimal-maxScale-le-int, getint-neg-02,
• int-abs/numls-03 is used by maxScale-not-negt,
• int-abs/sub-add-01 is used by mkDecimal-enlarge, maxScale-pot10-02,
• int-abs/sub-eq is used by mkDecimal-negated, mkDecimal-maxScale-le-scale, mkDecimal-maxScale-le, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10,
• int-abs/sub-eq-01 is used by maxScale-pot10-add, equality-any,
• int-abs/sub-le-01 is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-scale, mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-add, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10,
• int-abs/sub-ls is used by scale-neq-01, scale-le, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-int, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, equality-any,
• int-abs/sub-ls-01 is used by mkDecimal-reduce-int, maxScale-pot10-nls, maxScale-pot10-add, equality-any,
• int-abs/sub-pred is used by mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, equality-any, dec2int-def-any,
• int-abs/sub-sub is used by mkDecimal-reduce-scale, equality-any,
• int-abs/sub-sub-03 is used by maxScale-pot10-add,
• int-abs/sub-zero-01 is used by mkDecimal-reduce-scale, mkDecimal-maxScale-le,
• int-abs/subsub is used by mkDecimal-enlarge,
• int-abs/succ-01 is used by mkDecimal-maxScale-le-scale, mkDecimal-maxScale-le-int,
• int-abs/succ-02 is used by scale-neq-01, scale-le, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-int,
• int-abs/zero-gels-01 is used by maxScale-pot10-add, getint-neg-02,
• int-abs/zero-gels-03 is used by maxScale-pot10-add, getint-neg-02,
• int-abs/zero-gels-04 is used by maxScale-pot10-add,

Used from specification int-min

• int-min/Min-left is used by mkDecimal-reduce-int,
• int-min/Min-right is used by mkDecimal-reduce-int, maxScale-pot10-add, maxScale-min,
• int-min/Min-left is used by mkDecimal-reduce-int, maxScale-pot10-add, maxScale-min,
• int-min/Min-right is used by mkDecimal-reduce-int,
• int-min/max is used by mkDecimal-reduce-scale,
• int-min/max-a is used by mkDecimal-reduce-scale,
• int-min/max-c is used by mkDecimal-reduce-scale,
• int-min/min-03 is used by maxScale-pot10-add,
• int-min/min-a is used by mkDecimal-reduce-int, maxScale-pot10-add, maxScale-min,
• int-min/min-abs-zero is used by mkDecimal-reduce-int,
• int-min/min-c is used by mkDecimal-reduce-int, maxScale-pot10-add, maxScale-min,
• int-min/min-right is used by mkDecimal-reduce-int,

Used from specification nat-basic2

• nat-basic2/a is used by equality-any, eq-same,
• nat-basic2/add-base is used by eq-same,
• nat-basic2/c is used by equality-any, eq-same,
• nat-basic2/l is used by equality-any,

Used from specification intnat

• intnat/abs-pred is used by mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10,
• intnat/labs is used by scale-not-neg, scale-negate, scale-le, mkDecimal-selectors, mkDecimal-reduce-scale, mkDecimal-reduce-int, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-scale, mkDecimal-maxScale-le-int, maxScale-zero-01, maxScale-not-negt, intvalue-mod-10, getint-zero, getint-pos, getint-neg-02, getint-neg, equality-any, eq-same, dec2int-def-any,
• intnat/labs-01 is used by eq-same,

Used from specification int-basic2

• int-basic2/not-zero-pos is used by mkDecimal-enlarge,
• int-basic2/add-a is used by test-inc-01, scale-neq-01, scale-le, mkDecimal-reduce-int, mkDecimal-negated, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-scale, mkDecimal-maxScale-le-int, mkDecimal-maxScale-le, mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-add, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, maxScale-not-negt, getint-neg-02, getint-neg, equality-any,
• int-basic2/add-c is used by test-inc-01, scale-neq-01, scale-le, mkDecimal-reduce-scale, mkDecimal-reduce-int, mkDecimal-negated, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-scale, mkDecimal-maxScale-le-int, mkDecimal-maxScale-le, mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-add, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, maxScale-not-negt, getint-neg-02, getint-neg, equality-any,
• int-basic2/add-in is used by maxScale-pot10-add,
• int-basic2/add-zero is used by mkDecimal-negated, mkDecimal-maxScale-le, mkDecimal-enlarge, maxScale-pot10-add, maxScale-pot10-02, equality-any,
• int-basic2/eq is used by mkDecimal-maxScale-le-scale,
• int-basic2/ls is used by mkDecimal-enlarge,
• int-basic2/lst-03 is used by mkDecimal-reduce-int, maxScale-pot10-nls,
• int-basic2/pred is used by mkDecimal-maxScale-le-int,

Used from specification int-div

• int-div/div-div is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-int,
• int-div/div-div-intro is used by maxScale-zero-01,
• int-div/mod-zero-05 is used by getint-neg-02,
• int-div/mod-zero-num is used by equality-any,
• int-div/modex is used by getint-zero, equality-any, eq-same, dec2int-def-any,
• int-div/abs is used by scale-not-neg, scale-negate, scale-le, mkDecimal-selectors, mkDecimal-reduce-scale, mkDecimal-reduce-int, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-scale, mkDecimal-maxScale-le-int, maxScale-zero-01, maxScale-not-negt, intvalue-mod-10, getint-zero, getint-pos, getint-neg-02, getint-neg, equality-any, eq-same, dec2int-def-any,
• int-div/abs-div10-le is used by scale-not-neg, scale-negate, scale-le, mkDecimal-selectors, mkDecimal-reduce-scale, mkDecimal-reduce-int, mkDecimal-maxScale-nle-scale, mkDecimal-maxScale-nle-int, mkDecimal-maxScale-le-scale, mkDecimal-maxScale-le-int, maxScale-zero-01, maxScale-not-negt, intvalue-mod-10, getint-zero, getint-pos, getint-neg-02, getint-neg, equality-any, dec2int-def-any,
• int-div/div-div is used by maxScale-zero-01,
• int-div/div-eq-same-01 is used by mkDecimal-maxScale-le-int, dec2int-zero,
• int-div/div-eq-zero-01 is used by maxScale-zero-01,
• int-div/div-lezero is used by getint-pos,
• int-div/div-ls-zero is used by getint-neg-02,
• int-div/div-mult-01 is used by dec2int-def-any,
• int-div/div-mult-num is used by mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, getint-zero, equality-any, eq-same, dec2int-def-any,
• int-div/div-ngr-zero is used by getint-neg-02,
• int-div/div-zero-ngr is used by getint-pos,
• int-div/divmult is used by eq-same,
• int-div/mod-neg-01 is used by scale-negate, getint-neg,
• int-div/mod-zero-05 is used by maxScale-zero-01,
• int-div/mod-zero-08 is used by getint-pos,
• int-div/mod-zero-num is used by mkDecimal-enlarge, maxScale-pot10-nls, maxScale-pot10-02, maxScale-pot10-01, maxScale-pot10, equality-any,
• int-div/neg-01 is used by scale-negate, getint-neg,
• int-div/neqf is used by dec2int-def-any,
• int-div/one is used by mkDecimal-reduce-int, mkDecimal-maxScale-nle-int, maxScale-zero-01, dec2int-def-any,
• int-div/zero is used by dec2int-def-any,