[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/f
is used by
challenge3b,
challenge3a,
challenge3,
- nat-basic1/lf
is used by
challenge3b,
challenge3a,
- nat-basic1/lf-01
is used by
challenge3b,
challenge3a,
- nat-basic1/lf-02
is used by
challenge3b,
challenge3a,
- nat-basic1/ls-02
is used by
challenge3b,
challenge3a,
- nat-basic1/neq-01
is used by
challenge3b,
challenge3a,
- nat-basic1/ref-1
is used by
challenge3b,
challenge3a,
- nat-basic1/trans-1
is used by
challenge3b,
challenge3a,
- nat-basic1/zero-01
is used by
challenge3b,
challenge3a,
Used from specification nat
- nat/anti
is used by
challenge3b,
challenge3a,
- nat/elim-sub
is used by
challenge3b,
challenge3a,
- nat/eqle-one
is used by
challenge3b,
challenge3a,
- nat/fle
is used by
challenge3b,
challenge3a,
- nat/fle-01
is used by
challenge3b,
challenge3a,
- nat/le
is used by
challenge3b,
challenge3a,
- nat/le-add
is used by
challenge3b,
challenge3a,
- nat/le-ls-simp
is used by
challenge3b,
challenge3a,
- nat/lels
is used by
challenge3b,
challenge3a,
- nat/lels-01
is used by
challenge3b,
challenge3a,
- nat/lels-02
is used by
challenge3b,
challenge3a,
- nat/lels-03
is used by
challenge3b,
challenge3a,
- nat/lep-02
is used by
challenge3b,
challenge3a,
- nat/ler
is used by
challenge3b,
challenge3a,
- nat/lez
is used by
challenge3b,
challenge3a,
- nat/ls-01
is used by
challenge3b,
challenge3a,
- nat/ls-le-simp
is used by
challenge3b,
challenge3a,
- nat/succ-01
is used by
challenge3b,
challenge3a,
- nat/zero-02
is used by
challenge3b,
challenge3a,
Used from specification nat-basic2
- nat-basic2/a
is used by
challenge3b,
challenge3a,
- nat-basic2/c
is used by
challenge3b,
challenge3a,
- nat-basic2/eq-inc-neq
is used by
challenge3b,
challenge3a,
- nat-basic2/eqs
is used by
challenge3b,
challenge3a,
- nat-basic2/l
is used by
challenge3b,
challenge3a,
- nat-basic2/l-02
is used by
challenge3b,
challenge3a,
- nat-basic2/l-06
is used by
challenge3b,
challenge3a,
- nat-basic2/s
is used by
challenge3b,
challenge3a,
- nat-basic2/succ
is used by
challenge3b,
challenge3a,