---

Step * 1 2 of Lemma maxsegsum_sqexists


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])}
BY
{ D 3 }

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

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

---

Latex:



1.  L  :  \mBbbZ{}  List
2.  u  :  \mBbbZ{}
3.  v  :  \mBbbZ{}  List
4.  \mexists{}p:\{\mBbbZ{}  \mtimes{}  \mBbbZ{}|  let  m,i  =  p 
                            in  max\_seg\_sum(m;v)  \mwedge{}  max\_initseg\_sum(i;v)\}
\mvdash{}  \mexists{}p:\{\mBbbZ{}  \mtimes{}  \mBbbZ{}|  let  m,i  =  p 
                          in  max\_seg\_sum(m;[u  /  v])  \mwedge{}  max\_initseg\_sum(i;[u  /  v])\}


By

D  3

---

Home Index