---

Step * 2 1 of Lemma maxsegsum_singleton


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]))))
BY
{ (OrRight THENA Auto) }

1
1. x : @i
 (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{}  (([x]  =  [])  \mwedge{}  (x  =  0))
\mvee{}  ((\mexists{}h:\mBbbZ{}.  \mexists{}t:\mBbbZ{}  List.  ([x]  =  [h  /  t]))
    \mwedge{}  (\mforall{}r:\mBbbN{}||[x]||.  (x  \mgeq{}  initseg\_sum(r;[x])  ))
    \mwedge{}  (\mexists{}c:\mBbbN{}||[x]||.  (x  =  initseg\_sum(c;[x]))))


By

(OrRight  THENA  Auto)

---

Home Index