main.loe

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