\begin{proof}
La preuve est directe pour $t=0$.
Supposons qu'elle est établie jusqu'en $t$ valant un certain $t_0$.
- On considère des stratégies pseudo périodiques.
+ On considère des stratégies pseudo-périodiques.
Grâce à l'hypothèse d'équité faible, \verb+update_elems+ modifie
les éléments de $S^t$ à l'itération $t$.
\end{proof}
Pour chaque modèle $\psi$
qui ne vérifie pas la propriété LTL (\ref{eq:ltl:conv}),
il est immédiat de construire les itérations correspondantes du
- système dynamique, dont la stratégie est pseudo périodique en raison
+ système dynamique, dont la stratégie est pseudo-périodique en raison
de la propriété d'équité faible..
% i.e. iterations that are divergent. Executions are
