Pour le dernier item, soit $k$, $0 \le k \le n-1$.
A la fin de la première exécution du processus \verb+update_elems+,
la valur de
-\ver+Xp[k]+ est $F(\verb+Xd[+k\verb+].v[0]+, \ldots,
+\verb+Xp[k]+ est $F(\verb+Xd[+k\verb+].v[0]+, \ldots,
\verb+Xd[+k\verb+].v[+n-1\verb+]+)$.
Ainsi par définition de $Xd$, ceci est égal à
$F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$. Grâce à l'équation \Equ{eq:correct_retrieve},
-\paragraph{Inductive case:}
+\paragraph{Induction:}
+Supposons maintenant que le lemme~\ref{lemma:execution} est établi jusqu'à
+l'itération $l$.
-Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$.
+Tout d'abord, si le domaine de définition de la fonction $M_{ij}^l$
+n'est pas vide, par hypothèse d'induction $M_{ij}^{l}(0)$ est
+$\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
+\right)$ où $c$ est $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-First, if domain of definition of the function $M_{ij}^l$ is not empty, by
-induction hypothesis $M_{ij}^{l}(0)$ is $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
-\right)$ where $c$ is $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-
-At iteration $l$, if $l < c + 1$ then the \verb+skip+ statement is executed in
+A l'itération $l$, si $l < c + 1$ alors \verb+skip+ statement is executed in
the \verb+fetch_values+ function. Thus, $M_{ij}^{l+1}(0)$ is equal to
$M_{ij}^{l}(0)$. Since $c > l-1$ then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$
is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. Obviously, this implies also that
