---

Step * 1 of Lemma max_seg_sum_wf


1. [m] : 
2. [L] :  List
 max_seg_sum(m;L)  
BY
{ Unfold `max_seg_sum` 0 }

1
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))))  

---

Latex:



1.  [m]  :  \mBbbZ{}
2.  [L]  :  \mBbbZ{}  List
\mvdash{}  max\_seg\_sum(m;L)  \mmember{}  \mBbbP{}


By

Unfold  `max\_seg\_sum`  0

---

Home Index