Used simplifier rules/spec theorems by specification

Used from specification recovery-entry

• recovery-entry/elim is used by prepost-scan-all, prepost-init-vols-sizes, prepost-init-vols-mappings, inv-recover,
• recovery-entry/inj is used by prepost-init-vols-mappings, inv-recover,
• recovery-entry/sel-01 is used by lf-valid-recs-sqns-vidhdr,
• recovery-entry/sel-02 is used by prepost-init-vols-sizes, prepost-init-vols-mappings, lf-valid-recs-valid-peb, lf-valid-recs-sqns-vidhdr, lf-valid-recs-notin-eraseq, lf-valid-recs-max, lf-valid-recs-in-apebs, inv-recover,

Used from specification lebref

• lebref/disj is used by prepost-write-once, prepost-atomic-leb-change,
• lebref/inj is used by prepost-atomic-leb-change,

Used from specification apeb

• apeb/elim is used by valid-peb-write-valid-peb, ubi-is-max-unique, prepost-write-once, prepost-write-multiple, prepost-scan-all, prepost-io-write-data, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-vtbl-info, lf-valid-wl-free-emptyvidhdr, lf-valid-recs-valid-peb, lf-valid-recs-sqns-vidhdr, lf-valid-recs-notin-eraseq, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-mapped-valid-peb, inv-read, inv-write, inv-unmap, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• apeb/inj is used by prepost-scan-all, prepost-init-vols-mappings, inv-format, inv-wl-worker,
• apeb/sel-04 is used by valid-peb-write-valid-peb, ubi-io-inv-fillcount0, prepost-write-once, prepost-scan-all, prepost-io-write-data, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-datasize-wear-level, lf-valid-wl-free-emptyvidhdr, lf-valid-eraseq-stronger-notin-recs, inv-recover, inv-format, inv-wl-worker,
• apeb/sel-05 is used by valid-peb-write-valid-peb, ubi-io-inv-fillcount0, prepost-write-once, prepost-scan-all, prepost-io-write-data, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-datasize-wear-level, lf-valid-wl-free-emptyvidhdr, lf-valid-recs-valid-peb, lf-valid-recs-sqns-vidhdr, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-mapped-valid-peb, inv-recover, inv-format, inv-wl-worker,
• apeb/sel-06 is used by valid-peb-write-valid-peb, ubi-io-inv-fillcount0, prepost-write-once, prepost-write-multiple, prepost-scan-all, prepost-io-write-data, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-atomic-leb-change, ls-datasize-wear-level, lf-valid-wl-free-emptyvidhdr, inv-change, inv-recover, inv-format, inv-wl-worker,
• apeb/sel-07 is used by valid-peb-write-valid-peb, ubi-io-inv-fillcount0, prepost-write-once, prepost-write-multiple, prepost-io-write-data, prepost-atomic-leb-change, ls-datasize-wear-level, lf-valid-wl-free-emptyvidhdr, inv-write, inv-change, inv-format, inv-wl-worker,
• apeb/sel-08 is used by valid-peb-write-valid-peb, ubi-io-inv-fillcount0, prepost-write-once, prepost-scan-all, prepost-io-write-data, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-datasize-wear-level, lf-valid-wl-not-erroneous, lf-valid-wl-free-emptyvidhdr, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, inv-recover, inv-format, inv-wl-worker,
• apeb/upd-04 is used by prepost-erase-worker-helper,
• apeb/upd-05 is used by prepost-write-once, prepost-atomic-leb-change, inv-format,
• apeb/upd-08 is used by prepost-erase-worker-helper,
• apeb/updsel-21 is used by prepost-atomic-leb-change,
• apeb/updsel-26 is used by prepost-atomic-leb-change,

Used from specification array-splice

• array-splice/buffer/append-at1 is used by valid-peb-write-valid-peb, ls-datasize-zero,
• array-splice/buffer/append-at2 is used by valid-peb-write-valid-peb, ls-datasize-zero,
• array-splice/buffer/subarray-split-at is used by ls-subarray-datasize, ls-datasize-wear-level,
• array-splice/buffer/append-a is used by valid-peb-write-valid-peb, prepost-write-once, prepost-write-multiple, prepost-io-write-data, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-zero, ls-datasize-wear-level, ls-datasize-empbuf-append-lower, ls-array-append-length0, inv-change, inv-format, inv-create-volume, inv-wl-worker,
• array-splice/buffer/append-eq-left is used by prepost-write-once, prepost-write-multiple, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-empbuf-append-lower, inv-change,
• array-splice/buffer/append-len is used by valid-peb-write-valid-peb, prepost-io-write-data, prepost-atomic-leb-change, ls-datasize-zero, ls-datasize-wear-level, ls-datasize-empbuf-append-lower,
• array-splice/buffer/append-prefix-left is used by ls-datasize-wear-level,
• array-splice/buffer/append-right-size0 is used by ls-array-append-length0,
• array-splice/buffer/append-zero-left is used by prepost-write-once, prepost-write-multiple, inv-format,
• array-splice/buffer/emparray-at is used by valid-peb-write-valid-peb, subbarray-alignup-datasize-empty, ls-datasize-zero,
• array-splice/buffer/emparray-len is used by valid-peb-write-valid-peb, subbarray-alignup-datasize-empty, prepost-write-once, prepost-write-multiple, prepost-io-write-data, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-zero, ls-datasize-empbuf-append-lower,
• array-splice/buffer/mkemparray-append is used by prepost-write-once, prepost-write-multiple, prepost-atomic-leb-change, ls-subarray-datasize,
• array-splice/buffer/mkemparray-eq is used by ls-subarray-datasize,
• array-splice/buffer/mkemparray0-append-right is used by inv-format, inv-create-volume, inv-wl-worker,
• array-splice/buffer/range-eq-0 is used by prepost-scan-all, inv-write, inv-recover, inv-wl-worker,
• array-splice/buffer/range-eq-refl is used by inv-read, inv-write,
• array-splice/buffer/subarray-append-elim-left is used by ls-datasize-wear-level,
• array-splice/buffer/subarray-append-left is used by valid-peb-write-valid-peb, prepost-atomic-leb-change,
• array-splice/buffer/subarray-same-ar-eq is used by prepost-atomic-leb-change,

Used from specification nat-basic

• nat-basic/a is used by valid-peb-write-valid-peb, subbarray-alignup-datasize-empty, prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-get-peb, prepost-fix-ecs, prepost-erase-worker-helper, prepost-atomic-leb-change, nat-sum-leq, ls-subarray-datasize, ls-datasize-zero, ls-datasize-wear-level, ls-datasize-empbuf-append-lower, ls-add2-add2-samelimit, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-recs-in-apebs, lf-cmp-peb, inv-erase-all, inv-read, inv-write, inv-map, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• nat-basic/add-base is used by valid-peb-write-valid-peb, prepost-write-once, prepost-write-multiple, prepost-scan-all, prepost-io-write-data, prepost-atomic-leb-change, nat-sum-leq, ls-subarray-datasize, ls-datasize-wear-level, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-recs-in-apebs, inv-read, inv-write, inv-recover, inv-format, inv-wl-worker,
• nat-basic/c is used by valid-peb-write-valid-peb, subbarray-alignup-datasize-empty, prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-get-peb, prepost-fix-ecs, prepost-erase-worker-helper, prepost-atomic-leb-change, nat-sum-leq, ls-subarray-datasize, ls-datasize-zero, ls-datasize-wear-level, ls-datasize-empbuf-append-lower, ls-add2-add2-samelimit, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-recs-in-apebs, lf-cmp-peb, inv-erase-all, inv-read, inv-write, inv-map, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• nat-basic/eq-01 is used by prepost-write-once, ls-subarray-datasize, ls-add2-add2-samelimit, inv-write,
• nat-basic/eq-02 is used by prepost-write-multiple, prepost-atomic-leb-change, inv-format,
• nat-basic/eqs is used by valid-peb-write-valid-peb, prepost-write-once, prepost-write-multiple, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-wear-level, inv-change,
• nat-basic/f is used by valid-peb-write-valid-peb, ubi-io-inv-fwd, ubi-io-inv-fillcount0, subbarray-alignup-datasize-empty, prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-get-peb, prepost-fix-ecs, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-zero, ls-datasize-wear-level, lf-vtbl-info, lf-valid-wl-not-erroneous, lf-valid-wl-free-emptyvidhdr, lf-valid-wl-bad, lf-valid-recs-valid-peb, lf-valid-recs-sqns-vidhdr, lf-valid-recs-notin-eraseq, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-used-valid-peb, lf-used-info, lf-mapped-valid-peb, lf-mapped-info, lf-cmp-peb, inv-erase-all, inv-read, inv-write, inv-unmap, inv-erase, inv-map, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker, inv-erase-worker,
• nat-basic/l is used by valid-peb-write-valid-peb, prepost-scan-all, prepost-erase-worker-helper, ls-subarray-datasize, ls-datasize-zero, lf-cmp-peb, inv-format, inv-create-volume,
• nat-basic/l-01 is used by valid-peb-write-valid-peb, prepost-write-once, prepost-write-multiple, prepost-scan-all, prepost-io-write-data, prepost-get-pebs-for-wl, prepost-get-peb, ls-datasize-zero, lf-cmp-peb, inv-format,
• nat-basic/l-02 is used by valid-peb-write-valid-peb, prepost-write-once, prepost-write-multiple, prepost-scan-all, ls-datasize-empbuf-append-lower, inv-write,
• nat-basic/l-05 is used by inv-read,
• nat-basic/l-06 is used by valid-peb-write-valid-peb, subbarray-alignup-datasize-empty,
• nat-basic/lf is used by prepost-wl-get-used-min, prepost-wl-free-max-below, prepost-scan-all,
• nat-basic/lf-01 is used by valid-peb-write-valid-peb, prepost-write-once, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-zero, ls-datasize-wear-level, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, inv-erase-all, inv-read, inv-write, inv-unmap, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker, inv-erase-worker,
• nat-basic/lf-02 is used by prepost-write-multiple, prepost-wl-free-max-below, prepost-scan-all, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-wear-level, lf-mapped-valid-peb, lf-mapped-info, inv-read, inv-recover, inv-wl-worker,
• nat-basic/ls-02 is used by prepost-wl-get-used-min, prepost-scan-all, inv-format,
• nat-basic/neq-03 is used by prepost-scan-all,
• nat-basic/one-01 is used by prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-fix-ecs,
• nat-basic/oz is used by prepost-erase-worker-helper,
• nat-basic/s-04 is used by prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-fix-ecs, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-erase-all, inv-format,
• nat-basic/succ is used by prepost-write-multiple, prepost-wl-get-used-min, prepost-scan-all, inv-erase-all,
• nat-basic/succ-03 is used by prepost-scan-all,
• nat-basic/zero is used by prepost-write-once, prepost-io-write-data, prepost-atomic-leb-change, inv-format,
• nat-basic/zero-01 is used by inv-erase-all, inv-format,

