Used simplifier rules/spec theorems by specification

Used from specification store+set

• store+set/group-store-ablock-store-nat-store/Diff-base is used by inv-commit, inv-check-commit,
• store+set/group-store-ablock-store-nat-store/Diff-del-rw is used by inv-gc,
• store+set/group-store-ablock-store-nat-store/Diff-empty is used by inv-format,
• store+set/node-index/Dom is used by inv-gc-update-index, inv-gc-copy,
• store+set/group-store-ablock-store-nat-store/Dom is used by term-restore-log, inv-gc-update-index, inv-allocate, inv-recover, inv-gc, inv-truncate, inv-store,
• store+set/node-index/In-data-in is used by prepost-gc-referenced-nodes,
• store+set/group-store-ablock-store-nat-store/diff-add-rem is used by inv-gc,
• store+set/node-index/dom-add-in is used by inv-gc-update-index,
• store+set/group-store-ablock-store-nat-store/dom-add-in is used by inv-gc-update-index, inv-addn, inv-truncate, inv-remove, inv-store,
• store+set/group-store-ablock-store-nat-store/dom-del is used by inv-gc,
• store+set/group-store-ablock-store-nat-store/dom-emp is used by inv-format,
• store+set/node-index/dom-ins is used by inv-gc-update-index,
• store+set/group-store-ablock-store-nat-store/dom-ins is used by inv-gc-update-index, inv-allocate, inv-addn, inv-truncate, inv-remove, inv-store,
• store+set/group-store-ablock-store-nat-store/in-dom-inter is used by inv-gc,

Used from specification nat-basic

• nat-basic/a is used by term-restore-log, term-remove-nonend-blocks, prepost-split-nodes, prepost-gc-referenced-nodes, ls-inv-prefix-app-prefixn, lf-inv-append-sizes, inv-gc-update-index, inv-gc-copy, inv-transaction, inv-addn, inv-orphans-insert, inv-truncate, inv-remove, inv-store, inv-newino, inv-format,
• nat-basic/add-base is used by prepost-split-nodes, prepost-gc-referenced-nodes, inv-gc-copy,
• nat-basic/c is used by term-restore-log, term-remove-nonend-blocks, prepost-split-nodes, prepost-gc-referenced-nodes, ls-inv-prefix-app-prefixn, lf-inv-append-sizes, inv-gc-update-index, inv-gc-copy, inv-transaction, inv-addn, inv-orphans-insert, inv-truncate, inv-remove, inv-store, inv-newino, inv-format,
• nat-basic/eq-01 is used by prepost-split-nodes, prepost-gc-referenced-nodes, ls-inv-prefix-app-prefixn, lf-inv-append-sizes, inv-gc-update-index, inv-gc-copy, inv-transaction, inv-store,
• nat-basic/eq-02 is used by inv-gc-update-index, inv-truncate,
• nat-basic/f is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, ls-inv-prefix-app-prefixn, inv-gc-update-index, inv-gc-copy, inv-allocate, inv-addn, inv-orphans-insert, inv-store, inv-newino,
• nat-basic/l is used by prepost-split-nodes, inv-addn,
• nat-basic/l-01 is used by inv-gc-copy,
• nat-basic/l-02 is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, inv-gc-copy, inv-newino,
• nat-basic/lf is used by prepost-gc-referenced-nodes,
• nat-basic/lf-01 is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, inv-add5, inv-gc-copy, inv-add4,
• nat-basic/lf-02 is used by prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs,
• nat-basic/ls-02 is used by prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, inv-addn,
• nat-basic/one is used by inv-add5, inv-add2, inv-add3, inv-add4,
• nat-basic/one-01 is used by term-remove-nonend-blocks, prepost-split-nodes, inv-transaction, inv-truncate,
• nat-basic/one-06 is used by inv-transaction,
• nat-basic/oz is used by inv-gc-copy, inv-orphans-insert, inv-store, inv-newino, inv-format,
• nat-basic/s-04 is used by term-restore-log, term-remove-nonend-blocks, prepost-split-nodes, prepost-gc-referenced-nodes, inv-gc-update-index, inv-gc-copy, inv-transaction, inv-truncate,
• nat-basic/succ is used by term-restore-log, prepost-gc-referenced-nodes, inv-gc-update-index, inv-gc-copy, inv-transaction,
• nat-basic/succ-03 is used by prepost-gc-referenced-nodes,
• nat-basic/zero is used by term-remove-nonend-blocks, inv-add5, inv-gc-copy, inv-addn, inv-add1, inv-add2, inv-add3, inv-add4,
• nat-basic/zero-01 is used by prepost-gc-referenced-nodes, inv-gc-copy,

Used from specification nat-set

• nat-set/le-add-bound is used by inv-gc-update-index, inv-gc-copy, inv-commit, inv-check-commit, inv-recover,
• nat-set/ls-add-bound is used by inv-newino,

Used from specification ablock

• ablock/group-store/elim is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, inv-gc-update-index, inv-addn, inv-recover, inv-gc, inv-truncate, inv-remove, inv-store,
• ablock/group-store/inj is used by inv-gc-update-index, inv-addn, inv-gc, inv-truncate, inv-remove, inv-store,
• ablock/group-store/sel-01 is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, ls-inv-prefix-app-prefixn, lf-inv-append-sizes, inv-gc-update-index, inv-allocate, inv-addn, inv-gc, inv-store,
• ablock/group-store/sel-02 is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, ls-inv-prefix-app-prefixn, lf-inv-append-sizes, inv-gc-update-index, inv-allocate, inv-addn, inv-gc, inv-store,
• ablock/group-store/sel-03 is used by inv-allocate, inv-addn,
• ablock/group-store/upd-01 is used by inv-addn,
• ablock/group-store/upd-02 is used by inv-addn,
• ablock/group-store/upd-03 is used by inv-gc-update-index, inv-truncate, inv-remove, inv-store,
• ablock/group-store/updsel-03 is used by inv-addn,
• ablock/group-store/updsel-10 is used by inv-truncate,
• ablock/group-store/updsel-11 is used by inv-truncate,
• ablock/group-store/updsel-28 is used by inv-addn,
• ablock/group-store/updsel-29 is used by inv-addn,

Used from specification list+set

