---

Step * 2 1 1 2 of Lemma maxsegsum_singleton


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

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

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

---

Latex:



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


By

D  0

---

Home Index