[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
# .	address-list-set	f	address-list → nat
# .	address-store	f	address-store → nat
# .	address-list-set	f	address-set → nat
# .	buffer	f	buffer → nat
# .	list-data	f	list → nat
# .	nat-store	f	nat-set → nat
# .	laddress-list	f	laddress-list → nat
# .	store	f	store → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. '	address-list-set	f	address → address-list
. '	laddress-list	f	laddress → laddress-list
. '	list	f	elem → list
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. + .	address-list-set	f	address × address-list → address-list
. + .	address-list-set	f	address-list × address-list → address-list
. + .	laddress-list	f	laddress-list × laddress → laddress-list
. + .	address-list-set	f	address-list × address → address-list
. + .	laddress-list	f	laddress-list × laddress-list → laddress-list
. + .	list-data	f	elem × list → list
. + .	laddress-list	f	laddress × laddress-list → laddress-list
. + .	list	f	list × list → list
. + .	list	f	list × elem → list
. ++ .	nat-store	f	nat-set × nat → nat-set
. ++ .	address-list-set	f	address-list × address → address-list
. ++ .	laddress-list	f	laddress-list × laddress → laddress-list
. ++ .	address-list-set	f	address-set × address → address-set
. ++ .	list-dup	f	list × elem → list
. +1	nat-basic	f	nat → nat
. +2 .	address-list-set	f	address × address → address-list
. +2 .	list	f	elem × elem → list
. +2 .	laddress-list	f	laddress × laddress → laddress-list
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	address-list-set	f	address-set × address → address-set
. -- .	address-store	f	address-store × address → address-store
. -- .	nat-store	f	store × nat → store
. -- .	nat-store	f	nat-set × nat → nat-set
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	address-list-set	f	address-list × address → address-list
. -1l .	laddress-list	f	laddress-list × laddress → laddress-list
. -1l .	list-del	f	list × elem → list
. -l .	address-list-set	f	address-list × address → address-list
. -l .	laddress-list	f	laddress-list × laddress → laddress-list
. -l .	list-del	f	list × elem → list
. -p .	address-list-set	f	address-list × nat → address-list
. -p .	laddress-list	f	laddress-list × nat → laddress-list
. -p .	list-del	f	list × nat → list
. .butlast	laddress-list	pf	laddress-list → laddress-list with λ lax. lax ≠ []
. .butlast	address-list-set	pf	address-list → address-list with λ ax. ax ≠ []
. .butlast	list-last	pf	list → list with λ x. x ≠ []
. .butmax	nat-set	pf	nat-set → nat-set with λ ns. ns ≠ ∅
. .butmin	nat-set	pf	nat-set → nat-set with λ ns. ns ≠ ∅
. .flashsize	ablock-store-inv	f	elem → nat
. .flashsize	ablock-store-inv	f	list → nat
. .head	laddress-list	pf	laddress-list → laddress with λ lax. lax ≠ []
. .head	address-list-set	pf	address-list → address with λ ax. ax ≠ []
. .head	list-data	pf	list → elem with λ x. x ≠ []
. .ladrlist	ablock	f	ablock → laddress-list
. .ladrlist:= .	ablock	f	ablock × laddress-list → ablock
. .last	laddress-list	pf	laddress-list → laddress with λ lax. lax ≠ []
. .last	address-list-set	pf	address-list → address with λ ax. ax ≠ []
. .last	list-last	pf	list → elem with λ x. x ≠ []
. .list	ablock	f	ablock → list
. .list:= .	ablock	f	ablock × list → ablock
. .lnum	address-data	f	address → nat
. .lnum:= .	address-data	f	address × nat → address
. .map ( . )	address-store	f	address-store × (address × elem → elem) → address-store
. .map ( . )	ablock-store	f	store × (ablock → ablock) → store
. .map ( . )	address-store	f	address-store × (elem → elem) → address-store
. .map ( . )	ablock-store	f	store × (nat × ablock → ablock) → store
. .max	nat-set	pf	nat-set → nat with λ ns. ns ≠ ∅
. .min	nat-set	pf	nat-set → nat with λ ns. ns ≠ ∅
. .off	laddress	f	laddress → nat
. .off:= .	laddress	f	laddress × nat → laddress
. .pos	address-data	f	address → nat
. .pos:= .	address-data	f	address × nat → address
. .ref-size	ablock	f	ablock → nat
. .ref-size:= .	ablock	f	ablock × nat → ablock
. .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	list-data	pf	list → list with λ x. x ≠ []
. .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
. / .	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
. < .	list-data	p	list × list
. < .	nat-set	p	nat × nat-set
. < .	laddress-list	p	laddress-list × laddress-list
. =○refsize .	ablock-store-inv	p	store × store
. > .	nat	p	nat × nat
. [ . ]	address-store	pf	address-store × address → elem with λ ast, adr. adr ∈ ast
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. [ . ]	ablock-store	pf	store × nat → ablock with λ st, n. n ∈ st
. [ . ]	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
. [ . ]	ablock-store	f	store × nat × ablock → store
. [ . ]	list-del	pf	list × nat × elem → list with λ x, n, a. n < # x
. [ . ]	ablock-store-inv	f	store × address → elem
. [ . ]	list-del	pf	list × nat → elem with λ x, n. n < # x
. [ . ]	address-store	f	address-store × address × elem → address-store
. [ . ]	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
. \ .	address-list-set	f	address-set × address-set → address-set
. \ .	nat-store	f	nat-set × nat-set → nat-set
. \ .	nat-store	f	store × nat-set → store
. \ .	address-store	f	address-store × address-set → address-store
. \| .	ablock-store-refsize-cons	f	address-set × nat → address-set
. \| .	nat-store	f	store × nat-set → store
. \| .	address-store	f	address-store × address-set → address-store
. ∈ .	address-store	p	elem × address-store
. ∈ .	address-list-set	p	address × address-list
. ∈ .	address-store	p	address × address-store
. ∈ .	address-list-set	p	address × address-set
. ∈ .	ablock-store-inv	p	address × store
. ∈ .	list	p	elem × list
. ∈ .	buffer	p	data × buffer
. ∈ .	laddress-list	p	laddress × laddress-list
. ∈ .	ablock-store	p	ablock × store
. ∈ .	nat-store	p	nat × store
. ∈ .	nat-store	p	nat × nat-set
. ∩ .	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
. ⊆ .	address-store	p	address-store × address-store
. ⊆ .	address-list-set	p	address-set × address-set
. ⊆ .	nat-store	p	nat-set × nat-set
. ⊆ .	store	p	store × store
. ⊑ .	ablock-store-inv	p	store × store
. ⊑ .	address-list-set	p	address-list × address-list
. ⊑ .	laddress-list	p	laddress-list × laddress-list
. ⊑ .	list-last	p	list × list
. ⊒ .	laddress-list	p	laddress-list × laddress-list
. ⊒ .	address-list-set	p	address-list × address-list
. ⊒ .	list-last	p	list × list
. ⊕ .	store+set	f	store × store → store
. ⊕ .	address-store	f	address-store × address-store → address-store
@	laddress	f	nat × nat → laddress
@	address-data	f	nat × nat × nat → address
[]	address-list-set	c	address-list
[]	list-data	c	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
∅	store	c	store
∅	address-store	c	address-store
∅	nat-store	c	nat-set
EB_PAGE_SIZE	eraseblock	c	nat
LEB_SIZE	eraseblock	c	nat
PAGES_PER_LEB	eraseblock	c	nat
PAGES_PER_PEB	eraseblock	c	nat
PEB_SIZE	eraseblock	c	nat
a	elem	v	elem
a0	list-data	v	elem
ablock	ablock	s
ablock	ablock	v	ablock
ablock0	ablock-store	v	ablock
ablock1	ablock-store	v	ablock
ablock2	ablock-store	v	ablock
address	address	s
address-list	address-list-set	s
address-set	address-list-set	s
address-store	address-store	s
addresselemf	address-store	v	address × elem → elem
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
ast	address-store	v	address-store
ast0	address-store	v	address-store
ast1	address-store	v	address-store
ast2	address-store	v	address-store
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	elem	v	elem
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	list-last	pf	nat × list → list with λ n, x. n ≤ # x
butlastn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
c	elem	v	elem
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
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
dataf	ablock-store	v	ablock → ablock
disj	laddress-list	p	laddress-list × laddress-list
disj	list-dup	p	list × list
disj	address-list-set	p	address-list × address-list
dom .	nat-store	f	store → nat-set
dom .	address-store	f	address-store → address-set
dropn	address-list-set	f	nat × address-list → address-list
dropn	list-prefixn	f	nat × list → list
dropn	laddress-list	f	nat × laddress-list → laddress-list
dups	laddress-list	p	laddress-list
dups	address-list-set	p	address-list
dups	list-dup	p	list
elem	elem	s
elemdataf	ablock-store	v	nat × ablock → ablock
elemf	address-store	v	elem → elem
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	buffer	f	buffer × data → buffer
fillfirst	address-list-set	f	nat × address × address-list → address-list
fillfirst	list-last	f	nat × elem × list → list
fillfirst	laddress-list	f	nat × laddress × laddress-list → laddress-list
firstn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
firstn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
firstn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
frome	address-list-set	f	address-list × address → address-list
frome	list-del	f	list × elem → list
frome	laddress-list	f	laddress-list × laddress → laddress-list
id○	buffer	p	buffer × buffer × nat
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
inv	ablock-store-inv	p	store
inv	ablock-store-inv	p	ablock
inv-flashsize	ablock-store-inv	p	list × laddress-list
is-aligned	align	p	nat × nat
isempty	eraseblock	p	buffer × nat × nat
isempty	eraseblock	p	buffer
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	list-del	pf	nat × list → list with λ n, x. n ≤ # x
lastn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
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
list	list-data	s
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
mkblock	ablock	f	list × laddress-list × nat → ablock
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mklist	address-list-set	f	address × nat → address-list
mklist	list-last	f	elem × nat → 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	ablock-nodes	f	store → 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	address-list-set	f	address × address-list → nat
pos	laddress-list	f	laddress × laddress-list → nat
pos	list-del	f	elem × list → nat
prefixn	address-list-set	f	nat × address-list → address-list
prefixn	list-prefixn	f	nat × list → list
prefixn	laddress-list	f	nat × laddress-list → laddress-list
range=	buffer	p	buffer × nat × buffer × nat × nat
refsize-cons	ablock-store-refsize-cons	p	store × address-set
remove-refsize0	ablock-store-inv	f	store → store
resize	buffer	f	buffer × nat → buffer
restn	laddress-list	pf	nat × laddress-list → laddress-list with λ n, lax. n ≤ # lax
restn	address-list-set	pf	nat × address-list → address-list with λ n, ax. n ≤ # ax
restn	list-del	pf	nat × list → list with λ n, x. n ≤ # x
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	buffer	f	buffer → buffer
rev	address-list-set	f	address-list → address-list
rev	laddress-list	f	laddress-list → laddress-list
rev	list-last	f	list → list
rmdup	address-list-set	f	address-list → address-list
rmdup	laddress-list	f	laddress-list → laddress-list
rmdup	list-dup	f	list → list
slice	address-list-set	f	nat × nat × address-list → address-list
slice	list-prefixn	f	nat × nat × list → list
slice	laddress-list	f	nat × nat × laddress-list → laddress-list
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
st	store	v	store
st0	store	v	store
st1	store	v	store
st2	store	v	store
store	store	s
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
sublist	laddress-list	pf	nat × nat × laddress-list → laddress-list with λ n, m, lax. n + m ≤ # lax
sublist	list-del	pf	nat × nat × list → list with λ n, m, x. n + m ≤ # x
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
x	list-data	v	list
x0	list-data	v	list
x1	list-data	v	list
y	list-data	v	list
z	list-data	v	list
zero	buffer	c	data