Used simplifier rules/spec theorems by specification

Used from specification nat-basic

• nat-basic/a is used by gcdexh,
• nat-basic/c is used by gcdexh,
• nat-basic/a is used by twodiv-02, twodiv-01, succ, prime-smallest, mult-01, modprime, gcdnex-prime, gcdnex, gcdexh, gcdex-dist, gcd-zero-01-h, gcd-rec2, gcd-one, gcd-mult, gcd-mod-one, gcd-mod, gcd-le-both-h, gcd-div-both-h, gcd-conq-one, gcd-alldiv-h, gcd-add, divi-two-03, divi-two-01, divi-succ, divi-sub, divi-same, divi-primmult, divi-mod, divi-dist, divi-add-01, divi-add, div-multadd, dist-snd-01, dist-mult-01, dist-mult, dist-c, dist-add-01, dist-add, cong-equiv,
• nat-basic/add-base is used by modprime, cong-equiv,
• nat-basic/c is used by twodiv-02, twodiv-01, succ, prime-smallest, mult-01, modprime, gcdnex-prime, gcdnex, gcdexh, gcdex-dist, gcd-zero-01-h, gcd-rec2, gcd-one, gcd-mult, gcd-mod-one, gcd-mod, gcd-le-both-h, gcd-div-both-h, gcd-conq-one, gcd-alldiv-h, gcd-add, divi-two-03, divi-two-01, divi-succ, divi-sub, divi-same, divi-primmult, divi-mod, divi-dist, divi-add-01, divi-add, div-multadd, dist-snd-01, dist-mult-01, dist-mult, dist-c, dist-add-01, dist-add, cong-equiv,
• nat-basic/eq-01 is used by gcd-mult, gcd-conq-one, divi-two-01, divi-sub, divi-same, cong-equiv,
• nat-basic/eq-02 is used by divi-add,
• nat-basic/eqs is used by gcdex-dist,
• nat-basic/f is used by prime-smallest, not-prime, mult-01, modprime, mod-zero, lstwo, gcdexh, gcdex-dist, gcdex, gcd-zero-01-h, gcd-zero-01, gcd-mult, gcd-mod-one, gcd-mod, gcd-max, gcd-le-both-h, gcd-le-both, gcd-le, gcd-eq, gcd-div-both-h, gcd-conq-one, gcd-alldiv-h, divi-sub, divi-same, divi-mod, divi-ls, divi-dist, dist-mult, dist-eq, dist-add-01, cong-equiv,
• nat-basic/l is used by gcd-mult, divi-same, dist-add-01,
• nat-basic/l-01 is used by gcd-zero-01-h, gcd-mult, gcd-le-both-h, gcd-div-both-h, gcd-alldiv-h, divi-same, divi-dist, dist-c, cong-equiv,
• nat-basic/l-02 is used by mult-01, gcdex-dist, gcd-rec2, gcd-one, gcd-mod, gcd-le-both-h, gcd-add, dist-c, cong-equiv,
• nat-basic/less-1 is used by cong-equiv,
• nat-basic/lf is used by not-prime,
• nat-basic/lf-01 is used by mult-01, gcd-eq,
• nat-basic/lf-02 is used by prime-smallest, gcdex-dist, gcd-mod-one,
• nat-basic/ls-02 is used by prime-smallest, not-prime, gcdex, gcd-zero-01-h, gcd-mult, gcd-le-both-h, gcd-div-both-h, gcd-alldiv-h, divi-same, dist-mult, dist-c, dist-add-01, cong-equiv,
• nat-basic/ls-03 is used by gcd-div-both, gcd-alldiv, divi-add,
• nat-basic/lstwo is used by prime-prime,
• nat-basic/neq-01 is used by not-prime, gcd-zero-01,
• nat-basic/one is used by twodiv-02, twodiv-01, succ, prime-smallest, prime-prime, not-prime, mult-02, mult-01, mult, modprime, mod-zero, lstwo, leone, gcdnex-prime, gcdnex, gcd-mod-one-01, gcd-mod-one, gcd-conq-one, divi-primmult, div,
• nat-basic/one-01 is used by gcd-mod-one, gcd-conq-one,
• nat-basic/one-03 is used by gcdnex-prime, gcdnex, divi-primmult,
• nat-basic/one-05 is used by gcdnex,
• nat-basic/one-06 is used by twodiv-01,
• nat-basic/oz is used by twodiv-01, gcd-conq-one,
• nat-basic/ref is used by gcd-le-both-h, gcd-le, gcd-id, gcd-eq, dist-same, dist-add-01,
• nat-basic/succ is used by gcd-one, gcd-mod, divi-two-03,
• nat-basic/trans is used by not-prime,
• nat-basic/twols-01 is used by prime-smallest, not-prime, modprime, lstwo, gcd-two,
• nat-basic/twols-02 is used by prime-smallest, prime-prime,
• nat-basic/z is used by prime-smallest,
• nat-basic/z-01 is used by gcd-mod-one, divi-two-01, divi-add,
• nat-basic/z-02 is used by prime-smallest, gcdexh, gcd-mod-one, gcd-mod, divi-sub, divi-same, divi-mod, divi-add, dist-add, cong-equiv,
• nat-basic/zero is used by modprime, divi-ls, cong-equiv,
• nat-basic/zero-01 is used by cong-equiv,

