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
Array	array	s
Elem	elem	s
Nat	nat-basic	s
a	array-revin	v	Elem
ar	array-revin	v	Array
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
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
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