Used simplifier rules/spec theorems by specification

Used from specification array-splice

• array-splice/buffer/append-a is used by prepost-read-superblock, prepost-read-orphans,
• array-splice/buffer/append-at is used by prepost-read-log,
• array-splice/buffer/array-split2 is used by prepost-read-log, prepost-decode-orphans,
• array-splice/buffer/copy2append is used by prepost-read-orphans, prepost-read-log,
• array-splice/buffer/copy2append0 is used by prepost-read-lebs,
• array-splice/buffer/emparray-at is used by prepost-read-log,
• array-splice/avolume/range-eq-ext is used by rangeeq-write-right-concrete-below, rangeeq-till-leb5-fwd, rangeeq-subarray-5, rangeeq-subarray,
• array-splice/avolume/range-eq-rec is used by rangeeq-concrete-unfold,
• array-splice/buffer/subarray-append-consec0 is used by prepost-encode-orphans,
• array-splice/buffer/subarray-append-elim-left is used by prepost-read-log,
• array-splice/buffer/subarray-append-shift-right is used by prepost-read-superblock,
• array-splice/buffer/subarray-elim-right is used by prepost-read-orphans,
• array-splice/buffer/subarray-eq-elim is used by prepost-read-superblock,
• array-splice/buffer/subarray-split-size is used by prepost-encode-orphans,
• array-splice/buffer/append-a is used by prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-decode-orphans, prepost-add-log-leb, inv-write, inv-read,
• array-splice/buffer/append-eq-emptyar is used by prepost-decode-orphans,
• array-splice/buffer/append-eq-left is used by prepost-read-lebs,
• array-splice/buffer/append-inj is used by prepost-decode-orphans,
• array-splice/buffer/append-left-size0 is used by prepost-write-orphans, prepost-read-superblock,
• array-splice/buffer/append-len is used by prepost-write-orphans, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-decode-orphans, prepost-add-log-leb, inv-read,
• array-splice/buffer/append-prefix-left is used by prepost-encode-orphans,
• array-splice/buffer/append-zero-left is used by prepost-write-orphans, prepost-write-lebs, prepost-read-orphans, prepost-read-log,
• array-splice/buffer/append-zero-right is used by prepost-read-orphans, prepost-read-log,
• array-splice/buffer/copy-append is used by prepost-read-log,
• array-splice/buffer/emparray-len is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-add-log-leb, inv-read,
• array-splice/buffer/mkemparray0-append-left is used by prepost-write-orphans, prepost-write-lebs, prepost-add-log-leb,
• array-splice/avolume/range-eq-0 is used by inv-commit, inv-format,
• array-splice/buffer/range-eq-0 is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log,
• array-splice/buffer/range-eq-refl is used by prepost-read-lebs, inv-read,
• array-splice/avolume/range-eq-refl is used by prepost-write-lebs,
• array-splice/avolume/rangeeq-write-left-above is used by prepost-write-lebs,
• array-splice/avolume/rangeeq-write-left-below is used by prepost-write-lebs,
• array-splice/buffer/subarray-append-consec0 is used by prepost-write-lebs,
• array-splice/buffer/subarray-append-elim-left is used by prepost-read-log, prepost-decode-orphans,
• array-splice/buffer/subarray-append-elim-left0-simp is used by prepost-read-log, prepost-decode-orphans,
• array-splice/buffer/subarray-append-left is used by prepost-read-superblock, prepost-read-log, prepost-read-lebs, prepost-decode-orphans,
• array-splice/buffer/subarray-append-shift-right-simp-0 is used by prepost-read-log, prepost-decode-orphans,
• array-splice/buffer/subarray-elim-right is used by prepost-read-superblock, prepost-read-log,
• array-splice/buffer/subarray-same-ar-eq is used by prepost-write-lebs,

Used from specification nat-basic

