Step
*
1
2
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(firstn(r + 1;[u / v])) = x
BY
{ RecUnfold `firstn` 0 }
1
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
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(firstn(r  +  1;[u  /  v]))  =  x
By
RecUnfold  `firstn`  0
Home
Index