[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 store+set

store+set/group-store-ablock-store-nat-store/Dom is used by refine-get-gc-block,

Used from specification array-splice

array-splice/buffer/append-a is used by refine-sync, refine-add-ind, refine-add-gnds, refine-read-ind, refine-read-gnd,
array-splice/buffer/append-len is used by refine-sync, refine-add-ind, refine-add-gnds, refine-read-ind, refine-read-gnd,
array-splice/buffer/subarray-append-elim-left0-simp is used by refine-read-ind, refine-read-gnd,
array-splice/buffer/subarray-append-left is used by refine-read-ind, refine-read-gnd,

Used from specification ablock

ablock/group-store/elim is used by fwd-in-gstore-lpt, refine-sync, refine-add-gnds, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-gblock-refsize, refine-set-gblock-refsize, refine-read-gblock-nodes, refine-read-gnd,
ablock/index-store/elim is used by fwd-in-istore-lpt, refine-sync, refine-add-ind, refine-commit, refine-allocate-ind, refine-get-iblock-refsize, refine-set-iblock-refsize, refine-read-ind,
ablock/index-store/inj is used by refine-add-ind, refine-commit,
ablock/group-store/inj is used by refine-add-gnds, refine-commit, refine-deallocate-gnd, refine-allocate-gnd,
ablock/group-store/sel-01 is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd, refine-read-gblock-nodes, refine-read-gnd,
ablock/index-store/sel-01 is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-read-ind,
ablock/index-store/sel-02 is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-read-ind,
ablock/group-store/sel-02 is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd, refine-read-gblock-nodes, refine-read-gnd,
ablock/group-store/sel-03 is used by fwd-in-gstore-lpt, refine-sync, refine-add-gnds, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-get-gblock-refsize, refine-set-gblock-refsize, refine-read-gblock-nodes, refine-read-gnd,
ablock/index-store/sel-03 is used by fwd-in-istore-lpt, refine-sync, refine-add-ind, refine-commit, refine-allocate-ind, refine-get-iblock-refsize, refine-read-ind,
ablock/index-store/upd-01 is used by refine-add-ind,
ablock/group-store/upd-01 is used by refine-add-gnds,
ablock/index-store/upd-02 is used by refine-add-ind,
ablock/group-store/upd-02 is used by refine-add-gnds,
ablock/group-store/upd-03 is used by refine-set-gblock-refsize,
ablock/index-store/upd-03 is used by refine-set-iblock-refsize,
ablock/group-store/updsel-03 is used by refine-add-gnds,
ablock/index-store/updsel-28 is used by refine-add-ind,
ablock/group-store/updsel-28 is used by refine-add-gnds,
ablock/group-store/updsel-29 is used by refine-add-gnds,

Used from specification nat-basic

nat-basic/a is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-read-ind, refine-read-gnd,
nat-basic/add-base is used by refine-sync, refine-add-ind, refine-add-gnds,
nat-basic/c is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-read-ind, refine-read-gnd,
nat-basic/eq-01 is used by refine-sync, refine-add-ind, refine-add-gnds, refine-read-ind, refine-read-gnd,
nat-basic/eq-02 is used by refine-add-ind,
nat-basic/eqs is used by refine-sync,
nat-basic/f is used by fwd-in-istore-lpt, fwd-in-gstore-lpt, refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, recovery, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-iblock-refsize, refine-get-gblock-refsize, refine-set-iblock-refsize, refine-set-gblock-refsize, refine-get-gc-block, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,
nat-basic/l is used by refine-add-ind,
nat-basic/l-02 is used by refine-get-block-free-size, refine-read-ind, refine-read-gnd,
nat-basic/lf-01 is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, recovery, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-iblock-refsize, refine-get-gblock-refsize, refine-set-iblock-refsize, refine-set-gblock-refsize, refine-get-gc-block, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,
nat-basic/lf-02 is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, recovery, refine-allocate-ind, refine-deallocate-gnd,
nat-basic/succ is used by refine-read-ind, refine-read-gnd,
nat-basic/z-01 is used by refine-add-ind,

Used from specification node-header-size

node-header-size/leb-size-aligned-2-node-header is used by refine-sync,
node-header-size/nodeheader-notzero is used by refine-add-ind,

Used from specification encoding-node-base

encoding-node-base/encoding-index-node/node-flash-size is used by refine-add-ind, refine-read-ind,
encoding-node-base/encoding-group-node/node-flash-size is used by refine-read-gnd,

Used from specification ablock-store-inv

ablock-store-inv/group-store/at-remove-refsize0 is used by refine-commit,
ablock-store-inv/index-store/at-remove-refsize0 is used by refine-commit,
ablock-store-inv/group-store/in is used by refine-read-gnd,
ablock-store-inv/index-store/in is used by refine-add-ind, refine-read-ind,
ablock-store-inv/group-store/in-remove-refsize0 is used by refine-commit,
ablock-store-inv/index-store/in-remove-refsize0 is used by refine-commit,
ablock-store-inv/group-store/adrs-empty is used by refine-add-gnds,
ablock-store-inv/index-store/at-explicit is used by refine-read-ind,
ablock-store-inv/group-store/at-explicit-diff is used by refine-read-gnd,
ablock-store-inv/group-store/inv-flashsize-empty is used by refine-add-gnds,
ablock-store-inv/group-store/inv-nodups is used by refine-add-gnds,
ablock-store-inv/index-store/prefix-notin-fwd is used by refine-read-ind,
ablock-store-inv/group-store/to-adrs-eq is used by refine-read-gblock-nodes,

Used from specification apersistence-base

Used from specification gc-heap-rename

gc-heap-rename/id-idx-len-eq-0 is used by refine-commit,

Used from specification store

store/group-store-ablock-store-nat-store/At-other is used by refine-allocate-gnd,
store/index-store-ablock-store-nat-store/At-same is used by refine-add-ind,
store/group-store-ablock-store-nat-store/At-same is used by refine-add-gnds, refine-allocate-gnd,
store/group-store-ablock-store-nat-store/Del-at is used by refine-deallocate-gnd,
store/group-store-ablock-store-nat-store/Del-in is used by refine-deallocate-gnd,
store/index-store-ablock-store-nat-store/In-empty is used by initialization,
store/group-store-ablock-store-nat-store/In-empty is used by initialization,
store/group-store-ablock-store-nat-store/in-neq is used by refine-allocate-gnd,
store/group-store-ablock-store-nat-store/ins is used by refine-add-gnds,
store/index-store-ablock-store-nat-store/insin is used by refine-add-ind,
store/group-store-ablock-store-nat-store/insin is used by refine-add-gnds, refine-allocate-gnd,
store/index-store-ablock-store-nat-store/insins is used by refine-add-ind,
store/group-store-ablock-store-nat-store/insins is used by refine-add-gnds,
store/group-store-ablock-store-nat-store/notmemlookup is used by refine-commit, refine-allocate-gnd,
store/index-store-ablock-store-nat-store/notmemlookup is used by refine-commit,

Used from specification nat

nat/cancel-01 is used by refine-add-ind,
nat/elim-sub is used by refine-get-block-free-size, refine-sync,
nat/eq-02 is used by refine-sync,
nat/fle is used by refine-add-gnds, recovery, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-iblock-refsize, refine-get-gblock-refsize, refine-set-iblock-refsize, refine-set-gblock-refsize,
nat/fle-01 is used by refine-get-block-free-size, refine-add-ind, refine-add-gnds, recovery, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-iblock-refsize, refine-get-gblock-refsize, refine-set-iblock-refsize, refine-set-gblock-refsize,
nat/ge is used by refine-get-block-free-size, refine-sync,
nat/le is used by refine-sync,
nat/le-add is used by refine-sync, refine-add-ind, refine-add-gnds,
nat/le-def is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, recovery, refine-read-ind, refine-read-gnd,
nat/le-ls-simp is used by refine-get-block-free-size, refine-sync, recovery, refine-commit, refine-allocate-ind,
nat/lels is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, recovery, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-iblock-refsize, refine-get-gblock-refsize, refine-set-iblock-refsize, refine-set-gblock-refsize,
nat/lels-02 is used by refine-sync, refine-add-ind, refine-add-gnds,
nat/lels-03 is used by refine-sync, refine-add-ind, refine-add-gnds,
nat/lep is used by refine-read-ind, refine-read-gnd,
nat/lep-02 is used by refine-add-ind, refine-read-ind, refine-read-gnd,
nat/ler is used by refine-sync, refine-add-ind, refine-add-gnds,
nat/let is used by refine-sync,
nat/lez is used by refine-get-block-free-size, refine-add-gnds,
nat/lez-01 is used by refine-add-gnds,
nat/ls-le-simp is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-set-gblock-refsize,

Used from specification set-union

set-union/nat-set/Delete is used by refine-allocate-gnd,
set-union/nat-set/int-a is used by refine-sync, refine-add-gnds, recovery, refine-commit, refine-allocate-ind, refine-set-gblock-refsize,
set-union/nat-set/int-c is used by refine-sync, refine-add-gnds, recovery, refine-commit, refine-allocate-ind, refine-set-gblock-refsize,
set-union/nat-set/int-ins is used by refine-sync, refine-add-gnds, refine-allocate-ind,
set-union/nat-set/una is used by refine-sync, refine-add-gnds, recovery, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-set-gblock-refsize,
set-union/nat-set/unadd is used by refine-sync, refine-add-gnds, refine-allocate-ind,
set-union/nat-set/unc is used by refine-sync, refine-add-gnds, recovery, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-set-gblock-refsize,

Used from specification error-class

error-class/ecommit is used by refine-allocate-ind, refine-allocate-gnd,
error-class/enospc is used by refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd,
error-class/erofs is used by refine-commit, refine-allocate-ind, refine-deallocate-gnd,
error-class/esuccess is used by refine-sync, refine-add-ind, refine-add-gnds, initialization, recovery, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
error-class/not-esuccess is used by refine-sync, refine-add-ind, refine-add-gnds, initialization, recovery, refine-commit, refine-allocate-ind, refine-allocate-gnd, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,

Used from specification abs-list

abs-list/encoding-index-node/abs-failed-abs-nodes-h is used by refine-add-ind,
abs-list/encoding-group-node/abs-nodes-append is used by refine-add-gnds,
abs-list/encoding-index-node/abs-nodes-append is used by refine-add-ind,
abs-list/encoding-index-node/abs-nodes-base is used by refine-sync,
abs-list/encoding-group-node/abs-nodes-base is used by refine-sync,
abs-list/encoding-group-node/abs-nodes-nodups is used by refine-add-gnds,
abs-list/encoding-index-node/abs-nodes-strong-imp-weak-h is used by refine-add-ind,
abs-list/encoding-group-node/abs-nodes-subarray-failed is used by refine-add-gnds,
abs-list/encoding-group-node/abs-nodes-unique-strong is used by refine-read-gblock-nodes,
abs-list/encoding-group-node/abs-split-by-address is used by refine-read-gnd,
abs-list/encoding-index-node/abs-split-by-address is used by refine-read-ind,
abs-list/encoding-group-node/abs-nodes-aligned-2headersize is used by refine-sync,
abs-list/encoding-index-node/abs-nodes-aligned-2headersize is used by refine-sync,
abs-list/encoding-group-node/abs-nodes-append-empty is used by refine-sync,
abs-list/encoding-index-node/abs-nodes-append-empty is used by refine-sync, refine-add-ind,
abs-list/encoding-index-node/abs-nodes-atend-no-address is used by refine-add-ind,
abs-list/encoding-group-node/abs-nodes-elems-adr-length is used by refine-sync, refine-add-gnds, refine-read-gblock-nodes, refine-read-gnd,
abs-list/encoding-index-node/abs-nodes-elems-adr-length is used by refine-sync, refine-add-ind, refine-read-ind,
abs-list/encoding-group-node/abs-nodes-elems-adr-length-h is used by refine-add-gnds,
abs-list/encoding-group-node/abs-nodes-mkbuf0-empty is used by refine-allocate-gnd,
abs-list/encoding-index-node/abs-nodes-mkbuf0-empty is used by refine-allocate-ind,
abs-list/encoding-index-node/abs-nodes-one-abs-node is used by refine-add-ind,
abs-list/encoding-index-node/abs-nodes-prefix-elim is used by refine-sync,
abs-list/encoding-index-node/abs-nodes-strengthen is used by refine-add-ind,
abs-list/encoding-group-node/abs-nodes-strengthen is used by refine-add-gnds, refine-read-gblock-nodes,
abs-list/encoding-group-node/abs-nodes-strong-imp-weak is used by refine-read-gblock-nodes,
abs-list/encoding-index-node/abs-nodes-unique-strong is used by refine-add-ind,
abs-list/encoding-group-node/abs-nodes-unique-strong is used by refine-add-gnds, refine-read-gblock-nodes,
abs-list/encoding-group-node/abs-nodes-unique-strong-h is used by refine-add-gnds,
abs-list/encoding-group-node/abs-nodes-unique-weak is used by refine-read-gblock-nodes,
abs-list/encoding-index-node/abs-padding-abs-nodes-h is used by refine-sync,
abs-list/encoding-group-node/abs-padding-abs-nodes-h is used by refine-sync,
abs-list/encoding-group-node/add-failed-is-aligned is used by refine-sync, refine-add-gnds,
abs-list/encoding-index-node/add-failed-is-aligned is used by refine-sync, refine-add-ind,
abs-list/encoding-group-node/flashsize-eq-0 is used by refine-add-gnds,

Used from specification error

error/disj-120 is used by refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
error/disj-35 is used by refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd, refine-get-gc-block,
error/disj-91 is used by refine-allocate-ind, refine-allocate-gnd,

Used from specification aleb

aleb/aleb-not-mapped is used by refine-allocate-ind,
aleb/inj is used by refine-sync, refine-add-ind, refine-add-gnds, refine-read-ind, refine-read-gnd,
aleb/sel is used by refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,
aleb/test-01 is used by refine-allocate-ind,
aleb/test-02 is used by refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,

Used from specification lprops

lprops/disj-01 is used by refine-sync, refine-add-gnds, initialization, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
lprops/disj-02 is used by refine-sync, refine-add-ind, refine-add-gnds, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-set-iblock-refsize, refine-set-gblock-refsize,
lprops/disj-03 is used by refine-sync, refine-add-ind, initialization, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
lprops/elim is used by fwd-in-istore-lpt, fwd-in-gstore-lpt, refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-iblock-refsize, refine-get-gblock-refsize, refine-set-iblock-refsize, refine-set-gblock-refsize, refine-get-gc-block, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,
lprops/inj is used by refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-iblock-refsize, refine-get-gblock-refsize,
lprops/upd-04 is used by refine-allocate-ind, refine-allocate-gnd, refine-set-iblock-refsize, refine-set-gblock-refsize,
lprops/upd-06 is used by refine-allocate-ind, refine-allocate-gnd,
lprops/updsel-01 is used by refine-deallocate-gnd,
lprops/updsel-03 is used by refine-deallocate-gnd,
lprops/updsel-09 is used by refine-deallocate-gnd,
lprops/updsel-13 is used by refine-deallocate-gnd,
lprops/updsel-15 is used by refine-deallocate-gnd,

Used from specification set-basic

set-basic/nat-set/in-02 is used by refine-deallocate-gnd,
set-basic/gc-heap-rename-gc-heap-base-keyindex-set/ne-01 is used by refine-deallocate-gnd, refine-set-gblock-refsize,
set-basic/gc-heap-rename-gc-heap-base-keyindex-set/size-zero-01 is used by refine-deallocate-gnd, refine-set-gblock-refsize,

Used from specification list-last

list-last/nat-list-set/last-def is used by refine-sync, refine-add-gnds, refine-allocate-ind,
list-last/nat-list-set/lin-01 is used by refine-add-gnds,
list-last/nat-list-set/lin-02 is used by refine-add-gnds, refine-deallocate-gnd,

Used from specification list-prefixn

list-prefixn/group-store/prefixn-0 is used by refine-add-gnds,
list-prefixn/group-store/prefixn-fulln is used by refine-add-gnds,
list-prefixn/laddress-list/prefixn-len-n is used by refine-add-gnds,
list-prefixn/group-store/prefixn-len-n is used by refine-add-gnds,

Used from specification list-data

list-data/nat-list-set/elim-list-c is used by refine-allocate-ind, refine-allocate-gnd,
list-data/group-store/l is used by refine-add-gnds,
list-data/laddress-list/l is used by refine-add-gnds,
list-data/laddress-list/size-01 is used by refine-add-gnds,
list-data/group-store/size-01 is used by refine-add-gnds,

Used from specification laddress

laddress/inj is used by refine-add-ind, refine-read-ind, refine-read-gnd,

Used from specification persistence-state

persistence-state/disj-01 is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-deallocate-gnd,
persistence-state/disj-02 is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
persistence-state/disj-03 is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, initialization, recovery, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
persistence-state/disj-05 is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-deallocate-gnd,
persistence-state/disj-06 is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
persistence-state/elim-01 is used by refine-add-gnds,
persistence-state/elim-02 is used by refine-add-ind,
persistence-state/not-journal-or-index is used by refine-sync, recovery, refine-commit,
persistence-state/sel-01 is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
persistence-state/sel-02 is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-deallocate-gnd,
persistence-state/test-01 is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-deallocate-gnd,
persistence-state/test-02 is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
persistence-state/test-03 is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd,
persistence-state/test-04 is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
persistence-state/test-07 is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-deallocate-gnd,
persistence-state/test-09 is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd,
persistence-state/test-10 is used by refine-get-block-free-size, refine-sync, refine-add-gnds,
persistence-state/test-11 is used by refine-get-block-free-size, refine-sync, refine-add-ind,

Used from specification align

align/is-aligned-add is used by refine-sync, refine-add-ind, refine-add-gnds,
align/is-aligned-pad is used by refine-sync,

Used from specification list

list/laddress-list/in-def is used by refine-read-ind, refine-read-gnd,
list/nat-list-set/lastdiv-rew is used by refine-sync, refine-add-gnds, refine-allocate-ind,
list/index-store/Last is used by refine-add-ind,
list/nat-list-set/Last is used by refine-deallocate-gnd, refine-allocate-gnd,
list/laddress-list/Last is used by refine-add-ind,
list/group-store/a is used by refine-add-gnds, refine-read-gblock-nodes, refine-read-gnd,
list/laddress-list/a is used by refine-sync, refine-add-gnds, refine-read-ind, refine-read-gnd,
list/nat-list-set/a is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd,
list/index-store/a is used by refine-sync, refine-read-ind,
list/address-list-set/a is used by refine-read-gblock-nodes,
list/laddress-list/app is used by refine-add-gnds,
list/group-store/app is used by refine-add-gnds,
list/group-store/app-01 is used by refine-read-gblock-nodes,
list/nat-list-set/app-01 is used by refine-allocate-gnd,
list/address-list-set/app-01 is used by refine-read-gblock-nodes,
list/nat-list-set/app-02 is used by refine-allocate-ind, refine-allocate-gnd,
list/laddress-list/app-04 is used by refine-sync,
list/index-store/app-04 is used by refine-sync,
list/laddress-list/c is used by refine-read-ind, refine-read-gnd,
list/nat-list-set/c is used by refine-allocate-ind, refine-allocate-gnd,
list/nat-list-set/e is used by refine-allocate-ind, refine-allocate-gnd,
list/nat-list-set/e-01 is used by refine-allocate-ind, refine-allocate-gnd,
list/nat-list-set/e-02 is used by refine-add-gnds,
list/laddress-list/in-append is used by refine-read-ind, refine-read-gnd,
list/laddress-list/in-rec is used by refine-read-ind, refine-read-gnd,
list/index-store/len is used by refine-read-ind,
list/laddress-list/len is used by refine-read-ind, refine-read-gnd,
list/group-store/len is used by refine-read-gnd,
list/laddress-list/len-05 is used by refine-read-ind, refine-read-gnd,
list/index-store/len-05 is used by refine-read-ind,
list/group-store/len-05 is used by refine-read-gnd,

Used from specification persistence-base

persistence-base/abs-gstore-cleanup-lpt is used by refine-commit,
persistence-base/abs-gstore-crash is used by recovery,
persistence-base/abs-gstore-def is used by fwd-in-gstore-lpt, refine-sync, refine-add-gnds, initialization, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-gc-block, refine-read-gblock-nodes, refine-read-gnd,
persistence-base/abs-istore-cleanup-lpt is used by refine-commit,
persistence-base/abs-istore-crash is used by recovery,
persistence-base/abs-istore-def is used by fwd-in-istore-lpt, refine-sync, refine-add-ind, initialization, refine-commit, refine-allocate-ind, refine-read-ind,
persistence-base/buf-ro-rw-mode is used by refine-sync,
persistence-base/bufs-log-only is used by refine-sync,
persistence-base/flash-lpt-cons is used by initialization, refine-commit,
persistence-base/gc-heap-in is used by refine-deallocate-gnd, refine-set-gblock-refsize,
persistence-base/lpt-free-unref is used by initialization,
persistence-base/lpt-leb-size is used by refine-get-block-free-size,
persistence-base/abs-gstore-avol-change-other is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-allocate-gnd,
persistence-base/abs-gstore-lpt-change-other is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-allocate-gnd, refine-set-iblock-refsize,
persistence-base/abs-gstore-reduce-write is used by refine-add-gnds,
persistence-base/abs-gstore-replay-lpt-unchanged is used by recovery,
persistence-base/abs-gstore-set-lebsize is used by refine-sync, refine-add-gnds,
persistence-base/abs-gstore-set-refsize is used by refine-set-gblock-refsize,
persistence-base/abs-istore-avol-change-other is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
persistence-base/abs-istore-lpt-change-other is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-set-gblock-refsize,
persistence-base/abs-istore-reduce-write is used by refine-add-ind, refine-allocate-ind,
persistence-base/abs-istore-replay-lpt-unchanged is used by recovery,
persistence-base/abs-istore-set-lebsize is used by refine-sync, refine-add-ind,
persistence-base/abs-istore-set-refsize is used by refine-set-iblock-refsize,
persistence-base/abs-nodes-inv-flashsize-h is used by refine-add-gnds,
persistence-base/avol-replay-lpt-unchanged-size is used by recovery,
persistence-base/bin-heap-inv-write-other is used by refine-add-ind,
persistence-base/bin-heap-inv-write-other-fields is used by refine-sync, refine-add-gnds, refine-deallocate-gnd, refine-set-gblock-refsize,
persistence-base/buf-ro-rw-mode-leb-size is used by refine-sync, refine-add-ind, refine-add-gnds,
persistence-base/buf-ro-rw-mode-nobuffer is used by refine-get-block-free-size, refine-sync, recovery, refine-commit,
persistence-base/buf-ro-rw-mode-switch is used by refine-sync, refine-add-ind, refine-add-gnds, refine-commit,
persistence-base/buf-ro-rw-mode-write is used by refine-sync, refine-add-ind, refine-add-gnds,
persistence-base/bufs-log-only-empty is used by refine-get-block-free-size, refine-sync, recovery, refine-commit,
persistence-base/bufs-log-only-notfree is used by refine-sync, refine-allocate-ind, refine-allocate-gnd,
persistence-base/bufs-log-only-rembuf is used by refine-commit,
persistence-base/bufs-log-only-write-lpt-same-flags is used by refine-sync, refine-add-ind, refine-add-gnds,
persistence-base/free-unref-at is used by refine-commit, refine-allocate-ind, refine-allocate-gnd,
persistence-base/freelist-cons-first-free is used by refine-allocate-ind, refine-allocate-gnd,
persistence-base/freelist-cons-write-lpt-other is used by refine-sync, refine-add-ind, refine-add-gnds,
persistence-base/gc-heap-write-nochange is used by refine-sync, refine-add-gnds,
persistence-base/gc-heap-write-other is used by refine-sync, refine-add-ind,
persistence-base/id-idx-abs-gstore is used by recovery, refine-commit, refine-deallocate-gnd, refine-set-gblock-refsize,
persistence-base/id-idx-abs-istore is used by recovery, refine-commit, refine-deallocate-gnd, refine-set-gblock-refsize,
persistence-base/id-idx-freelist-cons is used by recovery, refine-commit,
persistence-base/id-idx-gcheap is used by recovery, refine-commit,
persistence-base/id-idx-lpt-free-unref is used by recovery, refine-commit,
persistence-base/log-disjoint-istore is used by recovery,
persistence-base/log-group-block-empty is used by refine-commit,
persistence-base/log-group-block-write-at is used by refine-sync, refine-add-gnds,
persistence-base/log-group-block-write-other is used by refine-sync, refine-add-ind,
persistence-base/lpt-free-unref-cleanup-lpt is used by refine-commit,
persistence-base/lpt-free-unref-replay-log is used by recovery,
persistence-base/lpt-free-unref-replay-lpt is used by recovery,
persistence-base/lpt-free-unref-write is used by refine-sync, refine-add-ind, refine-add-gnds,
persistence-base/lpt-leb-size-at is used by refine-get-block-free-size,
persistence-base/lpt-leb-size-id-idx is used by recovery, refine-commit,
persistence-base/lpt-leb-size-write is used by refine-sync, refine-add-ind, refine-add-gnds,
persistence-base/lpt-ram-flash-write-allocate is used by refine-add-gnds,
persistence-base/replay-log-size is used by recovery,

Used from specification array-copy

array-copy/lp-array/at-fill-mkarray is used by initialization,
array-copy/avolume/size-fill is used by initialization,
array-copy/lp-array/size-fill is used by initialization,
array-copy/buffer/size-subarray is used by refine-sync, refine-add-ind, refine-add-gnds,
array-copy/buffer/subarray-elim is used by refine-sync, refine-add-ind, refine-add-gnds,
array-copy/buffer/subarray-zero is used by refine-add-ind,

Used from specification list-dup

list-dup/nat-list-set/e-01 is used by refine-commit,
list-dup/nat-list-set/f is used by refine-sync, refine-add-gnds, refine-allocate-ind,

Used from specification address-data

address-data/elim is used by refine-read-ind, refine-read-gnd,
address-data/sel-03 is used by refine-add-ind, refine-read-ind, refine-read-gnd,
address-data/sel-04 is used by refine-add-ind, refine-read-ind, refine-read-gnd,
address-data/sel-05 is used by refine-add-ind, refine-read-ind, refine-read-gnd,

Used from specification abs-node

abs-node/encoding-index-node/abs-node-subarray-failed is used by refine-add-ind,
abs-node/encoding-index-node/abs-padding-subarray-failed is used by refine-sync,
abs-node/encoding-index-node/encode-node is used by refine-add-ind,
abs-node/encoding-group-node/abs-node-unique is used by refine-read-gnd,
abs-node/encoding-index-node/abs-node-unique is used by refine-add-ind, refine-read-ind,
abs-node/encoding-index-node/buf-size-zero is used by refine-sync, refine-add-ind, refine-allocate-ind,

Used from specification bufleb

bufleb/disj is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, initialization, recovery, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
bufleb/elim-is-buf-ant is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind,
bufleb/elim-is-buf-suc is used by refine-get-block-free-size, refine-sync,
bufleb/inj is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
bufleb/sel is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind,
bufleb/test-01 is used by refine-sync,
bufleb/test-02 is used by refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind,

Used from specification eraseblock

eraseblock/lebsize-neq-zero is used by refine-sync, refine-allocate-ind, refine-allocate-gnd,
eraseblock/lebsize-page-size-is-aligned is used by refine-sync, refine-add-ind, refine-add-gnds,
eraseblock/page-size is used by refine-sync, refine-add-ind, refine-add-gnds,
eraseblock/page-size-rewrite-sum is used by refine-sync,

Used from specification nat-mult

nat-mult/dist-sub-04 is used by refine-add-ind,
nat-mult/mult-a is used by refine-sync, refine-add-ind,
nat-mult/mult-c is used by refine-sync, refine-add-ind,
nat-mult/two-zero-01 is used by refine-add-ind,
nat-mult/zero is used by refine-add-ind,

Used from specification oelem

oelem/gc-heap-rename-gc-heap-base-binheap-key/irreflexivity is used by refine-add-ind, refine-add-gnds, recovery, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-iblock-refsize, refine-get-gblock-refsize, refine-set-iblock-refsize, refine-set-gblock-refsize,

Used from specification awbuf-inv

awbuf-inv/awbuf-inv-crash is used by recovery,
awbuf-inv/down-arrow-size0 is used by recovery,
awbuf-inv/inv-aligned-synced is used by refine-sync,
awbuf-inv/inv-buf-in-vol is used by refine-get-block-free-size, refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd,
awbuf-inv/inv-leb-size is used by refine-sync,
awbuf-inv/inv-nobuf-synced is used by refine-get-block-free-size, refine-sync, initialization, recovery, refine-commit,
awbuf-inv/inv-synced-write-buf is used by refine-sync, refine-add-ind, refine-add-gnds,
awbuf-inv/synced-aligned is used by refine-sync, refine-allocate-ind,
awbuf-inv/synced-down-synced is used by recovery,
awbuf-inv/synced-map is used by refine-allocate-ind, refine-allocate-gnd,
awbuf-inv/synced-unmap is used by refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,

Used from specification persistence-asm

persistence-asm/inv-add-gnds is used by refine-add-gnds,
persistence-asm/inv-add-ind is used by refine-add-ind,
persistence-asm/inv-commit is used by refine-commit,
persistence-asm/inv-get-gc-block is used by refine-get-gc-block,
persistence-asm/inv-read-gblock-nodes is used by refine-read-gblock-nodes,
persistence-asm/inv-read-gnd is used by refine-read-gnd,
persistence-asm/inv-read-ind is used by refine-read-ind,
persistence-asm/inv-recover is used by recovery,
persistence-asm/inv-sync is used by refine-sync,
persistence-asm/prepost-cleanup-lpt is used by refine-commit,
persistence-asm/prepost-create-freelist is used by initialization, recovery,
persistence-asm/prepost-create-gcheap is used by recovery,
persistence-asm/prepost-encode-group-nodes is used by refine-add-gnds,
persistence-asm/prepost-encode-padding is used by refine-sync,
persistence-asm/prepost-gcheap-add-log is used by refine-commit,
persistence-asm/prepost-replay-log is used by recovery,
persistence-asm/prepost-replay-lpt is used by recovery,
persistence-asm/elim-lp-upd-size is used by refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
persistence-asm/elim-mapped is used by refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,
persistence-asm/flush-padding-space-aligned is used by refine-sync,
persistence-asm/flush-padding-space-header is used by refine-sync,

Used from specification oset

oset/nat-set/ls-add is used by refine-deallocate-gnd,
oset/nat-set/ls-emptyset is used by initialization, refine-commit,
oset/nat-set/ls-rm is used by refine-allocate-gnd,

Used from specification elem-index

elem-index/gc-heap-base/sel-01-M01 is used by fwd-in-istore-lpt, fwd-in-gstore-lpt, refine-sync, refine-add-ind, refine-add-gnds, initialization, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-set-gblock-refsize, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,
elem-index/gc-heap-base/sel-01-M02 is used by refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,
elem-index/gc-heap-base/sel-01-M03 is used by fwd-in-istore-lpt, fwd-in-gstore-lpt, refine-sync, refine-add-ind, refine-add-gnds, initialization, refine-commit, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-get-iblock-refsize, refine-get-gblock-refsize, refine-set-iblock-refsize, refine-set-gblock-refsize, refine-get-gc-block, refine-read-gblock-nodes, refine-read-ind, refine-read-gnd,
elem-index/gc-heap-base/sel-02 is used by refine-sync, refine-add-ind, refine-add-gnds, refine-deallocate-gnd, refine-allocate-gnd,

Used from specification array

array/lp-array/Put-other is used by refine-sync, refine-add-ind, refine-deallocate-gnd, refine-allocate-gnd,
array/avolume/Put-other is used by refine-sync, refine-add-ind, refine-deallocate-gnd, refine-allocate-gnd,
array/lp-array/Put-same is used by refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
array/avolume/Put-same is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-allocate-gnd,
array/lp-array/Size-mkarray is used by initialization,
array/buffer/Size-mkarray is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-allocate-gnd,
array/avolume/Size-mkarray is used by initialization,
array/lp-array/Size-put is used by refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd, refine-set-iblock-refsize, refine-set-gblock-refsize,
array/avolume/Size-put is used by refine-sync, refine-add-ind, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd,
array/lp-array/cgetput is used by refine-sync, refine-add-ind, refine-deallocate-gnd, refine-allocate-gnd,
array/avolume/cngetput is used by refine-allocate-ind,
array/lp-array/cputput is used by refine-allocate-ind, refine-deallocate-gnd, refine-allocate-gnd,
array/lp-array/put-same-content is used by refine-add-ind,

Used from specification nat-div

nat-div/mod-le-02 is used by refine-sync,
nat-div/mod-same is used by refine-sync,

Used from specification abs-leb

abs-leb/encoding-index-node/abs-leb-def is used by refine-sync, refine-add-ind, refine-allocate-ind, refine-read-ind,
abs-leb/encoding-group-node/abs-leb-def is used by refine-sync, refine-add-gnds, refine-allocate-ind, refine-allocate-gnd, refine-read-gblock-nodes, refine-read-gnd,

Used from specification debug

debug/debug is used by refine-sync, refine-add-gnds, initialization, recovery,

Used from specification array-indices

array-indices/lp-array/valid-indices-nonrec is used by recovery,

Used from specification index-array

index-array/gc-heap-base/id-idx is used by refine-deallocate-gnd, refine-set-gblock-refsize,

Used from specification bin-min-heap-prepost

bin-min-heap-prepost/gc-heap-rename-gc-heap-base/prepost-remove is used by refine-deallocate-gnd,
bin-min-heap-prepost/gc-heap-rename-gc-heap-base/prepost-update is used by refine-set-gblock-refsize,

Used from specification awbuf-asm

awbuf-asm/inv-destroy-buf is used by refine-commit,
awbuf-asm/inv-format is used by initialization,
awbuf-asm/inv-write-buf is used by refine-add-ind,