• nat-basic/a is used by rangeeq-write-right-concrete-below, rangeeq-till-leb5-fwd, rangeeq-subarray, rangeeq-lebs-5, rangeeq-lebs, rangeeq-concrete-unfold, prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, prepost-add-log-leb, nat-stuff3, nat-stuff2, nat-stuff1, nat-stuff0, id-circle-subarray-concrete-below, inv-write, inv-read, inv-unmap, inv-remap, inv-add-log-leb, inv-get-volume-size, inv-commit, inv-recover, inv-format,
• nat-basic/add-base is used by rangeeq-till-leb5-fwd, rangeeq-lebs-5, prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-decode-orphans, prepost-add-log-leb, nat-stuff1, inv-write, inv-read,
• nat-basic/c is used by rangeeq-write-right-concrete-below, rangeeq-till-leb5-fwd, rangeeq-subarray, rangeeq-lebs-5, rangeeq-lebs, rangeeq-concrete-unfold, prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, prepost-add-log-leb, nat-stuff3, nat-stuff2, nat-stuff1, nat-stuff0, id-circle-subarray-concrete-below, inv-write, inv-read, inv-unmap, inv-remap, inv-add-log-leb, inv-get-volume-size, inv-commit, inv-recover, inv-format,
• nat-basic/eq-01 is used by prepost-read-lebs, prepost-decode-orphans, prepost-add-log-leb, inv-commit, inv-recover, inv-format,
• nat-basic/eq-02 is used by prepost-read-log, prepost-read-lebs, prepost-encode-orphans, inv-recover,
• nat-basic/eqs is used by prepost-read-orphans, prepost-read-log, prepost-decode-orphans, inv-write, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-recover, inv-format,
• nat-basic/f is used by rangeeq-write-right-concrete-below, rangeeq-till-leb5-fwd, rangeeq-subarray-5, rangeeq-subarray, prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, prepost-add-log-leb, idcircle-concrete-write, id-circle-subarray-concrete-below, avol-down-mapped-eq, inv-write, inv-read, inv-unmap, inv-remap, inv-get-volume-size, inv-commit, inv-recover, inv-format,
• nat-basic/l is used by rangeeq-subarray, prepost-write-lebs, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, prepost-add-log-leb, inv-write, inv-read, inv-unmap, inv-remap, inv-commit, inv-format,
• nat-basic/l-01 is used by prepost-write-lebs, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-lpt, prepost-decode-lpt, inv-format,
• nat-basic/l-02 is used by rangeeq-write-right-concrete-below, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-decode-orphans, prepost-add-log-leb, id-circle-subarray-concrete-below, inv-write, inv-unmap, inv-remap, inv-get-volume-size, inv-commit, inv-recover, inv-format,
• nat-basic/l-05 is used by prepost-read-log, prepost-read-lebs, inv-read,
• nat-basic/l-06 is used by prepost-read-log, inv-write, inv-read, inv-unmap, inv-remap, inv-format,
• nat-basic/l-08 is used by prepost-read-log,
• nat-basic/lf is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-add-log-leb, inv-commit,
• nat-basic/lf-01 is used by prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, prepost-add-log-leb, idcircle-concrete-write, avol-down-mapped-eq, inv-write, inv-read, inv-unmap, inv-remap, inv-commit,
• nat-basic/lf-02 is used by prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, prepost-add-log-leb, inv-write, inv-read, inv-unmap, inv-remap, inv-get-volume-size, inv-commit, inv-recover, inv-format,
• nat-basic/ls-02 is used by prepost-write-lebs, prepost-read-superblock, prepost-read-log, prepost-read-lebs, prepost-encode-orphans,
• nat-basic/nls-fst is used by rangeeq-till-leb5-fwd, prepost-read-log,
• nat-basic/one is used by prepost-read-log, prepost-add-log-leb, inv-commit, inv-recover, inv-format,
• nat-basic/one-01 is used by prepost-write-lebs, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt,
• nat-basic/one-03 is used by prepost-read-log,
• nat-basic/oz is used by rangeeq-concrete-unfold, prepost-encode-orphans, prepost-decode-orphans,
• nat-basic/s-04 is used by prepost-write-lebs, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt,
• nat-basic/succ is used by prepost-read-superblock, prepost-read-log,
• nat-basic/z-01 is used by prepost-write-orphans, prepost-read-lebs, nat-stuff2, inv-write, inv-unmap, inv-remap, inv-recover,
• nat-basic/zero is used by prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-add-log-leb, inv-write, inv-commit, inv-recover, inv-format,
• nat-basic/zero-01 is used by prepost-encode-lpt, prepost-decode-lpt,

Used from specification encoding-lpt

• encoding-lpt/is-encoded is used by prepost-encode-lpt, prepost-decode-lpt,
• encoding-lpt/is-encoded-full is used by prepost-encode-lpt, prepost-decode-lpt,
• encoding-lpt/lpt-lebs is used by inv-format,
• encoding-lpt/lpt-size is used by inv-format,
• encoding-lpt/lptsize-ge-min is used by prepost-encode-lpt,
• encoding-lpt/encoding-shift is used by prepost-encode-lpt,
• encoding-lpt/encoding-unique is used by inv-recover,
• encoding-lpt/lptlebs-lptsize is used by inv-commit, inv-recover, inv-format,
• encoding-lpt/lptlebs-zero is used by inv-recover,
• encoding-lpt/lptsize-zero is used by inv-recover,

Used from specification encoding-page-size-nonempty

• encoding-page-size-nonempty/encoding-ref-node/decode-contract is used by prepost-read-log,
• encoding-page-size-nonempty/encoding-ref-node/encode-contract is used by prepost-add-log-leb,
• encoding-page-size-nonempty/encoding-ref-node/is-encoded-size is used by prepost-read-log, prepost-add-log-leb,
• encoding-page-size-nonempty/encoding-ref-node/is-encoded-unique is used by prepost-read-log, prepost-add-log-leb,

