[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
# .	datastream	f	datastream → natinf
# .	datastream	f	datalist → nat
. '	datastream	f	data → datalist
. + .	nat-basic	f	nat × nat → nat
. + .	datastream	f	datastream × datastream → datastream
. + .	datastream	f	data × datalist → datalist
. + .	datastream	f	data × datastream → datastream
. + .	datastream	f	datalist × datalist → datalist
. + .	nat-inf	f	natinf × natinf → natinf
. + .	datastream	f	datalist × data → datalist
. ++ .	datastream	f	datalist × data → datalist
. +1	nat-basic	f	nat → nat
. +2 .	datastream	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 .	datastream	f	datalist × data → datalist
. -l .	datastream	f	datalist × data → datalist
. -p .	datastream	f	datalist × nat → datalist
. .butlast	datastream	pf	datalist → datalist with λ dx. dx ≠ []
. .f	datastream	pf	datastream → nat → data with λ σ0. λ m. ∃ nf0. σ0 = ⌜nf0⌝
. .head	datastream	pf	datalist → data with λ dx. dx ≠ []
. .l	datastream	pf	datastream → datalist with λ σ0. finp(σ0)
. .last	datastream	pf	datalist → data with λ dx. dx ≠ []
. .n	nat-inf	pf	natinf → nat with λ n∞. n∞ ≠ ∞
. .tail	datastream	pf	datalist → datalist with λ dx. dx ≠ []
. < .	nat-basic	p	nat × nat
. < .	nat-inf	p	natinf × natinf
. < .	datastream	p	datalist × datalist
. > .	nat	p	nat × nat
. [ . ]	datastream	pf	datastream × nat × data → datastream with λ σ, n, d. finp(σ) → ⌜n⌝ < # σ
. [ . ]	datastream	pf	datastream × nat → data with λ σ, n. finp(σ) → ⌜n⌝ < # σ
. [ . ]	datastream	pf	datalist × nat × data → datalist with λ dx, n, d. n < # dx
. [ . ]	datastream	pf	datalist × nat → data with λ dx, n. n < # dx
. ∈ .	datastream	p	data × datalist
. ≤ .	nat	p	nat × nat
. ≤ .	datastream	p	datastream × datastream
. ≥ .	nat	p	nat × nat
. ⊑ .	datastream	p	datalist × datalist
. ⊒ .	datastream	p	datalist × datalist
. from .	datastream	pf	datalist × nat → datalist with λ dx, n. n ≤ # dx
. from .	datastream	f	(nat → data) × nat → nat → data
. from .	datastream	pf	datastream × nat → datastream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to .	datastream	pf	datalist × nat → datalist with λ dx, n. n ≤ # dx
. to .	datastream	f	(nat → data) × nat → datalist
. to .	datastream	pf	datastream × nat → datastream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. to∞ .	datastream	pf	datastream × natinf → datastream with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ
[]	datastream	c	datalist
[]	datastream	c	datastream
σ	datastream	v	datastream
σ1	datastream	v	datastream
σ2	datastream	v	datastream
∞	nat-inf	c	natinf
⌜ . ⌝	nat-inf	f	nat → natinf
⌜ . ⌝	datastream	f	datalist → datastream
⌜ . ⌝	datastream	f	(nat → data) → datastream
butlastn	datastream	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
datalist	datastream	s
datastream	datastream	s
disj	datastream	p	datalist × datalist
dups	datastream	p	datalist
dx	datastream	v	datalist
dx0	datastream	v	datalist
dx1	datastream	v	datalist
dx3	datastream	v	datalist
dx7	datastream	v	datalist
fillfirst	datastream	f	nat × data × datalist → datalist
finp	datastream	p	datastream
firstn	datastream	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
frome	datastream	f	datalist × data → datalist
hd	datastream	pf	datastream → data with λ σ. σ ≠ []
lastn	datastream	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
m	nat-basic	v	nat
m0	nat-inf	v	nat
min	nat-inf	f	natinf × natinf → natinf
mklist	datastream	f	data × nat → datalist
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	datastream	v	nat → data
nf0	datastream	v	nat → data
pos	datastream	f	data × datalist → nat
restn	datastream	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
rev	datastream	f	datalist → datalist
rmdup	datastream	f	datalist → datalist
sublist	datastream	pf	nat × nat × datalist → datalist with λ n, m, dx. n + m ≤ # dx
tl	datastream	pf	datastream → datastream with λ σ. σ ≠ []