Used from specification list-set

• list-set/erasequeue-base/subset-append is used by prepost-init-vols-mappings,
• list-set/erasequeue-base/subset-empty is used by inv-create-volume,
• list-set/erasequeue-base/subset-rec is used by inv-erase-all,
• list-set/erasequeue-base/subset-ref is used by prepost-init-vols-mappings, inv-erase-all,

Used from specification aecheader

• aecheader/disj-02 is used by lf-valid-wl-free-emptyvidhdr,
• aecheader/disj-03 is used by lf-valid-wl-free-emptyvidhdr,
• aecheader/elim is used by prepost-write-once, prepost-scan-all, prepost-atomic-leb-change, inv-format,
• aecheader/inj is used by prepost-erase-worker-helper, inv-recover,
• aecheader/sel is used by prepost-scan-all, inv-format,
• aecheader/test-01 is used by prepost-erase-worker-helper,
• aecheader/test-02 is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-valid-wl-free-emptyvidhdr, inv-format,

Used from specification erasequeue

• erasequeue/in-append is used by prepost-init-vols-mappings, prepost-atomic-leb-change,
• erasequeue/in-append is used by prepost-atomic-leb-change, inv-wl-worker,
• erasequeue/in-append-other is used by prepost-atomic-leb-change, inv-wl-worker,
• erasequeue/in-concat is used by prepost-get-peb, prepost-erase-worker-helper, inv-erase-all, inv-erase-worker,
• erasequeue/in-empty is used by prepost-get-peb, inv-format, inv-create-volume, inv-erase-worker,
• erasequeue/in-prepend is used by prepost-erase-worker-helper,
• erasequeue/in-prepend-other is used by prepost-get-peb, prepost-erase-worker-helper, inv-erase-all, inv-erase-worker,
• erasequeue/in-single is used by prepost-get-peb, inv-erase-all, inv-erase-worker,
• erasequeue/lebrefs-append-lref is used by prepost-write-once, prepost-atomic-leb-change, inv-wl-worker,
• erasequeue/lebrefs-append-none is used by prepost-write-once, prepost-atomic-leb-change,
• erasequeue/lebrefs-base is used by prepost-get-peb, inv-create-volume,
• erasequeue/lebrefs-lref is used by inv-create-volume,
• erasequeue/lebrefs-rec is used by prepost-get-peb,
• erasequeue/subseteq-lebrefs-subseteq is used by inv-create-volume,

Used from specification ubi-crash-recovery-base

• ubi-crash-recovery-base/disj is used by prepost-init-vols-mappings,
• ubi-crash-recovery-base/indices-set-erasing is used by prepost-scan-all,
• ubi-crash-recovery-base/unmapped-vols is used by prepost-init-vols-sizes,
• ubi-crash-recovery-base/valid-eraseq-map-indices-nostatchange is used by inv-recover,
• ubi-crash-recovery-base/valid-eraseq-strong-notinvols is used by prepost-init-vols-mappings,
• ubi-crash-recovery-base/valid-eraseq-stronger-next-append-lref is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-eraseq-stronger-next-append-none is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-eraseq-stronger-no-maxsqnum is used by lf-valid-eraseq-stronger-notin-recs, inv-recover,
• ubi-crash-recovery-base/valid-eraseq-stronger-prev-append-lref is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-recs is used by prepost-init-vols-sizes, prepost-init-vols-mappings, lf-valid-recs-valid-peb, lf-valid-recs-notin-eraseq, lf-valid-recs-max, lf-valid-recs-in-apebs, lf-valid-eraseq-stronger-notin-recs, inv-recover,
• ubi-crash-recovery-base/valid-recs-sqns is used by lf-valid-recs-sqns-vidhdr,
• ubi-crash-recovery-base/valid-vtbl-weak is used by prepost-init-vols-sizes, inv-recover,
• ubi-crash-recovery-base/valid-wl-map-indices is used by inv-recover,
• ubi-crash-recovery-base/vols-eraseq-bound is used by inv-recover,
• ubi-crash-recovery-base/vols-is-max-is-max-vols is used by ubi-is-max-unique, inv-recover,
• ubi-crash-recovery-base/vols-is-max-is-min-eraseq is used by inv-recover,
• ubi-crash-recovery-base/vols-is-max-weak is used by ubi-is-max-unique, inv-recover,
• ubi-crash-recovery-base/disj-remove is used by prepost-init-vols-mappings,
• ubi-crash-recovery-base/disj-shift is used by prepost-init-vols-mappings,
• ubi-crash-recovery-base/indices-erasing-at is used by inv-recover,
• ubi-crash-recovery-base/indices-erasing-base is used by prepost-scan-all,
• ubi-crash-recovery-base/indices-erasing-eraseq is used by inv-recover,
• ubi-crash-recovery-base/indices-erasing-rec is used by prepost-scan-all,
• ubi-crash-recovery-base/indices-erasing-write-notin is used by prepost-scan-all,
• ubi-crash-recovery-base/scan-all-inv is used by prepost-scan-all, inv-recover,
• ubi-crash-recovery-base/ubi-io-initial-unique-sqns is used by inv-format,
• ubi-crash-recovery-base/ubi-io-initial-valid-sqns is used by inv-format,
• ubi-crash-recovery-base/unmapped-vols-disj is used by prepost-init-vols-mappings,
• ubi-crash-recovery-base/unmapped-vols-unmapped is used by prepost-init-vols-mappings,
• ubi-crash-recovery-base/valid-eraseq-strong-imp-p is used by ubi-is-max-unique, inv-recover,
• ubi-crash-recovery-base/valid-eraseq-strong-imp-q is used by ubi-is-max-unique, inv-recover,
• ubi-crash-recovery-base/valid-eraseq-stronger-base is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-eraseq-stronger-imp-strong is used by prepost-init-vols-mappings,
• ubi-crash-recovery-base/valid-eraseq-stronger-next is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-recs-emptyset is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-recs-in-nonempty-sqns is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-recs-next-add is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-recs-next-samerecs is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-recs-next-update is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-recs-sqns-emptyset is used by prepost-scan-all,
• ubi-crash-recovery-base/valid-recs-sqns-update is used by prepost-scan-all,
• ubi-crash-recovery-base/vols-le-antisym is used by ubi-is-max-unique,

Used from specification bag-union

