Used simplifier rules/spec theorems by specification

Used from specification array-splice

• array-splice/buffer/append-at is used by refine-read-buf, refine-write-buf,
• array-splice/buffer/append-at1 is used by at-append-cut,
• array-splice/buffer/array-split-elim-size is used by refine-read-buf,
• array-splice/buffer/array-split1 is used by refine-read-buf,
• array-splice/buffer/copy2append is used by refine-read-buf, refine-write-buf,
• array-splice/buffer/copy2append0 is used by refine-write-buf,
• array-splice/buffer/emparray-at is used by refine-read-buf,
• array-splice/buffer/subarray-append-shift-right is used by refine-read-buf,
• array-splice/buffer/append-a is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• array-splice/buffer/append-at1 is used by refine-read-buf,
• array-splice/buffer/append-at1-simp1 is used by refine-read-buf,
• array-splice/buffer/append-eq-left is used by refine-read-buf, refine-write-buf,
• array-splice/buffer/append-eq-right is used by refine-read-buf,
• array-splice/buffer/append-len is used by refine-destroy-buf, refine-read-buf, refine-add-log-leb, refine-write-buf, refine-move-buf,
• array-splice/buffer/append-prefix-left is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-read-buf, refine-commit, refine-write-buf,
• array-splice/buffer/append-zero-left is used by refine-read-buf, refine-write-buf,
• array-splice/buffer/append-zero-right is used by refine-add-log-leb, refine-write-buf, refine-move-buf,
• array-splice/buffer/copy-append is used by refine-read-buf,
• array-splice/buffer/copy-shift-right is used by refine-read-buf, refine-write-buf,
• array-splice/buffer/emparray-len is used by refine-read-buf,
• array-splice/buffer/mkemparray-eq is used by refine-read-buf,
• array-splice/buffer/mkemparray0-append-left is used by refine-read-buf, refine-write-buf,
• array-splice/buffer/range-eq-0 is used by refine-read-buf,
• array-splice/buffer/range-eq-refl is used by refine-read-buf,
• array-splice/buffer/range-eq-refl-simp is used by refine-read-buf,
• array-splice/buffer/subarray-append-consec0 is used by refine-write-buf,
• array-splice/buffer/subarray-append-elim-left is used by refine-read-buf,
• array-splice/buffer/subarray-append-elim-left0-simp is used by refine-read-buf, refine-write-buf,
• array-splice/buffer/subarray-append-left is used by refine-read-buf, refine-write-buf,
• array-splice/buffer/subarray-append-shift-right-simp-0 is used by refine-read-buf,
• array-splice/buffer/subarray-elim-right is used by refine-read-buf,
• array-splice/buffer/subarray-emparray is used by refine-read-buf,
• array-splice/buffer/subarray-same-ar-eq is used by refine-read-buf, refine-write-buf,

Used from specification nat-basic

• nat-basic/addex is used by refine-read-buf,
• nat-basic/c is used by refine-read-buf,
• nat-basic/a is used by nat1, nat0, mod-to-aligndown-minus, refine-enter-readonly, refine-destroy-buf, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• nat-basic/add-base is used by refine-enter-readonly, refine-read-buf, refine-commit, refine-write-buf,
• nat-basic/c is used by nat1, nat0, mod-to-aligndown-minus, refine-enter-readonly, refine-destroy-buf, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• nat-basic/eq-01 is used by refine-read-buf, refine-write-buf,
• nat-basic/eq-02 is used by refine-read-buf, refine-write-buf,
• nat-basic/eqs is used by refine-read-buf,
• nat-basic/f is used by abs-unbuffered, abs-buffered, refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• nat-basic/l is used by refine-read-buf, refine-write-buf,
• nat-basic/l-01 is used by refine-read-buf, refine-write-buf,
• nat-basic/l-02 is used by refine-read-buf, refine-write-buf,
• nat-basic/l-04 is used by refine-read-buf,
• nat-basic/l-05 is used by refine-read-buf,
• nat-basic/l-06 is used by refine-read-buf,
• nat-basic/l-08 is used by refine-read-buf,
• nat-basic/lf is used by refine-read-buf, refine-write-buf,
• nat-basic/lf-01 is used by abs-unbuffered, abs-buffered, refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• nat-basic/lf-02 is used by refine-enter-readonly, refine-destroy-buf, refine-read-buf, refine-commit, refine-write-buf, refine-move-buf,
• nat-basic/ls-02 is used by refine-read-buf, refine-write-buf,
• nat-basic/one is used by refine-read-buf,
• nat-basic/one-03 is used by refine-read-buf,
• nat-basic/succ is used by refine-read-buf, refine-write-buf,
• nat-basic/z-01 is used by refine-write-buf,
• nat-basic/zero is used by refine-read-buf, refine-write-buf,
• nat-basic/zero-01 is used by refine-read-buf,

