[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
#c .	matrix	f	Matrix → Nat
#oc	list-as-arrayinstance	f	Elem × Array → Nat
#r .	matrix	f	Matrix → Nat
. '	list-as-arrayinstance	f	Elem → Array
. ( . )	matrix	pf	Matrix × Nat × Nat → Elem with λ mx, r, c. r < #r mx ∧ c < #c mx
. ( . )	array	pf	Array × Nat → Elem with λ ar, n. n < # ar
. ( . := . )	matrix	pf	Matrix × Nat × Nat × Elem → Matrix with λ mx, r, c, a. r < #r mx ∧ c < #c mx
. ( . := . )	array	pf	Array × Nat × Elem → Array with λ ar, n, a. n < # ar
. * .	nat-mult	f	Nat × Nat → Nat
. + .	nat-basic	f	Nat × Nat → Nat
. + .	list-as-arrayinstance	f	Array × Array → Array
. + .	list-as-arrayinstance	f	Array × Elem → Array
. + .	array-listops	f	Elem × Array → Array
. ++ .	list-as-arrayinstance	f	Array × Elem → Array
. +1	nat-basic	f	Nat → Nat
. +2 .	list-as-arrayinstance	f	Elem × Elem → Array
. - .	nat	pf	Nat × Nat → Nat with λ n, m. n ≥ m
. -1	nat-basic	pf	Nat → Nat with λ n. n ≠ 0
. -1l .	list-as-arrayinstance	f	Array × Elem → Array
. -l .	list-as-arrayinstance	f	Array × Elem → Array
. -p .	list-as-arrayinstance	f	Array × Nat → Array
. < .	nat-basic	p	Nat × Nat
. < .	array-listops	p	Array × Array
. > .	nat	p	Nat × Nat
. [ . := . ]c	rowcol-upd	pf	Matrix × Nat × Array → Matrix with λ mx, c, a. c < #c mx ∧ # a = #r mx
. [ . := . ]r	rowcol-upd	pf	Matrix × Nat × Array → Matrix with λ mx, r, a. r < #r mx ∧ # a = #c mx
. [ . ]c	matrix+array	pf	Matrix × Nat → Array with λ mx, c. c < #c mx
. [ . ]r	matrix+array	pf	Matrix × Nat → Array with λ mx, r. r < #r mx
. \ .	list-as-arrayinstance	f	Array × Array → Array
. ∈ .	list-as-arrayinstance	p	Elem × Array
. ∪ .	list-as-arrayinstance	f	Array × Array → Array
. ≤ .	nat	p	Nat × Nat
. ≥ .	nat	p	Nat × Nat
. ⊆ .	list-as-arrayinstance	p	Array × Array
. ⊆m .	list-as-arrayinstance	p	Array × Array
. ⊑ .	list-as-arrayinstance	p	Array × Array
. ⊒ .	list-as-arrayinstance	p	Array × Array
. butlast	list-as-arrayinstance	pf	Array → Array with λ x. x ≠ []
. first	array-listops	pf	Array → Elem with λ ar. ar ≠ []
. last	list-as-arrayinstance	pf	Array → Elem with λ x. x ≠ []
. rest	array-listops	pf	Array → Array with λ ar. ar ≠ []
. toArc	rowcol-upd	f	Matrix → Array
. toArr	rowcol-upd	f	Matrix → Array
[]	array-listops	c	Array
Array	array	s
Elem	elem	s
Matrix	matrix	s
Nat	nat-basic	s
a	rowcol-upd	v	Array
butlastn	list-as-arrayinstance	pf	Nat × Array → Array with λ n, x. n ≤ # x
c	rowcol-upd	v	Nat
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
disj	list-as-arrayinstance	p	Array × Array
dups	list-as-arrayinstance	p	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
fillfirst	list-as-arrayinstance	f	Nat × Elem × Array → Array
filter	list-as-arrayinstance	f	Array × Array → Array
firstn	list-as-arrayinstance	pf	Nat × Array → Array with λ n, x. n ≤ # x
frome	list-as-arrayinstance	f	Array × Elem → Array
i	rowcol-upd	v	Elem
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
j	rowcol-upd	v	Elem
lastn	list-as-arrayinstance	pf	Nat × Array → Array with λ n, x. n ≤ # x
m	rowcol-upd	v	Nat
mkarray	array	f	Nat → Array
mklist	list-as-arrayinstance	f	Elem × Nat → Array
mkmatrix	matrix	f	Nat × Nat × Elem → Matrix
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
mx	rowcol-upd	v	Matrix
n	rowcol-upd	v	Nat
perm	list-as-arrayinstance	p	Array × Array
pos	list-as-arrayinstance	f	Elem × Array → Nat
r	rowcol-upd	v	Nat
resize	array-copy	f	Array × Nat → Array
restn	list-as-arrayinstance	pf	Nat × Array → Array with λ n, x. n ≤ # x
rev	list-as-arrayinstance	f	Array → Array
rmdup	list-as-arrayinstance	f	Array → 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
sublist	list-as-arrayinstance	pf	Nat × Nat × Array → Array with λ n, m, x. n + m ≤ # x
toArc	rowcol-upd	f	Matrix × Nat → Array
toArr	rowcol-upd	f	Matrix × Nat → Array