• bag-union/nat-bag/diff-empty is used by prepost-write-once, prepost-atomic-leb-change,
• bag-union/nat-bag/diff-empty1 is used by inv-format,
• bag-union/nat-bag/in-emp is used by inv-format,
• bag-union/nat-bag/union-ass is used by prepost-scan-all, inv-format,
• bag-union/nat-bag/union-com is used by prepost-scan-all, inv-format,
• bag-union/nat-bag/union-empty is used by inv-format,

Used from specification avidheader

• avidheader/disj-02 is used by valid-peb-write-valid-peb, prepost-scan-all,
• avidheader/elim is used by prepost-scan-all, prepost-init-vols-mappings, inv-wl-worker,
• avidheader/inj is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-atomic-leb-change,
• avidheader/sel-06 is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-format,
• avidheader/sel-07 is used by prepost-scan-all,
• avidheader/sel-08 is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-format,
• avidheader/sel-09 is used by prepost-scan-all,
• avidheader/sel-10 is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-format,
• avidheader/test-03 is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-format, inv-wl-worker,
• avidheader/upd-06 is used by prepost-atomic-leb-change,

Used from specification nat

• nat/le-addex is used by lf-cmp-peb,
• nat/add-01 is used by valid-peb-write-valid-peb, prepost-write-multiple, prepost-erase-worker-helper,
• nat/anti is used by prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, inv-format, inv-wl-worker,
• nat/cancel-01 is used by prepost-write-multiple,
• nat/elim-sub is used by valid-peb-write-valid-peb, prepost-write-once, prepost-write-multiple, prepost-scan-all, prepost-io-write-data, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-zero, ls-datasize-wear-level, inv-read, inv-change, inv-format,
• nat/eq-01 is used by inv-write,
• nat/eq-02 is used by prepost-write-multiple,
• nat/eqle-one is used by prepost-erase-worker-helper,
• nat/fle is used by valid-peb-write-valid-peb, prepost-write-once, prepost-wl-get-used-min, prepost-scan-all, prepost-get-pebs-for-wl, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-valid-recs-valid-peb, lf-valid-recs-max, inv-recover, inv-format,
• nat/fle-01 is used by valid-peb-write-valid-peb, prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-scan-all, prepost-io-write-data, prepost-get-peb, prepost-fix-ecs, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-zero, lf-valid-eraseq-stronger-notin-recs, lf-cmp-peb, inv-read, inv-write, inv-format, inv-create-volume,
• nat/ge is used by valid-peb-write-valid-peb, prepost-write-once, prepost-scan-all, prepost-io-write-data, prepost-get-pebs-for-wl, prepost-atomic-leb-change, ls-datasize-wear-level, inv-read, inv-write, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• nat/gr-def is used by prepost-write-once, prepost-wl-free-max-below, prepost-scan-all, prepost-init-vols-mappings, prepost-atomic-leb-change, ls-valid-global-sqn-vtbl, ls-max, inv-format, inv-create-volume,
• nat/le is used by prepost-write-multiple,
• nat/le-add is used by prepost-scan-all, nat-sum-leq, inv-format,
• nat/le-def is used by valid-peb-write-valid-peb, subbarray-alignup-datasize-empty, prepost-write-once, prepost-write-multiple, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-fix-ecs, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-wear-level, ls-datasize-empbuf-append-lower, lf-valid-recs-valid-peb, lf-valid-recs-max, inv-read, inv-write, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• nat/le-ls-simp is used by valid-peb-write-valid-peb, prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-valid-global-sqn-vtbl, ls-datasize-wear-level, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-recs-in-apebs, lf-valid-eraseq-stronger-notin-recs, inv-read, inv-write, inv-recover, inv-format,
• nat/le-sum is used by prepost-erase-worker-helper,
• nat/lels is used by valid-peb-write-valid-peb, ubi-io-inv-fillcount0, prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-get-peb, prepost-fix-ecs, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-zero, ls-datasize-wear-level, lf-valid-wl-free-emptyvidhdr, lf-valid-recs-in-apebs, lf-valid-eraseq-stronger-notin-recs, lf-valid-eraseq-middle-wlar, inv-erase-all, inv-read, inv-write, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker, inv-erase-worker,
• nat/lels-02 is used by prepost-write-multiple, prepost-wl-free-max-below, prepost-io-write-data, prepost-atomic-leb-change, ls-subarray-datasize, inv-format,
• nat/lels-03 is used by valid-peb-write-valid-peb, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, inv-format,
• nat/lep is used by valid-peb-write-valid-peb, prepost-scan-all, prepost-atomic-leb-change, ls-datasize-zero, inv-write,
• nat/lep-02 is used by valid-peb-write-valid-peb, prepost-write-multiple, prepost-erase-worker-helper, inv-write, inv-format,
• nat/ler is used by subbarray-alignup-datasize-empty, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-atomic-leb-change, nat-sum-leq, ls-subarray-datasize, ls-datasize-wear-level, inv-read, inv-write, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• nat/les is used by prepost-erase-worker-helper,
• nat/let is used by valid-peb-write-valid-peb, prepost-io-write-data, prepost-atomic-leb-change, ls-subarray-datasize, inv-write, inv-format, inv-create-volume,
• nat/lez is used by ubi-io-inv-fillcount0, prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-erase-worker-helper, inv-write, inv-map, inv-recover, inv-format, inv-wl-worker,
• nat/lez-01 is used by prepost-write-once, prepost-atomic-leb-change, inv-format,
• nat/ls-01 is used by prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-fix-ecs, prepost-erase-worker-helper, inv-format,
• nat/ls-02 is used by prepost-write-once, prepost-write-multiple, prepost-io-write-data,
• nat/ls-03 is used by ls-datasize-wear-level,
• nat/ls-le-simp is used by valid-peb-write-valid-peb, ubi-io-inv-fillcount0, prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, prepost-get-peb, prepost-fix-ecs, prepost-atomic-leb-change, ls-datasize-zero, lf-valid-wl-free-emptyvidhdr, inv-read, inv-write, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• nat/pred-03 is used by prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-fix-ecs,
• nat/prop-07 is used by prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below,
• nat/sub-add is used by valid-peb-write-valid-peb,
• nat/sub-base is used by ubi-io-inv-fillcount0, inv-format,
• nat/succ-01 is used by prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, inv-format,
• nat/zero is used by valid-peb-write-valid-peb, prepost-scan-all, ls-datasize-wear-level, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• nat/zero-02 is used by prepost-write-multiple,

Used from specification min-max

• min-max/min-comm is used by ls-datasize-wear-level,
• min-max/min-le-left is used by ls-datasize-wear-level,
• min-max/min-same is used by valid-peb-write-valid-peb,

Used from specification store

• store/vtbl/Extension is used by prepost-init-vols-sizes,
• store/recovery-entries/Extension is used by prepost-init-vols-mappings,
• store/vtbl/Size-insert is used by inv-create-volume,
• store/volumes/At-in-out is used by prepost-init-vols-sizes,
• store/volumes/At-other is used by prepost-init-vols-sizes, prepost-init-vols-mappings,
• store/volumes/At-same is used by prepost-write-multiple, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-create-volume,
• store/recovery-entries/Del-at is used by prepost-init-vols-mappings,
• store/recovery-entries/Del-in is used by prepost-init-vols-mappings,
• store/vtbl/In-empty is used by prepost-init-vols-sizes,
• store/recovery-entries/In-empty is used by prepost-init-vols-mappings,
• store/volumes/In-empty is used by prepost-init-vols-sizes, inv-format,
• store/volumes/In-insert is used by prepost-write-once, prepost-write-multiple, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-unmap, inv-change, inv-create-volume, inv-wl-worker,
• store/vtbl/Size-empty is used by inv-format,
• store/recovery-entries/empty is used by prepost-init-vols-mappings,
• store/vtbl/empty is used by prepost-init-vols-sizes, inv-create-volume,
• store/volumes/in-neq is used by prepost-init-vols-sizes, prepost-init-vols-mappings, inv-create-volume,
• store/volumes/inj-put is used by inv-create-volume,
• store/volumes/ins-same-01 is used by prepost-atomic-leb-change,
• store/volumes/insin is used by prepost-write-multiple, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-atomic-leb-change,
• store/volumes/insins is used by prepost-init-vols-sizes, inv-create-volume,
• store/vtbl/neq is used by inv-create-volume,
• store/vtbl/notmemlookup is used by prepost-init-vols-sizes,
• store/recovery-entries/notmemlookup is used by prepost-init-vols-mappings,
• store/recovery-entries/size is used by prepost-init-vols-mappings,
• store/vtbl/size is used by prepost-init-vols-sizes,

Used from specification set-union

