[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
# .	zheap	f	zheap → nat
# .	zbranch-array	f	zbranch-array → nat
# .	refset	f	refset → nat
# .	address-list-set	f	address-list → nat
# .	address-set-array	f	address-set-array → nat
# .	address-list-set	f	address-set → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	string	f	char → string
. '	address-list-set	f	address → address-list
. * .	zheap	f	(zheap → bool) × (zheap → bool) → zheap → bool
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	string	f	char × string → string
. + .	address-list-set	f	address-list × address → address-list
. + .	string	f	string × string → string
. + .	address-list-set	f	address-list × address-list → address-list
. + .	string	f	string × char → string
. + .	address-list-set	f	address × address-list → address-list
. ++ .	zheap	f	zheap × ref → zheap
. ++ .	string	f	string × char → string
. ++ .	refset	f	refset × ref → refset
. ++ .	address-list-set	f	address-list × address → address-list
. ++ .	address-list-set	f	address-set × address → address-set
. +1	nat-basic	f	nat → nat
. +2 .	string	f	char × char → string
. +2 .	address-list-set	f	address × address → address-list
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -* .	zheap	f	(zheap → bool) × (zheap → bool) → zheap → bool
. -- .	address-list-set	f	address-set × address → address-set
. -- .	refset	f	refset × ref → refset
. -- .	zheap	f	zheap × ref → zheap
. -> .	zheap	f	(zheap → bool) × (zheap → bool) → zheap → bool
. -⊗ .	zheap	f	(zheap → bool) × (zheap → bool) → zheap → bool
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -1l .	address-list-set	f	address-list × address → address-list
. -l .	string	f	string × char → string
. -l .	address-list-set	f	address-list × address → address-list
. -p .	string	f	string × nat → string
. -p .	address-list-set	f	address-list × nat → address-list
. .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	address-list-set	pf	address-list → address-list with λ ax. ax ≠ []
. .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
. .head	address-list-set	pf	address-list → address with λ ax. ax ≠ []
. .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:= .	branch	f	branch × key → branch
. .key:= .	zbranch	f	zbranch × key → zbranch
. .last	address-list-set	pf	address-list → address with λ ax. ax ≠ []
. .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 ≠ ""
. .tail	address-list-set	pf	address-list → address-list with λ ax. ax ≠ []
. .toSet	address-list-set	f	address-list → address-set
. .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
. < .	address-list-set	p	address-list × address-list
. < .	nat-basic	p	nat × nat
. < .	key-order-def	p	key × key
. < .	string-less	p	string × string
. < .	string-less	p	char × char
. => .	zheap	f	ref × znode → zheap → bool
. =>?	zheap	f	ref → zheap → bool
. =>_	zheap	f	ref → zheap → bool
. > .	nat	p	nat × nat
. [ . ]	address-set-array	pf	address-set-array × nat × address-set → address-set-array with λ asar, n, a0. n < # asar
. [ . ]	address-set-array	pf	address-set-array × nat → address-set with λ asar, n. n < # asar
. [ . ]	address-list-set	pf	address-list × nat × address → address-list with λ ax, n, adr. n < # ax
. [ . ]	address-list-set	pf	address-list × nat → address with λ ax, n. n < # ax
. [ . ]	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
. [ . ]	zheap	f	zheap × ref → znode
. [ . ]	zheap	f	zheap × ref × znode → zheap
. \ .	address-list-set	f	address-set × address-set → address-set
. \ .	refset	f	refset × refset → refset
. \ .	zheap	f	zheap × zheap → zheap
. \ .	zheap	f	zheap × refset → zheap
. ∈ .	zheap	p	ref × zheap
. ∈ .	string	p	char × string
. ∈ .	refset	p	ref × refset
. ∈ .	zbranch-array	p	zbranch × zbranch-array
. ∈ .	address-set-array	p	address-set × address-set-array
. ∈ .	address-list-set	p	address × address-list
. ∈ .	address-list-set	p	address × address-set
. ∩ .	address-list-set	f	address-set × address-set → address-set
. ∩ .	refset	f	refset × refset → refset
. ∪ .	address-list-set	f	address-set × address-set → address-set
. ∪ .	refset	f	refset × refset → refset
. ∪ .	zheap	f	zheap × zheap → zheap
. ≡ .	zheap	p	zheap × zheap
. ≤ .	nat	p	nat × nat
. ≤ .	zbranch-array-sorted	p	key × key
. ≥ .	nat	p	nat × nat
. ⊆ .	zheap	p	(zheap → bool) × (zheap → bool)
. ⊆ .	zheap	p	zheap × zheap
. ⊆ .	address-list-set	p	address-set × address-set
. ⊆ .	refset	p	refset × refset
. ⊑ .	string	p	string × string
. ⊑ .	address-list-set	p	address-list × address-list
. ⊒ .	address-list-set	p	address-list × address-list
. ⊒ .	string	p	string × string
. ⊗ .	zheap	f	(zheap → bool) × (zheap → bool) → zheap → bool
. ⊗_ ( . )	zheap	f	(nat → zheap → bool) × nat × nat → zheap → bool
. ⊥ .	zheap	p	zheap × zheap
. and .	zheap	f	(zheap → bool) × (zheap → bool) → zheap → bool
. or .	zheap	f	(zheap → bool) × (zheap → bool) → zheap → bool
[]	address-list-set	c	address-list
_∃ .	zheap	f	(address-set-array → zheap → bool) → zheap → bool
_∃ .	zheap	f	(znode → zheap → bool) → zheap → bool
_∃ .	zheap	f	(ref → zheap → bool) → zheap → bool
_∃ .	zheap	f	(ref × ref → zheap → bool) → zheap → bool
{ . }	address-list-set	f	address → address-set
{ . }	zheap	f	zheap → zheap → bool
{ . }	refset	f	ref → refset
∅	address-list-set	c	address-set
∅	zheap	c	zheap
∅	refset	c	refset
⊏	string	p	string × string
⌜ . ⌝	zheap	f	bool → zheap → bool
ADR_DUMMY	constants	c	address
BRANCH_SIZE	constants	c	nat
Boolvar	key-order	v	bool,flexible
MIN_SIZE	constants	c	nat
P	zheap	v	zheap → bool
P0	zheap	v	zheap → bool
P1	zheap	v	zheap → bool
P2	zheap	v	zheap → bool
Pa	zheap	v	address-set-array → zheap → bool
True	separation	p	bool
a	address-set-array	v	address-set
address	address	s
address-list	address-list-set	s
address-set	address-list-set	s
address-set-array	address-set-array	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
as	address-list-set	v	address-set
as0	address-list-set	v	address-set
as1	address-list-set	v	address-set
as2	address-list-set	v	address-set
asar	address-set-array	v	address-set-array
asar0	address-set-array	v	address-set-array
asar1	address-set-array	v	address-set-array
asar2	address-set-array	v	address-set-array
ax	address-list-set	v	address-list
ax0	address-list-set	v	address-list
ax1	address-list-set	v	address-list
ay	address-list-set	v	address-list
az	address-list-set	v	address-list
b	address-set-array	v	address-set
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	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
bv	heap-sep	v	bool
c	address-set-array	v	address-set
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	address-set-array	pp	address-set-array × address-set × nat × nat with λ asar, a0, m, n. m + n ≤ # asar
cmp	address-set-array	pp	address-set-array × nat × address-set-array × nat × nat with λ asar, m, asar0, m0, n. m + n ≤ # asar ∧ m0 + n ≤ # asar0
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
copy	address-set-array	pf	address-set-array × nat × address-set-array × nat × nat → address-set-array with λ asar, m, asar0, m0, n. m + n ≤ # asar ∧ m0 + n ≤ # asar0
datakey	key	f	nat × nat → key
dentrykey	key	f	nat × string → key
disj	address-list-set	p	address-list × address-list
disj	string	p	string × string
dropn	address-list-set	f	nat × address-list → address-list
dups	string	p	string
dups	address-list-set	p	address-list
emp	zheap	p	zheap
false	zheap	p	zheap
fill	address-set-array	pf	address-set-array × address-set × nat × nat → address-set-array with λ asar, a0, n, m. n + m ≤ # asar
fill	zbranch-array	f	zbranch-array × zbranch → zbranch-array
fill	zbranch-array	pf	zbranch-array × zbranch × nat × nat → zbranch-array with λ zbrar, zbr, n, m. n + m ≤ # zbrar
fill	address-set-array	f	address-set-array × address-set → address-set-array
fillfirst	string	f	nat × char × string → string
fillfirst	address-list-set	f	nat × address × address-list → address-list
firstn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
frome	string	f	string × char → string
frome	address-list-set	f	address-list × address → address-list
id○	address-set-array	p	address-set-array × address-set-array × nat
id○	zbranch-array	p	zbranch-array × zbranch-array × nat
idrange	address-set-array	pp	address-set-array × nat × nat with λ asar, m, n. m + n ≤ # asar
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
ite	zheap	f	bool × (zheap → bool) × (zheap → bool) → zheap → bool
key	key	s
key	key	v	key
key0	zbranch	v	key
key1	key-order	v	key
lastn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
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
mkarray	address-set-array	f	nat → address-set-array
mkbranch	branch	f	key × address → branch
mkentry	branch	f	key × address → branch
mklist	string	f	char × nat → string
mklist	address-list-set	f	address × nat → address-list
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
nP	zheap	v	nat → zheap → bool
nat	nat-basic	s
not .	zheap	f	(zheap → bool) → zheap → bool
null	ref	c	ref
oP	zheap	v	znode → zheap → bool
pos	string	f	char × string → nat
pos	address-list-set	f	address × address-list → nat
precise	zheap	p	(zheap → bool)
prefixn	address-list-set	f	nat × address-list → address-list
r	ref	v	ref
r0	ref	v	ref
r1	ref	v	ref
rP	zheap	v	ref → zheap → bool
ref	ref	s
refset	refset	s
restn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
rev	address-set-array	pf	address-set-array × nat → address-set-array with λ asar, n. n ≤ # asar
rev	zbranch-array	pf	zbranch-array × nat → zbranch-array with λ zbrar, n. n ≤ # zbrar
rev	address-set-array	f	address-set-array → address-set-array
rev	string	f	string → string
rev	address-list-set	f	address-list → address-list
rev	zbranch-array	f	zbranch-array → zbranch-array
rmdup	string	f	string → string
rmdup	address-list-set	f	address-list → address-list
rrP	zheap	v	ref × ref → zheap → bool
rs	refset	v	refset
rs0	refset	v	refset
rs1	refset	v	refset
rs2	refset	v	refset
slice	address-list-set	f	nat × nat × address-list → address-list
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	address-set-array	pf	address-set-array × nat × nat → address-set-array with λ asar, m, n. m + n ≤ # asar
subarray	zbranch-array	pf	zbranch-array × nat × nat → zbranch-array with λ zbrar, m, n. m + n ≤ # zbrar
sublist	address-list-set	pf	nat × nat × address-list → address-list with λ n, m, ax. n + m ≤ # ax
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
true	zheap	p	zheap
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
zh	zheap	v	zheap
zh0	zheap	v	zheap
zh1	zheap	v	zheap
zh2	zheap	v	zheap
zheap	zheap	s
znd	znode	v	znode
znd0	zheap	v	znode
znd1	zheap	v	znode
znode	znode	s