[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
# .	int-array	f	int-array → nat
. % .	int-div	pf	int × int → int with λ i, j. j ≠ 0
. * .	int-mult	f	int × int → int
. + .	int-basic2	f	int × int → int
. + .	nat-basic	f	nat × nat → nat
. +1	int-basic1	f	int → int
. +1	nat-basic	f	nat → nat
. - .	nat	pf	nat × nat → nat with λ n, m. n ≥ m
. - .	int-abs	f	int × int → int
. -1	int-basic1	f	int → int
. -1	nat-basic	pf	nat → nat with λ n. n ≠ 0
. / .	int-div	pf	int × int → int with λ i, j. j ≠ 0
. < .	int-basic1	p	int × int
. < .	nat-basic	p	nat × nat
. > .	nat	p	nat × nat
. > .	int-abs	p	int × int
. [ . ]	int-array	pf	int-array × nat × int → int-array with λ ar, n, i. n < # ar
. [ . ]	int-array	pf	int-array × nat → int with λ ar, n. n < # ar
. ∈ .	int-array	p	int × int-array
. ≤ .	int-abs	p	int × int
. ≤ .	nat	p	nat × nat
. ≥ .	nat	p	nat × nat
. ≥ .	int-abs	p	int × int
~ .	int-abs	f	int → int
a	kadane	v	int-array
abs	int-abs	f	int → int
ar	int-array	v	int-array
ar0	int-array	v	int-array
ar1	int-array	v	int-array
ar2	int-array	v	int-array
cmp	int-array	pp	int-array × int × nat × nat with λ ar, i, m, n. m + n ≤ # ar
cmp	int-array	pp	int-array × nat × int-array × nat × nat with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
cmp	int-array	p	int-array × int
copy	int-array	pf	int-array × nat × int-array × nat × nat → int-array with λ ar, m, ar0, m0, n. m + n ≤ # ar ∧ m0 + n ≤ # ar0
fill	int-array	f	int-array × int → int-array
fill	int-array	pf	int-array × int × nat × nat → int-array with λ ar, i, n, m. n + m ≤ # ar
i	int-basic1	v	int
i0	int-basic1	v	int
id○	int-array	p	int-array × int-array × nat
idrange	int-array	pp	int-array × nat × nat with λ ar, m, n. m + n ≤ # ar
int	int-basic1	s
int-array	int-array	s
j	int-basic1	v	int
j0	int-basic1	v	int
m	nat-basic	v	nat
m0	array-copy	v	nat
max_ending_here	kadane	v	int
max_so_far	kadane	v	int
maxSubArraySum#	kadane	pr	int-array : : int
maximum-suffix-sum	int-array-ops	p	int-array × nat × int
maximum-sum	int-array-ops	p	int-array × int
maximum-sum	int-array-ops	p	int-array × nat × nat × int
mkarray	int-array	f	nat → int-array
n	nat-basic	v	nat
n0	nat-basic	v	nat
n1	nat-basic	v	nat
nat	nat-basic	s
res	kadane	v	int
rev	int-array	pf	int-array × nat → int-array with λ ar, n. n ≤ # ar
rev	int-array	f	int-array → int-array
size	kadane	v	nat
subarray	int-array	pf	int-array × nat × nat → int-array with λ ar, m, n. m + n ≤ # ar
suffix-upper-bound	int-array-ops	p	int-array × int
sum	int-array-ops	f	int-array × nat × nat → int
upper-bound	int-array-ops	p	int-array × int