Nuprl Definition : max_seg_sum
max_seg_sum(m;L) ==
((L = []) 
(m = 0))
((
h:
. t: List. (L = [h / t]))
(
p:
||L||. q:{p..||L||
}. (m 
seg_sum(p;q;L) ))
(a:||L||. b:{a..||L||}. (m = seg_sum(a;b;L))))
Definitions occuring in Statement :
seg_sum: seg_sum(p;q;L),
length: ||as||,
nil: [],
cons: [a / b],
list: T List,
int_seg: {i..j},
ge: i j ,
all: x:A. B[x],
exists: x:A. B[x],
or: P Q,
and: P Q,
natural_number: $n,
int: ,
equal: s = t
FDL editor aliases :
max_seg_sum
max\_seg\_sum(m;L) ==
((L = []) \mwedge{} (m = 0))
\mvee{} ((\mexists{}h:\mBbbZ{}. \mexists{}t:\mBbbZ{} List. (L = [h / t]))
\mwedge{} (\mforall{}p:\mBbbN{}||L||. \mforall{}q:\{p..||L||\msupminus{}\}. (m \mgeq{} seg\_sum(p;q;L) ))
\mwedge{} (\mexists{}a:\mBbbN{}||L||. \mexists{}b:\{a..||L||\msupminus{}\}. (m = seg\_sum(a;b;L))))
Date html generated:
2014_01_21-PM-02_38_42
Last ObjectModification:
2013_10_25-AM-09_11_38
Home
Index