
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}



