[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 vfs-base

vfs-base/is-open is used by inv-put-inode, inv-close,
vfs-base/of-cons is used by of-cons-reduce, inv-close, inv-format,
vfs-base/valid-content is used by valid-content-reduce,
vfs-base/dir-not-open is used by inv-rmdir, inv-renam,
vfs-base/min-0 is used by read-loop-term,
vfs-base/min-less-first is used by read-loop-term,
vfs-base/min-less-second is used by read-loop-term,
vfs-base/min-less-third is used by read-loop-term,
vfs-base/of-cons-file is used by write-term, inv-put-inode, inv-open, inv-close, inv-seek, inv-read, inv-write,
vfs-base/of-cons-notdir is used by write-term, inv-put-inode, inv-close, inv-seek, inv-read, inv-write,

Used from specification store+set

store+set/open-files/dom-add-in is used by inv-seek, inv-read, inv-write,
store+set/open-files/dom-del is used by inv-close,
store+set/open-files/dom-emp is used by inv-recover, inv-format,
store+set/open-files/dom-ins is used by inv-open, inv-seek, inv-read, inv-write,

Used from specification nat-set

nat-set/ls-add-1 is used by inv-open,
nat-set/ls-add-bound is used by inv-open,

Used from specification nat-basic

nat-basic/a is used by write-term, write-loop-term, write-loop-0, walk-term, walk-prepost-h, read-loop-term, inv-rmdir, inv-unlink, inv-renam, inv-open, inv-truncate, inv-read, inv-write,
nat-basic/add-base is used by write-term, write-loop-0, inv-read, inv-write,
nat-basic/c is used by write-term, write-loop-term, write-loop-0, walk-term, walk-prepost-h, read-loop-term, inv-rmdir, inv-unlink, inv-renam, inv-open, inv-truncate, inv-read, inv-write,
nat-basic/eq-01 is used by read-loop-term,
nat-basic/eq-02 is used by read-loop-term, inv-write,
nat-basic/f is used by write-term, write-loop-term, read-loop-term, inv-write,
nat-basic/l is used by write-loop-term, read-loop-term, inv-write,
nat-basic/l-01 is used by read-loop-term,
nat-basic/l-02 is used by write-loop-term, read-loop-term,
nat-basic/lf-01 is used by write-term, inv-write,
nat-basic/lf-02 is used by write-term, write-loop-term, read-loop-term, inv-write,
nat-basic/ls-02 is used by write-term,
nat-basic/oz is used by inv-rmdir, inv-unlink, inv-renam,
nat-basic/s-04 is used by walk-term, walk-prepost-h,
nat-basic/succ is used by walk-term, walk-prepost-h,
nat-basic/z-01 is used by write-loop-0,

Used from specification abstract-file

abstract-file/elim is used by write-term, write-loop-term, write-loop-err, write-loop-0, valid-content-reduce, read-loop-term, inv-put-inode, inv-fsync, inv-writemeta, inv-unlink, inv-renam, inv-link, inv-open, inv-close, inv-truncate, inv-seek, inv-read, inv-write,
abstract-file/inj is used by write-term, write-loop-term, inv-fsync, inv-unlink, inv-renam, inv-link, inv-truncate, inv-write,
abstract-file/sel-01 is used by write-term, write-loop-term, valid-content-reduce, inv-truncate, inv-write,
abstract-file/sel-02 is used by write-term, write-loop-term, inv-put-inode, inv-fsync, inv-writemeta, inv-unlink, inv-renam, inv-link, inv-close, inv-truncate, inv-write,
abstract-file/sel-06 is used by write-term, valid-content-reduce, inv-unlink, inv-renam, inv-link, inv-write,
abstract-file/sel-07 is used by write-term, inv-writemeta, inv-unlink, inv-renam, inv-link, inv-write,
abstract-file/upd-04 is used by write-term, inv-unlink, inv-renam, inv-link, inv-truncate, inv-write,
abstract-file/upd-05 is used by write-term, write-loop-term, inv-truncate, inv-write,
abstract-file/upd-06 is used by write-term, inv-unlink, inv-renam, inv-link, inv-truncate, inv-write,
abstract-file/upd-07 is used by inv-unlink, inv-renam, inv-link,

Used from specification afs-base

afs-base/afs-cons is used by inv-rmdir, inv-renam,
afs-base/expath is used by walk-prepost-h,
afs-base/path-trans is used by walk-prepost-h,
afs-base/valid-content is used by valid-content-reduce,
afs-base/afs-cons-dir-nlink is used by walk-term, walk-prepost-parent, walk-prepost-h, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-readdir,
afs-base/afs-cons-file-nlink is used by write-term, write-loop-term, read-loop-term, inv-put-inode, inv-fsync, inv-unlink, inv-renam, inv-link, inv-open, inv-truncate, inv-read, inv-write,
afs-base/afs-cons-in-next is used by walk-term, walk-prepost-h, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-write,
afs-base/afs-cons-init is used by inv-format,
afs-base/afs-cons-links-empty is used by inv-put-inode, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
afs-base/afs-cons-nlink0-notin is used by inv-truncate,
afs-base/afs-cons-notfile is used by write-loop-term, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-write,
afs-base/afs-cons-pagesize is used by write-term, write-loop-term, read-loop-term, inv-truncate, inv-write,
afs-base/afs-cons-root-dir is used by write-loop-term, walk-prepost-parent, walk-prepost-h, walk-prepost, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-write,
afs-base/afs-cons-root-notfile is used by walk-term, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-close,
afs-base/at-upto is used by inv-write,
afs-base/dir-empty is used by write-loop-term, inv-rmdir, inv-renam, inv-write,
afs-base/expath-eps is used by walk-prepost-h,
afs-base/expath-rec is used by walk-prepost-parent, walk-prepost-h,
afs-base/getinode is used by write-term, walk-term, walk-prepost-h, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-close, inv-truncate, inv-seek, inv-readdir, inv-read, inv-write,
afs-base/in-upto is used by inv-write,
afs-base/links-nonempty is used by walk-term, walk-prepost-h, inv-rmdir, inv-unlink, inv-renam, inv-link,
afs-base/meta-dir is used by walk-prepost-h,
afs-base/meta-path is used by walk-prepost-h,
afs-base/path-file is used by walk-prepost-h,
afs-base/path-here is used by walk-prepost-h, walk-prepost, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
afs-base/path-in-dirs is used by inv-link,
afs-base/path-in-end is used by inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-truncate, inv-readmeta, inv-readdir,
afs-base/path-links-empty is used by inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
afs-base/path-one is used by walk-prepost-h,
afs-base/path-rec is used by walk-prepost-parent, walk-prepost-h,
afs-base/valid-dentry-03 is used by inv-link,
afs-base/valid-dentry-with-parent is used by inv-rmdir, inv-unlink, inv-renam, inv-link,
afs-base/valid-dir-ino is used by write-term, walk-prepost-parent, walk-prepost-h, inv-put-inode, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-close, inv-readdir, inv-write,
afs-base/valid-file-ino is used by write-term, write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-put-inode, inv-fsync, inv-writemeta, inv-unlink, inv-renam, inv-link, inv-close, inv-truncate, inv-write,
afs-base/valid-ino is used by write-term, write-loop-term, walk-term, walk-prepost-h, walk-prepost, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-close, inv-truncate, inv-seek, inv-readmeta, inv-readdir, inv-read, inv-write,
afs-base/valid-negdentry is used by inv-create, inv-mkdir, inv-renam, inv-link,
afs-base/valid-pagesize is used by write-loop-term, inv-rmdir, inv-renam, inv-write,
afs-base/valid-parent-ino is used by walk-term, walk-prepost-h, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,

Used from specification file-mode

file-mode/disj-01 is used by inv-truncate,
file-mode/disj-02 is used by inv-fsync, inv-truncate, inv-readdir,
file-mode/disj-03 is used by inv-fsync, inv-readdir,

Used from specification file

file/elim is used by write-term, of-cons-reduce, inv-put-inode, inv-open, inv-close, inv-seek, inv-read, inv-write,
file/inj is used by inv-open, inv-seek, inv-read, inv-write,
file/sel is used by of-cons-reduce, inv-put-inode, inv-open, inv-close, inv-seek, inv-read, inv-write,
file/sel-02 is used by inv-read,
file/upd-03 is used by inv-seek, inv-read, inv-write,

Used from specification nat

nat/cancel-01 is used by write-loop-term, read-loop-term, inv-write,
nat/elim-pred-c is used by inv-rmdir, inv-unlink, inv-renam,
nat/elim-sub is used by write-term, write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-truncate, inv-write,
nat/eq-01 is used by write-term, write-loop-term, read-loop-term, inv-read,
nat/eq-02 is used by inv-write,
nat/fle-01 is used by write-loop-term, read-loop-term,
nat/ge is used by write-term, write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-rmdir, inv-unlink, inv-renam, inv-truncate, inv-write,
nat/le is used by write-term, inv-truncate, inv-write,
nat/le-add is used by write-loop-term, read-loop-term,
nat/le-def is used by write-term, write-loop-term, read-loop-term, inv-read, inv-write,
nat/le-ls-simp is used by write-term, valid-content-reduce, inv-read, inv-write,
nat/lels is used by write-loop-term, valid-content-reduce, read-loop-term, inv-write,
nat/lels-02 is used by read-loop-term,
nat/lels-03 is used by read-loop-term,
nat/lep is used by write-term, write-loop-term, read-loop-term, inv-rmdir, inv-unlink, inv-renam, inv-read, inv-write,
nat/lep-02 is used by write-term, write-loop-term, read-loop-term, inv-truncate, inv-write,
nat/ler is used by write-term, inv-truncate, inv-write,
nat/let is used by write-loop-term, read-loop-term, inv-write,
nat/lez is used by inv-write,
nat/ls-01 is used by write-loop-term, read-loop-term,
nat/ls-03 is used by write-loop-term, read-loop-term,
nat/ls-le-simp is used by inv-write,
nat/not-zero is used by inv-rmdir, inv-unlink, inv-renam,
nat/zero-02 is used by read-loop-term, inv-write,

Used from specification store

store/open-files/At-other is used by inv-seek, inv-write,
store/file-content/At-in-out is used by inv-write,
store/file-content/At-other is used by write-loop-term, inv-write,
store/open-files/At-other is used by inv-open, inv-seek, inv-read, inv-write,
store/file-content/At-same is used by write-loop-term, inv-write,
store/open-files/At-same is used by inv-open, inv-seek, inv-read, inv-write,
store/open-files/Del-at is used by inv-close,
store/open-files/Del-in is used by inv-close,
store/open-files/In-empty is used by inv-recover, inv-format,
store/file-content/In-insert is used by inv-write,
store/open-files/In-insert is used by inv-open, inv-seek, inv-read, inv-write,
store/dir-entries/del-put is used by inv-renam,
store/dir-entries/empty is used by inv-rmdir, inv-renam,
store/file-content/in-neq is used by write-loop-term, inv-write,
store/open-files/in-neq is used by inv-open, inv-seek, inv-read, inv-write,
store/dir-entries/ins is used by inv-renam,
store/open-files/ins is used by inv-read, inv-write,
store/open-files/insin is used by inv-seek, inv-write,
store/open-files/k-At-same is used by inv-open, inv-seek, inv-read, inv-write,
store/dir-entries/notmemlookup is used by inv-rmdir,
store/open-files/notmemlookup is used by write-term, inv-read, inv-write,

Used from specification min-max

min-max/min-comm is used by inv-truncate,
min-max/min-le-left is used by inv-truncate,
min-max/min-notls1 is used by write-loop-term,
min-max/min-notls2 is used by write-loop-term,
min-max/min-same is used by write-term, inv-write,

Used from specification error-class

error-class/eaccess is used by walk-prepost-parent, walk-prepost-h,
error-class/ecommit is used by write-term, write-loop-term, walk-term, read-loop-term, inv-fsync, inv-sync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-close, inv-truncate, inv-seek, inv-readmeta, inv-readdir, inv-read, inv-format,
error-class/enoent is used by walk-prepost-h, inv-create, inv-mkdir, inv-renam, inv-link,
error-class/esuccess is used by write-term, write-loop-term, write-loop-err, write-loop-0, walk-prepost-h, inv-fsync, inv-writemeta, inv-recover, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-truncate, inv-readmeta, inv-readdir, inv-write, inv-format,
error-class/not-esuccess is used by write-term, write-loop-term, write-loop-err, write-loop-0, walk-term, walk-prepost-h, read-loop-term, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-close, inv-truncate, inv-seek, inv-readmeta, inv-readdir, inv-read, inv-write,

Used from specification error

error/disj-07 is used by walk-prepost-parent, walk-prepost-h,
error/disj-29 is used by walk-term, walk-prepost-parent, walk-prepost-h, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-truncate, inv-readmeta, inv-readdir,
error/disj-31 is used by inv-fsync, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-truncate, inv-readdir,
error/disj-32 is used by inv-fsync, inv-unlink, inv-renam, inv-link, inv-open, inv-truncate, inv-readdir,
error/disj-33 is used by walk-term, walk-prepost-h, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-truncate, inv-readmeta, inv-readdir,
error/disj-34 is used by inv-create, inv-mkdir, inv-link,
error/disj-55 is used by inv-rmdir, inv-renam,
error/disj-91 is used by write-term, write-loop-term, inv-fsync, inv-sync, inv-writemeta, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-truncate,

Used from specification set-basic

set-basic/alink-set/Size-empty is used by inv-truncate,
set-basic/alink-set/size-zero is used by walk-term, inv-rmdir, inv-unlink, inv-renam,
set-basic/alink-set/size-zero-01 is used by walk-term,
set-basic/alink-set/size-zero-02 is used by inv-put-inode,

Used from specification list-last

list-last/path/b-01 is used by walk-prepost-parent, inv-link,
list-last/path/bc is used by walk-prepost-parent, walk-prepost-h,
list-last/path/butlast-def is used by walk-prepost-h,
list-last/path/butlast-last is used by walk-prepost-parent,
list-last/path/butlast-one is used by inv-link,
list-last/path/last-def is used by inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
list-last/path/last-elim is used by walk-prepost-parent,
list-last/path/prefix-app is used by walk-prepost-parent,
list-last/path/prefix-attach is used by px-last,
list-last/path/prefix-empty is used by px-last,
list-last/path/prefix-nil is used by walk-prepost-h,
list-last/path/prefix-rec-02 is used by walk-prepost-h,
list-last/path/prefix-self is used by px-last,

Used from specification list-data

list-data/path/elim-list-c is used by walk-term, walk-prepost-parent, walk-prepost-h, inv-link,

Used from specification path-permission

path-permission/vfs-permission/px is used by px-last,
path-permission/vfs-permission/px-eps is used by walk-prepost-h,
path-permission/vfs-permission/px-parent-eps is used by walk-prepost-h, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
path-permission/vfs-permission/px-parent-last is used by walk-prepost-h,
path-permission/vfs-permission/px-parent-noneps is used by walk-prepost-h,
path-permission/vfs-permission/px-prefix is used by walk-prepost-parent,

Used from specification dentry

dentry/disj is used by inv-renam,
dentry/inj is used by inv-renam,
dentry/sel-03 is used by walk-term, walk-prepost-h, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
dentry/sel-04 is used by inv-rmdir, inv-unlink, inv-renam, inv-link,
dentry/sel-05 is used by walk-term, walk-prepost-h, inv-rmdir, inv-unlink, inv-renam, inv-link,
dentry/test-01 is used by inv-create, inv-mkdir, inv-renam, inv-link,
dentry/test-02 is used by walk-term, walk-prepost-h, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
dentry/test-03 is used by inv-renam,
dentry/test-04 is used by inv-renam,

Used from specification abstract-dir

abstract-dir/elim is used by write-loop-term, walk-term, walk-prepost-parent, walk-prepost-h, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-readdir, inv-write,
abstract-dir/inj is used by walk-prepost-h, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
abstract-dir/sel-03 is used by inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
abstract-dir/sel-04 is used by walk-prepost-h, inv-writemeta, inv-rmdir, inv-renam,
abstract-dir/sel-05 is used by inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
abstract-dir/sel-08 is used by inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
abstract-dir/sel-09 is used by walk-term, walk-prepost-h, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
abstract-dir/upd-03 is used by inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
abstract-dir/upd-04 is used by inv-create, inv-rmdir, inv-unlink, inv-renam, inv-link,
abstract-dir/upd-05 is used by inv-rmdir, inv-renam,
abstract-dir/upd-08 is used by inv-mkdir, inv-rmdir, inv-renam,
abstract-dir/upd-09 is used by inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
abstract-dir/updsel-01 is used by inv-renam,
abstract-dir/updsel-03 is used by inv-renam,
abstract-dir/updsel-09 is used by inv-renam,
abstract-dir/updsel-11 is used by inv-renam,
abstract-dir/updsel-13 is used by inv-rmdir, inv-unlink, inv-renam, inv-link,
abstract-dir/updsel-20 is used by inv-mkdir, inv-rmdir, inv-renam,
abstract-dir/updsel-21 is used by inv-renam,
abstract-dir/updsel-24 is used by inv-mkdir, inv-rmdir, inv-renam,

Used from specification page

page/emptypage-size is used by write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-write,
page/page-size is used by write-term, write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-truncate, inv-write,

Used from specification buffer-option

buffer-option/test-03 is used by write-term, inv-truncate, inv-write,

Used from specification list

list/path/Last is used by walk-prepost-parent, walk-prepost-h, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
list/path/Nil is used by walk-prepost-h, walk-prepost,
list/path/a is used by walk-term, walk-prepost-parent, walk-prepost-h, walk-prepost, px-last, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
list/path/app is used by walk-prepost-h, inv-link,
list/path/app-02 is used by walk-term, walk-prepost-parent, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
list/path/app-04 is used by walk-prepost-parent,
list/path/app-08 is used by walk-prepost-parent,
list/path/c is used by walk-term, walk-prepost-parent, walk-prepost-h, inv-link,
list/path/c-03 is used by inv-link,
list/path/c-07 is used by walk-term, walk-prepost-h,
list/path/e is used by walk-term, walk-prepost-parent, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
list/path/e-01 is used by walk-term, walk-prepost-parent, walk-prepost-h, inv-link,
list/path/e-02 is used by walk-prepost-h, px-last, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
list/path/in-14 is used by walk-term, walk-prepost-parent, walk-prepost-h,
list/path/in-15 is used by walk-prepost-parent,
list/path/in-17 is used by walk-prepost-parent,
list/path/in-append is used by walk-prepost-parent,
list/path/in-rec is used by walk-term, walk-prepost-parent, walk-prepost-h,
list/path/len-05 is used by walk-term, walk-prepost-h,

Used from specification array-copy

array-copy/buffer/size-copy is used by write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-write,
array-copy/buffer/size-fill-h is used by inv-write,

Used from specification heap

heap/file-heap/at-write is used by write-term, write-loop-term, inv-writemeta, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-truncate, inv-write,
heap/dir-heap/at-write is used by inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
heap/file-heap/in-alloc is used by inv-create,
heap/dir-heap/in-alloc is used by inv-mkdir,
heap/file-heap/in-del is used by inv-put-inode,
heap/file-heap/in-write is used by write-term, write-loop-term, inv-writemeta, inv-create, inv-unlink, inv-renam, inv-link, inv-truncate, inv-write,
heap/dir-heap/in-write is used by write-term, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-write,
heap/file-heap/overwrite is used by write-term, inv-writemeta, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-truncate, inv-write,
heap/dir-heap/overwrite is used by inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
heap/dir-heap/overwrite-split is used by inv-rmdir, inv-renam,
heap/dir-heap/overwrite-split2 is used by inv-renam,
heap/file-heap/write-again is used by inv-renam,
heap/dir-heap/write-again is used by inv-renam,

Used from specification nat-mult

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

Used from specification oelem

oelem/nat-set/irreflexivity is used by walk-term, walk-prepost-h,

Used from specification afs-pre

afs-pre/pre-create is used by inv-create,
afs-pre/pre-evict is used by inv-put-inode, inv-rmdir, inv-unlink, inv-renam, inv-close,
afs-pre/pre-iget is used by write-term, walk-term, walk-prepost-h, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-close, inv-truncate, inv-seek, inv-readmeta, inv-readdir, inv-read, inv-write,
afs-pre/pre-link is used by inv-link,
afs-pre/pre-lookup is used by walk-term, walk-prepost-h, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link,
afs-pre/pre-mkdir is used by inv-mkdir,
afs-pre/pre-readdir is used by inv-readdir,
afs-pre/pre-readpage is used by write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-write,
afs-pre/pre-rename is used by inv-renam,
afs-pre/pre-rmdir is used by inv-rmdir,
afs-pre/pre-truncate is used by write-term, inv-truncate, inv-write,
afs-pre/pre-unlink is used by inv-unlink,
afs-pre/pre-write-inode is used by write-term, inv-writemeta, inv-write,
afs-pre/pre-writepage is used by write-loop-term, write-loop-err, write-loop-0, inv-write,
afs-pre/valid-dir-inode is used by write-term, inv-put-inode, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-close, inv-write,
afs-pre/valid-file-inode is used by write-term, write-loop-term, inv-put-inode, inv-fsync, inv-writemeta, inv-unlink, inv-renam, inv-link, inv-close, inv-truncate, inv-write,
afs-pre/valid-wb-inode is used by write-term, inv-put-inode, inv-writemeta, inv-rmdir, inv-unlink, inv-renam, inv-close, inv-write,

Used from specification inode

inode/elim is used by write-term, write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-put-inode, inv-writemeta, inv-write,
inode/inj is used by write-term, inv-writemeta, inv-write,
inode/sel-01 is used by write-term, write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-put-inode, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-close, inv-truncate, inv-readdir, inv-read, inv-write,
inode/sel-02 is used by write-term, walk-term, walk-prepost-h, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-truncate, inv-readdir, inv-write,
inode/sel-03 is used by write-term, walk-term, walk-prepost-h, inv-put-inode, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-open, inv-close, inv-truncate, inv-readdir, inv-read, inv-write,
inode/sel-04 is used by write-term, inv-put-inode, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-close, inv-truncate, inv-write,
inode/sel-10 is used by write-term, inv-put-inode, inv-fsync, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-close, inv-truncate, inv-write,
inode/sel-11 is used by write-term, read-loop-term, inv-put-inode, inv-writemeta, inv-create, inv-mkdir, inv-rmdir, inv-unlink, inv-renam, inv-link, inv-truncate, inv-seek, inv-read, inv-write,
inode/upd-02 is used by inv-writemeta,
inode/upd-11 is used by write-term, inv-truncate, inv-write,

Used from specification path

path/parent-elim is used by px-last,

Used from specification oset

oset/nat-set/ls-emptyset is used by inv-recover, inv-format,
oset/nat-set/ls-rm is used by inv-close,

Used from specification seekflag

seekflag/disj-03 is used by inv-seek,

Used from specification array

array/buffer/Size-mkarray is used by write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-write,

Used from specification nat-div

nat-div/rax is used by inv-write,
nat-div/cond is used by inv-write,
nat-div/mod-le-02 is used by write-term, write-loop-term, write-loop-err, write-loop-0, read-loop-term, inv-truncate, inv-write,

Used from specification afs-asm

afs-asm/afs-cons-reduce is used by write-loop-term, inv-write,
afs-asm/inv-check-commit is used by inv-create, inv-mkdir,
afs-asm/inv-create is used by inv-create,
afs-asm/inv-evict is used by inv-put-inode,
afs-asm/inv-iget is used by inv-link,
afs-asm/inv-link is used by inv-link,
afs-asm/inv-lookup is used by inv-create,
afs-asm/inv-mkdir is used by inv-mkdir,
afs-asm/inv-recovery is used by inv-recover,
afs-asm/inv-renam is used by inv-renam,
afs-asm/inv-rmdir is used by inv-rmdir,
afs-asm/inv-truncate is used by write-term, inv-truncate,
afs-asm/inv-unlink is used by inv-unlink,
afs-asm/inv-write_inode is used by inv-writemeta,