Used simplifier rules/spec theorems by specification

Used from specification nat-basic

• nat-basic/a is used by down-appended-less, align-down-elim, align-down-append-eq, align-down-app-same,
• nat-basic/add-base is used by down-appended-less, align-down-elim, align-down-append-eq, align-down-app-same,
• nat-basic/c is used by down-appended-less, align-down-elim, align-down-append-eq, align-down-app-same,
• nat-basic/f is used by synced-write, synced-unmap, synced-map, synced-down-synced, synced-buffered-aligned, synced-aligned, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-unmap, inv-synced-write-buf, inv-nobuf-synced, inv-leb-size, inv-is-aligned-notbuffer, inv-aligned-synced, down-written-not-down-before, down-written-eq, down-two-writtes, down-appended-less, awbuf-inv-crash, align-down-app-same,
• nat-basic/l is used by align-down-app-same,
• nat-basic/l-01 is used by align-down-app-same,
• nat-basic/lf is used by align-down-app-same,
• nat-basic/lf-01 is used by synced-down-synced, down-written-not-down-before, down-written-eq, down-two-writtes, down-appended-less, awbuf-inv-crash, align-down-app-same,
• nat-basic/lf-02 is used by inv-aligned-synced, align-down-app-same,
• nat-basic/ls-02 is used by align-down-app-same,
• nat-basic/ref is used by awbuf-inv-crash, align-down-elim,
• nat-basic/trans is used by align-down-app-same,
• nat-basic/zero is used by align-down-app-same,

Used from specification array-splice

• array-splice/buffer/subarray-append-consec0 is used by align-down-elim,
• array-splice/buffer/append-a is used by down-appended-less, align-down-elim, align-down-append-eq, align-down-app-same,
• array-splice/buffer/append-at1 is used by align-down-app-same,
• array-splice/buffer/append-at2 is used by align-down-app-same,
• array-splice/buffer/append-len is used by down-appended-less, align-down-elim, align-down-append-eq, align-down-app-same,
• array-splice/buffer/subarray-append-left is used by down-appended-less, align-down-elim, align-down-append-eq,
• array-splice/buffer/subarray-same-ar-eq is used by align-down-idempot,

Used from specification nat

• nat/elim-sub is used by align-down-elim,
• nat/fle is used by align-down-app-same,
• nat/fle-01 is used by inv-write-buf, awbuf-inv-crash, align-down-app-same,
• nat/ge is used by synced-write,
• nat/le-def is used by synced-write, inv-write-buf, awbuf-inv-crash, align-down-elim,
• nat/le-ls-simp is used by awbuf-inv-crash, align-down-app-same,
• nat/lels is used by align-down-elim, align-down-app-same,
• nat/ler is used by align-down-elim,
• nat/ls-01 is used by align-down-elim,
• nat/ls-le-simp is used by synced-write, inv-write-buf, inv-leb-size, awbuf-inv-crash,

Used from specification aleb

• aleb/aleb-not-mapped is used by inv-write-unbuf, inv-unmap,
• aleb/disj is used by synced-unmap, inv-write-unbuf, inv-unmap,
• aleb/ex is used by synced-write, synced-unmap, synced-map, synced-down-synced, synced-buffered-aligned, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-unmap, inv-synced-write-buf, inv-nobuf-synced, inv-is-aligned-notbuffer, inv-aligned-synced, awbuf-inv-crash,
• aleb/inj is used by synced-write, synced-map, synced-down-synced, mapped-down-mapped, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-synced-write-buf, inv-aligned-synced, down-appended-less, awbuf-inv-crash,
• aleb/sel is used by synced-write, synced-unmap, synced-map, synced-down-synced, synced-buffered-aligned, synced-aligned, mapped-down-mapped, is-aligned-down, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-synced-write-buf, inv-nobuf-synced, inv-leb-size, inv-is-aligned-notbuffer, inv-aligned-synced, down-written-eq, down-appended-less, awbuf-inv-crash,
• aleb/test-01 is used by synced-unmap, inv-unmap,
• aleb/test-02 is used by synced-write, synced-unmap, synced-map, synced-down-synced, synced-buffered-aligned, synced-aligned, mapped-down-mapped, is-aligned-down, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-synced-write-buf, inv-nobuf-synced, inv-leb-size, inv-is-aligned-notbuffer, inv-aligned-synced, down-written-eq, down-appended-less, awbuf-inv-crash,

Used from specification align

