From 821ed92d748a8c1b093d90e9cb7f164753f8371c Mon Sep 17 00:00:00 2001
From: Mysaa <samy.avrillon@ens-lyon.fr>
Date: Sat, 30 Jul 2022 12:58:19 +0200
Subject: [PATCH] =?UTF-8?q?D=C3=A9but=20de=20preuve=20....=20faux=20s?=
 =?UTF-8?q?=C3=BBrement.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 RapportStage.tex | 50 ++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 48 insertions(+), 2 deletions(-)

diff --git a/RapportStage.tex b/RapportStage.tex
index ea8584b..251e18d 100644
--- a/RapportStage.tex
+++ b/RapportStage.tex
@@ -834,9 +834,55 @@
 				Pour $h$ expression avec des variables libres tel que $\operatorname{Var}(h) \subset \operatorname{Dom}(\varepsilon)$\\
 				Si $\varepsilon \prec \gamma$\\
 				Alors $h\bracket{\varepsilon} \prec h\bracket{\gamma}$\\
-				C'est à dire \[\forall \hbar \left(\exists e'\quad h\bracket{\varepsilon}\rightarrow^* h\bracket{e'}\right)\implies\left(\exists f'\quad h\bracket{\gamma}\rightarrow^* h\bracket{f'}\right)\]
+				C'est à dire \[\forall \hbar \left(\exists \overline{e'}\quad h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{\overline{e'}}\right)\implies\left(\exists f'\quad h\bracket{\gamma}\rightarrow^* \hbar\bracket{\overline{f'}}\right)\]
 			\end{theorem}
-		
+			
+			C'est sous cette seconde forme que nous allons prouver le théorème (elle est plus \enquote{bas niveau}).
+			
+			Procédons par induction sur $h$.
+			
+			\subparagraph{$h$ = $\fj{x}$ (variable)}
+				Alors
+				\[h\bracket{\varepsilon} = \varepsilon(x
+				\fj{x}) \prec \gamma(\fj{x}) = h\bracket{\gamma}\]
+				
+			\subparagraph{$h$ = $\fj{$h_0$.meth($\overline{h'}$)}$}
+				
+				Par hypothèse d'induction, on a
+				\[h_0\bracket{\varepsilon} \prec h_0\bracket{\gamma} \quad\text{et}\quad \overline{h'}\bracket{\varepsilon}\prec\overline{h'}\bracket{\gamma}\]
+				
+				Soit $\hbar$ tel que $h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{e'}$
+				
+				Le cas $\hbar = \hole$ se traite de la même manière dans tous les cas de l'induction, puisque alors, en considérant $\overline{f'} = \left(h\bracket{\gamma}\right)$, alors $h\bracket{\gamma} = \hbar\bracket{\overline{f'}}$, donc $h\bracket{\gamma}\rightarrow^* \hbar\bracket{f'}$
+				
+				Sinon, on a que $\hbar=\fj{new C($\overline{\hbar'}$)}$
+				
+				Donc, puisque la racine de l'expression $h\bracket{\varepsilon}$ passe d'un appel à méthode à un \fj{new}, c'est nécessairement qu'il y a eu une réduction \textsc{R-Invk} sur la racine, donc que 
+				\[h_0\bracket{\varepsilon} \rightarrow^* \fj{new D($\overline{h_1\bracket{\varepsilon}}$)}\]
+					
+				Et donc, par hypothèse d'induction,
+				\[h_0\bracket{\gamma} \rightarrow^* \fj{new D($\overline{h_1\bracket{\gamma}}$)}\]
+				
+				Alors, en notant $h_{\fj{meth}} = \operatorname{mbody}(\fj{D},\fj{meth})$ (c'est une expression avec des variables libres, que l'on note d'ailleurs $\overline{\fj{x}}$).
+				
+				\begin{align}
+					h\bracket{\epsilon} & \rightarrow^* & \fj{new D($\overline{h_1}\bracket{\varepsilon}$).meth(\overline{h'}\bracket{\varepsilon})} \\
+					& \rightarrow & h_{\fj{body}}\bracket{\varepsilon'}
+				\end{align}
+				et \[\varepsilon' = \left[\begin{array}{ccl}
+				\fj{this} & \mapsto & \fj{new D($\overline{h_1\bracket{\varepsilon}}$)}\\
+				\overline{\fj{x}} & \mapsto & \overline{h'}\bracket{\varepsilon}
+				\end{array}\right]\]
+			
+				De même, on a 
+				\begin{align}
+					h\bracket{\gamma} & \rightarrow^* & \fj{new D($\overline{h_1}\bracket{\gamma}$).meth(\overline{h'}\bracket{\gamma})} \\
+					& \rightarrow & h_{\fj{body}}\bracket{\vargamma'}
+				\end{align}
+				et \[\vargamma' = \left[\begin{array}{ccl}
+					\fj{this} & \mapsto & \fj{new D($\overline{h_1\bracket{\vargamma}}$)}\\
+					\overline{\fj{x}} & \mapsto & \overline{h'}\bracket{\vargamma}
+				\end{array}\right]\]