et $\psi$ sa traduction en PROMELA. Le nombre de configurations
de l'exécution en SPIN de $\psi$ est bornée par $2^{m(\delta_0+1)+n(n+2)}$.
\end{theorem}
-\begin{Proof}
+\begin{proof}
Une configuration est une évaluation des variables globales.
Leur nombre ne dépend que de celles qui ne sont pas constantes.
$m$ et $\delta_0$.
%\JFC{Donner un ordre de grandeur de cet ordre de grandeur}
-\end{Proof}
+\end{proof}
La méthode détaillée ici a pu être appliquée sur l'exemple
pour prouver formellement sa convergence universelle.