• set-union/nat-set/del-in is used by inv-wl-worker,
• set-union/nat-set/Delete is used by prepost-init-vols-mappings, prepost-atomic-leb-change, inv-unmap, inv-wl-worker,
• set-union/lebrefset/One is used by prepost-get-peb, inv-create-volume,
• set-union/nat-set/del-addeq-05 is used by prepost-scan-all, inv-wl-worker,
• set-union/nat-set/delete-insert is used by prepost-wl-free-max-below,
• set-union/nat-set/int-a is used by prepost-write-multiple, inv-erase-all, inv-change, inv-create-volume, inv-wl-worker,
• set-union/nat-set/int-c is used by prepost-write-multiple, inv-erase-all, inv-change, inv-create-volume, inv-wl-worker,
• set-union/nat-set/int-idem is used by prepost-write-multiple, inv-erase-all, inv-change, inv-create-volume, inv-wl-worker,
• set-union/lebrefset/subset-union-left-rem is used by prepost-get-peb,
• set-union/lebrefset/una is used by prepost-get-peb,
• set-union/lebrefset/unc is used by prepost-get-peb,
• set-union/lebrefset/unsub is used by prepost-get-peb,

Used from specification error-class

• error-class/ecommit is used by prepost-scan-all, prepost-erase-worker-helper, inv-read, inv-write, inv-recover, inv-format, inv-wl-worker,
• error-class/einval is used by inv-recover, inv-create-volume,
• error-class/eio is used by prepost-write-multiple,
• error-class/enospc is used by prepost-get-peb, inv-format, inv-create-volume,
• error-class/esuccess is used by prepost-write-once, prepost-scan-all, prepost-io-write-data, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-read, inv-write, inv-recover, inv-format, inv-wl-worker,
• error-class/not-esuccess is used by prepost-write-once, prepost-write-multiple, prepost-scan-all, prepost-io-write-data, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-erase-all, inv-read, inv-write, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker, inv-erase-worker,

Used from specification bag-max

• bag-max/bag-add-nonempty is used by prepost-init-vols-mappings,
• bag-max/bag-single-max is used by inv-format,
• bag-max/bag-union-one is used by prepost-scan-all,
• bag-max/unique-elems-addtwice is used by prepost-init-vols-mappings,

Used from specification error

• error/disj-35 is used by prepost-get-peb, inv-format, inv-create-volume,
• error/disj-66 is used by prepost-write-multiple, prepost-erase-worker-helper,
• error/disj-78 is used by inv-recover, inv-create-volume,
• error/disj-91 is used by prepost-scan-all, prepost-erase-worker-helper, inv-read, inv-write, inv-recover, inv-format, inv-wl-worker,

Used from specification encoding-fixed-size

• encoding-fixed-size/encoding-nat/encoding-requires-space is used by inv-format,

Used from specification set-basic

• set-basic/nat-set/Extension is used by prepost-wl-free-max-below, prepost-get-pebs-for-wl,
• set-basic/nat-set/In-empty is used by prepost-wl-free-max-below, prepost-get-pebs-for-wl,
• set-basic/nat-set/In-insert is used by inv-wl-worker,
• set-basic/lebrefset/In-insert is used by inv-wl-worker,
• set-basic/lebrefset/add is used by prepost-write-multiple,
• set-basic/lebrefset/in-04 is used by inv-create-volume,
• set-basic/nat-set/ne is used by prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below,
• set-basic/nat-set/ne-01 is used by prepost-get-pebs-for-wl, inv-recover,
• set-basic/nat-set/size-zero is used by prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-get-pebs-for-wl, prepost-get-peb,
• set-basic/nat-set/size-zero-01 is used by prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-get-pebs-for-wl, prepost-get-peb, inv-recover, inv-wl-worker,
• set-basic/lebrefset/sub-add-01 is used by prepost-write-multiple, prepost-atomic-leb-change, inv-wl-worker,
• set-basic/lebrefset/sub-add-03 is used by prepost-write-multiple, inv-wl-worker,
• set-basic/lebrefset/sub-add-04 is used by prepost-write-once, inv-change,
• set-basic/lebrefset/sub-e is used by prepost-get-peb, inv-create-volume,
• set-basic/lebrefset/sub-idem is used by prepost-write-multiple, prepost-get-peb, inv-create-volume,
• set-basic/lebrefset/sub-insert-01 is used by prepost-write-once, prepost-write-multiple,
• set-basic/lebrefset/sub-ntrans is used by prepost-write-multiple, inv-change,
• set-basic/lebrefset/sub-ntrans-01 is used by prepost-write-multiple,
• set-basic/lebrefset/sub-one-02 is used by inv-create-volume,
• set-basic/lebrefset/sub-trans is used by prepost-write-multiple,
• set-basic/lebrefset/subset-empty is used by inv-create-volume,
• set-basic/lebrefset/subset-insert-same is used by prepost-atomic-leb-change, inv-wl-worker,

Used from specification wlarray

• wlarray/below-nonempty is used by prepost-get-pebs-for-wl,
• wlarray/below-rec is used by prepost-wl-free-max-below,
• wlarray/free-ecs is used by prepost-wl-get-free-min, prepost-wl-free-max-below,
• wlarray/free-ecs-rec is used by prepost-wl-get-free-min, prepost-wl-free-max-below,
• wlarray/in-free-h is used by prepost-wl-free-max-below,
• wlarray/used-ecs is used by prepost-wl-get-used-min,
• wlarray/used-ecs-rec is used by prepost-wl-get-used-min,
• wlarray/below-base is used by prepost-wl-free-max-below,
• wlarray/below-rem-in is used by prepost-wl-free-max-below,
• wlarray/below-rem-notin is used by prepost-wl-free-max-below,
• wlarray/elim-update-status is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-unmap, inv-format,
• wlarray/free-ecs-base is used by prepost-wl-get-free-min, prepost-wl-free-max-below,
• wlarray/in-below is used by prepost-wl-free-max-below,
• wlarray/in-free is used by prepost-get-pebs-for-wl, prepost-get-peb,
• wlarray/used-ecs-base is used by prepost-wl-get-used-min,

Used from specification list-last

• list-last/erasequeue-base/butlast-def is used by inv-wl-worker,

Used from specification wlstatus

• wlstatus/disj-01 is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-valid-wl-free-emptyvidhdr, lf-valid-vtbl-neq-free, lf-valid-eraseq-stronger-notin-recs, lf-mapped-valid-peb, inv-recover, inv-format, inv-wl-worker,
• wlstatus/disj-02 is used by prepost-scan-all, prepost-io-write-data, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-used-valid-peb, lf-mapped-valid-peb, inv-read, inv-write, inv-unmap, inv-recover, inv-format, inv-wl-worker,
• wlstatus/disj-03 is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-valid-vtbl-neq-erasing, lf-valid-recs-notin-eraseq, lf-valid-eraseq-stronger-notin-recs, lf-used-info, lf-mapped-valid-peb, inv-unmap, inv-recover, inv-format, inv-wl-worker,
• wlstatus/disj-04 is used by prepost-write-once, prepost-get-peb, prepost-atomic-leb-change, lf-valid-wl-free-emptyvidhdr, inv-change, inv-format, inv-create-volume, inv-wl-worker,
• wlstatus/disj-05 is used by prepost-write-once, prepost-scan-all, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-valid-wl-free-emptyvidhdr, lf-valid-eraseq-stronger-notin-recs, inv-recover, inv-format,
• wlstatus/disj-06 is used by prepost-scan-all, prepost-erase-worker-helper, lf-valid-eraseq-stronger-notin-recs, inv-recover, inv-format,

Used from specification buffer

• buffer/subarray-mkempbuf-leq is used by prepost-write-once, prepost-atomic-leb-change,

Used from specification valid-peb

