Used simplifier rules/spec theorems by specification

Used from specification store+set

• store+set/index-store-ablock-store-nat-store/Dom is used by log-disjoint-istore, abs-istore-crash, abs-gstore-crash,
• store+set/group-store-ablock-store-nat-store/Dom is used by abs-gstore-crash, abs-gstore-cleanup-lpt,

Used from specification nat-basic

• nat-basic/a is used by replay-lpt-size, replay-lpt-at-above, replay-lpt-at, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-ididx-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h, cleanup-lpt-n-size, cleanup-lpt-n-read-above, cleanup-lpt-n-at, abs-nodes-inv-flashsize-h,
• nat-basic/add-base is used by abs-nodes-inv-flashsize-h,
• nat-basic/c is used by replay-lpt-size, replay-lpt-at-above, replay-lpt-at, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-ididx-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h, cleanup-lpt-n-size, cleanup-lpt-n-read-above, cleanup-lpt-n-at, abs-nodes-inv-flashsize-h,
• nat-basic/eq-01 is used by abs-nodes-inv-flashsize-h,
• nat-basic/f is used by replay-lpt-size, replay-lpt-at-above, replay-lpt-at, replay-log-at-other, replay-log-at, replay-log-append-one, remove-wbufs-rec, remove-wbufs-at, lpt-ram-flash-write-same, lpt-ram-flash-write-non-group, lpt-ram-flash-write-log-buf, lpt-ram-flash-id-idx, lpt-ram-flash-cleanup, lpt-ram-flash-allocate, lpt-leb-size-write, lpt-leb-size-id-idx, lpt-leb-size-cleanup, lpt-leb-size-at, lpt-free-unref-write, lpt-free-unref-replay-lpt, lpt-free-unref-replay-log, lpt-free-unref-remove-wbufs, lpt-free-unref-cleanup-lpt, log-group-block-write-other, log-group-block-write-at, log-group-block-remove-wbufs, log-group-block-id-idx, log-disjoint-istore, id-idx-write-both, id-idx-lpt-free-unref, id-idx-abs-istore, id-idx-abs-gstore, gc-heap-write-other-h, gc-heap-write-other, gc-heap-write-nochange-h, gc-heap-write-nochange, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-log, gc-heap-update-h, gc-heap-update, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-in, gc-heap-ididx-h, gc-heap-free-h, gc-heap-free, gc-heap-fill-free-h, gc-heap-append-log-h, gc-heap-allocate-h, gc-heap-allocate, freelist-cons-write-lpt-other, freelist-cons-first-free, freelist-cons-add, free-unref-at, cleanup-lpt-to-n, cleanup-lpt-n-size, cleanup-lpt-n-read-above, cleanup-lpt-n-at, bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, bufs-log-only-notfree, bufs-log-only-id-idx, buf-ro-rw-mode-write-vol-other, buf-ro-rw-mode-write-lpt-other, binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt, avol-replay-lpt-unchanged-write-right, avol-replay-lpt-unchanged-extract-right, avol-cleanup-lpt-unchanged-extract-right, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-replay-lpt-unchanged, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-istore-idcircle, abs-istore-crash, abs-istore-cleanup-lpt, abs-istore-avol-change-other, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other, abs-gstore-idcircle, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,
• nat-basic/l-02 is used by replay-lpt-at-above, cleanup-lpt-n-read-above,
• nat-basic/lf is used by replay-lpt-at-above, gc-heap-write-above, gc-heap-update-h, gc-heap-in-h, gc-heap-free-h, cleanup-lpt-n-read-above, abs-istore-replay-lpt-unchanged, abs-gstore-replay-lpt-unchanged,
• nat-basic/lf-01 is used by lpt-ram-flash-write-same, lpt-ram-flash-write-non-group, lpt-ram-flash-write-log-buf, lpt-ram-flash-id-idx, lpt-ram-flash-cleanup, lpt-ram-flash-allocate, lpt-leb-size-write, lpt-leb-size-id-idx, lpt-leb-size-cleanup, id-idx-write-both, id-idx-lpt-free-unref, id-idx-abs-istore, id-idx-abs-gstore, gc-heap-in-h, bufs-log-only-id-idx, avol-replay-lpt-unchanged-write-right, avol-replay-lpt-unchanged-extract-right, avol-cleanup-lpt-unchanged-extract-right, abs-istore-replay-lpt-unchanged, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-idcircle, abs-istore-crash, abs-istore-cleanup-lpt, abs-gstore-replay-lpt-unchanged, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-idcircle, abs-gstore-crash, abs-gstore-cleanup-lpt,
• nat-basic/lf-02 is used by replay-lpt-at, lpt-leb-size-write, lpt-leb-size-cleanup, gc-heap-update-log-h, gc-heap-in-h, gc-heap-free-h, gc-heap-allocate-h, cleanup-lpt-n-at, bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, bufs-log-only-notfree, bufs-log-only-id-idx, binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt, abs-istore-replay-lpt-unchanged, abs-istore-crash, abs-gstore-replay-lpt-unchanged, abs-gstore-crash,
• nat-basic/ls-02 is used by lpt-leb-size-write, gc-heap-in-h, cleanup-lpt-n-at, abs-istore-replay-lpt-unchanged, abs-gstore-replay-lpt-unchanged,
• nat-basic/s-04 is used by replay-lpt-at, gc-heap-update-log-h, gc-heap-update-h, gc-heap-in-h, gc-heap-free-h, cleanup-lpt-n-at,
• nat-basic/succ is used by replay-lpt-size, replay-lpt-at-above, replay-lpt-at, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-ididx-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h, cleanup-lpt-n-size, cleanup-lpt-n-read-above, cleanup-lpt-n-at, abs-nodes-inv-flashsize-h,
• nat-basic/z-01 is used by abs-nodes-inv-flashsize-h,
• nat-basic/zero-01 is used by replay-lpt-at, gc-heap-update-h, gc-heap-in-h, cleanup-lpt-n-at,

