Used simplifier rules/spec theorems by specification

Used from specification nat-basic

• nat-basic/addex is used by range-eq-validtrailer,
• nat-basic/c is used by prepost-encode-group-nodes,
• nat-basic/a is used by range-eq-validtrailer, prepost-replay-lpt, prepost-replay-log, prepost-gcheap-add-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, nat-stuff0, isprefix-size, flush-padding-space-write, flush-padding-space-header, adrlist-append-eq-size1, adrlist-append-eq-size, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat-basic/add-base is used by range-eq-validtrailer, prepost-encode-padding, prepost-create-freelist, nat-stuff0, flush-padding-space-write, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat-basic/c is used by range-eq-validtrailer, prepost-replay-lpt, prepost-replay-log, prepost-gcheap-add-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, nat-stuff0, isprefix-size, flush-padding-space-write, flush-padding-space-header, adrlist-append-eq-size1, adrlist-append-eq-size, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat-basic/eq-01 is used by prepost-encode-group-nodes, inv-sync, inv-add-gnds, inv-add-ind, inv-read-gblock-nodes,
• nat-basic/eq-02 is used by prepost-encode-group-nodes, adrlist-append-eq-size, inv-read-gblock-nodes,
• nat-basic/eqs is used by inv-sync, inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,
• nat-basic/f is used by range-eq-validtrailer, prepost-replay-lpt, prepost-replay-log, prepost-gcheap-add-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, isprefix-size, id-idx-cleanup-lpt-backwards-fwd, flush-padding-space-write, adrlist-append-eq-size1, inv-get-block-free-size, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-commit, inv-recover, inv-set-iblock-refsize, inv-get-iblock-refsize, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat-basic/l is used by prepost-replay-lpt, prepost-encode-padding, prepost-encode-group-nodes, prepost-cleanup-lpt, inv-sync, inv-add-ind, inv-read-gblock-nodes,
• nat-basic/l-01 is used by range-eq-validtrailer, prepost-replay-lpt, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-cleanup-lpt, nat-stuff0, flush-padding-space-write, inv-sync, inv-read-gblock-nodes,
• nat-basic/l-02 is used by range-eq-validtrailer, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-cleanup-lpt, isprefix-size, adrlist-append-eq-size1, inv-sync, inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,
• nat-basic/lf is used by prepost-replay-lpt, prepost-encode-padding, prepost-cleanup-lpt, inv-recover, inv-read-gblock-nodes,
• nat-basic/lf-01 is used by prepost-replay-lpt, prepost-gcheap-add-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-cleanup-lpt, id-idx-cleanup-lpt-backwards-fwd, inv-get-block-free-size, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-commit, inv-recover, inv-set-iblock-refsize, inv-get-iblock-refsize, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat-basic/lf-02 is used by prepost-replay-lpt, prepost-gcheap-add-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, isprefix-size, adrlist-append-eq-size1, inv-read-ind, inv-read-gnd, inv-recover, inv-read-gblock-nodes,
• nat-basic/ls-02 is used by prepost-replay-lpt, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-freelist, inv-recover, inv-read-gblock-nodes,
• nat-basic/nls-fst is used by inv-read-gblock-nodes,
• nat-basic/one is used by inv-read-gblock-nodes,
• nat-basic/one-01 is used by prepost-replay-log, prepost-encode-group-nodes,
• nat-basic/one-03 is used by inv-read-gblock-nodes,
• nat-basic/oz is used by prepost-encode-group-nodes,
• nat-basic/s-04 is used by prepost-replay-lpt, prepost-replay-log, prepost-gcheap-add-log, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt,
• nat-basic/succ is used by prepost-replay-lpt, prepost-gcheap-add-log, prepost-encode-group-nodes, prepost-cleanup-lpt, inv-read-gblock-nodes,
• nat-basic/z-01 is used by inv-read-gblock-nodes,
• nat-basic/zero is used by inv-get-gc-block, inv-read-gblock-nodes,
• nat-basic/zero-01 is used by prepost-create-freelist,

Used from specification array-splice

• array-splice/buffer/append-at is used by range-eq-validtrailer, prepost-encode-padding,
• array-splice/buffer/array-split-elim-size is used by prepost-encode-group-nodes,
• array-splice/buffer/emparray-at is used by range-eq-validtrailer,
• array-splice/buffer/range-eq-ext is used by range-eq-validtrailer, inv-read-gblock-nodes,
• array-splice/buffer/range-eq-subarrays is used by range-eq-validtrailer,
• array-splice/buffer/subarray-elim-right is used by inv-read-gblock-nodes,
• array-splice/buffer/append-a is used by range-eq-validtrailer, prepost-encode-padding, prepost-encode-group-nodes, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-add-ind, inv-read-gblock-nodes,
• array-splice/buffer/append-left-size0 is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• array-splice/buffer/append-len is used by range-eq-validtrailer, prepost-encode-padding, prepost-encode-group-nodes, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-add-ind, inv-read-gblock-nodes,
• array-splice/buffer/append-zero-left is used by inv-read-gblock-nodes,
• array-splice/buffer/append-zero-right is used by inv-read-gblock-nodes,
• array-splice/buffer/emparray-len is used by range-eq-validtrailer, inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,
• array-splice/buffer/range-eq-0 is used by inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,
• array-splice/buffer/range-eq-shift-right is used by inv-read-gblock-nodes,
• array-splice/buffer/subarray-append-elim is used by prepost-encode-group-nodes,
• array-splice/buffer/subarray-append-elim-left is used by range-eq-validtrailer, prepost-encode-group-nodes, inv-read-gblock-nodes,
• array-splice/buffer/subarray-append-elim-left0-simp is used by inv-read-gblock-nodes,
• array-splice/buffer/subarray-append-left is used by prepost-encode-group-nodes,
• array-splice/buffer/subarray-elim-right is used by range-eq-validtrailer, inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,

Used from specification node-header-size

• node-header-size/2-node-header-size-add-eq-0 is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• node-header-size/node-header-size-add-eq-0 is used by range-eq-validtrailer, prepost-encode-padding, inv-read-gblock-nodes,
• node-header-size/node-header-size-ls-2-node-header-size is used by prepost-encode-padding,
• node-header-size/nodeheader-notzero is used by range-eq-validtrailer, prepost-encode-padding, flush-padding-space-header, flush-padding-space-aligned, inv-read-gblock-nodes,
• node-header-size/nodeheader-pagesize is used by flush-padding-space-aligned,
• node-header-size/validtrailer-not-empty is used by range-eq-validtrailer,
• node-header-size/validtrailer-size is used by range-eq-validtrailer, prepost-encode-padding, inv-read-gblock-nodes,

