[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 of,
vfs-base/dir-not-open is used by refine-rmdir,
vfs-base/of-cons-file is used by refine-seek, refine-write, refine-read, refine-close,
vfs-base/of-cons-notdir is used by refine-seek, refine-read, refine-close,

Used from specification root-ino

root-ino/neq-0 is used by initialization,

Used from specification store+set

store+set/open-files/Dom is used by refine-open,
store+set/dir-entries/Dom is used by refine-readdir,
store+set/directory-tree-inst/Dom is used by refine-readdir,
store+set/open-files/dom-add-in is used by refine-read,
store+set/open-files/dom-del is used by refine-close,
store+set/open-files/dom-emp is used by recovery,
store+set/open-files/dom-ins is used by refine-read, refine-open,

Used from specification alink

alink/elim is used by refine-readmeta,
alink/inj is used by refine-readmeta,
alink/sel-01 is used by refine-readmeta,
alink/sel-02 is used by refine-readmeta,

Used from specification nat-basic

nat-basic/addex is used by refine-truncate,
nat-basic/a is used by abs-fold-new-p, abs-fold-del-p, abs-fold-del, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-read, refine-open, refine-create, refine-rmdir,
nat-basic/add-base is used by abs-fold-del-p, abs-fold-del, refine-truncate, refine-unlink, refine-read, refine-rmdir,
nat-basic/c is used by abs-fold-new-p, abs-fold-del-p, abs-fold-del, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-read, refine-open, refine-create, refine-rmdir,
nat-basic/eq-01 is used by abs-fold-new-p, refine-readmeta, refine-seek,
nat-basic/f is used by refine-truncate, refine-read,
nat-basic/l is used by refine-truncate, refine-read,
nat-basic/l-01 is used by refine-truncate, refine-read,
nat-basic/l-02 is used by refine-read,
nat-basic/lf is used by refine-truncate,
nat-basic/lf-01 is used by refine-truncate,
nat-basic/lf-02 is used by refine-truncate, refine-read,
nat-basic/ls-02 is used by refine-truncate,
nat-basic/nls-fst is used by refine-truncate,
nat-basic/one is used by refine-truncate,
nat-basic/one-01 is used by refine-rmdir,
nat-basic/oz is used by refine-unlink, refine-rmdir,
nat-basic/succ is used by refine-truncate,
nat-basic/zero is used by refine-truncate,

Used from specification array-splice

array-splice/buffer/resize-at is used by refine-truncate,
array-splice/buffer/resize-len is used by refine-truncate,

Used from specification nat-set

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

Used from specification abstract-file

abstract-file/elim is used by refine-fsync, recovery, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-write, refine-read, refine-close, refine-open, refine-rmdir,
abstract-file/inj is used by refine-fsync, refine-truncate, refine-unlink, refine-link, refine-read,
abstract-file/sel-01 is used by recovery, refine-writemeta, refine-truncate, refine-write, refine-read,
abstract-file/sel-02 is used by refine-writemeta, refine-unlink, refine-link, refine-close, refine-rmdir,
abstract-file/sel-06 is used by recovery, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-write, refine-read,
abstract-file/sel-07 is used by refine-fsync, recovery, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-write, refine-open,
abstract-file/upd-04 is used by refine-writemeta, refine-truncate, refine-unlink, refine-link,
abstract-file/upd-05 is used by refine-truncate,
abstract-file/upd-06 is used by refine-writemeta, refine-truncate, refine-unlink, refine-link,
abstract-file/upd-07 is used by refine-unlink, refine-link,

Used from specification afs-base

afs-base/afs-cons is used by make-abs-fold-work, refine-readmeta, refine-unlink, refine-rmdir,
afs-base/afs-cons-links-empty is used by refine-unlink,
afs-base/expath is used by ispath-target,
afs-base/orphans is used by recovery,
afs-base/path-split is used by refine-readmeta,
afs-base/path-trans is used by dir-entry, abs-acyclic,
afs-base/afs-cons-dir-nlink is used by make-abs-fold-work, fid-ino-entry, dir-entry, dir-empty, abs-unfold, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
afs-base/afs-cons-file-nlink is used by refine-fsync, recovery, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-write, refine-read, refine-close, refine-open, refine-rmdir,
afs-base/afs-cons-in-next is used by path-in-last, dir-entry, refine-unlink, refine-link, refine-create, refine-rmdir,
afs-base/afs-cons-links-empty is used by refine-unlink, refine-close, refine-rmdir,
afs-base/afs-cons-nlink0-notin is used by refine-writemeta, refine-readmeta, refine-truncate,
afs-base/afs-cons-notfile is used by py-prefix, px, pw, pr, path-in-eq, path-in, file-fid, fid-ino-entry, fid-ino, dir-entry, abs-acyclic, recovery, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
afs-base/afs-cons-pagesize is used by refine-truncate,
afs-base/afs-cons-root-dir is used by file-fid, abs-acyclic, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
afs-base/afs-cons-root-notfile is used by recovery, refine-readmeta,
afs-base/at-upto is used by refine-truncate,
afs-base/dir-empty is used by make-abs-fold-work, refine-readmeta, refine-unlink, refine-rmdir,
afs-base/expath-eps is used by refine-create,
afs-base/expath-one is used by path-in-last, refine-link, refine-create, refine-mkdir,
afs-base/expath-split-given is used by path-in-last, refine-link, refine-create, refine-mkdir,
afs-base/getinode is used by refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-read, refine-close, refine-open, refine-create, refine-rmdir, refine-mkdir,
afs-base/in-upto is used by refine-truncate,
afs-base/isexpath is used by py-strong, py-prefix, py, px-prefix, px-parent, px, pw, pr, path-in-last, path-in, ispath-target, fid-ino-entry, fid-ino, dir-entry, dir-empty, abs-unfold, abs-acyclic, refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
afs-base/links is used by refine-readmeta,
afs-base/links-delsame-mod-subdirs is used by refine-rmdir,
afs-base/links-modmeta-write2 is used by refine-rmdir,
afs-base/links-nonempty is used by refine-unlink, refine-link, refine-rmdir,
afs-base/meta-dir is used by refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
afs-base/meta-file is used by refine-fsync, refine-writemeta, refine-readmeta, refine-truncate, refine-open,
afs-base/meta-path is used by py-strong, py-pw, py-last, py, pw, pr, refine-link,
afs-base/path-here is used by py-strong, abs-acyclic, refine-writemeta, refine-readmeta, refine-link,
afs-base/path-in-dirs is used by py-prefix, px-parent, px, pw, pr, dir-entry, abs-acyclic, refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
afs-base/path-in-end is used by refine-writemeta, refine-readmeta,
afs-base/path-inj is used by refine-readmeta,
afs-base/path-lookup is used by refine-readmeta,
afs-base/path-one is used by dir-entry, abs-acyclic, refine-readmeta,
afs-base/path-prefix is used by py-prefix, px,
afs-base/subdirs is used by refine-readmeta,
afs-base/valid-dentry-03 is used by refine-link,
afs-base/valid-dentry-with-parent is used by refine-unlink, refine-link, refine-rmdir,
afs-base/valid-dir-ino is used by refine-readdir, refine-writemeta, refine-unlink, refine-link, refine-close, refine-create, refine-rmdir, refine-mkdir,
afs-base/valid-file-ino is used by refine-fsync, refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-close, refine-rmdir,
afs-base/valid-ino is used by py-strong, make-abs-fold-work, abs-acyclic, refine-fsync, recovery, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-read, refine-close, refine-open, refine-create, refine-rmdir, refine-mkdir,
afs-base/valid-negdentry is used by refine-link, refine-create, refine-mkdir,
afs-base/valid-pagesize is used by make-abs-fold-work, refine-readmeta, refine-unlink, refine-rmdir,
afs-base/valid-parent-ino is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,

Used from specification afs-stream

afs-stream/getbyte is used by refine-truncate,
afs-stream/getpage is used by refine-truncate,
afs-stream/stream-at is used by refine-truncate,
afs-stream/stream-size is used by refine-readmeta, refine-truncate, refine-seek, refine-write, refine-read,

Used from specification heap-sep

heap-sep/dir-heap/Imp is used by refine-mkdir,
heap-sep/dir-heap/Imp-refl is used by abs-fold-new,
heap-sep/dir-heap/Imp2 is used by abs-fold-new-p,
heap-sep/dir-heap/and is used by fid-ino-entry, dir-empty, abs-unfold, abs-fold-new-p, abs-fold-del-p, abs-fold-del, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta,
heap-sep/dir-heap/and-ass is used by fid-ino-entry, dir-empty, abs-unfold-entry-p, abs-unfold, abs-fold-new-p, abs-fold-del-p, abs-fold-del, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create,
heap-sep/dir-heap/and-com is used by fid-ino-entry, dir-empty, abs-unfold-entry-p, abs-unfold, abs-fold-new-p, abs-fold-del-p, abs-fold-del, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create,
heap-sep/dir-heap/emp is used by abs-acyclic,
heap-sep/dir-heap/emp-sep is used by py-prefix, px, pw, pr, path-in-eq, path-in, dir-entry, abs-fold-new-p, abs-fold-new, abs-fold-del-p, abs-fold-del, abs-acyclic, refine-writemeta, refine-readmeta,
heap-sep/dir-heap/false-and is used by dir-empty, abs-acyclic,
heap-sep/dir-heap/false-rev is used by dir-empty,
heap-sep/dir-heap/false-sep is used by dir-empty, abs-acyclic,
heap-sep/dir-heap/falseH is used by dir-empty, abs-acyclic,
heap-sep/dir-heap/prop is used by fid-ino-entry, dir-empty, abs-unfold, abs-fold-new-p, abs-fold-del-p, abs-fold-del, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta,
heap-sep/dir-heap/prop-shift is used by fid-ino-entry, dir-empty, abs-unfold, abs-fold-new-p, abs-fold-del-p, abs-fold-del, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta,
heap-sep/dir-heap/sep-ass is used by py-prefix, px, pw, pr, path-in-eq, path-in, fid-ino-entry, fid-ino, dir-entry, dir-empty, abs-unfold-entry-p, abs-unfold, abs-fold-new-p, abs-fold-new, abs-fold-del-p, abs-fold-del, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
heap-sep/dir-heap/sep-com is used by py-prefix, px, pw, pr, path-in-eq, path-in, fid-ino-entry, fid-ino, dir-entry, dir-empty, abs-unfold-entry-p, abs-unfold, abs-fold-new-p, abs-fold-new, abs-fold-del-p, abs-fold-del, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
heap-sep/dir-heap/true-and is used by fid-ino-entry, dir-empty, abs-unfold-entry-p, abs-fold-new-p, abs-fold-del-p, abs-acyclic, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create,
heap-sep/dir-heap/true-rev is used by fid-ino-entry, dir-empty, abs-unfold-entry-p, abs-fold-new-p, abs-fold-del-p, abs-acyclic, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create,

Used from specification file-mode

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

Used from specification directory-tree-base

directory-tree-base/At-same is used by refine-readmeta,
directory-tree-base/In-insert is used by refine-readmeta,
directory-tree-base/disj is used by abs-acyclic,
directory-tree-base/dnode-inj is used by abs-acyclic,
directory-tree-base/fnode-inj is used by fid-ino-entry, fid-ino, refine-readmeta,

Used from specification directory-tree

directory-tree/fnode-elim-strong is used by refine-readmeta,
directory-tree/split-at is used by fid-ino-entry, dir-empty, abs-acyclic, refine-readmeta, refine-rmdir,
directory-tree/split-del is used by abs-fold-del-p,
directory-tree/split-put is used by abs-fold-new-p,
directory-tree/del-here is used by abs-fold-del-p,
directory-tree/dnode-elim is used by fid-ino-entry, dir-empty, abs-unfold, abs-acyclic, refine-readdir, refine-readmeta, refine-unlink, refine-link, refine-rmdir,
directory-tree/entries is used by refine-writemeta, refine-rmdir,
directory-tree/fnode-elim is used by refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-open,
directory-tree/isdnode is used by fid-ino-entry, dir-empty, abs-unfold, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-rmdir, refine-mkdir,
directory-tree/isfnode is used by refine-readmeta, refine-link,
directory-tree/nil-at is used by py-strong, px-parent, abs-fold-new-p, abs-fold-del-p, abs-acyclic, refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
directory-tree/nil-in is used by abs-fold-new-p, abs-fold-del-p, refine-writemeta, refine-mkdir,
directory-tree/nil-put is used by abs-fold-new-p, abs-fold-del-p, refine-writemeta, refine-mkdir,
directory-tree/notdir-notin is used by abs-fold-new-p, abs-fold-del-p, refine-writemeta, refine-readmeta,
directory-tree/one-at is used by fid-ino-entry, dir-empty, abs-acyclic, refine-readmeta, refine-rmdir,
directory-tree/one-ind is used by refine-readmeta,
directory-tree/put-here is used by abs-fold-new-p,
directory-tree/same-at is used by abs-fold-new-p, abs-fold-del-p, refine-writemeta,
directory-tree/same-in is used by abs-fold-new-p, abs-fold-del-p, refine-writemeta,
directory-tree/setmeta-elim is used by refine-writemeta,
directory-tree/split-in is used by px-parent, path-in-last, abs-fold-new-p, abs-fold-del-p, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-rmdir,
directory-tree/subdirs is used by refine-readmeta,

Used from specification file

file/elim is used by refine-seek, refine-write, refine-read, refine-close,
file/inj is used by refine-read,
file/sel is used by refine-seek, refine-write, refine-read, refine-close,
file/sel-02 is used by refine-seek, refine-write, refine-read,
file/sel-03 is used by refine-seek, refine-write, refine-read,
file/upd-03 is used by refine-seek, refine-write, refine-read,

Used from specification nat

nat/anti is used by refine-truncate, refine-rmdir,
nat/add-01 is used by abs-fold-del-p, abs-fold-del, refine-unlink, refine-rmdir,
nat/elim-pred-c is used by abs-fold-del-p, abs-fold-del, refine-unlink, refine-rmdir,
nat/elim-sub is used by refine-truncate,
nat/eq-01 is used by refine-read,
nat/fle is used by refine-truncate, refine-read,
nat/fle-01 is used by refine-truncate, refine-read,
nat/ge is used by refine-truncate, refine-unlink, refine-rmdir,
nat/le is used by refine-truncate,
nat/le-def is used by refine-truncate, refine-write, refine-read,
nat/le-ls-simp is used by refine-truncate, refine-write, refine-read,
nat/lels is used by refine-truncate,
nat/lels-02 is used by refine-truncate, refine-rmdir,
nat/lels-03 is used by refine-truncate,
nat/lep is used by refine-unlink, refine-read, refine-rmdir,
nat/lep-02 is used by refine-truncate, refine-read,
nat/ler is used by refine-truncate,
nat/let is used by refine-write, refine-read, refine-rmdir,
nat/lez is used by refine-read,
nat/ls-le-simp is used by refine-truncate, refine-read,
nat/not-zero is used by refine-unlink, refine-rmdir,
nat/pred-03 is used by abs-fold-del-p, refine-rmdir,
nat/zero-02 is used by refine-rmdir,

Used from specification min-max

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

Used from specification set-union

set-union/dir-entries/size-eq-ext is used by refine-readmeta,
set-union/alink-set/del-e-02 is used by refine-rmdir,

Used from specification store

store/file-content/At-other is used by refine-truncate,
store/file-content/In-insert is used by refine-truncate,
store/file-data-store/k-Extension is used by recovery,
store/file-content/At-same is used by refine-truncate,
store/dir-entries/At-same is used by abs-fold-new-p, refine-readmeta,
store/dir-entries/Del-empty is used by abs-fold-del-p, abs-fold-del,
store/dir-entries/Del-rec-same is used by abs-fold-new-p,
store/dir-entries/In-empty is used by abs-fold-del-p, abs-fold-del, refine-rmdir,
store/dir-entries/Size-empty is used by dir-empty, abs-fold-del-p, abs-fold-del, refine-unlink, refine-rmdir,
store/dir-entries/Size-insert is used by abs-fold-new-p, refine-readmeta,
store/dir-entries/empty is used by abs-fold-del-p, abs-fold-del, refine-unlink, refine-rmdir,
store/open-files/ins is used by refine-read,
store/directory-tree-inst/insin is used by refine-readmeta,
store/dir-entries/insin is used by abs-fold-new-p, refine-readmeta,
store/dir-entries/neq is used by refine-readmeta,
store/open-files/notmemlookup is used by refine-seek, refine-write, refine-read, refine-close,
store/dir-entries/notmemlookup is used by refine-unlink,
store/dir-entries/size is used by abs-fold-del-p,

Used from specification error-class

error-class/eaccess is used by refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
error-class/ecommit is used by refine-sync, refine-writemeta, refine-seek, initialization,
error-class/enoent is used by refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
error-class/esuccess is used by refine-fsync, recovery, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-read, refine-open, refine-create, refine-rmdir, refine-mkdir,
error-class/not-esuccess is used by refine-fsync, recovery, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-write, refine-read, refine-close, refine-open, refine-create, refine-rmdir, refine-mkdir, initialization,

Used from specification maplet

maplet/dir-heap/at-eq is used by fid-ino-entry, dir-empty, abs-unfold, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
maplet/dir-heap/ex1 is used by fid-ino-entry, fid-ino, dir-empty, abs-unfold, abs-fold-new-p, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta,
maplet/dir-heap/ex1-shift is used by abs-fold-del-p,
maplet/dir-heap/ex2 is used by refine-mkdir, initialization,
maplet/dir-heap/ex2-shift is used by refine-rmdir,
maplet/dir-heap/ex3-shift is used by fid-ino-entry, dir-empty, abs-unfold, abs-fold-new-p, abs-fold-del-p, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta,
maplet/dir-heap/map-in is used by fid-ino-entry, dir-empty, abs-unfold, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
maplet/dir-heap/map-same is used by abs-acyclic,
maplet/dir-heap/mapex-in is used by refine-mkdir,
maplet/dir-heap/maplet-singleton-heap is used by initialization,

Used from specification error

error/disj-29 is used by refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
error/disj-30 is used by refine-seek, refine-write, refine-read, refine-close,
error/disj-31 is used by refine-fsync, refine-readdir, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
error/disj-32 is used by refine-fsync, refine-readdir, refine-truncate, refine-unlink, refine-link, refine-open,
error/disj-33 is used by refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
error/disj-34 is used by refine-link, refine-create, refine-mkdir,
error/disj-55 is used by refine-rmdir,
error/disj-91 is used by refine-sync, refine-writemeta,

Used from specification buffer-inf-conv

buffer-inf-conv/tobuf-at is used by refine-truncate,
buffer-inf-conv/tobuf-size is used by refine-readmeta, refine-truncate, refine-seek, refine-read,
buffer-inf-conv/tostream-inj is used by refine-read,

Used from specification set-basic

set-basic/dir-entries/Extension is used by refine-readdir,
set-basic/alink-set/Size-empty is used by refine-writemeta, refine-readmeta, refine-truncate,
set-basic/dir-heap-refset/ne-01 is used by recovery,
set-basic/pathset/ne-01 is used by refine-readmeta,
set-basic/alink-set/size-zero is used by recovery, refine-unlink, refine-link, refine-close, refine-create, refine-rmdir, refine-mkdir,
set-basic/open-files/size-zero-01 is used by recovery,
set-basic/alink-set/size-zero-01 is used by recovery, refine-unlink, refine-link, refine-close, refine-create, refine-rmdir, refine-mkdir,
set-basic/pathset/size-zero-01 is used by refine-readmeta,
set-basic/alink-set/size-zero-02 is used by refine-close, refine-rmdir,

Used from specification list-last

list-last/path/butlast-def is used by refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
list-last/path/last-def is used by refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
list-last/path/prefix-self is used by py-last, abs-fold-new-p, abs-fold-del-p, refine-writemeta, refine-link,
list-last/path/prefix-trans is used by py-prefix,

Used from specification posix-base

posix-base/crash-exists is used by recovery,
posix-base/fids-cons is used by fid-file, refine-readmeta,
posix-base/ofh-fids is used by of,
posix-base/posix-crash is used by recovery,
posix-base/meta-dir is used by px, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate,

Used from specification file-handle

file-handle/elim is used by refine-write, refine-read,
file-handle/inj is used by refine-write, refine-read,
file-handle/sel-03 is used by refine-seek, refine-read,
file-handle/sel-04 is used by refine-seek, refine-read,
file-handle/sel-05 is used by of, refine-seek, refine-write, refine-read, refine-close,
file-handle/setpos is used by refine-seek, refine-write, refine-read,

Used from specification path-permission

path-permission/posix-permission/pr is used by pr, refine-readdir, refine-readmeta,
path-permission/vfs-permission/pw is used by py-strong, py,
path-permission/posix-permission/pw is used by pw, refine-writemeta, refine-truncate,
path-permission/vfs-permission/px is used by py-prefix, py-last, px, refine-link,
path-permission/posix-permission/px is used by py-prefix, px,
path-permission/vfs-permission/px-parent is used by py-strong, refine-link,
path-permission/posix-permission/px-prefix is used by px-prefix,
path-permission/vfs-permission/py is used by py-strong, py-px-prefix, py,
path-permission/posix-permission/py is used by py-prefix, py,
path-permission/vfs-permission/py-pw is used by py-pw,
path-permission/vfs-permission/px-eps is used by py-strong, refine-link,
path-permission/vfs-permission/px-parent-eps is used by px-parent, refine-fsync, refine-readdir, refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
path-permission/posix-permission/px-parent-eps is used by px-parent,
path-permission/posix-permission/px-parent-last is used by refine-writemeta,
path-permission/posix-permission/px-parent-noneps is used by px-parent, refine-readdir, refine-readmeta, refine-truncate,
path-permission/vfs-permission/px-parent-noneps is used by px-parent, refine-writemeta,
path-permission/vfs-permission/px-prefix is used by py-px-prefix,
path-permission/vfs-permission/px-to-parent is used by py-strong, py, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
path-permission/vfs-permission/py-px is used by py-px,

Used from specification stream

stream/buffer-inf/append-assoc is used by refine-read,
stream/buffer-inf/empty-append is used by refine-read,
stream/buffer-inf/fin-to is used by refine-readmeta, refine-truncate, refine-seek, refine-read,
stream/buffer-inf/from-zero is used by refine-read,
stream/buffer-inf/get-to is used by refine-truncate,
stream/buffer-inf/size-to is used by refine-readmeta, refine-truncate, refine-seek, refine-read,
stream/buffer-inf/to-zero is used by refine-read,

Used from specification dentry

dentry/sel-03 is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
dentry/sel-04 is used by refine-unlink, refine-link, refine-rmdir,
dentry/sel-05 is used by refine-unlink, refine-link, refine-rmdir,
dentry/test-01 is used by refine-link, refine-create, refine-mkdir,
dentry/test-02 is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,

Used from specification file-id-data

file-id-data/elim is used by refine-readmeta,
file-id-data/inj is used by of, refine-readmeta,
file-id-data/sel is used by refine-link, refine-create,

Used from specification abstract-dir

abstract-dir/elim is used by path-in-last, dir-empty, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
abstract-dir/inj is used by abs-acyclic, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
abstract-dir/sel-03 is used by make-abs-fold-work, fid-ino-entry, dir-empty, abs-unfold, abs-fold-new-p, abs-fold-del-p, refine-readdir, refine-writemeta, refine-readmeta, refine-rmdir, refine-mkdir,
abstract-dir/sel-04 is used by fid-ino-entry, dir-empty, abs-unfold, abs-fold-new-p, abs-fold-del-p, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
abstract-dir/sel-05 is used by refine-writemeta, refine-rmdir,
abstract-dir/sel-08 is used by make-abs-fold-work, refine-writemeta, refine-rmdir, refine-mkdir,
abstract-dir/sel-09 is used by make-abs-fold-work, fid-ino-entry, dir-entry, dir-empty, abs-unfold, abs-fold-new-p, abs-fold-del-p, refine-readdir, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
abstract-dir/upd-03 is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
abstract-dir/upd-04 is used by refine-writemeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
abstract-dir/upd-05 is used by refine-rmdir,
abstract-dir/upd-08 is used by refine-rmdir, refine-mkdir,
abstract-dir/upd-09 is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
abstract-dir/updsel-13 is used by refine-unlink, refine-link, refine-rmdir,
abstract-dir/updsel-20 is used by refine-rmdir,
abstract-dir/updsel-24 is used by refine-rmdir,

Used from specification page

page/emptypage-at is used by refine-truncate,
page/page-size is used by refine-truncate,

Used from specification buffer-option

buffer-option/test-03 is used by refine-truncate,

Used from specification posix-pre

posix-pre/pre-fsync-esuccess is used by refine-fsync,
posix-pre/pre-link-enoent is used by refine-link,
posix-pre/pre-link-esuccess is used by refine-link,
posix-pre/pre-mkdir-esuccess is used by refine-mkdir,
posix-pre/pre-rmdir-enoent is used by refine-rmdir,
posix-pre/pre-unlink-enoent is used by refine-unlink,
posix-pre/pre-close-ebadfd is used by refine-close,
posix-pre/pre-close-elowlevel is used by refine-close,
posix-pre/pre-close-esuccess is used by refine-close,
posix-pre/pre-create-eaccess is used by refine-create,
posix-pre/pre-create-eexists is used by refine-create,
posix-pre/pre-create-elowlevel is used by refine-create,
posix-pre/pre-create-enoent is used by refine-create,
posix-pre/pre-create-enotdir is used by refine-create,
posix-pre/pre-create-esuccess is used by refine-create,
posix-pre/pre-fsync-eaccess is used by refine-fsync,
posix-pre/pre-fsync-eisdir is used by refine-fsync,
posix-pre/pre-fsync-elowlevel is used by refine-fsync,
posix-pre/pre-fsync-enoent is used by refine-fsync,
posix-pre/pre-link-eaccess is used by refine-link,
posix-pre/pre-link-eexists is used by refine-link,
posix-pre/pre-link-eisdir is used by refine-link,
posix-pre/pre-link-elowlevel is used by refine-link,
posix-pre/pre-link-enotdir is used by refine-link,
posix-pre/pre-mkdir-eaccess is used by refine-mkdir,
posix-pre/pre-mkdir-eexists is used by refine-mkdir,
posix-pre/pre-mkdir-elowlevel is used by refine-mkdir,
posix-pre/pre-mkdir-enotdir is used by refine-mkdir,
posix-pre/pre-mkdir-enotent is used by refine-mkdir,
posix-pre/pre-open-eaccess is used by refine-open,
posix-pre/pre-open-eisdir is used by refine-open,
posix-pre/pre-open-elowlevel is used by refine-open,
posix-pre/pre-open-enoent is used by refine-open,
posix-pre/pre-open-esuccess is used by refine-open,
posix-pre/pre-read-ebadfd is used by refine-read,
posix-pre/pre-read-elowlevel is used by refine-read,
posix-pre/pre-read-esuccess is used by refine-read,
posix-pre/pre-readdir-eaccess is used by refine-readdir,
posix-pre/pre-readdir-elowlevel is used by refine-readdir,
posix-pre/pre-readdir-enoent is used by refine-readdir,
posix-pre/pre-readdir-enotdir is used by refine-readdir,
posix-pre/pre-readdir-esuccess is used by refine-readdir,
posix-pre/pre-readmeta-eaccess is used by refine-readmeta,
posix-pre/pre-readmeta-elowlevel is used by refine-readmeta,
posix-pre/pre-readmeta-enoent is used by refine-readmeta,
posix-pre/pre-readmeta-esuccess is used by refine-readmeta,
posix-pre/pre-rmdir-eaccess is used by refine-rmdir,
posix-pre/pre-rmdir-elowlevel is used by refine-rmdir,
posix-pre/pre-rmdir-enotdir is used by refine-rmdir,
posix-pre/pre-rmdir-enotempty is used by refine-rmdir,
posix-pre/pre-rmdir-esuccess is used by refine-rmdir,
posix-pre/pre-seek-ebadfd is used by refine-seek,
posix-pre/pre-seek-elowlevel is used by refine-seek,
posix-pre/pre-seek-esuccess is used by refine-seek,
posix-pre/pre-truncate-eaccess is used by refine-truncate,
posix-pre/pre-truncate-eisdir is used by refine-truncate,
posix-pre/pre-truncate-elowlevel is used by refine-truncate,
posix-pre/pre-truncate-enoent is used by refine-truncate,
posix-pre/pre-truncate-esuccess is used by refine-truncate,
posix-pre/pre-unlink-eaccess is used by refine-unlink,
posix-pre/pre-unlink-eisdir is used by refine-unlink,
posix-pre/pre-unlink-elowlevel is used by refine-unlink,
posix-pre/pre-unlink-enotdir is used by refine-unlink,
posix-pre/pre-unlink-esuccess is used by refine-unlink,
posix-pre/pre-write-ebadfd is used by refine-write,
posix-pre/pre-write-elowlevel is used by refine-write,
posix-pre/pre-write-esuccess is used by refine-write,
posix-pre/pre-writemeta-eaccess is used by refine-writemeta,
posix-pre/pre-writemeta-elowlevel is used by refine-writemeta,
posix-pre/pre-writemeta-enoent is used by refine-writemeta,
posix-pre/pre-writemeta-esuccess is used by refine-writemeta,

Used from specification vfs-contracts

vfs-contracts/read-inv is used by refine-read,
vfs-contracts/read-inv-strong is used by refine-read,
vfs-contracts/read-loop-err is used by refine-read,
vfs-contracts/read-loop-inv is used by refine-read,
vfs-contracts/write-prepost-partial is used by refine-write,
vfs-contracts/read-inv-post is used by refine-read,

Used from specification list

list/path/Last is used by dir-entry, abs-acyclic, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
list/path/Nil is used by refine-link,
list/path/a is used by px-parent, path-in-last, dir-entry, abs-fold-new-p, abs-fold-del-p, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
list/path/app-03 is used by refine-readmeta,
list/path/e is used by abs-fold-new-p, abs-fold-del-p, refine-writemeta, refine-readmeta,
list/path/e-02 is used by px-parent, dir-entry, abs-fold-new-p, abs-fold-del-p, refine-writemeta, refine-readmeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
list/path/in-15 is used by refine-create,
list/path/in-17 is used by refine-create,
list/path/in-append is used by refine-create,

Used from specification nat-inf

nat-inf/add-assoc is used by refine-truncate,
nat-inf/add-comm is used by refine-truncate,
nat-inf/add-fin is used by refine-truncate,
nat-inf/disj is used by refine-truncate, refine-write,
nat-inf/less-fin is used by refine-truncate,
nat-inf/less-inf1 is used by refine-readmeta, refine-truncate, refine-seek, refine-read,
nat-inf/less-inf2 is used by refine-write, refine-read,
nat-inf/ls-natinf-to-nat-1-2 is used by refine-truncate,
nat-inf/prime-add-fin is used by refine-truncate,
nat-inf/sel is used by refine-readmeta, refine-truncate, refine-seek, refine-read,

Used from specification vfs-abs

vfs-abs/abs-delorphans is used by recovery,
vfs-abs/abs-dir-h is used by path-in, dir-entry, abs-acyclic,
vfs-abs/abs-dnode is used by dir-empty, abs-unfold, abs-fold-new-p, abs-fold-del-p, refine-readdir, refine-writemeta, refine-readmeta,
vfs-abs/abs-files-at is used by recovery,
vfs-abs/abs-files-cong is used by refine-write,
vfs-abs/abs-has-rootpath is used by refine-readmeta,
vfs-abs/abs-is-dnode is used by fid-ino-entry, dir-empty, abs-unfold, abs-acyclic, refine-readmeta,
vfs-abs/abs-meta-h is used by py-prefix, px, pw, pr,
vfs-abs/abs-nlinks-h is used by file-fid, refine-unlink,
vfs-abs/abs-path-h is used by path-in-eq, path-in,
vfs-abs/abs-paths-eq is used by refine-readmeta,
vfs-abs/abs-rec is used by abs-fold-new-p,
vfs-abs/absc-dnode is used by abs-acyclic,
vfs-abs/absc-drop is used by abs-fold-new-p, abs-fold-del-p, refine-writemeta,
vfs-abs/absc-path is used by abs-acyclic,
vfs-abs/count-entries is used by refine-readmeta,
vfs-abs/counttheshit is used by refine-readmeta,
vfs-abs/entries-recdel is used by fid-ino-entry, dir-empty, abs-unfold-entry-p, abs-acyclic, refine-readmeta, refine-unlink,
vfs-abs/entries-unfold is used by refine-readmeta,
vfs-abs/path-unfold is used by fid-ino-entry, fid-ino, dir-empty, abs-unfold, abs-fold-new-p, abs-fold-del-p, abs-acyclic, refine-readdir, refine-writemeta, refine-readmeta,
vfs-abs/abs-dnode-emp is used by refine-rmdir, refine-mkdir, initialization,
vfs-abs/abs-empty is used by dir-empty,
vfs-abs/abs-files-at is used by recovery, refine-writemeta, refine-readmeta, refine-truncate, refine-seek, refine-write, refine-read,
vfs-abs/abs-files-del is used by refine-unlink, refine-close,
vfs-abs/abs-files-emp is used by initialization,
vfs-abs/abs-files-in is used by fid-file, recovery, refine-writemeta, refine-readmeta, refine-truncate, refine-seek, refine-write, refine-read, refine-create,
vfs-abs/abs-files-new is used by refine-create,
vfs-abs/abs-files-put is used by refine-writemeta, refine-truncate, refine-write,
vfs-abs/abs-files-put-nlink is used by refine-unlink, refine-link,
vfs-abs/abs-fnode is used by abs-acyclic, refine-readmeta, refine-link, refine-create,
vfs-abs/abs-is-file is used by fid-ino-entry, fid-ino, abs-acyclic, refine-readmeta, refine-unlink,
vfs-abs/abs-of-at is used by of, refine-seek, refine-write, refine-read, refine-close,
vfs-abs/abs-of-del is used by refine-close,
vfs-abs/abs-of-emp is used by recovery, initialization,
vfs-abs/abs-of-in is used by of, refine-seek, refine-write, refine-read, refine-close, refine-open,
vfs-abs/abs-of-put is used by refine-seek, refine-write, refine-read, refine-open,
vfs-abs/absc-emp is used by abs-fold-new-p, abs-fold-del-p, abs-acyclic, refine-writemeta,
vfs-abs/absc-path is used by fid-ino-entry, fid-ino, dir-empty, abs-unfold, refine-readdir, refine-readmeta,
vfs-abs/entries-del is used by abs-fold-new-p,
vfs-abs/entries-dom1 is used by fid-ino-entry, dir-empty, abs-unfold-entry-p, abs-acyclic, refine-readdir, refine-readmeta, refine-unlink, refine-link,
vfs-abs/entries-dom2 is used by fid-ino-entry, dir-empty, abs-fold-new-p, abs-acyclic, refine-readdir, refine-readmeta, refine-unlink, refine-link,
vfs-abs/entries-empty is used by dir-empty, abs-fold-del-p, abs-fold-del,

Used from specification heap

heap/file-heap/ext is used by files-del-eq,
heap/file-heap/at-del is used by files-del-eq, refine-unlink,
heap/file-heap/at-diffs is used by recovery,
heap/dir-heap/at-write is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
heap/file-heap/at-write is used by files-del-eq, refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-write, refine-rmdir,
heap/dir-heap/del-notin is used by refine-unlink,
heap/file-heap/in-alloc is used by refine-create,
heap/file-heap/in-del is used by files-del-eq, refine-unlink,
heap/file-heap/in-diffs is used by recovery,
heap/dir-heap/in-emp is used by abs-acyclic,
heap/file-heap/in-write is used by files-del-eq, refine-truncate, refine-unlink, refine-link, refine-write, refine-create,
heap/dir-heap/in-write is used by refine-unlink, refine-link, refine-create, refine-rmdir,
heap/dir-heap/nonnull is used by refine-mkdir,
heap/dir-heap/overwrite is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
heap/file-heap/overwrite is used by refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-rmdir,
heap/dir-heap/overwrite-split is used by refine-rmdir,
heap/dir-heap/write-again is used by refine-rmdir, refine-mkdir,
heap/file-heap/write-del is used by files-del-eq, refine-unlink,

Used from specification separation

separation/dir-heap/eq is used by refine-unlink, refine-create, refine-rmdir,
separation/dir-heap/alloc is used by refine-mkdir,
separation/dir-heap/alloc-rw is used by refine-mkdir,
separation/dir-heap/assign-known is used by refine-writemeta, refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
separation/dir-heap/assign-new-other is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
separation/dir-heap/assign-unknown is used by refine-mkdir,
separation/dir-heap/collapse-assigns is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
separation/dir-heap/eq-cong-injl is used by refine-mkdir,
separation/dir-heap/eq-cong-injr is used by refine-unlink,
separation/dir-heap/eq-other is used by refine-unlink,
separation/dir-heap/free-known is used by refine-rmdir,

Used from specification nat-mult

nat-mult/modeq is used by refine-truncate,
nat-mult/modeq-01 is used by refine-truncate,
nat-mult/modls is used by refine-truncate,
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 refine-unlink, refine-close, refine-rmdir,
afs-pre/pre-iget is used by refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-read, refine-close, refine-open, refine-create, refine-rmdir, refine-mkdir,
afs-pre/pre-link is used by refine-link,
afs-pre/pre-lookup is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
afs-pre/pre-mkdir is used by refine-mkdir,
afs-pre/pre-readdir is used by refine-readdir,
afs-pre/pre-rmdir is used by refine-rmdir,
afs-pre/pre-truncate is used by refine-truncate,
afs-pre/pre-unlink is used by refine-unlink,
afs-pre/pre-write-inode is used by refine-writemeta,
afs-pre/valid-dir-inode is used by refine-writemeta, refine-unlink, refine-link, refine-close, refine-create, refine-rmdir, refine-mkdir,
afs-pre/valid-file-inode is used by refine-fsync, refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-close, refine-rmdir,
afs-pre/valid-wb-inode is used by refine-writemeta, refine-unlink, refine-close, refine-rmdir,

Used from specification inode

inode/elim is used by refine-writemeta, refine-readmeta, refine-rmdir,
inode/inj is used by refine-writemeta, refine-readmeta, refine-rmdir,
inode/sel-01 is used by refine-fsync, refine-readdir, refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-read, refine-close, refine-create, refine-rmdir, refine-mkdir,
inode/sel-02 is used by refine-fsync, refine-readdir, refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-open, refine-create, refine-rmdir, refine-mkdir,
inode/sel-03 is used by refine-fsync, refine-readdir, refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-read, refine-close, refine-open, refine-create, refine-rmdir, refine-mkdir,
inode/sel-04 is used by refine-fsync, refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-close, refine-create, refine-rmdir, refine-mkdir,
inode/sel-10 is used by refine-fsync, refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-close, refine-create, refine-rmdir, refine-mkdir,
inode/sel-11 is used by refine-writemeta, refine-truncate, refine-unlink, refine-link, refine-seek, refine-read, refine-create, refine-rmdir, refine-mkdir,
inode/upd-02 is used by refine-writemeta,
inode/upd-11 is used by refine-truncate,

Used from specification oelem

oelem/nat-set/irreflexivity is used by refine-truncate, refine-open,
oelem/nat-set/ls-le is used by refine-truncate,
oelem/nat-set/transitivity is used by refine-truncate,

Used from specification path

path/parent-elim is used by px-parent, abs-fold-new-p, abs-fold-del-p, refine-writemeta, refine-readmeta,

Used from specification oset

oset/nat-set/Greater is used by refine-open,
oset/nat-set/ls-emptyset is used by recovery,
oset/nat-set/ls-rm is used by refine-close,

Used from specification seekflag

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

Used from specification file-data

file-data/elim is used by refine-write, refine-read,
file-data/inj is used by refine-write, refine-read,
file-data/sel-01 is used by refine-writemeta, refine-readmeta, refine-truncate, refine-seek, refine-write, refine-read,
file-data/sel-02 is used by refine-writemeta, refine-readmeta, refine-truncate, refine-write,
file-data/setcontent is used by refine-truncate, refine-write,
file-data/setmeta is used by refine-writemeta,

Used from specification nat-div

nat-div/div-elim is used by refine-truncate,
nat-div/mod-eq is used by refine-truncate,
nat-div/mod-le-02 is used by refine-truncate,
nat-div/mod-mult is used by refine-truncate,
nat-div/mult is used by refine-truncate,
nat-div/zero-01 is used by refine-truncate,

Used from specification directory-tree-fids

directory-tree-fids/fids-path is used by refine-readmeta,

Used from specification posix-links

posix-links/in-plinks is used by refine-readmeta,
posix-links/plinks-fids is used by refine-readmeta,

Used from specification vfs-asm

vfs-asm/inv-close is used by refine-close,
vfs-asm/inv-create is used by refine-create,
vfs-asm/inv-fsync is used by refine-fsync,
vfs-asm/inv-fsyncdir is used by refine-fsyncdir,
vfs-asm/inv-link is used by refine-link,
vfs-asm/inv-mkdir is used by refine-mkdir,
vfs-asm/inv-open is used by refine-open,
vfs-asm/inv-read is used by refine-read,
vfs-asm/inv-readdir is used by refine-readdir,
vfs-asm/inv-readmeta is used by refine-readmeta,
vfs-asm/inv-recover is used by recovery,
vfs-asm/inv-rmdir is used by refine-rmdir,
vfs-asm/inv-truncate is used by refine-truncate,
vfs-asm/inv-unlink is used by refine-unlink,
vfs-asm/px-last is used by py-strong, refine-link,
vfs-asm/walk-prepost is used by refine-fsync, refine-readdir, refine-writemeta, refine-readmeta, refine-truncate, refine-open,
vfs-asm/walk-prepost-parent is used by refine-unlink, refine-link, refine-create, refine-rmdir, refine-mkdir,
vfs-asm/write-term is used by refine-write,

Used from specification array-copy

array-copy/buffer/at-fill-h is used by refine-truncate,

Used from specification posix-asm

posix-asm/inv-unlink is used by refine-unlink,

Used from specification array

array/buffer/Extension is used by refine-truncate,