[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/forward-lels
is used by
max-a,
- real-abs/forward-lsle
is used by
min-a,
- real-abs/lels
is used by
max-a,
min-distr,
max-distr,
min-c,
max-c,
min-a,
min-ls-self1,
- real-abs/lels-02
is used by
max-a,
min-a,
- real-abs/lels-03
is used by
max-a,
min-distr,
max-distr,
min-a,
min-ls-self1,
- real-abs/lenls
is used by
min-c,
max-c,
Used from specification real-basic
- real-basic/add-assoc
is used by
min-distr,
max-distr,
- real-basic/add-comm
is used by
min-distr,
max-distr,
- real-basic/add-in
is used by
min-distr,
max-distr,
- real-basic/bls-01
is used by
max-a,
min-c,
max-ls-self1,
max-c,
min-a,
- real-basic/blst-01
is used by
max-a,
min-c,
min-i,
max-c,
min-a,
max-i,
- real-basic/irref
is used by
max-ls-both,
max-a,
min-i,
min-ls-both,
max-ls-self1,
min-a,
max-i,
min-ls-self1,
- real-basic/less-add-cancel-l
is used by
min-distr,
max-distr,
- real-basic/trans
is used by
max-a,
min-a,