[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
# .	buffer	f	buffer → nat
# .	avolume	f	avolume → nat
. + .	avolume	f	avolume × avolume → avolume
. + .	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
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .data	aleb	pf	aleb → buffer with λ aleb. aleb.mapped?
. .data:= .	aleb	pf	aleb × buffer → aleb with λ aleb, buf. aleb.mapped?
. .mapped?	aleb	p	aleb
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	avolume	pf	avolume × nat × aleb → avolume with λ avol, n, aleb. n < # avol
. [ . ]	avolume	pf	avolume × nat → aleb with λ avol, n. n < # avol
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. ∈ .	buffer	p	data × buffer
. ∈ .	avolume	p	aleb × avolume
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
aleb	aleb	s
aleb	aleb	v	aleb
aleb0	avolume	v	aleb
aleb1	avolume	v	aleb
avol	avolume	v	avolume
avol0	avolume	v	avolume
avol1	avolume	v	avolume
avol2	avolume	v	avolume
avolume	avolume	s
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
cmp	avolume	pp	avolume × aleb × nat × nat with λ avol, aleb, m, n. m + n ≤ # avol
cmp	avolume	pp	avolume × nat × avolume × nat × nat with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0
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	avolume	pf	avolume × nat × avolume × nat × nat → avolume with λ avol, m, avol0, m0, n. m + n ≤ # avol ∧ m0 + n ≤ # avol0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
empty	buffer	c	data
empty	avolume	c	aleb
fill	avolume	pf	avolume × aleb × nat × nat → avolume with λ avol, aleb, n, m. n + m ≤ # avol
fill	buffer	f	buffer × data → buffer
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	avolume	f	avolume × aleb → avolume
id○	avolume	p	avolume × avolume × nat
id○	buffer	p	buffer × buffer × nat
idrange	avolume	pp	avolume × nat × nat with λ avol, m, n. m + n ≤ # avol
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
m	nat-basic	v	nat
m0	array-copy	v	nat
mapped	aleb	f	buffer → aleb
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkavolume	avolume	f	nat → avolume
mkbuf	buffer	f	nat → buffer
mkemparray	avolume	f	nat → avolume
mkempbuf	buffer	f	nat → buffer
mkzarray	avolume	f	nat → avolume
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
range=	avolume	p	avolume × nat × avolume × nat × nat
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
resize	avolume	f	avolume × nat → avolume
rev	avolume	pf	avolume × nat → avolume with λ avol, n. n ≤ # avol
rev	buffer	f	buffer → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	avolume	f	avolume → avolume
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
splice	avolume	f	avolume × nat × avolume × nat × nat → avolume
subarray	avolume	pf	avolume × nat × nat → avolume with λ avol, m, n. m + n ≤ # avol
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
unmapped	aleb	c	aleb
zero	buffer	c	data
zero	avolume	c	aleb