Used from specification wbuf-base

• wbuf-base/wbuf-cons is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• wbuf-base/wbuf-cons-mapped is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• wbuf-base/wbuf-cons-nobuf is used by refine-enter-readonly, refine-is-readonly, refine-get-buf, refine-destroy-buf, refine-get-page-size, refine-get-leb-size, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-requires-commit, refine-commit, refine-write-buf, refine-move-buf, refine-get-volume-size,

Used from specification min-max

• min-max/min is used by refine-read-buf,
• min-max/min-comm is used by refine-read-buf,
• min-max/min-le-left is used by refine-read-buf,
• min-max/min-ls-add is used by refine-read-buf,
• min-max/min-ls-right is used by refine-read-buf,
• min-max/min-not-ls-add is used by refine-read-buf,
• min-max/min-notls1 is used by refine-read-buf,
• min-max/min-notls2 is used by refine-read-buf,

Used from specification nat

• nat/anti is used by refine-read-buf,
• nat/cancel-01 is used by refine-read-buf, refine-write-buf,
• nat/elim-sub is used by mod-to-aligndown-minus, refine-read-buf, refine-write-buf,
• nat/eq-01 is used by refine-read-buf, refine-write-buf,
• nat/eq-02 is used by refine-read-buf, refine-write-buf,
• nat/fle is used by recovery, refine-unmap, refine-remap, refine-read-buf, refine-write-buf,
• nat/fle-01 is used by refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-write-buf,
• nat/ge is used by refine-read-buf, refine-write-buf,
• nat/le is used by refine-read-buf, refine-write-buf,
• nat/le-add is used by refine-read-buf, refine-write-buf,
• nat/le-def is used by refine-read-buf, refine-write-buf,
• nat/le-ls-simp is used by refine-read-buf, refine-write-buf,
• nat/lels is used by refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-write-buf, refine-move-buf,
• nat/lels-02 is used by refine-read-buf, refine-write-buf,
• nat/lels-03 is used by recovery, refine-read-buf, refine-write-buf,
• nat/lep is used by refine-read-buf, refine-write-buf,
• nat/lep-02 is used by nat1, nat0, refine-read-buf, refine-write-buf,
• nat/ler is used by refine-read-buf, refine-write-buf,
• nat/let is used by refine-read-buf, refine-write-buf,
• nat/lez is used by refine-read-buf,
• nat/lez-01 is used by refine-write-buf,
• nat/ls is used by refine-read-buf,
• nat/ls-01 is used by refine-read-buf, refine-write-buf,
• nat/ls-03 is used by refine-read-buf, refine-write-buf,
• nat/ls-le-simp is used by refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-write-buf, refine-move-buf,
• nat/prop-07 is used by refine-read-buf,
• nat/sub-add is used by refine-read-buf,
• nat/sub-base is used by refine-read-buf, refine-write-buf,
• nat/sub-ls is used by refine-read-buf,
• nat/zero is used by mod-to-aligndown-minus, refine-read-buf, refine-write-buf,
• nat/zero-02 is used by refine-read-buf, refine-write-buf,

