X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/98c34e4d34d6f63836eefca981f5d1ce73a865e2..2b04820abccb0772b10b2c53542ecddc6a6f600c:/annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index dbc5774..1f70e9f 100644
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -228,11 +228,7 @@ to      $F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      Thanks      to
 \end{Proof}
 
 
-\begin{theorem}[Soundness wrt universal convergence property]\label{Theo:sound}
-  Let $\phi$ be  a DDN model and $\psi$ be its  translation.  If $\psi$ verifies
-  the  LTL  property  (\ref{eq:ltl:conv})  under weak  fairness  property,  then
-  iterations of $\phi$ are universally convergent.
-\end{theorem}
+\promelasound*
 \begin{Proof}
 %   For  the  case  where  the  strategy  is  finite,  one  notice  that  property
 %   verification  is achieved  under  weak fairness  property.  Instructions  that
@@ -259,12 +255,8 @@ to      $F(Xd^{l+1}_{k\,0},      \ldots,Xd^{l+1}_{k\,n-1})$.      Thanks      to
 % \end{Corol}
 
 
+\promelacomplete*
 
-\begin{theorem}[Completeness wrt universal convergence property]\label{Theo:completeness}
-  Let $\phi$ be a  DDN model and $\psi$ be its translation.   If $\psi$ does not
-  verify the LTL property  (\ref{eq:ltl:conv}) under weak fairness property then
-  the iterations of $\phi$ are divergent.
-\end{theorem}
 \begin{Proof}
   For models $\psi$  that do not verify the  LTL property (\ref{eq:ltl:conv}) it
   is easy  to construct corresponding iterations  of the DDN,  whose strategy is