X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/9e9f22c16917d3bf287f5e1f0df739200c392594..d4e1bfa4290a182013268daf63d78c1f4fce5b55:/modelchecking.tex

diff --git a/modelchecking.tex b/modelchecking.tex
index b01a526..d9e626e 100644
--- a/modelchecking.tex
+++ b/modelchecking.tex
@@ -657,7 +657,7 @@ puis présente ensuite les expérimentations issues de ce travail.
   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.
 
@@ -673,7 +673,7 @@ puis présente ensuite les expérimentations issues de ce travail.
   $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.