---

Step * 1 of Lemma maxsegsum_sqexists


1. L :  List@i
 p:{  | let m,i = p 
             in max_seg_sum(m;L)  max_initseg_sum(i;L)}
BY
{ ListInd 1 }

1
1. L :  List
 p:{  | let m,i = p 
             in max_seg_sum(m;[])  max_initseg_sum(i;[])}

2
1. L :  List
2. u : 
3. v :  List
4. p:{  | let m,i = p 
              in max_seg_sum(m;v)  max_initseg_sum(i;v)}
 p:{  | let m,i = p 
             in max_seg_sum(m;[u / v])  max_initseg_sum(i;[u / v])}

---

Latex:



1.  L  :  \mBbbZ{}  List@i
\mvdash{}  \mexists{}p:\{\mBbbZ{}  \mtimes{}  \mBbbZ{}|  let  m,i  =  p 
                          in  max\_seg\_sum(m;L)  \mwedge{}  max\_initseg\_sum(i;L)\}


By

ListInd  1

---

Home Index