Used from specification wbuf

• wbuf/elim is used by abs-unbuffered, refine-enter-readonly, refine-is-readonly, refine-get-buf, refine-destroy-buf, refine-get-page-size, refine-get-leb-size, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-requires-commit, refine-commit, refine-write-buf, refine-move-buf, refine-get-volume-size,
• wbuf/inj is used by refine-add-log-leb,
• wbuf/sel-01 is used by abs-buffered, refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• wbuf/sel-02 is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• wbuf/sel-03 is used by abs-buffered, refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• wbuf/upd-01 is used by refine-write-buf,
• wbuf/upd-02 is used by refine-add-log-leb, refine-write-buf, refine-move-buf,
• wbuf/upd-03 is used by refine-add-log-leb, refine-write-buf, refine-move-buf,

Used from specification error-class

• error-class/ecommit is used by recovery, initialization, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf,
• error-class/erofs is used by refine-add-log-leb, refine-move-buf,
• error-class/esuccess is used by recovery, initialization, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• error-class/not-esuccess is used by recovery, initialization, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf,

Used from specification error

• error/disj-120 is used by refine-add-log-leb, refine-move-buf,
• error/disj-91 is used by recovery, initialization, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf,

Used from specification aleb

• aleb/aleb-not-mapped is used by recovery, refine-add-log-leb,
• aleb/disj is used by recovery, refine-add-log-leb,
• aleb/ex is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• aleb/inj is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• aleb/sel is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• aleb/test-01 is used by recovery,
• aleb/test-02 is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,

Used from specification buffer

• buffer/subarray-append-mkempbuf-from is used by refine-read-buf,
• buffer/subarray-mkempbuf-leq is used by refine-read-buf,

Used from specification wbuf-asm

• wbuf-asm/aligndown-simp is used by refine-write-buf,

Used from specification align

• align/align-down-add-eq-add-ls is used by refine-write-buf,
• align/aligndown-is-aligned-add is used by refine-write-buf,
• align/aligndown-is-smaller is used by refine-write-buf,
• align/aligndown-is-smaller-01 is used by mod-to-aligndown-minus,
• align/aligndown-is-zero is used by refine-write-buf,
• align/aligndown-remainder is used by mod-to-aligndown-minus,
• align/aligndown-same is used by mod-to-aligndown-minus, refine-write-buf,
• align/is-aligned-add is used by refine-destroy-buf, refine-read-buf, refine-add-log-leb, refine-write-buf, refine-move-buf,
• align/is-aligned-align-down is used by refine-write-buf,
• align/is-aligned-ls-eq-zero is used by refine-destroy-buf, refine-add-log-leb, refine-write-buf, refine-move-buf,
• align/is-aligned-zero is used by refine-write-buf,

Used from specification ebm-vol-inv

• ebm-vol-inv/ebm-vol-inv is used by recovery, refine-read-buf,
• ebm-vol-inv/ebm-vol-le is used by recovery,
• ebm-vol-inv/ebm-vol-inv-lebsize is used by refine-read-buf,

Used from specification list

• list/nat-list-set/Last is used by refine-add-log-leb,

Used from specification array-copy

• array-copy/buffer/at-subarray is used by refine-read-buf,
• array-copy/buffer/subarray-subarray-elim is used by refine-read-buf,
• array-copy/buffer/subarray-subarray-elim-0 is used by refine-read-buf,
• array-copy/buffer/at-copy is used by refine-read-buf,
• array-copy/buffer/size-copy is used by refine-read-buf, refine-write-buf,
• array-copy/buffer/size-subarray is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• array-copy/buffer/subarray-at is used by refine-read-buf, refine-write-buf,
• array-copy/buffer/subarray-copy-elim-exact is used by refine-write-buf,
• array-copy/buffer/subarray-copy-higher is used by refine-write-buf,
• array-copy/buffer/subarray-copy-lower is used by refine-write-buf,
• array-copy/buffer/subarray-elim is used by recovery, refine-read-buf, refine-write-buf,
• array-copy/buffer/subarray-zero is used by refine-enter-readonly, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,

