---

Step * 1 of Lemma initseg_sum0


1. h : @i
2. t :  List@i
 initseg_sum(0;[h / t]) = h
BY
{ Unfold `initseg_sum` 0 }

1
1. h : @i
2. t :  List@i
 l_sum(firstn(0 + 1;[h / t])) = h

---

Latex:



1.  h  :  \mBbbZ{}@i
2.  t  :  \mBbbZ{}  List@i
\mvdash{}  initseg\_sum(0;[h  /  t])  =  h


By

Unfold  `initseg\_sum`  0

---

Home Index