---

Step * 1 1 1 2 1 of Lemma maxsegsum_singleton


1. x : @i
 p:||[x]||. q:{p..||[x]||}.  (x  seg_sum(p;q;[x]) )
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

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

---

Latex:



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


By

RepeatFor  2  ((D  0  THENA  Auto))\mcdot{}

---

Home Index