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

nat-inf-basic/disj is used by add-inf-02,
nat-inf-basic/inj is used by eq-natinf-to-nat-2-1,
nat-inf-basic/sel is used by prime-add-fin,
nat-inf-basic/disj is used by zerols-neqzero, sum-zero-fin, sum-zero, sum-notinf, rem-seln-on-add, prime-add-fin, onels-neqzero, ls-one, less-less-leftsucc, lele-refl, inf-less, add-less-fin-01, add-less, add-inf-02, add-inf-01, add-cancel-03, add-cancel-02, add-cancel-01,
nat-inf-basic/inj is used by zerols-neqzero, sum-zero-fin, sum-zero, onels-neqzero, ls-one, less-less-leftsucc, lele-refl, eqsucc-ls, add-less-fin-01, add-cancel-num-02, add-cancel-03, add-cancel-02,
nat-inf-basic/sel is used by rem-seln-on-add, prime-add-fin,

Used from specification nat

nat/add is used by add-cancel-num-01,
nat/anti is used by add-cancel-num-02,
nat/elim-sub is used by add-ls-cancel-num-04, add-ls-cancel-num-03, add-ls-cancel-num-02, add-ls-cancel-num-01, add-cancel-num-04, add-cancel-num-03, add-cancel-num-01,
nat/fle is used by lsle-trans, leq-notgradd,
nat/fle-01 is used by lsle-trans, ls-lsadd,
nat/le-add is used by add-less-fin-01,
nat/le-ls-simp is used by lsle-trans,
nat/lels is used by lsle-trans, ls-lsadd, lele-refl, add-ls-cancel-01, add-less-fin-01, add-cancel-num-02,
nat/lels-03 is used by add-cancel-num-04,
nat/ler is used by lele-refl,
nat/let is used by lsle-trans,
nat/ls-le-simp is used by add-ls-cancel-01,

Used from specification nat-basic2

nat-basic2/addex is used by less-notgeqinf,
nat-basic2/a is used by sum-zero-fin, sum-zero, rem-seln-on-add, num-add, ls-succ, ls-natinf-to-nat-3-3, ls-natinf-to-nat-3-2, ls-natinf-to-nat-3-1, ls-natinf-to-nat-2-3, ls-natinf-to-nat-1-3, ls-lsadd, less-succ-leq, less-notgeqinf, less-less-leftsucc, leq-notgradd, eqsum-notless, eq-natinf-to-nat-3-3, eq-natinf-to-nat-3-2, eq-natinf-to-nat-3-1, add-not-less, add-ls-cancel-num-04, add-ls-cancel-num-03, add-ls-cancel-num-02, add-ls-cancel-num-01, add-ls-cancel-01, add-less-fin-01, add-cancel-num-04, add-cancel-num-03, add-cancel-num-02, add-cancel-num-01, add-cancel-03, add-cancel-01, add-assoc, add-all-zero,
nat-basic2/add-base is used by add-all-zero,
nat-basic2/c is used by sum-zero-fin, sum-zero, rem-seln-on-add, num-add, ls-succ, ls-natinf-to-nat-3-3, ls-natinf-to-nat-3-2, ls-natinf-to-nat-3-1, ls-natinf-to-nat-2-3, ls-natinf-to-nat-1-3, ls-lsadd, less-succ-leq, less-notgeqinf, less-less-leftsucc, leq-notgradd, inf-inseq-reduce, eqsum-notless, eq-natinf-to-nat-3-3, eq-natinf-to-nat-3-2, eq-natinf-to-nat-3-1, add-not-less, add-ls-cancel-num-04, add-ls-cancel-num-03, add-ls-cancel-num-02, add-ls-cancel-num-01, add-ls-cancel-01, add-less-fin-01, add-comm, add-cancel-num-04, add-cancel-num-03, add-cancel-num-02, add-cancel-num-01, add-cancel-03, add-cancel-01, add-assoc, add-all-zero,
nat-basic2/eq is used by add-cancel-03,
nat-basic2/eq-01 is used by rem-seln-on-add, add-cancel-01,
nat-basic2/l is used by eqsum-notless, add-ls-cancel-01,
nat-basic2/l-02 is used by ls-lsadd, leq-notgradd, add-not-less,
nat-basic2/oz is used by sum-zero-fin,
nat-basic2/s is used by less-succ-leq, less-less-leftsucc, add-cancel-num-02,
nat-basic2/succ is used by sum-zero-fin, add-cancel-num-02, add-cancel-01,
nat-basic2/z-01 is used by sum-zero-fin,

Used from specification nat-basic1

nat-basic1/f is used by lsle-trans, ls-lsadd, less-notgeqinf, leq-notgradd, add-cancel-num-04, add-cancel-num-02,
nat-basic1/less-1 is used by add-cancel-num-02,
nat-basic1/ls-02 is used by ls-trans, lele-refl,
nat-basic1/neq-01 is used by less-less-leftsucc, lele-refl,
nat-basic1/one is used by onels-neqzero,
nat-basic1/one-01 is used by ls-one,
nat-basic1/ref-1 is used by ls-notlssucc, ls-irref, add-less-fin-01,
nat-basic1/zero is used by zerols-neqzero,
nat-basic1/zero-01 is used by not-less-zero,