[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
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
- nat-basic/c
is used by
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
- nat-basic/eq-01
is used by
to-vtbl-size,
- nat-basic/ref
is used by
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
- nat-basic/s-04
is used by
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
Used from specification store
- store/volumes/Extension
is used by
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
- store/vtbl/Extension
is used by
to-vtbl-update-vol,
to-vtbl-update,
- store/vtbl/In-insert
is used by
to-vtbl-in,
- store/volumes/In-insert
is used by
to-vtbl-in,
- store/vtbl/Size-insert
is used by
to-vtbl-size,
- store/volumes/exin
is used by
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
- store/vtbl/notmemlookup
is used by
to-vtbl-update-vol,
to-vtbl-update,
- store/vtbl/At-other
is used by
to-vtbl-update-vol,
to-vtbl-update,
to-vtbl-at,
- store/volumes/At-other
is used by
to-vtbl-at,
- store/vtbl/At-same
is used by
to-vtbl-update-vol,
to-vtbl-update,
to-vtbl-at,
- store/volumes/At-same
is used by
to-vtbl-at,
- store/volumes/Del-at
is used by
to-vtbl-update-vol,
to-vtbl-update,
- store/volumes/Del-in
is used by
to-vtbl-update-vol,
to-vtbl-update,
- store/volumes/In-empty
is used by
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
- store/vtbl/In-empty
is used by
to-vtbl-in,
- store/volumes/In-insert
is used by
to-vtbl-size,
- store/volumes/Size-empty
is used by
to-vtbl-size,
- store/vtbl/Size-empty
is used by
to-vtbl-size,
- store/volumes/Size-insert
is used by
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
- store/vtbl/in-neq
is used by
to-vtbl-update-vol,
to-vtbl-update,
- store/volumes/in-neq
is used by
to-vtbl-at,
- store/vtbl/insin
is used by
to-vtbl-update-vol,
to-vtbl-update,
- store/volumes/notin-del-notin
is used by
to-vtbl-update,
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
- store/volumes/notmemlookup
is used by
to-vtbl-update,
to-vtbl-size,
to-vtbl-in,
to-vtbl-at,
- store/vtbl/size-in
is used by
to-vtbl-size,
Used from specification array