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