%% Time-stamp: <modified on  4 Apr 2006 at 20:15 by Pierre Lescanne>
%% /MIM-1/REECRITURE/UNIFICATION/unif.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\def\printlandscape{\special{landscape}}     % pour sortir en landscape
\slidesmag{5}

\usepackage{amsfonts,amsmath,amsthm,amssymb,stmaryrd}
\usepackage{fancybox}
%\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{amsmath}
\usepackage[all]{xy}
\input{mes_couleurs}

%% Time-stamping  
%% compute the time in hours and minutes; 
 \newcount\timehh\newcount\timemm \timehh=\time 
 \divide\timehh by 60 \timemm=\time
 \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255
 \newcommand{\timestamp}
 { {\protect\small\sl\today\ -- 
 \ifnum\timehh<10 0\fi\number\timehh\,h\,
   \ifnum\timemm<10 0\fi\number\timemm}}
                                          % avec dvips


\articlemag{1}

\rotateheaderstrue       % si tu combines slide et slide*

\title{\color{red}{\textit{Réécriture}}}

\author{Ordre sur les preuves}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

%--- couleurs ----
\renewcommand{\emph}[1]{\rouge{#1}}

%--- symboles ---
\renewcommand{\phi}{\varphi}
%\newcommand{\llbracket}{\ensuremath{|\![}}
%\newcommand{\rrbracket}{\ensuremath{]\!|}}
\newcommand{\PP}{\bl{\ensuremath{\cal P}}}
\newcommand{\gec}{\ensuremath{\succ_C}}
\newcommand{\Emb}{\bl{\ensuremath{\cal EMB}}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\shat}{\ensuremath{\hat{\sigma}}}
\newcommand{\pref}{\mathop{\textbf{\textsl{prefix}}}}
\newcommand{\IN}{\ensuremath{\mathcal{IN}}}
\newcommand{\gtmult}{\ensuremath{>_{mult}}}
\newcommand{\dminus}{\mbox{\ensuremath{\stackrel{\raisebox{+.01ex}{.}}{-}}}}
%\newcommand{\Nat}{\textsf{I}\hspace{-.7pt}\textsf{N}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Natstar}{\Nat_\star}
\newcommand{\A}{\ensuremath{\bl{\cal A}}}
\newcommand{\M}{{\cal M}}
\newcommand{\U}{{\cal U}}
\newcommand{\Ra}{\ensuremath{\mathop{\Rightarrow}}}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\set}[2]{\{#1~|~#2\}}
\newcommand{\da}{\downarrow}
\newcommand{\jgbl}{\mathop{\da}}
\newcommand{\lpo}{<_{lpo}}
\newcommand{\lepo}{\le_{lpo}}
\newcommand{\eq}{\stackrel{?}{=}}
\newcommand{\aco}{\{\!\!\{}
\newcommand{\acf}{\}\!\!\}}

%%%%%%%%% ajout special pour la completion %%%%%%%%%%%%
\newcommand{\la}{\leftarrow}
%\newcommand{\rastar}{\stackrel{\ast}{\rightarrow}}
\newcommand{\hligne}{\rule{\textwidth}{2pt}}
%\newcommand{\subsum}{\mbox{\small \tt |}\!\!{\stackrel{\scriptscriptstyle _\bullet}{}\!\!\!>}}
\newcommand{\subsum}{\mathop{\raisebox{1pt}{$\scriptscriptstyle \bullet$}\hspace{-7pt}\vartriangleright}}
%\newcommand{\ench}{\mbox{\small \tt |}\hspace{-2.9pt}{\stackrel{\scriptscriptstyle _\bullet}{}\hspace{-5pt}>}}
%\newcommand{\encheq}{\mbox{\raisebox{+0.2ex}{\small \tt |}
%    \hspace{-5pt}\raisebox{+.5ex}{$\scriptscriptstyle \bullet$}\hspace{-5pt}$\ge$}}
\newcommand{\ench}{\mathop{\raisebox{1pt}{$\scriptscriptstyle \bullet$}\hspace{-7pt}\vartriangleright}}
\newcommand{\encheq}{\mathop{\raisebox{2pt}{$\scriptscriptstyle \bullet$}\hspace{-7pt}\trianglerighteq}}
\newcommand{\eqone}{\mbox{\mysymb \symbol{1}}}
\newcommand{\tri}{\mbox{\mysymb \symbol{2}}}
%%%%%%%% fin ajout %%%%%%%%%

\newcommand{\inferTwoLabel}[4]{\bl{
 {#1} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}}}

\newcommand{\leafLabel}[2]{\bl{
 {#1} \quad
  \begin{array}{c}
  #2
  \end{array} }}


%\newcommand{\inferLabel}[3]{\emph{#1}\ali #2 \Mapsto #3}

\newcommand{\inferLabel}[3]{
    \rouge{#1} \quad 
    \bl{\begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \end{array}
  }}
\newenvironment{bdp}[1]{\begin{displaymath}\color{blue}#1}{\end{displaymath}}
    
%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

%\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\ra}{\rightarrow}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}

%%%%%%%%%%%%%%%%%%%% iteration of arrows  %%%%%%%%%%%%%%%%%%%%
\newcommand{\rastar}{\rasup{*}}
\newcommand{\raplus}{\rasup{+}}

%%%%%%%%%%%%%%%%%%%% fleches avec souscrit et superscrit %%%%%%%%%%%%%
% par exemple -- B, p --> s'ecrit \rasub{B,p}

\newcommand{\rasub}[1]{\xymatrix{\ar@{>}[r]_{#1} &}}
\newcommand{\subar}[1]{\xymatrix{\ar@{<-}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix{\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix{\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix{\ar@{>}[r]^{#1} &}}
\newcommand{\supar}[1]{\xymatrix{\ar@{<-}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix{\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix{\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\rarasupsub}[2]{\xymatrix{\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\cv}[1]{\xymatrix{\ar@{<->}[r]_{#1} &}}
\newcommand{\conv}[1]{\xymatrix{\ar@{<->}[r]_{#1}^{*} &}}
\newcommand{\convplus}[1]{\xymatrix{\ar@{<->}[r]_{#1}^{+} &}}

%%%%%%%%%%%%%%%%%%%% Les fleches %%%%%%%%%%%%%

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raE}{\rasub{E}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\Rar}{\subar{R}}
\newcommand{\rastarR}{\rasupsub{*}{R}}
\newcommand{\raraR}{\rarasub{R}}
\newcommand{\plusararR}{\xymatrix{&\ar@{>>}[l]^{R}_+}}
\newcommand{\plusraraR}{\rarasupsub{+}{R}}
\newcommand{\rapar}{\xymatrix @ -1.5pc {\ar@{>}[rr]&||&}}
\newcommand{\rarapar}{\xymatrix @ -1.5pc {\ar@{>>}[rr]&||&}}
\newcommand{\remb}{\rasub{\Emb}}
\newcommand{\plgt}{\rasupsub{+}{\Emb}}
\newcommand{\plonge}{\xymatrix{\ar@{<-}[r]_{\Emb}^{*} &}}

%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\heading}[1]{%
{\color{vertfonce}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{vertfonce}{\bf\Ovalbox{#1}}
  \end{center}}

\begin{document}
%------------------------------------------------------
\begin{slide}
    \maketitle
    \addtocounter{slide}{-1}
    \slidepagestyle{empty}

\vfill 
\hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Rappel}

\vspace*{20pt}

\begin{center}
  
  \bleu{
\begin{array}[c]{ll}
E_{\infty} = \bigcup_{i\ge 0}E_i
&
R_{\infty} = \bigcup_{i\ge 0}R_i
\\\\
E_{\omega} = \bigcup_{i\ge 0}\bigcap_{j\ge i}E_j
&
 R_{\omega} = \bigcup_{i\ge 0}\bigcap_{j\ge i}R_j
\end{array}
}
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Petite histoire d'une preuve}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les preuves de $a = b$ }

Considérons les preuves équationnelles possibles de l'égalité de deux
termes \bleu{a = b}.

\vfill

Au niveau \bleu{(E_0, R_0)} (avec \bleu{R_0 = \emptyset)} c'est une
preuve complètement par identités.  

\vspace*{20pt}

\bl{
\xymatrix @C 20pt {
a \ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&b
}
}

\end{slide}
%------------------------------------------------------
\begin{slide}
%\heading{Les preuves de $a = b$ (suite)}

alors qu'au niveau \bleu{(E_i, R_i)} pour un \bleu{i} quelconque,
c'est une preuve hétérogène.

\vspace*{20pt}

\bl{
\xymatrix @C 18pt {
&\ar[ld]\ar[rd]&&&&&&&&&\ar[ld]\ar[rd]&\\
a &&\ar@{=}[r]&\ar[dr]&&\ar[dl]\ar@{=}[r] &\ar[dr]&&&\ar[dl]&&b\\
&&&&&&&\ar@{=}[r]&&&&&
}
}


\vspace*{20pt}

Car certaines identités ne sont plus présentes et il faut les remplacer
par des réécritures.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les preuves de $a = b$ (suite)}
En fait ce qu'on souhaite c'est une preuve complétement
par réécriture (une preuve en vallée).

\vspace*{20pt}

\bl{
\xymatrix @C 16pt @R 5pt {
a \ar[dr]&&&&&&&&&&&& \ar[dl]b\\
&\ar[dr]&&&&&&&&&&\ar[dl]&\\
&&\ar[dr]&&&&&&&&\ar[dl]&&\\
&&&\ar[dr]&&&&&&\ar[dl]&&&\\
&&&&\ar[dr]&&&&\ar[dl]&&&&\\
&&&&&\ar[dr]&&\ar[dl]&&&&&\\
&&&&&&&&&&&&&&&&&&&&&
}
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

\emph{Début}

\bl{
\xymatrix @C 18pt {
a \ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&\ar@{=}[r]&b
}
}


\emph{Milieu}

\bl{
\xymatrix @C 18pt @R 3pt {
&\ar[ld]\ar[rd]&&&&&&&&&\ar[ld]\ar[rd]&\\
a &&\ar@{=}[r]&\ar[dr]&&\ar[dl]\ar@{=}[r] &\ar[dr]&&&\ar[dl]&&b\\
&&&&&&&\ar@{=}[r]&&&&&
}
}

% choisir parmi RCMLHW*!
 

\emph{Fin}

\bl{
\xymatrix @C 16pt @R 3pt {
a \ar[dr]&&&&&&&&&&&& \ar[dl]b\\
&\ar[dr]&&&&&&&&&&\ar[dl]&\\
&&\ar[dr]&&&&&&&&\ar[dl]&&\\
&&&\ar[dr]&&&&&&\ar[dl]&&&\\
&&&&\ar[dr]&&&&\ar[dl]&&&&\\
&&&&&\ar[dr]&&\ar[dl]&&&&&\\
&&&&&&&&&&&&&&&&&&&&&
}
}

\end{slide}
%------------------------------------------------------
\begin{slide}
  Il faut montrer que pour tout couple tel que \bleu{a =_{E_0} b}, il
  y a une \emph{preuve de réécriture} dans \bleu{R_\omega}, c'est-à-dire  qu'il
existe un \bleu{c} tels que

\bl{
\[ a \rasupsub{*}{R_\omega} c \xymatrix{\ar@{<-}[r]_{R_\omega}^{*} &} b\]
}

Il faut donc voir comment les preuves se transforment.

Pour cela, on transforme chaque étape de preuve \emph{en une étape de
preuve plus simple} et on montre en se servant d'un ordre noethérien
adéquat que le processus de transformation termine.

\end{slide}

%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Un ordre sur les preuves}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le coût d'une preuve} Une preuve où les termes
  intermédiaires sont \bleu{a_1, .... a_k, a_{k+1}, ... a_n} est associée
  au multiensemble \bleu{\aco a_1 ~£_1~ a_2 , ..., a_k ~£_k~ a_{k+1},
    ... \acf}.

Chaque \bleu{£_k} représente soit 

\begin{center}
  \bleu{=} \qquad \bleu{\ra} \qquad \bleu{\leftarrow}.
\end{center}

On va attribuer à chaque preuve un \emph{coût}.  

Auparavant on attribue un \emph{coût} à \emph{chaque étape élémentaire}.


Le \emph{coût d'une preuve} est le \emph{multiensemble des coûts} de chacune de ses
étapes élémentaires.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Le coût d'une étape élémentaire}
 
 Le \emph{coût} d'une étape élémentaire \bleu{a ~£~ b} est un
 triplet \bleu{(M, l, r)}.

\vfill 
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Le coût d'une paire (suite)}

On attribue les coûts de la façon suivante :

\begin{footnotesize}
\begin{itemize}
\item si \bleu{a_k ~£_k~ a_{k+1}} est de la forme \bleu{a_k =
    a_{k+1}}, le coût est \bleu{(\aco a_k, a_{k+1}\acf, \_,
    \_)}\footnote{\bleu{\_} signifie qu'on n'attache pas d'importance
    à ce champ.},
\item si \bleu{a_k ~£_k~ a_{k+1}} est de la forme \bleu{a_k \ra
    a_{k+1}}, le coût est \bleu{(\aco a_k\acf, l,r)}, où \bleu{l} est
  le membre gauche de la règle de réécriture employée et \bleu{r} est
  le membre droit de la règle de réécriture employée.
\item si \bleu{a_k ~£_k~ a_{k+1}} est de la forme \bleu{a_k \leftarrow
    a_{k+1}}, le coût est \bleu{(\aco a_{k+1}\acf, l,r)}, où \bleu{l}
  est le membre gauche de la règle de la réécriture employée et
  \bleu{r} est le membre droit de la règle de réécriture employée.
\end{itemize}
\end{footnotesize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La comparaison des coûts de paires} 
  
  Pour la \verdir{première composante} (\bleu{M}), c'est l'\emph{extension multiensemble
  de l'ordre sur les termes.}

Pour la \verdir{deuxième composante} (\bleu{l}), c'est l'ordre d'\emph{enchâssement}.

Pour la \verdir{troisième composante} (\bleu{r}), c'est l'\emph{ordre sur les termes}.

Ainsi 
\begin{itemize}
\item l'ordre sur les coûts termine.
\item l'ordre sur les preuves termine.
\end{itemize}
\vfill
\end{slide}
%-----------------------------------------------------------------------
\begin{slide}{}
\heading{L'enchâssement}
La relation d'enchâssement \emph{$\encheq$} (en anglais encompassment)
est définie par 
\bl{
\[s \encheq t \]
}
\centerline{si et seulement si}
\bl{
\[\quad \exists p \in Pos(s) \cdot \exists
\sigma\in Sub(T(\Sigma, V)) \cdot \quad s_{|p} = \sigma(t) \]
}
\vfill
\bleu{\encheq \cap \mbox{
    \raisebox{+.5ex}{$\scriptscriptstyle
      \bullet$}\hspace{-7pt}$\le$\hspace{-3pt}\raisebox{+.2ex}{\small
      \tt |}}} est \bleu{=}.

\bleu{\ench}  est la relation \bleu{\encheq \cap \not\sim} (où $\sim$
est le renommage des variables), elle termine.

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'ordre sur les preuves} 
L'ordre sur les preuves  s'écrit :

\bl{\[\PP \gec \PP'\]}

Deux preuves sont équivalentes si elles prouvent la même identité.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Décroissance des preuves}

Chaque transition fait décroître les preuves.

Si la transition est \emph{Delete}.  Si cette transition affecte une étape
\bleu{a_k ~£_k~ a_{k+1}} de la preuve alors cette étape disparaît et
le coût de la preuve diminue.

\begin{center}
  \bl{\xymatrix @C 3pt @R 8pt {
      \ar@{.}[r] & a_k  \ar@{=}[rr] && a_{k+1}\ar@{.}[r] & \\
      &&\rouge{\ar@{=>}[d]}\\
      &&&&\\
      \ar@{.}[r]&&a_k \ar@{.}[r] & }}
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Décroissance des preuves}
Si la transition est \emph{Compose}.

\begin{center}
  \bl{\xymatrix @C 3pt @R 5pt {
      a_k  \ar[rr]_{R_\infty} && a_{k+1}\\
      &\ar@{=>}[d]\\
      &&\\
      a_k \ar[ddr]_{R_\infty} && \ar[ddl]^{R_\infty} a_{k+1}\\
      &&\\
      &c&
}}
\end{center}

\begin{scriptsize}
  \bleu{cout(a_k \ra a_{k+1}) = (\aco a_k\acf, s, t) > cout(a_k \ra c) =
    (\aco a_k\acf, s, u)} parce que \bleu{\aco a_k\acf = \aco a_k\acf} ,
  \bleu{s=s} et \bleu{t > u},

et\\
\bleu{cout(a_k \ra a_{k+1})> cout(c \leftarrow a_{k+1})} parce que
\bleu{\aco a_k\acf \gg \aco a_{k+1}\acf}.
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Décroissance des preuves}
Si la transition est \emph{Simplify}.

\begin{center}
  \bl{\xymatrix @C 3pt @R 6pt {
      a_k  \ar@{=}[rr]_{E_\infty} && a_{k+1}\\
      &\ar@{=>}[d]\\
      &&\\
      a_k \ar@{=}[ddr]_{E_\infty}&& \ar[ddl]^{R_\infty}a_{k+1}\\
      &&\\
      &c&
}}
\end{center}

\begin{scriptsize}
\bleu{cout(a_k = a_{k+1}) > cout(a_k = c)} parce que  \bleu{\aco a_k,
  a_{k+1}\acf \gg \aco a_k, c\acf}

et

\bleu{cout(a_k = a_{k+1})> cout(c \leftarrow a_{k+1})} parce que  \bleu{\aco a_k,
  a_{k+1}\acf \gg \aco a_{k+1}\acf}.
\end{scriptsize}
\vfill
\end{slide}

%------------------------------------------------------
\begin{slide}
 \heading{Décroissance des preuves}
Si la transition est \emph{Collapse}.

\begin{center}
  \bl{\xymatrix @C 3pt @R 5pt {
      a_k  \ar[rr]_{R_\infty} && a_{k+1}\\
      &\ar@{=>}[d]\\
      &&\\
      a_k \ar[ddr]_{R_\infty}&& \ar@{=}[ddl]^{E_\infty}a_{k+1}\\
      &&\\
      &c&
}}
\end{center}

\begin{scriptsize}
  \bleu{cout(a_k \ra a_{k+1}) = (\aco a_k\acf, s, t) > cout(a_k \ra c)=
    (\aco a_{k}\acf,
    l, r) } parce que \bleu{\aco a_k\acf = \aco a_k\acf}, et ou bien
  ou bien \bleu{s\subsum l} ou bien \bleu{s=l} et \bleu{t>r}.\\
et\\
\bleu{cout(a_k \ra a_{k+1})> cout(c = a_{k+1})} parce que  \bleu{\aco
  a_k\acf \gg \aco c, a_{k+1}\acf}.
\end{scriptsize}
\vfill
\end{slide}

%------------------------------------------------------
\begin{slide}
 \heading{Décroissance des preuves}
Si la transition est \emph{Orient}.

\begin{center}
  \bl{\xymatrix @C 3pt @R 6pt {
      a_k  \ar@{=}[rr]_{R_\infty} && a_{k+1}\\
      &\ar@{=>}[d]\\
      &&\\
      a_k  \ar[rr]_{R_\infty} && a_{k+1}\\
}}
\end{center}

\begin{scriptsize}
  \bleu{cout(a_k = a_{k+1}) > cout(a_k \ra a_{k+1})} parce que
  \bleu{\aco a_k, a_{k+1}\acf \gg \aco a_k\acf}.
\end{scriptsize}
\vfill
\end{slide}

%------------------------------------------------------
\begin{slide}
  \heading{Décroissance des preuves} \verdir{Comment décroître un pic ?}
  \bleu{a_{k-1}\subar{R_\infty}a_k\rasub{R_\infty}a_{k+1}}

Sans nuire à la généralité, on peut supposer que le pic est un pic
dans \bleu{R_\omega} soit
\bleu{a_{k-1}\subar{R_\omega}a_k\rasub{R_\omega}a_{k+1}}. 

Sinon ce pic disparaît par l'une des transitions \emph{Compose} ou
\emph{Collapse} déjà vues.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Décroissance des preuves} \verdir{Comment décroître un pic ?}

Deux cas :
\begin{enumerate}
\item il s'agit d'une paire critique de  \bleu{R_\omega},
\item il s'agit de deux règles qui s'appliquent sans superposition.
\end{enumerate}
\vfill
\end{slide}

%------------------------------------------------------
\begin{slide}

\verdir{Comment décroître un pic ?}



Pour le cas 1, grâce à l'équité, on sait qu'une transition
\emph{Deduce} va s'appliquer tôt ou tard et

\begin{center}
  \bl{\xymatrix @C 3pt @R 6pt {
      && a_k \ar[lld]^{R_\omega}\ar[rrd]_{R_\omega}&\\
      a_{k-1} &&&& a_{k+1}\\
      &&\ar@{=>}[d]\\
      &&\\
      a_{k-1} \ar@{=}[rrrr]_{E_\infty} &&&& a_{k+1}}}
\end{center}

et on remarque que \bleu{\aco a_k\acf \gg \aco a_{k-1},
  a_{k+1}\acf} 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

\verdir{Comment décroître un pic ?}

Pour le cas 2, sans le besoin d'aucune transition cette preuve a,\\
à l'étape \bleu{i}, une preuve d'un coût moindre.

\begin{center}
  \bl{\xymatrix @C 3pt @R 6pt {
      & a_k \ar[ld]^{R_\omega}\ar[rd]_{R_\omega}&\\
      a_{k-1} & & a_{k+1}\\
      &\ar@{=>}[d]&\\
      &&\\
      a_{k-1} \ar@{.>}[rd]^{*}_{R_\infty}& &
      a_{k+1}\ar@{.>}[ld]_{*}^{R_\infty}\\ 
      &c&}}
\end{center}

En effet, \bleu{\aco a_k\acf} domine toutes les étapes de réécriture de
\bleu{a_{k-1} \rastar c \xymatrix{\ar@{<-}[r]^{*} &} a_{k+1}}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \doublebox{\parbox{8cm}{\emph{Théorème :} 

      \textit{Le contrôle de la complétion est supposé équitable.}

      \bigskip
      
      Si il existe une preuve \PP{} dans \bleu{E_\infty\cup R_\infty}\\
      qui n'est pas une preuve de réécriture %
      \ali alors il existe dans \bleu{E_\infty\cup R_\infty} une
      preuve $\PP'$ équivalente à \PP{} telle que $\PP\gec \PP'$.}}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \doublebox{\parbox{8cm}{\emph{Théorème :} 

      \textit{Le contrôle de la complétion est supposé équitable.}

      \bigskip
     
      Si il existe une preuve \PP{} dans \bleu{E_\infty\cup R_\infty}\\
      qui n'est pas une preuve de réécriture %
      \ali alors il existe dans \bleu{E_\infty\cup R_\infty} une
      preuve $\PP'$ équivalente à \PP{} telle que $\PP\gec \PP'$.}}

\vspace*{40pt}

Par les résultats précédents, si la preuve \PP{} n'est pas une preuve
par réécriture, elle peut-être réduite.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \doublebox{\parbox{9.3cm}{\emph{Corollaire:} 
  
      \textit{Le contrôle de la complétion est supposé équitable.}

      \bigskip
     
     \begin{itemize}
      \item Si il existe une preuve \PP{} dans \bleu{E_\infty\cup
          R_\infty} \ali alors il existe une \emph{preuve de réécriture
        equivalente} dans \bleu{R_\omega}.
      \item \bleu{R_\omega} est \emph{canonique}, c-à-d est
        \verdir{confluent}, \verdir{terminant} et \verdir{interréduit}.

      \item Si \bleu{R_\omega} est fini alors \emph{le problème du mot} dans
        \bleu{E_0} est \emph{décidable}. 
\end{itemize}
}}

\vfill
\end{slide}

\end{document}