Used from specification ablock

• ablock/group-store/elim is used by id-idx-abs-gstore, abs-istore-crash, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other, abs-gstore-idcircle, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,
• ablock/index-store/elim is used by log-disjoint-istore, id-idx-abs-istore, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-replay-lpt-unchanged, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-istore-idcircle, abs-istore-crash, abs-istore-cleanup-lpt, abs-istore-avol-change-other, abs-gstore-crash,
• ablock/group-store/inj is used by abs-gstore-set-refsize, abs-gstore-replay-lpt-unchanged, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-crash, abs-gstore-cleanup-lpt,
• ablock/index-store/inj is used by abs-istore-set-refsize, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-crash, abs-istore-cleanup-lpt, abs-gstore-crash,
• ablock/group-store/sel-01 is used by id-idx-abs-gstore, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-idcircle, abs-gstore-crash,
• ablock/index-store/sel-01 is used by id-idx-abs-istore, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-crash, abs-gstore-crash,
• ablock/index-store/sel-02 is used by id-idx-abs-istore, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-crash, abs-gstore-crash,
• ablock/group-store/sel-02 is used by id-idx-abs-gstore, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-idcircle, abs-gstore-crash,
• ablock/index-store/sel-03 is used by id-idx-abs-istore, abs-istore-set-lebsize, abs-istore-replay-lpt-unchanged, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-istore-idcircle, abs-istore-crash, abs-istore-cleanup-lpt, abs-istore-avol-change-other,
• ablock/group-store/sel-03 is used by id-idx-abs-gstore, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other, abs-gstore-idcircle, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,

Used from specification array-splice

• array-splice/buffer/append-a is used by abs-nodes-inv-flashsize-h,
• array-splice/buffer/append-len is used by abs-nodes-inv-flashsize-h,

Used from specification node-header-size

• node-header-size/validtrailer-size is used by abs-nodes-inv-flashsize-h,

Used from specification encoding-node-base

• encoding-node-base/encoding-group-node/node-flash-size is used by abs-nodes-inv-flashsize-h,

Used from specification ablock-store-inv

• ablock-store-inv/index-store/at-remove-refsize0 is used by abs-istore-crash,
• ablock-store-inv/index-store/in-remove-refsize0 is used by abs-istore-crash,
• ablock-store-inv/group-store/at-remove-refsize0 is used by abs-gstore-cleanup-lpt,
• ablock-store-inv/index-store/at-remove-refsize0 is used by abs-istore-replay-lpt-unchanged, abs-istore-cleanup-lpt,
• ablock-store-inv/group-store/in-remove-refsize0 is used by abs-gstore-cleanup-lpt,
• ablock-store-inv/index-store/in-remove-refsize0 is used by abs-istore-replay-lpt-unchanged, abs-istore-crash, abs-istore-cleanup-lpt,
• ablock-store-inv/group-store/inv-flashsize-empty is used by abs-nodes-inv-flashsize-h,
• ablock-store-inv/group-store/inv-flashsize-prepend is used by abs-nodes-inv-flashsize-h,
• ablock-store-inv/index-store/prefix-fwd-in is used by abs-istore-crash, abs-gstore-crash,

Used from specification apersistence-base

• apersistence-base/crash-group-at is used by abs-gstore-replay-lpt-unchanged, abs-gstore-crash,
• apersistence-base/crash-group-in is used by abs-gstore-crash,
• apersistence-base/crash-index-at is used by abs-istore-crash,
• apersistence-base/crash-group-in is used by abs-gstore-replay-lpt-unchanged, abs-gstore-crash,
• apersistence-base/crash-index-in is used by abs-istore-crash,
• apersistence-base/elems-append is used by replay-log-append-one,
• apersistence-base/elems-def is used by replay-log-at-other, replay-log-at, replay-log-append-one, lpt-free-unref-replay-log, log-disjoint-istore, abs-istore-crash, abs-gstore-crash,
• apersistence-base/elems-empty is used by replay-log-base, abs-gstore-crash,
• apersistence-base/elems-in-notin-ginval is used by log-disjoint-istore, abs-istore-crash, abs-gstore-crash,
• apersistence-base/fwd-in-log-in-gstore is used by log-disjoint-istore,

Used from specification gc-heap-rename

• gc-heap-rename/id-idx-fwd-0 is used by log-group-block-id-idx, gc-heap-ididx-h,
• gc-heap-rename/id-idx-imp-ls-0 is used by log-group-block-id-idx,
• gc-heap-rename/id-idx-imp-ls-1 is used by gc-heap-ididx-h,

Used from specification bin-min-heap

• bin-min-heap/gc-heap-base/elim is used by binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt,
• bin-min-heap/gc-heap-base/sel-01 is used by binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt,
• bin-min-heap/gc-heap-base/sel-02 is used by binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt,

Used from specification nat