Used from specification nat

• nat/add is used by prepost-read-superblock, prepost-read-lebs,
• nat/add-01 is used by prepost-read-log,
• nat/add-num-03 is used by prepost-add-log-leb, nat-stuff3, inv-commit, inv-recover, inv-format,
• nat/anti is used by prepost-write-lebs, prepost-read-log, prepost-read-lebs, prepost-encode-lpt, prepost-decode-lpt, inv-recover,
• nat/elim-pred-c is used by rangeeq-concrete-unfold, prepost-encode-orphans, prepost-decode-orphans,
• nat/elim-sub is used by prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, inv-write, inv-read, inv-commit, inv-recover, inv-format,
• nat/eq-01 is used by prepost-decode-orphans,
• nat/fle is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-encode-orphans, prepost-decode-orphans, prepost-decode-lpt, inv-read, inv-commit,
• nat/fle-01 is used by rangeeq-till-leb5-fwd, prepost-write-lebs, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-decode-orphans, prepost-add-log-leb, inv-read, inv-commit, inv-recover, inv-format,
• nat/ge is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-add-log-leb, inv-write, inv-read, inv-get-volume-size, inv-commit, inv-recover,
• nat/gr-def is used by prepost-encode-orphans,
• nat/l-num-03 is used by prepost-add-log-leb, inv-commit, inv-format,
• nat/le is used by prepost-write-lebs, inv-commit, inv-format,
• nat/le-add is used by prepost-write-lebs, prepost-read-lebs, prepost-decode-lpt, prepost-add-log-leb, nat-stuff1,
• nat/le-def is used by prepost-write-superblock, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, prepost-add-log-leb, inv-write, inv-read, inv-unmap, inv-remap, inv-get-volume-size, inv-commit, inv-recover, inv-format,
• nat/le-ls-simp is used by prepost-write-lebs, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, inv-read, inv-commit, inv-recover,
• nat/le-num-06 is used by inv-commit,
• nat/lels is used by rangeeq-till-leb5-fwd, prepost-write-orphans, prepost-write-lebs, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-lpt, prepost-add-log-leb, id-circle-subarray-concrete-below, inv-commit, inv-recover, inv-format,
• nat/lels-02 is used by prepost-write-lebs, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-decode-orphans, prepost-decode-lpt,
• nat/lels-03 is used by prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-lpt, prepost-decode-lpt,
• nat/lep is used by rangeeq-lebs, prepost-read-superblock, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-decode-orphans, inv-write, inv-commit, inv-format,
• nat/lep-02 is used by rangeeq-lebs-5, rangeeq-lebs, prepost-write-lebs, prepost-read-log, prepost-read-lebs, prepost-encode-lpt, prepost-decode-orphans, nat-stuff1, nat-stuff0, id-circle-subarray-concrete-below, inv-commit, inv-format,
• nat/ler is used by rangeeq-lebs, prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, prepost-add-log-leb, nat-stuff1, inv-read, inv-commit, inv-recover, inv-format,
• nat/let is used by prepost-write-superblock, prepost-write-lebs, prepost-read-superblock, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, id-circle-subarray-concrete-below, inv-write, inv-commit, inv-recover, inv-format,
• nat/lez is used by rangeeq-lebs-5, prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-lpt, prepost-decode-lpt, inv-commit, inv-format,
• nat/ls-01 is used by prepost-write-lebs, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-lpt,
• nat/ls-le-simp is used by prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-log, prepost-read-lebs, prepost-decode-orphans, nat-stuff0, id-circle-subarray-concrete-below, inv-commit,
• nat/not-zero is used by prepost-write-lebs, prepost-read-lebs, inv-format,
• nat/sub-add is used by prepost-read-lebs, prepost-add-log-leb,
• nat/sub-base is used by prepost-read-orphans, prepost-read-log, prepost-decode-orphans,
• nat/sub-ls is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, inv-read,
• nat/succ-01 is used by prepost-write-lebs, prepost-encode-lpt, prepost-decode-lpt,
• nat/zero is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-decode-orphans, prepost-add-log-leb,

Used from specification set-union

• set-union/nat-set/Difference is used by prepost-encode-orphans,
• set-union/nat-set/del-in is used by ls-del-notin,
• set-union/nat-set/del-size is used by prepost-encode-orphans,
• set-union/nat-set/diff-e is used by prepost-encode-orphans,
• set-union/nat-set/diff-idem is used by prepost-encode-orphans,
• set-union/nat-set/int-a is used by prepost-decode-orphans,
• set-union/nat-set/int-c is used by prepost-decode-orphans,
• set-union/nat-set/int-e is used by prepost-decode-orphans,
• set-union/nat-set/int-empty-02 is used by prepost-decode-orphans,
• set-union/nat-set/int-ins is used by prepost-decode-orphans,
• set-union/nat-set/intersect-add-rem is used by prepost-decode-orphans,
• set-union/nat-set/sub-del-03 is used by prepost-encode-orphans,
• set-union/nat-set/subseteq-rem-del is used by prepost-encode-orphans,

