[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-inf	f	datalist → nat
. '	buffer-inf	f	data → datalist
. + .	nat-basic2	f	nat × nat → nat
. + .	buffer-inf	f	buffer-inf × buffer-inf → buffer-inf
. + .	buffer-inf	f	data × datalist → datalist
. + .	buffer-inf	f	data × buffer-inf → buffer-inf
. + .	buffer-inf	f	datalist × datalist → datalist
. + .	nat-inf	f	natinf × natinf → natinf
. + .	buffer-inf	f	datalist × data → datalist
. + .	buffer-inf	f	data × data → datalist
. ++ .	buffer-inf	f	datalist × data → datalist
. +1	nat-basic1	f	nat → nat
. - .	nat	f	nat × nat → nat
. -1	nat-basic1	f	nat → nat
. -1l .	buffer-inf	f	datalist × nat → datalist
. -1l .	buffer-inf	f	datalist × data → datalist
. -l .	buffer-inf	f	datalist × data → datalist
. .butlast	buffer-inf	f	datalist → datalist
. .f	buffer-inf	f	buffer-inf → nat → data
. .first	buffer-inf	f	datalist → data
. .l	buffer-inf	f	buffer-inf → datalist
. .last	buffer-inf	f	datalist → data
. .n	nat-inf-basic	f	natinf → nat
. .rest	buffer-inf	f	datalist → datalist
. < .	nat-inf	p	natinf × natinf
. < .	buffer-inf	p	datalist × datalist
. < .	nat-basic1	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	buffer-inf	f	datalist × nat → data
. [ . ]	buffer-inf	f	datalist × nat × data → datalist
. [ . ]	buffer-inf	f	buffer-inf × nat × data → buffer-inf
. [ . ]	buffer-inf	f	buffer-inf × nat → data
. ∈ .	buffer-inf	p	data × datalist
. ≤ .	buffer-inf	p	buffer-inf × buffer-inf
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ⊑ .	buffer-inf	p	datalist × datalist
. ⊒ .	buffer-inf	p	datalist × datalist
. from .	buffer-inf	f	buffer-inf × nat → buffer-inf
. from .	buffer-inf	f	(nat → data) × nat → nat → data
. from .	buffer-inf	f	datalist × nat → datalist
. to .	buffer-inf	f	buffer-inf × nat → buffer-inf
. to .	buffer-inf	f	(nat → data) × nat → datalist
. to .	buffer-inf	f	datalist × nat → datalist
. to∞ .	buffer-inf	f	buffer-inf × natinf → buffer-inf
[]	buffer-inf	c	datalist
[]	buffer-inf	c	buffer-inf
σ	buffer-inf	v	buffer-inf
σ1	buffer-inf	v	buffer-inf
σ2	buffer-inf	v	buffer-inf
∞	nat-inf-basic	c	natinf
⌜ . ⌝	nat-inf-basic	f	nat → natinf
⌜ . ⌝	buffer-inf	f	datalist → buffer-inf
⌜ . ⌝	buffer-inf	f	(nat → data) → buffer-inf
buffer-inf	buffer-inf	s
butlastn	buffer-inf	f	nat × datalist → datalist
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
dx10	buffer-inf	v	datalist
dx2	buffer-inf	v	datalist
dx3	buffer-inf	v	datalist
dx4	buffer-inf	v	datalist
dx5	buffer-inf	v	datalist
dx6	buffer-inf	v	datalist
dx7	buffer-inf	v	datalist
dx8	buffer-inf	v	datalist
dx9	buffer-inf	v	datalist
fillfirst	buffer-inf	f	nat × data × datalist → datalist
finp	buffer-inf	p	buffer-inf
firstn	buffer-inf	f	nat × datalist → datalist
frome	buffer-inf	f	datalist × data → datalist
hd	buffer-inf	f	buffer-inf → data
lastn	buffer-inf	f	nat × datalist → datalist
m	nat-basic1	v	nat
m0	nat-inf-basic	v	nat
min	nat-inf	f	natinf × natinf → natinf
mklist	buffer-inf	f	data × nat → datalist
n	nat-basic1	v	nat
n∞	nat-inf-basic	v	natinf
n∞0	nat-inf	v	natinf
n0	nat-basic1	v	nat
n1	nat-basic1	v	nat
nat	nat-basic1	s
natinf	nat-inf-basic	s
nf	buffer-inf	v	nat → data
nf0	buffer-inf	v	nat → data
pos	buffer-inf	f	data × datalist → nat
restn	buffer-inf	f	nat × datalist → datalist
rev	buffer-inf	f	datalist → datalist
rmdup	buffer-inf	f	datalist → datalist
sublist	buffer-inf	f	nat × nat × datalist → datalist
tl	buffer-inf	f	buffer-inf → buffer-inf