• nat/anti is used by replay-lpt-at, gc-heap-update-log-h, gc-heap-in-h, gc-heap-free-h, cleanup-lpt-n-at,
• nat/fle is used by replay-lpt-at-above, replay-lpt-at, lpt-leb-size-write, lpt-free-unref-replay-lpt, gc-heap-update-log-h, gc-heap-update-h, gc-heap-free-h, gc-heap-append-log-h, cleanup-lpt-n-read-above, cleanup-lpt-n-at, binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt, abs-istore-replay-lpt-unchanged, abs-istore-crash, abs-gstore-replay-lpt-unchanged, abs-gstore-crash,
• nat/fle-01 is used by replay-lpt-at-above, lpt-leb-size-write, lpt-leb-size-id-idx, lpt-leb-size-cleanup, lpt-leb-size-at, lpt-free-unref-replay-lpt, gc-heap-write-above, gc-heap-in-h, cleanup-lpt-n-read-above,
• nat/le-add is used by abs-nodes-inv-flashsize-h,
• nat/le-def is used by lpt-leb-size-write, lpt-leb-size-id-idx, lpt-leb-size-cleanup, lpt-free-unref-replay-lpt, gc-heap-remove-wbufs, gc-heap-in, gc-heap-fill-free, cleanup-lpt-to-n, bin-heap-inv-write-other, abs-istore-replay-lpt-unchanged, abs-istore-crash, abs-gstore-replay-lpt-unchanged, abs-gstore-crash,
• nat/le-ls-simp is used by set-less-ar1, set-less-ar0, replay-lpt-size, replay-lpt-at, lpt-leb-size-write, lpt-leb-size-cleanup, lpt-free-unref-replay-lpt, freelist-cons-write-lpt-other, freelist-cons-alloc, cleanup-lpt-n-size, cleanup-lpt-n-at, buf-ro-rw-mode-write-other-fields, buf-ro-rw-mode-write-lpt-other, abs-istore-set-refsize, abs-istore-lpt-change-other, abs-istore-crash, abs-istore-cleanup-lpt, abs-istore-avol-change-other, abs-gstore-set-refsize, abs-gstore-lpt-change-other, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,
• nat/lels is used by set-less-ar0, replay-lpt-size, replay-lpt-at-above, replay-lpt-at, replay-log-append-one, remove-wbufs-rec, lpt-free-unref-replay-lpt, id-idx-write-both, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h, freelist-cons-write-lpt-other, freelist-cons-alloc, cleanup-lpt-n-size, cleanup-lpt-n-read-above, cleanup-lpt-n-at, buf-ro-rw-mode-write-other-fields, buf-ro-rw-mode-write-lpt-other, binheap-inv-remove-wbufs, abs-nodes-inv-flashsize-h, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-istore-crash, abs-istore-cleanup-lpt, abs-istore-avol-change-other, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,
• nat/lels-02 is used by gc-heap-update-h, gc-heap-free-h, cleanup-lpt-n-at,
• nat/lels-03 is used by replay-lpt-size, replay-lpt-at-above, replay-lpt-at, lpt-free-unref-replay-lpt, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-ididx-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h, cleanup-lpt-n-size, cleanup-lpt-n-read-above, cleanup-lpt-n-at,
• nat/ler is used by replay-lpt-at, id-idx-gcheap, gc-heap-write-other, gc-heap-write-nochange, gc-heap-update-log, gc-heap-update-h, gc-heap-update, gc-heap-in-h, gc-heap-in, gc-heap-free-h, gc-heap-free, gc-heap-append-log, gc-heap-allocate, cleanup-lpt-to-n, cleanup-lpt-n-at, bin-heap-inv-write-other, abs-istore-replay-lpt-unchanged, abs-istore-crash, abs-gstore-replay-lpt-unchanged, abs-gstore-crash,
• nat/lez is used by replay-lpt-at, gc-heap-update-h, cleanup-lpt-n-at,
• nat/ls-le-simp is used by replay-lpt-at, replay-log-append-one, remove-wbufs-rec, lpt-leb-size-write, id-idx-write-both, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h, cleanup-lpt-n-at, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write,
• nat/succ-01 is used by replay-lpt-size, replay-lpt-at-above, replay-lpt-at, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-ididx-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h, cleanup-lpt-n-size, cleanup-lpt-n-read-above, cleanup-lpt-n-at,

Used from specification store

• store/index-store-ablock-store-nat-store/At-other is used by abs-istore-set-refsize,
• store/group-store-ablock-store-nat-store/At-other is used by abs-gstore-set-refsize,
• store/group-store-ablock-store-nat-store/At-other is used by abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write,
• store/index-store-ablock-store-nat-store/At-other is used by abs-istore-reduce-write-idcircle, abs-istore-reduce-write,
• store/index-store-ablock-store-nat-store/At-same is used by abs-istore-set-refsize, abs-istore-reduce-write-idcircle, abs-istore-reduce-write,
• store/group-store-ablock-store-nat-store/At-same is used by abs-gstore-set-refsize, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write,
• store/group-store-ablock-store-nat-store/in-neq is used by abs-gstore-set-refsize, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write,
• store/index-store-ablock-store-nat-store/in-neq is used by abs-istore-set-refsize, abs-istore-reduce-write-idcircle, abs-istore-reduce-write,
• store/index-store-ablock-store-nat-store/insin is used by abs-istore-set-refsize, abs-istore-reduce-write-idcircle, abs-istore-reduce-write,
• store/group-store-ablock-store-nat-store/insin is used by abs-gstore-set-refsize, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write,
• store/group-store-ablock-store-nat-store/notmemlookup is used by id-idx-abs-gstore, abs-istore-crash, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-lpt-change-other, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,
• store/index-store-ablock-store-nat-store/notmemlookup is used by id-idx-abs-istore, abs-istore-set-lebsize, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-istore-crash, abs-istore-cleanup-lpt, abs-istore-avol-change-other, abs-gstore-crash,

Used from specification set-union