Used from specification error-class

• error-class/ecommit is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-add-log-leb, inv-read, inv-commit, inv-format,
• error-class/enoent is used by prepost-read-log,
• error-class/enospc is used by prepost-write-superblock, prepost-encode-orphans,
• error-class/esuccess is used by prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-recover-main-same, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-add-log-leb, inv-write, inv-read, inv-remap, inv-commit, inv-recover, inv-format,
• error-class/not-esuccess is used by prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-recover-main-same, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-decode-orphans, prepost-add-log-leb, inv-write, inv-read, inv-remap, inv-add-log-leb, inv-commit, inv-recover, inv-format,

Used from specification error

• error/disj-33 is used by prepost-read-log,
• error/disj-35 is used by prepost-write-superblock, prepost-encode-orphans,
• error/disj-91 is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-add-log-leb, inv-read, inv-commit, inv-format,

Used from specification aleb

• aleb/aleb-not-mapped is used by prepost-read-log, prepost-read-lebs, inv-read,
• aleb/disj is used by prepost-read-log, prepost-read-lebs, avol-down-mapped-eq, inv-read,
• aleb/ex is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-add-log-leb, inv-write, inv-read, inv-unmap, inv-remap, inv-requires-commit, inv-add-log-leb, inv-get-volume-size, inv-commit, inv-recover, inv-format,
• aleb/inj is used by prepost-write-superblock, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-add-log-leb, inv-write, inv-read, inv-add-log-leb, inv-commit, inv-format,
• aleb/sel is used by prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-add-log-leb, inv-write, inv-read, inv-unmap, inv-remap, inv-requires-commit, inv-add-log-leb, inv-get-volume-size, inv-commit, inv-recover, inv-format,
• aleb/test-01 is used by inv-unmap, inv-commit,
• aleb/test-02 is used by prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-add-log-leb, avol-down-mapped-eq, inv-write, inv-read, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-recover, inv-format,

Used from specification encoding-fixed-size

• encoding-fixed-size/encoding-lprops/encoding-requires-space is used by prepost-encode-lpt,
• encoding-fixed-size/encoding-nat/encoding-requires-space is used by prepost-write-orphans, prepost-read-orphans, prepost-decode-orphans,
• encoding-fixed-size/encoding-lprops/encoding-size is used by prepost-encode-lpt, prepost-decode-lpt,
• encoding-fixed-size/encoding-nat/encoding-size is used by prepost-encode-orphans, prepost-decode-orphans,
• encoding-fixed-size/encoding-lprops/is-encoded-size is used by prepost-decode-lpt,
• encoding-fixed-size/encoding-nat/is-encoded-size is used by prepost-encode-orphans, prepost-decode-orphans,

Used from specification set-basic

• set-basic/nat-set/Extension is used by prepost-encode-orphans,
• set-basic/nat-set/In-empty is used by prepost-encode-orphans, prepost-decode-orphans,
• set-basic/nat-set/Size-empty is used by prepost-write-orphans, prepost-encode-orphans,
• set-basic/nat-set/ne-01 is used by prepost-encode-orphans, prepost-decode-orphans,
• set-basic/nat-set/size-zero is used by prepost-write-orphans, prepost-read-orphans, prepost-encode-orphans,
• set-basic/nat-set/size-zero-01 is used by prepost-write-orphans, prepost-read-orphans, prepost-encode-orphans, prepost-decode-orphans,
• set-basic/nat-set/sub-e is used by prepost-encode-orphans,
• set-basic/nat-set/sub-idem is used by prepost-encode-orphans,
• set-basic/nat-set/sub-in is used by prepost-encode-orphans,

Used from specification ref-node

• ref-node/elim is used by prepost-read-log,

Used from specification encoding

• encoding/encoding-lprops/decode-contract is used by prepost-decode-lpt,
• encoding/encoding-nat/decode-contract is used by prepost-decode-orphans,
• encoding/encoding-nat/encode-contract is used by prepost-encode-orphans,
• encoding/encoding-lprops/encode-contract is used by prepost-encode-lpt,
• encoding/encoding-superblock/is-encoded-unique-size is used by prepost-read-superblock,
• encoding/encoding-nat/is-encoded-prefix is used by prepost-decode-orphans,
• encoding/encoding-superblock/is-encoded-prefix is used by prepost-read-superblock,
• encoding/encoding-superblock/is-encoded-unique is used by prepost-read-superblock,
• encoding/encoding-lprops/is-encoded-unique is used by prepost-decode-lpt,
• encoding/encoding-nat/is-encoded-unique is used by prepost-encode-orphans, prepost-decode-orphans,

