[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[A] → Nat
# .	fsarray	f	FSArray[A] → Nat
. ( . )	array	pf	Array[A] × Nat → A with λ ar, n. n < # ar
. ( . )	fsarray	pf	FSArray[A] × Nat → A with λ ar, n. n < size
. ( . := . )	array	pf	Array[A] × Nat × A → Array[A] with λ ar, n, a. n < # ar
. ( . := . )	fsarray	pf	FSArray[A] × Nat × A → FSArray[A] with λ ar, n, a. n < size
. + .	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
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. toArray	array-fsarray	f	FSArray[A] → Array[A]
. toFSArray	array-fsarray	pf	Array[A] → FSArray[A] with λ ar. # ar = size
Array	array	s
FSArray	fsarray	s
Nat	nat-basic	s
a	array-fsarray	v	A
ar	array-fsarray	v	Array[A]
cmp	array-copy	p	Array('A) × 'A
cmp	fsarray-copy	p	FSArray('A) × 'A
cmp	array-copy	pp	Array('A) × Nat × Array('A) × Nat × Nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmp	array-copy	pp	Array('A) × 'A × Nat × Nat with λ ar, a, m, n. m + n ≤ # ar
cmp	fsarray-copy	pp	FSArray('A) × Nat × FSArray('A) × Nat × Nat with λ ar, m, ar0, m0, n. m + n ≤ size ∧ m0 + n ≤ size
cmp	fsarray-copy	pp	FSArray('A) × 'A × Nat × Nat with λ ar, a, m, n. m + n ≤ size
cmp	array-fsarray	pp	FSArray('A) × Nat × Array('A) × Nat × Nat with λ fsar, m, ar, m0, n. m + n ≤ size ∧ m0 + n ≤ # ar
copy	array-copy	pf	Array[A] × Nat × Array[A] × Nat × Nat → Array[A] with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
copy	fsarray-copy	pf	FSArray[A] × Nat × FSArray[A] × Nat × Nat → FSArray[A] with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ size
copy	array-fsarray	pf	Array[A] × Nat × FSArray[A] × Nat × Nat → FSArray[A] with λ ar, m, fsar, m0, n. m + n ≤ # ar ∧ m0 + n ≤ size
copy	array-fsarray	pf	FSArray[A] × Nat × Array[A] × Nat × Nat → Array[A] with λ fsar, m, ar, m0, n. m + n ≤ size ∧ m0 + n ≤ # ar
copyAndFill#	array-copy	pr	Nat × Nat × Nat × A : Array[A] × Array[A]
fill	array-copy	f	Array[A] × A → Array[A]
fill	fsarray-copy	f	FSArray[A] × A → FSArray[A]
fill	array-copy	pf	Array[A] × A × Nat × Nat → Array[A] with λ ar, a, n, m. n + m ≤ # ar
fill	fsarray-copy	pf	FSArray[A] × A × Nat × Nat → FSArray[A] with λ ar, a, n, m. n + m ≤ size
fsar	array-fsarray	v	FSArray[A]
id○	array-copy	p	Array('A) × Array('A) × Nat
id○	array-copy	p	Array('A) × Array('A) × Nat × Nat
id○	fsarray-copy	p	FSArray('A) × FSArray('A) × Nat
id○	fsarray-copy	p	FSArray('A) × FSArray('A) × Nat × Nat
idrange	array-copy	pp	Array('A) × Nat × Nat with λ ar, m, n. m + n ≤ # ar
idrange	fsarray-copy	pp	FSArray('A) × Nat × Nat with λ ar, m, n. m + n ≤ size
m	array-fsarray	v	Nat
mkarray	fsarray	c	FSArray[A]
mkarray	array	f	Nat → Array[A]
mkarray	array	f	Nat × A → Array[A]
mkfsarray	fsarray	f	A → FSArray[A]
move	array-copy	pf	Array[A] × Nat × Nat × Nat → Array[A] with λ ar, m, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar
moveAndFill#	array-copy	pr	Nat × Nat × Nat × A : Array[A]
n	array-fsarray	v	Nat
resize	array-copy	f	Array[A] × Nat → Array[A]
rotateLeft	array-copy	pf	Array[A] × Nat × Nat × Nat → Array[A] with λ ar, m, n, n0. m + n ≤ # ar ∧ n0 ≤ m
rotateRight	array-copy	pf	Array[A] × Nat × Nat × Nat → Array[A] with λ ar, m, n, n0. m + n + n0 ≤ # ar
shiftLeft	array-copy	pf	Array[A] × Nat × Nat × Nat → Array[A] with λ ar, m, n, n0. m + n ≤ # ar ∧ n0 ≤ m
shiftRight	array-copy	pf	Array[A] × Nat × Nat × Nat → Array[A] with λ ar, m, n, n0. m + n + n0 ≤ # ar
size	fsarray	c	Nat
subarray	array-copy	pf	Array[A] × Nat × Nat → Array[A] with λ ar, m, n. m + n ≤ # ar
subarray	array-fsarray	pf	FSArray[A] × Nat × Nat → Array[A] with λ fsar, m, n. m + n ≤ size