---

Step * 1 1 of Lemma seg_sum_shift

.....assertion..... 
1. p : @i
2. q : @i
3. L :  List@i
 x:. (x = seg_sum(p - 1;q - 1;tl(L)))
BY
{ (InstConcl [seg_sum(p - 1;q - 1;tl(L))] THEN Auto) }

---

Latex:


.....assertion..... 
1.  p  :  \mBbbN{}\msupplus{}@i
2.  q  :  \mBbbN{}\msupplus{}@i
3.  L  :  \mBbbZ{}  List@i
\mvdash{}  \mexists{}x:\mBbbZ{}.  (x  =  seg\_sum(p  -  1;q  -  1;tl(L)))


By

(InstConcl  [\mkleeneopen{}seg\_sum(p  -  1;q  -  1;tl(L))\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index