[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

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-twicerev, gcd-twice, 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-mod, gcd-add, dist-c, dist-add, cong-equiv,
nat/eq-02 is used by gcdexh,
nat/fle is used by not-prime, gcd-eq,
nat/fle-01 is used by not-prime, modprime, mod-zero, gcd-le-both-h, gcd-eq,
nat/le-add is used by gcd-zero-01-h, gcd-le-both-h, gcd-div-both-h, gcd-alldiv-h, dist-add,
nat/le-ls-simp is used by gcd-mult, gcd-le-both-h,
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-01 is used by prime-smallest, prime-prime, not-prime, modprime, gcdexh, gcdex-dist, gcdex, gcd-twicerev, gcd-twice, gcd-rec2, gcd-mult, gcd-mod-one, gcd-mod, gcd-max, gcd-le, gcd-id, gcd-eq, gcd-conq-one, gcd-add, divi-same, divi-dist, dist-same, dist-mult, dist-c, dist-add-01, cong-equiv,
nat/lels-02 is used by two-01, prime-smallest, gcdnex-prime, gcdexh, gcd-two, gcd-le-both, dist-eq,
nat/lels-03 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, divi-dist, dist-mult, dist-c, dist-add-01, cong-equiv,
nat/lep is used by gcd-rec2, gcd-mult, gcd-mod, divi-sub, divi-same, cong-equiv,
nat/lep-02 is used by divi-same, dist-add-01,
nat/ler is used by gcdexh, 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,
nat/lez is used by gcdexh, dist-zero,
nat/ls-le-simp is used by gcd-le, dist-add-01,
nat/not-zero is used by prime-smallest, prime-prime, not-prime, mult-03, 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-basic2

nat-basic2/a is used by gcdexh,
nat-basic2/c is used by gcdexh,
nat-basic2/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-twicerev, gcd-twice, 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-addrev, 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-basic2/add-base is used by prime-smallest, modprime, divi-sub, divi-same, divi-mod, divi-add, dist-add,
nat-basic2/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-twicerev, gcd-twice, 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-addrev, 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-basic2/eq is used by divi-add,
nat-basic2/eq-01 is used by gcd-mult, gcd-conq-one, divi-two-01, divi-sub, divi-same, cong-equiv,
nat-basic2/eqs is used by gcdex-dist,
nat-basic2/l is used by gcd-mult, divi-same, dist-add-01,
nat-basic2/l-01 is used by gcd-zero-01-h, gcd-mult, gcd-le-both-h, gcd-div-both-h, gcd-alldiv-h, divi-same, dist-c, cong-equiv,
nat-basic2/l-02 is used by gcdex-dist, gcd-rec2, gcd-mod, gcd-add, dist-c, cong-equiv,
nat-basic2/l-05 is used by mult-01,
nat-basic2/nls-fst is used by gcd-le-both-h,
nat-basic2/one is used by gcdnex-prime, gcdnex, divi-primmult,
nat-basic2/one-02 is used by gcdnex,
nat-basic2/one-03 is used by twodiv-01,
nat-basic2/oz is used by twodiv-01,
nat-basic2/succ is used by gcd-one, gcd-mod, divi-two-03,
nat-basic2/z is used by gcdexh, gcd-mod-one, gcd-mod, cong-equiv,
nat-basic2/z-01 is used by gcd-zero-01-h, gcd-mod-one, gcd-div-both-h, gcd-conq-one, gcd-alldiv-h, divi-two-01, divi-add,

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,
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/eq-same is used by not-prime, mult-01, modprime, gcdexh, gcd-div-one, divi-three, divi-sym, divi-ref, divi-eq,
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/le-05 is used by not-prime,
nat-mult/ls is used by gcdexh, gcd-mult, divi-sub, divi-same, cong-equiv,
nat-mult/ls-01 is used by 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,
nat-mult/ls-10 is used by not-prime,
nat-mult/mult-a is used by twodiv, prime-smallest, prime-prime, not-prime, mult-03, mult-02, mult-01, mult, modprime, mod2, mod-zero, gcdnex-prime, gcdexh, gcdex-dist, gcd-twicerev, gcd-twice, gcd-multdiv, gcd-mult, gcd-mod-one, gcd-mod, gcd-le-both-h, gcd-div-one, gcd-div-both-h, gcd-conq-one, gcd-alldiv-h, 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-one, gcd-mod, cong-equiv,
nat-mult/mult-c is used by twodiv, prime-smallest, prime-prime, not-prime, mult-03, mult-02, mult-01, mult, modprime, mod2, mod-zero, gcdnex-prime, gcdexh, gcdex-dist, gcd-twicerev, gcd-twice, gcd-multdiv, gcd-mult, gcd-mod-one, gcd-mod, gcd-le-both-h, gcd-div-one, gcd-div-both-h, gcd-conq-one, gcd-alldiv-h, 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/numeral-25 is used by gcd-twicerev, gcd-twice,
nat-mult/one is used by mult-03, mult-02, gcdnex-prime, gcd-twicerev, gcd-twice, divi-sym, divi-succ, divi-one-01, divi-one,
nat-mult/one-01 is used by prime-smallest, prime-prime, mult-01, modprime, gcd-conq-one, 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, divi-two-01,
nat-mult/square-less is used by not-prime,
nat-mult/sqzero is used by not-prime,
nat-mult/three is used by divi-three,
nat-mult/two-02 is used by gcd-mult, gcd-le-both-h, gcd-div-both-h, gcd-alldiv-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/twole-02 is used by gcd-twicerev, gcd-twice,
nat-mult/twols is used by gcd-twicerev, gcd-twice,
nat-mult/zero is used by divi-zero-01, divi-zero, divi-sub, divi-same, divi-add,
nat-mult/zero-01 is used by mult, gcdex-dist, gcd-conq-one, divi-same, divi-add,
nat-mult/zero-02 is used by gcd-multdiv, dist-mult-01, dist-mult,
nat-mult/zero-06 is used by prime-smallest, prime-prime, not-prime, mult-01, modprime, mod-zero, gcdnex-prime, gcd-le-both-h, gcd-div-both-h, gcd-conq-one, gcd-alldiv-h, divi-same, divi-ls, divi-add,

Used from specification nat-basic1

nat-basic1/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-eq, gcd-div-both-h, gcd-alldiv-h, divi-sub, divi-same, divi-ls, divi-dist, dist-mult, dist-eq, dist-add-01, cong-equiv,
nat-basic1/less-1 is used by cong-equiv,
nat-basic1/lf-01 is used by mult-01, gcd-eq,
nat-basic1/lf-02 is used by prime-smallest, gcdex-dist, gcd-mod-one, gcd-le-both-h, divi-ls, cong-equiv,
nat-basic1/ls-02 is used by gcd-mult, cong-equiv,
nat-basic1/ls-03 is used by gcd-div-both, gcd-alldiv, divi-add,
nat-basic1/neq-01 is used by not-prime, gcd-zero-01, dist-eq,
nat-basic1/one is used by twodiv-02, twodiv-01, succ, rax, 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-basic1/one-01 is used by gcd-mod-one, gcd-conq-one,
nat-basic1/one-02 is used by gcd-conq-one,
nat-basic1/ref-1 is used by gcd-le, gcd-id, gcd-eq, dist-same,
nat-basic1/twols-01 is used by not-prime, gcd-two,
nat-basic1/twols-02 is used by prime-smallest, prime-prime, not-prime, modprime, lstwo,
nat-basic1/zero is used by prime-smallest, modprime,

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-le-02 is used by gcdexh,
nat-div/mod-ls is used by cong-equiv,
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,