• set-union/nat-set/Intersect is used by abs-gstore-cleanup-lpt,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/unrax is used by gc-heap-update-h,
• set-union/nat-set/unrax is used by abs-gstore-crash,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/Delete is used by gc-heap-update-h, gc-heap-free-h, gc-heap-append-log-h,
• set-union/nat-set/Intersect is used by log-disjoint-istore,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/One is used by gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-ididx-h, gc-heap-free-h, gc-heap-allocate-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/del-addeq-05 is used by gc-heap-update-h, gc-heap-free-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/del-e-01 is used by gc-heap-update-h, gc-heap-free-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/del-in is used by gc-heap-free-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/del-in-03 is used by gc-heap-free-h,
• set-union/nat-set/int-a is used by log-disjoint-istore, abs-istore-crash, abs-gstore-crash,
• set-union/nat-set/int-c is used by log-disjoint-istore, abs-istore-crash, abs-gstore-crash,
• set-union/nat-set/int-e is used by abs-gstore-crash,
• set-union/nat-set/una is used by log-disjoint-istore,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/una is used by gc-heap-write-other-h, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/unadd is used by gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-allocate-h,
• set-union/nat-set/unc is used by log-disjoint-istore,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/unc is used by gc-heap-write-other-h, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/undel-02 is used by gc-heap-update-h, gc-heap-free-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/une is used by gc-heap-write-other-h, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/uneq is used by gc-heap-write-other-h, gc-heap-remove-wbufs-h, gc-heap-free-h, gc-heap-allocate-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/unin is used by gc-heap-in-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/unin-01 is used by gc-heap-in-h,
• set-union/gc-heap-rename-gc-heap-base-keyindex-set/union-rem-unchdg is used by gc-heap-free-h,

Used from specification abs-list

• abs-list/encoding-group-node/abs-nodes is used by abs-nodes-inv-flashsize,
• abs-list/encoding-group-node/abs-nodes-rec is used by abs-nodes-inv-flashsize-h,
• abs-list/encoding-index-node/abs-nodes-elems-adr-length is used by id-idx-abs-istore, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-crash, abs-gstore-crash,
• abs-list/encoding-group-node/abs-nodes-elems-adr-length is used by id-idx-abs-gstore, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-idcircle, abs-gstore-crash,
• abs-list/encoding-group-node/abs-nodes-elems-adr-length-h is used by abs-nodes-inv-flashsize-h,
• abs-list/encoding-index-node/abs-nodes-nospace is used by abs-gstore-crash,
• abs-list/encoding-index-node/abs-nodes-strong-imp-weak is used by abs-istore-set-lebsize, abs-istore-crash,
• abs-list/encoding-group-node/abs-nodes-strong-imp-weak is used by abs-gstore-set-lebsize, abs-gstore-crash,
• abs-list/encoding-group-node/abs-nodes-unique-strong is used by abs-gstore-crash,
• abs-list/encoding-group-node/abs-nodes-unique-weak is used by abs-gstore-set-lebsize, abs-gstore-crash,
• abs-list/encoding-index-node/abs-nodes-unique-weak is used by abs-istore-set-lebsize, abs-istore-crash,

Used from specification lprops

• lprops/disj-01 is used by lpt-ram-flash-cleanup, lpt-free-unref-replay-log, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-allocate-h, bufs-log-only-write-lpt-free, bufs-log-only-notfree, abs-gstore-replay-lpt-unchanged, abs-gstore-crash, abs-gstore-cleanup-lpt,
• lprops/disj-02 is used by lpt-ram-flash-write-log-buf, log-disjoint-istore, abs-istore-crash, abs-gstore-crash,
• lprops/disj-03 is used by replay-lpt-size, replay-lpt-at-above, replay-lpt-at, bufs-log-only-write-lpt-free, bufs-log-only-notfree, abs-istore-replay-lpt-unchanged, abs-istore-crash, abs-istore-cleanup-lpt, abs-gstore-crash,
• lprops/elim is used by replay-lpt-size, replay-lpt-at-above, replay-lpt-at, replay-log-at, replay-log-append-one, lpt-ram-flash-write-same, lpt-ram-flash-write-non-group, lpt-ram-flash-write-log-buf, lpt-ram-flash-id-idx, lpt-ram-flash-cleanup, lpt-ram-flash-allocate, lpt-leb-size-write, lpt-leb-size-id-idx, lpt-leb-size-cleanup, lpt-free-unref-write, lpt-free-unref-replay-lpt, lpt-free-unref-replay-log, lpt-free-unref-remove-wbufs, lpt-free-unref-cleanup-lpt, log-group-block-write-other, log-group-block-write-at, log-group-block-remove-wbufs, log-group-block-id-idx, log-disjoint-istore, id-idx-write-both, id-idx-lpt-free-unref, id-idx-freelist-cons, id-idx-abs-istore, id-idx-abs-gstore, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-in, gc-heap-ididx-h, gc-heap-free-h, gc-heap-append-log-h, gc-heap-allocate-h, freelist-cons-write-lpt-other, freelist-cons-remove-wbufs, freelist-cons-first-free, freelist-cons-alloc, freelist-cons-add, cleanup-lpt-to-n, cleanup-lpt-n-size, cleanup-lpt-n-read-above, cleanup-lpt-n-at, bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, bufs-log-only-id-idx, buf-ro-rw-mode-write-vol-other, buf-ro-rw-mode-write-other-fields, buf-ro-rw-mode-write-lpt-other, buf-ro-rw-mode-id-idx, binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt, avol-replay-lpt-unchanged-write-right, avol-replay-lpt-unchanged-extract-right, avol-cleanup-lpt-unchanged-extract-right, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-replay-lpt-unchanged, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-istore-idcircle, abs-istore-crash, abs-istore-cleanup-lpt, abs-istore-avol-change-other, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other, abs-gstore-idcircle, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,
• lprops/inj is used by replay-lpt-at, lpt-ram-flash-write-same, lpt-ram-flash-write-non-group, lpt-ram-flash-write-log-buf, lpt-ram-flash-cleanup, lpt-leb-size-write, lpt-leb-size-cleanup, lpt-free-unref-write, lpt-free-unref-replay-lpt, lpt-free-unref-replay-log, lpt-free-unref-remove-wbufs, lpt-free-unref-cleanup-lpt, log-group-block-write-at, log-group-block-remove-wbufs, id-idx-write-both, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-update-h, gc-heap-remove-wbufs-h, gc-heap-in-h, gc-heap-free-h, gc-heap-append-log-h, gc-heap-allocate-h, freelist-cons-write-lpt-other, freelist-cons-remove-wbufs, freelist-cons-alloc, freelist-cons-add, cleanup-lpt-n-at, bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, bufs-log-only-id-idx, buf-ro-rw-mode-write-other-fields, buf-ro-rw-mode-write-lpt-other, binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt, avol-replay-lpt-unchanged-write-right, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-replay-lpt-unchanged, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-istore-idcircle, abs-istore-crash, abs-istore-cleanup-lpt, abs-istore-avol-change-other, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other, abs-gstore-idcircle, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,
• lprops/upd-05 is used by replay-lpt-size, replay-lpt-at-above, replay-lpt-at, lpt-free-unref-replay-lpt, lpt-free-unref-remove-wbufs, log-group-block-remove-wbufs, gc-heap-remove-wbufs-h, freelist-cons-remove-wbufs, binheap-inv-remove-wbufs, abs-istore-replay-lpt-unchanged, abs-istore-crash, abs-gstore-replay-lpt-unchanged, abs-gstore-crash,

