Prove the essentially trivial proposition about strategies (exists/forall).

1 files changed, 58 insertions, 1 deletions

diff --git a/notes-mitro206.tex b/notes-mitro206.tex
index 7d5f1b3..30f16f2 100644
--- a/notes-mitro206.tex
+++ b/notes-mitro206.tex
@@ -68,6 +68,9 @@ Git: \input{vcline.tex}
 \immediate\write18{echo ' (stale)' >> vcline.tex}
 \par}
 
+\pretolerance=8000
+\tolerance=50000
+
 
 
 %
@@ -1378,7 +1381,61 @@ Dans le jeu de Gale-Stewart $G_X(A)$ :
 \end{itemize}
 \end{prop}
 \begin{proof}
-\textcolor{red}{...}
+La démonstration suivante ne fait que (laborieusement) formaliser
+l'argument « une stratégie gagnante pour Alice détermine un premier
+coup, après quoi elle a une stratégie gagnante, et une stratégie
+gagnante pour Bob est prête à répondre à n'importe quel coup d'Alice
+après quoi il a une stratégie gagnante » :
+
+Si Alice (premier joueur) possède une stratégie $\varsigma$ gagnante
+dans $G_X(A)$, on pose $x := \varsigma(())$ le premier coup préconisé
+par cette stratégie, et on définit
+$\varsigma'((x_1,x_2,\ldots,x_{i-1})) =
+\varsigma((x,x_1,x_2,\ldots,x_{i-1}))$ pour $i$ pair : cette
+définition fait que si $(x_1,x_2,x_3,\ldots)$ est une confrontation où
+Alice joue en second selon $\varsigma'$ alors $(x,x_1,x_2,x_3,\ldots)$
+en est une où elle joue en premier selon $\varsigma$, donc cette suite
+appartient à $A$ puisque $\varsigma$ est gagnante pour Alice
+dans $G_X(A)$, donc $(x_1,x_2,x_3,\ldots)$ appartient à $x^{\$} A$, et
+Alice a bien une stratégie gagnante, $\varsigma'$, en jouant en second
+dans $G_X(x^{\$} A)$.
+
+Réciproquement, si Alice possède une stratégie gagnante $\varsigma'$
+en jouant en second dans $G_X(x^{\$} A)$, on définit $\varsigma$ par
+$\varsigma(()) = x$ et $\varsigma((x,x_1,x_2,\ldots,x_{i-1})) =
+\varsigma'((x_1,x_2,\ldots,x_{i-1}))$ pour $i > 0$ pair : cette
+définition fait que si $(x_0,x_1,x_2,x_3,\ldots)$ est une
+confrontation où Alice joue en premier selon $\varsigma$ alors $x_0 =
+x$ et $(x_1,x_2,x_3,\ldots)$ est confrontation où elle (Alice) joue en
+second selon $\varsigma'$, donc cette suite appartient à $x^{\$} A$
+puisque $\varsigma'$ est gagnante pour Alice second joueur
+dans $G_X(x^{\$} A)$, donc $(x_0,x_1,x_2,x_3,\ldots)$ appartient
+à $A$, et Alice a bien une stratégie gagnante, $\varsigma$, en jouant
+en premier dans $G_X(A)$.
+
+Si Bob (second joueur) possède une stratégie $\tau$ gagnante
+dans $G_X(A)$ et si $x \in X$ est quelconque, on définit
+$\tau'((x_1,x_2,\ldots,x_{i-1})) = \tau((x,x_1,x_2,\ldots,x_{i-1}))$
+pour $i$ impair : cette définition fait que si $(x_1,x_2,x_3,\ldots)$
+est une confrontation où Bob joue en premier selon $\tau'$ alors
+$(x,x_1,x_2,x_3,\ldots)$ en est une où il joue en second selon $\tau$,
+donc cette suite n'appartient pas à $A$ puisque $\tau$ est gagnante
+pour Bob dans $G_X(A)$, donc $(x_1,x_2,x_3,\ldots)$ n'appartient pas
+à $x^{\$} A$, et Bob a bien une stratégie gagnante, $\tau'$, en jouant
+en premier dans $G_X(x^{\$} A)$.
+
+Réciproquement, si Bob possède une stratégie gagnante en jouant en
+second dans $G_X(x^{\$} A)$ pour chaque $x\in X$, on en choisit une
+$\tau_x$ pour chaque $x$, et on définit $\tau$ par
+$\tau((x,x_1,x_2,\ldots,x_{i-1})) = \tau_x((x_1,x_2,\ldots,x_{i-1}))$
+pour $i$ impair : cette définition fait que si
+$(x_0,x_1,x_2,x_3,\ldots)$ est une confrontation où Bob joue en second
+selon $\tau$ alors $(x_1,x_2,x_3,\ldots)$ est confrontation où il
+(Bob) joue en premier selon $\tau_{x_0}$, donc cette suite
+n'appartient pas à ${x_0}^{\$} A$ puisque $\tau_{x_0}$ est gagnante
+pour Bob premier joueur dans $G_X({x_0}^{\$} A)$, donc
+$(x_0,x_1,x_2,x_3,\ldots)$ n'appartient pas à $A$, et Bob a bien une
+stratégie gagnante, $\tau$, en jouant en second dans $G_X(A)$.
 \end{proof}