[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-inf	f	buffer-inf → natinf
# .	buffer	f	buffer → nat
# .	buffer-inf	f	datalist → nat
. '	buffer-inf	f	data → datalist
. + .	nat-basic	f	nat × nat → nat
. + .	buffer-inf	f	buffer-inf × buffer-inf → buffer-inf
. + .	buffer	f	buffer × buffer → buffer
. + .	buffer-inf	f	data × buffer-inf → buffer-inf
. + .	buffer-inf	f	data × datalist → datalist
. + .	nat-inf	f	natinf × natinf → natinf
. + .	buffer-inf	f	datalist × datalist → datalist
. + .	buffer-inf	f	datalist × data → datalist
. ++ .	buffer-inf	f	datalist × data → datalist
. +1	nat-basic	f	nat → nat
. +2 .	buffer-inf	f	data × data → datalist
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. -1l .	buffer-inf	f	datalist × data → datalist
. -l .	buffer-inf	f	datalist × data → datalist
. -p .	buffer-inf	f	datalist × nat → datalist
. .buf	buffer-inf-conv	f	buffer-inf → buffer
. .butlast	buffer-inf	pf	datalist → datalist with λ dx. dx ≠ []
. .f	buffer-inf	pf	buffer-inf → nat → data with λ σ0. λ m. ∃ nf0. σ0 = ⌜nf0⌝
. .head	buffer-inf	pf	datalist → data with λ dx. dx ≠ []
. .l	buffer-inf	pf	buffer-inf → datalist with λ σ0. finp(σ0)
. .last	buffer-inf	pf	datalist → data with λ dx. dx ≠ []
. .n	nat-inf	pf	natinf → nat with λ n∞. n∞ ≠ ∞
. .tail	buffer-inf	pf	datalist → datalist with λ dx. dx ≠ []
. < .	nat-basic	p	nat × nat
. < .	nat-inf	p	natinf × natinf
. < .	buffer-inf	p	datalist × datalist
. > .	nat	p	nat × nat
. [ . ]	buffer-inf	pf	buffer-inf × nat × data → buffer-inf with λ σ, n, d. finp(σ) → ⌜n⌝ < # σ
. [ . ]	buffer-inf	pf	buffer-inf × nat → data with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. [ . ]	buffer-inf	pf	datalist × nat × data → datalist with λ dx, n, d. n < # dx
. [ . ]	buffer	pf	buffer × nat → data with λ buf, n. n < # buf
. [ . ]	buffer-inf	pf	datalist × nat → data with λ dx, n. n < # dx
. [ . ]	buffer	pf	buffer × nat × data → buffer with λ buf, n, d. n < # buf
. ∈ .	buffer	p	data × buffer
. ∈ .	buffer-inf	p	data × datalist
. ≤ .	nat	p	nat × nat
. ≤ .	buffer-inf	p	buffer-inf × buffer-inf
. ≥ .	nat	p	nat × nat
. ⊑ .	buffer-inf	p	datalist × datalist
. ⊒ .	buffer-inf	p	datalist × datalist
. from .	buffer-inf	pf	datalist × nat → datalist with λ dx, n. n ≤ # dx
. from .	buffer-inf	f	(nat → data) × nat → nat → data
. from .	buffer-inf	pf	buffer-inf × nat → buffer-inf with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to .	buffer-inf	pf	datalist × nat → datalist with λ dx, n. n ≤ # dx
. to .	buffer-inf	f	(nat → data) × nat → datalist
. to .	buffer-inf	pf	buffer-inf × nat → buffer-inf with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to∞ .	buffer-inf	pf	buffer-inf × natinf → buffer-inf with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
[]	buffer-inf	c	datalist
[]	buffer-inf	c	buffer-inf
σ	buffer-inf	v	buffer-inf
σ⊥	buffer-inf-conv	c	buffer-inf
σ1	buffer-inf	v	buffer-inf
σ2	buffer-inf	v	buffer-inf
∞	nat-inf	c	natinf
⌜ . ⌝	buffer-inf	f	datalist → buffer-inf
⌜ . ⌝	buffer-inf	f	(nat → data) → buffer-inf
⌜ . ⌝	nat-inf	f	nat → natinf
⌜ . ⌝	buffer-inf-conv	f	buffer → buffer-inf
buf	buffer	v	buffer
buf0	buffer	v	buffer
buf1	buffer	v	buffer
buf2	buffer	v	buffer
buffer	buffer	s
buffer-inf	buffer-inf	s
butlastn	buffer-inf	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
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
datalist	buffer-inf	s
disj	buffer-inf	p	datalist × datalist
dups	buffer-inf	p	datalist
dx	buffer-inf	v	datalist
dx0	buffer-inf	v	datalist
dx1	buffer-inf	v	datalist
dx3	buffer-inf	v	datalist
dx7	buffer-inf	v	datalist
empty	buffer	c	data
fill	buffer	f	buffer × data → buffer
fill	buffer	pf	buffer × data × nat × nat → buffer with λ buf, d, n, m. n + m ≤ # buf
fillfirst	buffer-inf	f	nat × data × datalist → datalist
finp	buffer-inf	p	buffer-inf
firstn	buffer-inf	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
frome	buffer-inf	f	datalist × data → datalist
hd	buffer-inf	pf	buffer-inf → data with λ σ. σ ≠ []
id○	buffer	p	buffer × buffer × nat
idrange	buffer	pp	buffer × nat × nat with λ buf, m, n. m + n ≤ # buf
lastn	buffer-inf	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
m	nat-basic	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
min	nat-inf	f	natinf × natinf → natinf
mkbuf	buffer	f	nat → buffer
mkempbuf	buffer	f	nat → buffer
mklist	buffer-inf	f	data × nat → datalist
mkzbuf	buffer	f	nat → buffer
n	nat-basic	v	nat
n∞	nat-inf	v	natinf
n∞0	nat-inf	v	natinf
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
natinf	nat-inf	s
nf	buffer-inf	v	nat → data
nf0	buffer-inf	v	nat → data
pos	buffer-inf	f	data × datalist → nat
range=	buffer	p	buffer × nat × buffer × nat × nat
resize	buffer	f	buffer × nat → buffer
restn	buffer-inf	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
rev	buffer	f	buffer → buffer
rev	buffer	pf	buffer × nat → buffer with λ buf, n. n ≤ # buf
rev	buffer-inf	f	datalist → datalist
rmdup	buffer-inf	f	datalist → datalist
splice	buffer	f	buffer × nat × buffer × nat × nat → buffer
subarray	buffer	pf	buffer × nat × nat → buffer with λ buf, m, n. m + n ≤ # buf
sublist	buffer-inf	pf	nat × nat × datalist → datalist with λ n, m, dx. n + m ≤ # dx
tl	buffer-inf	pf	buffer-inf → buffer-inf with λ σ. σ ≠ []
zero	buffer	c	data