Used from specification encoding-elem-alignment

• encoding-elem-alignment/encoding-superblock/alignment-not-zero is used by prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-read-orphans, prepost-read-log, prepost-encode-orphans, prepost-add-log-leb, inv-write, inv-commit, inv-format,

Used from specification align

• align/between-is-aligned is used by prepost-read-log,
• align/is-aligned-intro is used by prepost-read-log,
• align/alignup-div-mult is used by inv-format,
• align/alignup-is-aligned is used by prepost-write-superblock, prepost-encode-orphans,
• align/alignup-is-bigger is used by prepost-encode-orphans,
• align/alignup-le-is-aligned is used by prepost-encode-orphans,
• align/is-aligned-add is used by prepost-read-orphans, prepost-read-log, prepost-encode-orphans,
• align/is-aligned-ls-eq-zero is used by prepost-read-log, prepost-add-log-leb,
• align/is-aligned-same is used by prepost-read-log, prepost-add-log-leb,
• align/is-aligned-zero is used by prepost-write-orphans, prepost-write-lebs, prepost-read-log, prepost-add-log-leb, inv-write, inv-commit, inv-format,

Used from specification superblock

• superblock/elim is used by prepost-read-orphans, prepost-read-log, prepost-add-log-leb, inv-write, inv-read, inv-unmap, inv-remap, inv-requires-commit, inv-add-log-leb, inv-get-volume-size, inv-commit, inv-recover,
• superblock/sel-07 is used by inv-commit, inv-recover,
• superblock/sel-08 is used by inv-commit, inv-recover,
• superblock/sel-09 is used by prepost-read-log, prepost-add-log-leb, inv-add-log-leb, inv-commit, inv-recover,
• superblock/sel-10 is used by prepost-read-orphans, prepost-add-log-leb, inv-add-log-leb, inv-commit, inv-recover,
• superblock/sel-11 is used by prepost-read-orphans, inv-add-log-leb, inv-commit, inv-recover,
• superblock/sel-12 is used by prepost-add-log-leb, inv-add-log-leb, inv-commit, inv-recover,
• superblock/sel-13 is used by prepost-read-orphans, prepost-add-log-leb, inv-write, inv-read, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-recover,
• superblock/upd-07 is used by inv-commit, inv-format,
• superblock/upd-08 is used by inv-commit, inv-format,
• superblock/upd-09 is used by inv-commit, inv-format,
• superblock/upd-10 is used by inv-commit, inv-format,
• superblock/upd-11 is used by inv-commit, inv-format,
• superblock/upd-12 is used by inv-commit, inv-format,
• superblock/upd-13 is used by inv-format,
• superblock/updsel-02 is used by inv-format,
• superblock/updsel-04 is used by inv-format,
• superblock/updsel-14 is used by inv-format,
• superblock/updsel-16 is used by inv-format,
• superblock/updsel-26 is used by inv-format,
• superblock/updsel-28 is used by inv-format,
• superblock/updsel-29 is used by inv-format,
• superblock/updsel-32 is used by inv-format,
• superblock/updsel-35 is used by inv-format,
• superblock/updsel-36 is used by inv-format,
• superblock/updsel-37 is used by inv-format,
• superblock/updsel-38 is used by inv-format,
• superblock/updsel-39 is used by inv-format,
• superblock/updsel-40 is used by inv-format,
• superblock/updsel-41 is used by inv-format,
• superblock/updsel-42 is used by inv-format,
• superblock/updsel-43 is used by inv-format,
• superblock/updsel-44 is used by inv-format,
• superblock/updsel-45 is used by inv-format,
• superblock/updsel-46 is used by inv-format,
• superblock/updsel-47 is used by inv-format,
• superblock/updsel-48 is used by inv-format,
• superblock/updsel-53 is used by inv-format,
• superblock/updsel-54 is used by inv-format,
• superblock/updsel-55 is used by inv-format,
• superblock/updsel-57 is used by inv-format,
• superblock/updsel-58 is used by inv-format,
• superblock/updsel-61 is used by inv-format,

Used from specification ebm-vol-inv

• ebm-vol-inv/ebm-vol-inv is used by prepost-read-superblock, prepost-read-orphans,
• ebm-vol-inv/ebm-vol-inv-lebsize is used by inv-read,
• ebm-vol-inv/ebm-vol-le is used by avol-down-size-le, avol-down-mapped-eq, inv-recover,
• ebm-vol-inv/ebm-vol-inv-lebsize is used by prepost-read-orphans, prepost-read-log, prepost-read-lebs,
• ebm-vol-inv/ebm-vol-inv-write is used by inv-unmap, inv-commit, inv-format,
• ebm-vol-inv/le-inv is used by inv-recover,
• ebm-vol-inv/le-size-0 is used by inv-recover,
• ebm-vol-inv/le-size-2 is used by avol-down-size, inv-recover,

