\addvspace {10\p@ }
\contentsline {xpl}{\numberline {\let \autodot \@empty }Exemple}{11}{thmt@dummyctr.dummy.1}
\contentsline {xpl}{\numberline {\let \autodot \@empty }Exemple}{12}{thmt@dummyctr.dummy.2}
\contentsline {theorem}{\numberline {1}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Correction}}{16}{theorem.1}
\contentsline {theorem}{\numberline {2}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Compl\IeC {\'e}tude}}{16}{theorem.2}
\contentsline {theorem}{\numberline {3}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Nombre d'\IeC {\'e}tats }}{17}{theorem.3}
\contentsline {Proof}{\numberline {1}Preuve}{17}{Proof.1}
\addvspace {10\p@ }
\contentsline {lemma}{\numberline {1}Lemme}{21}{lemma.1}
\contentsline {Proof}{\numberline {2}Preuve}{21}{Proof.2}
\contentsline {lemma}{\numberline {2}Lemme}{21}{lemma.2}
\contentsline {Proof}{\numberline {3}Preuve}{21}{Proof.3}
\contentsline {Proof}{\numberline {4}Preuve}{21}{Proof.4}
\contentsline {lemma}{\numberline {3}Lemme\thmtformatoptarg {Strategy Equivalence}}{23}{lemma.3}
\contentsline {Proof}{\numberline {5}Preuve}{23}{Proof.5}
\contentsline {lemma}{\numberline {4}Lemme\thmtformatoptarg {Existence of SPIN Execution}}{24}{lemma.4}
\contentsline {Proof}{\numberline {6}Preuve}{24}{Proof.6}
\contentsline {lemma}{\numberline {5}Lemme}{25}{lemma.5}
\contentsline {Proof}{\numberline {7}Preuve}{25}{Proof.7}
\contentsline {theorem}{\numberline {4}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Soundness wrt universal convergence property}}{25}{theorem.4}
\contentsline {Proof}{\numberline {8}Preuve}{25}{Proof.8}
\contentsline {theorem}{\numberline {5}Th\IeC {\'e}or\IeC {\`e}me\thmtformatoptarg {Completeness wrt universal convergence property}}{26}{theorem.5}
\contentsline {Proof}{\numberline {9}Preuve}{26}{Proof.9}