Used simplifier rules/spec theorems by specification

Used from specification int-mult

• int-mult/associativity is used by mult-def-02, equality-01, distributivity, add-def-02,
• int-mult/commutativity is used by transitivity, factor-rat, equality-pos, equality-01, distributivity, add-def-02,
• int-mult/dist-lsplit is used by add-asso,
• int-mult/dist-rsplit is used by add-eq, add-asso,
• int-mult/eq-pos-01 is used by equality-01,
• int-mult/minus-left is used by factor-rat-02,
• int-mult/zero-eq is used by div-neg-01, add-def-02,
• int-mult/zero-le is used by div-pos-def,
• int-mult/Mult-zero is used by num-neg-03, num-div-denom-01, negate, mult-zero-01, mult-zero, mult-def-02, ls-def, int-mult, int-add, factor-rat-03, equality-pos, equality-02, equality-01, div-pos-def, div-def-01, add-zero, add-eq, add-def-03, add-def-02, Extsimple,
• int-mult/abs-eqall is used by root-is-irrational, mult-def-02, factor-rat-03, factor-rat-02, add-def-02,
• int-mult/associativity is used by transitivity, totality, sub-def-01, root-is-irrational, rational-add-same, num-neg-03, num-div-denom-01, num-div-denom, negate, mult-zero-01, mult-zero, mult-one, mult-def-03, mult-def-02, mult-ass, ls-def, irreflexivity, int-mult, int-add, factor-rat-03, factor-rat-02, factor-rat-01, equality-pos, equality-02, equality-01, equal-same, div-pos-def, div-neg-01, div-neg, div-def-01, distributivity, add-zero, add-eq, add-def-03, add-def-02, add-asso, Extsimple,
• int-mult/commutativity is used by transitivity, totality, sub-def-01, root-is-irrational, rational-add-same, num-neg-03, num-div-denom-01, num-div-denom, negate, mult-zero-01, mult-zero, mult-one, mult-def-03, mult-def-02, mult-def-01, mult-comm, mult-ass, ls-def, irreflexivity, int-mult, int-add, factor-rat-03, factor-rat-02, factor-rat-01, equality-pos, equality-02, equality-01, equal-same, div-pos-def, div-neg-01, div-neg, div-def-01, distributivity, add-zero, add-eq, add-def-03, add-def-02, add-def-01, add-comm, add-asso, Extsimple,
• int-mult/dist-rmerge is used by rational-add-same, distributivity, add-def-02,
• int-mult/eq-neg is used by factor-rat-01,
• int-mult/eq-nonzero is used by factor-rat-01, equal-same, add-eq,
• int-mult/le-pos is used by totality,
• int-mult/le-same-05 is used by mult-def-02, add-def-02,
• int-mult/ls-pos is used by transitivity, irreflexivity,
• int-mult/minus-left is used by sub-def-01, num-div-denom-01, num-div-denom, mult-def-03, ls-def, factor-rat-02, factor-rat-01, equality-02, div-neg-01, div-neg, div-def-01, add-def-03,
• int-mult/one is used by root-is-irrational, num-neg-03, negate, mult-zero-01, mult-zero, mult-one, int-mult, int-add, div-pos-def, div-neg-01, div-def-01, add-zero,
• int-mult/square-eq is used by root-is-irrational,
• int-mult/square-zero is used by root-is-irrational,
• int-mult/zero-eq is used by factor-rat-03, equality-pos, equality-02, div-pos-def, div-neg-01, div-def-01, add-def-03, add-def-02,
• int-mult/zero-ge is used by ls-def, div-pos-def,
• int-mult/zero-gr is used by totality, root-is-irrational, mult-def-02, ls-def, factor-rat-03, div-pos-def, add-eq, add-def-02,
• int-mult/zero-le is used by ls-def,
• int-mult/zero-ls is used by factor-rat-02, equality-02,
• int-mult/zero-neq-01 is used by mult-def-03, mult-def-02, mult-ass, factor-rat-03, equality-pos, equality-02, equality-01, distributivity, add-eq, add-asso,

Used from specification int-basic1

• int-basic1/trans is used by transitivity,
• int-basic1/forward-pos is used by mult-def-02, add-def-02,
• int-basic1/irref is used by irreflexivity,
• int-basic1/ls-01 is used by root-is-irrational, one, num-neg-01, num-neg, num-div-denom-01, num-div-denom, negate-01, mult-def-03, mult-def-02, make, ls-def, factor-rat-03, factor-rat-02, factor-rat-01, equality-pos, equality-02, div-pos-def, div-def-01, add-eq, add-def-03, add-def-02, abs-pos, Extsimple,
• int-basic1/lst-01 is used by one, mult-def-03, div-def-01, add-def-03, Extsimple,

