---

Step * of Lemma initseg_sum_shift

r:. u:. v: List.  (initseg_sum(r;[u / v]) = (u + initseg_sum(r - 1;v)))
BY
{ RepeatFor 3 ((D 0 THENA Auto)) }

1
1. r : @i
2. u : @i
3. v :  List@i
 initseg_sum(r;[u / v]) = (u + initseg_sum(r - 1;v))

---

Latex:


\mforall{}r:\mBbbN{}.  \mforall{}u:\mBbbZ{}.  \mforall{}v:\mBbbZ{}  List.    (initseg\_sum(r;[u  /  v])  =  (u  +  initseg\_sum(r  -  1;v)))


By

RepeatFor  3  ((D  0  THENA  Auto))

---

Home Index