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

Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	string	f	string → nat
# .	buffer-inf	f	buffer-inf → natinf
# .	dir-entries	f	dir-entries → nat
# .	buffer-inf	f	datalist → nat
# .	dir-entries	f	stringset → nat
# .	alink-set	f	alink-set → nat
# .	dir-heap	f	nat-set → nat
# .	path	f	path → nat
# .	dir-heap	f	dir-heap → nat
# .	file-heap	f	file-heap → nat
# .	buffer	f	buffer → nat
# .	file-content	f	file-content → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	buffer-inf	f	data → datalist
. '	string	f	char → string
. '	path	f	string → path
. * .	nat-mult	f	nat × nat → nat
. * .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. * .	file-heap	f	(file-heap → bool) × (file-heap → bool) → file-heap → bool
. + .	nat-basic	f	nat × nat → nat
. + .	buffer-inf	f	buffer-inf × buffer-inf → buffer-inf
. + .	string	f	char × string → string
. + .	buffer-inf	f	data × buffer-inf → buffer-inf
. + .	string	f	string × string → string
. + .	nat-inf	f	natinf × natinf → natinf
. + .	string	f	string × char → string
. + .	buffer	f	buffer × buffer → buffer
. + .	buffer-inf	f	datalist × data → datalist
. + .	path	f	string × path → path
. + .	buffer-inf	f	datalist × datalist → datalist
. + .	path	f	path × path → path
. + .	buffer-inf	f	data × datalist → datalist
. + .	path	f	path × string → path
. ++ .	buffer-inf	f	datalist × data → datalist
. ++ .	string	f	string × char → string
. ++ .	alink-set	f	alink-set × alink → alink-set
. ++ .	dir-entries	f	stringset × string → stringset
. ++ .	path	f	path × string → path
. ++ .	dir-heap	f	nat-set × nat → nat-set
. ++ .	file-heap	f	file-heap × nat → file-heap
. ++ .	dir-heap	f	dir-heap × nat → dir-heap
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. +2 .	path	f	string × string → path
. +2 .	buffer-inf	f	data × data → datalist
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -* .	file-heap	f	(file-heap → bool) × (file-heap → bool) → file-heap → bool
. -* .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. -- .	dir-entries	f	dir-entries × string → dir-entries
. -- .	alink-set	f	alink-set × alink → alink-set
. -- .	dir-entries	f	stringset × string → stringset
. -- .	dir-heap	f	nat-set × nat → nat-set
. -- .	file-heap	f	file-heap × nat → file-heap
. -- .	dir-heap	f	dir-heap × nat → dir-heap
. -- .	file-content	f	file-content × nat → file-content
. -> .	file-heap	f	(file-heap → bool) × (file-heap → bool) → file-heap → bool
. -> .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. -⊗ .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. -⊗ .	file-heap	f	(file-heap → bool) × (file-heap → bool) → file-heap → bool
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -1l .	buffer-inf	f	datalist × data → datalist
. -1l .	path	f	path × string → path
. -l .	string	f	string × char → string
. -l .	buffer-inf	f	datalist × data → datalist
. -l .	path	f	path × string → path
. -p .	string	f	string × nat → string
. -p .	path	f	path × nat → path
. -p .	buffer-inf	f	datalist × nat → datalist
. .buf	buffer-inf-conv	f	buffer-inf → buffer
. .butlast	buffer-inf	pf	datalist → datalist with λ dx. dx ≠ []
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .char1	string	pf	string → char with λ str. str ≠ ""
. .content	abstract-file	f	abstract-file → file-content
. .content:= .	abstract-file	f	abstract-file × file-content → abstract-file
. .dentry?	dentry	p	dentry
. .directory	inode	p	inode
. .directory:= .	inode	f	inode × bool → inode
. .entries	abstract-dir	f	abstract-dir → dir-entries
. .entries:= .	abstract-dir	f	abstract-dir × dir-entries → abstract-dir
. .f	buffer-inf	pf	buffer-inf → nat → data with λ σ0. λ m. ∃ nf0. σ0 = ⌜nf0⌝
. .head	buffer-inf	pf	datalist → data with λ dx. dx ≠ []
. .head	path	pf	path → string with λ p. p ≠ ε
. .ino	inode	f	inode → nat
. .ino	dentry	pf	dentry → nat with λ dent. dent.dentry?
. .ino:= .	dentry	pf	dentry × nat → dentry with λ dent, m. dent.dentry?
. .ino:= .	inode	f	inode × nat → inode
. .l	buffer-inf	pf	buffer-inf → datalist with λ σ0. finp(σ0)
. .last	string	pf	string → char with λ str. str ≠ ""
. .last	buffer-inf	pf	datalist → data with λ dx. dx ≠ []
. .last	path	pf	path → string with λ p. p ≠ ε
. .meta	abstract-dir	f	abstract-dir → metadata
. .meta	abstract-file	f	abstract-file → metadata
. .meta	inode	f	inode → metadata
. .meta:= .	inode	f	inode × metadata → inode
. .meta:= .	abstract-dir	f	abstract-dir × metadata → abstract-dir
. .meta:= .	abstract-file	f	abstract-file × metadata → abstract-file
. .n	nat-inf	pf	natinf → nat with λ n∞. n∞ ≠ ∞
. .name	alink	f	alink → string
. .name	dentry	f	dentry → string
. .name:= .	dentry	f	dentry × string → dentry
. .negdentry?	dentry	p	dentry
. .nlink	abstract-dir	f	abstract-dir → nat
. .nlink	abstract-file	f	abstract-file → nat
. .nlink	inode	f	inode → nat
. .nlink:= .	inode	f	inode × nat → inode
. .nlink:= .	abstract-dir	f	abstract-dir × nat → abstract-dir
. .nlink:= .	abstract-file	f	abstract-file × nat → abstract-file
. .nsubdirs	abstract-dir	f	abstract-dir → nat
. .nsubdirs	inode	f	inode → nat
. .nsubdirs:= .	inode	f	inode × nat → inode
. .nsubdirs:= .	abstract-dir	f	abstract-dir × nat → abstract-dir
. .pino	alink	f	alink → nat
. .rstring	string	pf	string → string with λ str. str ≠ ""
. .size	abstract-dir	f	abstract-dir → nat
. .size	inode	f	inode → nat
. .size	abstract-file	f	abstract-file → nat
. .size:= .	abstract-dir	f	abstract-dir × nat → abstract-dir
. .size:= .	abstract-file	f	abstract-file × nat → abstract-file
. .size:= .	inode	f	inode × nat → inode
. .stream	afs-stream	f	file-content → buffer-inf
. .tail	buffer-inf	pf	datalist → datalist with λ dx. dx ≠ []
. .tail	path	pf	path → path with λ p. p ≠ ε
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. < .	nat-inf	p	natinf × natinf
. < .	path	p	path × path
. < .	buffer-inf	p	datalist × datalist
. => .	dir-heap	f	nat × abstract-dir → dir-heap → bool
. => .	file-heap	f	nat × abstract-file → file-heap → bool
. =>ad	dir-heap	f	nat → dir-heap → bool
. =>ad?	dir-heap	f	nat → dir-heap → bool
. =>af	file-heap	f	nat → file-heap → bool
. =>af?	file-heap	f	nat → file-heap → bool
. > .	nat	p	nat × nat
. [ . ]	buffer-inf	pf	buffer-inf × nat × data → buffer-inf with λ σ, n, d. finp(σ) → ⌜n⌝ < # σ
. [ . ]	dir-entries	f	dir-entries × string × nat → dir-entries
. [ . ]	buffer-inf	pf	buffer-inf × nat → data with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. [ . ]	buffer-inf	pf	datalist × nat × data → datalist with λ dx, n, d. n < # dx
. [ . ]	buffer-inf	pf	datalist × nat → data with λ dx, n. n < # dx
. [ . ]	path	pf	path × nat × string → path with λ p, n, str. n < # p
. [ . ]	dir-heap	f	dir-heap × nat → abstract-dir
. [ . ]	path	pf	path × nat → string with λ p, n. n < # p
. [ . ]	dir-heap	f	dir-heap × nat × abstract-dir → dir-heap
. [ . ]	file-content	pf	file-content × nat → buffer with λ content, n. n ∈ content
. [ . ]	file-content	f	file-content × nat × buffer → file-content
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	file-heap	f	file-heap × nat → abstract-file
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. [ . ]	file-heap	f	file-heap × nat × abstract-file → file-heap
. [ . ]	dir-entries	pf	dir-entries × string → nat with λ entries, str. str ∈ entries
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. \ .	dir-entries	f	stringset × stringset → stringset
. \ .	dir-entries	f	dir-entries × stringset → dir-entries
. \ .	alink-set	f	alink-set × alink-set → alink-set
. \ .	file-heap	f	file-heap × file-heap → file-heap
. \ .	dir-heap	f	nat-set × nat-set → nat-set
. \ .	file-heap	f	file-heap × nat-set → file-heap
. \ .	dir-heap	f	dir-heap × nat-set → dir-heap
. \ .	dir-heap	f	dir-heap × dir-heap → dir-heap
. \| .	dir-entries	f	dir-entries × stringset → dir-entries
. ~ .	afs-stream	p	file-heap × file-heap
. ∈ .	string	p	char × string
. ∈ .	buffer-inf	p	data × datalist
. ∈ .	dir-entries	p	string × dir-entries
. ∈ .	alink-set	p	alink × alink-set
. ∈ .	dir-entries	p	string × stringset
. ∈ .	path	p	string × path
. ∈ .	dir-entries	p	nat × dir-entries
. ∈ .	file-heap	p	nat × file-heap
. ∈ .	dir-heap	p	nat × nat-set
. ∈ .	file-content	p	nat × file-content
. ∈ .	dir-heap	p	nat × dir-heap
. ∈ .	buffer	p	data × buffer
. ∩ .	dir-entries	f	stringset × stringset → stringset
. ∩ .	alink-set	f	alink-set × alink-set → alink-set
. ∩ .	dir-heap	f	nat-set × nat-set → nat-set
. ∪ .	dir-entries	f	stringset × stringset → stringset
. ∪ .	dir-heap	f	nat-set × nat-set → nat-set
. ∪ .	dir-heap	f	dir-heap × dir-heap → dir-heap
. ∪ .	alink-set	f	alink-set × alink-set → alink-set
. ∪ .	file-heap	f	file-heap × file-heap → file-heap
. ≡ .	file-heap	p	file-heap × file-heap
. ≡ .	dir-heap	p	dir-heap × dir-heap
. ≤ .	buffer-inf	p	buffer-inf × buffer-inf
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	alink-set	p	alink-set × alink-set
. ⊆ .	dir-entries	p	dir-entries × dir-entries
. ⊆ .	file-heap	p	(file-heap → bool) × (file-heap → bool)
. ⊆ .	dir-entries	p	stringset × stringset
. ⊆ .	file-heap	p	file-heap × file-heap
. ⊆ .	dir-heap	p	nat-set × nat-set
. ⊆ .	file-content	p	file-content × file-content
. ⊆ .	dir-heap	p	dir-heap × dir-heap
. ⊆ .	dir-heap	p	(dir-heap → bool) × (dir-heap → bool)
. ⊑ .	buffer-inf	p	datalist × datalist
. ⊑ .	string	p	string × string
. ⊑ .	path	p	path × path
. ⊒ .	buffer-inf	p	datalist × datalist
. ⊒ .	string	p	string × string
. ⊒ .	path	p	path × path
. ⊕ .	dir-entries	f	dir-entries × dir-entries → dir-entries
. ⊗ .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. ⊗ .	file-heap	f	(file-heap → bool) × (file-heap → bool) → file-heap → bool
. ⊥ .	file-heap	p	file-heap × file-heap
. ⊥ .	dir-heap	p	dir-heap × dir-heap
. and .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. and .	file-heap	f	(file-heap → bool) × (file-heap → bool) → file-heap → bool
. from .	buffer-inf	pf	datalist × nat → datalist with λ dx, n. n ≤ # dx
. from .	buffer-inf	pf	buffer-inf × nat → buffer-inf with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. from .	buffer-inf	f	(nat → data) × nat → nat → data
. or .	dir-heap	f	(dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
. or .	file-heap	f	(file-heap → bool) × (file-heap → bool) → file-heap → bool
. to .	buffer-inf	pf	datalist × nat → datalist with λ dx, n. n ≤ # dx
. to .	buffer-inf	f	(nat → data) × nat → datalist
. to .	buffer-inf	pf	buffer-inf × nat → buffer-inf with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to∞ .	buffer-inf	pf	buffer-inf × natinf → buffer-inf with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
. upto .	afs-base	f	file-content × nat → file-content
[]	buffer-inf	c	datalist
[]	buffer-inf	c	buffer-inf
_∃ .	file-heap	f	(abstract-file → file-heap → bool) → file-heap → bool
_∃ .	dir-heap	f	(nat → dir-heap → bool) → dir-heap → bool
_∃ .	file-heap	f	(nat × nat → file-heap → bool) → file-heap → bool
_∃ .	dir-heap	f	(nat × nat → dir-heap → bool) → dir-heap → bool
_∃ .	file-heap	f	(nat → file-heap → bool) → file-heap → bool
_∃ .	dir-heap	f	(abstract-dir → dir-heap → bool) → dir-heap → bool
{ . }	alink-set	f	alink → alink-set
{ . }	dir-entries	f	string → stringset
{ . }	file-heap	f	file-heap → file-heap → bool
{ . }	dir-heap	f	nat → nat-set
{ . }	dir-heap	f	dir-heap → dir-heap → bool
ε	path	c	path
σ	buffer-inf	v	buffer-inf
σ⊥	buffer-inf-conv	c	buffer-inf
σ1	buffer-inf	v	buffer-inf
σ2	buffer-inf	v	buffer-inf
∅	dir-entries	c	dir-entries
∅	dir-entries	c	stringset
∅	dir-heap	c	nat-set
∅	dir-heap	c	dir-heap
∅	file-content	c	file-content
∅	file-heap	c	file-heap
∅	alink-set	c	alink-set
∞	nat-inf	c	natinf
⊏	string	p	string × string
⌜ . ⌝	dir-heap	f	bool → dir-heap → bool
⌜ . ⌝	buffer-inf-conv	f	buffer → buffer-inf
⌜ . ⌝	file-heap	f	bool → file-heap → bool
⌜ . ⌝	nat-inf	f	nat → natinf
⌜ . ⌝	buffer-inf	f	datalist → buffer-inf
⌜ . ⌝	buffer-inf	f	(nat → data) → buffer-inf
D	dir-heap	v	dir-heap → bool
D0	dir-heap	v	dir-heap → bool
D1	dir-heap	v	dir-heap → bool
D2	dir-heap	v	dir-heap → bool
F	file-heap	v	file-heap → bool
F0	file-heap	v	file-heap → bool
F1	file-heap	v	file-heap → bool
F2	file-heap	v	file-heap → bool
ROOT_INO	root-ino	c	nat
True	separation	p	bool
VFS_PAGE_SIZE	page	c	nat
abstract-dir	abstract-dir	s
abstract-file	abstract-file	s
ad	abstract-dir	v	abstract-dir
ad0	dir-heap	v	abstract-dir
ad1	dir-heap	v	abstract-dir
adD	dir-heap	v	abstract-dir → dir-heap → bool
adF	file-heap	v	abstract-file → file-heap → bool
af	abstract-file	v	abstract-file
af0	file-heap	v	abstract-file
af1	file-heap	v	abstract-file
afs-cons	afs-base	p	dir-heap × file-heap
alink	alink	s
alink	alink	v	alink
alink-set	alink-set	s
alink0	alink-set	v	alink
alink1	alink-set	v	alink
boolvar	inode	v	bool
boolvar0	inode	v	bool
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
buffer-inf	buffer-inf	s
butlastn	buffer-inf	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
butlastn	path	pf	nat × path → path with λ n, p. n ≤ # p
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
bv	heap-sep	v	bool
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
cmp	buffer	pp	buffer × data × nat × nat with λ buf, d, m, n. m + n ≤ # buf
cmp	buffer	pp	buffer × nat × buffer × nat × nat with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
content	file-content	v	file-content
content0	file-content	v	file-content
content1	file-content	v	file-content
content2	file-content	v	file-content
copy	buffer	pf	buffer × nat × buffer × nat × nat → buffer with λ buf, m, buf0, m0, n. m + n ≤ # buf ∧ m0 + n ≤ # buf0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
datalist	buffer-inf	s
dent	dentry	v	dentry
dentry	dentry	s
dir-empty	afs-base	p	nat × dir-heap × file-heap
dir-entries	dir-entries	s
dir-heap	dir-heap	s
dirs	dir-heap	v	dir-heap
dirs0	dir-heap	v	dir-heap
dirs1	dir-heap	v	dir-heap
dirs2	dir-heap	v	dir-heap
disj	string	p	string × string
disj	buffer-inf	p	datalist × datalist
disj	path	p	path × path
dom .	dir-entries	f	dir-entries → stringset
dups	string	p	string
dups	path	p	path
dups	buffer-inf	p	datalist
dx	buffer-inf	v	datalist
dx0	buffer-inf	v	datalist
dx1	buffer-inf	v	datalist
dx3	buffer-inf	v	datalist
dx7	buffer-inf	v	datalist
emp	dir-heap	p	dir-heap
emp	file-heap	p	file-heap
empty	buffer	c	data
entries	dir-entries	v	dir-entries
entries0	dir-entries	v	dir-entries
entries1	dir-entries	v	dir-entries
entries2	dir-entries	v	dir-entries
false	dir-heap	p	dir-heap
false	file-heap	p	file-heap
file-content	file-content	s
file-heap	file-heap	s
files	file-heap	v	file-heap
files0	file-heap	v	file-heap
files1	file-heap	v	file-heap
files2	file-heap	v	file-heap
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	buffer	f	buffer × data → buffer
fillfirst	string	f	nat × char × string → string
fillfirst	path	f	nat × string × path → path
fillfirst	buffer-inf	f	nat × data × datalist → datalist
finp	buffer-inf	p	buffer-inf
firstn	buffer-inf	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
firstn	path	pf	nat × path → path with λ n, p. n ≤ # p
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
frome	string	f	string × char → string
frome	path	f	path × string → path
frome	buffer-inf	f	datalist × data → datalist
getbyte	afs-stream	f	nat × file-content → data
getinode	afs-base	f	nat × dir-heap × file-heap → inode
getpage	afs-stream	f	nat × file-content → buffer
hd	buffer-inf	pf	buffer-inf → data with λ σ. σ ≠ []
id○	buffer	p	buffer × buffer × nat
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
ino	file-heap	v	nat
ino0	file-heap	v	nat
ino1	file-heap	v	nat
ino2	dir-entries	v	nat
inode	inode	s
inode	inode	v	inode
ispath	afs-base	p	path × nat × nat × dir-heap × file-heap
ispath	afs-base	p	path × nat × dir-heap × file-heap
ite	dir-heap	f	bool × (dir-heap → bool) × (dir-heap → bool) → dir-heap → bool
ite	file-heap	f	bool × (file-heap → bool) × (file-heap → bool) → file-heap → bool
lastn	buffer-inf	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
lastn	path	pf	nat × path → path with λ n, p. n ≤ # p
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
links	afs-base	f	nat × dir-heap → alink-set
lookup	afs-base	f	path × nat × dir-heap × file-heap → nat
ls	alink-set	v	alink-set
ls0	alink-set	v	alink-set
ls1	alink-set	v	alink-set
ls2	alink-set	v	alink-set
m	nat-basic	v	nat
m0	inode	v	nat
m1	inode	v	nat
m2	inode	v	nat
m3	inode	v	nat
m4	inode	v	nat
m5	inode	v	nat
m6	inode	v	nat
max	min-max	f	nat × nat → nat
md	metadata	v	metadata
md0	inode	v	metadata
meta	afs-base	f	path × nat × dir-heap × file-heap → metadata
metadata	metadata	s
min	nat-inf	f	natinf × natinf → natinf
min	min-max	f	nat × nat → nat
mkbuf	buffer	f	nat → buffer
mkdentry	dentry	f	string × nat → dentry
mkdir	abstract-dir	f	nat × metadata × nat × nat × dir-entries → abstract-dir
mkempbuf	buffer	f	nat → buffer
mkfile	abstract-file	f	nat × metadata × nat × file-content → abstract-file
mkinode	inode	f	nat × metadata × bool × nat × nat × nat → inode
mklink	alink	f	nat × string → alink
mklist	string	f	char × nat → string
mklist	buffer-inf	f	data × nat → datalist
mkpath	path	f	string × nat → path
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n∞	nat-inf	v	natinf
n∞0	nat-inf	v	natinf
n0	nat-basic	v	nat
n1	nat-basic	v	nat
n2	file-content	v	nat
n3	file-content	v	nat
n4	file-content	v	nat
nD	dir-heap	v	nat → dir-heap → bool
nF	file-heap	v	nat → file-heap → bool
name	afs-base	v	string
nat	nat-basic	s
nat-set	dir-heap	s
natinf	nat-inf	s
negdentry	dentry	f	string → dentry
nf	buffer-inf	v	nat → data
nf0	buffer-inf	v	nat → data
nnD	dir-heap	v	nat × nat → dir-heap → bool
nnF	file-heap	v	nat × nat → file-heap → bool
not .	dir-heap	f	(dir-heap → bool) → dir-heap → bool
not .	file-heap	f	(file-heap → bool) → file-heap → bool
ns	dir-heap	v	nat-set
ns0	dir-heap	v	nat-set
ns1	dir-heap	v	nat-set
ns2	dir-heap	v	nat-set
orphans	afs-base	f	dir-heap × file-heap → nat-set
p	path	v	path
p'	path	v	path
p_ino	afs-base	v	nat
p0	path	v	path
p1	path	v	path
parent	path	pf	path → path with λ p. p ≠ ε
path	path	s
pos	string	f	char × string → nat
pos	path	f	string × path → nat
pos	buffer-inf	f	data × datalist → nat
precise	file-heap	p	(file-heap → bool)
precise	dir-heap	p	(dir-heap → bool)
q	path	v	path
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
restn	buffer-inf	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
restn	path	pf	nat × path → path with λ n, p. n ≤ # p
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
rev	string	f	string → string
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	buffer	f	buffer → buffer
rev	buffer-inf	f	datalist → datalist
rev	path	f	path → path
rmdup	string	f	string → string
rmdup	buffer-inf	f	datalist → datalist
rmdup	path	f	path → path
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
str	string	v	string
str0	string	v	string
str1	string	v	string
str2	string	v	string
str3	string	v	string
string	string	s
strings	dir-entries	v	stringset
strings0	dir-entries	v	stringset
strings1	dir-entries	v	stringset
strings2	dir-entries	v	stringset
stringset	dir-entries	s
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
subdirs	afs-base	f	nat × dir-heap → stringset
sublist	buffer-inf	pf	nat × nat × datalist → datalist with λ n, m, dx. n + m ≤ # dx
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
sublist	path	pf	nat × nat × path → path with λ n, m, p. n + m ≤ # p
tl	buffer-inf	pf	buffer-inf → buffer-inf with λ σ. σ ≠ []
true	dir-heap	p	dir-heap
true	file-heap	p	file-heap
valid-content	afs-base	p	nat × file-heap
valid-dentry	afs-base	p	dentry × dir-heap × file-heap
valid-dentry	afs-base	p	nat × dentry × dir-heap × file-heap
valid-dir-ino	afs-base	p	nat × dir-heap × file-heap
valid-file-ino	afs-base	p	nat × dir-heap × file-heap
valid-ino	afs-base	p	nat × dir-heap × file-heap
valid-inode	afs-base	p	inode × dir-heap × file-heap
valid-negdentry	afs-base	p	nat × dentry × dir-heap × file-heap
valid-pagesize	afs-base	p	nat × nat × file-heap
valid-parent-ino	afs-base	p	nat × dir-heap × file-heap
zero	buffer	c	data
zeropage	page	c	buffer