---

Step * 1 2 1 1 1 1 of Lemma seg_sum_shift


1. p : @i
2. q : @i
3. L :  List@i
4. x : 
5. x = seg_sum(p - 1;q - 1;tl(L))
 l_sum(firstn((q + 1) - p;if p z 0 then L else nth_tl(p - 1;tl(L)) fi )) = x
BY
{ AutoBoolCase p z 0 }

1
1. p : @i
2. (p  0)
3. q : @i
4. L :  List@i
5. x : 
6. x = seg_sum(p - 1;q - 1;tl(L))
 l_sum(firstn((q + 1) - p;nth_tl(p - 1;tl(L)))) = x

---

Latex:



1.  p  :  \mBbbN{}\msupplus{}@i
2.  q  :  \mBbbN{}\msupplus{}@i
3.  L  :  \mBbbZ{}  List@i
4.  x  :  \mBbbZ{}
5.  x  =  seg\_sum(p  -  1;q  -  1;tl(L))
\mvdash{}  l\_sum(firstn((q  +  1)  -  p;if  p  \mleq{}z  0  then  L  else  nth\_tl(p  -  1;tl(L))  fi  ))  =  x


By

AutoBoolCase  \mkleeneopen{}p  \mleq{}z  0\mkleeneclose{}\mcdot{}

---

Home Index