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


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


Latex:



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


By

Auto




Home Index