Used from specification int-gcd

• int-gcd/abs-gcd-not-less is used by denom-not-zero,
• int-gcd/div-eq is used by equal-same,
• int-gcd/div-mult-shift is used by div-pos-def,
• int-gcd/divides-mult-02 is used by div-pos-def,
• int-gcd/gcd-abs is used by abs-pos,
• int-gcd/gcd-abs-rew-01 is used by abs-pos,
• int-gcd/gcd-abs-rew-02 is used by denum-same, abs-pos, abs-num,
• int-gcd/gcd-com is used by equality-01,
• int-gcd/gcd-div-eq is used by equality-pos, equality-01, equal-same,
• int-gcd/gcd-div-mult-shift is used by equality-pos, equality-01, equal-same, div-pos-def,
• int-gcd/gcd-mult-pos is used by equality-pos,
• int-gcd/gcd-mult-pos-01 is used by equality-pos,
• int-gcd/gcd-one is used by mult-def-02, add-def-02,
• int-gcd/gcd-one-01 is used by zero-denom,
• int-gcd/gcd-pos is used by make, denom-not-zero,
• int-gcd/gcd-same is used by one,
• int-gcd/square-neq-any is used by root-is-irrational,
• int-gcd/abs-not-less is used by denom-pos-01,
• int-gcd/div-gcd-is-neg is used by make,
• int-gcd/div-gcd-is-neg-01 is used by make,
• int-gcd/div-gcd-is-neg-01-01 is used by num-neg-02, make, Extsimple,
• int-gcd/div-gcd-neg-not-zero is used by num-div-denom-01, num-div-denom, make,
• int-gcd/div-gcd-not-neg is used by make, div-pos-def, canon-pos, canon-any, abs-pos, Extsimple,
• int-gcd/div-gcd-zero is used by num-zero-denum-one, num-zero, make, gcd-num-one, equality-01, equal-same, canon-pos, canon-any, abs-pos,
• int-gcd/divides is used by mult-def-02, equal-same, add-def-02,
• int-gcd/gcd-abs is used by make, denom-not-zero, canon-pos, canon-any, abs-pos,
• int-gcd/gcd-com is used by one, num-pos, num-neg-02, num-neg, num-id, num-div-denom-01, num-div-denom, neg-neg, make, gcd-num-one, equality-pos, equality-01, equal-same, div-pos-def, denom-not-zero, denom-neg, denom-id, canon-pos, canon-any, abs-pos, Extsimple,
• int-gcd/gcd-div-gcd is used by make, gcd-num-one, canon-pos, canon-any,
• int-gcd/gcd-div-gcd-pos is used by abs-pos,
• int-gcd/gcd-div-mult is used by num-div-denom-01, num-div-denom,
• int-gcd/gcd-div1 is used by div-pos-def,
• int-gcd/gcd-divides is used by equal-same, div-pos-def,
• int-gcd/gcd-less-eq-zero is used by num-neg-02, equality-01, div-pos-def, denom-pos-01, denom-pos, Extsimple,
• int-gcd/gcd-mult is used by factor-rat-03, equality-pos,
• int-gcd/gcd-neg is used by one, num-neg-03, num-neg-01, num-neg, neg-neg, make, gcd-num-one, denom-neg-01, denom-neg,
• int-gcd/gcd-one-01 is used by zero-denom, num-neg-01, make, int-mult, int-add, gcd-num-one, exrat-gcd1, denom-one,
• int-gcd/gcd-zero is used by one,
• int-gcd/gcd-zero-02 is used by num-neg-02,
• int-gcd/gcd-zero-04 is used by root-is-irrational, num-pos, num-id, gcd-num-one, div-pos-def, denom-id, canon-pos, add-def-02,
• int-gcd/gcd-zero-zero is used by one, num-zero-denum-one, num-zero, num-neg-02, num-neg-01, num-neg, num-div-denom-01, num-div-denom, make, gcd-num-one, factor-rat-03, equality-pos, equality-01, equal-same, div-pos-def, denom-pos-01, denom-pos, denom-not-zero, denom-neg, canon-pos, canon-any, abs-pos, Extsimple,
• int-gcd/mod-gcd is used by num-div-denom-01, num-div-denom,
• int-gcd/not-less-gcd is used by make,

Used from specification int-abs

