[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
# .	abstract-volume	f	abstract-volume → 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
. .data	leb	pf	leb → buffer with λ leb. leb.mapped?
. .data:= .	leb	pf	leb × buffer → leb with λ leb, buf. leb.mapped?
. .fill	leb	pf	leb → nat with λ leb. leb.mapped?
. .fill:= .	leb	pf	leb × nat → leb with λ leb, m. leb.mapped?
. .mapped?	leb	p	leb
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	abstract-volume	pf	abstract-volume × nat × leb → abstract-volume with λ evol, n, leb. n < # evol
. [ . ]	abstract-volume	pf	abstract-volume × nat → leb with λ evol, n. n < # evol
. [ . ]	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
. ∈ .	abstract-volume	p	leb × abstract-volume
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
abstract-volume	abstract-volume	s
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
cmp	abstract-volume	pp	abstract-volume × leb × nat × nat with λ evol, leb, m, n. m + n ≤ # evol
cmp	abstract-volume	pp	abstract-volume × nat × abstract-volume × nat × nat with λ evol, m, evol0, m0, n. m + n ≤ # evol ∧ m0 + n ≤ # evol0
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	abstract-volume	pf	abstract-volume × nat × abstract-volume × nat × nat → abstract-volume with λ evol, m, evol0, m0, n. m + n ≤ # evol ∧ m0 + n ≤ # evol0
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
empty	buffer	c	data
erased	leb	c	leb
evol	abstract-volume	v	abstract-volume
evol0	abstract-volume	v	abstract-volume
evol1	abstract-volume	v	abstract-volume
evol2	abstract-volume	v	abstract-volume
fill	abstract-volume	pf	abstract-volume × leb × nat × nat → abstract-volume with λ evol, leb, n, m. n + m ≤ # evol
fill	buffer	f	buffer × data → buffer
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	abstract-volume	f	abstract-volume × leb → abstract-volume
id○	abstract-volume	p	abstract-volume × abstract-volume × nat
id○	buffer	p	buffer × buffer × nat
idrange	abstract-volume	pp	abstract-volume × nat × nat with λ evol, m, n. m + n ≤ # evol
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
leb	leb	s
leb	leb	v	leb
leb0	abstract-volume	v	leb
leb1	abstract-volume	v	leb
m	nat-basic	v	nat
m0	array-copy	v	nat
mapped	leb	f	buffer × nat → leb
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkabstractvolume	abstract-volume	f	nat → abstract-volume
mkbuf	buffer	f	nat → buffer
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
nat	nat-basic	s
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
rev	abstract-volume	pf	abstract-volume × nat → abstract-volume with λ evol, n. n ≤ # evol
rev	buffer	f	buffer → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	abstract-volume	f	abstract-volume → abstract-volume
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	abstract-volume	pf	abstract-volume × nat × nat → abstract-volume with λ evol, m, n. m + n ≤ # evol
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
unmapped	leb	c	leb
zero	buffer	c	data