[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 alink

alink/inj is used by lastlink-move, afs-cons-rename-file-dentry, afs-cons-rename-dir-dentry,
alink/sel-01 is used by lastlink-move, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir, inv-link,
alink/sel-02 is used by lastlink-move, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir, inv-link,

Used from specification abstract-file

abstract-file/elim is used by inv-crash, afs-cons-rename-negdentry, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-rename-dentry, afs-cons-reduce, afs-cons-mkdir-ino, afs-cons-inode-sync, afs-cons-create-ino, inv-recovery, crash-neutral-unlink, crash-neutral-link, crash-neutral-renam, crash-neutral-readpage, crash-neutral-writepage, crash-neutral-evict, crash-neutral-truncate, inv-unlink, inv-rmdir, inv-link, inv-renam, inv-writepage, inv-evict, inv-truncate, inv-write_inode,
abstract-file/inj is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-inode-sync, afs-cons-create-ino, crash-neutral-link, crash-neutral-truncate, inv-unlink, inv-link, inv-writepage, inv-truncate, inv-write_inode,
abstract-file/sel-01 is used by afs-cons-reduce, crash-neutral-truncate, inv-writepage, inv-truncate,
abstract-file/sel-02 is used by afs-cons-rename-negdentry, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dentry, afs-cons-reduce, crash-neutral-link, crash-neutral-evict, crash-neutral-truncate, inv-unlink, inv-link, inv-renam, inv-evict, inv-truncate, inv-write_inode,
abstract-file/upd-04 is used by afs-cons-rename-file-dentry, afs-cons-inode-sync, inv-unlink, inv-link, inv-write_inode,
abstract-file/upd-05 is used by crash-neutral-writepage, inv-writepage, inv-truncate,
abstract-file/upd-06 is used by afs-cons-rename-file-dentry, afs-cons-inode-sync, inv-unlink, inv-link, inv-write_inode,
abstract-file/upd-07 is used by afs-cons-rename-file-dentry, crash-neutral-unlink, crash-neutral-link, inv-unlink, inv-link,

Used from specification nat-basic

nat-basic/a is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-create-ino, Insert-size, crash-neutral-unlink, crash-neutral-rmdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
nat-basic/add-base is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir,
nat-basic/c is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-create-ino, Insert-size, crash-neutral-unlink, crash-neutral-rmdir, inv-unlink, inv-rmdir, inv-link, inv-truncate,
nat-basic/eq-01 is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-create-ino, Insert-size, inv-link,
nat-basic/eq-02 is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir,
nat-basic/f is used by inv-truncate,
nat-basic/lf-01 is used by inv-truncate,
nat-basic/lf-02 is used by inv-truncate,
nat-basic/ls-02 is used by inv-truncate,
nat-basic/nls-fst is used by afs-cons-rename-file-dentry, afs-cons-rename-dir-dentry,
nat-basic/one is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-rmdir,
nat-basic/one-01 is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-unlink, crash-neutral-rmdir, inv-unlink, inv-rmdir,
nat-basic/one-03 is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
nat-basic/one-04 is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
nat-basic/oz is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-unlink, crash-neutral-rmdir, inv-unlink, inv-rmdir,
nat-basic/ref is used by inv-truncate,
nat-basic/z-01 is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir,

Used from specification afs-base

Used from specification set-union

set-union/dir-entries/del-size is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-rmdir,
set-union/dir-entries/size-eq-ext is used by afs-cons-mkdir-ino, inv-evict,
set-union/dir-entries/Delete is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
set-union/alink-set/Delete is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
set-union/dir-heap-refset/Delete is used by crash-neutral-evict,
set-union/dir-entries/One is used by inv-link,
set-union/alink-set/del-e-02 is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-rmdir,
set-union/dir-entries/del-in is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-rmdir,
set-union/alink-set/del-in is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir,
set-union/dir-entries/diff-e is used by afs-cons-create-ino, inv-link,
set-union/dir-entries/una is used by afs-cons-create-ino, inv-link,
set-union/dir-entries/unc is used by afs-cons-create-ino, inv-link,
set-union/dir-entries/une is used by afs-cons-create-ino, inv-link,

Used from specification nat

nat/add-01 is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir,
nat/anti is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
nat/elim-pred-c is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-unlink, crash-neutral-rmdir, inv-unlink, inv-rmdir,
nat/elim-sub is used by inv-truncate,
nat/eq-02 is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
nat/fle is used by inv-truncate,
nat/ge is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-unlink, crash-neutral-rmdir, inv-unlink, inv-rmdir, inv-truncate,
nat/le is used by inv-truncate,
nat/le-def is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-unlink, crash-neutral-rmdir, inv-unlink, inv-rmdir, inv-truncate,
nat/lels-02 is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
nat/lep is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-unlink, crash-neutral-rmdir, inv-unlink, inv-rmdir,
nat/lep-02 is used by inv-truncate,
nat/ler is used by inv-truncate,
nat/let is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
nat/not-zero is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-unlink, crash-neutral-rmdir, inv-unlink, inv-rmdir,
nat/one-02 is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-rmdir, inv-link,
nat/pred-03 is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir,
nat/succ-01 is used by afs-cons-rename-dir-dentry, inv-rmdir,

Used from specification store

store/dir-entries/At-other is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
store/file-content/At-other is used by inv-truncate,
store/dir-entries/Size-insert is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
store/dir-entries/At-in-out is used by afs-cons-rename-file-negdentry, afs-cons-rename-dir-negdentry, afs-cons-mkdir-ino, afs-cons-create-ino, inv-link,
store/dir-entries/At-other is used by afs-cons-rename-file-dentry, afs-cons-rename-dir-dentry,
store/file-content/At-other is used by inv-writepage,
store/file-content/At-same is used by inv-writepage, inv-truncate,
store/dir-entries/At-same is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-create-ino,
store/dir-entries/Del-at is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, Del-at-entries, inv-unlink, inv-rmdir,
store/dir-entries/Del-empty is used by afs-cons-rename-dir-dentry, inv-rmdir,
store/dir-entries/Del-in is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir,
store/file-content/In-empty is used by afs-cons-create-ino,
store/dir-entries/In-empty is used by inv-crash, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, inv-recovery, inv-unlink, inv-rmdir, inv-evict,
store/dir-entries/In-insert is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-create-ino, inv-link,
store/dir-entries/Size-empty is used by inv-crash, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, inv-recovery, inv-unlink, inv-rmdir, inv-evict,
store/dir-entries/Size-insert is used by afs-cons-rename-file-negdentry, afs-cons-rename-dir-negdentry, afs-cons-mkdir-ino, afs-cons-create-ino, inv-link,
store/dir-entries/del-put is used by afs-cons-rename-file-dentry, afs-cons-rename-dir-dentry,
store/dir-entries/empty is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir,
store/file-content/in-neq is used by inv-writepage, inv-truncate,
store/dir-entries/in-neq is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-create-ino,
store/dir-entries/ins is used by afs-cons-rename-file-dentry, afs-cons-rename-dir-dentry,
store/dir-entries/insin is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino,
store/dir-entries/k-At-same is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, inv-link,
store/dir-entries/lookupisempty is used by Del-at-entries,
store/dir-entries/neq is used by afs-cons-mkdir-ino, afs-cons-create-ino, inv-link,
store/dir-entries/notmemlookup is used by afs-cons-rename-file-negdentry, afs-cons-rename-dir-negdentry, afs-cons-mkdir-ino,
store/dir-entries/size is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-unlink, inv-rmdir,
store/dir-entries/size-in is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,

Used from specification min-max

min-max/min-comm is used by inv-truncate,
min-max/min-le-left is used by inv-truncate,

Used from specification error-class

error-class/ecommit is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-fsyncdir, inv-fsync, inv-sync, inv-recovery, inv-check-commit, inv-lookup, inv-create, inv-unlink, inv-mkdir, inv-rmdir, inv-link, inv-readpage, inv-writepage, inv-readdir, inv-truncate, inv-iget, inv-write_inode, inv-format,
error-class/efail is used by crash-neutral-unlink, crash-neutral-rmdir, crash-neutral-link, crash-neutral-renam, crash-neutral-truncate,
error-class/eio is used by crash-neutral-create, crash-neutral-mkdir, crash-neutral-writepage, crash-neutral-write_inode,
error-class/esuccess is used by crash-neutral-fsyncdir, crash-neutral-fsync, crash-neutral-sync, inv-recovery, crash-neutral-check-commit, inv-format,

Used from specification error

error/disj-91 is used by inv-fsyncdir, inv-fsync, inv-sync, inv-check-commit,

Used from specification set-basic

set-basic/alink-set/Extension is used by lastlink-move,
set-basic/dir-entries/Extension is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, inv-rmdir,
set-basic/dir-entries/Size-insert is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
set-basic/alink-set/size-one-03 is used by lastlink-move,
set-basic/dir-entries/In-empty is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, inv-rmdir,
set-basic/dir-entries/In-insert is used by afs-cons-mkdir-ino,
set-basic/alink-set/Size-empty is used by afs-cons-inode-sync, afs-cons-create-ino, inv-mkdir, inv-evict,
set-basic/dir-entries/Size-empty is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-rmdir,
set-basic/dir-entries/eq is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
set-basic/alink-set/eq is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
set-basic/alink-set/in-04 is used by lastlink-move,
set-basic/alink-set/ne is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry,
set-basic/alink-set/one-size is used by lastlink-move,
set-basic/alink-set/size-ins is used by inv-link,
set-basic/dir-entries/size-ins is used by afs-cons-rename-dir-negdentry, afs-cons-mkdir-ino,
set-basic/alink-set/size-one-01 is used by lastlink-move, afs-cons-mkdir-ino, afs-cons-create-ino,
set-basic/alink-set/size-zero is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-rmdir, inv-create, inv-unlink, inv-rmdir,
set-basic/dir-entries/size-zero is used by afs-cons-mkdir-ino,
set-basic/alink-set/size-zero-01 is used by inv-crash, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-inode-sync, afs-cons-create-ino, inv-recovery, crash-neutral-unlink, crash-neutral-rmdir, crash-neutral-evict, inv-create, inv-unlink, inv-rmdir, inv-link, inv-evict,
set-basic/dir-entries/size-zero-01 is used by afs-cons-mkdir-ino,
set-basic/alink-set/size-zero-02 is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-unlink, crash-neutral-rmdir, crash-neutral-evict, inv-unlink, inv-rmdir, inv-evict,
set-basic/dir-entries/size-zero-02 is used by afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, inv-rmdir,

Used from specification dentry

Used from specification page

page/page-size is used by crash-neutral-truncate, inv-truncate,

Used from specification abstract-dir

Used from specification array-copy

array-copy/buffer/size-fill-h is used by inv-truncate,

Used from specification afs-asm

Used from specification nat-mult

nat-mult/mult-a is used by inv-truncate,
nat-mult/mult-c is used by inv-truncate,

Used from specification heap

heap/dir-heap/at-alloc is used by afs-cons-mkdir-ino,
heap/file-heap/at-del is used by crash-neutral-evict,
heap/file-heap/at-diffs is used by crash-neutral-evict,
heap/dir-heap/at-diffs is used by crash-neutral-evict,
heap/dir-heap/diffs-sw is used by crash-neutral-evict,
heap/file-heap/diffs-sw is used by crash-neutral-evict,
heap/dir-heap/ext is used by crash-neutral-evict,
heap/file-heap/ext is used by crash-neutral-evict,
heap/file-heap/at-alloc is used by afs-cons-create-ino,
heap/dir-heap/at-del is used by crash-neutral-evict, inv-evict,
heap/file-heap/at-del is used by crash-neutral-evict, inv-evict,
heap/file-heap/at-diffs is used by inv-crash, inv-recovery, crash-neutral-evict,
heap/dir-heap/at-diffs is used by inv-crash, inv-recovery, crash-neutral-evict,
heap/dir-heap/at-write is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-inode-sync, afs-cons-create-ino, crash-neutral-unlink, crash-neutral-rmdir, crash-neutral-link, inv-create, inv-unlink, inv-mkdir, inv-rmdir, inv-link, inv-write_inode,
heap/file-heap/at-write is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-inode-sync, afs-cons-create-ino, crash-neutral-unlink, crash-neutral-rmdir, crash-neutral-link, inv-create, inv-unlink, inv-rmdir, inv-link, inv-writepage, inv-truncate, inv-write_inode,
heap/file-heap/in-alloc is used by afs-cons-create-ino, New-same,
heap/dir-heap/in-alloc is used by afs-cons-mkdir-ino, inv-mkdir,
heap/dir-heap/in-del is used by crash-neutral-evict, inv-evict,
heap/file-heap/in-del is used by crash-neutral-evict, inv-evict,
heap/file-heap/in-diffs is used by inv-crash, inv-recovery, crash-neutral-evict,
heap/dir-heap/in-diffs is used by inv-crash, inv-recovery, crash-neutral-evict,
heap/dir-heap/in-write is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-inode-sync, afs-cons-create-ino, crash-neutral-unlink, crash-neutral-rmdir, crash-neutral-link, inv-create, inv-unlink, inv-mkdir, inv-rmdir, inv-link, inv-write_inode,
heap/file-heap/in-write is used by afs-cons-rename-file-dentry, afs-cons-inode-sync, afs-cons-create-ino, New-same, crash-neutral-unlink, crash-neutral-link, inv-unlink, inv-link, inv-writepage, inv-truncate, inv-write_inode,
heap/file-heap/overwrite is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-inode-sync, crash-neutral-unlink, crash-neutral-rmdir, crash-neutral-link, inv-create, inv-unlink, inv-rmdir, inv-link, inv-write_inode,
heap/dir-heap/overwrite is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-mkdir-ino, afs-cons-create-ino, crash-neutral-unlink, crash-neutral-rmdir, crash-neutral-link, inv-create, inv-unlink, inv-mkdir, inv-rmdir, inv-link,
heap/dir-heap/overwrite-split is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-rmdir, inv-rmdir,
heap/dir-heap/overwrite-split2 is used by afs-cons-rename-dir-dentry,
heap/dir-heap/write-again is used by afs-cons-rename-file-dentry, afs-cons-rename-dir-dentry,

Used from specification inode

Used from specification afs-pre

afs-pre/pre-create is used by afs-cons-create-ino, crash-neutral-create, inv-create,
afs-pre/pre-evict is used by crash-neutral-evict, inv-evict,
afs-pre/pre-iget is used by crash-neutral-iget, inv-iget,
afs-pre/pre-link is used by crash-neutral-link, inv-link,
afs-pre/pre-lookup is used by crash-neutral-lookup, inv-lookup,
afs-pre/pre-mkdir is used by afs-cons-mkdir-ino, crash-neutral-mkdir, inv-mkdir,
afs-pre/pre-readdir is used by crash-neutral-readdir, inv-readdir,
afs-pre/pre-readpage is used by crash-neutral-readpage, inv-readpage,
afs-pre/pre-rename is used by afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, crash-neutral-renam, inv-renam,
afs-pre/pre-rmdir is used by crash-neutral-rmdir, inv-rmdir,
afs-pre/pre-truncate is used by crash-neutral-truncate, inv-truncate,
afs-pre/pre-unlink is used by crash-neutral-unlink, inv-unlink,
afs-pre/pre-write-inode is used by crash-neutral-write_inode, inv-write_inode,
afs-pre/pre-writepage is used by crash-neutral-writepage, inv-writepage,
afs-pre/valid-dir-inode is used by afs-cons-rename-negdentry, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-rename-dentry, afs-cons-mkdir-ino, afs-cons-create-ino, crash-neutral-create, crash-neutral-unlink, crash-neutral-mkdir, crash-neutral-rmdir, crash-neutral-link, crash-neutral-renam, crash-neutral-evict, crash-neutral-write_inode, inv-create, inv-unlink, inv-mkdir, inv-rmdir, inv-link, inv-renam, inv-evict, inv-write_inode,
afs-pre/valid-file-inode is used by afs-cons-rename-negdentry, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-rename-dentry, inv-fsync, crash-neutral-fsync, crash-neutral-unlink, crash-neutral-link, crash-neutral-renam, crash-neutral-evict, crash-neutral-truncate, crash-neutral-write_inode, inv-unlink, inv-link, inv-renam, inv-evict, inv-truncate, inv-write_inode,
afs-pre/valid-wb-inode is used by afs-cons-rename-negdentry, afs-cons-rename-file-negdentry, afs-cons-rename-file-dentry, afs-cons-rename-dir-negdentry, afs-cons-rename-dir-dentry, afs-cons-rename-dentry, crash-neutral-renam, crash-neutral-evict, crash-neutral-write_inode, inv-renam, inv-evict, inv-write_inode,

Used from specification nat-div

nat-div/mod-le-02 is used by inv-truncate,