Used from specification aleb

• aleb/aleb-not-mapped is used by abs-istore-set-refsize, abs-gstore-set-refsize,
• aleb/disj is used by abs-istore-set-refsize, abs-gstore-set-refsize,
• aleb/ex is used by id-idx-abs-istore, id-idx-abs-gstore, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-crash, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-idcircle, abs-gstore-crash,
• aleb/sel is used by id-idx-abs-istore, id-idx-abs-gstore, buf-ro-rw-mode-write, abs-istore-set-lebsize, abs-istore-crash, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-idcircle, abs-gstore-crash,
• aleb/test-02 is used by id-idx-abs-istore, id-idx-abs-gstore, abs-istore-set-lebsize, abs-istore-crash, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-idcircle, abs-gstore-crash,

Used from specification set-basic

• set-basic/nat-set/Extension is used by log-disjoint-istore, abs-gstore-crash, abs-gstore-cleanup-lpt,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/Extension is used by gc-heap-append-log-h, bin-heap-inv-write-other,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/ext-rec is used by gc-heap-update-log-h, gc-heap-update-h,
• set-basic/nat-set/In-empty is used by log-disjoint-istore, abs-gstore-cleanup-lpt,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/In-empty is used by gc-heap-in-h,
• set-basic/nat-set/In-insert is used by replay-log-append-one, remove-wbufs-rec,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/In-insert is used by gc-heap-update-log-h, gc-heap-update-h,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/eq-03 is used by gc-heap-remove-wbufs-h,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/in-02 is used by gc-heap-update-h,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/in-04 is used by gc-heap-update-h, gc-heap-in-h, gc-heap-free-h,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/ne is used by gc-heap-update-h, gc-heap-in-h, gc-heap-free-h,
• set-basic/nat-set/ne-01 is used by set-less-ar1, set-less-ar0, remove-wbufs-rec, remove-wbufs-at, abs-gstore-lpt-change-other, abs-gstore-crash, abs-gstore-avol-change-other,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/ne-01 is used by gc-heap-update-h, gc-heap-in-h, gc-heap-free-h,
• set-basic/nat-set/size-zero is used by log-disjoint-istore,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/size-zero is used by gc-heap-fill-free-h, gc-heap-fill-free,
• set-basic/nat-set/size-zero-01 is used by set-less-ar1, set-less-ar0, remove-wbufs-rec, remove-wbufs-at, log-disjoint-istore, abs-gstore-lpt-change-other, abs-gstore-crash, abs-gstore-avol-change-other,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/size-zero-01 is used by gc-heap-update-h, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-fill-free,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/sub-e is used by gc-heap-write-other-h, gc-heap-remove-wbufs-h, gc-heap-free-h, gc-heap-allocate-h,
• set-basic/gc-heap-rename-gc-heap-base-keyindex-set/sub-one-02 is used by gc-heap-remove-wbufs-h, gc-heap-allocate-h,

Used from specification list-last

• list-last/nat-list-set/lin-02 is used by lpt-ram-flash-write-log-buf,

Used from specification key-index

• key-index/gc-heap-rename-gc-heap-base/elim is used by binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt,
• key-index/gc-heap-rename-gc-heap-base/inj is used by gc-heap-update-h, gc-heap-in-h, gc-heap-free-h, gc-heap-append-log-h,
• key-index/gc-heap-rename-gc-heap-base/sel-01 is used by binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt,

Used from specification list-data

• list-data/laddress-list/elim-list-c is used by abs-nodes-inv-flashsize-h,
• list-data/group-store/l is used by abs-nodes-inv-flashsize-h,
• list-data/laddress-list/l is used by abs-nodes-inv-flashsize-h,
• list-data/group-store/size-01 is used by abs-nodes-inv-flashsize-h,
• list-data/laddress-list/size-01 is used by abs-nodes-inv-flashsize-h,

Used from specification array-indices

