---

Step * 1 1 1 2 of Lemma maxsegsum_singleton


1. x : @i
 (p:||[x]||. q:{p..||[x]||}.  (x  seg_sum(p;q;[x]) ))  (a:||[x]||. b:{a..||[x]||}. (x = seg_sum(a;b;[x])))
BY
{ D 0 }

1
1. x : @i
 p:||[x]||. q:{p..||[x]||}.  (x  seg_sum(p;q;[x]) )

2
1. x : @i
 a:||[x]||. b:{a..||[x]||}. (x = seg_sum(a;b;[x]))

---

Latex:



1.  x  :  \mBbbZ{}@i
\mvdash{}  (\mforall{}p:\mBbbN{}||[x]||.  \mforall{}q:\{p..||[x]||\msupminus{}\}.    (x  \mgeq{}  seg\_sum(p;q;[x])  ))
\mwedge{}  (\mexists{}a:\mBbbN{}||[x]||.  \mexists{}b:\{a..||[x]||\msupminus{}\}.  (x  =  seg\_sum(a;b;[x])))


By

D  0

---

Home Index