[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
# .	pebs	f	pebs → nat
# .	buffer	f	buffer → 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
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. .bad	peb	p	peb
. .bad:= .	peb	f	peb × bool → peb
. .data	peb	f	peb → buffer
. .data:= .	peb	f	peb × buffer → peb
. .fill	peb	f	peb → nat
. .fill:= .	peb	f	peb × nat → peb
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	pebs	pf	pebs × nat × peb → pebs with λ pebs, n, peb. n < # pebs
. [ . ]	pebs	pf	pebs × nat → peb with λ pebs, n. n < # pebs
. [ . ]	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
. ∈ .	pebs	p	peb × pebs
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
bool	bool	s
boolvar	bool	v	bool
boolvar0	bool	v	bool
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
cmp	pebs	pp	pebs × peb × nat × nat with λ pebs, peb, m, n. m + n ≤ # pebs
cmp	pebs	pp	pebs × nat × pebs × nat × nat with λ pebs, m, pebs0, m0, n. m + n ≤ # pebs ∧ m0 + n ≤ # pebs0
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	pebs	pf	pebs × nat × pebs × nat × nat → pebs with λ pebs, m, pebs0, m0, n. m + n ≤ # pebs ∧ m0 + n ≤ # pebs0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
empty	buffer	c	data
fill	pebs	pf	pebs × peb × nat × nat → pebs with λ pebs, peb, n, m. n + m ≤ # pebs
fill	buffer	f	buffer × data → buffer
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	pebs	f	pebs × peb → pebs
id○	pebs	p	pebs × pebs × nat
id○	buffer	p	buffer × buffer × nat
idrange	pebs	pp	pebs × nat × nat with λ pebs, m, n. m + n ≤ # pebs
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
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
mkempbuf	buffer	f	nat → buffer
mkpeb	peb	f	buffer × nat × bool → peb
mkpebs	pebs	f	nat → pebs
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
peb	peb	s
peb	peb	v	peb
peb0	pebs	v	peb
peb1	pebs	v	peb
pebs	pebs	s
pebs	pebs	v	pebs
pebs0	pebs	v	pebs
pebs1	pebs	v	pebs
pebs2	pebs	v	pebs
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
rev	pebs	pf	pebs × nat → pebs with λ pebs, n. n ≤ # pebs
rev	buffer	f	buffer → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	pebs	f	pebs → pebs
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	pebs	pf	pebs × nat × nat → pebs with λ pebs, m, n. m + n ≤ # pebs
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
zero	buffer	c	data