cas, les arcs sont des boucles sur ${\mathsf{N}}$).
\end{lemma}
-\begin{Proof}
+\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
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}
+\end{proof}
\begin{lemma}\label{lemma:iso}
Les graphes $\textsc{giu}(f^\alpha)$ et $\textsc{giu}(f)^\alpha$ sont isomorphes.
\end{lemma}
-\begin{Proof}
+\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}$.
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}
+\end{proof}
-\begin{Proof}
-du Théorème~\ref{th:Adrien}.
+On peut alors prouver le théorème:
+\thAdrien*
+
+\begin{proof}
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.
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$.
+$G(f)$, il existe $x\in\Bool^{\mathsf{N}}$ tel que $f_{{\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}})$;
${\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
+il existe $i\in [{\mathsf{N}}]$ 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.}
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}
+\end{proof}