[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 array-splice

array-splice/buffer/append-at is used by refine-read, refine-write,
array-splice/buffer/copy2append is used by refine-read,
array-splice/buffer/append-a is used by refine-change, refine-read, refine-write,
array-splice/buffer/append-at1 is used by refine-read,
array-splice/buffer/append-eq-right is used by refine-write,
array-splice/buffer/append-len is used by refine-read, refine-write,
array-splice/buffer/copy-append is used by refine-read,
array-splice/buffer/emparray-at is used by refine-read, refine-write,
array-splice/buffer/emparray-len is used by refine-read, refine-write,
array-splice/buffer/range-eq-refl is used by refine-read,
array-splice/buffer/range-eq-refl-simp is used by refine-read,
array-splice/buffer/subarray-append-elim-left is used by refine-read,
array-splice/buffer/subarray-append-left is used by refine-change, refine-write,

Used from specification nat-basic

nat-basic/a is used by refine-change, refine-read, refine-write,
nat-basic/add-base is used by refine-change, refine-read, refine-write,
nat-basic/c is used by refine-change, refine-read, refine-write,
nat-basic/eq-01 is used by refine-write,
nat-basic/eqs is used by refine-read,
nat-basic/f is used by recovery, initialization, refine-unmap, refine-remap, refine-change, refine-read, refine-write,
nat-basic/l is used by refine-read, refine-write,
nat-basic/l-01 is used by refine-read, refine-write,
nat-basic/l-02 is used by refine-read, refine-write,
nat-basic/l-05 is used by refine-read,
nat-basic/l-06 is used by refine-read,
nat-basic/lf-01 is used by recovery, refine-read, refine-write,
nat-basic/lf-02 is used by refine-read,
nat-basic/ls-02 is used by refine-write,
nat-basic/zero is used by refine-write,

Used from specification ebm-base

ebm-base/ebm-le is used by recovery,
ebm-base/ebm-cons-leb-size-le is used by recovery, refine-read,
ebm-base/ebm-order-in-avol-left is used by recovery,

Used from specification nat

nat/add-01 is used by refine-read,
nat/elim-sub is used by refine-change, refine-read, refine-write,
nat/fle is used by refine-read, refine-write,
nat/fle-01 is used by refine-read, refine-write,
nat/ge is used by refine-change, refine-read, refine-write,
nat/le-def is used by refine-read, refine-write,
nat/le-ls-simp is used by refine-read, refine-write,
nat/lels is used by initialization, refine-unmap, refine-remap, refine-change, refine-read, refine-write,
nat/lels-02 is used by refine-change, refine-read, refine-write,
nat/lels-03 is used by refine-read, refine-write,
nat/lep is used by refine-read, refine-write,
nat/lep-02 is used by refine-read,
nat/ler is used by refine-read,
nat/let is used by refine-read, refine-write,
nat/ls-01 is used by refine-read,
nat/ls-02 is used by refine-read, refine-write,
nat/ls-le-simp is used by initialization, refine-unmap, refine-remap, refine-change, refine-read, refine-write,
nat/sub-ls is used by refine-read,

Used from specification store

store/abstract-volumes/At-same is used by initialization, refine-unmap, refine-remap, refine-change, refine-write,
store/abstract-volumes/In-empty is used by initialization,
store/abstract-volumes/insin is used by refine-remap,
store/abstract-volumes/insins is used by refine-remap,
store/abstract-volumes/notmemlookup is used by refine-get-volume-size,

Used from specification error-class

error-class/ecommit is used by refine-sync-device, recovery, initialization, refine-remap, refine-change, refine-read, refine-write,
error-class/esuccess is used by recovery, initialization, refine-remap, refine-change, refine-read, refine-write,
error-class/not-esuccess is used by recovery, initialization, refine-remap, refine-change, refine-read, refine-write,

Used from specification aleb

aleb/disj is used by recovery,
aleb/inj is used by recovery, refine-remap, refine-change, refine-write,
aleb/sel is used by recovery, refine-read, refine-write,

Used from specification error

error/disj-91 is used by refine-sync-device, recovery, initialization, refine-remap, refine-change, refine-read, refine-write,

Used from specification leb

leb/disj is used by recovery,
leb/disj-01 is used by recovery,
leb/disj-02 is used by recovery,
leb/inj is used by recovery, refine-read, refine-write,
leb/sel is used by refine-read, refine-write,
leb/sel-01 is used by refine-write,
leb/test-01 is used by refine-remap,
leb/test-03 is used by elim-mapped, refine-read, refine-write,

Used from specification align

align/is-aligned-zero is used by refine-write,

Used from specification array-copy

array-copy/buffer/at-copy is used by refine-read,
array-copy/abstract-volume/at-fill-mkarray is used by initialization,
array-copy/avolume/at-fill-mkarray is used by initialization,
array-copy/buffer/size-copy is used by refine-read,
array-copy/abstract-volume/size-fill is used by initialization,
array-copy/avolume/size-fill is used by initialization,
array-copy/buffer/size-subarray is used by recovery, refine-change, refine-read, refine-write,
array-copy/buffer/subarray-at is used by refine-read, refine-write,
array-copy/buffer/subarray-elim is used by refine-change, refine-read, refine-write,
array-copy/buffer/subarray-zero is used by refine-remap,

Used from specification ebm-vol-abs

ebm-vol-abs/abs-at is used by initialization, refine-unmap, refine-remap, refine-change, refine-write,
ebm-vol-abs/abs-at is used by recovery, refine-unmap, refine-remap, refine-change, refine-read, refine-write,
ebm-vol-abs/abs-leb-eq-mapped is used by recovery, refine-read, refine-write,
ebm-vol-abs/abs-leb-erased is used by recovery, initialization,
ebm-vol-abs/abs-leb-mapped is used by recovery, refine-remap, refine-change, refine-read, refine-write,
ebm-vol-abs/abs-leb-unmapped is used by recovery, refine-unmap, refine-remap,
ebm-vol-abs/abs-size is used by recovery, refine-get-volume-size, initialization, refine-unmap, refine-remap, refine-change, refine-read, refine-write,
ebm-vol-abs/ebm-cons-above-fillcount is used by refine-read, refine-write,
ebm-vol-abs/ebm-cons-aligned is used by recovery,
ebm-vol-abs/ebm-cons-is-aligned-fill is used by refine-write,
ebm-vol-abs/ebm-cons-lebsize is used by refine-read, refine-write,

Used from specification eraseblock

eraseblock/lebsize-neq-zero is used by refine-read, refine-write,
eraseblock/page-size is used by refine-write,

Used from specification oelem

oelem/nat-set/irreflexivity is used by refine-read,
oelem/nat-set/sls is used by refine-read,

Used from specification array

array/buffer/Extension is used by refine-read, refine-write,
array/avolume/Extension is used by initialization, refine-unmap, refine-remap, refine-change, refine-write,
array/avolume/Put-other is used by refine-unmap, refine-remap, refine-change, refine-write,
array/abstract-volume/Put-other is used by refine-unmap, refine-remap, refine-change, refine-write,
array/abstract-volume/Put-same is used by refine-unmap, refine-remap, refine-change, refine-write,
array/abstract-volume/Size-mkarray is used by initialization,
array/avolume/Size-mkarray is used by initialization,
array/avolume/Size-put is used by refine-unmap, refine-remap, refine-change, refine-write,
array/abstract-volume/Size-put is used by refine-unmap, refine-remap, refine-change, refine-write,
array/avolume/cgetput is used by refine-unmap, refine-remap, refine-change, refine-write,
array/abstract-volume/cputput is used by refine-remap,

Used from specification ebm-vol-refine

ebm-vol-refine/elim-mapped is used by elim-mapped,

Used from specification ebm-vol-inv

ebm-vol-inv/ebm-vol-le is used by recovery,