[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-read-buf, inv-write-buf,
array-splice/buffer/append-len is used by inv-read-buf, inv-write-buf,
array-splice/buffer/emparray-len is used by inv-read-buf, inv-write-buf,
array-splice/buffer/range-eq-0 is used by inv-read-buf,
array-splice/buffer/range-eq-refl is used by inv-read-buf,

Used from specification nat-basic

nat-basic/a is used by aligndown-simp, inv-read-buf, inv-write-buf,
nat-basic/add-base is used by aligndown-simp, inv-read-buf, inv-write-buf,
nat-basic/c is used by aligndown-simp, inv-read-buf, inv-write-buf,
nat-basic/eq-01 is used by inv-write-buf,
nat-basic/f is used by aligndown-simp, inv-enter-readonly, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,
nat-basic/l is used by inv-read-buf, inv-write-buf,
nat-basic/l-01 is used by aligndown-simp, inv-read-buf, inv-write-buf,
nat-basic/l-02 is used by inv-write-buf,
nat-basic/lf is used by aligndown-simp, inv-read-buf, inv-write-buf,
nat-basic/lf-01 is used by inv-enter-readonly, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,
nat-basic/lf-02 is used by aligndown-simp, inv-enter-readonly, inv-commit, inv-read-buf, inv-write-buf,
nat-basic/ls-02 is used by inv-enter-readonly, inv-commit, inv-read-buf,
nat-basic/one is used by aligndown-simp,
nat-basic/one-03 is used by aligndown-simp,
nat-basic/succ is used by aligndown-simp, inv-read-buf, inv-write-buf,
nat-basic/z-01 is used by aligndown-simp,
nat-basic/zero is used by aligndown-simp, inv-add-log-leb, inv-write-buf, inv-move-buf,
nat-basic/zero-01 is used by inv-read-buf,

Used from specification wbuf-base

wbuf-base/wbuf-cons is used by inv-enter-readonly, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,
wbuf-base/wbuf-cons-mapped is used by inv-enter-readonly, inv-unmap, inv-remap, inv-commit, inv-read-buf, inv-write-buf,
wbuf-base/wbuf-cons-nbytes-le-pagesize is used by inv-enter-readonly, inv-write-buf,
wbuf-base/wbuf-cons-nbytes-ls-pagesize is used by inv-write-buf,
wbuf-base/wbuf-cons-nobuf is used by inv-enter-readonly, inv-is-readonly, inv-destroy-buf, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf, inv-get-volume-size, inv-recover, inv-get-buf, inv-format,

Used from specification min-max

min-max/min-notls1 is used by inv-read-buf,
min-max/min-notls2 is used by inv-read-buf,

Used from specification wbuf

wbuf/elim is used by inv-enter-readonly, inv-is-readonly, inv-destroy-buf, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf, inv-get-volume-size, inv-recover, inv-get-buf,
wbuf/sel-01 is used by inv-enter-readonly, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,
wbuf/sel-02 is used by inv-enter-readonly, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,
wbuf/sel-03 is used by inv-enter-readonly, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,
wbuf/upd-01 is used by inv-write-buf,
wbuf/upd-02 is used by inv-add-log-leb, inv-write-buf, inv-move-buf,
wbuf/upd-03 is used by inv-add-log-leb, inv-write-buf, inv-move-buf,
wbuf/updsel-14 is used by inv-recover, inv-format,

Used from specification nat

nat/anti is used by inv-read-buf, inv-write-buf,
nat/elim-sub is used by inv-read-buf, inv-write-buf,
nat/fle is used by aligndown-simp, inv-read-buf, inv-write-buf,
nat/fle-01 is used by inv-read-buf, inv-write-buf,
nat/ge is used by inv-read-buf, inv-write-buf,
nat/le is used by inv-read-buf, inv-write-buf,
nat/le-def is used by inv-enter-readonly, inv-commit, inv-read-buf, inv-write-buf,
nat/le-ls-simp is used by aligndown-simp, inv-read-buf, inv-write-buf,
nat/lels is used by inv-enter-readonly, inv-unmap, inv-remap, inv-write-buf,
nat/lels-02 is used by inv-read-buf, inv-write-buf,
nat/lels-03 is used by inv-read-buf, inv-write-buf,
nat/lep is used by inv-read-buf, inv-write-buf,
nat/lep-02 is used by inv-write-buf,
nat/ler is used by inv-write-buf,
nat/let is used by inv-read-buf, inv-write-buf,
nat/lez is used by inv-read-buf,
nat/ls is used by inv-read-buf,
nat/ls-03 is used by inv-read-buf, inv-write-buf,
nat/ls-le-simp is used by inv-enter-readonly, inv-unmap, inv-remap, inv-commit, inv-read-buf,
nat/sub-add is used by inv-read-buf,
nat/sub-ls is used by inv-read-buf,
nat/zero-02 is used by inv-read-buf,

Used from specification error-class

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

Used from specification error

error/disj-91 is used by inv-add-log-leb, inv-commit, inv-read-buf, inv-recover,

Used from specification aleb

aleb/ex is used by inv-enter-readonly, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,
aleb/inj is used by inv-read-buf, inv-write-buf,
aleb/sel is used by inv-enter-readonly, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,
aleb/test-01 is used by inv-unmap,
aleb/test-02 is used by inv-enter-readonly, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,

Used from specification align

align/aligndown-def is used by aligndown-simp,
align/aligndown-is-aligned is used by inv-write-buf,
align/aligndown-is-smaller is used by inv-write-buf,
align/aligndown-is-zero is used by inv-write-buf,
align/aligndown-plus-remainder is used by inv-write-buf,
align/aligndown-same is used by inv-write-buf,
align/is-aligned-add is used by inv-write-buf,
align/is-aligned-zero is used by inv-write-buf,

Used from specification ebm-vol-inv

ebm-vol-inv/ebm-vol-inv is used by inv-add-log-leb, inv-move-buf,
ebm-vol-inv/ebm-vol-inv-lebsize is used by inv-read-buf,
ebm-vol-inv/ebm-vol-inv-write is used by inv-unmap,
ebm-vol-inv/le-inv is used by inv-recover,
ebm-vol-inv/le-size-2 is used by inv-recover,

Used from specification array-copy

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

Used from specification bufleb

bufleb/disj is used by inv-enter-readonly, inv-unmap, inv-remap, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,
bufleb/elim is used by inv-enter-readonly, inv-unmap, inv-remap, inv-commit, inv-write-buf,
bufleb/inj is used by inv-unmap, inv-remap,
bufleb/sel is used by inv-add-log-leb, inv-read-buf, inv-write-buf, inv-move-buf,
bufleb/test-02 is used by inv-write-buf,

Used from specification nat-mult

nat-mult/ls-01 is used by aligndown-simp,
nat-mult/ls-08 is used by aligndown-simp,
nat-mult/mult-a is used by aligndown-simp,
nat-mult/mult-c is used by aligndown-simp,
nat-mult/zero is used by aligndown-simp,

Used from specification eraseblock

eraseblock/page-size is used by aligndown-simp, inv-enter-readonly, inv-add-log-leb, inv-commit, inv-read-buf, inv-write-buf, inv-move-buf,

Used from specification oelem

oelem/nat-set/irreflexivity is used by inv-write-buf,
oelem/nat-set/sls is used by inv-read-buf,
oelem/nat-set/transitivity is used by aligndown-simp, inv-read-buf, inv-write-buf,

Used from specification array

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

Used from specification nat-div

nat-div/div-elim is used by aligndown-simp,
nat-div/mod-eq is used by aligndown-simp,
nat-div/mod-le is used by inv-write-buf,
nat-div/mod-le-02 is used by inv-write-buf,
nat-div/mod-le-03 is used by inv-write-buf,
nat-div/mod-ls-03 is used by inv-write-buf,

Used from specification apersistence-io-asm

apersistence-io-asm/inv-format is used by inv-format,
apersistence-io-asm/inv-remap is used by inv-remap,
apersistence-io-asm/inv-write is used by inv-write-buf,