---

Step * 1 2 2 1 1 1 1 1 of Lemma maxsegsum_sqexists


1. L :  List
2. u : 
3. u1 : 
4. v :  List
5. p1 : 
6. p2 : 
7. max_seg_sum(p1;[u1 / v])
8. max_initseg_sum(p2;[u1 / v])
 max_initseg_sum(imax(u;u + p2);[u; u1 / v])
BY
{ Unfold `max_initseg_sum` 0 }

1
1. L :  List
2. u : 
3. u1 : 
4. v :  List
5. p1 : 
6. p2 : 
7. max_seg_sum(p1;[u1 / v])
8. max_initseg_sum(p2;[u1 / v])
 (([u; u1 / v] = [])  (imax(u;u + p2) = 0))
 ((h:. t: List. ([u; u1 / v] = [h / t]))
   (r:||[u; u1 / v]||. (imax(u;u + p2)  initseg_sum(r;[u; u1 / v]) ))
   (c:||[u; u1 / v]||. (imax(u;u + p2) = initseg_sum(c;[u; u1 / v]))))

---

Latex:



1.  L  :  \mBbbZ{}  List
2.  u  :  \mBbbZ{}
3.  u1  :  \mBbbZ{}
4.  v  :  \mBbbZ{}  List
5.  p1  :  \mBbbZ{}
6.  p2  :  \mBbbZ{}
7.  max\_seg\_sum(p1;[u1  /  v])
8.  max\_initseg\_sum(p2;[u1  /  v])
\mvdash{}  max\_initseg\_sum(imax(u;u  +  p2);[u;  u1  /  v])


By

Unfold  `max\_initseg\_sum`  0

---

Home Index