[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/min-0 is used by read-loop-inv, read-loop-err, read-inv-rec,
vfs-base/min-less-first is used by read-loop-inv, read-inv-rec,
vfs-base/min-less-second is used by read-inv-rec,
vfs-base/min-less-third is used by read-loop-inv,
vfs-base/of-cons-file is used by write-prepost-partial, write-prepost,
vfs-base/of-cons-notdir is used by write-prepost-partial, write-prepost,

Used from specification nat-basic

nat-basic/a is used by writepage-prepost, write-inv-rec,
nat-basic/addex is used by write-prepost-partial, write-prepost,
nat-basic/a is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-others, write-inv-meta, write-inv-ls, write-inv-in1, write-inv-in0, write-inode-inv, truncate-inv, read-loop-inv, read-inv-rec, read-inv-post,
nat-basic/add-base is used by write-prepost-partial, write-prepost, write-inv-post, write-inode-inv, truncate-inv, read-inv-post,
nat-basic/c is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-others, write-inv-meta, write-inv-ls, write-inv-in1, write-inv-in0, write-inode-inv, truncate-inv, read-loop-inv, read-inv-rec, read-inv-post,
nat-basic/eq-01 is used by write-inv-rec, write-inv-post, write-inode-inv, read-loop-inv,
nat-basic/eq-02 is used by read-loop-inv,
nat-basic/eqs is used by write-inv-rec, truncate-inv, read-inv-rec,
nat-basic/f is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inv-ls, write-inv-in1, write-inv-in0, truncate-inv, read-loop-inv, read-loop-err, read-inv-rec, read-inv-post,
nat-basic/l is used by write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-rec, write-inv-post, read-loop-inv, read-inv-rec,
nat-basic/l-01 is used by write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-rec, write-inv-post, truncate-inv, read-loop-inv, read-inv-rec,
nat-basic/l-02 is used by writepage-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inv-in1, write-inv-in0, read-inv-rec, read-inv-post,
nat-basic/l-05 is used by read-loop-inv,
nat-basic/l-06 is used by read-inv-rec,
nat-basic/l-08 is used by write-inv-post,
nat-basic/lf is used by write-prepost-partial, write-prepost, read-loop-inv,
nat-basic/lf-01 is used by write-inv-rec, write-inv-post, truncate-inv, read-loop-inv, read-inv-rec, read-inv-post,
nat-basic/lf-02 is used by write-prepost-partial, write-prepost, write-inv-rec, truncate-inv, read-loop-inv, read-inv-rec,
nat-basic/ls-02 is used by write-prepost-partial, write-prepost, write-inv-rec,
nat-basic/succ is used by write-prepost-partial, write-prepost, read-loop-inv,
nat-basic/zero is used by truncate-inv,
nat-basic/zero-01 is used by write-prepost-partial, write-prepost, read-inv-post,

Used from specification array-splice

array-splice/buffer/splice-copy is used by write-prepost-partial, write-prepost, write-inv-post,
array-splice/buffer/splice-len is used by write-inv-post,
array-splice/buffer/splice-resize is used by write-inv-post,
array-splice/buffer/resize-at is used by write-inv-post,
array-splice/buffer/resize-len is used by write-inv-post,
array-splice/buffer/splice-0 is used by write-prepost-partial, write-prepost, write-inv-post,

Used from specification abstract-file

abstract-file/elim is used by writepage-afs-cons, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-rec, write-inode-inv, write-block-inv, truncate-inv, read-loop-inv,
abstract-file/inj is used by writepage-afs-cons, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inode-inv, truncate-inv,
abstract-file/sel-01 is used by write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inode-inv, write-block-inv, truncate-inv, read-loop-inv, read-inv-post,
abstract-file/sel-02 is used by write-prepost-partial, write-prepost, truncate-inv,
abstract-file/sel-06 is used by write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inode-inv, truncate-inv, read-loop-inv, read-inv-post,
abstract-file/sel-07 is used by write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inode-inv, truncate-inv,
abstract-file/upd-04 is used by write-prepost, write-inode-inv, truncate-inv,
abstract-file/upd-05 is used by writepage-afs-cons, write-block-inv, truncate-inv,
abstract-file/upd-06 is used by write-prepost, write-inode-inv, truncate-inv,
abstract-file/updsel-01 is used by write-prepost-partial, write-prepost, write-inode-inv,
abstract-file/updsel-07 is used by write-prepost-partial, write-prepost,
abstract-file/updsel-09 is used by write-prepost-partial, write-prepost,
abstract-file/updsel-15 is used by write-prepost-partial, write-prepost,
abstract-file/updsel-16 is used by write-prepost-partial, write-prepost,

Used from specification afs-base

afs-base/afs-cons-nlink0-notin is used by writepage-afs-cons,
afs-base/afs-cons-file-nlink is used by writepage-afs-cons, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inode-inv, truncate-inv, read-loop-inv, read-inv-rec, read-inv-post,
afs-base/afs-cons-notfile is used by writepage-afs-cons, write-inv-strong-rec, write-inode-inv, truncate-inv,
afs-base/afs-cons-pagesize is used by writepage-afs-cons, write-inv-strong-rec, write-inode-inv, truncate-inv,
afs-base/afs-cons-root-dir is used by writepage-afs-cons, write-inv-strong-rec, write-inode-inv,
afs-base/dir-empty is used by writepage-afs-cons, write-inv-strong-rec, write-inode-inv,
afs-base/getinode is used by write-prepost-partial, write-prepost, truncate-inv,
afs-base/valid-dir-ino is used by write-prepost-partial, write-prepost, write-inode-inv,
afs-base/valid-file-ino is used by writepage-afs-cons, write-prepost-partial, write-prepost, write-inode-inv, write-block-inv, truncate-inv, read-loop-err,
afs-base/valid-ino is used by writepage-afs-cons, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inode-inv,
afs-base/valid-pagesize is used by writepage-afs-cons, write-inv-strong-rec, write-inode-inv,

Used from specification afs-stream

afs-stream/at-content-stream is used by truncate-inv,
afs-stream/content-read is used by write-inv-rec, read-inv-rec,
afs-stream/content-trunc is used by truncate-inv,
afs-stream/content-trunc-exact is used by truncate-inv,
afs-stream/content-write is used by write-inv-rec, truncate-inv,
afs-stream/copy-stream-append is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-rec, read-inv-rec,
afs-stream/fill-stream-append is used by truncate-inv,
afs-stream/iso-unfold is used by write-prepost-partial, write-prepost,
afs-stream/afs-cons-getpage-size is used by write-inv-strong-rec, write-inv-rec, read-loop-inv, read-inv-rec,
afs-stream/iso-refl is used by write-prepost-partial, write-prepost, truncate-inv,
afs-stream/iso-sym is used by write-prepost-partial, write-prepost,
afs-stream/stream-at is used by write-inv-post, read-inv-rec, read-inv-post,
afs-stream/stream-size is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
afs-stream/stream-size-from is used by write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
afs-stream/stream-split-lastpage is used by truncate-inv,
afs-stream/zerostream-size is used by write-inv-post, truncate-inv,

Used from specification file

file/elim is used by write-prepost-partial, write-prepost,
file/sel is used by write-prepost,
file/sel-02 is used by write-prepost-partial, write-prepost,
file/sel-03 is used by write-prepost,
file/upd-03 is used by write-prepost-partial, write-prepost,

Used from specification nat

nat/cancel-01 is used by write-prepost-partial, write-prepost, write-inv-rec, truncate-inv,
nat/elim-sub is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-rec, write-inv-post, write-block-inv, truncate-inv, read-loop-inv, read-loop-err, read-inv-rec, read-inv-post,
nat/eq-01 is used by write-inv-rec, write-inv-post, write-inv-ls, truncate-inv, read-inv-rec,
nat/fle is used by write-inv-rec, write-inv-post, truncate-inv, read-loop-inv, read-inv-rec, read-inv-post,
nat/fle-01 is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inv-in1, write-inv-in0, read-loop-inv, read-inv-rec, read-inv-post,
nat/ge is used by write-prepost-partial, write-prepost, write-block-inv, truncate-inv, read-loop-inv, read-loop-err,
nat/le is used by truncate-inv,
nat/le-add is used by write-prepost-partial, write-prepost, truncate-inv,
nat/le-def is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inv-ls, write-inv-in1, write-inv-in0, read-loop-inv, read-inv-rec, read-inv-post,
nat/le-ls-simp is used by write-prepost-partial, write-prepost, write-inv-rec, write-inv-post,
nat/lels is used by write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat/lels-02 is used by read-loop-inv, read-loop-err,
nat/lels-03 is used by truncate-inv, read-loop-inv, read-loop-err, read-inv-rec, read-inv-post,
nat/lep is used by write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-rec, write-inv-post, truncate-inv, read-loop-inv, read-inv-rec, read-inv-post,
nat/lep-02 is used by write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inv-ls, truncate-inv, read-loop-inv, read-inv-rec, read-inv-post,
nat/ler is used by write-prepost-partial, write-prepost, write-inv-rec, truncate-inv, read-inv-rec,
nat/let is used by write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inode-inv, read-inv-post,
nat/lez is used by write-prepost-partial, write-prepost, write-inv-post,
nat/ls-03 is used by write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-meta, write-inv-in1, write-inv-in0, read-loop-inv, read-inv-post,
nat/ls-le-simp is used by write-prepost-partial, write-prepost, write-inv-post, write-inv-ls, read-inv-rec, read-inv-post,
nat/prop-07 is used by truncate-inv,
nat/sub-base is used by write-inode-inv, read-inv-post,
nat/zero is used by write-prepost-partial, write-prepost, truncate-inv,
nat/zero-02 is used by read-loop-inv, read-loop-err,

Used from specification min-max

min-max/max-first-ls is used by write-inv-post,
min-max/max-second-le is used by write-inv-post,
min-max/min-notls1 is used by write-inv-strong-rec,
min-max/min-same is used by truncate-inv,

Used from specification store

store/file-content/At-other is used by writepage-afs-cons,
store/file-content/At-other is used by write-inv-strong-rec,
store/file-content/At-same is used by writepage-afs-cons, write-inv-strong-rec,
store/file-content/in-neq is used by writepage-afs-cons, write-inv-strong-rec,
store/open-files/ins is used by write-prepost-partial, write-prepost,
store/open-files/notmemlookup is used by write-prepost-partial, write-prepost,

Used from specification error-class

error-class/esuccess is used by writepage-prepost, writepage-afs-cons, write-prepost-partial, write-prepost, write-block-inv, truncate-inv, read-loop-inv, read-loop-err,
error-class/not-esuccess is used by writepage-prepost, write-prepost-partial, write-prepost, write-inode-inv, write-block-inv, read-loop-err,

Used from specification buffer-inf-conv

buffer-inf-conv/emptystream-cancel is used by truncate-inv,
buffer-inf-conv/split-prefix-append-to is used by writepage-prepost, write-inv-rec,
buffer-inf-conv/tobuf-rev is used by write-prepost-partial, write-prepost,
buffer-inf-conv/tostream-inj is used by write-prepost-partial, write-prepost,
buffer-inf-conv/at-emptystream is used by write-inv-post, truncate-inv,
buffer-inf-conv/from-emptystream is used by truncate-inv,
buffer-inf-conv/from-to-rest is used by writepage-prepost, read-inv-rec,
buffer-inf-conv/tobuf-at is used by write-inv-post, read-inv-post,
buffer-inf-conv/tobuf-size is used by write-prepost-partial, write-prepost, write-inv-post,
buffer-inf-conv/tostream-at is used by write-inv-post, read-inv-post,
buffer-inf-conv/tostream-size is used by write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, read-inv-rec, read-inv-post,

Used from specification error

error/disj-30 is used by write-prepost-partial, write-prepost,

Used from specification set-basic

set-basic/alink-set/Size-empty is used by writepage-afs-cons,

Used from specification stream

stream/buffer-inf/append-assoc is used by writepage-prepost, write-inv-rec,
stream/buffer-inf/append-from-ge-02 is used by write-inv-rec, truncate-inv, read-inv-rec,
stream/buffer-inf/append-to-ls is used by write-prepost-partial, write-prepost, write-inv-rec, truncate-inv, read-inv-rec,
stream/buffer-inf/extensionality is used by write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
stream/buffer-inf/from-append-tofrom is used by writepage-prepost, write-inv-rec,
stream/buffer-inf/from-from is used by writepage-prepost, write-inv-rec, read-inv-rec,
stream/buffer-inf/get-append-ls is used by write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
stream/buffer-inf/get-from is used by write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
stream/buffer-inf/inf-size-from is used by write-inv-rec, truncate-inv,
stream/buffer-inf/size-to is used by write-prepost-partial, write-prepost,
stream/buffer-inf/swap-from-to is used by write-inv-rec,
stream/buffer-inf/swap-to-from is used by writepage-prepost, write-inv-rec, read-inv-rec,
stream/buffer-inf/swap-to-from-app is used by truncate-inv,
stream/buffer-inf/to-append-add is used by write-prepost-partial, write-prepost, write-inv-rec,
stream/buffer-inf/to-plus-from is used by write-inv-rec,
stream/buffer-inf/to-to-eq is used by write-inv-rec,
stream/buffer-inf/to-to-leq is used by writepage-prepost, write-prepost-partial, write-prepost, read-inv-rec,
stream/buffer-inf/to-to-ls is used by write-prepost-partial, write-prepost,
stream/buffer-inf/append-assoc is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-stream, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
stream/buffer-inf/append-cancel-r-02 is used by truncate-inv,
stream/buffer-inf/append-cut1 is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-rec,
stream/buffer-inf/append-empty is used by write-prepost-partial, write-prepost,
stream/buffer-inf/empty-append is used by write-inv-post, truncate-inv,
stream/buffer-inf/fin-to is used by write-prepost-partial, write-prepost, write-inv-post, read-inv-post,
stream/buffer-inf/from-zero is used by write-prepost-partial, write-prepost, truncate-inv,
stream/buffer-inf/get-append-notls is used by write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
stream/buffer-inf/get-to is used by write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
stream/buffer-inf/inf-size-from is used by writepage-prepost, write-inv-rec,
stream/buffer-inf/less-size-from is used by truncate-inv,
stream/buffer-inf/size-append is used by write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
stream/buffer-inf/size-to is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
stream/buffer-inf/to-plus-from-simp is used by truncate-inv,
stream/buffer-inf/to-to-eq is used by write-prepost-partial, write-prepost, write-inv-rec, truncate-inv, read-inv-rec,
stream/buffer-inf/to-to-ls is used by write-prepost-partial, write-prepost, write-inv-rec, truncate-inv,
stream/buffer-inf/to-zero is used by write-prepost-partial, write-prepost, write-inv-post, truncate-inv,

Used from specification page

page/emptypage-size is used by read-loop-err,
page/page-size is used by write-prepost-partial, write-prepost, write-inv-rec, write-block-inv, truncate-inv, read-loop-inv, read-loop-err, read-inv-rec,

Used from specification abstract-dir

abstract-dir/elim is used by writepage-afs-cons, write-inv-strong-rec, write-inode-inv,

Used from specification buffer-option

buffer-option/ex-01 is used by truncate-inv,
buffer-option/test-01 is used by write-prepost-partial, write-prepost, truncate-inv,
buffer-option/test-03 is used by truncate-inv,

Used from specification array-copy

array-copy/buffer/at-copy is used by write-inv-post,
array-copy/buffer/at-copy is used by read-inv-post,
array-copy/buffer/size-copy is used by writepage-afs-cons, write-inv-strong-rec, write-inv-rec, write-block-inv, read-loop-inv, read-inv-post,
array-copy/buffer/size-fill-h is used by truncate-inv,

Used from specification nat-inf

nat-inf/add-all-inf is used by write-prepost-partial, write-prepost,
nat-inf/add-assoc is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat-inf/add-cancel-01 is used by read-inv-rec,
nat-inf/add-comm is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat-inf/add-fin is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat-inf/add-inf2 is used by write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv,
nat-inf/add-ls-cancel-01 is used by write-inv-rec, truncate-inv, read-inv-rec,
nat-inf/addeqinf-cancel is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat-inf/disj is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat-inf/inf-less is used by write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat-inf/less-fin is used by write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat-inf/less-inf1 is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat-inf/less-inf2 is used by write-inv-post,
nat-inf/ls-lsadd is used by read-inv-rec,
nat-inf/ls-natinf-to-nat-1-2 is used by write-prepost-partial, write-prepost, write-inv-rec, read-inv-rec,
nat-inf/ls-natinf-to-nat-2-1 is used by write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,
nat-inf/ls-natinf-to-nat-2-2 is used by write-inv-rec,
nat-inf/ls-natinf-to-nat-3-1 is used by truncate-inv, read-inv-rec,
nat-inf/prime-add-fin is used by write-prepost-partial, write-prepost, write-inv-rec, truncate-inv, read-inv-rec,
nat-inf/sel is used by write-prepost-partial, write-prepost, write-inv-rec, write-inv-post, truncate-inv, read-inv-rec, read-inv-post,

Used from specification heap

heap/file-heap/at-write is used by writepage-afs-cons, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inode-inv, truncate-inv,
heap/file-heap/del-notin is used by write-inv-in1, write-inv-in0,
heap/file-heap/in-write is used by writepage-afs-cons, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inode-inv, truncate-inv,
heap/file-heap/overwrite is used by write-prepost-partial, write-prepost, write-inode-inv, truncate-inv,
heap/file-heap/write-del is used by write-prepost-partial, write-prepost, write-inv-strong-rec, write-inode-inv, truncate-inv,

Used from specification nat-mult

nat-mult/coef-20 is used by write-inv-rec,
nat-mult/ls is used by truncate-inv,
nat-mult/modls is used by write-inv-rec, truncate-inv,
nat-mult/mult-a is used by writepage-prepost, write-inv-rec, truncate-inv,
nat-mult/mult-c is used by writepage-prepost, write-inv-rec, truncate-inv,
nat-mult/rsucc-02 is used by writepage-prepost, write-inv-rec, truncate-inv,
nat-mult/zero-01 is used by write-inv-rec,

Used from specification oelem

oelem/nat-set/irreflexivity is used by write-inv-rec, truncate-inv, read-loop-inv, read-inv-rec, read-inv-post,
oelem/nat-set/transitivity is used by write-prepost-partial, write-prepost, read-loop-inv,

Used from specification inode

inode/elim is used by writepage-prepost, writepage-afs-cons, write-block-inv, read-loop-inv, read-loop-err,
inode/inj is used by write-prepost-partial, write-prepost, truncate-inv,
inode/sel-01 is used by writepage-prepost, write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-others, write-inv-meta, write-inv-ls, write-inv-in1, write-inv-in0, write-inode-inv, write-block-inv, truncate-inv, read-loop-inv, read-loop-err, read-inv-post,
inode/sel-02 is used by write-prepost-partial, write-prepost, write-inode-inv, truncate-inv,
inode/sel-03 is used by write-prepost-partial, write-prepost, write-inode-inv, truncate-inv,
inode/sel-04 is used by write-prepost-partial, write-prepost, write-inode-inv, truncate-inv,
inode/sel-10 is used by write-prepost-partial, write-prepost, write-inode-inv, truncate-inv,
inode/sel-11 is used by write-prepost-partial, write-prepost, write-inv-strong-rec, write-inv-stream, write-inv-rec, write-inv-post, write-inv-others, write-inv-meta, write-inv-ls, write-inv-in1, write-inv-in0, write-inode-inv, truncate-inv, read-loop-inv, read-inv-post,
inode/upd-11 is used by write-prepost-partial, write-prepost, truncate-inv,

Used from specification afs-pre

afs-pre/pre-iget is used by write-prepost-partial, write-prepost,
afs-pre/pre-readpage is used by read-loop-err,
afs-pre/pre-truncate is used by truncate-inv,
afs-pre/pre-write-inode is used by write-prepost-partial, write-prepost, write-inode-inv,
afs-pre/pre-writepage is used by writepage-afs-cons, write-block-inv,
afs-pre/valid-dir-inode is used by write-prepost-partial, write-prepost, write-inode-inv,
afs-pre/valid-file-inode is used by write-prepost-partial, write-prepost, write-inode-inv, truncate-inv,
afs-pre/valid-wb-inode is used by write-prepost-partial, write-prepost, write-inode-inv,

Used from specification array

array/buffer/Extension is used by write-inv-post, read-inv-post,
array/buffer/Size-mkarray is used by read-loop-err,

Used from specification nat-div

nat-div/div-elim is used by write-inv-rec, truncate-inv, read-inv-rec,
nat-div/mod-le-02 is used by write-block-inv, truncate-inv, read-loop-inv, read-loop-err,

Used from specification vfs-asm

vfs-asm/write-loop-0 is used by write-prepost-partial, write-prepost,
vfs-asm/write-loop-err is used by write-prepost-partial, write-prepost,

Used from specification afs-contracts

afs-contracts/mkfile-stream is used by writepage-prepost,
afs-contracts/mkfile-stream-reduce is used by writepage-prepost,
afs-contracts/readpage-get is used by write-block-inv, read-loop-inv,
afs-contracts/readpage-prepost is used by writepage-prepost,
afs-contracts/truncate-same-iso is used by truncate-inv,
afs-contracts/writepage-prepost is used by writepage-prepost,

Used from specification afs-asm

afs-asm/afs-cons-reduce is used by writepage-afs-cons, write-inv-strong-rec, write-inode-inv,
afs-asm/inv-truncate is used by truncate-inv,