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

apeb/elim is used by wlar-erase-worker-helper, delta-wear-leveling,
apeb/sel-04 is used by wlar-erase-worker-helper, delta-wear-leveling,
apeb/sel-05 is used by delta-wear-leveling,
apeb/sel-06 is used by delta-wear-leveling,
apeb/sel-08 is used by wlar-erase-worker-helper, delta-wear-leveling,
apeb/upd-04 is used by wlar-erase-worker-helper,

Used from specification nat-basic

nat-basic/a is used by wlar-erase-worker-helper, delta-wear-leveling, delta-erase-worker-helper,
nat-basic/add-base is used by delta-wear-leveling,
nat-basic/c is used by wlar-erase-worker-helper, delta-wear-leveling, delta-erase-worker-helper,
nat-basic/eq-01 is used by delta-erase-worker-helper,
nat-basic/f is used by wlar-erase-worker-helper, delta-wear-leveling, delta-erase-worker-helper,
nat-basic/l is used by delta-erase-worker-helper,
nat-basic/l-01 is used by delta-erase-worker-helper,
nat-basic/l-06 is used by delta-erase-worker-helper,
nat-basic/lf is used by delta-erase-worker-helper,
nat-basic/lf-01 is used by wlar-erase-worker-helper, delta-wear-leveling, delta-erase-worker-helper,
nat-basic/lf-02 is used by wlar-erase-worker-helper, delta-wear-leveling,
nat-basic/nls-fst is used by delta-erase-worker-helper,
nat-basic/oz is used by wlar-erase-worker-helper,
nat-basic/s-04 is used by wlar-erase-worker-helper,
nat-basic/succ is used by delta-erase-worker-helper,

Used from specification array-splice

array-splice/buffer/append-a is used by delta-wear-leveling,
array-splice/buffer/mkemparray0-append-right is used by delta-wear-leveling,
array-splice/buffer/range-eq-0 is used by delta-wear-leveling,

Used from specification aecheader

aecheader/test-02 is used by wlar-erase-worker-helper,

Used from specification ubi-quality-base

ubi-quality-base/delta-atomic-leb-change is used by delta-wear-leveling,
ubi-quality-base/delta-write is used by delta-erase-worker-helper,
ubi-quality-base/in-delta is used by delta-erase-worker-helper,
ubi-quality-base/in-ecs is used by delta-wear-leveling,
ubi-quality-base/threshold-ge-erase-retries is used by delta-wear-leveling,

Used from specification erasequeue

erasequeue/lebrefs-append-lref is used by delta-wear-leveling,

Used from specification avidheader

avidheader/elim is used by delta-wear-leveling,
avidheader/test-03 is used by delta-wear-leveling,

Used from specification nat

nat/elim-sub is used by delta-erase-worker-helper,
nat/eq-02 is used by delta-erase-worker-helper,
nat/eqle-one is used by wlar-erase-worker-helper,
nat/ge is used by delta-wear-leveling,
nat/le-add is used by delta-wear-leveling,
nat/le-def is used by wlar-erase-worker-helper, delta-wear-leveling, delta-erase-worker-helper,
nat/le-ls-simp is used by delta-erase-worker-helper,
nat/le-one is used by delta-erase-worker-helper,
nat/le-sum is used by wlar-erase-worker-helper,
nat/lels is used by wlar-erase-worker-helper, delta-wear-leveling,
nat/lels-03 is used by delta-erase-worker-helper,
nat/lep is used by wlar-erase-worker-helper,
nat/lep-02 is used by wlar-erase-worker-helper, delta-wear-leveling, delta-erase-worker-helper,
nat/ler is used by wlar-erase-worker-helper, delta-wear-leveling,
nat/les is used by wlar-erase-worker-helper,
nat/let is used by delta-wear-leveling,
nat/lez is used by wlar-erase-worker-helper, delta-wear-leveling,
nat/ls-le-simp is used by wlar-erase-worker-helper, delta-wear-leveling,
nat/zero is used by delta-wear-leveling,

Used from specification store

store/volumes/In-insert is used by delta-wear-leveling,

Used from specification bag-max

bag-max/max-in-ls is used by delta-wear-leveling,

Used from specification error-class

error-class/esuccess is used by wlar-erase-worker-helper, delta-wear-leveling,
error-class/not-esuccess is used by wlar-erase-worker-helper, delta-wear-leveling,

Used from specification error

error/disj-35 is used by delta-wear-leveling,
error/disj-66 is used by wlar-erase-worker-helper,

Used from specification wlarray

wlarray/elim-update-status is used by wlar-erase-worker-helper,

Used from specification set-basic

set-basic/lebrefset/In-insert is used by delta-wear-leveling,
set-basic/lebrefset/sub-add-01 is used by delta-wear-leveling,
set-basic/lebrefset/sub-add-03 is used by delta-wear-leveling,

