---

Step * 1 1 of Lemma initseg_sum0


1. h : @i
2. t :  List@i
 l_sum(firstn(0 + 1;[h / t])) = h
BY
{ (RecUnfold `firstn` 0 THEN Reduce 0) }

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

---

Latex:



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


By

(RecUnfold  `firstn`  0  THEN  Reduce  0)

---

Home Index