---

Step * 1 of Lemma seg_sum0


1. r : @i
2. L :  List@i
 seg_sum(0;r;L) = initseg_sum(r;L)
BY
{ RepUR ``seg_sum segment initseg_sum`` 0 }

1
1. r : @i
2. L :  List@i
 l_sum(firstn((r + 1) - 0;L)) = l_sum(firstn(r + 1;L))

---

Latex:



1.  r  :  \mBbbZ{}@i
2.  L  :  \mBbbZ{}  List@i
\mvdash{}  seg\_sum(0;r;L)  =  initseg\_sum(r;L)


By

RepUR  ``seg\_sum  segment  initseg\_sum``  0

---

Home Index