• int-abs/Abs-pos is used by abs-pos,
• int-abs/abs-01 is used by denom-not-zero, abs-pos, abs-num,
• int-abs/abs-08 is used by div-def-01,
• int-abs/lep is used by ls-def,
• int-abs/neg-02 is used by negate-01,
• int-abs/Abs-pos is used by div-def-01, Extsimple,
• int-abs/abs is used by mult-def-02, add-def-02,
• int-abs/abs-01 is used by denum-same, denom-not-zero,
• int-abs/abs-06 is used by div-def-01, abs-pos,
• int-abs/abs-07 is used by div-def-01, denum-same, denom-not-zero, abs-pos, abs-num,
• int-abs/abs-08 is used by one, num-zero-denum-one, num-zero, num-neg-01, num-neg, num-div-denom-01, num-div-denom, negate-01, mult-def-03, make, gcd-num-one, factor-rat-02, denom-neg, add-def-03, abs-pos, Extsimple,
• int-abs/abs-16 is used by root-is-irrational, one, num-pos, num-neg-01, num-neg, num-id, num-div-denom-01, num-div-denom, make, gcd-num-one, factor-rat-03, factor-rat-02, equality-pos, equality-01, equal-same, div-pos-def, denom-id, canon-pos, canon-any, abs-pos, Extsimple,
• int-abs/abs-18 is used by denum-same,
• int-abs/abs-neg is used by num-neg-01, num-neg, neg-neg, make, denom-neg,
• int-abs/absls is used by denom-pos,
• int-abs/anti is used by totality, num-zero-denum-one, num-zero, make, gcd-num-one, equality-02,
• int-abs/elim-sub is used by ls-def,
• int-abs/forward-le-01 is used by ls-def, equality-02, canon-pos, Extsimple,
• int-abs/forward-le-02 is used by one, num-neg-02, num-neg-01, num-neg, num-div-denom-01, num-div-denom, negate-01, mult-def-03, make, ls-def, gcd-num-one, factor-rat-02, factor-rat-01, equality-02, div-def-01, denom-pos, denom-neg, canon-any, add-def-03, Extsimple,
• int-abs/forward-le-04 is used by num-zero-denum-one, num-zero, num-neg-02, negate-01, make, gcd-num-one, equality-02, div-pos-def, denom-pos-01, denom-pos,
• int-abs/forward-le-05 is used by transitivity, totality, sub-def-01, root-is-irrational, num-pos, num-neg-03, num-neg-02, num-neg-01, num-neg, num-id, num-div-denom-01, num-div-denom, negate, mult-one, mult-def-03, mult-def-02, mult-ass, make, ls-def, gcd-num-one, factor-rat-03, factor-rat-02, exrat-01, equality-pos, equality-def, equality-02, equality-01, equal-same, elim-sub, div-pos-def, div-neg-01, div-def-01, distributivity, denom-pos, denom-not-zero, denom-neg-02, denom-id, canon-pos, canon-any, add-eq, add-def-03, add-def-02, add-asso, abs-pos, abs-num, Extsimple,
• int-abs/forward-lels is used by num-neg-02, make, equality-02, div-pos-def, denom-pos,
• int-abs/forward-lsle is used by equality-02, Extsimple,
• int-abs/gr-def is used by mult-def-02, add-def-02,
• int-abs/lels is used by transitivity, totality, root-is-irrational, one, num-zero-denum-one, num-zero, num-pos, num-neg-03, num-neg-02, num-neg-01, num-neg, num-id, num-div-denom-01, num-div-denom, negate-01, mult-def-03, mult-def-02, make, ls-def, gcd-num-one, factor-rat-03, factor-rat-02, factor-rat-01, exrat-gcd1, exrat-01, exrat, equality-pos, equality-02, equality-01, elim-sub, div-pos-def, div-def-01, denom-pos-01, denom-pos, denom-not-zero, denom-neg-02, canon-pos, canon-any, add-eq, add-def-03, add-def-02, abs-pos, abs-num, Extsimple,
• int-abs/lels-01 is used by num-neg-02, ls-def, equality-pos, div-pos-def, denum-same, canon-any, Extsimple,
• int-abs/lels-02 is used by root-is-irrational, num-zero-denum-one, num-zero, num-neg-02, num-neg-01, num-neg, num-div-denom-01, num-div-denom, negate-01, mult-def-03, mult-def-02, make, ls-def, gcd-num-one, factor-rat-03, factor-rat-02, factor-rat-01, equality-pos, equality-02, div-pos-def, denom-not-zero, canon-pos, add-eq, add-def-03, add-def-02, abs-pos, Extsimple,
• int-abs/lels-03 is used by transitivity, totality, one, num-pos, num-neg-03, num-neg-02, num-id, mult-def-03, mult-def-02, ls-def, factor-rat-02, exrat-01, equality-02, elim-sub, div-def-01, denom-not-zero, denom-neg-02, canon-any, add-eq, add-def-03, add-def-02,
• int-abs/lels-04 is used by transitivity, ls-def, equality-02,
• int-abs/ler is used by totality,
• int-abs/neg is used by one, num-neg-01, num-neg, negate-01, mult-def-03, make, factor-rat-02, factor-rat-01, equality-02, add-def-03,
• int-abs/neg-02 is used by num-neg-01, num-neg, neg-intro, mult-def-03, factor-rat-01, add-def-03,
• int-abs/neg-03 is used by num-neg-03, num-neg-01, num-neg, num-div-denom, negate, make, elim-sub, denom-neg, Extsimple,
• int-abs/neg-05 is used by num-neg-01, num-neg, make,
• int-abs/neg-06 is used by negate,
• int-abs/neg-10 is used by num-zero-denum-one, num-zero, num-neg-01, num-neg, neg-neg, make, gcd-num-one, factor-rat-01, denom-neg-01, denom-neg, abs-pos,
• int-abs/neg-11 is used by add-def-03,
• int-abs/neg-12 is used by equality-02, Extsimple,
• int-abs/neg-15 is used by sub-def-01, num-neg-01, num-div-denom-01, num-div-denom, ls-def, Extsimple,
• int-abs/negeq is used by num-neg-03, num-neg-01, num-neg, num-div-denom-01, num-div-denom, negate, make, denom-neg, Extsimple,
• int-abs/sub-eq is used by num-neg-01, num-div-denom-01, num-div-denom, Extsimple,
• int-abs/sub-eq-01 is used by Extsimple,
• int-abs/sub-zero-01 is used by num-neg-03,
• int-abs/zero-gels-01 is used by one, mult-def-03, factor-rat-02, equality-02, add-def-03, Extsimple,
• int-abs/zero-gels-03 is used by gcd-num-one, equality-02,

