[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
# .	vtbl	f	vtbl → nat
# .	volumes	f	volumes → nat
# .	buffer	f	buffer → nat
# .	ebatbl	f	ebatbl → nat
. % .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. * .	nat-mult	f	nat × nat → nat
. + .	nat-basic	f	nat × nat → nat
. + .	buffer	f	buffer × buffer → buffer
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -- .	vtbl	f	vtbl × volid → vtbl
. -- .	volumes	f	volumes × volid → volumes
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .pnum	ebaentry	pf	ebaentry → nat with λ ebae. ebae ≠ unmapped
. .pnum:= .	ebaentry	pf	ebaentry × nat → ebaentry with λ ebae, m. ebae ≠ unmapped
. / .	nat-div	pf	nat × nat → nat with λ n, m. m ≠ 0
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	volumes	pf	volumes × volid → ebatbl with λ vols, v. v ∈ vols
. [ . ]	ebatbl	pf	ebatbl × nat × ebaentry → ebatbl with λ ebatbl, n, ebae. n < # ebatbl
. [ . ]	vtbl	f	vtbl × volid × nat → vtbl
. [ . ]	ebatbl	pf	ebatbl × nat → ebaentry with λ ebatbl, n. n < # ebatbl
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	volumes	f	volumes × volid × ebatbl → volumes
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. [ . ]	vtbl	pf	vtbl × volid → nat with λ vtbl, v. v ∈ vtbl
. ∈ .	vtbl	p	volid × vtbl
. ∈ .	volumes	p	volid × volumes
. ∈ .	buffer	p	data × buffer
. ∈ .	ebatbl	p	ebaentry × ebatbl
. ∪ .	vtbl	f	vtbl × vtbl → vtbl
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊆ .	vtbl	p	vtbl × vtbl
. ⊥ .	vtbl	p	vtbl × vtbl
. subseteq .	volumes	p	volumes × volumes
∅	vtbl	c	vtbl
∅	volumes	c	volumes
⌜ . ⌝	ebaentry	f	nat → ebaentry
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
VTBL_LNUM	vtbl-conv	c	nat
VTBL_VOLID	vtbl-conv	c	volid
align↑	align	f	nat × nat → nat
align↓	align	f	nat × nat → nat
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
cmp	ebatbl	pp	ebatbl × ebaentry × nat × nat with λ ebatbl, ebae, m, n. m + n ≤ # ebatbl
cmp	ebatbl	pp	ebatbl × nat × ebatbl × nat × nat with λ ebatbl, m, ebatbl0, m0, n. m + n ≤ # ebatbl ∧ m0 + n ≤ # ebatbl0
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
copy	ebatbl	pf	ebatbl × nat × ebatbl × nat × nat → ebatbl with λ ebatbl, m, ebatbl0, m0, n. m + n ≤ # ebatbl ∧ m0 + n ≤ # ebatbl0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
ebae	ebaentry	v	ebaentry
ebae0	ebaentry	v	ebaentry
ebae1	ebaentry	v	ebaentry
ebae2	ebaentry	v	ebaentry
ebaentry	ebaentry	s
ebatbl	ebatbl	s
ebatbl	ebatbl	v	ebatbl
ebatbl0	ebatbl	v	ebatbl
ebatbl1	ebatbl	v	ebatbl
ebatbl2	ebatbl	v	ebatbl
empty	buffer	c	data
emptyleb	eraseblock	c	buffer
emptypage	eraseblock	c	buffer
emptypeb	eraseblock	c	buffer
fill	ebatbl	pf	ebatbl × ebaentry × nat × nat → ebatbl with λ ebatbl, ebae, n, m. n + m ≤ # ebatbl
fill	buffer	f	buffer × data → buffer
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	ebatbl	f	ebatbl × ebaentry → ebatbl
id○	ebatbl	p	ebatbl × ebatbl × nat
id○	buffer	p	buffer × buffer × nat
idrange	ebatbl	pp	ebatbl × nat × nat with λ ebatbl, m, n. m + n ≤ # ebatbl
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
is-aligned	align	p	nat × nat
isempty	eraseblock	p	buffer
isempty	eraseblock	p	buffer × nat × nat
m	nat-basic	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkbuf	buffer	f	nat → buffer
mkebatbl	ebatbl	f	nat → ebatbl
mkempbuf	buffer	f	nat → buffer
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
n2	vtbl	v	nat
n3	vtbl	v	nat
n4	vtbl	v	nat
n5	vtbl	v	nat
nat	nat-basic	s
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
rev	ebatbl	pf	ebatbl × nat → ebatbl with λ ebatbl, n. n ≤ # ebatbl
rev	buffer	f	buffer → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	ebatbl	f	ebatbl → ebatbl
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	ebatbl	pf	ebatbl × nat × nat → ebatbl with λ ebatbl, m, n. m + n ≤ # ebatbl
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
to-vtbl	vtbl-conv	f	volumes → vtbl
unmapped	ebaentry	c	ebaentry
v	volid	v	volid
v0	volid	v	volid
v1	volid	v	volid
v2	volid	v	volid
volid	volid	s
vols	volumes	v	volumes
vols0	volumes	v	volumes
vols1	volumes	v	volumes
vols2	volumes	v	volumes
volumes	volumes	s
vtbl	vtbl	s
vtbl	vtbl	v	vtbl
vtbl0	vtbl	v	vtbl
vtbl1	vtbl	v	vtbl
vtbl2	vtbl	v	vtbl
zero	buffer	c	data