[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 real-abs
- real-abs/le-def
is used by
inf-unique,
inf-exists,
boundedge-neg-boundedle,
sup-unique,
inf-neg-sup,
lowbound-neg-upperbound,
- real-abs/lels-02
is used by
inf-neg-sup,
- real-abs/lels-03
is used by
inf-unique,
inf-exists,
boundedge-neg-boundedle,
sup-unique,
inf-neg-sup,
lowbound-neg-upperbound,
- real-abs/negle-07
is used by
inf-exists,
boundedge-neg-boundedle,
inf-neg-sup,
lowbound-neg-upperbound,
- real-abs/negle-13
is used by
inf-exists,
boundedge-neg-boundedle,
inf-neg-sup,
- real-abs/sub-le
is used by
lowbound-neg-upperbound,
Used from specification real-basic
- real-basic/blst-01
is used by
inf-unique,
sup-unique,
- real-basic/add-assoc
is used by
boundedge-neg-boundedle,
inf-neg-sup,
lowbound-neg-upperbound,
- real-basic/add-comm
is used by
inf-exists,
boundedge-neg-boundedle,
inf-neg-sup,
lowbound-neg-upperbound,
- real-basic/add-zero
is used by
boundedge-neg-boundedle,
inf-neg-sup,
lowbound-neg-upperbound,
- real-basic/bls-01
is used by
inf-unique,
sup-unique,
- real-basic/double-neg
is used by
inf-exists,
boundedge-neg-boundedle,
inf-neg-sup,
lowbound-neg-upperbound,
- real-basic/negeq
is used by
inf-neg-sup,
- real-basic/negl-ls
is used by
inf-exists,