Used from specification encoding-node-base

• encoding-node-base/encoding-group-node/is-aligned-alignedsize is used by inv-read-gblock-nodes,
• encoding-node-base/encoding-index-node/node-flash-size is used by inv-read-ind, inv-add-ind,
• encoding-node-base/encoding-group-node/node-flash-size is used by prepost-encode-group-nodes, inv-read-gnd, inv-read-gblock-nodes,

Used from specification ablock-store-inv

• ablock-store-inv/group-store/size-append is used by prepost-encode-group-nodes,
• ablock-store-inv/group-store/size-base is used by prepost-encode-group-nodes,
• ablock-store-inv/group-store/size-one is used by prepost-encode-group-nodes,
• ablock-store-inv/group-store/size-rec is used by prepost-encode-group-nodes,
• ablock-store-inv/group-store/to-adrs-eq is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• ablock-store-inv/group-store/to-adrs-eq-app is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• ablock-store-inv/group-store/to-adrs-eq-empty is used by prepost-encode-group-nodes, inv-read-gblock-nodes,

Used from specification set-union

• set-union/gc-heap-rename-gc-heap-base-keyindex-set/One is used by prepost-create-gcheap,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/del-in is used by prepost-gcheap-add-log,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/delete-insert is used by prepost-gcheap-add-log,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/una is used by prepost-create-gcheap,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/unadd is used by prepost-create-gcheap,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/unc is used by prepost-create-gcheap,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/une is used by prepost-create-gcheap,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/uneq is used by prepost-create-gcheap,

Used from specification gc-heap-rename

• gc-heap-rename/id-idx-fwd-0 is used by prepost-gcheap-add-log, prepost-create-gcheap,
• gc-heap-rename/id-idx-fwd-1 is used by prepost-cleanup-lpt,
• gc-heap-rename/id-idx-imp-ls-0 is used by prepost-gcheap-add-log,
• gc-heap-rename/id-idx-imp-ls-1 is used by prepost-create-gcheap,
• gc-heap-rename/id-idx-len-eq-0 is used by prepost-cleanup-lpt, inv-commit,
• gc-heap-rename/id-idx-ls0 is used by prepost-create-gcheap, prepost-cleanup-lpt,

Used from specification bin-min-heap

• bin-min-heap/gc-heap-base/elim is used by prepost-gcheap-add-log, prepost-create-gcheap, prepost-cleanup-lpt, inv-get-gc-block,
• bin-min-heap/gc-heap-base/sel-01 is used by prepost-gcheap-add-log, prepost-create-gcheap, inv-get-gc-block, inv-format,
• bin-min-heap/gc-heap-base/sel-02 is used by prepost-create-gcheap, inv-get-gc-block, inv-format,

Used from specification nat

• nat/le-addex is used by inv-sync,
• nat/add-01 is used by inv-read-gblock-nodes,
• nat/anti is used by prepost-replay-lpt, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, inv-read-gblock-nodes,
• nat/cancel-01 is used by prepost-encode-group-nodes, inv-add-ind,
• nat/elim-sub is used by range-eq-validtrailer, prepost-replay-lpt, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-cleanup-lpt, inv-sync, inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,
• nat/eq-01 is used by prepost-encode-padding, prepost-encode-group-nodes,
• nat/eq-02 is used by inv-sync, inv-read-gblock-nodes,
• nat/fle is used by range-eq-validtrailer, prepost-replay-lpt, prepost-encode-padding, prepost-encode-group-nodes, prepost-cleanup-lpt, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-recover, inv-set-iblock-refsize, inv-get-iblock-refsize, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat/fle-01 is used by range-eq-validtrailer, prepost-replay-lpt, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-freelist, prepost-cleanup-lpt, flush-padding-space-write, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-set-iblock-refsize, inv-get-iblock-refsize, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat/ge is used by prepost-encode-padding, inv-get-block-free-size, inv-sync, inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,
• nat/gr-def is used by inv-read-gblock-nodes,
• nat/le is used by prepost-encode-padding, inv-sync,
• nat/le-add is used by range-eq-validtrailer, prepost-replay-lpt, prepost-cleanup-lpt, inv-read-gblock-nodes,
• nat/le-def is used by range-eq-validtrailer, prepost-replay-lpt, prepost-replay-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-cleanup-lpt, flush-padding-space-header, inv-get-block-free-size, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-recover, inv-set-iblock-refsize, inv-set-gblock-refsize, inv-add-ind, inv-read-gblock-nodes,
• nat/le-ls-simp is used by prepost-replay-lpt, prepost-replay-log, prepost-gcheap-add-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-cleanup-lpt, inv-get-block-free-size, inv-sync, inv-recover, inv-allocate-ind, inv-add-ind, inv-read-gblock-nodes,
• nat/lels is used by range-eq-validtrailer, prepost-replay-lpt, prepost-replay-log, prepost-gcheap-add-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, flush-padding-space-write, inv-get-block-free-size, inv-sync, inv-add-gnds, inv-recover, inv-set-iblock-refsize, inv-get-iblock-refsize, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat/lels-02 is used by prepost-encode-padding, prepost-create-freelist,
• nat/lels-03 is used by prepost-replay-lpt, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, id-idx-cleanup-lpt-backwards-fwd, inv-sync, inv-add-gnds, inv-add-ind, inv-read-gblock-nodes,
• nat/lep is used by range-eq-validtrailer, prepost-encode-padding, prepost-encode-group-nodes, inv-sync, inv-read-gblock-nodes,
• nat/lep-02 is used by range-eq-validtrailer, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, inv-read-ind, inv-read-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat/ler is used by range-eq-validtrailer, prepost-replay-lpt, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, id-idx-cleanup-lpt-backwards-fwd, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-recover, inv-add-ind, inv-read-gblock-nodes,
• nat/let is used by range-eq-validtrailer, flush-padding-space-write, inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,
• nat/lez is used by range-eq-validtrailer, prepost-replay-lpt, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-format,
• nat/lez-01 is used by inv-read-gblock-nodes,
• nat/ls is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• nat/ls-01 is used by prepost-replay-lpt, prepost-replay-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, inv-read-gblock-nodes,
• nat/ls-05 is used by inv-read-gblock-nodes,
• nat/ls-le-simp is used by range-eq-validtrailer, prepost-replay-lpt, prepost-replay-log, prepost-encode-padding, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, inv-get-block-free-size, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-recover, inv-set-iblock-refsize, inv-set-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind, inv-read-gblock-nodes,
• nat/not-zero is used by prepost-encode-group-nodes,
• nat/pred-03 is used by prepost-replay-log, inv-read-gblock-nodes,
• nat/prop-07 is used by prepost-replay-lpt, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, inv-read-gblock-nodes,
• nat/sub-add is used by prepost-encode-group-nodes,
• nat/sub-ls is used by inv-read-gblock-nodes,
• nat/succ-01 is used by prepost-replay-lpt, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt,
• nat/zero is used by prepost-encode-group-nodes, inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,
• nat/zero-01 is used by prepost-cleanup-lpt,

