[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	pf	Array × Nat → Elem with λ ar, n. n < # ar
. ( . := . )	array	pf	Array × Nat × Elem → Array with λ ar, n, a. n < # ar
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-as-arrayinstance	f	Elem × Array → Array
. +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
. < .	list-as-arrayinstance	p	Array × Array
. > .	nat	p	Nat × Nat
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. first	list-as-arrayinstance	pf	Array → Elem with λ ar. ar ≠ []
. rest	list-as-arrayinstance	pf	Array → Array with λ ar. ar ≠ []
[]	list-as-arrayinstance	c	Array
Array	array	s
Elem	elem	s
Nat	nat-basic	s
a	list-as-arrayinstance	v	Elem
ar	list-as-arrayinstance	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
copyAndFill#	array-copy	pr	Nat × Nat × Nat × Elem : Array × Array
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
mkarray	array	f	Nat → Array
move	array-copy	pf	Array × Nat × Nat × Nat → Array with λ ar, m, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar
moveAndFill#	array-copy	pr	Nat × Nat × Nat × Elem : Array
n	list-as-arrayinstance	v	Nat
resize	array-copy	f	Array × Nat → Array
rotateLeft	array-copy	pf	Array × Nat × Nat × Nat → Array with λ ar, m, n, n0. m + n ≤ # ar ∧ n0 ≤ m
rotateRight	array-copy	pf	Array × Nat × Nat × Nat → Array with λ ar, m, n, n0. m + n + n0 ≤ # ar
shiftLeft	array-copy	pf	Array × Nat × Nat × Nat → Array with λ ar, m, n, n0. m + n ≤ # ar ∧ n0 ≤ m
shiftRight	array-copy	pf	Array × Nat × Nat × Nat → Array with λ ar, m, n, n0. m + n + n0 ≤ # ar
subarray	array-copy	pf	Array × Nat × Nat → Array with λ ar, m, n. m + n ≤ # ar