---

Step * 2 1 1 2 2 1 of Lemma maxsegsum_singleton


1. x : @i
 x = initseg_sum(0;[x])
BY
{ (InstLemma `initseg_sum0` [x;[]] THENA Auto) }

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

---

Latex:



1.  x  :  \mBbbZ{}@i
\mvdash{}  x  =  initseg\_sum(0;[x])


By

(InstLemma  `initseg\_sum0`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index