• list+set/key-list-set/toSet-app is used by inv-gc-update-index, inv-gc-copy,
• list+set/nat-list-set/toSet-app is used by inv-allocate,
• list+set/address-list-set/toSet-app is used by inv-gc-update-index, inv-gc-copy,
• list+set/nat-list-set/toSet-diff-old is used by inv-allocate,
• list+set/key-list-set/toSet-empty is used by inv-gc-update-index, inv-gc-copy,
• list+set/nat-list-set/toSet-empty is used by inv-gc-copy,
• list+set/address-list-set/toSet-ext is used by inv-gc,
• list+set/nat-list-set/toSet-ext is used by inv-gc,
• list+set/key-list-set/toSet-one is used by inv-gc-update-index, inv-gc-copy,
• list+set/nat-list-set/toSet-one is used by inv-allocate,
• list+set/address-list-set/toSet-one is used by inv-gc-update-index, inv-gc-copy,

Used from specification aubifs-inv

• aubifs-inv/ri-cons is used by prepost-gc-referenced-nodes,
• aubifs-inv/ri-cons-inj is used by inv-gc,
• aubifs-inv/ri-cons-range-ri is used by inv-gc,
• aubifs-inv/ri-cons-variant1-01 is used by inv-gc, inv-lookup,
• aubifs-inv/ri-inj-del is used by inv-remove,
• aubifs-inv/ri-inj-empty is used by inv-format,
• aubifs-inv/ri-inj-rem is used by inv-truncate,
• aubifs-inv/ri-inj-write is used by inv-store,

Used from specification aubifs-base

• aubifs-base/range is used by inv-gc,
• aubifs-base/index-lookup-rec is used by inv-gc-copy,
• aubifs-base/index-update-key-base is used by inv-gc-update-index, inv-gc-copy,
• aubifs-base/new-append is used by inv-gc-copy,
• aubifs-base/new-base is used by inv-gc-copy, inv-addn,
• aubifs-base/nodups-new is used by inv-gc-copy,
• aubifs-base/range is used by inv-gc-update-index, inv-gc, inv-truncate, inv-remove, inv-store,
• aubifs-base/read-app is used by prepost-gc-referenced-nodes,
• aubifs-base/read-base is used by prepost-gc-referenced-nodes,
• aubifs-base/read-eq-empty is used by prepost-gc-referenced-nodes,
• aubifs-base/read-length is used by inv-gc,
• aubifs-base/read-one is used by prepost-gc-referenced-nodes,
• aubifs-base/update-index-app is used by inv-gc-update-index,
• aubifs-base/update-index-append is used by inv-gc-copy,
• aubifs-base/update-index-data-notin is used by inv-gc-update-index,
• aubifs-base/write-app is used by inv-gc-copy,
• aubifs-base/write-base is used by inv-gc-copy, inv-addn,
• aubifs-base/write-dom is used by inv-gc-copy,
• aubifs-base/write-new is used by inv-gc-copy,

Used from specification ablock-store-inv

• ablock-store-inv/group-store/at is used by prepost-gc-referenced-nodes,
• ablock-store-inv/group-store/except-refsizeeq-write-left is used by inv-store,
• ablock-store-inv/group-store/inv-block is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, ls-inv-prefix-app-prefixn, lf-inv-append-sizes,
• ablock-store-inv/group-store/inv-store is used by inv-recover,
• ablock-store-inv/group-store/addresslist-length is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, inv-addn, inv-gc,
• ablock-store-inv/group-store/adrs-empty is used by inv-allocate, inv-addn,
• ablock-store-inv/group-store/except-refsizeeq-refl is used by inv-truncate, inv-store,
• ablock-store-inv/group-store/except-refsizeeq-write-left is used by inv-truncate,
• ablock-store-inv/group-store/in-store-inv is used by inv-recover,
• ablock-store-inv/group-store/inv-eq-list-size is used by prepost-gc-referenced-nodes, inv-gc,
• ablock-store-inv/group-store/inv-flashsize-empty is used by inv-addn,
• ablock-store-inv/group-store/inv-nodups is used by inv-addn, inv-gc,
• ablock-store-inv/group-store/inv-nodups-app-left is used by inv-addn,
• ablock-store-inv/group-store/inv-prefixn-lax is used by inv-addn,
• ablock-store-inv/group-store/inv-reduce is used by ls-inv-reduce-jnlhead, inv-gc-update-index,
• ablock-store-inv/group-store/inv-reduce-rem is used by inv-gc,
• ablock-store-inv/group-store/inv-remove-refsize0-diff is used by inv-commit, inv-check-commit,
• ablock-store-inv/group-store/inv-set-sizes is used by inv-gc-update-index, inv-addn, inv-recover,
• ablock-store-inv/group-store/inv-store-empty is used by inv-format,
• ablock-store-inv/group-store/notin-notin is used by inv-gc-update-index, inv-store,
• ablock-store-inv/group-store/remove-refsize0-empty is used by inv-format,
• ablock-store-inv/group-store/remove-refsize0-idem is used by inv-commit, inv-check-commit,
• ablock-store-inv/group-store/size-append is used by inv-transaction,
• ablock-store-inv/group-store/size-base is used by inv-transaction,
• ablock-store-inv/group-store/size-one is used by inv-transaction,
• ablock-store-inv/group-store/to-adrs-append is used by prepost-gc-referenced-nodes, inv-addn,
• ablock-store-inv/group-store/to-adrs-eq is used by inv-addn, inv-gc,
• ablock-store-inv/group-store/to-adrs-eq-one is used by prepost-gc-referenced-nodes,
• ablock-store-inv/group-store/to-adrs-one is used by prepost-gc-referenced-nodes,
• ablock-store-inv/group-store/to-ards-no-dups is used by inv-addn, inv-gc,

Used from specification apersistence-base