Used from specification error-class

• error-class/ecommit is used by inv-read-ind, inv-read-gnd, inv-commit, inv-read-gblock-nodes,
• error-class/enoent is used by inv-read-gblock-nodes,
• error-class/erofs is used by inv-commit,
• error-class/esuccess is used by inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-commit, inv-recover, inv-allocate-gnd, inv-allocate-ind, inv-format, inv-add-ind, inv-read-gblock-nodes,
• error-class/not-esuccess is used by inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-commit, inv-recover, inv-allocate-gnd, inv-allocate-ind, inv-format, inv-add-ind, inv-read-gblock-nodes,

Used from specification abs-list

• abs-list/encoding-group-node/abs-nodes is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-nospace-header-h is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-notrailer-h is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-valid-node is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-aligned-headersize-h is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-append-empty-h is used by prepost-encode-group-nodes,
• abs-list/encoding-group-node/abs-nodes-append-h is used by prepost-encode-group-nodes,
• abs-list/encoding-group-node/abs-nodes-elems-adr-length is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-elems-adr-length-h is used by prepost-encode-group-nodes, inv-add-gnds, inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-emptyheader-h is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-headerspace is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-mkbuf0-empty is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-mkbuf0-empty-h is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-nospace-h is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-one-abs-node is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-prefix-elim is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-unique-strong is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-unique-weak is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-nodes-unique-weak-h is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/abs-padding-abs-nodes-h is used by inv-read-gblock-nodes,
• abs-list/encoding-group-node/flashsize-eq-0 is used by inv-add-gnds,

Used from specification error

• error/disj-120 is used by inv-commit, inv-allocate-gnd, inv-allocate-ind,
• error/disj-33 is used by inv-read-gblock-nodes,
• error/disj-35 is used by inv-get-gc-block, inv-allocate-gnd, inv-allocate-ind,
• error/disj-91 is used by inv-read-ind, inv-read-gnd, inv-commit, inv-read-gblock-nodes,

Used from specification aleb

• aleb/ex is used by elim-mapped,
• aleb/aleb-not-mapped is used by inv-sync, inv-read-gblock-nodes,
• aleb/disj is used by inv-sync, inv-read-gblock-nodes,
• aleb/inj is used by flush-padding-space-write, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-add-ind, inv-read-gblock-nodes,
• aleb/sel is used by flush-padding-space-write, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-allocate-gnd, inv-allocate-ind, inv-add-ind, inv-read-gblock-nodes,
• aleb/test-02 is used by flush-padding-space-write, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-allocate-gnd, inv-allocate-ind, inv-add-ind, inv-read-gblock-nodes,

Used from specification lprops

• lprops/disj-01 is used by prepost-cleanup-lpt, inv-sync, inv-add-gnds, inv-recover, inv-set-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd,
• lprops/disj-02 is used by inv-recover, inv-set-iblock-refsize, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• lprops/disj-03 is used by prepost-replay-lpt, inv-recover, inv-set-iblock-refsize, inv-allocate-ind, inv-add-ind,
• lprops/elim is used by prepost-replay-lpt, prepost-gcheap-add-log, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, elim-lp-upd-size, inv-get-block-free-size, inv-sync, inv-add-gnds, inv-commit, inv-recover, inv-set-iblock-refsize, inv-get-iblock-refsize, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-get-gc-block, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• lprops/inj is used by prepost-create-freelist, prepost-cleanup-lpt, inv-sync, inv-add-gnds, inv-recover, inv-allocate-gnd,
• lprops/upd-04 is used by inv-set-iblock-refsize, inv-set-gblock-refsize, inv-allocate-gnd, inv-allocate-ind,
• lprops/upd-05 is used by prepost-replay-lpt, elim-lp-upd-size,
• lprops/upd-06 is used by prepost-replay-lpt, inv-allocate-gnd, inv-allocate-ind,
• lprops/updsel-01 is used by prepost-replay-lpt, prepost-replay-log, prepost-cleanup-lpt, inv-deallocate-gnd,
• lprops/updsel-03 is used by inv-set-iblock-refsize, inv-set-gblock-refsize, inv-deallocate-gnd,
• lprops/updsel-06 is used by inv-set-iblock-refsize, inv-set-gblock-refsize,
• lprops/updsel-07 is used by prepost-replay-lpt, prepost-replay-log, prepost-cleanup-lpt,
• lprops/updsel-09 is used by inv-set-iblock-refsize, inv-set-gblock-refsize, inv-deallocate-gnd,
• lprops/updsel-13 is used by inv-deallocate-gnd,
• lprops/updsel-15 is used by prepost-replay-lpt, prepost-replay-log, prepost-cleanup-lpt, inv-deallocate-gnd,

Used from specification set-basic

• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/Extension is used by prepost-gcheap-add-log,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/eq-03 is used by prepost-gcheap-add-log,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/ne-01 is used by prepost-gcheap-add-log, prepost-create-gcheap, prepost-cleanup-lpt, inv-set-gblock-refsize, inv-deallocate-gnd,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/size-zero-01 is used by prepost-gcheap-add-log, prepost-create-gcheap, prepost-cleanup-lpt, inv-set-gblock-refsize, inv-deallocate-gnd,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/sub-e is used by prepost-create-gcheap,

Used from specification list-last

• list-last/laddress-list/prefix is used by isprefix-size,
• list-last/nat-list-set/last-def is used by inv-allocate-gnd,
• list-last/nat-list-set/lin-01 is used by inv-deallocate-gnd,
• list-last/nat-list-set/lin-02 is used by inv-deallocate-gnd,

Used from specification key-index

