[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 nat-basic

Used from specification abstract-file

Used from specification afs-base

Used from specification pcache-entry

Used from specification cache-base

Used from specification key

key/inj-02 is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-readpage,
key/sel-01 is used by refine-lookup,
key/sel-02 is used by refine-lookup,
key/sel-03 is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-create,
key/sel-05 is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
key/test-01 is used by refine-lookup,
key/test-09 is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-create,

Used from specification min-max

Used from specification nat

Used from specification store

store/file-content/At-other is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
store/icache/At-other is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
store/pcache/In-insert is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-readpage,
store/icache/In-insert is used by refine-mkdir,
store/file-content/k-Extension is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-dentry, refine-evict, refine-readpage, refine-link, refine-unlink, refine-create,
store/pcache/At-in-out is used by refine-readpage,
store/icache/At-in-out is used by refine-iget,
store/pcache/At-other is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
store/icache/At-other is used by refine-truncate-buff-some, refine-rename-file-dentry, refine-rename-dir-dentry, refine-write_inode, refine-create,
store/icache/At-same is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-write_inode, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
store/file-content/At-same is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
store/pcache/At-same is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-readpage,
store/icache/Del-at is used by refine-evict,
store/icache/Del-at-strong is used by refine-evict,
store/icache/Del-in is used by refine-evict,
store/file-content/In-empty is used by refine-create,
store/dir-entries/In-empty is used by refine-rename-dir-dentry,
store/file-content/In-insert is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
store/icache/In-insert is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-write_inode, refine-iget, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
store/dir-entries/del-put is used by refine-rename-file-dentry, refine-rename-dir-dentry,
store/dcache/del-put is used by refine-rename-file-dentry, refine-rename-dir-dentry,
store/pcache/in-neq is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
store/file-content/in-neq is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
store/icache/in-neq is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-write_inode, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
store/dir-entries/ins is used by refine-rename-file-dentry, refine-rename-dir-dentry,
store/icache/ins3 is used by refine-rename-dir-dentry,
store/icache/insin is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-dentry, refine-write_inode, refine-link, refine-unlink, refine-create,
store/file-content/insin is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
store/icache/insins is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry,
store/icache/k-At-same is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-iget, refine-link, refine-rmdir, refine-create,
store/dir-entries/notmemlookup is used by refine-lookup,
store/file-content/notmemlookup is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
store/icache/notmemlookup is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-write_inode, refine-iget, refine-evict, refine-readpage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
store/pcache/notmemlookup is used by refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-readpage,

Used from specification error-class

Used from specification error

error/disj-33 is used by refine-lookup,
error/disj-45 is used by refine-write_inode,
error/disj-91 is used by refine-fsyncdir, refine-sync,

Used from specification set-basic

set-basic/alink-set/Size-empty is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-mkdir,
set-basic/icache/ne-01 is used by recovery,
set-basic/alink-set/size-zero is used by refine-rename-file-dentry, recovery, refine-evict, refine-rmdir, refine-unlink,
set-basic/icache/size-zero-01 is used by recovery,
set-basic/alink-set/size-zero-01 is used by recovery, refine-evict, refine-rmdir, refine-unlink,
set-basic/alink-set/size-zero-02 is used by refine-evict, refine-rmdir, refine-unlink,

Used from specification dentry

dentry/disj is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
dentry/elim is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-renam, refine-link, refine-rmdir, refine-unlink, refine-lookup,
dentry/elim-02 is used by refine-rename-file-negdentry, refine-rename-dir-negdentry, refine-renam, refine-link, refine-mkdir, refine-create,
dentry/inj is used by refine-rename-file-dentry, refine-rename-dir-dentry,
dentry/inj-01 is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-rmdir, refine-unlink,
dentry/sel-03 is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-renam, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
dentry/sel-04 is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-renam, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
dentry/sel-05 is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-renam, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
dentry/test-01 is used by refine-rename-file-negdentry, refine-rename-dir-negdentry, refine-renam, refine-link, refine-mkdir, refine-create,
dentry/test-02 is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-renam, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
dentry/test-03 is used by refine-rename-file-dentry, refine-rename-dir-dentry,
dentry/test-04 is used by refine-rename-file-negdentry, refine-rename-dir-negdentry,

Used from specification page

page/page-size is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,

Used from specification buffer-option

Used from specification abstract-dir

Used from specification pcache-del-ops

pcache-del-ops/at-evict-other is used by refine-evict,
pcache-del-ops/at-truncate is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
pcache-del-ops/in-evict-other is used by refine-evict,
pcache-del-ops/in-truncate is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,

Used from specification nat-mult

Used from specification heap

heap/file-heap/at-alloc is used by refine-create,
heap/dir-heap/at-diffs is used by recovery,
heap/file-heap/ext is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, recovery, refine-write_inode, refine-iget, refine-evict, refine-readpage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
heap/dir-heap/ext is used by recovery,
heap/file-heap/at-del is used by refine-evict,
heap/dir-heap/at-write is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
heap/file-heap/at-write is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-write_inode, refine-link, refine-rmdir, refine-unlink, refine-create,
heap/dir-heap/in-alloc is used by refine-mkdir,
heap/file-heap/in-alloc is used by refine-create,
heap/file-heap/in-del is used by refine-evict,
heap/file-heap/in-diffs is used by recovery,
heap/dir-heap/in-diffs is used by recovery,
heap/dir-heap/in-write is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
heap/file-heap/in-write is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-dentry, refine-write_inode, refine-link, refine-unlink, refine-create,
heap/file-heap/nonnull is used by refine-create,
heap/dir-heap/overwrite is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
heap/file-heap/overwrite is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-write_inode, refine-link, refine-rmdir, refine-unlink,
heap/dir-heap/overwrite-split is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-rmdir,
heap/dir-heap/overwrite-split2 is used by refine-rename-dir-dentry,
heap/dir-heap/write-again is used by refine-rename-file-dentry, refine-rename-dir-dentry,

Used from specification icache-entry

Used from specification afs-pre

afs-pre/pre-create is used by refine-create,
afs-pre/pre-evict is used by refine-evict,
afs-pre/pre-iget is used by refine-iget,
afs-pre/pre-link is used by refine-link,
afs-pre/pre-lookup is used by refine-lookup,
afs-pre/pre-mkdir is used by refine-mkdir,
afs-pre/pre-readdir is used by refine-readdir,
afs-pre/pre-readpage is used by refine-readpage,
afs-pre/pre-rename is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-renam,
afs-pre/pre-rmdir is used by refine-rmdir,
afs-pre/pre-truncate is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-truncate,
afs-pre/pre-unlink is used by refine-unlink,
afs-pre/pre-write-inode is used by refine-write_inode,
afs-pre/pre-writepage is used by refine-writepage,
afs-pre/valid-dir-inode is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-write_inode, refine-evict, refine-renam, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
afs-pre/valid-file-inode is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached, refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-fsync, refine-write_inode, refine-iget, refine-truncate, refine-evict, refine-renam, refine-link, refine-unlink,
afs-pre/valid-wb-inode is used by refine-rename-file-negdentry, refine-rename-file-dentry, refine-rename-dir-negdentry, refine-rename-dir-dentry, refine-write_inode, refine-evict, refine-renam,

Used from specification inode

Used from specification nat-div

nat-div/rax is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
nat-div/cond is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
nat-div/cond-01 is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,
nat-div/mod-le-02 is used by refine-truncate-buff-some, refine-truncate-buff-none-uncached, refine-truncate-buff-none-cached,

Used from specification cache-contracts

cache-contracts/fsync-dirs is used by refine-fsync,
cache-contracts/fsync-err is used by refine-fsync,
cache-contracts/fsync-keep-abs is used by refine-fsync,

Used from specification cache-asm

cache-asm/inv-fsync is used by refine-fsync,
cache-asm/inv-rename-dir-dentry is used by refine-rename-dir-dentry,
cache-asm/inv-rename-dir-negdentry is used by refine-rename-dir-negdentry,
cache-asm/inv-rename-file-dentry is used by refine-rename-file-dentry,
cache-asm/inv-rmdir is used by refine-rmdir,
cache-asm/inv-unlink is used by refine-unlink,

Used from specification afs-asm

afs-asm/afs-cons-rename-file-negdentry is used by refine-rename-file-negdentry,
afs-asm/inv-check-commit is used by refine-check-commit,