---

Step * of Lemma seg_sum_shift

p,q:. L: List.  (seg_sum(p;q;L) = seg_sum(p - 1;q - 1;tl(L)))
BY
{ RepeatFor 3 ((D 0 THENA Auto)) }

1
1. p : @i
2. q : @i
3. L :  List@i
 seg_sum(p;q;L) = seg_sum(p - 1;q - 1;tl(L))

---

Latex:


\mforall{}p,q:\mBbbN{}\msupplus{}.  \mforall{}L:\mBbbZ{}  List.    (seg\_sum(p;q;L)  =  seg\_sum(p  -  1;q  -  1;tl(L)))


By

RepeatFor  3  ((D  0  THENA  Auto))

---

Home Index