Used from specification nat

• nat/sub-succ is used by gcd-mod-one,
• nat/add-01 is used by gcd-mod-one,
• nat/add-num-04 is used by twodiv-01,
• nat/anti is used by prime-smallest, gcd-zero-01-h, gcd-le-both-h, gcd-div-both-h, gcd-alldiv-h,
• nat/cancel-01 is used by dist-add-01,
• nat/elim-pred-c is used by gcd-conq-one, divi-two-01,
• nat/elim-sub is used by gcdex-dist, gcd-zero-01-h, gcd-rec2, gcd-mult, gcd-le-both-h, gcd-div-both-h, gcd-alldiv-h, divi-sub, divi-same, divi-dist, dist-snd-01, dist-mult, dist-c, dist-add-01, cong-equiv,
• nat/eq-01 is used by gcd-rec2, gcd-one, gcd-mod, gcd-add, dist-c, dist-add, cong-equiv,
• nat/eq-02 is used by gcdexh, gcd-mod-one,
• nat/fle is used by not-prime, gcd-le-both-h, gcd-le, gcd-eq, dist-add-01,
• nat/fle-01 is used by not-prime, modprime, mod-zero, gcd-le-both-h, gcd-le, gcd-eq, dist-add-01,
• nat/le-add is used by gcd-zero-01-h, gcd-div-both-h,
• nat/le-def is used by prime-smallest, prime-prime, not-prime, modprime, gcdexh, gcdex-dist, gcdex, gcd-zero-01-h, gcd-rec2, gcd-one, gcd-mult, gcd-mod-one, gcd-mod, gcd-max, gcd-le-both-h, gcd-le, gcd-id, gcd-eq, gcd-div-both-h, gcd-conq-one, gcd-alldiv-h, gcd-add, divi-same, divi-dist, dist-same, dist-mult, dist-eq, dist-c, dist-add-01, cong-equiv,
• nat/le-ls-simp is used by gcd-mult,
• nat/lels is used by gcd-zero-01-h, gcd-mult, gcd-mod-one, gcd-le-both-h, gcd-le-both, gcd-div-both-h, gcd-div-both, gcd-alldiv-h, gcd-alldiv, divi-sub, divi-add, dist-c, dist-add-01, dist-add,
• nat/lels-02 is used by two-01, prime-smallest, gcdexh, gcd-two, gcd-le-both,
• nat/lels-03 is used by gcd-zero-01-h, gcd-mult, gcd-le-both-h, gcd-div-both-h, gcd-alldiv-h, divi-same, divi-dist, dist-c, cong-equiv,
• nat/lep is used by gcd-rec2, gcd-mult, gcd-mod, gcd-add, divi-sub, divi-same, cong-equiv,
• nat/lep-01 is used by gcd-le-both-h, gcd-alldiv-h, dist-add,
• nat/lep-02 is used by divi-same, dist-add-01,
• nat/ler is used by gcdexh, gcd-le-both-h, gcd-le-both, gcd-div-both-h, gcd-div-both, gcd-alldiv-h, gcd-alldiv,
• nat/let is used by prime-smallest, prime-prime, gcdnex-prime, gcd-le-both-h,
• nat/lez is used by prime-smallest, prime-prime, gcdexh, dist-zero,
• nat/not-zero is used by prime-prime, not-prime, modprime, mod-zero, gcdnex-prime, gcd-conq-one,
• nat/one-02 is used by leone,
• nat/sub-base is used by dist-zero,
• nat/zero is used by gcd-id, divi-add, dist-same,
• nat/zero-01 is used by dist-eq,
• nat/zero-02 is used by dist-eq,

Used from specification nat-mult

