---

Step * 1 2 2 1 of Lemma maxsegsum_sqexists


1. L :  List
2. u : 
3. u1 : 
4. v :  List
5. p1 : 
6. p2 : 
7. [%3] : max_seg_sum(p1;[u1 / v])  max_initseg_sum(p2;[u1 / v])
 p:{  | let m,i = p 
             in max_seg_sum(m;[u; u1 / v])  max_initseg_sum(i;[u; u1 / v])}
BY
{ ((InstConcl [<imax(p1;imax(u;u + p2)), imax(u;u + p2)>] THENA Auto) THEN Reduce 0) }

1
1. L :  List
2. u : 
3. u1 : 
4. v :  List
5. p1 : 
6. p2 : 
7. max_seg_sum(p1;[u1 / v])  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])

---

Latex:



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


By

((InstConcl  [\mkleeneopen{}<imax(p1;imax(u;u  +  p2)),  imax(u;u  +  p2)>\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Reduce  0)

---

Home Index