• array-indices/lp-array/map-at is used by lpt-ram-flash-cleanup, lpt-leb-size-cleanup, lpt-free-unref-cleanup-lpt, cleanup-lpt-to-n, bin-heap-inv-cleanup-lpt, abs-istore-cleanup-lpt, abs-gstore-cleanup-lpt,
• array-indices/lp-array/mapindices-at is used by replay-log-at-other, replay-log-at, replay-log-append-one, remove-wbufs-rec, remove-wbufs-at, lpt-free-unref-replay-log, lpt-free-unref-remove-wbufs, log-group-block-remove-wbufs, gc-heap-remove-wbufs-h, freelist-cons-remove-wbufs, binheap-inv-remove-wbufs, abs-istore-crash, abs-gstore-crash,
• array-indices/lp-array/map-indices-empty is used by replay-log-base, remove-wbufs-empty,
• array-indices/lp-array/map-size is used by lpt-ram-flash-cleanup, lpt-leb-size-cleanup, lpt-free-unref-cleanup-lpt, cleanup-lpt-to-n, cleanup-lpt-size, bin-heap-inv-cleanup-lpt, abs-istore-cleanup-lpt, abs-gstore-cleanup-lpt,
• array-indices/lp-array/mapindices-size is used by replay-log-size, replay-log-append-one, remove-wbufs-size, remove-wbufs-rec, lpt-free-unref-replay-log, lpt-free-unref-remove-wbufs, log-group-block-remove-wbufs, gc-heap-remove-wbufs-h, gc-heap-remove-wbufs, freelist-cons-remove-wbufs, binheap-inv-remove-wbufs, abs-istore-crash, abs-gstore-crash,

Used from specification laddress

• laddress/elim is used by abs-nodes-inv-flashsize-h,
• laddress/sel-01 is used by abs-nodes-inv-flashsize-h,

Used from specification bin-min-heap-inv

• bin-min-heap-inv/gc-heap-rename-gc-heap-base/key-set-extract-index is used by bin-heap-inv-write-other,
• bin-min-heap-inv/gc-heap-rename-gc-heap-base/valid-idx is used by binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt,
• bin-min-heap-inv/gc-heap-rename-gc-heap-base/valid-idx-last-valid is used by binheap-inv-remove-wbufs,

Used from specification list

• list/nat-list-set/a is used by replay-log-append-one, lpt-ram-flash-write-allocate, lpt-ram-flash-allocate, gc-heap-append-log-h, gc-heap-allocate-h, freelist-cons-first-free, freelist-cons-alloc, freelist-cons-add,
• list/group-store/a is used by abs-nodes-inv-flashsize-h,
• list/laddress-list/a is used by abs-nodes-inv-flashsize-h,
• list/group-store/c is used by abs-nodes-inv-flashsize-h,
• list/laddress-list/c is used by abs-nodes-inv-flashsize-h,
• list/laddress-list/e-01 is used by abs-nodes-inv-flashsize-h,
• list/nat-list-set/in-17 is used by lpt-ram-flash-write-allocate, lpt-ram-flash-allocate, gc-heap-allocate-h, freelist-cons-add,
• list/nat-list-set/in-append is used by lpt-ram-flash-write-allocate, lpt-ram-flash-allocate, gc-heap-allocate-h, freelist-cons-add,
• list/nat-list-set/in-empty is used by lpt-ram-flash-cleanup, log-group-block-empty, abs-gstore-crash,
• list/nat-list-set/in-rec is used by gc-heap-append-log-h, freelist-cons-first-free, freelist-cons-alloc,
• list/laddress-list/len-05 is used by abs-nodes-inv-flashsize-h,
• list/group-store/len-05 is used by abs-nodes-inv-flashsize-h,

Used from specification array-copy

• array-copy/avolume/Idexcept is used by abs-istore-reduce-write-idcircle, abs-istore-idcircle, abs-gstore-reduce-write-idcircle, abs-gstore-idcircle,
• array-copy/lp-array/at-fill-mkarray is used by gc-heap-fill-free-h,
• array-copy/avolume/idexcept-size is used by abs-istore-reduce-write-idcircle, abs-istore-idcircle, abs-gstore-reduce-write-idcircle, abs-gstore-idcircle,
• array-copy/lp-array/size-fill is used by gc-heap-fill-free-h, gc-heap-fill-free,

Used from specification list-dup

• list-dup/nat-list-set/f is used by freelist-cons-add,
• list-dup/nat-list-set/rec is used by freelist-cons-first-free, freelist-cons-alloc,

Used from specification abs-node

• abs-node/encoding-group-node/abs-node is used by abs-nodes-inv-flashsize-h,
• abs-node/encoding-group-node/abs-node-emptybuf is used by abs-nodes-inv-flashsize-h,
• abs-node/encoding-index-node/abs-padding-mkbuf0 is used by abs-nodes-inv-flashsize-h,
• abs-node/encoding-index-node/buf-size-zero is used by abs-nodes-inv-flashsize-h,
• abs-node/encoding-index-node/lfw-is-encoded-nodeheader-size is used by abs-nodes-inv-flashsize-h,

Used from specification bufleb

• bufleb/disj is used by lpt-ram-flash-write-log-buf, bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, bufs-log-only-notfree, bufs-log-only-id-idx,
• bufleb/elim is used by bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, bufs-log-only-id-idx,
• bufleb/elim-is-buf-ant is used by buf-ro-rw-mode-write-vol-other, buf-ro-rw-mode-write-lpt-other, buf-ro-rw-mode-switch,
• bufleb/inj is used by buf-ro-rw-mode-write-vol-other, buf-ro-rw-mode-write-lpt-other,
• bufleb/sel is used by lpt-ram-flash-write-log-buf, bufs-log-only-notfree, buf-ro-rw-mode-write-vol-other, buf-ro-rw-mode-write-lpt-other, buf-ro-rw-mode-write, buf-ro-rw-mode-switch, buf-ro-rw-mode-leb-size,
• bufleb/test-01 is used by buf-ro-rw-mode-nobuffer,
• bufleb/test-02 is used by buf-ro-rw-mode-write, buf-ro-rw-mode-switch, buf-ro-rw-mode-leb-size,

Used from specification nat-mult

• nat-mult/mult-a is used by abs-nodes-inv-flashsize-h,
• nat-mult/mult-c is used by abs-nodes-inv-flashsize-h,
• nat-mult/numeral-19 is used by abs-nodes-inv-flashsize-h,
• nat-mult/one is used by abs-nodes-inv-flashsize-h,

Used from specification oelem

