---

Step * 1 1 of Lemma max_seg_sum_wf


1. [m] : 
2. [L] :  List
 ((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))))  
BY
{ Auto }

---

Latex:



1.  [m]  :  \mBbbZ{}
2.  [L]  :  \mBbbZ{}  List
\mvdash{}  ((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))))  \mmember{}  \mBbbP{}


By

Auto

---

Home Index