[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Used simplifier rules/spec theorems by specification

Used from specification array-splice

array-splice/buffer/append-a is used by inv-write-buf, inv-read-buf, synced-write-buf,
array-splice/buffer/append-eq-left is used by synced-write-buf,
array-splice/buffer/append-len is used by inv-write-buf, inv-read-buf, synced-write-buf,
array-splice/buffer/emparray-len is used by inv-read-buf,
array-splice/buffer/range-eq-refl is used by crash-neutral-read-buf, inv-read-buf,
array-splice/buffer/subarray-append-shift-right-simp-0 is used by synced-write-buf,
array-splice/buffer/subarray-same-ar-eq is used by synced-write-buf,

Used from specification nat-basic

nat-basic/a is used by crash-neutral-read-buf, inv-write-buf, inv-read-buf, synced-write-buf,
nat-basic/add-base is used by inv-write-buf, inv-read-buf, synced-write-buf,
nat-basic/c is used by crash-neutral-read-buf, inv-write-buf, inv-read-buf, synced-write-buf,
nat-basic/eq-01 is used by synced-write-buf,
nat-basic/f is used by fwd-buffered-mapped, inv-destroy-buf, inv-move-buf, crash-neutral-move-buf, inv-add-log-leb, crash-neutral-add-log-leb, crash-neutral-write-buf, crash-neutral-read-buf, crash-neutral-remap, crash-neutral-unmap, inv-write-buf, inv-read-buf, inv-remap, inv-unmap, synced-unmap, synced-remap, synced-add-log-leb, synced-write-buf,
nat-basic/l is used by inv-write-buf, synced-write-buf,
nat-basic/l-01 is used by inv-write-buf,
nat-basic/lf-01 is used by inv-destroy-buf, inv-move-buf, crash-neutral-move-buf, inv-add-log-leb, crash-neutral-add-log-leb, crash-neutral-write-buf, crash-neutral-read-buf, crash-neutral-remap, crash-neutral-unmap, inv-write-buf, inv-read-buf, inv-remap, inv-unmap, synced-unmap, synced-remap, synced-add-log-leb, synced-write-buf,
nat-basic/lf-02 is used by inv-move-buf, inv-read-buf,
nat-basic/ls-02 is used by inv-write-buf, inv-read-buf,

Used from specification nat

nat/le-addex is used by synced-write-buf,
nat/elim-sub is used by crash-neutral-read-buf, inv-read-buf,
nat/fle is used by inv-move-buf, crash-neutral-move-buf, inv-write-buf, inv-read-buf, synced-write-buf,
nat/fle-01 is used by inv-write-buf, synced-write-buf,
nat/ge is used by crash-neutral-read-buf, inv-read-buf,
nat/le-def is used by inv-destroy-buf, inv-move-buf, inv-add-log-leb, crash-neutral-unmap, inv-write-buf, inv-read-buf, synced-write-buf,
nat/le-ls-simp is used by inv-move-buf, crash-neutral-move-buf, crash-neutral-write-buf, inv-write-buf, inv-read-buf,
nat/lels is used by inv-move-buf, crash-neutral-move-buf, crash-neutral-write-buf, inv-write-buf, inv-remap, synced-unmap, synced-remap, synced-write-buf,
nat/lels-02 is used by synced-write-buf,
nat/lels-03 is used by inv-write-buf, synced-write-buf,
nat/lep is used by crash-neutral-read-buf, inv-read-buf,
nat/lep-02 is used by crash-neutral-read-buf,
nat/ler is used by crash-neutral-read-buf,
nat/lez is used by inv-remap,
nat/ls-le-simp is used by inv-remap, synced-unmap, synced-remap, synced-write-buf,
nat/sub-ls is used by inv-read-buf,

Used from specification error-class

error-class/ecommit is used by inv-move-buf, inv-commit, inv-add-log-leb, inv-recover, inv-write-buf, inv-read-buf, inv-remap, inv-format,
error-class/eio is used by crash-neutral-recover, crash-neutral-commit, crash-neutral-add-log-leb, crash-neutral-write-buf, crash-neutral-read-buf, crash-neutral-remap, synced-write-buf,
error-class/esuccess is used by inv-move-buf, crash-neutral-move-buf, inv-add-log-leb, inv-recover, inv-write-buf, inv-read-buf, inv-remap, synced-remap, synced-add-log-leb, synced-commit, synced-write-buf, inv-format,
error-class/not-esuccess is used by inv-write-buf, inv-read-buf, inv-remap, synced-remap, synced-write-buf,

Used from specification aleb

aleb/aleb-not-mapped is used by fwd-buffered-mapped, inv-move-buf, crash-neutral-move-buf, crash-neutral-add-log-leb, crash-neutral-write-buf, inv-write-buf, synced-add-log-leb, synced-write-buf,
aleb/disj is used by fwd-buffered-mapped, inv-move-buf, crash-neutral-move-buf, crash-neutral-add-log-leb, crash-neutral-write-buf, inv-write-buf, synced-add-log-leb, synced-write-buf,
aleb/ex is used by fwd-buffered-mapped, inv-destroy-buf, inv-move-buf, crash-neutral-move-buf, inv-add-log-leb, crash-neutral-add-log-leb, crash-neutral-write-buf, crash-neutral-read-buf, crash-neutral-unmap, inv-write-buf, inv-read-buf, synced-read-buf, synced-add-log-leb, synced-write-buf,
aleb/inj is used by inv-move-buf, crash-neutral-add-log-leb, crash-neutral-write-buf, crash-neutral-unmap, inv-write-buf, synced-add-log-leb, synced-write-buf,
aleb/sel is used by inv-destroy-buf, inv-move-buf, inv-add-log-leb, crash-neutral-write-buf, crash-neutral-unmap, inv-write-buf, inv-read-buf, synced-write-buf,
aleb/test-01 is used by crash-neutral-unmap, inv-format,
aleb/test-02 is used by inv-move-buf, inv-add-log-leb, crash-neutral-add-log-leb, crash-neutral-read-buf, crash-neutral-unmap, inv-write-buf, inv-read-buf, synced-add-log-leb, synced-write-buf,

Used from specification error

error/disj-66 is used by crash-neutral-recover, crash-neutral-commit, crash-neutral-add-log-leb, crash-neutral-write-buf, crash-neutral-read-buf, crash-neutral-remap, synced-write-buf,
error/disj-91 is used by inv-move-buf, inv-commit, inv-add-log-leb, inv-recover, inv-write-buf, inv-read-buf, inv-remap, inv-format,

Used from specification align

align/align-down-add-ls is used by synced-write-buf,
align/align-down-add-eq is used by synced-write-buf,
align/align-down-add-eq-add-ls is used by synced-write-buf,
align/aligndown-eq-add is used by synced-write-buf,
align/aligndown-is-smaller is used by crash-neutral-unmap,
align/aligndown-same is used by crash-neutral-unmap, synced-write-buf,
align/aligndown-same0 is used by crash-neutral-unmap,
align/is-aligned-add is used by synced-write-buf,
align/is-aligned-align-down is used by synced-write-buf,
align/is-aligned-mod is used by synced-write-buf,
align/is-aligned-zero is used by inv-remap,

Used from specification list

list/nat-list-set/Last is used by inv-add-log-leb, crash-neutral-add-log-leb, synced-add-log-leb,
list/nat-list-set/a is used by synced-add-log-leb,
list/nat-list-set/app-04 is used by synced-add-log-leb,
list/nat-list-set/e is used by synced-add-log-leb,
list/nat-list-set/in-15 is used by synced-add-log-leb,
list/nat-list-set/in-17 is used by synced-add-log-leb,
list/nat-list-set/in-append is used by synced-add-log-leb,

Used from specification array-copy

array-copy/buffer/subarray-subarray-elim is used by synced-write-buf,
array-copy/avolume/at-fill-mkarray is used by inv-format,
array-copy/avolume/size-fill is used by inv-format,
array-copy/buffer/size-subarray is used by crash-neutral-unmap, inv-write-buf, synced-write-buf,
array-copy/buffer/subarray-elim is used by crash-neutral-unmap, synced-write-buf,

Used from specification bufleb

bufleb/disj is used by fwd-buffered-mapped, inv-destroy-buf, inv-move-buf, crash-neutral-move-buf, inv-add-log-leb, crash-neutral-write-buf, inv-write-buf, synced-write-buf,
bufleb/elim is used by synced-write-buf,
bufleb/elim-is-buf-ant is used by inv-move-buf, crash-neutral-move-buf, crash-neutral-write-buf, inv-write-buf,
bufleb/elim-is-buf-suc is used by inv-move-buf, crash-neutral-move-buf, crash-neutral-write-buf, inv-write-buf,
bufleb/inj is used by fwd-buffered-mapped, inv-move-buf, crash-neutral-move-buf, inv-add-log-leb,
bufleb/sel is used by fwd-buffered-mapped, inv-move-buf, crash-neutral-move-buf, inv-add-log-leb, crash-neutral-write-buf, inv-write-buf, synced-write-buf,
bufleb/test-02 is used by crash-neutral-write-buf, inv-write-buf, synced-write-buf,

Used from specification eraseblock

eraseblock/page-size is used by crash-neutral-unmap, inv-remap, synced-write-buf,

Used from specification oelem

oelem/nat-set/irreflexivity is used by inv-write-buf, synced-write-buf,

Used from specification awbuf-inv

awbuf-inv/align-down-is-aligned is used by synced-write-buf,
awbuf-inv/awbuf-inv-def is used by fwd-buffered-mapped, inv-destroy-buf, inv-move-buf, inv-add-log-leb, inv-format,
awbuf-inv/down-arrow-block-def is used by crash-neutral-unmap,
awbuf-inv/down-arrow-buf is used by crash-neutral-unmap, synced-write-buf,
awbuf-inv/down-arrow-def is used by crash-neutral-unmap,
awbuf-inv/align-down-app-same is used by synced-write-buf,
awbuf-inv/align-down-mkbuf0 is used by synced-remap,
awbuf-inv/align-down-size-is-aligned is used by crash-neutral-unmap,
awbuf-inv/awbuf-inv-crash is used by inv-recover,
awbuf-inv/down-appended-less is used by synced-write-buf,
awbuf-inv/down-arrow-size is used by crash-neutral-unmap,
awbuf-inv/down-arrow-size0 is used by inv-recover,
awbuf-inv/down-two-writtes is used by synced-write-buf,
awbuf-inv/down-written-eq is used by synced-remap, synced-write-buf,
awbuf-inv/down-written-not-down-before is used by synced-unmap, synced-remap, synced-write-buf,
awbuf-inv/inv-buf-in-vol is used by fwd-buffered-mapped, inv-move-buf, crash-neutral-move-buf, crash-neutral-write-buf, inv-write-buf, synced-write-buf,
awbuf-inv/inv-leb-size is used by inv-destroy-buf, inv-move-buf, inv-add-log-leb, crash-neutral-unmap, inv-read-buf,
awbuf-inv/inv-nobuf-synced is used by inv-recover, inv-format,
awbuf-inv/inv-synced-write-buf is used by synced-write-buf,
awbuf-inv/inv-unmap is used by inv-remap, inv-unmap,
awbuf-inv/inv-write-buf is used by inv-write-buf,
awbuf-inv/inv-write-unbuf is used by inv-remap,
awbuf-inv/mapped-down-mapped is used by synced-write-buf,
awbuf-inv/synced-aligned is used by inv-destroy-buf, inv-add-log-leb, crash-neutral-unmap,
awbuf-inv/synced-down-synced is used by crash-neutral-destroy-buf, crash-neutral-commit, crash-neutral-add-log-leb,
awbuf-inv/synced-map is used by synced-remap,
awbuf-inv/synced-unmap is used by synced-unmap, synced-remap,

Used from specification array

array/avolume/Put-other is used by crash-neutral-unmap,
array/avolume/Put-same is used by crash-neutral-unmap,
array/avolume/Size-mkarray is used by inv-format,
array/buffer/Size-mkarray is used by inv-remap,
array/avolume/Size-put is used by crash-neutral-unmap, inv-write-buf, inv-remap, inv-unmap,
array/avolume/cngetput is used by crash-neutral-unmap,