• oelem/nat-set/irreflexivity is used by lpt-leb-size-write, lpt-leb-size-id-idx, lpt-leb-size-at, gc-heap-update-h, gc-heap-remove-wbufs, gc-heap-in-h, gc-heap-in, gc-heap-free-h, gc-heap-fill-free, cleanup-lpt-to-n, cleanup-lpt-n-at, bin-heap-inv-write-other, abs-istore-replay-lpt-unchanged, abs-istore-crash, abs-gstore-replay-lpt-unchanged, abs-gstore-crash,
• oelem/nat-set/ls-le is used by gc-heap-in-h,
• oelem/nat-set/sls is used by cleanup-lpt-n-at,
• oelem/nat-set/transitivity is used by replay-lpt-at-above, gc-heap-write-above, cleanup-lpt-n-read-above, abs-istore-replay-lpt-unchanged, abs-gstore-replay-lpt-unchanged,

Used from specification awbuf-inv

• awbuf-inv/align-down-is-aligned is used by abs-istore-crash,
• awbuf-inv/down-arrow-block-def is used by abs-istore-crash, abs-gstore-crash,
• awbuf-inv/down-arrow-def is used by abs-istore-crash, abs-gstore-crash,
• awbuf-inv/synced is used by abs-istore-crash, abs-gstore-crash,
• awbuf-inv/align-down-is-aligned is used by abs-gstore-crash,

Used from specification array

• array/lp-array/Extension is used by replay-log-append-one, remove-wbufs-rec, cleanup-lpt-to-n,
• array/lp-array/Put-other is used by replay-lpt-at, replay-log-append-one, lpt-ram-flash-write-same, lpt-ram-flash-write-log-buf, id-idx-write-both, bin-heap-inv-write-other-fields, bin-heap-inv-write-other,
• array/avolume/Put-other is used by buf-ro-rw-mode-write-vol-other, avol-replay-lpt-unchanged-write-right, abs-istore-reduce-write, abs-istore-avol-change-other, abs-gstore-reduce-write, abs-gstore-avol-change-other,
• array/lp-array/Put-other is used by replay-lpt-at, remove-wbufs-rec, lpt-ram-flash-write-non-group, lpt-ram-flash-write-allocate, lpt-leb-size-write, lpt-free-unref-write, log-group-block-write-other, log-group-block-write-at, id-idx-write-both, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-update-h, gc-heap-free-h, gc-heap-allocate-h, freelist-cons-write-lpt-other, freelist-cons-alloc, freelist-cons-add, cleanup-lpt-n-at, bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, buf-ro-rw-mode-write-other-fields, buf-ro-rw-mode-write-lpt-other, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other,
• array/lp-array/Put-same is used by lpt-ram-flash-write-same, lpt-ram-flash-write-non-group, lpt-ram-flash-write-log-buf, lpt-ram-flash-write-allocate, lpt-leb-size-write, lpt-free-unref-write, log-group-block-write-other, log-group-block-write-at, id-idx-write-both, gc-heap-write-other-h, gc-heap-write-nochange-h, gc-heap-update-h, gc-heap-free-h, freelist-cons-write-lpt-other, freelist-cons-add, bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, buf-ro-rw-mode-write, buf-ro-rw-mode-leb-size, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, abs-istore-set-lebsize, abs-istore-lpt-change-other, abs-gstore-set-lebsize, abs-gstore-lpt-change-other,
• array/avolume/Put-same is used by buf-ro-rw-mode-write, avol-replay-lpt-unchanged-write-right, abs-istore-reduce-write, abs-gstore-reduce-write,
• array/lp-array/Size-mkarray is used by gc-heap-fill-free-h, gc-heap-fill-free,
• array/buffer/Size-mkarray is used by abs-nodes-inv-flashsize-h,
• array/lp-array/Size-put is used by replay-lpt-size, replay-log-append-one, remove-wbufs-rec, lpt-ram-flash-write-same, lpt-ram-flash-write-non-group, lpt-ram-flash-write-log-buf, lpt-ram-flash-write-log, lpt-ram-flash-write-allocate, lpt-leb-size-write, lpt-free-unref-write, log-group-block-write-other, log-group-block-write-at, id-idx-write-both, gc-heap-write-other-h, gc-heap-write-other, gc-heap-write-nochange-h, gc-heap-write-nochange, gc-heap-write-above, gc-heap-update-log-h, gc-heap-update-log, gc-heap-update-h, gc-heap-update, gc-heap-free-h, gc-heap-free, gc-heap-allocate-h, gc-heap-allocate, freelist-cons-write-lpt-other, freelist-cons-alloc, freelist-cons-add, cleanup-lpt-n-size, bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, buf-ro-rw-mode-write-other-fields, buf-ro-rw-mode-write-lpt-other, buf-ro-rw-mode-write, buf-ro-rw-mode-leb-size, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other,
• array/avolume/Size-put is used by avol-replay-lpt-unchanged-write-right,
• array/lp-array/cgetput is used by replay-lpt-at, replay-log-append-one, remove-wbufs-rec, id-idx-write-both, freelist-cons-alloc, cleanup-lpt-n-at, buf-ro-rw-mode-write-other-fields, buf-ro-rw-mode-write-lpt-other, abs-istore-set-refsize, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-gstore-set-refsize, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write,
• array/lp-array/cngetput is used by lpt-ram-flash-write-non-group, lpt-ram-flash-write-log, lpt-ram-flash-write-allocate, lpt-leb-size-write, gc-heap-write-other-h, gc-heap-update-log-h, gc-heap-free-h, bufs-log-only-write-lpt-same-flags, bufs-log-only-write-lpt-free, abs-istore-lpt-change-other, abs-gstore-lpt-change-other,
• array/lp-array/ngp-06 is used by replay-lpt-at-above, cleanup-lpt-n-read-above,
• array/lp-array/ngp-07 is used by gc-heap-write-above,

