---

Step * 1 2 1 1 1 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))
 l_sum(case [u / v] of [] => [] | a::as' => if 0 <z r + 1 then [a / firstn((r + 1) - 1;as')] else [] fi  esac) = x
BY
{ (AutoBoolCase 0 <z r + 1 THEN Reduce 0) }

1
1. r : @i
2. u : @i
3. v :  List@i
4. x : 
5. x = (u + initseg_sum(r - 1;v))
6. 0 < r + 1
 l_sum([u / firstn((r + 1) - 1;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{}  l\_sum(case  [u  /  v]  of 
                    []  =>  [] 
                    a::as'  =>
                      if  0  <z  r  +  1  then  [a  /  firstn((r  +  1)  -  1;as')]  else  []  fi   
esac)
=  x


By

(AutoBoolCase  \mkleeneopen{}0  <z  r  +  1\mkleeneclose{}\mcdot{}  THEN  Reduce  0)

---

Home Index