• key-index/gc-heap-rename-gc-heap-base/elim is used by prepost-gcheap-add-log, prepost-create-gcheap, inv-get-gc-block,
• key-index/gc-heap-rename-gc-heap-base/sel-01 is used by prepost-gcheap-add-log, prepost-create-gcheap,

Used from specification list-data

• list-data/nat-list-set/elim-list-c is used by prepost-replay-log, prepost-gcheap-add-log, inv-allocate-gnd, inv-allocate-ind,
• list-data/laddress-list/elim-list-c is used by inv-read-gblock-nodes,
• list-data/group-store/elim-list-c is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list-data/laddress-list/l is used by prepost-encode-group-nodes, isprefix-size, adrlist-append-eq-size1, adrlist-append-eq-size, inv-read-gblock-nodes,
• list-data/nat-list-set/l is used by prepost-replay-log,
• list-data/group-store/l is used by prepost-encode-group-nodes,
• list-data/nat-list-set/length-rest is used by prepost-replay-log,
• list-data/laddress-list/length-rest is used by inv-read-gblock-nodes,
• list-data/group-store/length-rest is used by inv-read-gblock-nodes,
• list-data/laddress-list/size-01 is used by inv-read-gblock-nodes,
• list-data/group-store/size-01 is used by inv-read-gblock-nodes,

Used from specification index-array

• index-array/gc-heap-base/id-idx is used by prepost-gcheap-add-log, prepost-create-gcheap, prepost-cleanup-lpt, id-idx-cleanup-lpt-backwards-fwd, inv-commit, inv-recover, inv-set-gblock-refsize, inv-deallocate-gnd,
• index-array/gc-heap-base/id-idx-refl is used by prepost-gcheap-add-log, prepost-create-gcheap, prepost-cleanup-lpt,
• index-array/gc-heap-base/id-idx-trans is used by prepost-gcheap-add-log, prepost-create-gcheap, prepost-cleanup-lpt,

Used from specification array-indices

• array-indices/lp-array/valid-indices-nonrec is used by inv-recover,
• array-indices/lp-array/valid-indices-append is used by prepost-replay-log,
• array-indices/lp-array/valid-indices-one is used by prepost-replay-log,
• array-indices/lp-array/valid-indices-write is used by prepost-replay-log,

Used from specification laddress

• laddress/inj is used by prepost-encode-group-nodes, inv-read-gblock-nodes,

Used from specification bin-min-heap-inv

• bin-min-heap-inv/gc-heap-rename-gc-heap-base/2exp-size-0 is used by inv-get-gc-block,
• bin-min-heap-inv/gc-heap-rename-gc-heap-base/2exp-size-1 is used by prepost-create-gcheap, inv-format,
• bin-min-heap-inv/gc-heap-rename-gc-heap-base/heap-order-0 is used by prepost-create-gcheap, inv-format,
• bin-min-heap-inv/gc-heap-rename-gc-heap-base/no-dups-idx-0 is used by prepost-create-gcheap, inv-format,
• bin-min-heap-inv/gc-heap-rename-gc-heap-base/valid-idx-0 is used by prepost-create-gcheap, inv-format,

Used from specification align

• align/between-is-aligned is used by flush-padding-space-write,
• align/is-aligned-add is used by flush-padding-space-aligned,
• align/is-aligned-aligndown-zero-ls is used by flush-padding-space-header,
• align/is-aligned-intro is used by flush-padding-space-aligned,
• align/is-aligned-is-aligned-mod is used by flush-padding-space-aligned,
• align/align-down-add-to-align-up is used by flush-padding-space-write,
• align/aligndown-is-aligned is used by flush-padding-space-write,
• align/aligndown-le is used by flush-padding-space-write,
• align/alignup-calc is used by flush-padding-space-write,
• align/alignup-same is used by inv-read-gblock-nodes,
• align/is-aligned-add is used by range-eq-validtrailer, prepost-encode-padding, inv-sync, inv-add-gnds, inv-add-ind, inv-read-gblock-nodes,
• align/is-aligned-align-up-multiple is used by inv-read-gblock-nodes,
• align/is-aligned-le-eq-zero is used by range-eq-validtrailer, prepost-encode-padding, inv-read-gblock-nodes,
• align/is-aligned-ls-eq-zero is used by range-eq-validtrailer, prepost-encode-padding, inv-read-gblock-nodes,
• align/is-aligned-mod is used by flush-padding-space-write,
• align/is-aligned-multiplier is used by inv-read-gblock-nodes,
• align/is-aligned-same is used by prepost-encode-padding, inv-read-gblock-nodes,
• align/is-aligned-zero is used by inv-read-gblock-nodes,

Used from specification encoding-fixed-size-nonempty

• encoding-fixed-size-nonempty/encoding-node-header/decode-contract is used by inv-read-gblock-nodes,
• encoding-fixed-size-nonempty/encoding-node-header/encode-contract is used by prepost-encode-padding,
• encoding-fixed-size-nonempty/encoding-node-header/is-encoded-unique is used by prepost-encode-padding, inv-read-gblock-nodes,

Used from specification persistence-base

