[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/add-num-04 is used by size-two, size-three-02,
nat/eq is used by subsize-eq,
nat/fle is used by size-two-06, size-three,
nat/l-num-02 is used by size-exgr,
nat/l-num-05 is used by size-two-06, size-three-01,
nat/le-ls-simp is used by sub-size-eq,
nat/lels is used by subsize-eq, sizesubl, size-two-06, size-three,
nat/lels-01 is used by sizesub, size-two-06, size-two-02, size-three-01,
nat/ler is used by sub-size-eq,
nat/not-zero is used by size-two-06,
nat/succ-01 is used by sizesubl,

Used from specification nat-basic2

nat-basic2/a is used by subsize-eq, sizesubl, size-zero-02, size-two-06, size-two-03, size-two-02, size-two-01, size-two, size-three-02, size-three-01, size-three, size-one-02, size-one-01, size-one, size-less-01, size-less, size-ins, size-exgr, eq-02,
nat-basic2/c is used by subsize-eq, sizesubl, size-zero-02, size-two-06, size-two-03, size-two-02, size-two-01, size-two, size-three-02, size-three-01, size-three, size-one-02, size-one-01, size-one, size-less-01, size-less, size-ins, size-exgr, eq-02,
nat-basic2/eq is used by size-ins,
nat-basic2/eq-01 is used by size-ins,
nat-basic2/l is used by size-less,
nat-basic2/l-02 is used by size-less-01, size-less,
nat-basic2/nls-fst is used by size-exgr,
nat-basic2/one is used by size-two-03, size-exgr,
nat-basic2/one-03 is used by size-two-03, size-one-02, size-one, eq-02,
nat-basic2/oz is used by size-two-03, size-three-02, size-less, size-exgr,
nat-basic2/z-01 is used by size-zero-02,

Used from specification nat-basic1

nat-basic1/f is used by sub-size, size-two-06, size-two-02, size-three-01, size-three, size-less-01, size-less, size-exgr,
nat-basic1/lf-02 is used by size-two-06,
nat-basic1/neq-01 is used by sub-sizeneqex,
nat-basic1/one is used by size-two-03, size-exgr,
nat-basic1/one-01 is used by size-two-06, size-three-01,
nat-basic1/one-02 is used by size-two-04,
nat-basic1/ref-1 is used by size-less-01, size-exgr,
nat-basic1/zero is used by size-exgr,