[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
. + .	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
. < .	oelem	p	elem × elem
. < .	nat-basic	p	nat × nat
. > .	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
. ≤ .	oarray-sorted	p	elem × elem
. ≥ .	nat	p	nat × nat
A	oarray-sorted	v	array
A0	oarray-sorted	v	array
a	elem	v	elem
ar	array	v	array
ar0	array	v	array
ar1	array	v	array
ar2	array	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	p	array × elem
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
i	oarray-sorted	v	nat
i0	oarray-sorted	v	nat
id○	array-copy	p	array × array × nat
idrange	array-copy	pp	array × nat × nat with λ ar, m, n. m + n ≤ # ar
j	oarray-sorted	v	nat
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
sorted	oarray-sorted	p	array × nat × nat
subarray	array-copy	pf	array × nat × nat → array with λ ar, m, n. m + n ≤ # ar
x	oarray-sorted	v	elem
y	oarray-sorted	v	elem