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