---

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


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

---

Latex:



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


By

Auto

---

Home Index