[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
# .	array	f	array → nat
. + .	array-splice	f	array × array → array
. + .	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
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. [ . ]	array	pf	array × nat × elem → array with λ ar, n, a. n < # ar
. [ . ]	array	pf	array × nat → elem with λ ar, n. n < # ar
. ∈ .	array-copy	p	elem × array
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
a	elem	v	elem
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar2	array	v	array
array	array	s
b	elem	v	elem
c	elem	v	elem
cmp	array-copy	pp	array × elem × nat × nat with λ ar, a, m, n. m + n ≤ # ar
cmp	array-copy	pp	array × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
copy	array-copy	pf	array × nat × array × nat × nat → array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
elem	elem	s
empty	array-splice	c	elem
fill	array-copy	pf	array × elem × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar
fill	array-copy	f	array × elem → array
id○	array-copy	p	array × array × nat
idrange	array-copy	pp	array × nat × nat with λ ar, m, n. m + n ≤ # ar
m	nat-basic	v	nat
m0	array-copy	v	nat
max	min-max	f	nat × nat → nat
min	min-max	f	nat × nat → nat
mkarray	array	f	nat → array
mkemparray	array-splice	f	nat → array
mkzarray	array-splice	f	nat → array
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
range=	array-splice	p	array × nat × array × nat × nat
resize	array-splice	f	array × nat → array
rev	array-copy	pf	array × nat → array with λ ar, n. n ≤ # ar
rev	array-copy	f	array → array
splice	array-splice	f	array × nat × array × nat × nat → array
subarray	array-copy	pf	array × nat × nat → array with λ ar, m, n. m + n ≤ # ar
zero	array-splice	c	elem