• valid-peb/valid-peb0 is used by valid-peb-write-valid-peb, prepost-scan-all, prepost-atomic-leb-change,
• valid-peb/valid-peb0-write-append is used by prepost-io-write-data,
• valid-peb/valid-peb2 is used by valid-peb-write-valid-peb, prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-format,
• valid-peb/not-valid-peb2-explicit-0 is used by prepost-write-once, prepost-scan-all, prepost-atomic-leb-change, inv-format,
• valid-peb/valid-peb-bad is used by lf-valid-eraseq-stronger-notin-recs,
• valid-peb/valid-peb-imp-valid-peb0 is used by lf-used-valid-peb,
• valid-peb/valid-peb-leb is used by prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-atomic-leb-change, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-mapped-valid-peb, inv-unmap, inv-recover, inv-wl-worker,
• valid-peb/valid-peb-unique is used by prepost-scan-all, prepost-init-vols-mappings, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-mapped-valid-peb, inv-write, inv-recover, inv-format, inv-wl-worker,
• valid-peb/valid-peb-valid-vidhdr is used by inv-recover,
• valid-peb/valid-peb-vidhdr-empty is used by prepost-write-once, prepost-atomic-leb-change, lf-valid-eraseq-stronger-notin-recs, inv-recover,
• valid-peb/valid-peb-vol is used by prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-atomic-leb-change, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-mapped-valid-peb, inv-unmap, inv-recover, inv-wl-worker,
• valid-peb/valid-peb0-bad is used by valid-peb-write-valid-peb, prepost-scan-all, prepost-erase-worker-helper,
• valid-peb/valid-peb0-imp-valid-peb is used by prepost-scan-all, prepost-init-vols-mappings, prepost-atomic-leb-change,
• valid-peb/valid-peb0-invalid-ehdr is used by prepost-scan-all, prepost-io-write-data,
• valid-peb/valid-peb0-invalid-vhdr is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change,
• valid-peb/valid-peb0-valid-vidhdr is used by prepost-io-write-data, inv-wl-worker,
• valid-peb/valid-peb0-vidhdr-empty is used by valid-peb-write-valid-peb, prepost-write-once, prepost-scan-all, prepost-erase-worker-helper, prepost-atomic-leb-change,

Used from specification lebadress

• lebadress/elim is used by prepost-init-vols-mappings,
• lebadress/inj is used by prepost-init-vols-mappings,
• lebadress/sel-01 is used by prepost-scan-all, prepost-init-vols-sizes, prepost-init-vols-mappings, lf-valid-recs-valid-peb, lf-valid-recs-notin-eraseq, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, inv-recover,
• lebadress/sel-02 is used by prepost-scan-all, prepost-init-vols-sizes, prepost-init-vols-mappings, lf-valid-recs-valid-peb, lf-valid-recs-notin-eraseq, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, inv-recover,

Used from specification ubi-io-pre

• ubi-io-pre/erase-pre is used by prepost-erase-worker-helper,
• ubi-io-pre/isbad-pre is used by prepost-scan-all, inv-format,
• ubi-io-pre/markbad-pre is used by prepost-erase-worker-helper,
• ubi-io-pre/read-data-pre is used by prepost-scan-all, inv-read, inv-write, inv-recover, inv-wl-worker,
• ubi-io-pre/read-echdr-pre is used by prepost-scan-all, inv-format,
• ubi-io-pre/read-vidhdr-pre is used by prepost-scan-all, inv-wl-worker,
• ubi-io-pre/write-data-pre is used by prepost-write-once, prepost-io-write-data, inv-format,
• ubi-io-pre/write-data-wl-pre is used by prepost-atomic-leb-change,
• ubi-io-pre/write-echdr-pre is used by prepost-erase-worker-helper,
• ubi-io-pre/write-vidhdr-pre is used by prepost-write-once, prepost-atomic-leb-change, inv-format,

Used from specification sqns

• sqns/valid-sqns-extract2-sqn is used by prepost-init-vols-mappings,
• sqns/valid-sqns-nonempty-extract-max is used by lf-valid-eraseq-stronger-notin-recs,
• sqns/valid-sqns-write is used by inv-format,
• sqns/valid-peb-sqns-nonempty is used by prepost-atomic-leb-change, lf-valid-eraseq-stronger-notin-recs,
• sqns/valid-sqns-rec is used by prepost-scan-all,
• sqns/valid-sqns-subarray is used by prepost-scan-all, lf-valid-recs-valid-peb, lf-valid-recs-max,

Used from specification checksum

• checksum/checksum-append-left is used by valid-peb-write-valid-peb, prepost-atomic-leb-change,
• checksum/checksum-prefix is used by prepost-atomic-leb-change,

Used from specification list-data

• list-data/nat-list-set/elim-list-c is used by prepost-fix-ecs,
• list-data/erasequeue-base/elim-list-c is used by prepost-get-peb, inv-erase-all, inv-erase-worker,
• list-data/nat-list-set/l is used by prepost-fix-ecs,
• list-data/nat-list-set/length-rest is used by prepost-fix-ecs,

Used from specification ubi-io-inv

• ubi-io-inv/initial is used by inv-format,
• ubi-io-inv/inv is used by valid-peb-write-valid-peb, ubi-io-inv-fwd, ubi-io-inv-fillcount0, lf-valid-wl-free-emptyvidhdr,
• ubi-io-inv/peb-initial is used by inv-format,
• ubi-io-inv/peb-inv is used by valid-peb-write-valid-peb, ubi-io-inv-fillcount0, ls-datasize-wear-level, lf-valid-wl-free-emptyvidhdr,
• ubi-io-inv/inv-size is used by inv-create-volume,
• ubi-io-inv/peb-inv-empty-vidhdr is used by prepost-write-once, prepost-get-peb, prepost-atomic-leb-change, inv-change, inv-format, inv-create-volume, inv-wl-worker,
• ubi-io-inv/peb-inv-markbad is used by prepost-erase-worker-helper,
• ubi-io-inv/peb-inv-size is used by prepost-scan-all, prepost-io-write-data, prepost-erase-worker-helper, inv-read, inv-write, inv-recover, inv-format, inv-wl-worker,
• ubi-io-inv/peb-inv-write-echdr is used by prepost-write-once, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-change, inv-create-volume, inv-wl-worker,
• ubi-io-inv/reduce is used by prepost-erase-worker-helper,
• ubi-io-inv/ubi-io-initial-imp-inv is used by inv-format,

Used from specification array-indices

• array-indices/wlarray-base/map-indices-append is used by prepost-fix-ecs,
• array-indices/wlarray-base/map-indices-at is used by prepost-fix-ecs, inv-recover,
• array-indices/wlarray-base/map-indices-size is used by prepost-fix-ecs, inv-recover,
• array-indices/wlarray-base/valid-indices is used by prepost-fix-ecs,
• array-indices/wlarray-base/mapindices-base is used by prepost-fix-ecs,
• array-indices/wlarray-base/valid-indices-append is used by prepost-fix-ecs,
• array-indices/wlarray-base/valid-indices-one is used by prepost-fix-ecs,
• array-indices/wlarray-base/valid-indices-simp is used by inv-recover,
• array-indices/wlarray-base/valid-indices-write is used by prepost-fix-ecs,

Used from specification nat-list-less

• nat-list-less/ls-add is used by prepost-scan-all,
• nat-list-less/ls-base is used by prepost-scan-all, prepost-fix-ecs,
• nat-list-less/ls-bound-notin is used by prepost-scan-all,
• nat-list-less/ls-prepend-bound-add1 is used by prepost-scan-all,

Used from specification align

• align/alignup-is-even-bigger is used by subbarray-alignup-datasize-empty,
• align/alignup-le-is-aligned is used by prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-wear-level,
• align/alignup-lower-bound is used by prepost-atomic-leb-change,
• align/alignup-same is used by prepost-atomic-leb-change, ls-subarray-datasize,
• align/alignup-same0 is used by prepost-atomic-leb-change,
• align/is-aligned-add is used by inv-write,
• align/is-aligned-zero is used by ubi-io-inv-fillcount0, prepost-write-once, prepost-write-multiple, prepost-io-write-data, prepost-atomic-leb-change, inv-write, inv-map, inv-format,

Used from specification ubi-base