Used from specification list-last

list-last/erasequeue-base/butlast-def is used by delta-wear-leveling,

Used from specification wlstatus

wlstatus/disj-01 is used by delta-wear-leveling,
wlstatus/disj-02 is used by delta-wear-leveling,
wlstatus/disj-03 is used by delta-wear-leveling,

Used from specification ubi-io-pre

ubi-io-pre/erase-pre is used by wlar-erase-worker-helper,
ubi-io-pre/markbad-pre is used by wlar-erase-worker-helper,
ubi-io-pre/read-data-pre is used by delta-wear-leveling,
ubi-io-pre/read-vidhdr-pre is used by delta-wear-leveling,
ubi-io-pre/write-echdr-pre is used by wlar-erase-worker-helper,

Used from specification valid-peb

valid-peb/valid-peb-leb is used by delta-wear-leveling,
valid-peb/valid-peb-valid-vidhdr is used by delta-wear-leveling,
valid-peb/valid-peb-vol is used by delta-wear-leveling,

Used from specification ubi-asm

ubi-asm/inv-wl-worker is used by delta-wear-leveling,
ubi-asm/prepost-atomic-leb-change is used by delta-wear-leveling,
ubi-asm/prepost-get-pebs-for-wl is used by delta-wear-leveling,
ubi-asm/ubi-io-inv-fwd is used by delta-wear-leveling,

Used from specification ubi-io-inv

ubi-io-inv/peb-inv-size is used by delta-wear-leveling,

Used from specification align

align/alignup-same is used by delta-wear-leveling,

Used from specification ubi-base

ubi-base/valid-ebatbl is used by delta-wear-leveling,
ubi-base/valid-vtbl is used by delta-wear-leveling,
ubi-base/valid-wl is used by delta-wear-leveling,
ubi-base/bitflips-cons-empty is used by delta-wear-leveling,
ubi-base/idset-weaken is used by delta-wear-leveling,
ubi-base/is-vtbl-pnum is used by delta-wear-leveling,
ubi-base/ubi-cons is used by delta-wear-leveling,
ubi-base/valid-vtbl-buf is used by delta-wear-leveling,
ubi-base/valid-vtbl-in-wlar is used by delta-wear-leveling,
ubi-base/valid-vtbl-update-vols is used by delta-wear-leveling,
ubi-base/valid-vtbl-wlar-status is used by delta-wear-leveling,

Used from specification list

list/erasequeue-base/Last is used by delta-wear-leveling,
list/erasequeue-base/a is used by delta-wear-leveling,
list/erasequeue-base/e-02 is used by delta-wear-leveling,
list/erasequeue-base/in-15 is used by delta-wear-leveling,
list/erasequeue-base/in-17 is used by delta-wear-leveling,
list/erasequeue-base/in-append is used by delta-wear-leveling,

Used from specification wlentry

wlentry/elim-02 is used by wlar-erase-worker-helper, delta-wear-leveling, delta-erase-worker-helper,
wlentry/inj-03 is used by delta-wear-leveling, delta-erase-worker-helper,
wlentry/sel-04 is used by delta-wear-leveling,
wlentry/sel-05 is used by wlar-erase-worker-helper, delta-wear-leveling, delta-erase-worker-helper,
wlentry/upd-04 is used by wlar-erase-worker-helper,
wlentry/updsel-02 is used by wlar-erase-worker-helper,

Used from specification array-copy

array-copy/buffer/copy-exact is used by delta-wear-leveling,
array-copy/wlarray-base/idexcept-same is used by wlar-erase-worker-helper,
array-copy/apebs/idexcept-size is used by delta-wear-leveling,
array-copy/wlarray-base/idexcept-write-at0-right is used by wlar-erase-worker-helper,
array-copy/buffer/subarray-elim is used by delta-wear-leveling,

Used from specification eraseblock

eraseblock/lebsize-page-size-is-aligned is used by delta-wear-leveling,
eraseblock/page-size is used by delta-wear-leveling,

Used from specification oelem

oelem/nat-set/irreflexivity is used by wlar-erase-worker-helper,
oelem/nat-set/transitivity is used by delta-erase-worker-helper,

Used from specification array

array/wlarray-base/Put-same is used by wlar-erase-worker-helper,
array/apebs/Put-same is used by wlar-erase-worker-helper,
array/buffer/Size-mkarray is used by delta-wear-leveling,
array/wlarray-base/Size-put is used by wlar-erase-worker-helper,
array/apebs/Size-put is used by wlar-erase-worker-helper,
array/apebs/cputput is used by wlar-erase-worker-helper,
array/wlarray-base/cputput is used by wlar-erase-worker-helper,

Used from specification ebaentry

ebaentry/disj is used by delta-wear-leveling,
ebaentry/sel is used by delta-wear-leveling,

Used from specification debug

debug/debug is used by wlar-erase-worker-helper,