Used from specification wbuf-abs

• wbuf-abs/abs-def is used by abs-unbuffered, abs-buffered, refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• wbuf-abs/abs-buf-leb-def is used by abs-buffered, refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• wbuf-abs/abs-buf-leb-unmapped is used by recovery,
• wbuf-abs/abs-mapped-is-mapped is used by refine-read-buf, refine-add-log-leb, refine-move-buf,
• wbuf-abs/abs-mapped-is-mapped-rev is used by refine-read-buf, refine-add-log-leb, refine-write-buf, refine-move-buf,
• wbuf-abs/abs-nobuffer is used by refine-enter-readonly, refine-destroy-buf, recovery, initialization, refine-unmap, refine-remap, refine-read-buf, refine-commit, refine-move-buf,
• wbuf-abs/abs-size1 is used by refine-add-log-leb,
• wbuf-abs/abs-size2 is used by refine-unmap, refine-remap, refine-write-buf,

Used from specification bufleb

• bufleb/disj is used by refine-enter-readonly, refine-destroy-buf, recovery, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• bufleb/elim is used by refine-enter-readonly, refine-destroy-buf, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• bufleb/elim-is-buf-ant is used by refine-move-buf,
• bufleb/elim-is-buf-suc is used by refine-move-buf,
• bufleb/inj is used by abs-buffered, refine-enter-readonly, refine-destroy-buf, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• bufleb/sel is used by recovery, refine-read-buf, refine-add-log-leb, refine-write-buf, refine-move-buf,
• bufleb/test-02 is used by refine-write-buf,

Used from specification eraseblock

• eraseblock/lebsize-neq-zero is used by recovery, refine-read-buf,
• eraseblock/page-size is used by refine-destroy-buf, recovery, refine-read-buf, refine-add-log-leb, refine-write-buf, refine-move-buf,
• eraseblock/page-size-plus-eq-0 is used by refine-read-buf,

Used from specification oelem

• oelem/nat-set/irreflexivity is used by refine-unmap, refine-remap, refine-read-buf, refine-write-buf,
• oelem/nat-set/ls-le is used by refine-write-buf,
• oelem/nat-set/sls is used by refine-read-buf, refine-write-buf,
• oelem/nat-set/transitivity is used by refine-read-buf, refine-write-buf,

Used from specification awbuf-inv

• awbuf-inv/awbuf-inv-def is used by recovery,
• awbuf-inv/down-arrow-block-def is used by recovery,
• awbuf-inv/down-arrow-def is used by recovery,
• awbuf-inv/synced is used by refine-destroy-buf, refine-add-log-leb,
• awbuf-inv/align-down-append-eq is used by recovery,
• awbuf-inv/align-down-eq is used by recovery,
• awbuf-inv/align-down-is-aligned is used by recovery,
• awbuf-inv/inv-buf-in-vol is used by refine-enter-readonly, refine-destroy-buf, refine-unmap, refine-remap, refine-read-buf, refine-add-log-leb, refine-commit, refine-write-buf, refine-move-buf,
• awbuf-inv/inv-leb-size is used by refine-read-buf,

Used from specification array

• array/avolume/Extension is used by refine-destroy-buf,
• array/buffer/Extension is used by refine-read-buf, refine-write-buf,
• array/avolume/Put-other is used by refine-unmap, refine-remap, refine-write-buf,
• array/avolume/Put-same is used by refine-unmap, refine-remap, refine-write-buf,
• array/buffer/Size-mkarray is used by refine-write-buf,
• array/avolume/Size-put is used by refine-unmap, refine-remap, refine-write-buf,
• array/avolume/cgetput is used by refine-unmap, refine-remap, refine-write-buf,

Used from specification nat-div

• nat-div/mod-eq is used by refine-write-buf,
• nat-div/mod-le is used by refine-write-buf,
• nat-div/mod-le-02 is used by refine-write-buf,