• ubi-base/bflipset-cons is used by prepost-get-pebs-for-wl, inv-recover,
• ubi-base/bitflip-cons-set-used is used by prepost-atomic-leb-change,
• ubi-base/id-set is used by inv-wl-worker,
• ubi-base/unique-sqns is used by prepost-init-vols-mappings,
• ubi-base/unique-sqns-2-valid-pebs is used by prepost-scan-all,
• ubi-base/unique-sqns-update is used by inv-format,
• ubi-base/valid-ebatbl is used by prepost-init-vols-mappings, lf-mapped-valid-peb, lf-mapped-info, inv-recover, inv-format, inv-wl-worker,
• ubi-base/valid-ebatbl-map is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-ebatbl-remap is used by prepost-atomic-leb-change,
• ubi-base/valid-eraseqp-append is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-eraseqp-invalidate is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/valid-eraseqp-update-other is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/valid-eraseqp-valid-lebref is used by inv-recover,
• ubi-base/valid-eraseqw is used by prepost-init-vols-mappings, lf-valid-eraseq-stronger-notin-recs, lf-used-info, inv-recover, inv-format,
• ubi-base/valid-eraseqw-use is used by prepost-atomic-leb-change,
• ubi-base/valid-global-sqn is used by prepost-atomic-leb-change, ls-valid-global-sqn-vtbl, inv-format,
• ubi-base/valid-global-sqn-add-valid is used by prepost-write-once, prepost-atomic-leb-change, inv-format,
• ubi-base/valid-global-sqn-invalidate is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/valid-global-sqn-write-valid is used by prepost-io-write-data,
• ubi-base/valid-vtbl is used by prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-atomic-leb-change, lf-vtbl-info, inv-recover, inv-format, inv-wl-worker,
• ubi-base/valid-vtbl-update-other-wlar is used by prepost-init-vols-mappings,
• ubi-base/valid-wl is used by prepost-init-vols-mappings, lf-valid-wl-not-erroneous, lf-valid-wl-free-emptyvidhdr, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-used-valid-peb, lf-mapped-valid-peb, inv-recover, inv-format, inv-wl-worker,
• ubi-base/valid-wl-erase is used by prepost-init-vols-mappings,
• ubi-base/valid-wl-erasing-invalidate is used by prepost-erase-worker-helper,
• ubi-base/valid-wl-erasing-invalidate0 is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-wl-map is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-wl-markbad is used by prepost-erase-worker-helper,
• ubi-base/valid-wl-next-invalid-erase is used by prepost-scan-all,
• ubi-base/valid-wl-next-valid-erase is used by prepost-scan-all,
• ubi-base/valid-wl-next-valid-update is used by prepost-scan-all,
• ubi-base/valid-wl-next-valid-use is used by prepost-scan-all,
• ubi-base/valid-wl-use is used by prepost-atomic-leb-change,
• ubi-base/valid-wl-write-unmapped is used by prepost-write-once,
• ubi-base/bflipset-subarray-add is used by prepost-scan-all,
• ubi-base/bflipset-subarray-erase-old is used by prepost-scan-all,
• ubi-base/bflipset-subarray-erase-old-add is used by prepost-scan-all,
• ubi-base/bflipset-subarray-next is used by prepost-scan-all,
• ubi-base/bitflip-cons-add is used by inv-read, inv-recover,
• ubi-base/bitflip-cons-del is used by prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-atomic-leb-change, inv-unmap,
• ubi-base/bitflip-cons-set is used by prepost-write-once, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-unmap,
• ubi-base/bitflip-cons-set-used is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/bitflips-cons-empty is used by prepost-scan-all, prepost-get-pebs-for-wl, inv-format, inv-wl-worker,
• ubi-base/bitflips-cons-in is used by prepost-write-once, prepost-get-pebs-for-wl, prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/datasize-alignup is used by prepost-atomic-leb-change,
• ubi-base/erase-worker-inv is used by prepost-erase-worker-helper,
• ubi-base/idset-idexpt-fwd is used by inv-wl-worker,
• ubi-base/idset-mapped-pebs-write-unused is used by prepost-erase-worker-helper,
• ubi-base/idset-refl is used by prepost-write-multiple, prepost-get-peb, prepost-atomic-leb-change, inv-erase-all, inv-create-volume, inv-wl-worker,
• ubi-base/idset-trans-intersect is used by prepost-write-multiple, inv-erase-all, inv-change, inv-create-volume, inv-wl-worker,
• ubi-base/idset-weaken is used by inv-change, inv-wl-worker,
• ubi-base/idset-write-notin is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/is-vtbl-pnum is used by prepost-atomic-leb-change, inv-wl-worker,
• ubi-base/mapped-pebs-add-empty-vol is used by inv-create-volume,
• ubi-base/mapped-pebs-rem-notmapped is used by inv-wl-worker,
• ubi-base/mapped-pebs-remap is used by inv-wl-worker,
• ubi-base/mapped-pebs-unused is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-wl-worker,
• ubi-base/ubi-cons is used by ubi-is-max-unique, prepost-write-once, prepost-write-multiple, prepost-io-write-data, prepost-get-pebs-for-wl, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-erase-all, inv-sync-device, inv-read, inv-write, inv-unmap, inv-erase, inv-map, inv-change, inv-recover, inv-format, inv-get-volume-size, inv-create-volume, inv-wl-worker, inv-erase-worker,
• ubi-base/unique-sqns-update is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/unique-sqns-write-valid is used by prepost-io-write-data,
• ubi-base/valid-ebatbl-add-unmapped-vol is used by prepost-atomic-leb-change,
• ubi-base/valid-ebatbl-move-vtbl is used by prepost-atomic-leb-change,
• ubi-base/valid-ebatbl-unmap is used by prepost-atomic-leb-change, inv-unmap,
• ubi-base/valid-ebatbl-update-vhdrs-unused is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/valid-ebatbl-update-wlar-unused is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/valid-ebatbl-write-data is used by prepost-io-write-data,
• ubi-base/valid-eraseq-array-0 is used by prepost-scan-all,
• ubi-base/valid-eraseq-next-erasing is used by prepost-scan-all,
• ubi-base/valid-eraseq-prev-erasing is used by prepost-scan-all,
• ubi-base/valid-eraseqd-append is used by prepost-write-once, prepost-atomic-leb-change, inv-unmap,
• ubi-base/valid-eraseqd-base is used by prepost-get-peb, inv-format, inv-create-volume, inv-erase-worker,
• ubi-base/valid-eraseqd-nodups-middle0 is used by prepost-erase-worker-helper,
• ubi-base/valid-eraseqd-nodups-middle1 is used by prepost-erase-worker-helper,
• ubi-base/valid-eraseqd-nodups-middle2 is used by prepost-erase-worker-helper,
• ubi-base/valid-eraseqd-one is used by inv-create-volume,
• ubi-base/valid-eraseqd-rem-middle is used by prepost-erase-worker-helper,
• ubi-base/valid-eraseqp-append is used by prepost-write-once, prepost-atomic-leb-change, inv-unmap,
• ubi-base/valid-eraseqp-base is used by prepost-get-peb, inv-format, inv-create-volume, inv-erase-worker,
• ubi-base/valid-eraseqp-in is used by lf-valid-recs-notin-eraseq,
• ubi-base/valid-eraseqp-in0 is used by prepost-erase-worker-helper,
• ubi-base/valid-eraseqp-invalidate is used by prepost-io-write-data,
• ubi-base/valid-eraseqp-rem-middle is used by prepost-erase-worker-helper,
• ubi-base/valid-eraseqp-update-other is used by prepost-io-write-data,
• ubi-base/valid-eraseqw-free is used by prepost-erase-worker-helper,
• ubi-base/valid-eraseqw-free-in is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-eraseqw-size-left is used by prepost-get-peb, inv-erase-all, inv-erase-worker,
• ubi-base/valid-eraseqw-size-middle is used by prepost-erase-worker-helper, lf-valid-eraseq-middle-wlar,
• ubi-base/valid-eraseqw-subarray-shift is used by prepost-scan-all,
• ubi-base/valid-eraseqw-unmap is used by prepost-write-once, prepost-atomic-leb-change, inv-unmap,
• ubi-base/valid-eraseqw-update-ec is used by prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/valid-eraseqw-use is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-global-sqn-array-0 is used by prepost-scan-all,
• ubi-base/valid-global-sqn-inc is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-global-sqn-invalidate is used by prepost-io-write-data,
• ubi-base/valid-global-sqn-next is used by prepost-scan-all,
• ubi-base/valid-global-sqn-next-max is used by prepost-scan-all,
• ubi-base/valid-global-sqn-not-leq is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-global-sqn-notin is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-vtbl-buf is used by inv-recover, inv-wl-worker,
• ubi-base/valid-vtbl-in-wlar is used by prepost-init-vols-mappings, prepost-atomic-leb-change, inv-recover, inv-wl-worker,
• ubi-base/valid-vtbl-sqns-notempty is used by prepost-atomic-leb-change, ls-valid-global-sqn-vtbl,
• ubi-base/valid-vtbl-update-other-pebs is used by prepost-write-once, prepost-io-write-data, prepost-erase-worker-helper, prepost-atomic-leb-change,
• ubi-base/valid-vtbl-update-other-wlar is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-unmap,
• ubi-base/valid-vtbl-update-vols is used by prepost-write-once, prepost-write-multiple, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-unmap, inv-change, inv-wl-worker,
• ubi-base/valid-vtbl-wlar-status is used by prepost-init-vols-mappings, prepost-atomic-leb-change, lf-valid-vtbl-neq-free, lf-valid-vtbl-neq-erasing, inv-recover, inv-wl-worker,
• ubi-base/valid-wl-array-0 is used by prepost-scan-all,
• ubi-base/valid-wl-erase is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-unmap,
• ubi-base/valid-wl-erasing-update-ec is used by prepost-erase-worker-helper,
• ubi-base/valid-wl-free is used by prepost-erase-worker-helper,
• ubi-base/valid-wl-free-echdr is used by prepost-write-once, prepost-atomic-leb-change,
• ubi-base/valid-wl-next-bad is used by prepost-scan-all,
• ubi-base/valid-wl-next-free is used by prepost-scan-all,
• ubi-base/valid-wl-write-valid is used by prepost-io-write-data,
• ubi-base/wl-threshold-nonzero is used by prepost-get-pebs-for-wl, prepost-get-peb,

