[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 refine-read-data, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
apeb/inj is used by refine-sync-erase, refine-write-echdr,
apeb/sel-04 is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
apeb/sel-05 is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
apeb/sel-06 is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
apeb/sel-07 is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
apeb/sel-08 is used by initial-ex-abstract-initial, refine-read-data, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
apeb/upd-04 is used by refine-write-echdr,
apeb/upd-05 is used by refine-write-vidhdr,
apeb/upd-08 is used by refine-markbad,

Used from specification aecheader

aecheader/disj-02 is used by initial-ex-abstract-initial, refine-write-echdr, refine-read-echdr,
aecheader/disj-03 is used by initial-ex-abstract-initial, refine-write-echdr, refine-read-echdr,
aecheader/elim is used by refine-write-echdr,
aecheader/inj is used by refine-read-echdr,
aecheader/not-garbage-valid-imp-empty is used by refine-read-echdr,
aecheader/sel is used by initial-ex-abstract-initial, refine-write-echdr, refine-read-echdr,
aecheader/test-01 is used by refine-write-echdr,
aecheader/test-02 is used by initial-ex-abstract-initial, refine-write-echdr,

Used from specification array-splice

array-splice/buffer/append-at is used by refine-write-data-wl,
array-splice/buffer/copy2append is used by refine-write-data,
array-splice/buffer/copy2append0 is used by refine-write-data-wl,
array-splice/buffer/range-eq-ext is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data,
array-splice/buffer/range-eq-subarrays is used by refine-write-data-wl, refine-write-echdr,
array-splice/buffer/append-a is used by refine-write-data-wl, refine-write-data,
array-splice/buffer/append-eq-left is used by refine-write-data-wl, refine-write-data,
array-splice/buffer/append-len is used by refine-write-data-wl,
array-splice/buffer/append-zero-left is used by refine-write-data-wl,
array-splice/buffer/emparray-at is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data,
array-splice/buffer/emparray-len is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data,
array-splice/buffer/range-eq-0 is used by refine-read-vidhdr, refine-read-echdr,

Used from specification nat-basic

nat-basic/a is used by initial-ex-abstract-initial, refine-get-leb-size, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat-basic/add-base is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat-basic/c is used by initial-ex-abstract-initial, refine-get-leb-size, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat-basic/eq-02 is used by refine-write-vidhdr,
nat-basic/eqs is used by refine-read-data, refine-write-data-wl, refine-write-data,
nat-basic/f is used by initial-ex-abstract-initial, refine-read-data, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat-basic/l is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data,
nat-basic/l-01 is used by refine-read-data, refine-write-data-wl,
nat-basic/l-02 is used by initial-ex-abstract-initial, refine-write-data,
nat-basic/l-06 is used by refine-read-data, refine-write-data-wl, refine-write-data,
nat-basic/lf is used by initial-ex-abstract-initial, refine-write-data-wl,
nat-basic/lf-01 is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data,
nat-basic/lf-02 is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data,
nat-basic/ls-02 is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data,
nat-basic/neq-01 is used by initial-ex-abstract-initial,
nat-basic/neq-04 is used by initial-ex-abstract-initial,
nat-basic/oz is used by initial-ex-abstract-initial,
nat-basic/ref is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data, refine-read-vidhdr, refine-read-echdr,
nat-basic/s-04 is used by initial-ex-abstract-initial,
nat-basic/succ is used by initial-ex-abstract-initial,
nat-basic/z-01 is used by refine-write-data,
nat-basic/zero is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,
nat-basic/zero-01 is used by initial-ex-abstract-initial, refine-write-data-wl,

Used from specification encoding-page-size-nonempty

encoding-page-size-nonempty/encoding-echeader/decode-contract is used by refine-read-echdr,
encoding-page-size-nonempty/encoding-vidheader/decode-contract is used by refine-read-vidhdr,
encoding-page-size-nonempty/encoding-vidheader/encode-contract is used by refine-write-vidhdr,
encoding-page-size-nonempty/encoding-echeader/encode-contract is used by refine-write-echdr,
encoding-page-size-nonempty/encoding-vidheader/is-encoded-not-garbage-pagesize is used by refine-read-vidhdr,
encoding-page-size-nonempty/encoding-echeader/is-encoded-not-garbage-pagesize is used by refine-read-echdr,
encoding-page-size-nonempty/encoding-echeader/is-encoded-size is used by initial-ex-abstract-initial, refine-write-echdr, refine-read-echdr,
encoding-page-size-nonempty/encoding-vidheader/is-encoded-size is used by refine-write-vidhdr, refine-read-vidhdr,
encoding-page-size-nonempty/encoding-vidheader/is-encoded-unique is used by refine-write-vidhdr, refine-read-vidhdr,
encoding-page-size-nonempty/encoding-echeader/is-encoded-unique is used by initial-ex-abstract-initial, refine-write-echdr, refine-read-echdr,

Used from specification mtd-base

mtd-base/mtd-cons is used by refine-write-data,
mtd-base/mtd-cons-extract is used by refine-write-data-wl, refine-write-echdr,
mtd-base/mtd-cons-peb-size is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
mtd-base/mtd-valid-peb is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data, refine-write-echdr,

Used from specification avidheader

avidheader/disj-01 is used by initial-ex-abstract-initial,
avidheader/disj-02 is used by refine-write-vidhdr,
avidheader/disj-03 is used by refine-write-vidhdr,
avidheader/elim is used by refine-write-vidhdr,
avidheader/not-garbage-valid-imp-empty is used by refine-read-vidhdr,
avidheader/sel-06 is used by refine-write-vidhdr, refine-read-vidhdr,
avidheader/sel-07 is used by refine-write-vidhdr, refine-read-vidhdr,
avidheader/sel-08 is used by refine-write-vidhdr, refine-read-vidhdr,
avidheader/sel-09 is used by refine-write-vidhdr, refine-read-vidhdr,
avidheader/sel-10 is used by refine-write-vidhdr, refine-read-vidhdr,
avidheader/test-01 is used by initial-ex-abstract-initial, refine-write-vidhdr,
avidheader/test-03 is used by refine-write-vidhdr,

Used from specification vidheader

vidheader/elim is used by refine-read-vidhdr,
vidheader/inj is used by refine-read-vidhdr,

Used from specification nat

nat/add-01 is used by refine-read-data, refine-write-data,
nat/anti is used by refine-read-data, refine-write-data,
nat/elim-sub is used by initial-ex-abstract-initial, refine-get-leb-size, refine-read-data, refine-write-data-wl, refine-write-data,
nat/eq is used by initial-ex-abstract-initial,
nat/eq-01 is used by refine-write-data,
nat/fle is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl,
nat/fle-01 is used by initial-ex-abstract-initial, refine-read-data, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat/ge is used by refine-get-leb-size, refine-read-data, refine-write-data-wl, refine-write-data,
nat/le-def is used by refine-get-leb-size, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat/le-ls-simp is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data,
nat/lels is used by initial-ex-abstract-initial, refine-read-data, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat/lels-02 is used by initial-ex-abstract-initial, refine-write-data-wl, refine-read-echdr,
nat/lels-03 is used by refine-read-data, refine-write-data-wl,
nat/lep is used by refine-read-data, refine-write-data-wl, refine-write-data,
nat/lep-02 is used by refine-read-data, refine-write-data,
nat/ler is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat/let is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-echdr, refine-read-echdr,
nat/lez is used by refine-write-data-wl, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat/ls-01 is used by refine-read-data,
nat/ls-02 is used by refine-write-data,
nat/ls-le-simp is used by initial-ex-abstract-initial, refine-read-data, refine-isbad, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
nat/sub-add is used by refine-write-data,
nat/sub-base is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-echdr,
nat/zero is used by refine-read-vidhdr, refine-read-echdr,

Used from specification peb

peb/elim is used by initial-ex-abstract-initial, refine-read-data, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
peb/inj is used by refine-write-data-wl,
peb/sel-05 is used by initial-ex-abstract-initial, refine-read-data, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
peb/sel-06 is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
peb/sel-07 is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
peb/upd-05 is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,
peb/upd-06 is used by refine-markbad,
peb/upd-07 is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,

Used from specification error-class

error-class/ecommit is used by refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,
error-class/esuccess is used by initialization, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
error-class/not-esuccess is used by initialization, refine-read-data, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,

Used from specification error

error/disj-91 is used by refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,

Used from specification ubi-io-pre

ubi-io-pre/erase-pre is used by refine-sync-erase,
ubi-io-pre/isbad-pre is used by refine-isbad,
ubi-io-pre/markbad-pre is used by refine-markbad,
ubi-io-pre/read-data-pre is used by refine-read-data,
ubi-io-pre/read-echdr-pre is used by refine-read-echdr,
ubi-io-pre/read-vidhdr-pre is used by refine-read-vidhdr,
ubi-io-pre/write-data-pre is used by refine-write-data,
ubi-io-pre/write-data-wl-pre is used by refine-write-data-wl,
ubi-io-pre/write-echdr-pre is used by refine-write-echdr,
ubi-io-pre/write-vidhdr-pre is used by refine-write-vidhdr,

Used from specification checksum

checksum/checksum-append-left is used by refine-write-data-wl,

Used from specification ubi-io-inv

ubi-io-inv/initial is used by initial-ex-abstract-initial,
ubi-io-inv/peb-initial is used by initial-ex-abstract-initial,
ubi-io-inv/ubi-io-inv-extract is used by refine-write-vidhdr,
ubi-io-inv/inv-size is used by refine-read-data, refine-write-data,
ubi-io-inv/peb-inv-empty-vidhdr is used by refine-write-vidhdr,
ubi-io-inv/peb-inv-markbad is used by initial-ex-abstract-initial,
ubi-io-inv/peb-inv-write-echdr is used by initial-ex-abstract-initial,

Used from specification ubi-io-abs

ubi-io-abs/abs is used by initial-ex-abstract-initial, refine-write-data-wl,
ubi-io-abs/abs-data-at is used by refine-read-data,
ubi-io-abs/abs-echdr is used by initial-ex-abstract-initial, refine-write-echdr, refine-read-echdr,
ubi-io-abs/abs-peb is used by initial-ex-abstract-initial, refine-markbad, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
ubi-io-abs/abs-vidhdr is used by initial-ex-abstract-initial, refine-write-vidhdr, refine-read-vidhdr,
ubi-io-abs/abs-bad is used by refine-read-data, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
ubi-io-abs/abs-fillcount-empty-echdr is used by refine-write-echdr,
ubi-io-abs/abs-fillcount-empty-vidhdr is used by refine-write-vidhdr,
ubi-io-abs/abs-fillcount-valid-headers is used by refine-write-data-wl, refine-write-data,
ubi-io-abs/abs-fwd is used by refine-read-data, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
ubi-io-abs/abs-peb-empty is used by refine-sync-erase, refine-write-echdr,
ubi-io-abs/abs-reduce is used by refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,
ubi-io-abs/abs-size-apebs0 is used by refine-read-data, refine-isbad, refine-markbad, refine-sync-erase, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
ubi-io-abs/abs-size-apebs1 is used by refine-get-blockcount, refine-write-data-wl,
ubi-io-abs/is-encoded-echeader-emptypage is used by refine-read-echdr,
ubi-io-abs/is-encoded-vidheader-emptypage is used by refine-read-vidhdr,
ubi-io-abs/subarray-emptypeb0 is used by refine-write-echdr,
ubi-io-abs/subarray-emptypeb1 is used by refine-write-echdr,

Used from specification align

align/alignup-is-aligned is used by refine-write-data-wl,
align/alignup-le-is-aligned is used by refine-write-data-wl,
align/alignup-same is used by refine-write-data-wl,
align/is-aligned-add is used by refine-write-data,
align/is-aligned-le-eq-zero is used by refine-write-vidhdr, refine-write-echdr,
align/is-aligned-ls-eq-zero is used by refine-write-vidhdr, refine-write-echdr,
align/is-aligned-multiplier is used by refine-write-data-wl, refine-write-data,
align/is-aligned-same is used by initial-ex-abstract-initial, refine-write-vidhdr, refine-write-echdr,
align/is-aligned-zero is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,

Used from specification array-copy

array-copy/apebs/at-copy is used by initial-ex-abstract-initial,
array-copy/buffer/at-copy is used by refine-write-data-wl,
array-copy/buffer/subarray-at is used by refine-write-data,
array-copy/buffer/subarray-copy is used by refine-write-data-wl, refine-write-data,
array-copy/buffer/subarray-subarray-elim is used by refine-write-data-wl, refine-write-data,
array-copy/buffer/at-copy is used by refine-read-data,
array-copy/buffer/copy-exact is used by refine-write-data-wl,
array-copy/apebs/copy-exact is used by initial-ex-abstract-initial,
array-copy/apebs/size-copy is used by initial-ex-abstract-initial,
array-copy/buffer/size-copy is used by refine-read-data, refine-write-data-wl,
array-copy/buffer/size-subarray is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data, refine-read-vidhdr, refine-read-echdr,
array-copy/pebs/size-subarray is used by initial-ex-abstract-initial,
array-copy/pebs/subarray-at is used by initial-ex-abstract-initial,
array-copy/buffer/subarray-at is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data,
array-copy/buffer/subarray-copy-elim-exact is used by refine-write-vidhdr, refine-write-echdr,
array-copy/buffer/subarray-copy-higher is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr,
array-copy/buffer/subarray-copy-lower is used by refine-write-vidhdr, refine-write-echdr,
array-copy/pebs/subarray-elim is used by initial-ex-abstract-initial,
array-copy/buffer/subarray-elim is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
array-copy/buffer/subarray-zero is used by refine-write-data-wl,

Used from specification datasize

datasize/datasize-base is used by refine-write-data-wl,
datasize/datasize-is-smaller-help is used by refine-write-data-wl,

Used from specification nat-mult

nat-mult/dist-sub-04 is used by refine-write-data-wl,
nat-mult/le-num is used by refine-write-data-wl, refine-write-vidhdr,
nat-mult/mult-a is used by initial-ex-abstract-initial, refine-get-leb-size, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr,
nat-mult/mult-c is used by initial-ex-abstract-initial, refine-get-leb-size, refine-read-data, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr,
nat-mult/neqone is used by refine-write-data-wl,
nat-mult/numeral-28 is used by refine-write-data, refine-write-echdr,
nat-mult/numeral-29 is used by refine-write-data,
nat-mult/one is used by refine-write-data, refine-write-echdr,
nat-mult/two-02 is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr,
nat-mult/two-zero-01 is used by refine-write-data-wl, refine-write-data,
nat-mult/twole-02 is used by refine-write-data-wl, refine-write-echdr,
nat-mult/zero is used by refine-write-data-wl,

Used from specification eraseblock

eraseblock/empbuf-eq-emptypage is used by refine-read-vidhdr, refine-read-echdr,
eraseblock/emptyleb-at is used by refine-write-data-wl,
eraseblock/emptyleb-size is used by refine-write-data-wl,
eraseblock/emptypage-at is used by initial-ex-abstract-initial,
eraseblock/emptypage-size is used by initial-ex-abstract-initial, refine-read-vidhdr, refine-read-echdr,
eraseblock/emptypeb-at is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data,
eraseblock/emptypeb-size is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data, refine-write-echdr,
eraseblock/isempty-empbuf is used by refine-read-vidhdr, refine-read-echdr,
eraseblock/lebsize-2page-size-le is used by refine-write-data,
eraseblock/lebsize-ls-2page-size-pebsize is used by refine-write-data-wl,
eraseblock/lebsize-neq-zero is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data,
eraseblock/lebsize-pebsize is used by initial-ex-abstract-initial, refine-get-leb-size, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,
eraseblock/page-size is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,
eraseblock/page-size-plus-eq-0 is used by refine-write-data, refine-write-echdr,
eraseblock/pebsize-le-2page-size is used by refine-get-leb-size, refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr,
eraseblock/pebsize-le-2page-size-lebsize is used by refine-read-data, refine-write-data-wl, refine-write-data,
eraseblock/pebsize-le-2page-size-n is used by refine-write-data,
eraseblock/pebsize-le-minus-eb-page-size is used by initial-ex-abstract-initial,
eraseblock/pebsize-le-page-size is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr, refine-read-echdr,
eraseblock/pebsize-ls-2page-size-n is used by refine-write-data-wl,
eraseblock/pebsize-minus-2eb-page-size is used by refine-get-leb-size, refine-write-data-wl, refine-write-data,
eraseblock/pebsize-minus-eb-page-size is used by initial-ex-abstract-initial,
eraseblock/subarray-emptypeb-eq-emptyleb is used by refine-write-data-wl, refine-write-echdr,

Used from specification echeader

echeader/elim is used by refine-read-echdr,
echeader/inj is used by refine-read-echdr,

Used from specification array

array/buffer/Extension is used by initial-ex-abstract-initial, refine-read-data, refine-write-data-wl, refine-write-data,
array/apebs/Put-other is used by initial-ex-abstract-initial, refine-write-data-wl,
array/pebs/Put-same is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,
array/apebs/Put-same is used by refine-write-data-wl,
array/apebs/Size-mkarray is used by initial-ex-abstract-initial,
array/buffer/Size-mkarray is used by initial-ex-abstract-initial, refine-write-data-wl, refine-write-vidhdr, refine-read-vidhdr, refine-write-echdr, refine-read-echdr,
array/pebs/Size-put is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,
array/apebs/Size-put is used by initial-ex-abstract-initial, refine-write-data-wl,
array/apebs/cgetput is used by initial-ex-abstract-initial,
array/pebs/cputput is used by refine-write-data-wl, refine-write-data, refine-write-vidhdr, refine-write-echdr,
array/apebs/put-same-content is used by refine-write-vidhdr, refine-write-echdr,

Used from specification ubi-io-asm

ubi-io-asm/inv-format is used by initialization,
ubi-io-asm/inv-io-read is used by refine-read-data, refine-read-vidhdr, refine-read-echdr,

Used from specification ubi-io-base

ubi-io-base/ubi-io-initial is used by initial-ex-abstract-initial,
ubi-io-base/ubi-io-peb-initial is used by initial-ex-abstract-initial,