• apersistence-base/crash-group-in is used by inv-recover,
• apersistence-base/crash-group-at is used by inv-recover,
• apersistence-base/crash-gstore-inv is used by inv-recover,
• apersistence-base/dom-gstore-crash is used by inv-recover,
• apersistence-base/elems-append is used by inv-allocate,
• apersistence-base/elems-def is used by inv-recover, inv-gc,
• apersistence-base/elems-empty is used by inv-gc-copy, inv-commit, inv-check-commit, inv-format,
• apersistence-base/elems-in-notin-ginval is used by inv-recover, inv-gc,
• apersistence-base/elems-log-subset-gstore-union-ginval is used by inv-recover,
• apersistence-base/elems-prepend is used by term-restore-log,
• apersistence-base/fwd-in-gstore-loghead is used by inv-gc-copy, inv-allocate, inv-addn, inv-recover, inv-gc, inv-truncate, inv-remove, inv-store,
• apersistence-base/fwd-in-gstore0 is used by inv-gc,
• apersistence-base/fwd-in-log-in-gstore is used by inv-recover, inv-gc,
• apersistence-base/fwd-inv-gblock is used by term-remove-nonend-blocks,
• apersistence-base/fwd-inv-gblock-rem is used by prepost-gc-referenced-nodes, inv-gc-update-index, inv-recover, inv-gc,
• apersistence-base/fwd-inv-loghead is used by inv-gc-copy, inv-allocate, inv-addn, inv-recover, inv-gc, inv-truncate, inv-remove, inv-store,
• apersistence-base/inv-journal is used by inv-add5, inv-sync, inv-gc-update-index, inv-gc-copy, inv-allocate, inv-addn, inv-get, inv-add1, inv-add2, inv-add3, inv-add4, inv-commit, inv-check-commit, inv-recover, inv-gc, inv-entries, inv-truncate, inv-remove, inv-store, inv-lookup, inv-contains, inv-format,
• apersistence-base/notin-gstore-ginval-notin-gstore0 is used by inv-recover,

Used from specification set-union

• set-union/nat-set/Difference is used by inv-gc,
• set-union/nat-set/rem-inter-empty3 is used by inv-gc-copy,
• set-union/node-store/sub-del-03 is used by ls-diff-rem-subseteq, inv-gc-copy,
• set-union/node-store/sub-union is used by ls-diff-rem-subseteq, inv-gc-copy,
• set-union/nat-set/subdef is used by inv-recover, inv-gc, inv-truncate,
• set-union/node-store/undel-03 is used by inv-truncate,
• set-union/node-index/union-sub is used by inv-gc-update-index,
• set-union/node-store/unrax is used by inv-gc,
• set-union/nat-set/unrax is used by inv-recover,
• set-union/node-store/Delete is used by inv-store,
• set-union/nat-set/Delete is used by inv-allocate,
• set-union/node-store/Difference is used by inv-gc,
• set-union/node-store/Intersect is used by inv-truncate,
• set-union/nat-set/del-e-01 is used by inv-allocate,
• set-union/node-store/del-size is used by inv-truncate,
• set-union/node-store/diff-add-del is used by inv-gc-copy,
• set-union/nat-set/diff-e is used by inv-gc-copy,
• set-union/nat-set/diff-e-01 is used by inv-gc-copy,
• set-union/nat-set/diff-idem is used by inv-gc-copy, inv-allocate,
• set-union/node-store/diff-sub is used by ls-diff-rem-subseteq, inv-gc-copy,
• set-union/nat-set/int-a is used by term-restore-log, inv-gc-copy, inv-allocate, inv-addn, inv-commit, inv-check-commit, inv-recover, inv-gc, inv-truncate, inv-remove, inv-store, inv-format,
• set-union/node-store/int-a is used by inv-gc-update-index, inv-gc-copy, inv-gc, inv-truncate,
• set-union/node-store/int-c is used by inv-gc-update-index, inv-gc-copy, inv-gc, inv-truncate,
• set-union/nat-set/int-c is used by term-restore-log, inv-gc-copy, inv-allocate, inv-addn, inv-commit, inv-check-commit, inv-recover, inv-gc, inv-truncate, inv-remove, inv-store, inv-format,
• set-union/nat-set/int-e is used by inv-gc-copy, inv-allocate, inv-commit, inv-check-commit, inv-format,
• set-union/node-store/int-e is used by inv-truncate,
• set-union/nat-set/int-empty-one is used by inv-allocate,
• set-union/node-store/int-ins is used by inv-gc-update-index,
• set-union/nat-set/int-ins is used by term-restore-log, inv-gc,
• set-union/nat-set/intersect-add-rem is used by inv-allocate,
• set-union/node-store/intersect-empty-rem is used by inv-truncate,
• set-union/node-store/intu-empty is used by inv-gc-update-index,
• set-union/nat-set/rem-union-ins is used by inv-allocate, inv-gc,
• set-union/nat-set/sub-del-04 is used by inv-gc,
• set-union/node-index/sub-union is used by inv-gc-copy,
• set-union/node-index/sub-union-01 is used by inv-gc-copy,
• set-union/node-store/subset-union-left-rem is used by ls-union-subseteq, inv-gc-copy,
• set-union/nat-set/subseteq-inter-empty-empty is used by inv-gc-copy,
• set-union/nat-set/una is used by inv-gc-update-index, inv-gc-copy, inv-allocate, inv-addn, inv-commit, inv-check-commit, inv-recover, inv-gc, inv-truncate, inv-remove, inv-store, inv-format,
• set-union/node-index/una is used by inv-gc-update-index, inv-gc-copy,
• set-union/node-store/una is used by ls-union-subseteq, inv-gc-update-index, inv-gc-copy, inv-truncate,
• set-union/node-index/unadd is used by inv-gc-update-index, inv-gc-copy,
• set-union/nat-set/unadd is used by inv-gc-update-index, inv-allocate, inv-gc, inv-store,
• set-union/node-store/unadd is used by inv-gc-update-index, inv-gc-copy,
• set-union/nat-set/unc is used by inv-gc-update-index, inv-gc-copy, inv-allocate, inv-addn, inv-commit, inv-check-commit, inv-recover, inv-gc, inv-truncate, inv-remove, inv-store, inv-format,
• set-union/node-index/unc is used by inv-gc-update-index, inv-gc-copy,
• set-union/node-store/unc is used by ls-union-subseteq, inv-gc-update-index, inv-gc-copy, inv-truncate,
• set-union/node-store/undel is used by inv-truncate,
• set-union/nat-set/une is used by inv-gc-copy, inv-allocate, inv-commit, inv-check-commit, inv-store, inv-format,
• set-union/node-store/une is used by inv-gc-update-index, inv-gc-copy, inv-truncate,
• set-union/node-index/une is used by inv-gc-update-index, inv-gc-copy,
• set-union/node-index/uneq is used by inv-gc-update-index,
• set-union/nat-set/uneq is used by inv-recover,
• set-union/nat-set/unin is used by inv-gc-update-index,
• set-union/node-store/unin is used by inv-truncate,
• set-union/nat-set/unin-01 is used by inv-recover, inv-gc,
• set-union/nat-set/unsub is used by inv-recover,
• set-union/node-index/unsub-union-01 is used by inv-gc-update-index, inv-gc-copy,

