---

Step * of Lemma maxsegsum_sqexists

L: List. (p:{  | let m,i = p in max_seg_sum(m;L)  max_initseg_sum(i;L)})
BY
{ (D 0 THENA Auto) }

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

---

Latex:


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


By

(D  0  THENA  Auto)

---

Home Index