[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
# .	zbranch-array	f	zbranch-array → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	string	f	char → string
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	string	f	char × string → string
. + .	string	f	string × char → string
. + .	string	f	string × string → string
. ++ .	string	f	string × char → string
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -l .	string	f	string × char → string
. -p .	string	f	string × nat → string
. .adr	zbranch	f	zbranch → address
. .adr	branch	f	branch → address
. .adr:= .	branch	f	branch × address → branch
. .adr:= .	zbranch	f	zbranch × address → zbranch
. .branch?	branch	p	branch
. .branch?	zbranch	p	zbranch
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .char1	string	pf	string → char with λ str. str ≠ ""
. .child	zbranch	pf	zbranch → ref with λ zbr. zbr.branch?
. .child:= .	zbranch	pf	zbranch × ref → zbranch with λ zbr, r. zbr.branch?
. .data?	key	p	key
. .dentry?	key	p	key
. .dirty	znode	p	znode
. .dirty:= .	znode	f	znode × bool → znode
. .entry?	branch	p	branch
. .entry?	zbranch	p	zbranch
. .ino	key	f	key → nat
. .ino:= .	key	f	key × nat → key
. .inode?	key	p	key
. .key	zbranch	f	zbranch → key
. .key	branch	f	branch → key
. .key:= .	zbranch	f	zbranch × key → zbranch
. .key:= .	branch	f	branch × key → branch
. .last	string	pf	string → char with λ str. str ≠ ""
. .leaf	znode	p	znode
. .leaf:= .	znode	f	znode × bool → znode
. .name	key	pf	key → string with λ key. key.dentry?
. .name:= .	key	pf	key × string → key with λ key, str. key.dentry?
. .parent	znode	f	znode → ref
. .parent:= .	znode	f	znode × ref → znode
. .part	key	pf	key → nat with λ key. key.data?
. .part:= .	key	pf	key × nat → key with λ key, m. key.data?
. .rstring	string	pf	string → string with λ str. str ≠ ""
. .usedsize	znode	f	znode → nat
. .usedsize:= .	znode	f	znode × nat → znode
. .zbranches	znode	f	znode → zbranch-array
. .zbranches:= .	znode	f	znode × zbranch-array → znode
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. < .	key-order-def	p	key × key
. < .	string-less	p	char × char
. < .	string-less	p	string × string
. > .	nat	p	nat × nat
. [ . ]	zbranch-array	pf	zbranch-array × nat × zbranch → zbranch-array with λ zbrar, n, zbr. n < # zbrar
. [ . ]	zbranch-array	pf	zbranch-array × nat → zbranch with λ zbrar, n. n < # zbrar
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. ∈ .	zbranch-array	p	zbranch × zbranch-array
. ∈ .	string	p	char × string
. ≤ .	nat	p	nat × nat
. ≤ .	zbranch-array-sorted	p	key × key
. ≥ .	nat	p	nat × nat
. ⊑ .	string	p	string × string
. ⊒ .	string	p	string × string
⊏	string	p	string × string
ADR_DUMMY	constants	c	address
BRANCH_SIZE	constants	c	nat
Boolvar	key-order	v	bool,flexible
MIN_SIZE	constants	c	nat
address	address	s
adr	address	v	address
adr0	address	v	address
adr1	address	v	address
adr2	address	v	address
adr3	address	v	address
adr4	address	v	address
adr5	address	v	address
align↑	align	f	nat × nat → nat
align↓	align	f	nat × nat → nat
boolvar	key-order	v	bool
boolvar0	key-order	v	bool
boolvar1	key-order	v	bool
boolvar2	znode	v	bool
br	branch	v	branch
branch	branch	s
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
char	char	s
char	char	v	char
char0	char	v	char
char1	char	v	char
char2	char	v	char
char3	string-less	v	char
cmp	zbranch-array	pp	zbranch-array × zbranch × nat × nat with λ zbrar, zbr, m, n. m + n ≤ # zbrar
cmp	zbranch-array	pp	zbranch-array × nat × zbranch-array × nat × nat with λ zbrar, m, zbrar0, m0, n. m + n ≤ # zbrar ∧ m0 + n ≤ # zbrar0
copy	zbranch-array	pf	zbranch-array × nat × zbranch-array × nat × nat → zbranch-array with λ zbrar, m, zbrar0, m0, n. m + n ≤ # zbrar ∧ m0 + n ≤ # zbrar0
datakey	key	f	nat × nat → key
dentrykey	key	f	nat × string → key
disj	string	p	string × string
dups	string	p	string
fill	zbranch-array	pf	zbranch-array × zbranch × nat × nat → zbranch-array with λ zbrar, zbr, n, m. n + m ≤ # zbrar
fill	zbranch-array	f	zbranch-array × zbranch → zbranch-array
fillfirst	string	f	nat × char × string → string
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
frome	string	f	string × char → string
id○	zbranch-array	p	zbranch-array × zbranch-array × nat
idrange	zbranch-array	pp	zbranch-array × nat × nat with λ zbrar, m, n. m + n ≤ # zbrar
ino	key-order-def	v	nat
inodekey	key	f	nat → key
is-aligned	align	p	nat × nat
key	key	s
key	key	v	key
key0	zbranch	v	key
key1	key-order	v	key
lastn	string	pf	nat × string → string with λ n, str. n ≤ # str
m	nat-basic	v	nat
m0	array-copy	v	nat
m1	key	v	nat
m2	key	v	nat
mkbranch	branch	f	key × address → branch
mkentry	branch	f	key × address → branch
mklist	string	f	char × nat → string
mkzbranch	zbranch	f	key × address × ref → zbranch
mkzbrarray	zbranch-array	f	nat → zbranch-array
mkzentry	zbranch	f	key × address → zbranch
mkznode	znode	f	ref × zbranch-array × bool × bool × nat → znode
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
null	ref	c	ref
pos	string	f	char × string → nat
r	ref	v	ref
r0	ref	v	ref
r1	ref	v	ref
ref	ref	s
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
rev	zbranch-array	pf	zbranch-array × nat → zbranch-array with λ zbrar, n. n ≤ # zbrar
rev	zbranch-array	f	zbranch-array → zbranch-array
rev	string	f	string → string
rmdup	string	f	string → string
sorted	zbranch-array-sorted	p	zbranch-array × nat × nat
sortedchars	string-less	c	string
str	string	v	string
str0	string	v	string
str1	string	v	string
str2	string	v	string
str3	string	v	string
string	string	s
subarray	zbranch-array	pf	zbranch-array × nat × nat → zbranch-array with λ zbrar, m, n. m + n ≤ # zbrar
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
zbr	zbranch	v	zbranch
zbr0	zbranch-array	v	zbranch
zbr1	zbranch-array	v	zbranch
zbranch	zbranch	s
zbranch-array	zbranch-array	s
zbrar	zbranch-array	v	zbranch-array
zbrar0	zbranch-array	v	zbranch-array
zbrar1	zbranch-array	v	zbranch-array
zbrar2	zbranch-array	v	zbranch-array
znd	znode	v	znode
znode	znode	s