Used from specification nat

• nat/anti is used by inv-addn,
• nat/elim-sub is used by inv-gc-update-index, inv-gc-copy, inv-truncate, inv-remove, inv-store,
• nat/eq-01 is used by inv-truncate, inv-store,
• nat/fle is used by term-remove-nonend-blocks, inv-add5, inv-gc-update-index, inv-gc-copy, inv-allocate, inv-add4, inv-orphans-insert, inv-store, inv-newino,
• nat/fle-01 is used by prepost-gc-referenced-nodes, inv-gc-update-index, inv-gc-copy,
• nat/ge is used by prepost-split-nodes, ls-inv-prefixn-ladrs, inv-gc-update-index, inv-gc-copy, inv-truncate, inv-remove, inv-store,
• nat/gr-def is used by prepost-split-nodes, inv-gc-copy, inv-allocate,
• nat/le-def is used by term-remove-nonend-blocks, prepost-split-nodes, prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, ls-inv-prefix-app-prefixn, inv-gc-update-index, inv-allocate, inv-transaction, inv-addn, inv-orphans-insert, inv-truncate, inv-store, inv-newino,
• nat/le-ls-simp is used by prepost-split-nodes,
• nat/lels is used by prepost-split-nodes, prepost-gc-referenced-nodes, inv-add5, inv-gc-copy, inv-allocate, inv-add3, inv-add4,
• nat/lels-02 is used by inv-addn,
• nat/lels-03 is used by ls-inv-prefix-app-prefixn, inv-allocate,
• nat/lep is used by prepost-split-nodes, prepost-gc-referenced-nodes, inv-gc-update-index, inv-truncate, inv-remove, inv-store,
• nat/lep-02 is used by inv-addn, inv-format,
• nat/ler is used by inv-gc-update-index, inv-gc-copy, inv-addn, inv-commit, inv-check-commit, inv-recover,
• nat/les is used by prepost-gc-referenced-nodes,
• nat/let is used by inv-gc-update-index, inv-gc-copy, inv-gc,
• nat/lez is used by inv-gc-copy,
• nat/lez-01 is used by term-remove-nonend-blocks, inv-gc-update-index, inv-gc-copy,
• nat/ls-01 is used by term-remove-nonend-blocks, prepost-split-nodes, inv-transaction, inv-truncate,
• nat/ls-03 is used by term-remove-nonend-blocks,
• nat/ls-le-simp is used by prepost-gc-referenced-nodes,
• nat/not-zero is used by inv-add5, inv-add3, inv-add4,
• nat/pred-03 is used by prepost-split-nodes, inv-transaction,
• nat/sub-add is used by prepost-split-nodes,
• nat/sub-ls is used by term-remove-nonend-blocks,
• nat/succ-01 is used by prepost-gc-referenced-nodes,
• nat/zero is used by prepost-gc-referenced-nodes,

Used from specification store

• store/group-store-ablock-store-nat-store/At-other is used by inv-truncate, inv-remove, inv-store,
• store/group-store-ablock-store-nat-store/At-same is used by inv-allocate, inv-addn, inv-truncate, inv-remove, inv-store,
• store/group-store-ablock-store-nat-store/Del-at is used by inv-gc,
• store/group-store-ablock-store-nat-store/Del-in is used by inv-gc,
• store/group-store-ablock-store-nat-store/In-insert is used by inv-gc-update-index, inv-truncate, inv-remove, inv-store,
• store/group-store-ablock-store-nat-store/in-neq is used by inv-truncate, inv-remove, inv-store,
• store/node-index/inj-put is used by inv-gc-update-index,
• store/group-store-ablock-store-nat-store/ins is used by inv-addn,
• store/group-store-ablock-store-nat-store/insin is used by inv-allocate, inv-addn, inv-truncate, inv-remove, inv-store,
• store/group-store-ablock-store-nat-store/insins is used by inv-addn, inv-store,
• store/group-store-ablock-store-nat-store/k-At-same is used by inv-gc-update-index, inv-store,
• store/node-index/notmemlookup is used by prepost-gc-referenced-nodes,
• store/group-store-ablock-store-nat-store/notmemlookup is used by inv-truncate, inv-store,
• store/node-store/notmemlookup is used by prepost-gc-referenced-nodes,

Used from specification min-max

• min-max/max-eq-0 is used by inv-orphans-insert, inv-store,
• min-max/max-notls2 is used by inv-gc-update-index, inv-orphans-insert, inv-store,

Used from specification error-class

• error-class/ecommit is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, inv-sync, inv-allocate, inv-get, inv-commit, inv-check-commit, inv-recover, inv-gc, inv-entries, inv-lookup, inv-contains, inv-format,
• error-class/einval is used by inv-gc-copy,
• error-class/enospc is used by inv-allocate,
• error-class/esuccess is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, inv-allocate, inv-addn, inv-commit, inv-check-commit, inv-recover, inv-gc, inv-lookup, inv-format,
• error-class/not-esuccess is used by prepost-gc-referenced-nodes, inv-add5, inv-gc-copy, inv-allocate, inv-addn, inv-add1, inv-add2, inv-add3, inv-add4, inv-commit, inv-check-commit, inv-recover, inv-gc, inv-format,

Used from specification error

• error/disj-35 is used by inv-allocate, inv-gc,
• error/disj-78 is used by inv-gc-copy,
• error/disj-91 is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, inv-sync, inv-allocate, inv-get, inv-commit, inv-check-commit, inv-recover, inv-gc, inv-entries, inv-lookup, inv-contains, inv-format,

Used from specification set-basic

