preuve promela:debut de traduction

[hdrcouchot.git] / annexesccg.tex

Soit $\alpha\in\Bool$. 
On nomme $f^{\alpha}$ la fonction de $\Bool^{{\mathsf{N}}-1}$ 
dans lui-même définie pour 
chaque $x\in\Bool^{{\mathsf{N}}-1}$ par 
\[
f^{\alpha}(x)=(f_1(x,\alpha),\dots,f_{{\mathsf{N}}-1}(x,\alpha)).
\]
On nomme $\textsc{giu}(f)^\alpha$ le sous-graphe
de $\textsc{giu}(f)$ engendré par le sous-ensemble
$\Bool^{{\mathsf{N}}-1} \times \{\alpha\}$ de $\Bool^{\mathsf{N}}$.




Énonçons et prouvons tout d'abord les lemmes techniques suivants:

\begin{lemma}\label{lemma:subgraph}
$G(f^\alpha)$ est un sous-graphe de $G(f)$: chaque arc de $G(f^\alpha)$ est
un arc de $G(f)$. De plus si $G(f)$ n'a pas d'arc de ${\mathsf{N}}$ vers un autre 
sommet $i\neq {\mathsf{N}}$, alors on déduit
$G(f^\alpha)$ de $G(f)$ en supprimant le sommet ${\mathsf{N}}$ ainsi que tous les 
arcs dont ${\mathsf{N}}$ est soit l'extrémité, soit l'origine (et dans ce dernier  
cas, les arcs sont des boucles sur ${\mathsf{N}}$).
\end{lemma}

\begin{Proof}
Supposons que $G(f^{\alpha})$ possède un arc de  $j$ vers $i$ de signe 
$s$. Par définition, il existe un sommet $x\in\Bool^{{\mathsf{N}}-1}$ tel que
$f^{\alpha}_{ij}(x)=s$, et puisque 
$f^{\alpha}_{ij}(x)=f_{ij}(x,\alpha)$, on en déduit que $G(f)$ possède un arc
de $j$ à $i$ de signe $s$. Ceci prouve la première assertion. 
Pour démontrer la seconde, il suffit de  prouver que si
$G(f)$ a un arc de $j$ vers $i$ de signe $s$, avec $i,j\neq {\mathsf{N}}$, alors
$G(f^\alpha)$ contient aussi cet arc. Ainsi, supposons que $G(f)$ a un 
arc de $j$ vers $i$ de signe $s$, avec $i,j\neq {\mathsf{N}}$.
Alors, il existe
$x\in\Bool^{{\mathsf{N}}-1}$ et $\beta\in\Bool$ tels que
$f_{ij}(x,\beta)=s$. Si $f_{ij}(x,\beta)\neq f_{ij}(x,\alpha)$, alors
$f_i$ dépend du  ${\mathsf{N}}^{\textrm{ème}}$ composant, ce qui est en contradiction 
avec les hypothèses.
Ainsi $f_{ij}(x,\alpha)$ est égal à $s$.
On a donc aussi
$f^{\alpha}_{ij}(x)=s$. Ainsi $G(f^\alpha)$ possède un arc 
arc de $j$ vers $i$ de signe $s$.
\end{Proof}

\begin{lemma}\label{lemma:iso}
Les graphes $\textsc{giu}(f^\alpha)$ et $\textsc{giu}(f)^\alpha$ sont isomorphes.
\end{lemma}

\begin{Proof}
Soit $h$ la bijection de $\Bool^{{\mathsf{N}}-1}$ vers
$\Bool^{{\mathsf{N}}-1}\times \{\alpha\}$ définie par $h(x)=(x,\alpha)$ pour chaque
$x\in\Bool^{{\mathsf{N}}-1}$.
On voit facilement que $h$ permet de définir un isomorphisme
entre $\textsc{giu}(f^\alpha)$ et $\textsc{giu}(f)^\alpha$: 
$\textsc{giu}(f^\alpha)$ possède un arc de $x$ vers $y$ si et seulement si 
$\textsc{giu}(f)^\alpha$ a un  arc de $h(x)$ vers $h(y)$.
\end{Proof}


