[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-basic1
- int-basic1/forward-pos
is used by
odd-rec,
- int-basic1/irref
is used by
min-03,
min-02,
min,
max-a,
max-04,
max,
- int-basic1/lf-01
is used by
min-a,
min-02,
- int-basic1/lf-07
is used by
min-a,
- int-basic1/ls-01
is used by
min-c,
min-a,
max-c,
- int-basic1/lst
is used by
max-01,
- int-basic1/lst-01
is used by
min-c,
min-a,
max-c,
max-a,
- int-basic1/trans
is used by
min-a,
min-02,
Used from specification int-mult
- int-mult/dist-rsplit
is used by
even-rec,
- int-mult/ex-two
is used by
not-odd-ex,
- int-mult/add-mult-two
is used by
odd-zero,
odd-two,
odd-rec,
odd-one,
odd-def-mod,
not-odd-ex,
not-even-odd,
even-zero,
even-rec,
even-not,
even-def-mod,
- int-mult/associativity
is used by
sgn-09,
sgn-02-01,
sgn-01-01,
odd-zero,
odd-two,
odd-rec,
odd-one,
odd-def-mod,
not-odd-ex,
not-even-odd,
even-zero,
even-rec,
even-not,
even-mult,
even-def-mod,
- int-mult/commutativity
is used by
sgn-09,
sgn-02-01,
sgn-01-01,
odd-zero,
odd-two,
odd-rec,
odd-one,
odd-def-mod,
not-odd-ex,
not-even-odd,
even-zero,
even-rec,
even-not,
even-mult,
even-def-mod,
- int-mult/eq-dist
is used by
even-not,
- int-mult/eq-one
is used by
odd-two,
- int-mult/eq-one-neg
is used by
odd-zero,
- int-mult/eq-pos
is used by
odd-rec,
odd-def-mod,
not-even-odd,
even-def-mod,
- int-mult/minus-one-02
is used by
sgn-02-01,
sgn-01-01,
- int-mult/odd-even
is used by
not-odd-ex,
- int-mult/one
is used by
sgn-09,
sgn-02-01,
- int-mult/succ-rmerge
is used by
odd-rec,
- int-mult/zero-neq-01
is used by
odd-one,
even-zero,
Used from specification int-abs
- int-abs/numadd-01
is used by
odd-rec,
- int-abs/abs-06
is used by
min-abs-zero,
- int-abs/abs-07
is used by
min-abs-zero,
- int-abs/absls
is used by
min-abs-zero-01,
- int-abs/elim-sub
is used by
odd-rec,
even-rec,
even-not,
- int-abs/forward-le-01
is used by
odd-rec,
- int-abs/forward-le-02
is used by
min-abs-zero-01,
- int-abs/forward-le-05
is used by
odd-rec,
- int-abs/forward-lele
is used by
max-01,
- int-abs/forward-lels
is used by
min-01,
max-a,
max-01,
- int-abs/forward-lsle
is used by
max-01,
- int-abs/lels
is used by
sr,
sgn-06,
min-c,
min-03,
min-01,
max-a,
max-03,
max-01,
- int-abs/lels-01
is used by
sgn-08,
sgn-04,
sgn-03,
sgn-02-01,
sgn-01,
- int-abs/lels-03
is used by
sgn-06,
min-03,
min-01,
max-a,
max-03,
max-01,
- int-abs/lenls
is used by
sgn-04,
sgn+1,
min-right,
min-c,
- int-abs/minus-add
is used by
odd-rec,
- int-abs/mone-06
is used by
odd-rec,
- int-abs/neg-12
is used by
sgn-02-01,
sgn-01-01,
- int-abs/numadd
is used by
odd-rec,
even-rec,
- int-abs/numadd-01
is used by
odd-zero,
odd-two,
odd-one,
- int-abs/numls-02
is used by
odd-rec,
- int-abs/numlsledel-01
is used by
odd-rec,
- int-abs/sub-eq
is used by
odd-rec,
- int-abs/sub-le-01
is used by
sgn-04,
- int-abs/sub-ls
is used by
sgn-06,
- int-abs/zero-gels-04
is used by
sgn-01,
Used from specification int-basic2
- int-basic2/add-a
is used by
sgn-06,
sgn-04,
odd-zero,
odd-two,
odd-rec,
odd-one,
odd-def-mod,
not-odd-ex,
not-even-odd,
even-zero,
even-rec,
even-not,
even-def-mod,
- int-basic2/add-c
is used by
sgn-07,
sgn-06,
sgn-05,
sgn-04,
odd-zero,
odd-two,
odd-rec,
odd-one,
odd-def-mod,
not-odd-ex,
not-even-odd,
even-zero,
even-rec,
even-not,
even-def-mod,
- int-basic2/add-zero-rev
is used by
sgn-06,
sgn-04,
even-rec,
- int-basic2/succ-01
is used by
min-02,
Used from specification int-div