Used from specification erasequeueentry

• erasequeueentry/elim is used by prepost-write-once, prepost-get-peb, inv-erase-all, inv-change, inv-erase-worker,
• erasequeueentry/sel-01 is used by prepost-get-peb,
• erasequeueentry/sel-02 is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-unmap,

Used from specification wlentry

• wlentry/elim-02 is used by prepost-write-once, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-io-write-data, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-vtbl-info, lf-valid-wl-bad, lf-valid-recs-valid-peb, lf-valid-recs-notin-eraseq, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-mapped-valid-peb, lf-mapped-info, inv-read, inv-write, inv-unmap, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• wlentry/inj-03 is used by prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-recover, inv-format,
• wlentry/sel-04 is used by prepost-write-once, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-valid-wl-not-erroneous, lf-valid-wl-free-emptyvidhdr, lf-valid-recs-valid-peb, lf-valid-recs-notin-eraseq, lf-valid-recs-max, lf-valid-eraseq-stronger-notin-recs, lf-used-valid-peb, lf-used-info, lf-mapped-valid-peb, lf-mapped-info, inv-read, inv-write, inv-unmap, inv-change, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• wlentry/sel-05 is used by prepost-write-once, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-init-vols-mappings, prepost-get-pebs-for-wl, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-valid-wl-free-emptyvidhdr, lf-mapped-valid-peb, inv-unmap, inv-recover, inv-wl-worker,
• wlentry/upd-04 is used by prepost-erase-worker-helper, inv-recover,
• wlentry/updsel-02 is used by prepost-scan-all, prepost-erase-worker-helper,
• wlentry/updsel-04 is used by inv-recover,

Used from specification list

• list/erasequeue-base/Last is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-unmap, inv-change, inv-create-volume, inv-wl-worker,
• list/erasequeue-base/Nil is used by prepost-get-peb, inv-erase-all, inv-create-volume, inv-erase-worker,
• list/nat-list-set/a is used by prepost-scan-all, prepost-fix-ecs,
• list/erasequeue-base/a is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-get-peb, prepost-erase-worker-helper, prepost-atomic-leb-change, lf-valid-eraseq-middle-wlar, inv-erase-all, inv-unmap, inv-change, inv-create-volume, inv-wl-worker, inv-erase-worker,
• list/nat-list-set/app is used by prepost-fix-ecs,
• list/erasequeue-base/app is used by inv-wl-worker,
• list/erasequeue-base/app-01 is used by prepost-atomic-leb-change,
• list/erasequeue-base/app-02 is used by prepost-get-peb, inv-erase-all, inv-wl-worker, inv-erase-worker,
• list/nat-list-set/app-03 is used by prepost-fix-ecs,
• list/erasequeue-base/app-05 is used by prepost-get-peb,
• list/nat-list-set/app-05 is used by prepost-fix-ecs,
• list/erasequeue-base/app-06 is used by prepost-atomic-leb-change,
• list/erasequeue-base/app-08 is used by prepost-get-peb,
• list/erasequeue-base/c is used by prepost-write-once, prepost-get-peb, prepost-erase-worker-helper, inv-erase-all, inv-change, inv-erase-worker,
• list/nat-list-set/c is used by prepost-scan-all, prepost-fix-ecs,
• list/erasequeue-base/c-07 is used by prepost-get-peb, inv-erase-all, inv-erase-worker,
• list/erasequeue-base/c-08 is used by prepost-get-peb,
• list/erasequeue-base/e is used by prepost-get-peb, inv-erase-all, inv-wl-worker, inv-erase-worker,
• list/nat-list-set/e-01 is used by prepost-fix-ecs,
• list/erasequeue-base/e-01 is used by prepost-write-once, prepost-get-peb, inv-erase-all, inv-change, inv-erase-worker,
• list/erasequeue-base/e-02 is used by inv-wl-worker,
• list/erasequeue-base/in-15 is used by inv-wl-worker,
• list/erasequeue-base/in-17 is used by inv-wl-worker,
• list/erasequeue-base/in-append is used by inv-wl-worker,
• list/erasequeue-base/len-05 is used by inv-erase-all,

Used from specification encoding-vtbl

• encoding-vtbl/decode is used by inv-recover,
• encoding-vtbl/encode is used by inv-format, inv-create-volume,
• encoding-vtbl/is-encoded-unique is used by prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-atomic-leb-change, inv-recover, inv-format, inv-create-volume,

Used from specification array-copy

• array-copy/apebs/Cmp-elem is used by lf-cmp-peb,
• array-copy/buffer/subarray-subarray-elim is used by ls-subarray-datasize,
• array-copy/ebatbl/at-fill-mkarray is used by prepost-init-vols-sizes,
• array-copy/buffer/copy-exact is used by prepost-scan-all, inv-recover, inv-wl-worker,
• array-copy/wlarray-base/idexcept-comm-simp is used by prepost-get-peb,
• array-copy/apebs/idexcept-comm-simp is used by prepost-get-peb,
• array-copy/apebs/idexcept-refl is used by prepost-erase-worker-helper,
• array-copy/apebs/idexcept-same is used by prepost-atomic-leb-change,
• array-copy/wlarray-base/idexcept-same is used by prepost-erase-worker-helper,
• array-copy/wlarray-base/idexcept-size is used by prepost-get-peb, prepost-erase-worker-helper, inv-erase-all, inv-wl-worker, inv-erase-worker,
• array-copy/apebs/idexcept-size is used by prepost-get-peb, prepost-erase-worker-helper, inv-erase-all, inv-change, inv-create-volume, inv-wl-worker, inv-erase-worker,
• array-copy/wlarray-base/idexcept-write-at0 is used by prepost-erase-worker-helper,
• array-copy/apebs/idexcept-write-at0 is used by prepost-erase-worker-helper, prepost-atomic-leb-change,
• array-copy/buffer/size-copy is used by inv-write,
• array-copy/wlarray-base/size-fill is used by prepost-scan-all,
• array-copy/ebatbl/size-fill is used by prepost-init-vols-sizes, prepost-atomic-leb-change,
• array-copy/buffer/size-subarray is used by valid-peb-write-valid-peb, subbarray-alignup-datasize-empty, prepost-write-multiple, prepost-io-write-data, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-zero, ls-datasize-wear-level,
• array-copy/apebs/size-subarray is used by prepost-scan-all, lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-recs-in-apebs,
• array-copy/wlarray-base/size-subarray is used by prepost-scan-all, lf-valid-recs-valid-peb, lf-valid-recs-max,
• array-copy/wlarray-base/subarray-at is used by lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-recs-in-apebs,
• array-copy/buffer/subarray-at is used by valid-peb-write-valid-peb, subbarray-alignup-datasize-empty, ls-datasize-zero,
• array-copy/apebs/subarray-at is used by lf-valid-recs-valid-peb, lf-valid-recs-max, lf-valid-recs-in-apebs,
• array-copy/buffer/subarray-elim is used by valid-peb-write-valid-peb, ubi-io-inv-fillcount0, prepost-io-write-data, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-wear-level, inv-write, inv-format, inv-create-volume, inv-wl-worker,
• array-copy/wlarray-base/subarray-elim is used by prepost-scan-all, inv-recover,
• array-copy/apebs/subarray-elim is used by prepost-scan-all, inv-recover,
• array-copy/buffer/subarray-subarray-elim-0 is used by prepost-atomic-leb-change,
• array-copy/wlarray-base/subarray-zero is used by prepost-scan-all,
• array-copy/buffer/subarray-zero is used by prepost-write-once, prepost-write-multiple, ls-datasize-wear-level, inv-format,
• array-copy/apebs/subarray-zero is used by prepost-scan-all,

Used from specification list-dup

• list-dup/nat-list-set/a is used by prepost-fix-ecs,
• list-dup/nat-list-set/c-02 is used by prepost-fix-ecs,
• list-dup/nat-list-set/dups-cons is used by prepost-scan-all, prepost-fix-ecs,
• list-dup/nat-list-set/e-01 is used by prepost-scan-all,
• list-dup/nat-list-set/f-01 is used by prepost-fix-ecs,

Used from specification datasize