\begin{Proof}
du Théorème~\ref{th:Adrien}.
La preuve se fait par induction sur ${\mathsf{N}}$. 
Soit $f$ une fonction de $\Bool^{\mathsf{N}}$ dans lui-même et qui vérifie les hypothèses 
du théorème.
Si ${\mathsf{N}}=1$ la démonstration est élémentaire:
en raison du troisième point du théorème, $G(f)$ a une boucle négative;
ainsi $f(x)=\overline{x}$ et $\textsc{giu}(f)$ est un cycle de longueur 2.
On suppose donc que ${\mathsf{N}}>1$ et que le théorème est valide pour toutes les 
fonctions de $\Bool^{{\mathsf{N}}-1}$ dans lui-même. 
En raison du premier point du théorème, $G(f)$
contient au moins un sommet $i$ tel qu'il n'existe pas dans $G(f)$
d'arc de $i$ vers un autre sommet $j\neq i$.
Sans perte de généralité, on peut considérer que 
ce sommet est  ${\mathsf{N}}$.
Alors, d'après le lemme~\ref{lemma:subgraph}, 
$f^0$ et $f^1$ vérifient les conditions de l'hypothèse.
Alors, par hypothèse d'induction $\textsc{giu}(f^0)$ et
$\textsc{giu}(f^1)$ sont fortement connexes. 
Ainsi, d'après le lemme~\ref{lemma:iso}, 
$\textsc{giu}(f)^0$ et $\textsc{giu}(f)^1$ sont fortement 
connexes. 
Pour prouver que $\textsc{giu}(f)$ est fortement connexe, il suffit 
de prouver que $\textsc{giu}(f)$ contient un arc $x\to y$ avec 
$x_{\mathsf{N}}=0<y_{\mathsf{N}}$ et un arc $x\to y$ avec $x_{\mathsf{N}}=1>y_{\mathsf{N}}$. 
En d'autres mots, il suffit de prouver que:
\begin{equation}\tag{$*$}
\forall \alpha\in\Bool,~\exists x\in\Bool^{\mathsf{N}},\qquad  x_{\mathsf{N}}=\alpha\neq f_{\mathsf{N}}(x).
\end{equation}

On suppose tout d'abord que ${\mathsf{N}}$ a une boucle 
négative.
Alors, d'après la définition de 
$G(f)$, il existe $x\in\Bool^{\mathsf{N}}$ tel que $f_{{\mathsf{N}}{\mathsf{N}}}(x)<0$. 
Ainsi si $x_{\mathsf{N}}=0$, on a  $f_{\mathsf{N}}(x)>f_{\mathsf{N}}(\overline{x}^{\mathsf{N}})$, et donc 
$x_{\mathsf{N}}=0\neq f_{\mathsf{N}}(x)$ et
$\overline{x}^{\mathsf{N}}_{\mathsf{N}}=1\neq f_{\mathsf{N}}(\overline{x}^{\mathsf{N}})$; 
et si  $x_{\mathsf{N}}=1$, on a 
$f_{\mathsf{N}}(x)<f_{\mathsf{N}}(\overline{x}^{\mathsf{N}})$, donc $x_{\mathsf{N}}=1\neq f_{\mathsf{N}}(x)$ et $\overline{x}^{\mathsf{N}}_{\mathsf{N}}=0\neq
f_{\mathsf{N}}(\overline{x}^{\mathsf{N}})$. 
Dans les deux cas, la condition ($*$) est établie.

Supposons maintenant que  ${\mathsf{N}}$ n'a pas de boucle négative.
D'après la seconde hypothèse, 
${\mathsf{N}}$ n'a pas de boucle, \emph{i.e.}, la valeur de $f_{\mathsf{N}}(x)$
ne dépend pas de la valeur de $x_{\mathsf{N}}$. 
D'après la troisième hypothèse, 
il existe $i\in \llbracket 1;{\mathsf{N}} \rrbracket$ tel que $G(f)$ a un arc de 
$i$ vers ${\mathsf{N}}$.
Ainsi, il existe $x \in \Bool^{\mathsf{N}}$ tel que $f_{{\mathsf{N}}i}(x) \neq 0$ et donc 
%$n$ n'est donc pas de degré zéro dans $G(f)$, \emph{i.e.} 
$f_{\mathsf{N}}$ n'est pas constante.
Ainsi, il existe $x,y\in \Bool^{\mathsf{N}}$ tel que
$f_{\mathsf{N}}(x)=1$ et $f_{\mathsf{N}}(y)=0$. 
Soit  $x'=(x_1,\dots,x_{{\mathsf{N}}-1},0)$ et
$y'=(y_1,\dots,y_{{\mathsf{N}}-1},1)$. 
Puisque la valeur de $f_{\mathsf{N}}(x)$
(resp. de $f_{\mathsf{N}}(y)$) ne dépend pas de la  valeur de  $x_{\mathsf{N}}$ (resp. de  $y_{\mathsf{N}}$),
on a $f_{\mathsf{N}}(x')=f_{\mathsf{N}}(x)=1\neq x'_{\mathsf{N}}$ (resp. $f_{\mathsf{N}}(y')=f_{\mathsf{N}}(y)=0\neq
y'_{\mathsf{N}}$). 
Ainsi la  condition ($*$) est établie, et le théorème est prouvé.
\end{Proof}