-\item if $\dom(M_{ij}^{l})=\{0\}$ and $\forall k\, . \, k\ge l \Rightarrow
- D^{k}_{ji} \neq l$ is established then $\dom(M_{ij}^{l+1})$ is empty and the
- first item of the lemma is established;
-\item if $\dom(M_{ij}^{l})=\{0\}$ and $\exists k\, . \, k\ge l \land D^{k}_{ji}
- = l$ is established then $M_{ij}^{l+1}(0)$ is $(\verb+Xp[i]+,l,c_{ij})$ that
- is added in the \verb+diffuse_values+ function s.t.\linebreak $c_{ij} =
- \min\{k \mid D^{k}_{ji} = l \} $. Let us prove that we can express
- $M_{ij}^{l+1}(0)$ as $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ where
- $c'$ is $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$. First, it is not hard to
- establish that $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ and thus
- $c_{ij} \geq c'$. Next, since $\dom(M_{ij}^{l})=\{0\}$, then between
- iterations $D_{ji}^{c}+1$ and $l-1$, the \texttt{diffuse\_values} function has
- not updated $M_{ij}$. Formally we have
+\item si $\dom(M_{ij}^{l})=\{0\}$ et $\forall k\, . \, k\ge l \Rightarrow
+ D^{k}_{ji} \neq l$ sont vraies, alors $\dom(M_{ij}^{l+1})$ est vide et le premier
+ item du lemme est vérifié;
+\item si $\dom(M_{ij}^{l})=\{0\}$ et $\exists k\, . \, k\ge l \land D^{k}_{ji}
+ = l$ sont vraies, alors $M_{ij}^{l+1}(0)$ vaut $(\verb+Xp[i]+,l,c_{ij})$ qui est ajouté
+ dans la fonction \verb+diffuse_values+ de sorte que $c_{ij} =
+ \min\{k \mid D^{k}_{ji} = l \} $.
+ Prouvons qu'on peut exprimer
+ $M_{ij}^{l+1}(0)$ comme $\left(X_i^{D_{ji}^{c'}},D_{ji}^{c'},c' \right)$ où
+ $c'$ vaut $\min\{k | D_{ji}^k > D_{ji}^{l-1} \}$.
+ Tout d'abord, il n'est pas difficile de prouver que
+ $D_{ji}^{c_{ij}}= l \geq D_{ji}^{l} > D_{ji}^{l-1}$ et que
+ $c_{ij} \geq c'$.
+ Ensuite, comme $\dom(M_{ij}^{l})=\{0\}$, alors, entre les
+ itérations $D_{ji}^{c}+1$ et $l-1$, la fonction \texttt{diffuse\_values} n'a pas mis à jour
+ $M_{ij}$. On a ainsi la propriété
