[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
min-ls1-right,
min-ls-add,
min-le-leftn,
min-add-same,
min-add-l-and-r,
min-add,
max-add,
- nat-basic/c
is used by
min-ls1-right,
min-ls-add,
min-le-leftn,
min-add-same,
min-add-l-and-r,
min-add,
max-add,
- nat-basic/eq-01
is used by
min-ls1-right,
min-add-same,
max-add,
- nat-basic/f
is used by
min-notls2,
min-notls1,
min-not-ls-add,
min-ls-add,
min-le-leftn,
min-l-and-r,
min-add-l-and-r,
max-notls2,
max-notls1,
max-le2,
max-le1,
- nat-basic/l
is used by
min-add-same,
- nat-basic/l-02
is used by
min-le-leftn,
min-add-l-and-r,
min-add,
max-add,
- nat-basic/l-05
is used by
min-ls-add,
- nat-basic/lf
is used by
min-ls-add,
- nat-basic/ls-02
is used by
min-notls2,
min-not-ls-add,
min-ls-right,
min-comm,
max-second-ls,
max-notls1,
max-le1,
max-comm,
- nat-basic/neq-01
is used by
min-le-leftn,
- nat-basic/ref
is used by
min-same,
min-notls2,
min-notls1,
min-not-ls-add,
min-l-and-r,
max-same,
max-notls2,
max-notls1,
max-le2,
max-le1,
- nat-basic/s-04
is used by
min-ls1-right,
- nat-basic/succ
is used by
min-ls-add,
- nat-basic/trans
is used by
min-ls-add,
- nat-basic/zero
is used by
min-0-left,
max-eq-0,
max-0-left,
- nat-basic/zero-01
is used by
min-0-right,
max-eq-0,
max-0-right,
Used from specification nat
- nat/fle
is used by
min-not-ls-add,
min-le-leftn,
min-add-l-and-r,
- nat/le-def
is used by
max-le2,
max-le1,
- nat/le-ls-simp
is used by
max-second-le,
- nat/lels
is used by
min-notls1,
min-not-ls-add,
min-comm,
min-add-l-and-r,
max-comm,
- nat/lels-02
is used by
min-le-left,
min-comm,
max-first-le,
max-comm,
- nat/lels-03
is used by
min-not-ls-add,
min-add-l-and-r,
- nat/ls-le-simp
is used by
min-notls1,