Used from specification list

• list/nat-list-set/Last is used by prepost-read-log, prepost-add-log-leb, inv-add-log-leb,
• list/nat-list-set/a is used by inv-add-log-leb,
• list/nat-list-set/app-04 is used by inv-add-log-leb,
• list/nat-list-set/e is used by inv-add-log-leb,

Used from specification array-copy

• array-copy/avolume/Idexcept is used by idcircle-concrete-write, id-circle-subarray-concrete-below,
• array-copy/avolume/at-fill is used by inv-format,
• array-copy/avolume/idexcept-extract-left is used by inv-commit, inv-format,
• array-copy/buffer/subarray-elim is used by prepost-read-orphans, prepost-read-log,
• array-copy/avolume/at-fill-mkarray is used by inv-format,
• array-copy/buffer/copy-exact is used by prepost-read-superblock, prepost-read-log,
• array-copy/avolume/idexcept-refl is used by prepost-write-superblock, prepost-write-orphans,
• array-copy/avolume/idexcept-size is used by idcircle-concrete-write, id-circle-subarray-concrete-below, inv-commit, inv-format,
• array-copy/avolume/idexcept-write-at0 is used by prepost-write-superblock, prepost-write-orphans,
• array-copy/buffer/size-copy is used by prepost-read-log, prepost-read-lebs,
• array-copy/lp-array/size-fill is used by inv-recover,
• array-copy/avolume/size-fill is used by inv-format,
• array-copy/avolume/size-subarray is used by rangeeq-subarray-5, rangeeq-subarray, id-circle-subarray-concrete-below, inv-format,
• array-copy/buffer/size-subarray is used by prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-encode-orphans, prepost-decode-orphans, prepost-decode-lpt,
• array-copy/avolume/subarray-at is used by rangeeq-subarray-5, rangeeq-subarray, id-circle-subarray-concrete-below, inv-format,
• array-copy/buffer/subarray-at is used by prepost-read-log,
• array-copy/buffer/subarray-copy-elim-exact is used by prepost-read-log,
• array-copy/buffer/subarray-elim is used by prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-decode-orphans, prepost-add-log-leb,
• array-copy/avolume/subarray-write-below is used by prepost-add-log-leb, inv-commit,
• array-copy/buffer/subarray-zero is used by prepost-write-lebs, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-decode-orphans,

Used from specification encoding-log

• encoding-log/is-encoded-app is used by prepost-read-log,
• encoding-log/is-encoded-app-one is used by prepost-add-log-leb,
• encoding-log/is-encoded-emptypage-middle is used by prepost-read-log,
• encoding-log/is-encoded-base is used by prepost-read-log, inv-commit, inv-format,
• encoding-log/is-encoded-empty is used by inv-commit, inv-format,
• encoding-log/is-encoded-one is used by prepost-read-log,
• encoding-log/is-encoded-pagealigned is used by prepost-read-log, prepost-add-log-leb,
• encoding-log/is-encoded-unique is used by prepost-read-log, prepost-add-log-leb, inv-write, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-recover,

Used from specification persistence-io-asm

• persistence-io-asm/avol-down-size-ls is used by avol-down-size-ls,

Used from specification eraseblock

• eraseblock/empbuf-eq-emptypage is used by prepost-read-log,
• eraseblock/emptyleb-size is used by prepost-read-superblock,
• eraseblock/emptypage-at is used by prepost-read-log,
• eraseblock/emptypage-size is used by prepost-read-log,
• eraseblock/isempty-empbuf is used by prepost-read-log,
• eraseblock/lebsize-add-eq-0 is used by prepost-write-lebs, prepost-read-lebs,
• eraseblock/lebsize-neq-zero is used by prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, inv-commit, inv-format,
• eraseblock/lebsize-page-size-is-aligned is used by prepost-write-lebs, prepost-read-log, prepost-encode-orphans,
• eraseblock/page-size-plus-eq-0 is used by prepost-read-log, prepost-add-log-leb,

Used from specification nat-mult

