---

Step * 2 of Lemma maxsegsum_singleton


1. x : @i
 max_initseg_sum(x;[x])
BY
{ Unfold `max_initseg_sum` 0 }

1
1. x : @i
 (([x] = [])  (x = 0))
 ((h:. t: List. ([x] = [h / t]))
   (r:||[x]||. (x  initseg_sum(r;[x]) ))
   (c:||[x]||. (x = initseg_sum(c;[x]))))

---

Latex:



1.  x  :  \mBbbZ{}@i
\mvdash{}  max\_initseg\_sum(x;[x])


By

Unfold  `max\_initseg\_sum`  0

---

Home Index