---

Step * 1 2 2 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_seg_sum(imax(p1;imax(u;u + p2));[u; u1 / v])  max_initseg_sum(imax(u;u + p2);[u; u1 / v])
BY
{ Assert max_initseg_sum(imax(u;u + p2);[u; u1 / v])
           (max_initseg_sum(imax(u;u + p2);[u; u1 / v])  max_seg_sum(imax(p1;imax(u;u + p2));[u; u1 / v])) }

1
.....assertion..... 
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])
 (max_initseg_sum(imax(u;u + p2);[u; u1 / v])  max_seg_sum(imax(p1;imax(u;u + p2));[u; u1 / v]))

2
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])
9. max_initseg_sum(imax(u;u + p2);[u; u1 / v])
 (max_initseg_sum(imax(u;u + p2);[u; u1 / v])  max_seg_sum(imax(p1;imax(u;u + p2));[u; u1 / v]))
 max_seg_sum(imax(p1;imax(u;u + p2));[u; u1 / v])  max_initseg_sum(imax(u;u + p2);[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\_seg\_sum(imax(p1;imax(u;u  +  p2));[u;  u1  /  v])  \mwedge{}  max\_initseg\_sum(imax(u;u  +  p2);[u;  u1  /  v])


By

Assert  \mkleeneopen{}max\_initseg\_sum(imax(u;u  +  p2);[u;  u1  /  v])
                \mwedge{}  (max\_initseg\_sum(imax(u;u  +  p2);[u;  u1  /  v])
                    {}\mRightarrow{}  max\_seg\_sum(imax(p1;imax(u;u  +  p2));[u;  u1  /  v]))\mkleeneclose{}\mcdot{}

---

Home Index