• persistence-base/avol-cleanup-lpt-unchanged is used by prepost-cleanup-lpt, inv-commit,
• persistence-base/buf-ro-rw-mode is used by inv-allocate-gnd,
• persistence-base/bufs-log-only is used by inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd,
• persistence-base/freelist-cons is used by prepost-create-freelist,
• persistence-base/freelist-cons-add is used by prepost-cleanup-lpt, inv-deallocate-gnd,
• persistence-base/gc-heap is used by prepost-create-gcheap,
• persistence-base/gc-heap-append-log is used by prepost-gcheap-add-log,
• persistence-base/gc-heap-free is used by prepost-cleanup-lpt,
• persistence-base/gc-heap-in is used by prepost-gcheap-add-log, prepost-cleanup-lpt, inv-set-gblock-refsize, inv-get-gc-block, inv-deallocate-gnd,
• persistence-base/gc-heap-in-h is used by prepost-create-gcheap,
• persistence-base/gc-heap-rec is used by prepost-create-gcheap,
• persistence-base/gc-heap-write-other is used by prepost-cleanup-lpt, inv-sync,
• persistence-base/id-idx-write-both is used by prepost-cleanup-lpt,
• persistence-base/log-group-block is used by inv-commit, inv-recover, inv-allocate-gnd, inv-deallocate-gnd,
• persistence-base/log-group-block-id-idx is used by inv-recover, inv-set-gblock-refsize, inv-deallocate-gnd,
• persistence-base/log-group-block-write-other is used by inv-sync,
• persistence-base/lpt-free-unref is used by inv-format,
• persistence-base/lpt-leb-size is used by inv-recover, inv-format,
• persistence-base/lpt-leb-size-cleanup is used by inv-commit,
• persistence-base/lpt-ram-flash is used by inv-recover,
• persistence-base/lpt-ram-flash-cleanup is used by inv-commit,
• persistence-base/lpt-ram-flash-id-idx is used by inv-commit, inv-set-gblock-refsize,
• persistence-base/lpt-ram-flash-write-same is used by inv-set-gblock-refsize,
• persistence-base/read-gblock-inv is used by inv-read-gblock-nodes,
• persistence-base/replay-log-at is used by inv-recover,
• persistence-base/replay-lpt-at is used by inv-recover,
• persistence-base/avol-cleanup-lpt-unchanged-refl is used by prepost-cleanup-lpt,
• persistence-base/avol-replay-lpt-unchanged-refl is used by prepost-replay-lpt,
• persistence-base/avol-replay-lpt-unchanged-size is used by prepost-replay-lpt, inv-recover,
• persistence-base/avol-replay-lpt-unchanged-write-right is used by prepost-replay-lpt,
• persistence-base/bin-heap-inv-write-other is used by inv-allocate-gnd, inv-allocate-ind, inv-add-ind,
• persistence-base/bin-heap-inv-write-other-fields is used by prepost-cleanup-lpt, inv-sync, inv-add-gnds, inv-set-iblock-refsize, inv-set-gblock-refsize, inv-deallocate-gnd,
• persistence-base/buf-ro-rw-mode-id-idx is used by inv-set-gblock-refsize, inv-deallocate-gnd,
• persistence-base/buf-ro-rw-mode-leb-size is used by inv-sync, inv-add-gnds, inv-add-ind,
• persistence-base/buf-ro-rw-mode-nobuffer is used by inv-commit, inv-recover, inv-format,
• persistence-base/buf-ro-rw-mode-switch is used by inv-sync, inv-add-gnds, inv-commit, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• persistence-base/buf-ro-rw-mode-write is used by inv-sync, inv-add-gnds, inv-allocate-gnd, inv-allocate-ind, inv-add-ind,
• persistence-base/buf-ro-rw-mode-write-lpt-other is used by inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd,
• persistence-base/buf-ro-rw-mode-write-other-fields is used by inv-set-iblock-refsize, inv-set-gblock-refsize,
• persistence-base/buf-ro-rw-mode-write-vol-other is used by inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd,
• persistence-base/bufs-log-only-empty is used by inv-commit, inv-recover, inv-format,
• persistence-base/bufs-log-only-id-idx is used by inv-set-gblock-refsize, inv-deallocate-gnd,
• persistence-base/bufs-log-only-notfree is used by inv-allocate-gnd, inv-allocate-ind,
• persistence-base/bufs-log-only-rembuf is used by inv-commit,
• persistence-base/bufs-log-only-write-lpt-same-flags is used by inv-sync, inv-add-gnds, inv-set-iblock-refsize, inv-set-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-add-ind,
• persistence-base/cleanup-lpt-base is used by prepost-cleanup-lpt,
• persistence-base/cleanup-lpt-n-read-above is used by prepost-cleanup-lpt, id-idx-cleanup-lpt-backwards-fwd,
• persistence-base/cleanup-lpt-n-size is used by prepost-cleanup-lpt, id-idx-cleanup-lpt-backwards-fwd,
• persistence-base/cleanup-lpt-rec is used by prepost-cleanup-lpt,
• persistence-base/cleanup-lpt-size is used by inv-commit,
• persistence-base/cleanup-lpt-to-n is used by prepost-cleanup-lpt,
• persistence-base/free-unref-at is used by inv-recover, inv-allocate-gnd, inv-allocate-ind,
• persistence-base/freelist-cons-alloc is used by inv-allocate-gnd, inv-allocate-ind,
• persistence-base/freelist-cons-first-free is used by inv-allocate-gnd, inv-allocate-ind,
• persistence-base/freelist-cons-write-lpt-other is used by inv-sync, inv-add-gnds, inv-set-iblock-refsize, inv-set-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-add-ind,
• persistence-base/gc-heap-allocate is used by inv-allocate-gnd,
• persistence-base/gc-heap-base is used by prepost-create-gcheap,
• persistence-base/gc-heap-fill-free is used by inv-format,
• persistence-base/gc-heap-free is used by inv-deallocate-gnd,
• persistence-base/gc-heap-ididx-h is used by prepost-create-gcheap,
• persistence-base/gc-heap-update is used by inv-set-gblock-refsize,
• persistence-base/gc-heap-update-log is used by inv-set-gblock-refsize,
• persistence-base/gc-heap-write-nochange is used by inv-sync, inv-add-gnds,
• persistence-base/gc-heap-write-other is used by inv-set-iblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-add-ind,
• persistence-base/id-idx-freelist-cons is used by prepost-cleanup-lpt, inv-commit, inv-recover, inv-set-gblock-refsize, inv-deallocate-gnd,
• persistence-base/id-idx-gcheap is used by prepost-gcheap-add-log, prepost-create-gcheap, prepost-cleanup-lpt, inv-commit, inv-recover, inv-set-gblock-refsize, inv-deallocate-gnd,
• persistence-base/id-idx-lpt-free-unref is used by inv-commit, inv-recover, inv-set-gblock-refsize, inv-deallocate-gnd,
• persistence-base/log-group-block-empty is used by inv-commit, inv-format,
• persistence-base/log-group-block-write-at is used by inv-sync, inv-add-gnds, inv-set-gblock-refsize,
• persistence-base/log-group-block-write-other is used by inv-sync, inv-set-iblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-add-ind,
• persistence-base/lpt-free-unref-cleanup-lpt is used by inv-commit,
• persistence-base/lpt-free-unref-replay-log is used by inv-recover,
• persistence-base/lpt-free-unref-replay-lpt is used by inv-recover,
• persistence-base/lpt-free-unref-write is used by inv-sync, inv-add-gnds, inv-set-iblock-refsize, inv-set-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• persistence-base/lpt-leb-size-at is used by inv-get-block-free-size, inv-recover, inv-set-iblock-refsize, inv-set-gblock-refsize,
• persistence-base/lpt-leb-size-id-idx is used by inv-commit, inv-recover, inv-set-gblock-refsize, inv-deallocate-gnd,
• persistence-base/lpt-leb-size-write is used by inv-sync, inv-add-gnds, inv-set-iblock-refsize, inv-set-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• persistence-base/lpt-ram-flash-allocate is used by inv-allocate-gnd,
• persistence-base/lpt-ram-flash-commit is used by inv-commit, inv-format,
• persistence-base/lpt-ram-flash-id-idx is used by inv-commit, inv-recover, inv-deallocate-gnd,
• persistence-base/lpt-ram-flash-write-allocate is used by inv-allocate-gnd,
• persistence-base/lpt-ram-flash-write-log-buf is used by inv-sync, inv-add-gnds,
• persistence-base/lpt-ram-flash-write-non-group is used by inv-set-iblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• persistence-base/replay-log-append-one is used by prepost-replay-log,
• persistence-base/replay-log-at-other is used by prepost-replay-log, inv-recover,
• persistence-base/replay-log-base is used by prepost-replay-log,
• persistence-base/replay-log-size is used by prepost-replay-log, inv-recover,
• persistence-base/replay-lpt-at-above is used by prepost-replay-lpt,
• persistence-base/replay-lpt-base is used by prepost-replay-lpt,
• persistence-base/replay-lpt-rec is used by prepost-replay-lpt,
• persistence-base/replay-lpt-size is used by prepost-replay-lpt, inv-recover,

