[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 nat-basic

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

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 gcd-le-both-h, prime-smallest, gcd-div-both-h, gcd-zero-01-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 gcd-le-both-h, gcd-mult, divi-sub, divi-dist, cong-equiv, dist-c, gcd-div-both-h, dist-add-01, dist-snd-01, dist-mult, gcd-zero-01-h, gcd-alldiv-h, gcdex-dist, gcd-rec2, divi-same,
nat/eq-01 is used by gcd-mod, dist-add, cong-equiv, dist-c, gcd-one, gcd-rec2, gcd-add,
nat/eq-02 is used by gcdexh, gcd-mod-one,
nat/fle is used by gcd-le-both-h, gcd-le, dist-add-01, gcd-eq, not-prime,
nat/fle-01 is used by gcd-le-both-h, modprime, gcd-le, dist-add-01, mod-zero, gcd-eq, not-prime,
nat/le-add is used by gcd-le-both-h, dist-add, gcd-div-both-h, gcd-zero-01-h, gcd-alldiv-h,
nat/le-def is used by gcd-le-both-h, gcd-mult, dist-eq, gcd-mod, prime-smallest, divi-dist, modprime, gcdex, cong-equiv, dist-c, gcd-le, gcd-conq-one, gcd-div-both-h, dist-add-01, dist-mult, gcd-zero-01-h, gcd-max, prime-prime, gcdexh, gcd-mod-one, gcd-alldiv-h, gcd-one, gcdex-dist, gcd-rec2, gcd-eq, dist-same, divi-same, gcd-id, gcd-add, not-prime,
nat/le-ls-simp is used by gcd-mult,
nat/lels is used by gcd-le-both-h, gcd-mult, gcd-alldiv, divi-sub, dist-add, gcd-div-both, dist-c, gcd-div-both-h, dist-add-01, divi-add, gcd-zero-01-h, gcd-mod-one, gcd-alldiv-h, gcd-le-both,
nat/lels-02 is used by prime-smallest, gcdexh, gcd-le-both, two-01, gcd-two,
nat/lels-03 is used by gcd-le-both-h, gcd-mult, prime-smallest, divi-dist, cong-equiv, dist-c, gcd-div-both-h, gcd-zero-01-h, gcd-alldiv-h, divi-same, not-prime,
nat/lep is used by gcd-mult, gcd-mod, divi-sub, cong-equiv, gcd-rec2, divi-same, gcd-add,
nat/lep-02 is used by dist-add-01, divi-same,
nat/ler is used by gcd-le-both-h, gcd-alldiv, gcd-div-both, gcd-div-both-h, gcdexh, gcd-alldiv-h, gcd-le-both,
nat/let is used by gcd-le-both-h, prime-smallest, prime-prime, gcdnex-prime,
nat/lez is used by dist-zero, prime-smallest, prime-prime, gcdexh,
nat/not-zero is used by prime-smallest, modprime, gcd-conq-one, prime-prime, gcdnex-prime, mod-zero, not-prime,
nat/one-02 is used by leone,
nat/sub-base is used by dist-zero,
nat/zero is used by divi-add, dist-same, gcd-id,
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 divi-sub, dist-mult-01, gcdexh, divi-same,
nat-mult/dist-sub is used by cong-equiv, gcdexh, gcd-mod-one,
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, gcd-div-one-02,
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 divi-add, gcdexh, 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, divi-add, gcd-mod-one,
nat-mult/le is used by gcd-mult, prime-smallest, prime-prime, gcdnex-prime, not-prime,
nat-mult/le-02 is used by gcd-mod-one,
nat-mult/le-05 is used by not-prime,
nat-mult/ls is used by gcd-mult, divi-sub, cong-equiv, gcdexh, gcd-mod-one, divi-same,
nat-mult/ls-01 is used by gcd-le-both-h, gcd-mod-one, divi-ls,
nat-mult/ls-02 is used by not-prime,
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, not-prime,
nat-mult/modeq-01 is used by divi-mod,
nat-mult/mult-a is used by mult-02, gcd-le-both-h, gcd-mult, divi-zero, gcd-mod, prime-smallest, divi-sub, divi-one, modprime, dist-mult-01, divi-one-01, divi-trans, cong-equiv, divi-zero-01, divi-ref, divi-sym, gcd-div-one, gcd-conq-one, mod2, divi-two-02, mult, divi-succ, divi-add, dist-mult, twodiv, divi-mult-01, divi-mod, divi-two, prime-prime, gcdnex-prime, gcd-multdiv, gcdexh, gcd-mod-one, mult-01, mod-zero, gcdex-dist, divi-primmult, div-multadd, divi-eq, divi-add-01, divi-ls, divi-same, divi-two-01, divi-three, not-prime,
nat-mult/mult-base is used by gcd-mult, gcd-mod, divi-sub, divi-zero-01, divi-add, gcdexh, divi-same,
nat-mult/mult-c is used by mult-02, gcd-le-both-h, gcd-mult, divi-zero, gcd-mod, prime-smallest, divi-sub, divi-one, modprime, dist-mult-01, divi-one-01, divi-trans, cong-equiv, divi-zero-01, divi-ref, divi-sym, gcd-div-one, gcd-conq-one, mod2, divi-two-02, mult, divi-succ, divi-add, dist-mult, twodiv, divi-mult-01, divi-mod, divi-two, prime-prime, gcdnex-prime, gcd-multdiv, gcdexh, gcd-mod-one, mult-01, mod-zero, gcdex-dist, divi-primmult, div-multadd, divi-eq, divi-add-01, divi-ls, divi-same, divi-two-01, divi-three, not-prime,
nat-mult/one is used by mult-02, divi-one, modprime, divi-one-01, divi-sym, gcd-conq-one, divi-succ, gcdnex-prime, mod-zero,
nat-mult/one-01 is used by prime-smallest, divi-one, modprime, divi-sym, divi-two, prime-prime, mult-01, divi-eq,
nat-mult/one-02 is used by mult,
nat-mult/rsucc-02 is used by gcd-mod, gcd-mod-one,
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-le-both-h, gcd-mult,
nat-mult/two-03 is used by divi-two-02, mod-zero,
nat-mult/twoeq is used by mod2, twodiv,
nat-mult/twole is used by gcd-mult,
nat-mult/zero is used by divi-zero, cong-equiv,
nat-mult/zero-01 is used by gcd-conq-one, mult, divi-add, prime-prime, gcdnex-prime, mult-01, mod-zero, gcdex-dist, divi-ls, divi-same,
nat-mult/zero-02 is used by dist-mult-01, dist-mult, gcd-multdiv,
nat-mult/zero-03 is used by modprime, divi-ref, divi-sym, gcd-div-one, gcdexh, mult-01, divi-eq, not-prime,
nat-mult/zero-06 is used by prime-smallest, modprime, divi-ls, not-prime,

Used from specification nat-div

nat-div/mod-rew is used by gcdexh,
nat-div/modex is used by mod2, prime-prime, gcdnex-prime, mod-zero,
nat-div/cond is used by gcdexh,
nat-div/cond-01 is used by gcdexh,
nat-div/div-elim is used by gcd-mod, prime-smallest, modprime, cong-equiv, gcd-conq-one, divi-mod, gcd-mod-one,
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 cong-equiv, gcd-mod-one,
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,