Signature symbols in this unit

Symbol	Specification	Kind	Type
# .	array	f	array → nat
. + .	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 with λ ar, n. n < # ar
. [ . ]	array	pf	array × nat × elem → array with λ ar, n, a. n < # ar
. ∈ .	array-revin	p	elem × array
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
a	array-revin	v	elem
ar	array-revin	v	array
array	array	s
cmp	array-copy	p	array × elem
cmp	array-copy	pp	array × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmp	array-copy	pp	array × elem × nat × nat with λ ar, a, m, n. m + n ≤ # ar
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
fill	array-copy	f	array × elem → array
fill	array-copy	pf	array × elem × nat × nat → array with λ ar, a, n, m. n + m ≤ # ar
id○	array-copy	p	array × array × nat
id○	array-copy	p	array × array × nat × nat
idrange	array-copy	pp	array × nat × nat with λ ar, m, n. m + n ≤ # ar
m	array-revin	v	nat
mkarray	array	f	nat → array
n	array-revin	v	nat
nat	nat-basic	s
rev	array-revin	f	array → array
rev	array-revin	pf	array × nat → array with λ ar, n. n ≤ # ar
subarray	array-copy	pf	array × nat × nat → array with λ ar, m, n. m + n ≤ # ar