Used from specification list

• list/address-list-set/Last is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list/group-store/Last is used by inv-read-gblock-nodes,
• list/laddress-list/Last is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list/nat-list-set/Last is used by prepost-create-freelist, prepost-cleanup-lpt, inv-allocate-gnd, inv-deallocate-gnd,
• list/group-store/Nil is used by prepost-encode-group-nodes,
• list/address-list-set/a is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list/nat-list-set/a is used by prepost-replay-log, prepost-gcheap-add-log, prepost-create-freelist, inv-allocate-gnd, inv-allocate-ind,
• list/group-store/a is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list/laddress-list/a is used by prepost-encode-group-nodes, isprefix-size, adrlist-append-eq-size1, adrlist-append-eq-size, inv-read-gblock-nodes,
• list/nat-list-set/app is used by prepost-replay-log,
• list/laddress-list/app is used by adrlist-append-eq-size, inv-read-gblock-nodes,
• list/group-store/app is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list/laddress-list/app-01 is used by adrlist-append-eq-size, inv-read-gblock-nodes,
• list/address-list-set/app-01 is used by inv-read-gblock-nodes,
• list/group-store/app-01 is used by inv-read-gblock-nodes,
• list/nat-list-set/app-02 is used by inv-allocate-gnd, inv-allocate-ind,
• list/nat-list-set/app-03 is used by prepost-replay-log,
• list/address-list-set/app-04 is used by inv-read-gblock-nodes,
• list/group-store/app-04 is used by inv-read-gblock-nodes,
• list/laddress-list/app-04 is used by inv-read-gblock-nodes,
• list/nat-list-set/app-05 is used by prepost-replay-log,
• list/laddress-list/c is used by inv-read-gblock-nodes,
• list/nat-list-set/c is used by prepost-replay-log, prepost-gcheap-add-log, inv-allocate-gnd, inv-allocate-ind,
• list/group-store/c is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list/nat-list-set/c-07 is used by inv-allocate-gnd, inv-allocate-ind,
• list/nat-list-set/e is used by inv-allocate-gnd, inv-allocate-ind,
• list/laddress-list/e-01 is used by inv-read-gblock-nodes,
• list/group-store/e-01 is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list/nat-list-set/e-01 is used by prepost-replay-log, prepost-gcheap-add-log, inv-allocate-gnd, inv-allocate-ind,
• list/nat-list-set/e-02 is used by inv-allocate-gnd,
• list/nat-list-set/in-10 is used by prepost-gcheap-add-log,
• list/laddress-list/in-15 is used by adrlist-append-eq-size1, adrlist-append-eq-size,
• list/nat-list-set/in-17 is used by prepost-create-freelist, inv-allocate-gnd,
• list/nat-list-set/in-append is used by prepost-create-freelist, inv-allocate-gnd,
• list/laddress-list/in-append is used by adrlist-append-eq-size1, adrlist-append-eq-size,
• list/nat-list-set/in-empty is used by prepost-gcheap-add-log, prepost-create-freelist, prepost-cleanup-lpt,
• list/nat-list-set/in-rec is used by prepost-gcheap-add-log,
• list/laddress-list/len is used by isprefix-size, adrlist-append-eq-size1, adrlist-append-eq-size, inv-read-gblock-nodes,
• list/group-store/len is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list/group-store/len-02 is used by prepost-encode-group-nodes,
• list/laddress-list/len-02 is used by adrlist-append-eq-size1, adrlist-append-eq-size,
• list/laddress-list/len-05 is used by inv-read-gblock-nodes,
• list/nat-list-set/len-05 is used by prepost-gcheap-add-log,
• list/group-store/len-05 is used by prepost-encode-group-nodes, inv-read-gblock-nodes,
• list/laddress-list/ni is used by adrlist-append-eq-size,

Used from specification array-copy

• array-copy/lp-array/subarray-at is used by prepost-create-freelist,
• array-copy/buffer/at-copy is used by prepost-encode-padding,
• array-copy/lp-array/at-fill-mkarray is used by inv-format,
• array-copy/buffer/copy-exact is used by inv-read-gblock-nodes,
• array-copy/buffer/size-copy is used by prepost-encode-padding, inv-read-ind, inv-read-gnd,
• array-copy/avolume/size-fill is used by inv-format,
• array-copy/lp-array/size-fill is used by inv-format,
• array-copy/lp-array/size-subarray is used by prepost-create-freelist,
• array-copy/buffer/size-subarray is used by range-eq-validtrailer, prepost-encode-padding, prepost-encode-group-nodes, inv-read-gblock-nodes,
• array-copy/buffer/subarray-at is used by range-eq-validtrailer, prepost-encode-padding,
• array-copy/buffer/subarray-copy-elim-exact is used by inv-read-ind, inv-read-gnd,
• array-copy/buffer/subarray-elim is used by range-eq-validtrailer, prepost-encode-padding, prepost-encode-group-nodes, inv-sync, inv-add-gnds, inv-add-ind, inv-read-gblock-nodes,
• array-copy/lp-array/subarray-elim is used by prepost-create-freelist,
• array-copy/buffer/subarray-zero is used by prepost-encode-padding, inv-add-ind,
• array-copy/lp-array/subarray-zero is used by prepost-create-freelist,

