[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
. + .	buffer	f	buffer × buffer → buffer
. + .	nat-basic	f	nat × nat → nat
. +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
. .checksum	avidheader	pf	avidheader → nat with λ avhdr. avhdr.valid?
. .checksum:= .	avidheader	pf	avidheader × nat → avidheader with λ avhdr, m. avhdr.valid?
. .leb	avidheader	pf	avidheader → nat with λ avhdr. avhdr.valid?
. .leb:= .	avidheader	pf	avidheader × nat → avidheader with λ avhdr, m. avhdr.valid?
. .size	avidheader	pf	avidheader → nat with λ avhdr. avhdr.valid?
. .size:= .	avidheader	pf	avidheader × nat → avidheader with λ avhdr, m. avhdr.valid?
. .sqn	avidheader	pf	avidheader → nat with λ avhdr. avhdr.valid?
. .sqn:= .	avidheader	pf	avidheader × nat → avidheader with λ avhdr, m. avhdr.valid?
. .valid?	avidheader	p	avidheader
. .vol	avidheader	pf	avidheader → volid with λ avhdr. avhdr.valid?
. .vol:= .	avidheader	pf	avidheader × volid → avidheader with λ avhdr, v. avhdr.valid?
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	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
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
avhdr	avidheader	v	avidheader
avhdr0	avidheader	v	avidheader
avhdr1	avidheader	v	avidheader
avidhdr	avidheader	f	volid × nat × nat × nat × nat → avidheader
avidheader	avidheader	s
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
checksum	checksum	f	buffer × nat → nat
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
empty	buffer	c	data
empty	avidheader	c	avidheader
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fill	buffer	f	buffer × data → buffer
garbage	avidheader	c	avidheader
id○	buffer	p	buffer × buffer × nat
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
m	nat-basic	v	nat
m0	array-copy	v	nat
m1	avidheader	v	nat
m2	avidheader	v	nat
m3	avidheader	v	nat
m4	avidheader	v	nat
m5	avidheader	v	nat
m6	avidheader	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
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	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	buffer	f	buffer → buffer
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
v	volid	v	volid
v0	volid	v	volid
v1	volid	v	volid
v2	volid	v	volid
volid	volid	s
zero	buffer	c	data