• datasize/datasize is used by valid-peb-write-valid-peb,
• datasize/datasize-append is used by valid-peb-write-valid-peb,
• datasize/datasize-append-empty-h is used by valid-peb-write-valid-peb, ls-datasize-wear-level,
• datasize/datasize-at-h is used by subbarray-alignup-datasize-empty,
• datasize/datasize-zero-h is used by ls-datasize-zero,
• datasize/datasize-base is used by valid-peb-write-valid-peb,
• datasize/datasize-datasize-elim-h is used by prepost-atomic-leb-change,
• datasize/datasize-empbuf is used by valid-peb-write-valid-peb, prepost-atomic-leb-change,
• datasize/datasize-is-smaller is used by valid-peb-write-valid-peb,
• datasize/datasize-is-smaller-help is used by prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-wear-level,
• datasize/datasize-le-fwd is used by valid-peb-write-valid-peb, prepost-scan-all, prepost-atomic-leb-change,
• datasize/datasize-ls-datasize-h is used by prepost-atomic-leb-change,
• datasize/datasize-mkempbuffer is used by prepost-write-once, prepost-atomic-leb-change,
• datasize/datasize-subarray0 is used by valid-peb-write-valid-peb, prepost-atomic-leb-change,

Used from specification eraseblock

• eraseblock/emptyleb-size is used by inv-recover, inv-wl-worker,
• eraseblock/lebsize-neq-zero is used by valid-peb-write-valid-peb, prepost-write-once, prepost-io-write-data, ls-datasize-wear-level, inv-format,
• eraseblock/lebsize-page-size-is-aligned is used by prepost-atomic-leb-change, inv-format, inv-create-volume, inv-wl-worker,
• eraseblock/page-size is used by ubi-io-inv-fillcount0, subbarray-alignup-datasize-empty, prepost-write-once, prepost-write-multiple, prepost-io-write-data, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-wear-level, inv-write, inv-map, inv-format,

Used from specification nat-mult

• nat-mult/coef-19 is used by inv-create-volume,
• nat-mult/mult-a is used by prepost-get-pebs-for-wl, inv-format, inv-create-volume,
• nat-mult/mult-c is used by prepost-get-pebs-for-wl, inv-format, inv-create-volume,
• nat-mult/numeral-21 is used by inv-create-volume,
• nat-mult/one is used by inv-create-volume,
• nat-mult/rsucc-02 is used by inv-create-volume,
• nat-mult/two-02 is used by inv-create-volume,
• nat-mult/two-zero-01 is used by prepost-get-pebs-for-wl,
• nat-mult/zero is used by inv-format,

Used from specification oelem

• oelem/nat-set/irreflexivity is used by valid-peb-write-valid-peb, prepost-write-once, prepost-write-multiple, prepost-wl-get-used-min, prepost-wl-get-free-min, prepost-wl-free-max-below, prepost-scan-all, prepost-init-vols-sizes, prepost-init-vols-mappings, prepost-get-peb, prepost-fix-ecs, prepost-erase-worker-helper, prepost-atomic-leb-change, ls-subarray-datasize, ls-datasize-wear-level, lf-valid-recs-notin-eraseq, inv-erase-all, inv-write, inv-recover, inv-format, inv-wl-worker,
• oelem/nat-set/ls-le is used by prepost-wl-free-max-below,
• oelem/nat-set/sls is used by inv-format,
• oelem/nat-set/transitivity is used by prepost-wl-get-used-min, prepost-wl-free-max-below, prepost-scan-all,

Used from specification vtbl-conv

• vtbl-conv/to-vtbl-at is used by prepost-init-vols-mappings,
• vtbl-conv/to-vtbl-base is used by prepost-init-vols-sizes, inv-format,
• vtbl-conv/to-vtbl-in is used by prepost-init-vols-sizes, prepost-init-vols-mappings, inv-recover, inv-create-volume,
• vtbl-conv/to-vtbl-size is used by inv-create-volume,
• vtbl-conv/to-vtbl-update-vol is used by prepost-init-vols-sizes, prepost-atomic-leb-change,

Used from specification oset

• oset/nat-set/Min-in is used by prepost-get-pebs-for-wl, prepost-get-peb,
• oset/nat-set/max-ifins is used by prepost-wl-free-max-below,
• oset/nat-set/min-ins-01 is used by prepost-wl-get-used-min, prepost-wl-get-free-min,
• oset/nat-set/min-inn is used by prepost-wl-get-used-min, prepost-wl-get-free-min,
• oset/nat-set/min-insert is used by prepost-wl-get-used-min, prepost-wl-get-free-min,
• oset/nat-set/min-one is used by prepost-wl-get-used-min, prepost-wl-get-free-min,

Used from specification store-union

• store-union/vtbl/union-move-left is used by prepost-init-vols-sizes,
• store-union/vtbl/disjoint-in-right is used by prepost-init-vols-sizes,
• store-union/vtbl/disjoint-left-empty is used by prepost-init-vols-sizes,
• store-union/vtbl/disjoint-move-left is used by prepost-init-vols-sizes,
• store-union/vtbl/disjoint-right-empty is used by prepost-init-vols-sizes,
• store-union/vtbl/union-left-empty is used by prepost-init-vols-sizes,
• store-union/vtbl/union-right-empty is used by prepost-init-vols-sizes,

Used from specification array

• array/buffer/Extension is used by valid-peb-write-valid-peb, subbarray-alignup-datasize-empty, ls-datasize-zero, ls-array-append-length0,
• array/wlarray-base/Put-other is used by prepost-atomic-leb-change,
• array/wlarray-base/cputput-reverse is used by prepost-atomic-leb-change,
• array/ebatbl/Put-other is used by prepost-init-vols-mappings,
• array/apebs/Put-other is used by inv-format,
• array/wlarray-base/Put-other is used by prepost-init-vols-mappings, prepost-atomic-leb-change, inv-format,
• array/ebatbl/Put-same is used by prepost-init-vols-mappings, prepost-atomic-leb-change,
• array/wlarray-base/Put-same is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-format,
• array/apebs/Put-same is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-format,
• array/buffer/Size-mkarray is used by prepost-scan-all, ls-datasize-wear-level, inv-write, inv-map, inv-recover, inv-format, inv-create-volume, inv-wl-worker,
• array/wlarray-base/Size-mkarray is used by prepost-scan-all, inv-format,
• array/ebatbl/Size-mkarray is used by prepost-init-vols-sizes, prepost-atomic-leb-change,
• array/apebs/Size-mkarray is used by inv-format,
• array/wlarray-base/Size-put is used by prepost-write-once, prepost-scan-all, prepost-init-vols-mappings, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-unmap, inv-format,
• array/ebatbl/Size-put is used by prepost-write-multiple, prepost-init-vols-mappings, prepost-atomic-leb-change,
• array/apebs/Size-put is used by prepost-write-once, prepost-io-write-data, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-format,
• array/apebs/cgetput is used by prepost-write-once, prepost-atomic-leb-change,
• array/wlarray-base/cgetput is used by prepost-atomic-leb-change, inv-format,
• array/wlarray-base/cngetput is used by prepost-scan-all, prepost-atomic-leb-change, inv-format,
• array/apebs/cngetput is used by prepost-atomic-leb-change, inv-format,
• array/wlarray-base/cputput is used by prepost-scan-all, prepost-atomic-leb-change,
• array/apebs/cputput is used by prepost-write-once, prepost-erase-worker-helper, prepost-atomic-leb-change, inv-format,
• array/wlarray-base/ngp-07 is used by inv-format,
• array/ebatbl/put-same-content is used by prepost-atomic-leb-change,

Used from specification nat-div

• nat-div/zero is used by inv-recover,

Used from specification ebaentry

• ebaentry/disj is used by prepost-init-vols-mappings, prepost-atomic-leb-change, inv-read, inv-write, inv-unmap, inv-recover, inv-wl-worker,
• ebaentry/elim is used by prepost-atomic-leb-change, inv-read, inv-write, inv-unmap, inv-recover,
• ebaentry/inj is used by prepost-init-vols-mappings,
• ebaentry/sel is used by inv-wl-worker,

Used from specification ubi-asm

• ubi-asm/ls-max is used by ls-max,

Used from specification debug

• debug/debug is used by prepost-erase-worker-helper, inv-write, inv-change, inv-format, inv-wl-worker,

Used from specification aubi-io-asm

• aubi-io-asm/inv-sync-erase is used by prepost-erase-worker-helper,
• aubi-io-asm/inv-write-data is used by prepost-write-once, prepost-io-write-data, inv-format,
• aubi-io-asm/inv-write-data-wl is used by prepost-atomic-leb-change,
• aubi-io-asm/inv-write-vidhdr is used by prepost-write-once, prepost-atomic-leb-change, inv-format,