Used from specification bin-min-heap-prepost

• bin-min-heap-prepost/gc-heap-rename-gc-heap-base/bin-heap-inv-def is used by prepost-create-gcheap, inv-get-gc-block, inv-format,
• bin-min-heap-prepost/gc-heap-rename-gc-heap-base/key-set-in is used by inv-get-gc-block,
• bin-min-heap-prepost/gc-heap-rename-gc-heap-base/prepost-insert is used by prepost-gcheap-add-log, prepost-create-gcheap,
• bin-min-heap-prepost/gc-heap-rename-gc-heap-base/prepost-remove is used by prepost-cleanup-lpt, inv-deallocate-gnd,
• bin-min-heap-prepost/gc-heap-rename-gc-heap-base/prepost-update is used by inv-set-gblock-refsize,
• bin-min-heap-prepost/gc-heap-rename-gc-heap-base/keyset-eq-empty is used by prepost-gcheap-add-log, prepost-create-gcheap, prepost-cleanup-lpt, inv-format,

Used from specification list-dup

• list-dup/nat-list-set/a is used by prepost-replay-log,
• list-dup/nat-list-set/dups-cons is used by prepost-replay-log, prepost-gcheap-add-log,
• list-dup/nat-list-set/e-01 is used by prepost-gcheap-add-log, prepost-create-freelist, inv-commit, inv-format,
• list-dup/nat-list-set/f is used by prepost-create-freelist, inv-allocate-gnd,
• list-dup/nat-list-set/f-01 is used by prepost-replay-log,

Used from specification address-data

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

Used from specification abs-node

• abs-node/encoding-index-node/abs-padding is used by prepost-encode-padding,
• abs-node/encoding-group-node/decode-node is used by inv-read-gnd, inv-read-gblock-nodes,
• abs-node/encoding-index-node/decode-node is used by inv-read-ind,
• abs-node/encoding-group-node/encode-node is used by prepost-encode-group-nodes,
• abs-node/encoding-index-node/encode-node is used by inv-add-ind,
• abs-node/encoding-group-node/abs-node-abs-node-append-subarray is used by inv-read-gblock-nodes,
• abs-node/encoding-index-node/abs-node-unique is used by inv-read-ind,
• abs-node/encoding-group-node/abs-node-unique is used by inv-read-gnd,
• abs-node/encoding-index-node/abs-padding-alignup is used by inv-read-gblock-nodes,
• abs-node/encoding-index-node/abs-padding-nospace is used by inv-read-gblock-nodes,
• abs-node/encoding-index-node/abs-padding-size is used by inv-read-gblock-nodes,
• abs-node/encoding-index-node/buf-size-zero is used by range-eq-validtrailer, prepost-encode-padding, prepost-encode-group-nodes, flush-padding-space-write, inv-sync, inv-read-ind, inv-read-gnd, inv-add-ind, inv-read-gblock-nodes,
• abs-node/encoding-index-node/lfw-is-encoded-nodeheader-size is used by prepost-encode-padding, inv-read-gblock-nodes,

Used from specification bufleb

• bufleb/disj is used by prepost-replay-lpt, prepost-cleanup-lpt, flush-padding-space-write, inv-get-block-free-size, inv-sync, inv-add-gnds, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• bufleb/elim is used by inv-allocate-ind, inv-deallocate-gnd,
• bufleb/elim-is-buf-ant is used by inv-get-block-free-size, inv-sync, inv-add-gnds, inv-allocate-ind, inv-add-ind,
• bufleb/elim-is-buf-suc is used by inv-get-block-free-size, inv-sync,
• bufleb/inj is used by inv-allocate-ind, inv-deallocate-gnd,
• bufleb/sel is used by flush-padding-space-write, inv-get-block-free-size, inv-sync, inv-add-gnds, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• bufleb/test-02 is used by inv-sync, inv-add-gnds, inv-add-ind,

Used from specification node-header

• node-header/elim is used by inv-read-gblock-nodes,

Used from specification eraseblock

• eraseblock/isempty is used by range-eq-validtrailer,
• eraseblock/isempty-ext is used by range-eq-validtrailer,
• eraseblock/emptyleb-size is used by inv-read-gblock-nodes,
• eraseblock/isempty-elim-left0 is used by inv-read-gblock-nodes,
• eraseblock/isempty-elim-right is used by inv-read-gblock-nodes,
• eraseblock/lebsize-neq-zero is used by inv-read-gblock-nodes,
• eraseblock/lebsize-page-size-is-aligned is used by flush-padding-space-write,
• eraseblock/page-size is used by flush-padding-space-write, flush-padding-space-aligned, inv-sync, inv-add-gnds, inv-add-ind,
• eraseblock/page-size-plus-eq-0 is used by inv-sync,
• eraseblock/page-size-rewrite-sum is used by inv-sync,

Used from specification nat-mult

• nat-mult/dist-sub-04 is used by inv-add-ind,
• nat-mult/le-05 is used by flush-padding-space-header,
• nat-mult/ls-01 is used by prepost-encode-padding,
• nat-mult/ls-08 is used by prepost-encode-padding, inv-read-gblock-nodes,
• nat-mult/mult-a is used by prepost-encode-padding, prepost-encode-group-nodes, flush-padding-space-header, flush-padding-space-aligned, inv-sync, inv-add-ind, inv-read-gblock-nodes,
• nat-mult/mult-c is used by prepost-encode-padding, prepost-encode-group-nodes, flush-padding-space-header, flush-padding-space-aligned, inv-sync, inv-add-ind, inv-read-gblock-nodes,
• nat-mult/numeral-19 is used by prepost-encode-padding,
• nat-mult/numeral-29 is used by inv-read-gblock-nodes,
• nat-mult/numeral-30 is used by prepost-encode-padding, inv-read-gblock-nodes,
• nat-mult/numeral-36 is used by prepost-encode-padding,
• nat-mult/one is used by prepost-encode-padding, inv-read-gblock-nodes,
• nat-mult/two-02 is used by prepost-encode-padding, inv-read-gblock-nodes,
• nat-mult/two-one-01 is used by inv-read-gblock-nodes,
• nat-mult/two-zero-01 is used by prepost-encode-padding, flush-padding-space-header, flush-padding-space-aligned, inv-read-gblock-nodes,
• nat-mult/zero is used by inv-add-ind,

Used from specification oelem

