---

Step * 1 1 1 2 2 1 1 of Lemma maxsegsum_singleton


1. x : @i
2. seg_sum(0;0;[x]) = initseg_sum(0;[x])
3. initseg_sum(0;[x]) = x
 x = seg_sum(0;0;[x])
BY
{ Auto }

---

Latex:



1.  x  :  \mBbbZ{}@i
2.  seg\_sum(0;0;[x])  =  initseg\_sum(0;[x])
3.  initseg\_sum(0;[x])  =  x
\mvdash{}  x  =  seg\_sum(0;0;[x])


By

Auto

---

Home Index