Deriving recursive definition from function specification Given this function specification, where name xs is bound to a list, # denotes its cardinality and . is the list index operator...

$$\left( \sum i: 0 \leq i &lt; \#xs: xs.i * (i + 1) \right)$$

I need to derive a recursive function using induction.

Base case: []

\begin{align}
 \left( \sum i: 0 \leq i &lt; \#[]: xs.i * (i + 1) \right) &amp;&amp; \text{(Textual substitution - xs is free)} \\
 \left( \sum i: 0 \leq i &lt; 0: xs.i * (i + 1) \right) &amp;&amp; \text{(Def. of #)} \\
 \left( \sum i: False: xs.i * (i + 1) \right) &amp;&amp; \text{(Algebra)} \\
 \left( \sum i: 0 \leq i &lt; \#xs: xs.i * (i + 1) \right) &amp;&amp; \text{(Empty range)} 
\end{align}

Inductive case: (x:xs)

\begin{align}
  \left( \sum i: 0 \leq i &lt; \#(x:xs): (x:xs).i * (i + 1) \right) &amp;&amp; \text{(Textual substitution - xs is free)} \\
  \left( \sum i: 0 \leq i &lt; 1 + \#xs: (x:xs).i * (i + 1) \right) &amp;&amp; \text{(Def. of #)}
\end{align}

How can I proceed from here ?
Your notation and understanding are pretty good. 

It is easier to consider (xs:x) as the inductive case instead of (x:xs)

\begin{align}
\sum_{i:\ 0 \leq i &lt; \#(xs:x)} &amp;(xs:x).i * (i + 1)\\
&amp;=\sum _{i:\ 0 \leq i &lt; \#xs+1} (x:xs).i * (i + 1) \\
&amp;=\sum_{i:\ 0 \leq i &lt; \#xs} (xs:x).i * (i + 1)+\sum_{i:\ i=\#xs}(xs:x).i * (i + 1)\\
&amp;=\sum_{i:\ 0 \leq i &lt; \#xs} xs.i * (i + 1)+x*(\#xs+1),\\
\end{align}
where we assume that list index starts with 0.

If we denote the function by $f$, the above equality becomes 
$$ f(xs:x) = f(xs) + x*(\#xs+1), $$
which is the recursive step of a recursive definition.

The base case, as you have indicated, is 
$$ f([]) =  \sum_{ i:\ 0 \leq i &lt; 0} [].i * (i + 1)  =  \sum_{i: \text{ empty set}}[].i * (i + 1) =0.$$



Exercise. Derive the following recursive formula of the same function $f$.
$$ f(x:xs) = f(xs) + t(xs)+ x, $$
where $$t(xs)=\sum_{i:\ 0 \leq i &lt; \#(xs)} xs.i,$$
the sum of items in $xs$.