[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-basic1

nat-basic1/less-2 is used by l-addone,
nat-basic1/trans-1 is used by l-03,
nat-basic1/disj-1 is used by z-01,
nat-basic1/elim-pred-c is used by pse, ps, pred, pe-01, pe, even-02, even,
nat-basic1/f is used by twols, s, q-01, pls, pe-01, nls-snd, neq-02, neq, less-06, less-04, less-03, less-02, less-01, less, l-addone, l-08, l-06, l-05, l-03, l-02, l, expand-nat, even-05, even-02, between, addex,
nat-basic1/inj-1 is used by z, succ, rec, eq-01, c, a,
nat-basic1/lf is used by s, l-05, between,
nat-basic1/lf-01 is used by q-01, pe-01, neq-02, addex,
nat-basic1/lf-02 is used by neq-02, neq,
nat-basic1/lf-03 is used by l-addone, l-08, l-06, expand-nat,
nat-basic1/lf-04 is used by pls,
nat-basic1/lf-05 is used by pls, even-02,
nat-basic1/lf-06 is used by pls, nls-snd, less-06, less-02, less-01, l-addone, l-06, expand-nat,
nat-basic1/lf-07 is used by s,
nat-basic1/ls-02 is used by q-01, neq-02, neq-01, less-06, l-07,
nat-basic1/ls-03 is used by pls, neq-01,
nat-basic1/neq-01 is used by succ-03, less-03, less, addex,
nat-basic1/one is used by twols,
nat-basic1/one-01 is used by l-02,
nat-basic1/psh-04 is used by lp,
nat-basic1/ref-1 is used by s, pls, l-01, l, between, addex,
nat-basic1/trans-1 is used by s, l-05, between,
nat-basic1/zero is used by even-02, addex,
nat-basic1/zero-01 is used by twols, q-01, addex,