X-Git-Url: https://bilbo.iut-bm.univ-fcomte.fr/and/gitweb/hdrcouchot.git/blobdiff_plain/4027522083d5f0dfb61df0df9bb8dda73a9cb72b..089adfe473f0b28ff70bdd8f9c0bb3e036345db9:/annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index d56d89b..70981a9 100644
--- a/annexePromelaProof.tex
+++ b/annexePromelaProof.tex
@@ -140,7 +140,7 @@ les deux cas sont égaux à
 Pour le dernier item, soit $k$, $0  \le  k \le  n-1$. 
 A la fin de la première exécution du processus \verb+update_elems+,
 la valur   de
-\ver+Xp[k]+       est       $F(\verb+Xd[+k\verb+].v[0]+,       \ldots,
+\verb+Xp[k]+       est       $F(\verb+Xd[+k\verb+].v[0]+,       \ldots,
 \verb+Xd[+k\verb+].v[+n-1\verb+]+)$.  
 Ainsi par définition de  $Xd$, ceci est égal à 
 $F(Xd^1_{k\,0}, \ldots,Xd^1_{k\,n-1})$.  Grâce à l'équation \Equ{eq:correct_retrieve},
@@ -148,15 +148,16 @@ on peut conclure la preuve.
 
 
 
-\paragraph{Inductive case:}
+\paragraph{Induction:}
+Supposons maintenant que le lemme~\ref{lemma:execution} est établi jusqu'à 
+l'itération $l$.
 
-Suppose now that lemma~\ref{lemma:execution} is established until iteration $l$.
+Tout d'abord, si le domaine  de définition  de la   fonction $M_{ij}^l$  
+n'est pas vide, par hypothèse d'induction $M_{ij}^{l}(0)$  est
+$\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
+\right)$ où $c$ est $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
 
-First,  if domain  of definition  of the  function $M_{ij}^l$  is not  empty, by
-induction  hypothesis $M_{ij}^{l}(0)$  is  $\left(X_i^{D_{ji}^{c}}, D_{ji}^{c},c
-\right)$ where $c$ is $\min\{k | D_{ji}^k > D_{ji}^{l-2} \}$.
-
-At iteration $l$, if  $l < c + 1$ then the  \verb+skip+ statement is executed in
+A l'itération $l$, si  $l < c + 1$ alors  \verb+skip+ statement is executed in
 the   \verb+fetch_values+  function.   Thus,   $M_{ij}^{l+1}(0)$  is   equal  to
 $M_{ij}^{l}(0)$.  Since $c > l-1$  then $D_{ji}^c > D_{ji}^{l-1}$ and hence, $c$
 is $\min\{k  | D_{ji}^k  > D_{ji}^{l-1} \}$.  Obviously, this implies  also that