• nat-mult/coef-18 is used by prepost-encode-lpt,
• nat-mult/coef-21 is used by prepost-write-lebs, prepost-read-lebs,
• nat-mult/le-num is used by inv-commit, inv-format,
• nat-mult/ls-01 is used by prepost-encode-orphans,
• nat-mult/ls-02 is used by prepost-read-orphans,
• nat-mult/ls-04 is used by inv-format,
• nat-mult/ls-08 is used by prepost-add-log-leb, inv-commit, inv-format,
• nat-mult/mult-a is used by prepost-write-orphans, prepost-write-lebs, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-add-log-leb, inv-commit, inv-recover, inv-format,
• nat-mult/mult-c is used by prepost-write-orphans, prepost-write-lebs, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-add-log-leb, inv-commit, inv-recover, inv-format,
• nat-mult/numeral-19 is used by inv-commit, inv-format,
• nat-mult/numeral-28 is used by inv-recover,
• nat-mult/numeral-29 is used by inv-format,
• nat-mult/numeral-30 is used by prepost-read-log,
• nat-mult/one is used by prepost-read-log, inv-commit, inv-recover, inv-format,
• nat-mult/rsucc-02 is used by prepost-write-lebs, prepost-read-lebs, prepost-encode-orphans, prepost-decode-orphans,
• nat-mult/two-02 is used by rangeeq-subarray, prepost-read-log, prepost-add-log-leb, inv-commit, inv-recover, inv-format,
• nat-mult/two-one-01 is used by prepost-read-log,
• nat-mult/two-zero-01 is used by prepost-read-log, inv-format,
• nat-mult/zero is used by prepost-write-lebs, prepost-read-lebs, prepost-encode-orphans, prepost-decode-orphans,
• nat-mult/zero-01 is used by prepost-read-orphans, prepost-read-lebs,
• nat-mult/zero-02 is used by prepost-write-lebs, prepost-read-lebs,
• nat-mult/zero-06 is used by prepost-write-orphans, prepost-read-orphans,

Used from specification oelem

• oelem/nat-set/irreflexivity is used by prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-decode-lpt, inv-commit,
• oelem/nat-set/sls is used by prepost-write-lebs, prepost-read-log, prepost-read-lebs, prepost-decode-orphans,
• oelem/nat-set/transitivity is used by prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-add-log-leb, inv-commit,

Used from specification persistence-io-inv

• persistence-io-inv/disk-layout is used by prepost-add-log-leb, inv-recover,
• persistence-io-inv/lebs-range-eq is used by rangeeq-lebs-5, rangeeq-lebs,
• persistence-io-inv/lebs-rec is used by prepost-read-lebs,
• persistence-io-inv/lebs-size-mappedfull is used by inv-recover,
• persistence-io-inv/mapped-full is used by prepost-read-lebs,
• persistence-io-inv/mapped-full-range-eq is used by inv-commit,
• persistence-io-inv/disk-layout-1-unfold is used by inv-commit, inv-format,
• persistence-io-inv/disk-layout-2-unfold is used by inv-commit,
• persistence-io-inv/disk-layout-avol-neq-0 is used by prepost-read-orphans, prepost-add-log-leb, inv-write, inv-read, inv-unmap, inv-remap, inv-recover,
• persistence-io-inv/disk-layout-log-above-main is used by prepost-add-log-leb, inv-write, inv-unmap, inv-remap, inv-recover,
• persistence-io-inv/disk-layout-log-neq-orphans is used by prepost-add-log-leb,
• persistence-io-inv/disk-layout-log-not-0 is used by prepost-add-log-leb,
• persistence-io-inv/disk-layout-lpt-below-main is used by inv-write, inv-unmap, inv-remap, inv-recover,
• persistence-io-inv/disk-layout-main-not-below-lpt is used by inv-write, inv-unmap, inv-remap,
• persistence-io-inv/disk-layout-not1-unfold is used by inv-commit,
• persistence-io-inv/disk-layout-orphans-below-main is used by inv-write, inv-unmap, inv-remap,
• persistence-io-inv/disk-layout-same-size is used by prepost-add-log-leb, inv-write, inv-unmap, inv-remap, inv-add-log-leb, inv-recover,
• persistence-io-inv/disk-layout-size-vol-orphans is used by prepost-read-orphans, inv-recover,
• persistence-io-inv/lebs-base is used by prepost-write-lebs, prepost-read-lebs, inv-recover,
• persistence-io-inv/lebs-crash is used by inv-recover,
• persistence-io-inv/lebs-idexpt-below is used by inv-commit, inv-format,
• persistence-io-inv/lebs-size is used by prepost-write-lebs, prepost-read-lebs,
• persistence-io-inv/lebs-write-above is used by inv-write, inv-unmap, inv-remap,
• persistence-io-inv/lebs-write-below is used by prepost-add-log-leb, inv-commit,
• persistence-io-inv/lebs-write-last is used by prepost-write-lebs,
• persistence-io-inv/mapped-full-aligndown-vol is used by inv-recover,
• persistence-io-inv/mapped-full-idexpt-below is used by inv-commit, inv-format,
• persistence-io-inv/mapped-full-last is used by prepost-write-lebs,
• persistence-io-inv/mapped-full-write-above is used by inv-write, inv-unmap, inv-remap,
• persistence-io-inv/mapped-full-write-below is used by prepost-add-log-leb, inv-commit,
• persistence-io-inv/mapped-full-zero is used by prepost-write-lebs,
• persistence-io-inv/persistence-io-inv is used by prepost-read-orphans, prepost-add-log-leb, inv-write, inv-read, inv-unmap, inv-remap, inv-requires-commit, inv-add-log-leb, inv-get-volume-size, inv-commit, inv-recover, inv-format,
• persistence-io-inv/sb-log is used by prepost-add-log-leb, inv-commit, inv-recover, inv-format,
• persistence-io-inv/sb-lpt is used by prepost-add-log-leb, inv-write, inv-unmap, inv-remap, inv-commit, inv-recover, inv-format,
• persistence-io-inv/sb-orph is used by prepost-add-log-leb, inv-commit, inv-recover, inv-format,

