[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
rev-rev,
rev-size-h,
rev-at-h,
rev-at,
- nat-basic/c
is used by
rev-rev,
rev-size-h,
rev-at-h,
rev-at,
- nat-basic/eq-01
is used by
rev-at-h,
- nat-basic/eqs
is used by
rev-rev,
rev-at-h,
rev-at,
- nat-basic/f
is used by
rev-rev,
rev-size-h,
rev-at-h,
in-at,
rev-at,
- nat-basic/l
is used by
rev-at-h,
- nat-basic/l-01
is used by
rev-at-h,
- nat-basic/l-02
is used by
rev-rev,
rev-at-h,
rev-at,
- nat-basic/l-06
is used by
rev-at-h,
- nat-basic/less-zero
is used by
rev-at-h,
- nat-basic/lf
is used by
rev-at-h,
- nat-basic/lf-01
is used by
rev-rev,
rev-at-h,
rev-at,
- nat-basic/oz
is used by
rev-rev,
- nat-basic/refl-nat
is used by
rev-size,
- nat-basic/s-04
is used by
rev-rev,
rev-at-h,
rev-at,
- nat-basic/succ
is used by
rev-size-h,
rev-at-h,
Used from specification nat
- nat/elim-sub
is used by
rev-rev,
rev-at-h,
rev-at,
- nat/fle
is used by
rev-rev,
rev-at-h,
- nat/fle-01
is used by
rev-at-h,
- nat/le-add
is used by
rev-rev,
- nat/le-def
is used by
rev-size,
- nat/lels
is used by
rev-rev,
rev-at-h,
rev-at,
- nat/lels-02
is used by
rev-at-h,
- nat/lels-03
is used by
rev-size-h,
rev-at-h,
- nat/lep
is used by
rev-at-h,
- nat/ler
is used by
rev-at-h,
rev-at,
- nat/let
is used by
rev-at-h,
- nat/lez
is used by
rev-at-h,
- nat/ls-le-simp
is used by
rev-rev,
rev-at-h,
rev-at,
- nat/succ-01
is used by
rev-rev,
rev-size-h,
rev-at-h,
rev-at,
Used from specification array