[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
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/add-base
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/c
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/f
is used by
htok-returnfalse-f,
allslotsfull-final,
rely-notinvkey-unchanged,
allslotsfull-final-close,
rely-add,
htok-add,
rely-notinvkey-f,
rely-trans,
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
rely-allslotsfull,
- nat-basic/l
is used by
allslotsfull-incfalse,
allslotsfull-inc,
- nat-basic/l-02
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/l-06
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/less-zero
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
- nat-basic/lf
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/lf-01
is used by
rely-notinvkey-unchanged,
rely-notinvkey-f,
rely-trans,
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
rely-allslotsfull,
- nat-basic/lf-02
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/ls-02
is used by
allslotsfull-inc,
- nat-basic/neq-01
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/one
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/one-01
is used by
allslotsfull-incfalse,
allslotsfull-inc,
- nat-basic/one-04
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/oz
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/refl-Nat
is used by
htok-returnfalse-f,
allslotsfull-incfalse,
allslotsfull-init,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/s-04
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/succ
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/succ-03
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/trans-Nat
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-basic/zero
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
Used from specification nat
- nat/anti
is used by
htok-returnfalse-f,
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/cancel-01
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat/eqle-one
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/fle
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/fle-01
is used by
htok-returnfalse-f,
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/le-add
is used by
allslotsfull-inctrue,
- nat/le-def
is used by
htok-returnfalse-f,
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/le-ls-simp
is used by
hash-ok-lem,
htok-returnfalse-f,
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/le-one
is used by
allslotsfull-inctrue,
- nat/le-sum
is used by
allslotsfull-inc,
- nat/lels
is used by
htok-returnfalse-f,
allslotsfull-incfalse,
allslotsfull-inctrue,
rely-notinvkey-unchanged-f,
allslotsfull-inc,
- nat/lels-03
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/lep
is used by
allslotsfull-inctrue,
- nat/lep-02
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat/ler
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/les
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/let
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/lez
is used by
allslotsfull-incfalse,
allslotsfull-inc,
- nat/ls
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat/ls-01
is used by
allslotsfull-inctrue,
- nat/ls-03
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat/ls-le-simp
is used by
htok-returnfalse-f,
allslotsfull-incfalse,
allslotsfull-init,
allslotsfull-inctrue,
rely-notinvkey-unchanged-f,
allslotsfull-inc,
- nat/not-zero
is used by
allslotsfull-inctrue,
- nat/succ-01
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat/zero
is used by
allslotsfull-inctrue,
allslotsfull-inc,
Used from specification nat-mult
- nat-mult/le-02
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-mult/ls-08
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-mult/ls-10
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-mult/mult-a
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-mult/mult-c
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-mult/rsucc-02
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-mult/two-02
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-mult/zero
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-mult/zero-01
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-mult/zero-06
is used by
allslotsfull-inc,
Used from specification array
Used from specification nat-div
- nat-div/rax
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-div/rec
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-div/cond
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-div/mod-eq
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-div/mod-ls
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-div/mod-zero
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-div/modsucc-less
is used by
allslotsfull-incfalse,
allslotsfull-inctrue,
allslotsfull-inc,
- nat-div/zero
is used by
allslotsfull-inctrue,
allslotsfull-inc,
- nat-div/zero-01
is used by
allslotsfull-inctrue,
allslotsfull-inc,