[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-list	f	elem × array → array
. + .	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
. .first	array-list	pf	array → elem with λ ar. ar ≠ []
. .rest	array-list	pf	array → array with λ ar. ar ≠ []
. < .	nat-basic	p	nat × nat
. < .	array-list	p	array × array
. > .	nat	p	nat × nat
. [ . ]	array	pf	array × nat × elem → array with λ ar, n, a. n < # ar
. [ . ]	array	pf	array × nat → elem with λ ar, n. n < # ar
. ∈ .	array-copy	p	elem × array
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
[]	array-list	c	array
a	elem	v	elem
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar10	array-list	v	array
ar2	array	v	array
ar3	array-list	v	array
ar4	array-list	v	array
ar5	array-list	v	array
ar6	array-list	v	array
ar7	array-list	v	array
ar8	array-list	v	array
ar9	array-list	v	array
array	array	s
b	elem	v	elem
c	elem	v	elem
cmp	array-copy	pp	array × elem × nat × nat with λ ar, a, m, n. m + n ≤ # ar
cmp	array-copy	pp	array × nat × array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
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
idrange	array-copy	pp	array × nat × nat with λ ar, m, n. m + n ≤ # ar
m	nat-basic	v	nat
m0	array-copy	v	nat
mkarray	array	f	nat → array
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
rev	array-copy	pf	array × nat → array with λ ar, n. n ≤ # ar
rev	array-copy	f	array → array
subarray	array-copy	pf	array × nat × nat → array with λ ar, m, n. m + n ≤ # ar