Used from specification nat-basic2

• nat-basic2/a is used by mult-def-02, add-def-02,
• nat-basic2/c is used by mult-def-02, add-def-02,
• nat-basic2/l is used by mult-def-02, add-def-02,

Used from specification intnat

• intnat/rlabs is used by denom-not-zero,
• intnat/labs is used by mult-def-02, denom-not-zero, add-def-02,

Used from specification int-basic2

• int-basic2/add-in is used by add-eq,
• int-basic2/not-zero-pos is used by Extsimple,
• int-basic2/zero is used by Extsimple,
• int-basic2/add-a is used by sub-def-01, rational-add-same, num-neg-03, num-neg-02, num-neg-01, num-neg, num-div-denom-01, num-div-denom, negate, make, ls-def, int-add, elim-sub, distributivity, denom-pos, denom-neg, add-zero, add-def-03, add-def-02, add-asso, Extsimple,
• int-basic2/add-c is used by sub-def-01, rational-add-same, num-neg-03, num-neg-02, num-neg-01, num-neg, num-div-denom-01, num-div-denom, negate, mult-split, make, ls-def, int-add, elim-sub, distributivity, denom-pos, denom-neg, add-zero, add-eq, add-def-03, add-def-02, add-def-01, add-comm, add-asso, Extsimple,
• int-basic2/add-zero is used by num-neg-03, num-neg-01, num-div-denom-01, num-div-denom, int-add, add-zero, add-def-03, add-def-02, Extsimple,
• int-basic2/ls is used by num-neg-02, ls-def, denom-pos,

Used from specification int-div

• int-div/abs is used by abs-pos,
• int-div/div-div-pos is used by div-pos-def,
• int-div/div-div-switch is used by num-div-denom-01, num-div-denom,
• int-div/div-lezero is used by denom-pos-01,
• int-div/div-ls-zero is used by num-neg-02, denom-pos,
• int-div/div-mult is used by equality-pos,
• int-div/div-zero-02 is used by denom-not-zero,
• int-div/num-ls is used by Extsimple,
• int-div/abs is used by make, canon-pos, canon-any, abs-pos,
• int-div/div-eq-zero-01 is used by denom-not-zero,
• int-div/div-lezero is used by make,
• int-div/div-mult-01 is used by factor-rat-03,
• int-div/div-mult-03 is used by equality-pos, equal-same,
• int-div/div-same is used by one, gcd-num-one, canon-pos,
• int-div/neg is used by one, num-div-denom-01, num-div-denom,
• int-div/neg-01 is used by one, num-zero-denum-one, num-zero, num-neg-01, num-neg, num-div-denom-01, num-div-denom, make, gcd-num-one, denom-neg, abs-pos, Extsimple,
• int-div/one is used by zero-denom, num-neg-01, num-id, make, int-mult, int-add, denum-same, denom-id, canon-pos, canon-any, abs-pos, abs-num,
• int-div/zero is used by num-div-denom-01, num-div-denom, canon-pos,