Used from specification encoding-orphans

• encoding-orphans/is-encoded-pad is used by prepost-write-orphans, prepost-read-orphans, prepost-encode-orphans,
• encoding-orphans/is-encoded-rec is used by prepost-decode-orphans,
• encoding-orphans/is-encoded-size is used by prepost-write-orphans, prepost-read-orphans,
• encoding-orphans/is-encoded-split-one is used by prepost-encode-orphans, prepost-decode-orphans,
• encoding-orphans/is-encoded-base is used by prepost-encode-orphans, prepost-decode-orphans, inv-format,
• encoding-orphans/is-encoded-pad-empbuf is used by prepost-write-orphans, inv-format,
• encoding-orphans/is-encoded-pad-unique is used by prepost-write-orphans, prepost-add-log-leb, inv-write, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-recover,
• encoding-orphans/is-encoded-unique is used by prepost-encode-orphans, prepost-decode-orphans,

Used from specification array

• array/buffer/Extension is used by prepost-read-superblock, prepost-read-log,
• array/avolume/Extension is used by rangeeq-subarray-5, rangeeq-subarray, id-circle-subarray-concrete-below, inv-format,
• array/avolume/Put-other is used by idcircle-concrete-write, inv-write, inv-unmap, inv-remap,
• array/avolume/Put-same is used by prepost-write-orphans, prepost-write-lebs, prepost-add-log-leb, inv-commit,
• array/buffer/Size-mkarray is used by prepost-write-superblock, prepost-write-orphans, prepost-write-lebs, prepost-read-superblock, prepost-read-orphans, prepost-read-log, prepost-read-lebs, prepost-encode-orphans, prepost-encode-lpt, prepost-decode-orphans, prepost-add-log-leb, inv-commit, inv-recover, inv-format,
• array/lp-array/Size-mkarray is used by inv-recover,
• array/avolume/Size-mkarray is used by inv-format,
• array/avolume/Size-put is used by rangeeq-write-right-concrete-below, prepost-write-orphans, prepost-write-lebs, prepost-add-log-leb, idcircle-concrete-write, inv-write, inv-unmap, inv-remap, inv-commit, inv-format,
• array/lp-array/Size-put is used by prepost-decode-lpt,
• array/lp-array/cgetput is used by prepost-decode-lpt,
• array/avolume/cgetput is used by prepost-write-superblock, prepost-write-lebs, inv-commit, inv-format,
• array/avolume/cngetput is used by rangeeq-write-right-concrete-below, prepost-add-log-leb, inv-write, inv-unmap, inv-remap,
• array/avolume/cngetput-num is used by inv-commit, inv-format,
• array/avolume/cputput is used by prepost-write-orphans, prepost-write-lebs,
• array/avolume/ngp-06 is used by inv-format,
• array/lp-array/ngp-07 is used by prepost-decode-lpt,

Used from specification ebm-avol-asm

• ebm-avol-asm/inv-change is used by prepost-write-superblock,
• ebm-avol-asm/inv-format is used by inv-format,
• ebm-avol-asm/inv-recover is used by inv-recover,
• ebm-avol-asm/inv-remap is used by prepost-write-orphans, prepost-write-lebs, inv-remap, inv-commit, inv-format,
• ebm-avol-asm/inv-write is used by prepost-write-orphans, prepost-write-lebs, prepost-add-log-leb, inv-write,

Used from specification debug

• debug/debug is used by prepost-add-log-leb, inv-recover, inv-format,

Used from specification encoding-aligned

• encoding-aligned/encoding-superblock/decode-contract is used by prepost-read-superblock,
• encoding-aligned/encoding-superblock/encode-contract is used by prepost-write-superblock,
• encoding-aligned/encoding-superblock/is-encoded-aligned is used by prepost-read-superblock,
• encoding-aligned/encoding-superblock/size-aligned is used by prepost-write-superblock,