• nat-mult/dist is used by gcdexh, divi-sub, divi-same, dist-mult-01,
• nat-mult/dist-sub is used by gcdexh, gcd-mod-one, cong-equiv,
• nat-mult/modeq is used by gcd-mod-one,
• nat-mult/mult-a is used by gcd-div-one,
• nat-mult/mult-c is used by gcd-div-one-02, gcd-div-one,
• nat-mult/numeral-07 is used by divi-add,
• nat-mult/numeral-08 is used by divi-add,
• nat-mult/addle is used by gcd-mult,
• nat-mult/addle-01 is used by gcd-mult, divi-sub, divi-same,
• nat-mult/coef-04 is used by gcdexh, divi-add, div-multadd,
• nat-mult/coef-17 is used by gcdexh, divi-two-01,
• nat-mult/dist is used by gcd-mult, divi-two-01,
• nat-mult/dist-sub-03 is used by gcd-mult,
• nat-mult/dist-sub-04 is used by gcd-mult,
• nat-mult/eq is used by gcd-mult, gcd-mod-one, divi-add,
• nat-mult/le is used by prime-smallest, prime-prime, not-prime, gcdnex-prime, gcd-mult,
• nat-mult/le-02 is used by gcd-mod-one,
• nat-mult/ls is used by not-prime, gcdexh, gcd-mult, gcd-mod-one, divi-sub, divi-same, cong-equiv,
• nat-mult/ls-01 is used by not-prime, gcd-mod-one, gcd-le-both-h, divi-ls,
• nat-mult/ls-04 is used by modprime, mod-zero,
• nat-mult/ls-05 is used by not-prime,
• nat-mult/ls-08 is used by gcd-mod-one,
• nat-mult/modeq-01 is used by divi-mod,
• nat-mult/mult-a is used by twodiv, prime-smallest, prime-prime, not-prime, mult-02, mult-01, mult, modprime, mod2, mod-zero, gcdnex-prime, gcdexh, gcdex-dist, gcd-multdiv, gcd-mult, gcd-mod-one, gcd-mod, gcd-le-both-h, gcd-div-one, gcd-conq-one, divi-zero-01, divi-zero, divi-two-02, divi-two-01, divi-two, divi-trans, divi-three, divi-sym, divi-succ, divi-sub, divi-same, divi-ref, divi-primmult, divi-one-01, divi-one, divi-mult-01, divi-mod, divi-ls, divi-eq, divi-add-01, divi-add, div-multadd, dist-mult-01, dist-mult, cong-equiv,
• nat-mult/mult-base is used by gcdexh, gcd-mult, gcd-mod, divi-zero-01, divi-zero, divi-sub, divi-same, divi-add, cong-equiv,
• nat-mult/mult-c is used by twodiv, prime-smallest, prime-prime, not-prime, mult-02, mult-01, mult, modprime, mod2, mod-zero, gcdnex-prime, gcdexh, gcdex-dist, gcd-multdiv, gcd-mult, gcd-mod-one, gcd-mod, gcd-le-both-h, gcd-div-one, gcd-conq-one, divi-zero-01, divi-zero, divi-two-02, divi-two-01, divi-two, divi-trans, divi-three, divi-sym, divi-succ, divi-sub, divi-same, divi-ref, divi-primmult, divi-one-01, divi-one, divi-mult-01, divi-mod, divi-ls, divi-eq, divi-add-01, divi-add, div-multadd, dist-mult-01, dist-mult, cong-equiv,
• nat-mult/one is used by mult-02, mod-zero, gcdnex-prime, gcd-conq-one, divi-sym, divi-succ, divi-one-01, divi-one,
• nat-mult/one-01 is used by prime-smallest, prime-prime, mult-01, modprime, divi-two, divi-sym, divi-one, divi-eq,
• nat-mult/one-02 is used by mult,
• nat-mult/rsucc-02 is used by gcd-mod-one, gcd-mod,
• nat-mult/square-less is used by not-prime,
• nat-mult/sqzero is used by not-prime,
• nat-mult/succ-01 is used by divi-succ,
• nat-mult/three is used by divi-three,
• nat-mult/two-02 is used by gcd-mult, gcd-le-both-h,
• nat-mult/two-03 is used by mod-zero, divi-two-02,
• nat-mult/twoeq is used by twodiv, mod2,
• nat-mult/twole is used by gcd-mult,
• nat-mult/zero-01 is used by prime-smallest, prime-prime, not-prime, mult-01, mult, modprime, mod-zero, gcdnex-prime, gcdex-dist, gcd-conq-one, divi-same, divi-ls, divi-add,
• nat-mult/zero-02 is used by gcd-multdiv, dist-mult-01, dist-mult,
• nat-mult/zero-03 is used by not-prime, mult-01, modprime, gcdexh, gcd-div-one, divi-three, divi-sym, divi-ref, divi-eq,
• nat-mult/zero-06 is used by divi-ls,

Used from specification nat-div

• nat-div/mod-rew is used by gcdexh,
• nat-div/modex is used by prime-prime, mod2, mod-zero, gcdnex-prime,
• nat-div/cond is used by gcdexh,
• nat-div/cond-01 is used by gcdexh,
• nat-div/div-elim is used by prime-smallest, modprime, gcd-mod-one, gcd-mod, gcd-conq-one, divi-mod, cong-equiv,
• nat-div/mod-eq-01 is used by cong-equiv,
• nat-div/mod-le-02 is used by gcdexh,
• nat-div/mod-mult is used by gcd-mod-one, cong-equiv,
• nat-div/mod-mult-01 is used by prime-smallest, modprime,
• nat-div/mod-one is used by prime-prime,
• nat-div/mod-one-01 is used by gcd-mod-one,
• nat-div/mod-zero is used by gcdexh,