Used from specification elem-index

• elem-index/gc-heap-base/sel-01-M01 is used by replay-log-at, replay-log-append-one, lpt-ram-flash-id-idx, lpt-leb-size-id-idx, lpt-leb-size-cleanup, lpt-free-unref-write, lpt-free-unref-replay-lpt, lpt-free-unref-replay-log, lpt-free-unref-cleanup-lpt, log-disjoint-istore, id-idx-lpt-free-unref, id-idx-freelist-cons, id-idx-abs-istore, id-idx-abs-gstore, gc-heap-write-other-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-in, gc-heap-free-h, gc-heap-append-log-h, gc-heap-append-log, gc-heap-allocate-h, free-unref-at, cleanup-lpt-to-n, bufs-log-only-id-idx, buf-ro-rw-mode-id-idx, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt, avol-replay-lpt-unchanged-write-right, avol-replay-lpt-unchanged-extract-right, avol-cleanup-lpt-unchanged-extract-right, abs-istore-replay-lpt-unchanged, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-istore-idcircle, abs-istore-crash, abs-istore-cleanup-lpt, abs-istore-avol-change-other, abs-gstore-replay-lpt-unchanged, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other, abs-gstore-idcircle, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,
• elem-index/gc-heap-base/sel-01-M02 is used by lpt-ram-flash-write-same, lpt-ram-flash-write-non-group, lpt-ram-flash-write-log-buf, lpt-ram-flash-id-idx, lpt-ram-flash-cleanup, lpt-ram-flash-allocate, lpt-leb-size-write, lpt-leb-size-id-idx, lpt-leb-size-at, id-idx-lpt-free-unref, id-idx-freelist-cons, id-idx-abs-istore, id-idx-abs-gstore, bufs-log-only-id-idx, buf-ro-rw-mode-write, buf-ro-rw-mode-leb-size, buf-ro-rw-mode-id-idx, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-crash, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-idcircle, abs-gstore-crash,
• elem-index/gc-heap-base/sel-01-M03 is used by lpt-ram-flash-write-same, lpt-ram-flash-write-non-group, lpt-ram-flash-write-log-buf, lpt-ram-flash-id-idx, lpt-ram-flash-cleanup, lpt-ram-flash-allocate, lpt-leb-size-id-idx, lpt-leb-size-cleanup, lpt-free-unref-write, lpt-free-unref-replay-lpt, lpt-free-unref-replay-log, lpt-free-unref-cleanup-lpt, log-group-block-write-other, log-group-block-write-at, log-disjoint-istore, id-idx-lpt-free-unref, id-idx-freelist-cons, id-idx-abs-istore, id-idx-abs-gstore, gc-heap-write-other-h, gc-heap-write-above, gc-heap-update-log-h, gc-heap-in, gc-heap-free-h, gc-heap-fill-free-h, gc-heap-append-log-h, gc-heap-allocate-h, freelist-cons-write-lpt-other, freelist-cons-first-free, freelist-cons-alloc, freelist-cons-add, free-unref-at, cleanup-lpt-to-n, bufs-log-only-notfree, bufs-log-only-id-idx, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt, avol-replay-lpt-unchanged-write-right, avol-replay-lpt-unchanged-extract-right, avol-cleanup-lpt-unchanged-extract-right, abs-istore-replay-lpt-unchanged, abs-istore-reduce-write-idcircle, abs-istore-reduce-write, abs-istore-lpt-change-other, abs-istore-idcircle, abs-istore-cleanup-lpt, abs-istore-avol-change-other, abs-gstore-replay-lpt-unchanged, abs-gstore-reduce-write-idcircle, abs-gstore-reduce-write, abs-gstore-lpt-change-other, abs-gstore-idcircle, abs-gstore-crash, abs-gstore-cleanup-lpt, abs-gstore-avol-change-other,
• elem-index/gc-heap-base/sel-02 is used by replay-log-at, replay-log-append-one, lpt-leb-size-cleanup, lpt-free-unref-replay-lpt, cleanup-lpt-to-n, bin-heap-inv-cleanup-lpt, abs-istore-replay-lpt-unchanged, abs-istore-crash, abs-istore-cleanup-lpt, abs-gstore-replay-lpt-unchanged, abs-gstore-crash, abs-gstore-cleanup-lpt,

Used from specification abs-leb

• abs-leb/encoding-group-node/abs-leb-def is used by id-idx-abs-gstore, abs-gstore-set-refsize, abs-gstore-set-lebsize, abs-gstore-replay-lpt-unchanged, abs-gstore-idcircle, abs-gstore-crash,
• abs-leb/encoding-index-node/abs-leb-def is used by id-idx-abs-istore, abs-istore-set-refsize, abs-istore-set-lebsize, abs-istore-crash, abs-gstore-crash,

Used from specification index-array

• index-array/gc-heap-base/id-idx is used by lpt-ram-flash-id-idx, lpt-leb-size-id-idx, id-idx-write-both, id-idx-lpt-free-unref, id-idx-gcheap, id-idx-freelist-cons, id-idx-abs-istore, id-idx-abs-gstore, bufs-log-only-id-idx, buf-ro-rw-mode-id-idx,

Used from specification bin-min-heap-prepost

• bin-min-heap-prepost/gc-heap-rename-gc-heap-base/bin-heap-inv-def is used by binheap-inv-remove-wbufs, bin-heap-inv-write-other-fields, bin-heap-inv-write-other, bin-heap-inv-cleanup-lpt,
• bin-min-heap-prepost/gc-heap-rename-gc-heap-base/keyset is used by bin-heap-inv-write-other,

Used from specification oset

• oset/nat-set/Greater is used by set-less-ar1, set-less-ar0, abs-gstore-crash,