preuve promela traduite

[hdrcouchot.git] / annexePreuveMixage.tex

diff --git a/annexePreuveMixage.tex b/annexePreuveMixage.tex
index d4087d42d45e028686c795b2cf5b056815b0d194..12c3223832ddf809b28d9ffa5b949988b48e3982 100644 (file)
--- a/annexePreuveMixage.tex
+++ b/annexePreuveMixage.tex
@@ -3,11 +3,9 @@ $\preceq$  entre les  classes d'équivalences.
 Formellement, \class{p}
 $\preceq$   \class{q}   
 s'il existe un chemin de longueur   $\alpha$
 Formellement, \class{p}
 $\preceq$   \class{q}   
 s'il existe un chemin de longueur   $\alpha$

-($0<\alpha<|\mathcal{K}|$)  entre un élément le la classe
+($0\le\alpha<|\mathcal{K}|$)  entre un élément le la classe

 \class{p} vers un élément  de
 \class{p} vers un élément  de

-\class{q}.  
-On remarque que si la  \class{p}$\preceq$\class{q}, 
-il n'est alors pas possible que  \class{q}$\preceq$\class{p}.
+\class{q}. 

 
 \begin{lemma}
   Il existe un processus de renommage qui effecte un nouvel identifiant aux
 
 \begin{lemma}
   Il existe un processus de renommage qui effecte un nouvel identifiant aux


@@ -17,7 +15,7 @@ il n'est alors pas possible que  \class{q}$\preceq$\class{p}.
   \begin{Proof}
     
     Tout d'abord,  soit  \class{p_1},   \ldots,  \class{p_l}  des   classes 
   \begin{Proof}
     
     Tout d'abord,  soit  \class{p_1},   \ldots,  \class{p_l}  des   classes 

-    contenant respectivement $n_1$,\ldots,  $n_l$  éléments respectively
+    contenant respectivement les éléments $n_1$,\ldots,  $n_l$

     qui ne dépendent d'aucune autre classe.  
     Les éléments de  \class{p_1} sont renommés par $1$, \ldots,  $n_1$,
     les elements  de \class{p_i},   $2  \le   i  \le   l$  sont renommés par 
     qui ne dépendent d'aucune autre classe.  
     Les éléments de  \class{p_1} sont renommés par $1$, \ldots,  $n_1$,
     les elements  de \class{p_i},   $2  \le   i  \le   l$  sont renommés par 


@@ -72,7 +70,7 @@ On peut remarquer que ce processus de renommage est inspiré des \emph{graphes
 %   Processes numbers are already compliant with the order $\preceq$.
 % \end{xpl}
 
 %   Processes numbers are already compliant with the order $\preceq$.
 % \end{xpl}
 

-\begin{Proof}[of Theorem~\ref{th:cvg}]
+\begin{Proof}[du théorème~\ref{th:cvg}]

 
   Le reste de la preuve est fait par induction sur le numéro de classe. 
   Considérons la première  classe \class{b_1} de $n_1$ éléments 
 
   Le reste de la preuve est fait par induction sur le numéro de classe. 
   Considérons la première  classe \class{b_1} de $n_1$ éléments 


@@ -95,10 +93,10 @@ On peut remarquer que ce processus de renommage est inspiré des \emph{graphes
   pour chaque 
   $p_{k+1} \in$ \class{b_{k+1}} et $p_j \in$ \class{b_j}, $1 \le j \le k$.
 
   pour chaque 
   $p_{k+1} \in$ \class{b_{k+1}} et $p_j \in$ \class{b_j}, $1 \le j \le k$.
 

-  Il nous reste donc des itérations synchronous entre les 
+  Il ne reste donc que des itérations synchrones entre les 

   elements  of \class{b_{k+1}} en démarant dans des configurations
   où tous les éléments de  \class{b_j}, $1 \le j
   elements  of \class{b_{k+1}} en démarant dans des configurations
   où tous les éléments de  \class{b_j}, $1 \le j

-  \le k$, on des valeurs constantes.  
+  \le k$, ont  des valeurs constantes.  

   D'après les hypothèses du théorème, cela converge.
 \end{Proof}
 
   D'après les hypothèses du théorème, cela converge.
 \end{Proof}