---

Step * 2 1 1 2 1 of Lemma maxsegsum_singleton


1. x : @i
 r:||[x]||. (x  initseg_sum(r;[x]) )
BY
{ (D 0 THENA Auto) }

1
1. x : @i
2. r : ||[x]||@i
 x  initseg_sum(r;[x]) 

---

Latex:



1.  x  :  \mBbbZ{}@i
\mvdash{}  \mforall{}r:\mBbbN{}||[x]||.  (x  \mgeq{}  initseg\_sum(r;[x])  )


By

(D  0  THENA  Auto)

---

Home Index