---

Step * 1 1 of Lemma maxsegsum_sqexists


1. L :  List
 p:{  | let m,i = p 
             in max_seg_sum(m;[])  max_initseg_sum(i;[])}
BY
{ ((InstConcl [<0, 0>] THENA Auto) THEN Reduce 0) }

1
1. L :  List
 max_seg_sum(0;[])  max_initseg_sum(0;[])

---

Latex:



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


By

((InstConcl  [\mkleeneopen{}ɘ,  0>\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Reduce  0)

---

Home Index