• set-basic/node-store/Extension is used by inv-truncate,
• set-basic/nat-set/Extension is used by inv-recover, inv-gc, inv-truncate,
• set-basic/nat-set/In-empty is used by inv-gc,
• set-basic/node-store/In-empty is used by inv-truncate,
• set-basic/nat-set/eq-03 is used by inv-gc-update-index, inv-gc, inv-store,
• set-basic/nat-set/in-02 is used by inv-gc,
• set-basic/nat-set/ne-01 is used by inv-recover, inv-gc, inv-store,
• set-basic/node-store/ne-01 is used by inv-gc, inv-truncate,
• set-basic/nat-set/size-zero is used by inv-gc-copy,
• set-basic/node-store/size-zero is used by inv-truncate,
• set-basic/nat-set/size-zero-01 is used by inv-gc-copy, inv-recover, inv-gc, inv-store,
• set-basic/node-store/size-zero-01 is used by inv-gc, inv-truncate,
• set-basic/nat-set/sub-add-01 is used by inv-allocate,
• set-basic/node-index/sub-add-03 is used by inv-gc-update-index, inv-gc-copy,
• set-basic/nat-set/sub-add-03 is used by term-restore-log, inv-gc-update-index, inv-store,
• set-basic/node-index/sub-e is used by inv-gc-update-index, inv-gc-copy,
• set-basic/nat-set/sub-e is used by inv-format,
• set-basic/nat-set/sub-idem is used by inv-gc-copy, inv-allocate,
• set-basic/nat-set/sub-insert-01 is used by inv-allocate,
• set-basic/nat-set/sub-ntrans is used by inv-recover,
• set-basic/node-store/sub-ntrans is used by inv-gc-copy,
• set-basic/node-store/sub-ntrans-01 is used by ls-diff-rem-subseteq, inv-gc-copy,
• set-basic/nat-set/sub-ntrans-01 is used by inv-truncate,
• set-basic/nat-set/sub-trans is used by inv-add5, inv-gc-copy, inv-addn, inv-add1, inv-add2, inv-add3, inv-add4, inv-gc,

Used from specification list-last

• list-last/group-store/lapp is used by inv-addn,
• list-last/nat-list-set/last-def is used by inv-allocate,
• list-last/address-list-set/lb is used by term-remove-nonend-blocks,
• list-last/group-store/lb is used by term-remove-nonend-blocks,
• list-last/nat-list-set/lin-01 is used by inv-gc,

Used from specification gjournal-base

• gjournal-base/index-update-range is used by inv-gc-copy, inv-gc,
• gjournal-base/lebs-set is used by inv-truncate,
• gjournal-base/nodes-cons-rec is used by inv-gc-update-index,
• gjournal-base/nodes-cons-write-app is used by inv-addn,
• gjournal-base/nodes-cons-write-other is used by inv-gc-update-index,
• gjournal-base/referenced-adrs-lookup-keys-nodups is used by inv-gc,
• gjournal-base/transaction is used by inv-addn,
• gjournal-base/transaction-prefix-app-last is used by inv-transaction,
• gjournal-base/transaction-prefix-app-nonlast is used by inv-transaction,
• gjournal-base/valid-journal-head is used by ls-inv-reduce-jnlhead, inv-allocate, inv-addn, inv-gc, inv-truncate, inv-remove, inv-store,
• gjournal-base/except-refsizeeq-valid-head is used by inv-truncate,
• gjournal-base/flashsize-app is used by prepost-split-nodes,
• gjournal-base/flashsize-nodes-base is used by prepost-split-nodes, inv-gc-copy,
• gjournal-base/flashsize-nodes-rec is used by inv-gc-copy,
• gjournal-base/flashsize-one is used by prepost-split-nodes,
• gjournal-base/in-index-in-range is used by inv-remove, inv-store,
• gjournal-base/index-update-dom is used by inv-gc-update-index, inv-gc-copy,
• gjournal-base/inos-empty is used by inv-format,
• gjournal-base/inos-greater-del is used by inv-remove,
• gjournal-base/inos-greater-rem is used by inv-truncate,
• gjournal-base/inos-write is used by inv-gc-update-index, inv-store,
• gjournal-base/key-cons-app is used by inv-gc-update-index, inv-gc-copy,
• gjournal-base/key-cons-base is used by inv-gc-update-index, inv-gc-copy,
• gjournal-base/key-cons-rec is used by inv-gc-update-index, inv-gc-copy,
• gjournal-base/keys-app is used by inv-gc-update-index, inv-gc-copy, inv-gc,
• gjournal-base/keys-base-01 is used by inv-gc-update-index, inv-gc-copy, inv-gc,
• gjournal-base/keys-len is used by inv-gc-update-index, inv-gc-copy, inv-gc,
• gjournal-base/keys-one is used by inv-gc-update-index,
• gjournal-base/keys-rec-01 is used by inv-gc-update-index, inv-gc-copy,
• gjournal-base/lebs-del-subseteq is used by inv-remove,
• gjournal-base/lebs-del-subseteq-set is used by inv-truncate,
• gjournal-base/lebs-empty is used by inv-format,
• gjournal-base/lebs-in-ri-in-gstore is used by inv-gc,
• gjournal-base/lebs-in-ri-in-gstore-explicit is used by inv-gc-update-index, inv-remove, inv-store, inv-lookup,
• gjournal-base/lebs-index is used by inv-gc,
• gjournal-base/lebs-lookup-subseteq is used by inv-truncate,
• gjournal-base/lebs-rem-subseteq is used by inv-truncate,
• gjournal-base/lebs-write is used by inv-gc-update-index, inv-store,
• gjournal-base/lebs-write-subseteq is used by inv-store,
• gjournal-base/lebs-write-subseteq0 is used by inv-gc-update-index,
• gjournal-base/natset-ls-add-max-ls is used by inv-orphans-insert, inv-store,
• gjournal-base/natset-ls-max-ls is used by inv-gc-update-index, inv-orphans-insert, inv-store,
• gjournal-base/new-inter-empty is used by inv-gc-copy, inv-gc,
• gjournal-base/range-del-in is used by inv-remove,
• gjournal-base/range-empty is used by inv-format,
• gjournal-base/range-write-in is used by inv-store,
• gjournal-base/range-write-notin is used by inv-gc-update-index, inv-store,
• gjournal-base/referenced-adrs-app is used by prepost-gc-referenced-nodes,
• gjournal-base/referenced-adrs-base is used by prepost-gc-referenced-nodes,
• gjournal-base/referenced-adrs-lookup-key-cons is used by inv-gc,
• gjournal-base/referenced-adrs-lookup-keys-in-dom is used by inv-gc,
• gjournal-base/referenced-adrs-lookup-keys-lookup is used by inv-gc,
• gjournal-base/referenced-adrs-one is used by prepost-gc-referenced-nodes,
• gjournal-base/refsize-cons-crash is used by inv-recover,
• gjournal-base/restrict-range-notin-lebs is used by inv-allocate,
• gjournal-base/ri-inj-index-update is used by inv-gc-update-index,
• gjournal-base/transaction-empty is used by inv-transaction,
• gjournal-base/transaction-empty-right is used by inv-addn,
• gjournal-base/transaction-length0 is used by inv-addn,
• gjournal-base/transaction-prefix-empty is used by inv-transaction,
• gjournal-base/transaction-prefix-is-transaction-prefix is used by inv-addn,

