[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/addex is used by less-notgeqinf,
nat-basic/a is used by eq-natinf-to-nat-3-1, add-ls-cancel-num-02, add-all-zero, ls-notlssucc, add-cancel-num-03, add-not-less, leq-notgradd, add-ls-cancel-num-03, ls-natinf-to-nat-3-1, ls-natinf-to-nat-1-3, less-notgeqinf, num-add, sum-zero, eq-natinf-to-nat-3-2, add-cancel-num-01, sum-zero-fin, add-cancel-03, ls-lsadd, rem-seln-on-add, add-cancel-num-04, ls-succ, less-succ-leq, add-ls-cancel-num-04, ls-natinf-to-nat-3-2, add-assoc, add-ls-cancel-num-01, ls-natinf-to-nat-2-3, eq-natinf-to-nat-3-3, add-less-fin-01, less-less-leftsucc, add-cancel-num-02, ls-natinf-to-nat-3-3, add-ls-cancel-01, add-cancel-01,
nat-basic/add-base is used by add-all-zero,
nat-basic/c is used by eq-natinf-to-nat-3-1, add-ls-cancel-num-02, add-all-zero, ls-notlssucc, add-cancel-num-03, add-not-less, leq-notgradd, add-ls-cancel-num-03, ls-natinf-to-nat-3-1, ls-natinf-to-nat-1-3, less-notgeqinf, num-add, sum-zero, eq-natinf-to-nat-3-2, add-cancel-num-01, sum-zero-fin, add-cancel-03, ls-lsadd, rem-seln-on-add, add-cancel-num-04, ls-succ, less-succ-leq, add-ls-cancel-num-04, ls-natinf-to-nat-3-2, add-assoc, add-ls-cancel-num-01, ls-natinf-to-nat-2-3, eq-natinf-to-nat-3-3, add-less-fin-01, less-less-leftsucc, add-cancel-num-02, add-comm, ls-natinf-to-nat-3-3, add-ls-cancel-01, add-cancel-01,
nat-basic/eq-01 is used by rem-seln-on-add, add-cancel-01,
nat-basic/eq-02 is used by add-cancel-03,
nat-basic/f is used by ls-notlssucc, leq-notgradd, less-notgeqinf, ls-lsadd, add-cancel-num-04, lsle-trans, less-less-leftsucc, add-cancel-num-02,
nat-basic/l is used by ls-notlssucc, add-ls-cancel-01,
nat-basic/l-02 is used by add-not-less, leq-notgradd, ls-lsadd,
nat-basic/less-zero is used by not-less-zero, add-cancel-num-02,
nat-basic/lf-01 is used by ls-notlssucc, less-less-leftsucc,
nat-basic/ls-02 is used by lele-refl, ls-trans, add-cancel-num-04,
nat-basic/neq-01 is used by lele-refl,
nat-basic/one is used by onels-neqzero,
nat-basic/one-01 is used by ls-one,
nat-basic/oz is used by ls-notlssucc, sum-zero-fin, less-less-leftsucc,
nat-basic/refl-nat is used by ls-irref, add-less-fin-01,
nat-basic/s-04 is used by less-succ-leq, add-cancel-num-02,
nat-basic/succ is used by sum-zero-fin, add-cancel-num-02, add-cancel-01,
nat-basic/z-01 is used by sum-zero-fin,
nat-basic/zero is used by zerols-neqzero,

Used from specification nat

nat/anti is used by add-cancel-num-02,
nat/elim-sub is used by add-ls-cancel-num-02, add-cancel-num-03, add-ls-cancel-num-03, add-cancel-num-01, add-cancel-num-04, add-ls-cancel-num-04, add-ls-cancel-num-01,
nat/eqle-one is used by ls-notlssucc, less-less-leftsucc,
nat/fle is used by leq-notgradd, lsle-trans,
nat/fle-01 is used by ls-lsadd, lsle-trans,
nat/le-add is used by add-less-fin-01,
nat/le-def is used by add-cancel-num-04,
nat/le-ls-simp is used by lsle-trans,
nat/lels is used by ls-notlssucc, ls-lsadd, lsle-trans, add-less-fin-01, less-less-leftsucc, add-cancel-num-02, add-ls-cancel-01,
nat/les is used by ls-notlssucc, less-less-leftsucc,
nat/let is used by lsle-trans,
nat/ls-le-simp is used by add-ls-cancel-01,