[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
# .	dataarray	f	dataarray → nat
# .	datastream	f	datalist → nat
. '	datastream	f	data → datalist
. + .	nat-basic	f	nat × nat → nat
. + .	datastream	f	datastream × datastream → datastream
. + .	dataarray	f	dataarray × dataarray → dataarray
. + .	datastream	f	data × datastream → datastream
. + .	datastream	f	data × datalist → datalist
. + .	nat-inf	f	natinf × natinf → natinf
. + .	datastream	f	datalist × datalist → datalist
. + .	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
. .ar	datastream-conv	f	datastream → dataarray
. .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
. [ . ]	dataarray	pf	dataarray × nat → data with λ ar0, n. n < # ar0
. [ . ]	datastream	pf	datalist × nat → data with λ dx, n. n < # dx
. [ . ]	dataarray	pf	dataarray × nat × data → dataarray with λ ar0, n, d. n < # ar0
. ∈ .	dataarray	p	data × dataarray
. ∈ .	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	pf	datastream × nat → datastream with λ σ, n. finp(σ) → ⌜n⌝ < # σ ∨ ⌜n⌝ = # σ
. from .	datastream	f	(nat → data) × nat → nat → data
. to .	datastream	f	(nat → data) × nat → datalist
. to .	datastream	pf	datalist × nat → datalist with λ dx, n. n ≤ # dx
. 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
σ⊥	datastream-conv	c	datastream
σ1	datastream	v	datastream
σ2	datastream	v	datastream
∞	nat-inf	c	natinf
⌜ . ⌝	datastream	f	datalist → datastream
⌜ . ⌝	datastream	f	(nat → data) → datastream
⌜ . ⌝	nat-inf	f	nat → natinf
⌜ . ⌝	datastream-conv	f	dataarray → datastream
ar	dataarray	v	dataarray
ar0	dataarray	v	dataarray
ar1	dataarray	v	dataarray
ar2	dataarray	v	dataarray
butlastn	datastream	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
cmp	dataarray	pp	dataarray × data × nat × nat with λ ar0, d, m, n. m + n ≤ # ar0
cmp	dataarray	pp	dataarray × nat × dataarray × nat × nat with λ ar1, m, ar2, m0, n. m + n ≤ # ar1 ∧ m0 + n ≤ # ar2
copy	dataarray	pf	dataarray × nat × dataarray × nat × nat → dataarray with λ ar1, m, ar2, m0, n. m + n ≤ # ar1 ∧ m0 + n ≤ # ar2
d	data	v	data
d0	data	v	data
d1	data	v	data
d2	data	v	data
data	data	s
dataarray	dataarray	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
empty	dataarray	c	data
fill	dataarray	pf	dataarray × data × nat × nat → dataarray with λ ar0, d, n, m. n + m ≤ # ar0
fill	dataarray	f	dataarray × data → dataarray
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 λ σ. σ ≠ []
id○	dataarray	p	dataarray × dataarray × nat
idrange	dataarray	pp	dataarray × nat × nat with λ ar0, m, n. m + n ≤ # ar0
lastn	datastream	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
mkarray	dataarray	f	nat → dataarray
mkemparray	dataarray	f	nat → dataarray
mklist	datastream	f	data × nat → datalist
mkzarray	dataarray	f	nat → dataarray
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
range=	dataarray	p	dataarray × nat × dataarray × nat × nat
resize	dataarray	f	dataarray × nat → dataarray
restn	datastream	pf	nat × datalist → datalist with λ n, dx. n ≤ # dx
rev	dataarray	f	dataarray → dataarray
rev	dataarray	pf	dataarray × nat → dataarray with λ ar0, n. n ≤ # ar0
rev	datastream	f	datalist → datalist
rmdup	datastream	f	datalist → datalist
splice	dataarray	f	dataarray × nat × dataarray × nat × nat → dataarray
subarray	dataarray	pf	dataarray × nat × nat → dataarray with λ ar0, m, n. m + n ≤ # ar0
sublist	datastream	pf	nat × nat × datalist → datalist with λ n, m, dx. n + m ≤ # dx
tl	datastream	pf	datastream → datastream with λ σ. σ ≠ []
zero	dataarray	c	data