---

Step * 2 1 1 2 2 of Lemma maxsegsum_singleton


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

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

---

Latex:



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


By

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

---

Home Index