+
+Let us introduce an ordering $\preceq$ between classes. Formally, \class{p}
+$\preceq$ \class{q} if there exists a path of length $\alpha$
+($0<\alpha<|\mathcal{K}|$) from an element of \class{p} to an element of
+\class{q}. One can remark that if \class{p}$\preceq$\class{q}, then it is not
+possible to also have \class{q}$\preceq$\class{p}.
+
+% \begin{lemma}
+% The relation $ \preceq$ is a partial order
+% \begin{Proof}
+% Reflexivity is established since for any $p_0 \in [p]$ there exists a path
+% of length 0 from $p_0$ to $p_0$.
+% For antisymmetry, suppose there exists two classes $[p]$ and
+% $[q]$ such that $[p] \preceq [q]$ and $[q] \preceq [p]$.
+% There exists then $p_0,p'_0 \in [p]$, $q_0, q'_0 \in [q]$ with paths
+% from $p_0$ to $q_0$ and from $q'_0$ to $p_0$.
+% Thus, elements $p_0$, $p'_0$, $q_0$ and $q'_0$ belong to the same
+% strongly connected component and then
+% $[p]$ = $[q]$. Transitivity is obviously established.
+% \end{Proof}
+% \end{lemma}
+
+\begin{lemma}
+ There exists a renaming process method that assigns new identifier numbers to
+ processes $i\in$ \class{p} and $j \in$ \class{q} s.t. $i \le j$ provided
+ \class{p} $\preceq$ \class{q}.
+ \begin{Proof}
+ % We first define a renaming process method and later show that it fulfills
+ % the requirements.
+
+ First of all, let \class{p_1}, \ldots, \class{p_l} be classes of
+ $n_1$,\ldots, $n_l$ elements respectively that do not depend on other
+ classes. Elements of \class{p_1} are renamed by $1$, \ldots, $n_1$ and
+ elements of \class{p_i}, $2 \le i \le l$ are renamed by $1+
+ \Sigma_{k=1}^{i-1} n_k$, \ldots, $\Sigma_{k=1}^{i} n_k$. We now consider
+ the classes \class{p_1}, \ldots, \class{p_{l'}} whose elements have been
+ renamed and let $m$ be the maximum index of elements of \class{p_1}, \ldots,
+ \class{p_{l'}}. Given another class \class{p} that exclusively depends on
+ some \class{p_i}, $1 \le i \le l'$ and that contains $k$ elements. Elements
+ of \class{p} are then renamed by $m+1$, \ldots, $m+k$.
+% In the end for remaining classes, i.e. those which do not depend on anything,
+% elements are arbitrarily numbered.
+ This renaming process method has then been applied on $l'+1$ classes. It
+ ends since it decreases the number of elements to assign a number. Notice
+ that this process is not determinist.
+
+ We are then ready to prove that this renaming method verifies property
+ expressed in the lemma. The proof is done by induction on the length $l$ of
+ the longest dependency path between classes.
+
+ First, if \class{p} $\preceq$ \class{q} and \class{q} immediately depends on
+ \class{p}, \textit{i.e.} the longest path from elements of \class{p} to
+ elements of \class{q} has length 1. Due to the renaming method, all element
+ numbers of \class{q} are greater than the ones of \class{p} and the result
+ is established. Let \class{p} and \class{q} s.t. the longest dependency
+ path from \class{p} to \class{q} has length $l+1$. Then there exists some
+ \class{q'} s.t. \class{q} immediately depends on \class{q'} and the longest
+ dependency path from \class{p} and \class{q'} has length $l$. We have then
+ \class{q'} $\preceq$ \class{q} and then for all $k$, $j$ s.t. $k \in$
+ \class{q'} and $j \in$ \class{q}, $k \le j$. By induction hypothesis
+ \class{p} $\preceq$ \class{q'} and then for all $i$, $k$ s.t. $i \in$
+ \class{p} and $k \in$ \class{q'}, $i \le k$ and the result is established.
+ \end{Proof}
+\end{lemma}
+
+It can be noticed that the renaming process is inspired from \emph{graphs by
+ layer} of Golès and Salinas~\cite{GS08}. It ensures that identifier numbers of
+a layer are greater than all the identifier numbers of any lower layers.
+
+\begin{xpl}
+ We have \class{1} $=\{1,2\}$, \class{3} $=\{3\}$ and \class{4} $=\{4,5\}$.
+ Processes numbers are already compliant with the order $\preceq$.
+\end{xpl}
+
+\begin{Proof}[of Theorem~\ref{th:cvg}]
+
+ % Since $\preceq$ is a partial order, [[JFC citer un theoreme qui dit cela ou
+ % le prouver]] there exists a renaming process that assigns new identifier
+ % number to processes $i\in [p]$ and $j \in [q]$ s.t. $i \le j$ provided $[p]
+ % \preceq [q]$.
+ % % $i \in [p]$ and $j \in [q]$.
+
+ The rest of the proof is done by induction on the class index. Let us
+ consider the first class \class{b_1} with $n_1$ elements \textit{i.e.} the
+ class with the smallest identifiers.
+
+ By theorem hypotheses, %following the strategy $(S^t)$,
+ synchronous iterations converge to the fixed point in a finite number of
+ iterations. %pseudo periods. % [[JFC : borner m1/n1]].
+ So, all \emph{source classes} (independant from any other class) will also
+ converge in mixed mode. Let us suppose now that mixed iterations with uniform
+ delays converge for classes \class{b_1}, \ldots, \class{b_k} in a time $t_k$.
+ By construction, \class{b_{k+1}} only depends on some \class{b_1}, \ldots,
+ \class{b_k} and \class{b_{k+1}}. There exists then a sufficiently large time
+ $t_0$ s.t. $D^{t_0}_{p_{k+1}p_j}$ is greater or equal to $t_k$ for any
+ $p_{k+1} \in$ \class{b_{k+1}} and $p_j \in$ \class{b_j}, $1 \le j \le k$.
+
+ We are then left with synchronous iterations of elements of \class{b_{k+1}}
+ starting with configurations where all the elements of \class{b_j}, $1 \le j
+ \le k$, have constant values. By theorem hypotheses, it converges.
+\end{Proof}
+
+
+
