Nuprl Definition : max_initseg_sum
max_initseg_sum(i;L) ==
((L = []) 
(i = 0))
((
h:
. t: List. (L = [h / t])) (
r:
||L||. (i 
initseg_sum(r;L) )) (c:||L||. (i = initseg_sum(c;L))))
Definitions occuring in Statement :
initseg_sum: initseg_sum(r;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_initseg_sum
max\_initseg\_sum(i;L) ==
((L = []) \mwedge{} (i = 0))
\mvee{} ((\mexists{}h:\mBbbZ{}. \mexists{}t:\mBbbZ{} List. (L = [h / t]))
\mwedge{} (\mforall{}r:\mBbbN{}||L||. (i \mgeq{} initseg\_sum(r;L) ))
\mwedge{} (\mexists{}c:\mBbbN{}||L||. (i = initseg\_sum(c;L))))
Date html generated:
2014_01_21-PM-02_38_46
Last ObjectModification:
2013_10_25-AM-09_17_11
Home
Index