\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
% \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
