[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 lebref

lebref/disj is used by refine-wl-worker, recovery, refine-create-volume,
lebref/inj is used by refine-wl-worker, refine-create-volume,

Used from specification apeb

apeb/elim is used by refine-wl-worker, recovery, refine-write, refine-read, refine-create-volume, refine-change,
apeb/inj is used by recovery, refine-write, refine-read,
apeb/sel-04 is used by recovery, refine-write,
apeb/sel-05 is used by lf-mapped-valid-vidhdr, lf-mapped-not-bad, recovery, refine-write, refine-read,
apeb/sel-06 is used by lf-mapped-data, refine-wl-worker, recovery, refine-write, refine-read, refine-create-volume, refine-change,
apeb/sel-07 is used by refine-wl-worker, recovery, refine-write, refine-create-volume, refine-change,
apeb/sel-08 is used by lf-mapped-not-bad, recovery, refine-write, refine-read,

Used from specification array-splice

array-splice/buffer/copy2append is used by refine-write,
array-splice/buffer/range-eq-ext is used by rangeeq-emptyleb-datasize, recovery,
array-splice/buffer/range-eq-subarrays is used by refine-write,
array-splice/buffer/subarray-elim-right is used by refine-write,
array-splice/buffer/append-a is used by refine-write, refine-map, refine-change,
array-splice/buffer/append-eq-left is used by refine-write, refine-change,
array-splice/buffer/append-len is used by refine-write,
array-splice/buffer/append-zero-left is used by refine-map,
array-splice/buffer/append-zero-right is used by refine-write,
array-splice/buffer/emparray-at is used by emptyleb-mkempbuf, recovery, refine-write,
array-splice/buffer/emparray-len is used by emptyleb-mkempbuf, recovery, refine-write,
array-splice/buffer/mkemparray0-append-left is used by refine-map,
array-splice/buffer/range-eq-0 is used by refine-write,
array-splice/buffer/range-eq-refl is used by refine-write, refine-read,
array-splice/buffer/subarray-append-elim-left is used by refine-write,

Used from specification nat-basic

nat-basic/a is used by rangeeq-emptyleb-datasize, recovery, refine-write, refine-read, refine-map, refine-change,
nat-basic/add-base is used by rangeeq-emptyleb-datasize, recovery, refine-write, refine-read, refine-change,
nat-basic/c is used by rangeeq-emptyleb-datasize, recovery, refine-write, refine-read, refine-map, refine-change,
nat-basic/eq-01 is used by refine-write,
nat-basic/eq-02 is used by refine-write,
nat-basic/eqs is used by refine-write, refine-read, refine-change,
nat-basic/f is used by rangeeq-emptyleb-datasize, lf-mapped-valid-vidhdr, lf-mapped-not-bad, lf-mapped-in-apebs, lf-mapped-data, refine-wl-worker, refine-erase-worker, recovery, refine-write, refine-read, refine-erase, refine-create-volume, refine-unmap, refine-map, refine-change,
nat-basic/l is used by refine-write,
nat-basic/l-01 is used by rangeeq-emptyleb-datasize, refine-write,
nat-basic/l-02 is used by recovery, refine-write,
nat-basic/l-05 is used by refine-write, refine-read,
nat-basic/lf-01 is used by rangeeq-emptyleb-datasize, lf-mapped-data, refine-wl-worker, refine-erase-worker, recovery, refine-write, refine-read, refine-erase, refine-create-volume, refine-unmap,
nat-basic/lf-02 is used by lf-mapped-valid-vidhdr, lf-mapped-not-bad, recovery, refine-write, refine-read,
nat-basic/s-04 is used by rangeeq-emptyleb-datasize,
nat-basic/succ is used by rangeeq-emptyleb-datasize,
nat-basic/zero is used by refine-write,
nat-basic/zero-01 is used by rangeeq-emptyleb-datasize,

Used from specification list-set

list-set/erasequeue-base/subset-app-01 is used by refine-erase-worker,
list-set/erasequeue-base/subset-empty is used by refine-erase,

Used from specification erasequeue

erasequeue/queue-in-vl is used by recovery,
erasequeue/in-vl-in-lebrefs is used by refine-wl-worker, recovery, refine-create-volume,

Used from specification ebm-base

ebm-base/ebm-cons is used by recovery,
ebm-base/ebm-cons-def is used by recovery,
ebm-base/ebm-le is used by recovery,
ebm-base/ebm-cons-leb-size is used by refine-write, refine-read,
ebm-base/ebm-cons-write is used by refine-write,
ebm-base/erased-fill is used by refine-wl-worker,
ebm-base/valid-leb-def is used by recovery, refine-write,

Used from specification avidheader

avidheader/elim is used by lf-mapped-not-bad, refine-read,
avidheader/sel-06 is used by lf-mapped-not-bad,
avidheader/sel-08 is used by lf-mapped-not-bad,
avidheader/test-01 is used by recovery,
avidheader/test-03 is used by lf-mapped-not-bad, refine-read,

Used from specification nat

nat/elim-sub is used by rangeeq-emptyleb-datasize, recovery, refine-write, refine-read, refine-change,
nat/eq-01 is used by refine-write,
nat/fle is used by rangeeq-emptyleb-datasize, refine-wl-worker, recovery, refine-write, refine-read, refine-unmap,
nat/fle-01 is used by rangeeq-emptyleb-datasize, refine-wl-worker, recovery, refine-write, refine-read,
nat/ge is used by refine-write, refine-read, refine-map, refine-change,
nat/le-def is used by rangeeq-emptyleb-datasize, refine-wl-worker, recovery, refine-write, refine-read, refine-change,
nat/le-ls-simp is used by rangeeq-emptyleb-datasize, lf-mapped-in-apebs, refine-wl-worker, refine-write, refine-read,
nat/lels is used by rangeeq-emptyleb-datasize, lf-mapped-in-apebs, emptyleb-mkempbuf, refine-wl-worker, refine-erase-worker, recovery, refine-write, refine-read, refine-unmap,
nat/lels-02 is used by refine-write, refine-change,
nat/lels-03 is used by rangeeq-emptyleb-datasize, refine-write,
nat/lep is used by refine-write,
nat/lep-02 is used by rangeeq-emptyleb-datasize, refine-write,
nat/ler is used by rangeeq-emptyleb-datasize, recovery, refine-write, refine-read,
nat/let is used by rangeeq-emptyleb-datasize, recovery, refine-write,
nat/lez is used by rangeeq-emptyleb-datasize, refine-write, refine-map,
nat/ls-01 is used by rangeeq-emptyleb-datasize,
nat/ls-02 is used by refine-write,
nat/ls-le-simp is used by rangeeq-emptyleb-datasize, emptyleb-mkempbuf, refine-wl-worker, recovery, refine-write, refine-read,
nat/sub-base is used by refine-map,
nat/succ-01 is used by rangeeq-emptyleb-datasize,
nat/zero is used by refine-write,

Used from specification store

store/volumes/At-other is used by refine-create-volume,
store/volumes/In-insert is used by refine-create-volume,
store/abstract-volumes/In-insert is used by refine-create-volume,
store/abstract-volumes/At-in-out is used by refine-create-volume,
store/abstract-volumes/At-same is used by refine-write, refine-create-volume, refine-change,
store/volumes/At-same is used by refine-wl-worker, refine-write, refine-create-volume, refine-change,
store/volumes/In-empty is used by initialization,
store/abstract-volumes/In-empty is used by initialization,
store/abstract-volumes/In-insert is used by refine-write,
store/volumes/In-insert is used by refine-wl-worker, refine-write, refine-erase, refine-create-volume, refine-change,
store/abstract-volumes/in-neq is used by refine-create-volume,
store/volumes/ins-same-01 is used by refine-erase,
store/abstract-volumes/insin is used by refine-write, refine-change,
store/volumes/insin is used by refine-wl-worker, refine-write, refine-change,
store/abstract-volumes/insins is used by refine-write,

Used from specification set-union

set-union/lebrefset/subdef is used by refine-wl-worker, recovery, refine-create-volume,
set-union/nat-set/Delete is used by refine-erase,
set-union/lebrefset/One is used by refine-create-volume,

Used from specification error-class

error-class/ecommit is used by refine-read,
error-class/esuccess is used by recovery, refine-write, refine-read, refine-map, initialization,
error-class/not-esuccess is used by recovery, refine-write, refine-read, refine-erase, refine-create-volume, refine-map, refine-change, initialization,

Used from specification error

error/disj-91 is used by refine-read,

Used from specification set-basic

set-basic/lebrefset/In-insert is used by refine-wl-worker,
set-basic/lebrefset/in-04 is used by refine-create-volume,
set-basic/nat-set/ne-01 is used by refine-erase,
set-basic/lebrefset/sub-insert-01 is used by refine-write,

Used from specification wlarray

wlarray/elim-update-status is used by refine-erase,

Used from specification wlstatus

wlstatus/disj-02 is used by lf-mapped-not-bad, refine-read,
wlstatus/disj-03 is used by refine-erase,

Used from specification ubi-asm

ubi-asm/inv-change is used by refine-change,
ubi-asm/inv-create-volume is used by refine-create-volume,
ubi-asm/inv-erase-all is used by refine-erase,
ubi-asm/inv-format is used by initialization,
ubi-asm/inv-recover is used by recovery,
ubi-asm/inv-sync-device is used by refine-sync-device,
ubi-asm/inv-unmap is used by refine-erase,
ubi-asm/inv-wl-worker is used by refine-wl-worker,
ubi-asm/prepost-erase-worker-helper is used by refine-erase-worker,
ubi-asm/prepost-io-write-data is used by refine-write,
ubi-asm/prepost-write-multiple is used by refine-write,
ubi-asm/ubi-io-inv-fwd is used by refine-wl-worker, recovery, refine-write, refine-read,

Used from specification ubi-io-pre

ubi-io-pre/read-data-pre is used by refine-write, refine-read,
ubi-io-pre/write-data-pre is used by refine-write,

Used from specification list-data

list-data/erasequeue-base/elim-list-c is used by refine-erase-worker,

Used from specification ubi-io-inv

ubi-io-inv/peb-inv is used by recovery,
ubi-io-inv/inv-size is used by recovery,
ubi-io-inv/peb-inv-size is used by recovery,

Used from specification leb

leb/disj is used by lf-mapped-data, refine-wl-worker, recovery, refine-write, refine-read, refine-change,
leb/disj-01 is used by recovery,
leb/disj-02 is used by recovery, refine-write,
leb/elim is used by refine-wl-worker, recovery, refine-write, refine-read,
leb/inj is used by recovery,
leb/sel is used by lf-mapped-data, refine-wl-worker, recovery, refine-write, refine-read,
leb/sel-01 is used by lf-mapped-data, refine-wl-worker, recovery, refine-write,
leb/test-01 is used by recovery,
leb/test-02 is used by refine-wl-worker, recovery, refine-create-volume,
leb/test-03 is used by lf-mapped-data, refine-wl-worker, recovery, refine-write, refine-read,

Used from specification align

align/alignup-le-is-aligned is used by refine-change,
align/alignup-same is used by refine-change,
align/is-aligned-add is used by refine-write,
align/is-aligned-zero is used by refine-write, refine-map,

Used from specification ubi-base

ubi-base/valid-ebatbl is used by lf-mapped-valid-vidhdr, lf-mapped-not-bad, lf-mapped-in-apebs, refine-write, refine-read,
ubi-base/valid-wl is used by lf-mapped-not-bad, refine-read,
ubi-base/bitflip-cons-del is used by refine-erase,
ubi-base/bitflip-cons-set is used by refine-erase,
ubi-base/mapped-pebs-add-empty-vol is used by refine-create-volume,
ubi-base/mapped-pebs-unmap is used by refine-erase,
ubi-base/ubi-cons is used by refine-wl-worker, refine-erase-worker, refine-get-page-size, refine-get-leb-size, refine-sync-device, recovery, refine-write, refine-read, refine-get-volume-size, refine-erase, refine-create-volume, refine-unmap, refine-map, refine-change, initialization,
ubi-base/valid-ebatbl-unmap is used by refine-erase,
ubi-base/valid-eraseqd-base is used by refine-erase,
ubi-base/valid-eraseqp-base is used by refine-erase,
ubi-base/valid-eraseqw-size-left is used by refine-erase-worker,
ubi-base/valid-vtbl-update-other-pebs is used by refine-write,
ubi-base/valid-vtbl-update-vols is used by refine-wl-worker, refine-write, refine-erase, refine-change,

Used from specification erasequeueentry

erasequeueentry/elim is used by refine-erase-worker,

Used from specification ubi-abs

ubi-abs/abs-def is used by lf-mapped-data, refine-wl-worker, recovery, refine-write, refine-read, refine-get-volume-size, refine-create-volume, initialization,
ubi-abs/abs-erase-emptyq is used by refine-erase,
ubi-abs/abs-idset-fwd is used by refine-erase,
ubi-abs/abs-lebrefs-subset-noterased-some is used by refine-wl-worker, refine-write, refine-change,
ubi-abs/abs-queue-subset is used by refine-erase-worker, refine-erase,
ubi-abs/absexpt-mapped-abs is used by refine-wl-worker, refine-write, refine-change,
ubi-abs/absf-at is used by recovery,
ubi-abs/absf-size is used by recovery,
ubi-abs/absfv-at is used by recovery,
ubi-abs/absfv-in is used by recovery,
ubi-abs/abs-absexpt is used by refine-write, refine-change,
ubi-abs/abs-avols-in is used by refine-wl-worker, recovery, refine-write, refine-get-volume-size, refine-erase, refine-create-volume, refine-unmap, refine-map, refine-change,
ubi-abs/abs-avols-size is used by refine-write, refine-erase, refine-unmap, refine-map, refine-change,
ubi-abs/abs-idset-fwd is used by refine-wl-worker, refine-erase-worker, refine-sync-device, refine-write, refine-erase, refine-create-volume, refine-change,
ubi-abs/abs-lebrefs-subset is used by refine-write, refine-create-volume, refine-change,
ubi-abs/abs-queue-subset is used by refine-sync-device, refine-erase,
ubi-abs/abs-unmap is used by refine-erase, refine-unmap,
ubi-abs/abs-unmap-twice is used by refine-write, refine-unmap,
ubi-abs/abs-vols-in is used by refine-wl-worker, recovery, refine-write, refine-get-volume-size, refine-erase, refine-create-volume, refine-unmap, refine-map, refine-change,
ubi-abs/abs-vols-mapped is used by lf-mapped-data, refine-wl-worker, refine-write, refine-erase, refine-unmap, refine-map, refine-change,
ubi-abs/abs-vols-size is used by refine-wl-worker, refine-write, refine-erase, refine-unmap, refine-map, refine-change,
ubi-abs/abs-vols-unmapped is used by refine-write, refine-erase, refine-unmap, refine-map,
ubi-abs/absexpt-avols-write is used by refine-write, refine-change,
ubi-abs/absexpt-idset is used by refine-wl-worker, refine-change,
ubi-abs/absexpt-pebs-write is used by refine-write,
ubi-abs/absexpt-vols-write is used by refine-wl-worker, refine-write, refine-change,

Used from specification list

list/erasequeue-base/Last is used by refine-erase, refine-unmap,
list/erasequeue-base/Nil is used by refine-erase-worker,
list/erasequeue-base/a is used by refine-erase-worker, refine-erase, refine-unmap,
list/erasequeue-base/app-02 is used by refine-erase-worker,
list/erasequeue-base/c is used by refine-erase-worker,
list/erasequeue-base/c-07 is used by refine-erase-worker,
list/erasequeue-base/e is used by refine-erase-worker,
list/erasequeue-base/e-01 is used by refine-erase-worker,
list/erasequeue-base/in-15 is used by refine-erase,
list/erasequeue-base/in-17 is used by refine-erase,
list/erasequeue-base/in-append is used by refine-erase,

Used from specification wlentry

wlentry/elim-02 is used by lf-mapped-not-bad, refine-erase-worker, refine-write, refine-read, refine-erase,
wlentry/sel-04 is used by lf-mapped-not-bad, refine-write, refine-read, refine-erase,

Used from specification array-copy

array-copy/buffer/subarray-copy-elim-exact is used by refine-write,
array-copy/buffer/subarray-copy-lower is used by refine-write,
array-copy/buffer/subarray-subarray-elim is used by refine-write,
array-copy/buffer/subarray-zero is used by refine-write,
array-copy/abstract-volume/at-fill-mkarray is used by refine-create-volume,
array-copy/ebatbl/at-fill-mkarray is used by refine-create-volume,
array-copy/apebs/idexcept-size is used by refine-erase-worker,
array-copy/wlarray-base/idexcept-size is used by refine-erase-worker,
array-copy/buffer/size-copy is used by refine-write,
array-copy/abstract-volume/size-fill is used by refine-create-volume,
array-copy/ebatbl/size-fill is used by refine-create-volume,
array-copy/buffer/size-subarray is used by recovery, refine-write,
array-copy/buffer/subarray-at is used by recovery, refine-write,
array-copy/buffer/subarray-elim is used by refine-write, refine-map, refine-change,

Used from specification datasize

datasize/datasize-rec is used by rangeeq-emptyleb-datasize,
datasize/datasize-base is used by rangeeq-emptyleb-datasize,
datasize/datasize-is-smaller-help is used by refine-change,

Used from specification eraseblock

eraseblock/emptyleb-at is used by rangeeq-emptyleb-datasize, emptyleb-mkempbuf, recovery, refine-write,
eraseblock/emptyleb-size is used by rangeeq-emptyleb-datasize, emptyleb-mkempbuf, recovery, refine-write,
eraseblock/lebsize-neq-zero is used by recovery, refine-write,
eraseblock/page-size is used by refine-write, refine-map, refine-change,

Used from specification oelem

oelem/nat-set/irreflexivity is used by recovery, refine-write, refine-read, refine-unmap,

Used from specification array

array/buffer/Extension is used by emptyleb-mkempbuf, recovery, refine-write,
array/ebatbl/Put-same is used by refine-wl-worker, refine-write, refine-change,
array/apebs/Put-same is used by refine-write,
array/abstract-volume/Put-same is used by refine-write, refine-change,
array/ebatbl/Size-mkarray is used by refine-create-volume,
array/buffer/Size-mkarray is used by refine-write, refine-map,
array/abstract-volume/Size-mkarray is used by refine-create-volume,
array/apebs/Size-put is used by refine-write,
array/abstract-volume/Size-put is used by refine-write, refine-change,
array/ebatbl/Size-put is used by refine-wl-worker, refine-write, refine-change,
array/wlarray-base/Size-put is used by refine-erase,
array/apebs/cgetput is used by refine-write,
array/abstract-volume/cputput is used by refine-write,
array/ebatbl/put-same-content is used by refine-erase,

Used from specification ebaentry

ebaentry/disj is used by lf-mapped-data, lf-elim-unmapped, refine-wl-worker, recovery, refine-write, refine-read, refine-erase, refine-unmap, refine-change,
ebaentry/inj is used by lf-elim-unmapped, refine-wl-worker, refine-write, refine-change,
ebaentry/sel is used by lf-mapped-data, refine-wl-worker, recovery, refine-write, refine-read, refine-erase, refine-unmap, refine-change,

Used from specification ubi-crash-recovery-base

ubi-crash-recovery-base/vols-eraseq-bound is used by recovery,
ubi-crash-recovery-base/vols-le is used by recovery,

Used from specification debug

debug/debug is used by refine-write,