[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/a
is used by
range-recbegin,
range-recend,
range-recend-simp,
range-one,
range-recend-simp2,
- nat-basic/add-base
is used by
range-recend,
- nat-basic/c
is used by
range-recbegin,
range-recend,
range-recend-simp,
range-one,
range-recend-simp2,
- nat-basic/f
is used by
range-recbegin,
range-recend,
range-recend-simp2,
- nat-basic/l
is used by
range-recend,
- nat-basic/less-zero
is used by
range-recend,
- nat-basic/lf-01
is used by
range-recend,
- nat-basic/ls-02
is used by
range-recend,
range-recend-simp,
range-recend-simp2,
- nat-basic/neq-01
is used by
range-recend-simp,
range-recend-simp2,
- nat-basic/one-01
is used by
range-recend,
- nat-basic/oz
is used by
range-recend,
- nat-basic/refl-nat
is used by
range-recend,
range-recend-simp,
range-one,
range-recend-simp2,
- nat-basic/s-04
is used by
range-recend,
range-recend-simp,
range-one,
range-recend-simp2,
Used from specification set-union
Used from specification nat
- nat/add-01
is used by
range-recend,
- nat/elim-pred-c
is used by
range-recend,
- nat/eqle-one
is used by
range-recend,
- nat/fle
is used by
range-recbegin,
- nat/fle-01
is used by
range-recbegin,
range-recend,
- nat/le-def
is used by
range-recend,
- nat/lels
is used by
range-recbegin,
range-recend,
- nat/lels-02
is used by
range-recbegin,
range-one,
- nat/lels-03
is used by
range-recbegin,
range-recend-simp2,
- nat/ler
is used by
range-recbegin,
range-one,
- nat/les
is used by
range-recend,
- nat/let
is used by
range-recbegin,
- nat/ls
is used by
range-recend,
- nat/ls-le-simp
is used by
range-recbegin,
range-empty,
- nat/succ-01
is used by
range-recbegin,
Used from specification set-basic
- set-basic/natset/Extension
is used by
range-recbegin,
range-recend,
range-recend-simp,
range-one,
range-empty,
range-recend-simp2,
- set-basic/natset/In-empty
is used by
range-recbegin,
range-recend,
range-empty,
- set-basic/natset/In-insert
is used by
range-recbegin,
range-recend,
range-recend-simp,
range-recend-simp2,
- set-basic/natset/add
is used by
range-recend,
- set-basic/natset/in-04
is used by
range-one,
- set-basic/natset/ne
is used by
range-recbegin,
- set-basic/natset/ne-01
is used by
range-recbegin,