• align/aligndown-def is used by align-down-app-same,
• align/align-down-add-eq is used by align-down-append-eq,
• align/align-down-ls-zero is used by down-appended-less, align-down-elim, align-down-append-eq,
• align/aligndown-add-n is used by align-down-elim,
• align/aligndown-add-same is used by align-down-app-same,
• align/aligndown-is-aligned is used by awbuf-inv-crash, align-down-size-is-aligned, align-down-idempot, align-down-elim,
• align/aligndown-is-aligned-add is used by down-appended-less, align-down-elim, align-down-append-eq,
• align/aligndown-is-aligned0 is used by synced-down-synced, is-aligned-down, align-down-size-eq, align-down-is-aligned, align-down-eq,
• align/aligndown-is-smaller is used by awbuf-inv-crash, align-down-app-same,
• align/aligndown-is-smaller-01 is used by align-down-elim,
• align/aligndown-is-zero is used by align-down-app-same,
• align/aligndown-plus-remainder is used by align-down-elim,
• align/aligndown-remainder is used by align-down-elim,
• align/aligndown-same is used by down-appended-less, awbuf-inv-crash, align-down-app-same,
• align/aligndown-same-equiv is used by align-down-size-eq, align-down-eq,
• align/aligndown-same0 is used by align-down-mkbuf0, align-down-idempot,
• align/is-aligned-mod is used by down-appended-less,
• align/is-aligned-zero is used by synced-map, align-down-mkbuf0,

Used from specification array-copy

• array-copy/buffer/subarray-at is used by align-down-app-same,
• array-copy/buffer/size-subarray is used by awbuf-inv-crash, align-down-size-is-aligned, align-down-size-eq, align-down-idempot, align-down-eq, align-down-elim, align-down-append-eq, align-down-app-same,
• array-copy/buffer/subarray-elim is used by synced-down-synced, is-aligned-down, down-appended-less, awbuf-inv-crash, align-down-size-eq, align-down-mkbuf0, align-down-is-aligned, align-down-idempot, align-down-eq, align-down-elim,

Used from specification bufleb

• bufleb/disj is used by synced-buffered-aligned, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-unmap, inv-synced-write-buf, inv-nobuf-synced, inv-is-aligned-notbuffer, inv-buf-in-vol, inv-aligned-synced, awbuf-inv-crash,
• bufleb/elim is used by inv-write-unbuf, inv-unmap,
• bufleb/inj is used by synced-buffered-aligned, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-unmap, inv-synced-write-buf, inv-is-aligned-notbuffer, inv-buf-in-vol, inv-aligned-synced,
• bufleb/sel is used by synced-buffered-aligned, inv-write-buf-destroy, inv-write-buf, inv-unmap, inv-synced-write-buf, inv-is-aligned-notbuffer, inv-buf-in-vol, inv-aligned-synced,

Used from specification eraseblock

• eraseblock/page-size is used by synced-map, synced-down-synced, is-aligned-down, down-appended-less, awbuf-inv-crash, align-down-size-is-aligned, align-down-size-eq, align-down-mkbuf0, align-down-is-aligned, align-down-idempot, align-down-eq, align-down-elim, align-down-append-eq, align-down-app-same,

Used from specification nat-mult

• nat-mult/ls is used by align-down-app-same,
• nat-mult/modeq is used by align-down-app-same,
• nat-mult/mult-a is used by align-down-app-same,
• nat-mult/mult-c is used by align-down-app-same,
• nat-mult/zero-01 is used by align-down-app-same,
• nat-mult/zero-06 is used by align-down-app-same,

Used from specification array

• array/buffer/Extension is used by align-down-eq, align-down-append-eq, align-down-app-same,
• array/avolume/Put-other is used by inv-synced-write-buf, down-written-not-down-before, down-appended-less,
• array/avolume/Put-other is used by synced-write, synced-unmap, synced-map, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-unmap, down-two-writtes,
• array/avolume/Put-same is used by synced-write, synced-unmap, synced-map, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-unmap, inv-synced-write-buf, down-written-not-down-before, down-written-eq, down-two-writtes, down-appended-less,
• array/buffer/Size-mkarray is used by synced-map, align-down-mkbuf0,
• array/avolume/Size-put is used by synced-write, synced-unmap, synced-map, inv-write-unbuf, inv-write-buf-destroy, inv-write-buf, inv-unmap, inv-synced-write-buf, down-written-not-down-before, down-written-eq, down-two-writtes, down-appended-less,
• array/avolume/cngetput is used by synced-unmap, inv-write-unbuf, inv-unmap,

Used from specification nat-div

• nat-div/div-elim is used by align-down-app-same,