Used from specification list-prefixn

• list-prefixn/group-store/in-prefixn-at-smaller is used by prepost-gc-referenced-nodes,
• list-prefixn/group-store/prefixn-fulln is used by inv-addn,
• list-prefixn/laddress-list/in-prefixn-samepos is used by prepost-gc-referenced-nodes,
• list-prefixn/laddress-list/prefixn-0 is used by inv-allocate,
• list-prefixn/group-store/prefixn-0 is used by inv-allocate,
• list-prefixn/group-store/prefixn-append-left is used by prepost-gc-referenced-nodes, inv-addn,
• list-prefixn/laddress-list/prefixn-append-left is used by prepost-gc-referenced-nodes, ls-inv-prefix-app-prefixn, inv-addn,
• list-prefixn/group-store/prefixn-full is used by inv-addn,
• list-prefixn/laddress-list/prefixn-full is used by inv-addn,
• list-prefixn/laddress-list/prefixn-full-eq is used by ls-inv-prefixn-ladrs,
• list-prefixn/laddress-list/prefixn-fulln is used by prepost-gc-referenced-nodes, ls-inv-prefix-app-prefixn, inv-addn,
• list-prefixn/group-store/prefixn-len-n is used by ls-inv-prefix-app-prefixn,
• list-prefixn/laddress-list/prefixn-notin is used by prepost-gc-referenced-nodes,

Used from specification list-data

• list-data/nat-list-set/elim-list-c is used by term-restore-log,
• list-data/group-store/elim-list-c is used by prepost-gc-referenced-nodes,
• list-data/address-list-set/elim-list-c is used by prepost-gc-referenced-nodes, inv-gc-update-index,
• list-data/node-list/elim-list-c is used by inv-gc-update-index, inv-gc-copy, inv-transaction,
• list-data/address-list-set/l is used by prepost-gc-referenced-nodes, inv-add5, inv-gc-update-index, inv-gc-copy, inv-add1, inv-add2, inv-add3, inv-add4,
• list-data/node-list/l is used by prepost-split-nodes, inv-gc-update-index, inv-gc-copy, inv-transaction,
• list-data/group-store/l is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, ls-inv-prefix-app-prefixn, inv-addn,
• list-data/laddress-list/l is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, inv-addn,
• list-data/node-list/length-rest is used by prepost-split-nodes, inv-transaction,
• list-data/address-list-set/size-01 is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, inv-add5, inv-gc-update-index, inv-gc-copy, inv-add1, inv-add2, inv-add3, inv-add4,
• list-data/node-list/size-01 is used by inv-gc-update-index, inv-gc-copy, inv-transaction,
• list-data/group-store/size-01 is used by prepost-gc-referenced-nodes, inv-transaction, inv-addn,

Used from specification laddress

• laddress/sel-01 is used by prepost-gc-referenced-nodes,
• laddress/sel-02 is used by prepost-gc-referenced-nodes,

Used from specification index-base

• index-base/lookup-range-rem-union is used by inv-truncate,
• index-base/lookup-rem-inj-range-inter-empty is used by inv-truncate,

Used from specification list

