après remarques tof

[hdrcouchot.git] / annexePreuveMarquageCorrectioncompletude.tex

\marquagecorrectioncompl*

\begin{proof}
Pour la suffisance, soit $d_i$ la dernière itération où l'élément $i \in \Im(S_p)$
de la configuration $x$ a été modifié:% is defined by 
$$
d_i = \max\{j | S^j_p = i \}.
$$ 
Soit $D=\{d_i|i \in \Im(S_p) \}$.
L'ensemble $\Im(S_c)_{|D}$ est donc la restriction de l'image de $S_c$ à $D$.


Le vecteur qui résulte de ces itérations est donc
$(x^l_0,\ldots,x^l_{\mathsf{N}-1})$ où
$x^l_i$ est soit  $x^{d_i}_i$ si $i$ appartient à $\Im(S_p)$ ou $x^0_i$ sinon.
De plus, pour chaque $i \in \Im(S_p)$, l'élément $x^{d_i}_i$ est égal à 
$m^{d_i-1}_{S^{d_i}_c}$. 
Sous hypothèse que la contrainte imposée soit réalisée,  tous les indices
$j \in \llbracket 0 ;\mathsf{P} -1 \rrbracket$ appartiennent à
$\Im(S_c)_{|D}$.
On a alors $j \in \llbracket 0 ;\mathsf{P} -1 \rrbracket$ tel que 
$S^{d_i}_c=j$. 
On retrouve ainsi tous les éléments $m^._j$ du vecteur $m$.
A partir de $m^{d_i-1}_j$, 
la valeur de  $m^0_j$ peut être déduite en comptant dans  $S_c$ combien de fois 
l'élément $j$ a été invoqué avant $d_i-1$.  

Réciproquement, si $\Im(S_c)_{|D} \subsetneq 
\llbracket 0 ;\mathsf{P} -1 \rrbracket$,
il existe un $j \in \llbracket 0 ;\mathsf{P} -1 \rrbracket$ qui n'appartient pas à $\Im(S_c)_{|\Im(S_p)}$. 
Ainsi, $m_j$ n'est pas présent dans $x^l$ et le message ne peut pas extrait.
\end{proof}