annexes~\ref{anx:promela}.
-\begin{theorem}[Correction]\label{Theo:sound}
+\begin{restatable}[Correction de la traduction vers Promela]{theorem}{promelasound}
+\label{Theo:sound}
+%
Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction PROMELA.
Si $\psi$ vérifie
la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible, alors
les itérations de $\phi$ sont universellement convergentes.
-\end{theorem}
-
+\end{restatable}
-\begin{theorem}[Complétude]\label{Theo:completeness}
+\begin{restatable}[Complétude de la traduction vers Promela]{theorem}{promelacomplete}
+\label{Theo:completeness}
+%
Soit $\phi$ un modèle de système dynamique discret et $\psi$ sa traduction. Si $\psi$ ne vérifie pas
la propriété LTL (\ref{eq:ltl:conv}) sous hypothèse d'équité faible,
alors les itérations de $\phi$ ne sont pas universellement convergentes.
-\end{theorem}
+\end{restatable}
+
+
