[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 int-basic2
- int-basic2/add-a
is used by
mone-03,
eqnum-add2,
eqnum-add1,
eqint-neg,
lsnum-add3,
lsnum-add4,
lsnum-add1,
lsnum-add2,
lsnum-addboth1,
lsnum-addboth2,
eqnum-addboth2,
eqnum-addboth1,
- int-basic2/add-c
is used by
mone-03,
eqnum-add2,
eqnum-add1,
eqint-neg,
lsnum-add3,
lsnum-add4,
lsnum-add1,
lsnum-add2,
lsnum-addboth1,
lsnum-addboth2,
eqnum-addboth2,
eqnum-addboth1,
- int-basic2/ls-02
is used by
eqnum-add2,
eqnum-add1,
lsnum-add3,
lsnum-add4,
lsnum-add1,
lsnum-add2,
lsnum-addboth1,
lsnum-addboth2,
eqnum-addboth2,
eqnum-addboth1,
Used from specification int-abs
- int-abs/minus-rew
is used by
eqint-sub,
- int-abs/elim-sub
is used by
eqnum-add2,
eqnum-add1,
lsnum-add3,
lsnum-add4,
lsnum-add1,
lsnum-add2,
lsnum-addboth1,
lsnum-addboth2,
eqnum-addboth2,
eqnum-addboth1,
- int-abs/forward-le-05
is used by
eqnum-add2,
eqnum-add1,
lsnum-add3,
lsnum-add4,
lsnum-add1,
lsnum-add2,
lsnum-addboth1,
lsnum-addboth2,
eqnum-addboth2,
eqnum-addboth1,
- int-abs/lenls
is used by
betweenlsls-zero-one,
- int-abs/lsone
is used by
betweenlsls-zero-one,
- int-abs/neg-03
is used by
eqint-neg,