---

Step * of Lemma seg_sum0

r:. L: List.  (seg_sum(0;r;L) = initseg_sum(r;L))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

1
1. r : @i
2. L :  List@i
 seg_sum(0;r;L) = initseg_sum(r;L)

---

Latex:


\mforall{}r:\mBbbZ{}.  \mforall{}L:\mBbbZ{}  List.    (seg\_sum(0;r;L)  =  initseg\_sum(r;L))


By

RepeatFor  2  ((D  0  THENA  Auto))

---

Home Index