[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 root-ino

root-ino/neq-0 is used by refine-rename-overwrite-reparent-dir, refine-write-inode, initialization,

Used from specification store+set

store+set/dir-entries/Dom is used by refine-readdir,
store+set/node-index/In-data-in is used by refine-truncate,

Used from specification alink

alink/inj is used by rename-precond-abs, refine-rmdir, refine-unlink,
alink/sel-01 is used by rename-precond-abs, refine-evict, refine-rmdir, refine-unlink,
alink/sel-02 is used by rename-precond-abs, refine-evict, refine-rmdir, refine-unlink,

Used from specification nat-basic

Used from specification abstract-file

Used from specification aubifs-asm

aubifs-asm/elim-dentry is used by rename-precond-abs, refine-evict, refine-rmdir, refine-unlink,
aubifs-asm/inv-create is used by refine-create,
aubifs-asm/inv-gc is used by refine-gc,
aubifs-asm/inv-iget is used by refine-iget,
aubifs-asm/inv-link is used by refine-link,
aubifs-asm/inv-mkdir is used by refine-mkdir,
aubifs-asm/inv-rename-new-keep-parent is used by refine-rename-new-keep-parent,
aubifs-asm/inv-rename-new-reparent is used by refine-rename-new-reparent,
aubifs-asm/inv-rename-overwrite-keep-parent is used by refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different,
aubifs-asm/inv-rename-overwrite-reparent is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir,
aubifs-asm/inv-replay is used by recovery,
aubifs-asm/inv-rmdir is used by refine-rmdir,
aubifs-asm/inv-truncate is used by refine-truncate,
aubifs-asm/inv-unlink is used by refine-unlink,
aubifs-asm/replay-prog is used by recovery,
aubifs-asm/replaylog-prog is used by recovery,
aubifs-asm/replayorphans-prepost is used by recovery,
aubifs-asm/at-diff-ri is used by recovery, refine-truncate, refine-evict,
aubifs-asm/at-fs is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, log-cons-2, at-fs, refine-write-inode, refine-truncate, refine-writepage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create, initialization,
aubifs-asm/data-notin-del2 is used by refine-rmdir, refine-unlink,
aubifs-asm/data-notin-other1 is used by refine-rename-overwrite-keep-parent-identity, refine-truncate, refine-link, refine-mkdir, refine-create,
aubifs-asm/data-notin-other2 is used by refine-rename-overwrite-keep-parent-identity, refine-link, refine-mkdir, refine-create,
aubifs-asm/data-ubifs-cons is used by refine-readpage,
aubifs-asm/dentry-ubifs-cons is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-link, refine-rmdir, refine-unlink, refine-lookup,
aubifs-asm/inode-ubifs-cons is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-fsync, refine-write-inode, refine-truncate, refine-link, refine-rmdir, refine-unlink,

Used from specification afs-base

Used from specification list+set

list+set/address-list-set/toSet-app is used by refine-gc,

Used from specification node

Used from specification aubifs-replay

aubifs-replay/orphans-cons is used by recovery,
aubifs-replay/replay-cons-strong is used by recovery,
aubifs-replay/orphans-cons-reduce is used by refine-gc,
aubifs-replay/replay is used by recovery,
aubifs-replay/replay-cons-strong-safe is used by recovery,

Used from specification aubifs-refine

Used from specification aubifs-inv

Used from specification aubifs-base

Used from specification key

Used from specification aubifs-abs

Used from specification min-max

min-max/min-comm is used by eq-io-truncate, refine-truncate,
min-max/min-le-left is used by eq-io-truncate, refine-truncate,

Used from specification nat

nat/add-01 is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rmdir, refine-unlink,
nat/anti is used by eq-io-truncate, refine-truncate,
nat/elim-pred-c is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-rmdir, refine-unlink,
nat/elim-sub is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, eq-io-truncate, refine-truncate,
nat/fle is used by eq-io-truncate, refine-truncate,
nat/ge is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, afs-cons-abs-dir-subdirs, afs-cons-abs-dir-size, eq-io-truncate, refine-truncate, refine-renam, refine-rmdir, refine-unlink,
nat/le is used by eq-io-truncate, refine-truncate,
nat/le-def is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, afs-cons-abs-dir-subdirs, afs-cons-abs-dir-size, eq-io-truncate, refine-truncate, refine-readpage, refine-rmdir, refine-unlink,
nat/le-ls-simp is used by refine-truncate,
nat/lels is used by refine-truncate,
nat/lels-02 is used by refine-truncate, refine-rmdir,
nat/lep is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-rmdir, refine-unlink,
nat/lep-02 is used by eq-io-truncate, refine-truncate,
nat/ler is used by eq-io-truncate, refine-truncate, refine-readpage,
nat/lez is used by refine-rename-overwrite-reparent-file,
nat/ls-le-simp is used by refine-truncate,
nat/not-zero is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-renam, refine-rmdir, refine-unlink,

Used from specification set-union

set-union/dir-heap-refset/Delete is used by refine-evict,
set-union/node-index/One is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-renam, refine-rmdir, refine-unlink,
set-union/node-store/int-a is used by refine-check-commit, refine-gc,
set-union/node-store/int-c is used by refine-check-commit, refine-gc,
set-union/node-store/int-e is used by refine-check-commit,
set-union/node-store/intu-empty is used by refine-gc,
set-union/node-store/una is used by refine-gc,
set-union/node-store/unc is used by refine-gc,

Used from specification store

store/file-content/At-other is used by refine-writepage,
store/dir-entries/Extension is used by rename-precond-abs, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, afs-cons-abs-dir-size, refine-evict, refine-rmdir, refine-unlink,
store/file-content/In-insert is used by refine-writepage,
store/node-store/At-in-out is used by log-cons-2,
store/node-store/At-other is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-truncate, refine-writepage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
store/dir-entries/At-other is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-link, refine-mkdir, refine-create,
store/node-index/At-other is used by at-ri, refine-truncate,
store/file-content/At-other is used by refine-truncate,
store/node-index/At-same is used by at-ri,
store/dir-entries/At-same is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-link, refine-mkdir, refine-create,
store/file-content/At-same is used by refine-truncate,
store/dir-entries/Del-at is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-rmdir, refine-unlink,
store/node-index/Del-at-strong is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-evict, refine-rmdir, refine-unlink,
store/dir-entries/Del-empty is used by refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rmdir,
store/dir-entries/Del-in is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-rmdir, refine-unlink,
store/node-index/Del-in is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, in-del, refine-evict, refine-rmdir, refine-unlink,
store/dir-entries/In-empty is used by rename-precond-abs, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, afs-cons-abs-dir-size, refine-truncate, refine-evict, refine-rmdir, refine-mkdir, refine-unlink, initialization,
store/node-index/In-empty is used by initialization,
store/file-content/In-empty is used by refine-create,
store/node-store/In-empty is used by initialization,
store/dir-entries/In-insert is used by in-insert,
store/node-store/In-insert is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
store/dir-entries/Size-empty is used by refine-evict, refine-rmdir,
store/dir-entries/del-put is used by refine-rename-overwrite-keep-parent-identity,
store/node-index/del-put is used by refine-rename-overwrite-keep-parent-identity,
store/dir-entries/empty is used by afs-cons-abs-dir-size,
store/node-store/in-neq is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
store/dir-entries/in-neq is used by in-insert,
store/file-content/in-neq is used by refine-truncate,
store/node-index/ins3 is used by refine-rename-overwrite-reparent-dir, refine-link,
store/node-index/insin is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-truncate, refine-writepage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create, initialization,
store/file-content/insin is used by refine-truncate, refine-writepage,
store/node-index/insins is used by refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different,
store/file-content/k-At-same is used by refine-writepage,
store/node-index/notmemlookup is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-truncate, refine-readpage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create, refine-lookup,
store/node-store/notmemlookup is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-truncate, refine-writepage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,

Used from specification error-class

Used from specification error

Used from specification set-basic

set-basic/stringset/Extension is used by rename-precond-abs, refine-readdir, refine-rmdir,
set-basic/dir-heap-refset/Extension is used by valid-parent-ino-precond, recovery, refine-evict, initialization,
set-basic/alink-set/Extension is used by rename-precond-abs, refine-evict, refine-rmdir, refine-unlink,
set-basic/node-index/Extension is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-truncate, refine-evict, refine-writepage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
set-basic/alink-set/size-one-03 is used by rename-precond-abs, refine-rmdir, refine-unlink,
set-basic/dir-heap-refset/In-empty is used by recovery, initialization,
set-basic/node-index/In-empty is used by rename-precond-abs, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, recovery, refine-evict, refine-rmdir,
set-basic/alink-set/In-empty is used by rename-precond-abs, refine-evict, refine-rmdir, refine-unlink,
set-basic/stringset/In-empty is used by rename-precond-abs, refine-rmdir,
set-basic/node-index/In-insert is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rmdir, refine-unlink,
set-basic/alink-set/Size-empty is used by rename-precond-abs, refine-evict, refine-rmdir, refine-unlink,
set-basic/node-index/in-04 is used by rename-precond-abs, refine-rmdir, refine-unlink,
set-basic/alink-set/in-04 is used by rename-precond-abs, refine-rmdir, refine-unlink,
set-basic/alink-set/ne is used by rename-precond-abs,
set-basic/node-index/ne-01 is used by valid-parent-ino-precond,
set-basic/node-index/one-size is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rmdir, refine-unlink,
set-basic/alink-set/one-size is used by rename-precond-abs, refine-rmdir, refine-unlink,
set-basic/alink-set/size-one-01 is used by rename-precond-abs, refine-rmdir, refine-unlink,
set-basic/node-index/size-one-01 is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rmdir, refine-unlink,
set-basic/dir-heap-refset/size-zero is used by recovery, initialization,
set-basic/stringset/size-zero is used by afs-cons-abs-dir-subdirs,
set-basic/alink-set/size-zero is used by valid-parent-ino-precond, rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-link, refine-rmdir, refine-unlink,
set-basic/node-index/size-zero is used by rename-precond-abs, refine-evict, refine-rmdir,
set-basic/dir-heap-refset/size-zero-01 is used by recovery, initialization,
set-basic/stringset/size-zero-01 is used by afs-cons-abs-dir-subdirs,
set-basic/alink-set/size-zero-01 is used by valid-parent-ino-precond, rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
set-basic/node-index/size-zero-01 is used by valid-parent-ino-precond, rename-precond-abs, refine-evict, refine-rmdir,
set-basic/stringset/size-zero-02 is used by afs-cons-abs-dir-subdirs,
set-basic/alink-set/size-zero-02 is used by valid-parent-ino-precond, rename-precond-abs, refine-evict, refine-link, refine-rmdir, refine-unlink,

Used from specification dentry

Used from specification page

page/page-size is used by eq-io-truncate, refine-truncate, refine-readpage,
page/zeropage-eq-fill is used by refine-readpage,

Used from specification abstract-dir

Used from specification buffer-option

buffer-option/inj is used by eq-io-truncate, refine-truncate,
buffer-option/test-04 is used by eq-io-truncate,

Used from specification list

list/address-list-set/Last is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-truncate, refine-writepage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create, initialization,
list/address-list-set/Nil is used by initialization,
list/address-list-set/a is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create, initialization, refine-gc,
list/address-list-set/in-17 is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
list/address-list-set/in-rec is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,

Used from specification node-store

node-store/in-insert is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, log-cons-2, refine-write-inode, refine-truncate, refine-writepage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create, initialization,

Used from specification array-copy

array-copy/buffer/copy-exact is used by refine-readpage,
array-copy/buffer/size-fill-h is used by refine-truncate,

Used from specification list-dup

list-dup/address-list-set/c is used by refine-write-inode, refine-writepage, initialization,
list-dup/address-list-set/dups-cons is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
list-dup/address-list-set/rec is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
list-dup/address-list-set/two-01 is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,

Used from specification heap

heap/dir-heap/at-alloc is used by refine-mkdir,
heap/file-heap/at-diffs is used by recovery,
heap/dir-heap/at-diffs is used by recovery,
heap/file-heap/at-alloc is used by refine-create,
heap/file-heap/at-del is used by refine-evict,
heap/dir-heap/at-del is used by refine-evict,
heap/dir-heap/at-write is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create, initialization,
heap/file-heap/at-write is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, eq-io-truncate, refine-write-inode, refine-truncate, refine-writepage, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
heap/dir-heap/in-alloc is used by refine-mkdir, initialization,
heap/file-heap/in-alloc is used by refine-create,
heap/file-heap/in-del is used by refine-evict,
heap/dir-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/file-heap/in-emp is used by initialization,
heap/dir-heap/in-emp is used by initialization,
heap/file-heap/in-write is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, eq-io-truncate, refine-write-inode, refine-truncate, refine-writepage, refine-link, refine-unlink, refine-create,
heap/dir-heap/in-write is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create, initialization,
heap/file-heap/nonnull is used by refine-create,
heap/dir-heap/nonnull is used by refine-mkdir, refine-create,
heap/dir-heap/overwrite is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
heap/file-heap/overwrite is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, eq-io-truncate, refine-write-inode, refine-truncate, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
heap/dir-heap/overwrite-split is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rmdir,
heap/dir-heap/overwrite-split2 is used by refine-rename-overwrite-reparent-dir,

Used from specification nat-mult

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

Used from specification afs-pre

afs-pre/pre-create is used by refine-create,
afs-pre/pre-evict is used by eq-io-evict, refine-evict,
afs-pre/pre-iget is used by eq-io-iget, refine-iget,
afs-pre/pre-link is used by refine-link,
afs-pre/pre-lookup is used by eq-io-lookup, refine-lookup,
afs-pre/pre-mkdir is used by refine-mkdir,
afs-pre/pre-readdir is used by eq-io-readdir, refine-readdir,
afs-pre/pre-readpage is used by eq-io-readpage, refine-readpage,
afs-pre/pre-rename is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-reparent, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-overwrite-keep-parent, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-renam,
afs-pre/pre-rmdir is used by refine-rmdir,
afs-pre/pre-truncate is used by eq-io-truncate, 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 rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-reparent, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-overwrite-keep-parent, refine-rename-new-reparent, refine-rename-new-keep-parent, eq-io-evict, 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 rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-reparent, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-overwrite-keep-parent, refine-rename-new-reparent, refine-rename-new-keep-parent, eq-io-evict, eq-io-truncate, refine-fsync, refine-write-inode, refine-truncate, refine-evict, refine-renam, refine-link, refine-unlink,
afs-pre/valid-wb-inode is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-reparent, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-overwrite-keep-parent, refine-rename-new-reparent, refine-rename-new-keep-parent, eq-io-evict, refine-write-inode, refine-evict, refine-renam,

Used from specification inode

Used from specification nat-div

nat-div/mod-le-02 is used by eq-io-truncate, refine-truncate,

Used from specification aubifs-pre

aubifs-pre/pre-create is used by refine-create,
aubifs-pre/pre-lookup is used by refine-lookup,
aubifs-pre/pre-mkdir is used by refine-mkdir,
aubifs-pre/pre-evict is used by refine-evict,
aubifs-pre/pre-iget is used by refine-iget,
aubifs-pre/pre-link is used by refine-link,
aubifs-pre/pre-readdir is used by refine-readdir,
aubifs-pre/pre-readpage is used by refine-readpage,
aubifs-pre/pre-rename is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-renam,
aubifs-pre/pre-rename-new-keep-parent is used by refine-rename-new-keep-parent,
aubifs-pre/pre-rename-new-reparent is used by refine-rename-new-reparent,
aubifs-pre/pre-rename-overwrite-keep-parent is used by refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different,
aubifs-pre/pre-rename-overwrite-reparent is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir,
aubifs-pre/pre-rmdir is used by refine-rmdir,
aubifs-pre/pre-truncate is used by refine-truncate,
aubifs-pre/pre-unlink is used by refine-unlink,
aubifs-pre/pre-write-inode is used by refine-write-inode,
aubifs-pre/pre-writepage is used by refine-writepage,
aubifs-pre/valid-dir-inode is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-renam, refine-link, refine-rmdir, refine-mkdir, refine-unlink, refine-create,
aubifs-pre/valid-file-inode is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-write-inode, refine-truncate, refine-renam, refine-link, refine-unlink,
aubifs-pre/valid-wb-inode is used by rename-precond-abs, refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent, refine-renam,

Used from specification afs-asm

afs-asm/afs-cons-reduce is used by refine-truncate,
afs-asm/inv-create is used by refine-create,
afs-asm/inv-evict is used by refine-evict,
afs-asm/inv-link is used by refine-link,
afs-asm/inv-mkdir is used by refine-mkdir,
afs-asm/inv-renam is used by refine-rename-overwrite-reparent-file, refine-rename-overwrite-reparent-dir, refine-rename-overwrite-keep-parent-identity, refine-rename-overwrite-keep-parent-different, refine-rename-new-reparent, refine-rename-new-keep-parent,
afs-asm/inv-rmdir is used by refine-rmdir,
afs-asm/inv-truncate is used by refine-truncate,
afs-asm/inv-unlink is used by refine-unlink,
afs-asm/inv-write_inode is used by refine-write-inode,
afs-asm/inv-writepage is used by refine-writepage,

Used from specification aubifs-internal-asm

aubifs-internal-asm/inv-recover is used by recovery,