[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
# .	index-store	f	index-address-store → nat
# .	branch-array	f	branch-array → nat
# .	buffer	f	buffer → nat
# .	address-list-set	f	address-list → nat
# .	nat-store	f	nat-set → nat
# .	address-list-set	f	address-set → nat
# .	index-store	f	index-store → nat
# .	index-store	f	index-node-list → nat
# .	laddress-list	f	laddress-list → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	laddress-list	f	laddress → laddress-list
. '	string	f	char → string
. '	index-store	f	index-node → index-node-list
. '	address-list-set	f	address → address-list
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. + .	string	f	char × string → string
. + .	string	f	string × string → string
. + .	laddress-list	f	laddress-list × laddress → laddress-list
. + .	string	f	string × char → string
. + .	laddress-list	f	laddress-list × laddress-list → laddress-list
. + .	address-list-set	f	address × address-list → address-list
. + .	laddress-list	f	laddress × laddress-list → laddress-list
. + .	address-list-set	f	address-list × address-list → address-list
. + .	index-store	f	index-node-list × index-node → index-node-list
. + .	address-list-set	f	address-list × address → address-list
. + .	index-store	f	index-node-list × index-node-list → index-node-list
. + .	index-store	f	index-node × index-node-list → index-node-list
. ++ .	nat-store	f	nat-set × nat → nat-set
. ++ .	string	f	string × char → string
. ++ .	laddress-list	f	laddress-list × laddress → laddress-list
. ++ .	address-list-set	f	address-list × address → address-list
. ++ .	index-store	f	index-node-list × index-node → index-node-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
. +2 .	laddress-list	f	laddress × laddress → laddress-list
. +2 .	index-store	f	index-node × index-node → index-node-list
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	address-list-set	f	address-set × address → address-set
. -- .	index-store	f	index-address-store × address → index-address-store
. -- .	index-store	f	index-store × nat → index-store
. -- .	nat-store	f	nat-set × nat → nat-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	string	f	string × char → string
. -1l .	laddress-list	f	laddress-list × laddress → laddress-list
. -1l .	address-list-set	f	address-list × address → address-list
. -1l .	index-store	f	index-node-list × index-node → index-node-list
. -l .	string	f	string × char → string
. -l .	laddress-list	f	laddress-list × laddress → laddress-list
. -l .	address-list-set	f	address-list × address → address-list
. -l .	index-store	f	index-node-list × index-node → index-node-list
. -p .	string	f	string × nat → string
. -p .	laddress-list	f	laddress-list × nat → laddress-list
. -p .	index-store	f	index-node-list × nat → index-node-list
. -p .	address-list-set	f	address-list × nat → address-list
. .adr	branch	f	branch → address
. .adr:= .	branch	f	branch × address → branch
. .branch?	branch	p	branch
. .branches	indexnode	f	index-node → branch-array
. .branches:= .	indexnode	f	index-node × branch-array → index-node
. .butlast	laddress-list	pf	laddress-list → laddress-list with λ lax. lax ≠ []
. .butlast	string	pf	string → string with λ str. str ≠ ""
. .butlast	index-store	pf	index-node-list → index-node-list with λ indx. indx ≠ []
. .butlast	address-list-set	pf	address-list → address-list with λ ax. ax ≠ []
. .butmax	nat-set	pf	nat-set → nat-set with λ ns. ns ≠ ∅
. .butmin	nat-set	pf	nat-set → nat-set with λ ns. ns ≠ ∅
. .char1	string	pf	string → char with λ str. str ≠ ""
. .data?	key	p	key
. .dentry?	key	p	key
. .entry?	branch	p	branch
. .flashsize	index-store	f	index-node → nat
. .flashsize	index-store	f	index-node-list → nat
. .head	laddress-list	pf	laddress-list → laddress with λ lax. lax ≠ []
. .head	address-list-set	pf	address-list → address with λ ax. ax ≠ []
. .head	index-store	pf	index-node-list → index-node with λ indx. indx ≠ []
. .indlist	index-store	f	index-block → index-node-list
. .indlist:= .	index-store	f	index-block × index-node-list → index-block
. .ino	key	f	key → nat
. .ino:= .	key	f	key × nat → key
. .inode?	key	p	key
. .key	branch	f	branch → key
. .key:= .	branch	f	branch × key → branch
. .ladrlist	index-store	f	index-block → laddress-list
. .ladrlist:= .	index-store	f	index-block × laddress-list → index-block
. .last	laddress-list	pf	laddress-list → laddress with λ lax. lax ≠ []
. .last	index-store	pf	index-node-list → index-node with λ indx. indx ≠ []
. .last	address-list-set	pf	address-list → address with λ ax. ax ≠ []
. .last	string	pf	string → char with λ str. str ≠ ""
. .leaf	indexnode	p	index-node
. .leaf:= .	indexnode	f	index-node × bool → index-node
. .lnum	address-data	f	address → nat
. .lnum:= .	address-data	f	address × nat → address
. .map ( . )	index-store	f	index-address-store × (address × index-node → index-node) → index-address-store
. .map ( . )	index-store	f	index-store × (index-block → index-block) → index-store
. .map ( . )	index-store	f	index-address-store × (index-node → index-node) → index-address-store
. .map ( . )	index-store	f	index-store × (nat × index-block → index-block) → index-store
. .max	nat-set	pf	nat-set → nat with λ ns. ns ≠ ∅
. .min	nat-set	pf	nat-set → nat with λ ns. ns ≠ ∅
. .name	key	pf	key → string with λ key. key.dentry?
. .name:= .	key	pf	key × string → key with λ key, str. key.dentry?
. .off	laddress	f	laddress → nat
. .off:= .	laddress	f	laddress × nat → laddress
. .part	key	pf	key → nat with λ key. key.data?
. .part:= .	key	pf	key × nat → key with λ key, m. key.data?
. .pos	address-data	f	address → nat
. .pos:= .	address-data	f	address × nat → address
. .ref-size	index-store	f	index-block → nat
. .ref-size:= .	index-store	f	index-block × nat → index-block
. .rstring	string	pf	string → string with λ str. str ≠ ""
. .size	laddress	f	laddress → nat
. .size	ablock-store-refsize-cons	f	address-set → nat
. .size	address-data	f	address → nat
. .size:= .	laddress	f	laddress × nat → laddress
. .size:= .	address-data	f	address × nat → address
. .tail	laddress-list	pf	laddress-list → laddress-list with λ lax. lax ≠ []
. .tail	index-store	pf	index-node-list → index-node-list with λ indx. indx ≠ []
. .tail	address-list-set	pf	address-list → address-list with λ ax. ax ≠ []
. .to-adr ( . )	ablock-store-inv	f	laddress-list × nat → address-list
. .toSet	address-list-set	f	address-list → address-set
. .usedsize	indexnode	f	index-node → nat
. .usedsize:= .	indexnode	f	index-node × nat → index-node
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. < .	address-list-set	p	address-list × address-list
. < .	nat-set	p	nat-set × nat
. < .	index-store	p	index-node-list × index-node-list
. < .	nat-set	p	nat × nat-set
. < .	laddress-list	p	laddress-list × laddress-list
. =○refsize .	index-store	p	index-store × index-store
. > .	nat	p	nat × nat
. [ . ]	index-store	pf	index-address-store × address → index-node with λ iast, adr. adr ∈ iast
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. [ . ]	index-store	pf	index-store × nat → index-block with λ istore, n. n ∈ istore
. [ . ]	laddress-list	pf	laddress-list × nat × laddress → laddress-list with λ lax, n, ladr. n < # lax
. [ . ]	laddress-list	pf	laddress-list × nat → laddress with λ lax, n. n < # lax
. [ . ]	index-store	pf	index-node-list × nat × index-node → index-node-list with λ indx, n, ind. n < # indx
. [ . ]	index-store	f	index-store × nat × index-block → index-store
. [ . ]	index-store	pf	index-node-list × nat → index-node with λ indx, n. n < # indx
. [ . ]	index-store	f	index-store × address → index-node
. [ . ]	address-list-set	pf	address-list × nat × address → address-list with λ ax, n, adr. n < # ax
. [ . ]	index-store	f	index-address-store × address × index-node → index-address-store
. [ . ]	address-list-set	pf	address-list × nat → address with λ ax, n. n < # ax
. [ . ]	string	pf	string × nat → char with λ str, n. n < # str
. [ . ]	branch-array	pf	branch-array × nat × branch → branch-array with λ brar, n, br. n < # brar
. [ . ]	string	pf	string × nat × char → string with λ str, n, char. n < # str
. [ . ]	branch-array	pf	branch-array × nat → branch with λ brar, n. n < # brar
. \ .	address-list-set	f	address-set × address-set → address-set
. \ .	nat-store	f	nat-set × nat-set → nat-set
. \ .	index-store	f	index-store × nat-set → index-store
. \ .	index-store	f	index-address-store × address-set → index-address-store
. \| .	ablock-store-refsize-cons	f	address-set × nat → address-set
. \| .	index-store	f	index-store × nat-set → index-store
. \| .	index-store	f	index-address-store × address-set → index-address-store
. ∈ .	index-store	p	index-node × index-address-store
. ∈ .	string	p	char × string
. ∈ .	index-store	p	address × index-address-store
. ∈ .	branch-array	p	branch × branch-array
. ∈ .	index-store	p	address × index-store
. ∈ .	address-list-set	p	address × address-list
. ∈ .	buffer	p	data × buffer
. ∈ .	address-list-set	p	address × address-set
. ∈ .	index-store	p	index-block × index-store
. ∈ .	index-store	p	index-node × index-node-list
. ∈ .	nat-store	p	nat × nat-set
. ∈ .	laddress-list	p	laddress × laddress-list
. ∈ .	index-store	p	nat × index-store
. ∩ .	address-list-set	f	address-set × address-set → address-set
. ∩ .	nat-store	f	nat-set × nat-set → nat-set
. ∪ .	address-list-set	f	address-set × address-set → address-set
. ∪ .	nat-store	f	nat-set × nat-set → nat-set
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	index-store	p	index-address-store × index-address-store
. ⊆ .	address-list-set	p	address-set × address-set
. ⊆ .	nat-store	p	nat-set × nat-set
. ⊆ .	index-store	p	index-store × index-store
. ⊑ .	index-store	p	index-store × index-store
. ⊑ .	string	p	string × string
. ⊑ .	laddress-list	p	laddress-list × laddress-list
. ⊑ .	address-list-set	p	address-list × address-list
. ⊑ .	index-store	p	index-node-list × index-node-list
. ⊒ .	laddress-list	p	laddress-list × laddress-list
. ⊒ .	string	p	string × string
. ⊒ .	index-store	p	index-node-list × index-node-list
. ⊒ .	address-list-set	p	address-list × address-list
. ⊕ .	index-store	f	index-store × index-store → index-store
. ⊕ .	index-store	f	index-address-store × index-address-store → index-address-store
@	laddress	f	nat × nat → laddress
@	address-data	f	nat × nat × nat → address
[]	address-list-set	c	address-list
[]	index-store	c	index-node-list
[]	laddress-list	c	laddress-list
{ . }	nat-store	f	nat → nat-set
{ . }	address-list-set	f	address → address-set
∅	address-list-set	c	address-set
∅	index-store	c	index-address-store
∅	index-store	c	index-store
∅	nat-store	c	nat-set
⊏	string	p	string × string
ADR_DUMMY	constants	c	address
BRANCH_SIZE	constants	c	nat
EB_PAGE_SIZE	eraseblock	c	nat
LEB_SIZE	eraseblock	c	nat
MIN_SIZE	constants	c	nat
PAGES_PER_LEB	eraseblock	c	nat
PAGES_PER_PEB	eraseblock	c	nat
PEB_SIZE	eraseblock	c	nat
address	address	s
address-list	address-list-set	s
address-set	address-list-set	s
addressif	index-store	v	address × index-node → index-node
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
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
boolvar	indexnode	v	bool
boolvar0	indexnode	v	bool
br	branch	v	branch
br0	branch-array	v	branch
br1	branch-array	v	branch
branch	branch	s
branch-array	branch-array	s
brar	branch-array	v	branch-array
brar0	branch-array	v	branch-array
brar1	branch-array	v	branch-array
brar2	branch-array	v	branch-array
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
butlastn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
butlastn	string	pf	nat × string → string with λ n, str. n ≤ # str
butlastn	index-store	pf	nat × index-node-list → index-node-list with λ n, indx. n ≤ # indx
butlastn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
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
cmp	branch-array	pp	branch-array × branch × nat × nat with λ brar, br, m, n. m + n ≤ # brar
cmp	branch-array	pp	branch-array × nat × branch-array × nat × nat with λ brar, m, brar0, m0, n. m + n ≤ # brar ∧ m0 + n ≤ # brar0
copy	branch-array	pf	branch-array × nat × branch-array × nat × nat → branch-array with λ brar, m, brar0, m0, n. m + n ≤ # brar ∧ m0 + n ≤ # brar0
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
datakey	key	f	nat × nat → key
dentrykey	key	f	nat × string → key
disj	laddress-list	p	laddress-list × laddress-list
disj	index-store	p	index-node-list × index-node-list
disj	address-list-set	p	address-list × address-list
disj	string	p	string × string
dom .	index-store	f	index-store → nat-set
dom .	index-store	f	index-address-store → address-set
dropn	address-list-set	f	nat × address-list → address-list
dropn	index-store	f	nat × index-node-list → index-node-list
dropn	laddress-list	f	nat × laddress-list → laddress-list
dups	laddress-list	p	laddress-list
dups	string	p	string
dups	index-store	p	index-node-list
dups	address-list-set	p	address-list
empty	buffer	c	data
emptyleb	eraseblock	c	buffer
emptypage	eraseblock	c	buffer
emptypeb	eraseblock	c	buffer
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	branch-array	pf	branch-array × branch × nat × nat → branch-array with λ brar, br, n, m. n + m ≤ # brar
fill	branch-array	f	branch-array × branch → branch-array
fill	buffer	f	buffer × data → buffer
fillfirst	string	f	nat × char × string → string
fillfirst	address-list-set	f	nat × address × address-list → address-list
fillfirst	laddress-list	f	nat × laddress × laddress-list → laddress-list
fillfirst	index-store	f	nat × index-node × index-node-list → index-node-list
firstn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
firstn	index-store	pf	nat × index-node-list → index-node-list with λ n, indx. n ≤ # indx
firstn	string	pf	nat × string → string with λ n, str. n ≤ # str
firstn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
frome	string	f	string × char → string
frome	address-list-set	f	address-list × address → address-list
frome	index-store	f	index-node-list × index-node → index-node-list
frome	laddress-list	f	laddress-list × laddress → laddress-list
iast	index-store	v	index-address-store
iast0	index-store	v	index-address-store
iast1	index-store	v	index-address-store
iast2	index-store	v	index-address-store
iblock	index-store	v	index-block
iblock0	index-store	v	index-block
iblock1	index-store	v	index-block
iblock2	index-store	v	index-block
id○	branch-array	p	branch-array × branch-array × nat
id○	buffer	p	buffer × buffer × nat
idataf	index-store	v	index-block → index-block
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
idrange	branch-array	pp	branch-array × nat × nat with λ brar, m, n. m + n ≤ # brar
ielemdataf	index-store	v	nat × index-block → index-block
ielemf	index-store	v	index-node → index-node
ind	indexnode	v	index-node
ind0	index-store	v	index-node
ind1	index-store	v	index-node
ind2	index-store	v	index-node
index-address-store	index-store	s
index-block	index-store	s
index-node	indexnode	s
index-node-list	index-store	s
index-store	index-store	s
indexblock	index-store	f	index-node-list × laddress-list × nat → index-block
indexnode	indexnode	f	branch-array × bool × nat → index-node
indx	index-store	v	index-node-list
indx0	index-store	v	index-node-list
indx1	index-store	v	index-node-list
indx2	index-store	v	index-node-list
indx3	index-store	v	index-node-list
inodekey	key	f	nat → key
inv	index-store	p	index-store
inv	index-store	p	index-block
inv-flashsize	index-store	p	index-node-list × laddress-list
is-aligned	align	p	nat × nat
isempty	eraseblock	p	buffer × nat × nat
isempty	eraseblock	p	buffer
istore	index-store	v	index-store
istore0	index-store	v	index-store
istore1	index-store	v	index-store
istore2	index-store	v	index-store
key	key	s
key	key	v	key
key0	branch	v	key
laddress	laddress	s
laddress-list	laddress-list	s
ladr	laddress	v	laddress
ladr0	laddress-list	v	laddress
ladr1	laddress-list	v	laddress
ladr2	laddress-list	v	laddress
lastn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
lastn	index-store	pf	nat × index-node-list → index-node-list with λ n, indx. n ≤ # indx
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
lax	laddress-list	v	laddress-list
lax0	laddress-list	v	laddress-list
lax1	laddress-list	v	laddress-list
lax2	laddress-list	v	laddress-list
lax3	laddress-list	v	laddress-list
m	nat-basic	v	nat
m0	address-data	v	nat
m1	address-data	v	nat
m2	address-data	v	nat
m3	address-data	v	nat
m4	address-data	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkbranch	branch	f	key × address → branch
mkbrarray	branch-array	f	nat → branch-array
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mkentry	branch	f	key × address → branch
mklist	string	f	char × nat → string
mklist	address-list-set	f	address × nat → address-list
mklist	index-store	f	index-node × nat → index-node-list
mklist	laddress-list	f	laddress × nat → laddress-list
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
n2	nat-store	v	nat
n3	nat-store	v	nat
n4	nat-store	v	nat
nat	nat-basic	s
nat-set	nat-store	s
nodes	index-store	f	index-store → index-address-store
ns	nat-store	v	nat-set
ns0	nat-store	v	nat-set
ns1	nat-store	v	nat-set
ns2	nat-store	v	nat-set
pos	string	f	char × string → nat
pos	address-list-set	f	address × address-list → nat
pos	laddress-list	f	laddress × laddress-list → nat
pos	index-store	f	index-node × index-node-list → nat
prefixn	address-list-set	f	nat × address-list → address-list
prefixn	laddress-list	f	nat × laddress-list → laddress-list
prefixn	index-store	f	nat × index-node-list → index-node-list
range=	buffer	p	buffer × nat × buffer × nat × nat
refsize-cons	index-store	p	index-store × address-set
remove-refsize0	index-store	f	index-store → index-store
resize	buffer	f	buffer × nat → buffer
restn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
restn	string	pf	nat × string → string with λ n, str. n ≤ # str
restn	index-store	pf	nat × index-node-list → index-node-list with λ n, indx. n ≤ # indx
restn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	branch-array	pf	branch-array × nat → branch-array with λ brar, n. n ≤ # brar
rev	buffer	f	buffer → buffer
rev	string	f	string → string
rev	laddress-list	f	laddress-list → laddress-list
rev	branch-array	f	branch-array → branch-array
rev	index-store	f	index-node-list → index-node-list
rev	address-list-set	f	address-list → address-list
rmdup	string	f	string → string
rmdup	address-list-set	f	address-list → address-list
rmdup	laddress-list	f	laddress-list → laddress-list
rmdup	index-store	f	index-node-list → index-node-list
slice	address-list-set	f	nat × nat × address-list → address-list
slice	index-store	f	nat × nat × index-node-list → index-node-list
slice	laddress-list	f	nat × nat × laddress-list → laddress-list
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
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
subarray	branch-array	pf	branch-array × nat × nat → branch-array with λ brar, m, n. m + n ≤ # brar
sublist	laddress-list	pf	nat × nat × laddress-list → laddress-list with λ n, m, lax. n + m ≤ # lax
sublist	index-store	pf	nat × nat × index-node-list → index-node-list with λ n, m, indx. n + m ≤ # indx
sublist	string	pf	nat × nat × string → string with λ n, m, str. n + m ≤ # str
sublist	address-list-set	pf	nat × nat × address-list → address-list with λ n, m, ax. n + m ≤ # ax
valid-adrs	ablock-store-refsize-cons	p	address-set
zero	buffer	c	data