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

Used from specification nat-basic

nat-basic/a is used by subarray-avol-write, refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
nat-basic/add-base is used by refine-write, refine-read,
nat-basic/c is used by subarray-avol-write, refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
nat-basic/eq-01 is used by subarray-avol-write, refine-write, refine-unmap, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-commit,
nat-basic/eqs is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, refine-add-log-leb, refine-requires-commit, refine-commit,
nat-basic/f is used by subarray-avol-write, refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
nat-basic/l is used by subarray-avol-write, refine-write, refine-read, refine-unmap, refine-remap,
nat-basic/l-02 is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
nat-basic/l-05 is used by refine-read, recovery,
nat-basic/l-06 is used by refine-write, refine-read, refine-unmap, recovery, refine-remap,
nat-basic/lf is used by refine-read,
nat-basic/lf-01 is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, refine-add-log-leb, refine-requires-commit, refine-commit,
nat-basic/lf-02 is used by subarray-avol-write, refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
nat-basic/ls-02 is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, refine-add-log-leb, refine-requires-commit, refine-commit,
nat-basic/zero is used by refine-write, recovery,

Used from specification encoding-lpt

encoding-lpt/encoding-unique is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, refine-add-log-leb, refine-requires-commit, refine-commit,

Used from specification nat

nat/elim-sub is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
nat/eq-01 is used by refine-write,
nat/eq-02 is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
nat/fle is used by refine-read, refine-add-log-leb,
nat/fle-01 is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-add-log-leb, refine-requires-commit,
nat/ge is used by refine-write, refine-read, refine-get-volume-size,
nat/le-def is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
nat/le-ls-simp is used by refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, refine-add-log-leb, refine-commit,
nat/lels is used by subarray-avol-write, refine-write, refine-unmap, recovery, refine-remap,
nat/lep is used by refine-write, refine-unmap, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-commit,
nat/ler is used by refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-add-log-leb, refine-commit,
nat/let is used by refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-add-log-leb,
nat/ls is used by refine-write, refine-read, refine-unmap, refine-remap,
nat/ls-le-simp is used by subarray-avol-write, refine-write, refine-unmap, refine-remap,
nat/sub-ls is used by refine-read,

Used from specification error-class

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

Used from specification aleb

aleb/aleb-not-mapped is used by refine-write, refine-read,
aleb/disj is used by refine-write, refine-read,
aleb/ex is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
aleb/inj is used by refine-write, refine-read, recovery, refine-add-log-leb, refine-commit,
aleb/sel is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
aleb/test-02 is used by refine-write, refine-read, recovery, refine-add-log-leb, refine-commit,

Used from specification error

error/disj-91 is used by refine-write, refine-read, refine-remap,

Used from specification encoding-elem-alignment

encoding-elem-alignment/encoding-superblock/alignment-not-zero is used by refine-write,

Used from specification align

align/is-aligned-add is used by refine-write,
align/is-aligned-zero is used by refine-write,

Used from specification superblock

superblock/elim is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
superblock/inj is used by recovery, refine-get-volume-size, refine-commit,
superblock/sel-09 is used by refine-add-log-leb, refine-commit,
superblock/sel-10 is used by refine-add-log-leb, refine-commit,
superblock/sel-11 is used by refine-add-log-leb, refine-commit,
superblock/sel-12 is used by refine-add-log-leb, refine-commit,
superblock/sel-13 is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, refine-add-log-leb, refine-requires-commit, refine-commit,

Used from specification ebm-vol-inv

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

Used from specification list

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

Used from specification array-copy

array-copy/avolume/size-subarray is used by subarray-avol-write, refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,
array-copy/avolume/subarray-at is used by subarray-avol-write, refine-write, refine-read, recovery,

Used from specification encoding-log

encoding-log/is-encoded-base is used by initialization, refine-commit,
encoding-log/is-encoded-empty is used by initialization, refine-commit,
encoding-log/is-encoded-unique is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,

Used from specification persistence-io-asm

persistence-io-asm/inv-commit is used by refine-commit,
persistence-io-asm/inv-format is used by initialization,
persistence-io-asm/inv-recover is used by recovery,
persistence-io-asm/prepost-add-log-leb is used by refine-add-log-leb,
persistence-io-asm/prepost-recover-main-same is used by recovery,
persistence-io-asm/avol-down-mapped-eq is used by recovery,
persistence-io-asm/avol-down-size is used by recovery,
persistence-io-asm/avol-down-size-le is used by recovery,

Used from specification oelem

oelem/nat-set/irreflexivity is used by refine-write,
oelem/nat-set/transitivity is used by refine-read,

Used from specification persistence-io-inv

persistence-io-inv/disk-layout-avol-neq-0 is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, refine-add-log-leb, refine-requires-commit, refine-commit,
persistence-io-inv/disk-layout-log-above-main is used by refine-write, refine-unmap, recovery, refine-remap,
persistence-io-inv/disk-layout-lpt-below-main is used by refine-write, refine-unmap, recovery, refine-remap,
persistence-io-inv/disk-layout-orphans-below-main is used by refine-write, refine-unmap, refine-remap,
persistence-io-inv/disk-layout-same-size is used by recovery, refine-add-log-leb, refine-commit,
persistence-io-inv/disk-layout-size-vol-orphans is used by recovery,
persistence-io-inv/lebs-crash is used by recovery,
persistence-io-inv/lebs-write-above is used by refine-write, refine-unmap, refine-remap,
persistence-io-inv/mapped-full-aligndown-vol is used by recovery,
persistence-io-inv/persistence-io-inv is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,

Used from specification encoding-orphans

encoding-orphans/is-encoded-base is used by initialization,
encoding-orphans/is-encoded-pad-empbuf is used by initialization,
encoding-orphans/is-encoded-pad-unique is used by refine-get-page-size, refine-get-leb-size, refine-write, refine-read, refine-unmap, recovery, refine-remap, refine-get-volume-size, initialization, refine-add-log-leb, refine-requires-commit, refine-commit,

Used from specification array

array/avolume/Extension is used by subarray-avol-write,
array/avolume/Put-other is used by refine-write,
array/avolume/Put-other is used by subarray-avol-write, refine-write, refine-unmap, refine-remap,
array/buffer/Size-mkarray is used by initialization,
array/avolume/Size-put is used by subarray-avol-write, refine-write, refine-unmap, refine-remap,
array/avolume/cgetput is used by subarray-avol-write,
array/avolume/cngetput is used by subarray-avol-write, refine-write, refine-unmap, refine-remap,