• list/node-list/elim-first is used by inv-gc-copy,
• list/node-list/Last is used by prepost-split-nodes, prepost-gc-referenced-nodes,
• list/group-store/Last is used by inv-transaction,
• list/nat-list-set/Last is used by inv-allocate,
• list/address-list-set/Nil is used by inv-gc-copy, inv-gc,
• list/node-list/Nil is used by prepost-split-nodes, inv-gc-copy,
• list/group-store/Nil is used by term-remove-nonend-blocks, inv-gc,
• list/key-list-set/Nil is used by inv-gc-copy,
• list/group-store/a is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, ls-inv-prefix-app-prefixn, lf-inv-append-sizes, inv-transaction, inv-addn, inv-gc,
• list/key-list-set/a is used by inv-gc-update-index, inv-gc-copy, inv-gc,
• list/nat-list-set/a is used by term-restore-log, inv-allocate,
• list/laddress-list/a is used by prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, ls-inv-prefix-app-prefixn, lf-inv-append-sizes, inv-addn,
• list/node-list/a is used by prepost-split-nodes, prepost-gc-referenced-nodes, inv-add5, inv-gc-update-index, inv-gc-copy, inv-transaction, inv-add2, inv-add3, inv-add4, inv-gc,
• list/address-list-set/a is used by term-remove-nonend-blocks, prepost-gc-referenced-nodes, abs-log-simp1, abs-log-simp0, inv-add5, inv-gc-update-index, inv-gc-copy, inv-allocate, inv-addn, inv-add1, inv-add2, inv-add3, inv-add4, inv-gc,
• list/key-list-set/app is used by inv-gc-update-index, inv-gc-copy, inv-gc,
• list/group-store/app is used by inv-addn,
• list/node-list/app is used by inv-gc-update-index, inv-gc-copy, inv-transaction, inv-gc,
• list/laddress-list/app is used by inv-addn,
• list/address-list-set/app is used by prepost-gc-referenced-nodes, inv-add5, inv-gc-update-index, inv-gc-copy, inv-allocate, inv-addn, inv-add1, inv-add2, inv-add3, inv-add4,
• list/node-list/app-01 is used by prepost-split-nodes, prepost-gc-referenced-nodes,
• list/address-list-set/app-02 is used by prepost-gc-referenced-nodes, inv-gc-copy,
• list/group-store/app-02 is used by prepost-gc-referenced-nodes,
• list/group-store/app-03 is used by prepost-gc-referenced-nodes,
• list/address-list-set/app-03 is used by abs-log-simp1, abs-log-simp0, inv-gc-update-index, inv-addn,
• list/node-list/app-03 is used by inv-gc-update-index, inv-gc-copy, inv-transaction,
• list/node-list/app-04 is used by prepost-gc-referenced-nodes,
• list/node-list/app-05 is used by inv-gc-update-index, inv-gc-copy, inv-transaction,
• list/group-store/app-05 is used by prepost-gc-referenced-nodes,
• list/address-list-set/app-05 is used by prepost-gc-referenced-nodes, inv-gc-update-index,
• list/nat-list-set/c is used by term-restore-log,
• list/node-list/c is used by inv-add5, inv-gc-update-index, inv-gc-copy, inv-transaction, inv-add2, inv-add3, inv-add4,
• list/key-list-set/c is used by inv-gc-update-index, inv-gc-copy,
• list/group-store/c is used by prepost-gc-referenced-nodes,
• list/address-list-set/c is used by prepost-gc-referenced-nodes, inv-gc-update-index, inv-gc-copy,
• list/node-list/c-04 is used by prepost-gc-referenced-nodes,
• list/node-list/c-06 is used by inv-gc-copy,
• list/address-list-set/c-07 is used by prepost-gc-referenced-nodes,
• list/group-store/c-07 is used by prepost-gc-referenced-nodes,
• list/node-list/c-08 is used by inv-gc-copy,
• list/address-list-set/e is used by prepost-gc-referenced-nodes,
• list/group-store/e is used by prepost-gc-referenced-nodes,
• list/nat-list-set/e-01 is used by term-restore-log,
• list/group-store/e-01 is used by prepost-gc-referenced-nodes,
• list/node-list/e-01 is used by inv-gc-update-index, inv-gc-copy, inv-transaction,
• list/address-list-set/e-01 is used by prepost-gc-referenced-nodes, inv-gc-update-index,
• list/node-list/e-02 is used by inv-transaction,
• list/nat-list-set/e-02 is used by inv-allocate,
• list/node-list/fr is used by prepost-split-nodes,
• list/address-list-set/in-12 is used by inv-gc,
• list/node-list/in-14 is used by inv-gc-copy,
• list/address-list-set/in-14 is used by prepost-gc-referenced-nodes,
• list/laddress-list/in-17 is used by prepost-gc-referenced-nodes,
• list/address-list-set/in-17 is used by prepost-gc-referenced-nodes,
• list/laddress-list/in-append is used by prepost-gc-referenced-nodes,
• list/node-list/in-append is used by inv-gc-copy,
• list/address-list-set/in-append is used by prepost-gc-referenced-nodes,
• list/key-list-set/in-append is used by inv-gc-copy,
• list/node-list/in-append0-not-left is used by inv-gc-copy,
• list/node-list/in-empty is used by inv-gc-copy,
• list/node-list/in-rec is used by inv-gc-copy,
• list/laddress-list/len is used by prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, ls-inv-prefix-app-prefixn, lf-inv-append-sizes, inv-addn,
• list/address-list-set/len is used by term-remove-nonend-blocks, inv-gc-update-index, inv-gc-copy,
• list/group-store/len is used by prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, ls-inv-prefix-app-prefixn, lf-inv-append-sizes, inv-transaction, inv-addn,
• list/node-list/len is used by inv-gc-update-index, inv-gc-copy, inv-transaction,
• list/node-list/len-02 is used by inv-add5, inv-gc-update-index, inv-transaction, inv-add1, inv-add2, inv-add3, inv-add4,
• list/laddress-list/len-02 is used by prepost-gc-referenced-nodes,
• list/group-store/len-02 is used by prepost-gc-referenced-nodes, inv-transaction,
• list/address-list-set/len-02 is used by inv-gc-update-index,
• list/nat-list-set/len-05 is used by term-restore-log,
• list/node-list/len-05 is used by inv-add5, inv-gc-update-index, inv-gc-copy, inv-transaction, inv-add2, inv-add3, inv-add4,
• list/group-store/len-05 is used by prepost-gc-referenced-nodes,
• list/key-list-set/len-05 is used by inv-gc-copy,
• list/laddress-list/len-05 is used by prepost-gc-referenced-nodes,
• list/address-list-set/len-05 is used by prepost-gc-referenced-nodes, inv-gc-update-index,

Used from specification list-dup

• list-dup/key-list-set/a is used by inv-gc-copy, inv-gc,
• list-dup/address-list-set/a is used by inv-gc-update-index,
• list-dup/laddress-list/a is used by prepost-gc-referenced-nodes, ls-inv-prefixn-ladrs, lf-inv-append-sizes, inv-addn,
• list-dup/key-list-set/c-02 is used by inv-gc-copy,
• list-dup/key-list-set/c-03 is used by inv-gc-copy,
• list-dup/address-list-set/dups-cons is used by inv-gc-update-index,
• list-dup/key-list-set/dups-cons is used by inv-gc-copy,
• list-dup/nat-list-set/e-01 is used by inv-gc-copy, inv-commit, inv-check-commit, inv-format,
• list-dup/address-list-set/e-01 is used by inv-gc-copy,
• list-dup/key-list-set/e-01 is used by inv-gc-copy, inv-gc,
• list-dup/laddress-list/e-01 is used by inv-addn,
• list-dup/nat-list-set/f is used by inv-allocate,
• list-dup/laddress-list/f-01 is used by prepost-gc-referenced-nodes,
• list-dup/key-list-set/f-01 is used by inv-gc-copy,
• list-dup/address-list-set/f-01 is used by inv-gc-update-index,

Used from specification ablock-store-refsize-cons

• ablock-store-refsize-cons/group-store/refsize-cons-def is used by inv-truncate, inv-store,
• ablock-store-refsize-cons/group-store/refsize-cons-remove-index is used by inv-remove,
• ablock-store-refsize-cons/group-store/refsize-cons-write is used by inv-addn,
• ablock-store-refsize-cons/group-store/size-rem is used by inv-truncate,
• ablock-store-refsize-cons/group-store/refsize-cons-dealloc is used by inv-gc,
• ablock-store-refsize-cons/group-store/refsize-cons-emtpy is used by inv-format,
• ablock-store-refsize-cons/group-store/refsize-cons-remove-refsize0 is used by inv-commit, inv-check-commit,
• ablock-store-refsize-cons/group-store/refsize-cons-write is used by inv-allocate, inv-addn,
• ablock-store-refsize-cons/group-store/restrict-add is used by inv-store,
• ablock-store-refsize-cons/group-store/restrict-add-other is used by inv-store,
• ablock-store-refsize-cons/group-store/restrict-del is used by inv-truncate, inv-store,
• ablock-store-refsize-cons/group-store/restrict-del-other is used by inv-truncate, inv-store,
• ablock-store-refsize-cons/group-store/restrict-in is used by inv-gc, inv-truncate, inv-store,
• ablock-store-refsize-cons/group-store/restrict-union is used by inv-truncate,
• ablock-store-refsize-cons/group-store/size-emp is used by inv-allocate,
• ablock-store-refsize-cons/group-store/size-rec-simp is used by inv-store,
• ablock-store-refsize-cons/group-store/size-rem is used by inv-store,

