quelques perspectives

[hdrcouchot.git] / annexePromelaProof.tex

diff --git a/annexePromelaProof.tex b/annexePromelaProof.tex
index d56d89b6a6e3b8d2a7fb3dda177927a15b342d73..70981a92fef0588cd3fcb0b7b340712144568724 100644 (file)
--- 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
 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},
 \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
 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