---

Step * 1 1 1 1 1 of Lemma initseg_sum0


1. h : @i
2. t :  List@i
3. firstn(0;t) ~ []
 l_sum([h]) = h
BY
{ RepUR ``l_sum`` 0 }

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

---

Latex:



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


By

RepUR  ``l\_sum``  0

---

Home Index