---

Step * 1 2 1 1 of Lemma maxsegsum_sqexists


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

---

Latex:



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


By

(InstLemma  `maxsegsum\_singleton`  [\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index