Step
*
1
of Lemma
seg_sum_shift
1. p : @i
2. q : @i
3. L :  List@i
 seg_sum(p;q;L) = seg_sum(p - 1;q - 1;tl(L))
BY
{ Assert x:. (x = seg_sum(p - 1;q - 1;tl(L))) }
1
.....assertion..... 
1. p : @i
2. q : @i
3. L :  List@i
 x:. (x = seg_sum(p - 1;q - 1;tl(L)))
2
1. p : @i
2. q : @i
3. L :  List@i
4. x:. (x = seg_sum(p - 1;q - 1;tl(L)))
 seg_sum(p;q;L) = seg_sum(p - 1;q - 1;tl(L))
Latex:
1.  p  :  \mBbbN{}\msupplus{}@i
2.  q  :  \mBbbN{}\msupplus{}@i
3.  L  :  \mBbbZ{}  List@i
\mvdash{}  seg\_sum(p;q;L)  =  seg\_sum(p  -  1;q  -  1;tl(L))
By
Assert  \mkleeneopen{}\mexists{}x:\mBbbZ{}.  (x  =  seg\_sum(p  -  1;q  -  1;tl(L)))\mkleeneclose{}\mcdot{}
Home
Index