---

Step * 1 1 1 2 2 of Lemma maxsegsum_singleton


1. x : @i
 a:||[x]||. b:{a..||[x]||}. (x = seg_sum(a;b;[x]))
BY
{ (InstConcl [0;0] THENA Auto) }

1
1. x : @i
 x = seg_sum(0;0;[x])

---

Latex:



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


By

(InstConcl  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}

---

Home Index