---

Step * 1 2 1 of Lemma initseg_sum_shift


1. r : @i
2. u : @i
3. v :  List@i
4. x : 
5. x = (u + initseg_sum(r - 1;v))
 initseg_sum(r;[u / v]) = (u + initseg_sum(r - 1;v))
BY
{ (RevHypSubst 5 0 THENA Auto) }

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

---

Latex:



1.  r  :  \mBbbN{}@i
2.  u  :  \mBbbZ{}@i
3.  v  :  \mBbbZ{}  List@i
4.  x  :  \mBbbZ{}
5.  x  =  (u  +  initseg\_sum(r  -  1;v))
\mvdash{}  initseg\_sum(r;[u  /  v])  =  (u  +  initseg\_sum(r  -  1;v))


By

(RevHypSubst  5  0  THENA  Auto)

---

Home Index