• oelem/nat-set/irreflexivity is used by range-eq-validtrailer, prepost-replay-lpt, prepost-replay-log, prepost-gcheap-add-log, prepost-encode-padding, prepost-encode-group-nodes, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, nat-stuff0, inv-sync, inv-add-gnds, inv-read-ind, inv-read-gnd, inv-recover, inv-set-iblock-refsize, inv-get-iblock-refsize, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind, inv-read-gblock-nodes,
• oelem/nat-set/ls-le is used by prepost-create-freelist,
• oelem/nat-set/sls is used by prepost-create-freelist,
• oelem/nat-set/transitivity is used by prepost-replay-lpt, prepost-encode-padding, prepost-cleanup-lpt, inv-recover, inv-read-gblock-nodes,

Used from specification awbuf-inv

• awbuf-inv/awbuf-inv-def is used by flush-padding-space-write,
• awbuf-inv/inv-unmap is used by prepost-replay-lpt, prepost-cleanup-lpt,
• awbuf-inv/awbuf-inv-crash is used by inv-recover,
• awbuf-inv/down-arrow-size0 is used by inv-recover,
• awbuf-inv/down-arrow-size1 is used by inv-recover,
• awbuf-inv/inv-buf-in-vol is used by inv-get-block-free-size, inv-sync, inv-add-gnds, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• awbuf-inv/inv-leb-size is used by inv-read-ind, inv-read-gnd, inv-read-gblock-nodes,
• awbuf-inv/inv-nobuf-synced is used by prepost-replay-lpt, prepost-cleanup-lpt, inv-commit, inv-recover, inv-format,
• awbuf-inv/inv-unmap is used by inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd,
• awbuf-inv/synced-buffered-aligned is used by inv-allocate-ind,
• awbuf-inv/synced-down-synced is used by inv-recover,
• awbuf-inv/synced-map is used by inv-allocate-gnd,

Used from specification list-del

• list-del/laddress-list/extension is used by isprefix-size, adrlist-append-eq-size1, adrlist-append-eq-size,
• list-del/group-store/get-append-grt is used by prepost-encode-group-nodes,
• list-del/group-store/get-append-less is used by prepost-encode-group-nodes,
• list-del/group-store/get-zero is used by prepost-encode-group-nodes,

Used from specification elem-index

• elem-index/gc-heap-base/sel-01-M01 is used by prepost-replay-lpt, prepost-gcheap-add-log, prepost-create-gcheap, prepost-cleanup-lpt, id-idx-cleanup-lpt-backwards-fwd, inv-sync, inv-add-gnds, inv-recover, inv-set-gblock-refsize, inv-get-gc-block, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-format, inv-add-ind,
• elem-index/gc-heap-base/sel-01-M02 is used by prepost-gcheap-add-log, prepost-create-gcheap, id-idx-cleanup-lpt-backwards-fwd, inv-sync, inv-add-gnds, inv-set-iblock-refsize, inv-set-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-format, inv-add-ind,
• elem-index/gc-heap-base/sel-01-M03 is used by prepost-replay-lpt, prepost-gcheap-add-log, prepost-create-gcheap, prepost-create-freelist, prepost-cleanup-lpt, id-idx-cleanup-lpt-backwards-fwd, inv-sync, inv-add-gnds, inv-commit, inv-recover, inv-set-iblock-refsize, inv-get-iblock-refsize, inv-set-gblock-refsize, inv-get-gblock-refsize, inv-get-gc-block, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-format, inv-add-ind,
• elem-index/gc-heap-base/sel-02 is used by prepost-replay-lpt, prepost-cleanup-lpt, inv-sync, inv-add-gnds, inv-recover, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,

Used from specification array

• array/buffer/Extension is used by range-eq-validtrailer, prepost-encode-padding,
• array/avolume/Put-other is used by prepost-cleanup-lpt,
• array/lp-array/Put-other is used by inv-allocate-gnd, inv-deallocate-gnd,
• array/avolume/Put-other is used by inv-allocate-ind,
• array/avolume/Put-same is used by inv-allocate-gnd, inv-allocate-ind,
• array/lp-array/Put-same is used by prepost-replay-lpt, prepost-cleanup-lpt, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd,
• array/buffer/Size-mkarray is used by prepost-encode-group-nodes, inv-sync, inv-read-ind, inv-read-gnd, inv-allocate-gnd, inv-allocate-ind, inv-add-ind, inv-read-gblock-nodes,
• array/lp-array/Size-mkarray is used by prepost-create-freelist, inv-format,
• array/gc-heap-base-key-index-array/Size-mkarray is used by prepost-create-gcheap, inv-format,
• array/avolume/Size-mkarray is used by inv-format,
• array/avolume/Size-put is used by prepost-cleanup-lpt, inv-sync, inv-add-gnds, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• array/lp-array/Size-put is used by prepost-replay-lpt, prepost-replay-log, prepost-cleanup-lpt, inv-sync, inv-add-gnds, inv-set-iblock-refsize, inv-set-gblock-refsize, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd, inv-add-ind,
• array/avolume/cgetput is used by prepost-cleanup-lpt,
• array/lp-array/cgetput is used by prepost-replay-lpt, prepost-replay-log, inv-allocate-gnd,
• array/lp-array/cngetput is used by inv-deallocate-gnd,
• array/avolume/cngetput is used by inv-allocate-ind,
• array/lp-array/cputput is used by prepost-replay-lpt, prepost-replay-log, prepost-cleanup-lpt, inv-allocate-gnd, inv-allocate-ind, inv-deallocate-gnd,

Used from specification nat-div

• nat-div/mod-le-02 is used by inv-sync,
• nat-div/mod-one is used by inv-read-gblock-nodes,
• nat-div/mod-same is used by inv-sync,

Used from specification debug

• debug/debug is used by inv-sync, inv-add-gnds, inv-recover, inv-format, inv-add-ind, inv-read-gblock-nodes,

Used from specification awbuf-asm

• awbuf-asm/inv-add-log-leb is used by inv-allocate-gnd,
• awbuf-asm/inv-destroy-buf is used by inv-commit,
• awbuf-asm/inv-format is used by inv-format,
• awbuf-asm/inv-move-buf is used by inv-allocate-ind,
• awbuf-asm/inv-recover is used by inv-recover,
• awbuf-asm/inv-remap is used by inv-allocate-gnd, inv-allocate-ind,
• awbuf-asm/inv-write-buf is used by inv-sync, inv-add-gnds, inv-add-ind,