Used from specification address-data

• address-data/elim is used by prepost-gc-referenced-nodes, inv-gc-update-index, inv-get, inv-gc, inv-truncate, inv-remove, inv-store, inv-lookup,
• address-data/sel-03 is used by prepost-gc-referenced-nodes, inv-gc-update-index, inv-get, inv-gc, inv-truncate, inv-remove, inv-store, inv-lookup,
• address-data/sel-04 is used by prepost-gc-referenced-nodes,
• address-data/sel-05 is used by prepost-gc-referenced-nodes, inv-gc-update-index, inv-truncate, inv-store,

Used from specification eraseblock

• eraseblock/lebsize-neq-zero is used by inv-gc-copy, inv-allocate,

Used from specification oelem

• oelem/nat-set/irreflexivity is used by term-restore-log, term-remove-nonend-blocks, prepost-split-nodes, prepost-gc-referenced-nodes, ls-inv-prefix-app-prefixn, inv-gc-update-index, inv-transaction, inv-addn, inv-truncate,
• oelem/nat-set/sls is used by inv-addn,
• oelem/nat-set/transitivity is used by prepost-gc-referenced-nodes,

Used from specification gjournal-abs

• gjournal-abs/ladr-split is used by prepost-gc-referenced-nodes,
• gjournal-abs/new-adrs-gstore is used by inv-addn,
• gjournal-abs/nodes-gstore-at is used by prepost-gc-referenced-nodes,
• gjournal-abs/nodes-gstore-in is used by prepost-gc-referenced-nodes,
• gjournal-abs/nodes-referenced-adrs-leb is used by inv-gc,
• gjournal-abs/nodes-transaction is used by inv-addn,
• gjournal-abs/nodes-write-nochange is used by inv-addn,
• gjournal-abs/valid-group-nodes-app-transaction-prefix is used by inv-addn,
• gjournal-abs/abs-log-adr-explicit-in-leb-notin is used by inv-gc,
• gjournal-abs/abs-log-append-one is used by inv-allocate,
• gjournal-abs/abs-log-base is used by inv-gc-copy,
• gjournal-abs/abs-log-change-other is used by inv-allocate,
• gjournal-abs/abs-log-eq-butlast is used by inv-addn,
• gjournal-abs/abs-log-except-refsize-down is used by inv-gc-update-index,
• gjournal-abs/abs-log-write-last is used by inv-addn,
• gjournal-abs/adr-in-index-node-key is used by prepost-gc-referenced-nodes,
• gjournal-abs/adr-in-ri-in-gstore is used by inv-lookup,
• gjournal-abs/adr-in-ri-leb-notin-ginval is used by inv-lookup,
• gjournal-abs/down-block-explicit is used by prepost-gc-referenced-nodes, inv-allocate, inv-addn,
• gjournal-abs/down-store-adr-in-explicit is used by prepost-gc-referenced-nodes,
• gjournal-abs/down-store-at is used by prepost-gc-referenced-nodes, inv-addn,
• gjournal-abs/down-store-in is used by inv-allocate, inv-addn,
• gjournal-abs/down-store-write is used by inv-allocate, inv-addn,
• gjournal-abs/in-ri is used by inv-remove,
• gjournal-abs/insert-subset-old is used by inv-gc-copy,
• gjournal-abs/inter-subset-rem-empty is used by inv-gc-copy,
• gjournal-abs/jnlhd-notin-ginval is used by inv-addn, inv-gc, inv-truncate, inv-remove, inv-store,
• gjournal-abs/key-in-ri-in-fs is used by prepost-gc-referenced-nodes,
• gjournal-abs/nodes-allocate is used by inv-allocate,
• gjournal-abs/nodes-except-refsize-down is used by inv-gc-update-index,
• gjournal-abs/refsize-0-notin-index is used by inv-gc,
• gjournal-abs/refsize-nonzero-notin-ginval is used by inv-gc,
• gjournal-abs/valid-group-nodes-app-transaction is used by inv-addn,
• gjournal-abs/valid-group-nodes-base is used by inv-allocate,
• gjournal-abs/valid-group-nodes-ls is used by prepost-gc-referenced-nodes,
• gjournal-abs/valid-journal-head-valid-group-nodes is used by inv-addn,

Used from specification oset

• oset/nat-set/ls-emptyset is used by inv-format,
• oset/nat-set/ls-rm is used by inv-orphans-remove,

Used from specification list-del

• list-del/group-store/get-append-grt is used by prepost-gc-referenced-nodes,
• list-del/laddress-list/app-05-neg is used by prepost-gc-referenced-nodes,
• list-del/group-store/get-append-less is used by prepost-gc-referenced-nodes,
• list-del/group-store/get-zero-01 is used by prepost-gc-referenced-nodes,
• list-del/laddress-list/pos-y is used by prepost-gc-referenced-nodes,

Used from specification groupnode

• groupnode/elim is used by prepost-gc-referenced-nodes, inv-gc-update-index, inv-addn, inv-gc, inv-truncate, inv-remove, inv-store,
• groupnode/inj is used by prepost-gc-referenced-nodes, inv-truncate, inv-remove, inv-store,
• groupnode/sel is used by prepost-gc-referenced-nodes, inv-gc-update-index, inv-store,
• groupnode/sel-05 is used by inv-addn, inv-gc,

Used from specification index-asm

• index-asm/inv-add-gnds is used by inv-addn,
• index-asm/inv-allocate-gnd is used by inv-allocate,
• index-asm/inv-remove is used by inv-remove,
• index-asm/inv-set-gblock-refsize is used by inv-truncate, inv-remove, inv-store,
• index-asm/inv-store is used by inv-store,
• index-asm/inv-sync is used by inv-addn,
• index-asm/inv-truncate is used by inv-truncate,

Used from specification debug

• debug/debug is used by inv-recover, inv-gc, inv-format,