\documentclass[12pt]{article}

\usepackage{a4}
\usepackage[latin1]{inputenc}
\usepackage[francais]{babel}
\usepackage[all]{xy}
\usepackage{amsfonts,amsmath,amsthm,amssymb,stmaryrd}

\renewcommand{\phi}{\varphi}

\renewcommand{\S}{\textbf{S}}
\newcommand{\bl}[1]{#1}
\newcommand{\bleu}[1]{$#1$}
\newcommand{\Un}{\textsf{\textbf{1}}}
\newcommand{\Y}{\mathbf{Y}}
\newcommand{\K}{\mathbf{K}}
\newcommand{\I}{\mathbf{I}}
\newcommand{\T}{\mathbf{T}}
\newcommand{\F}{\mathbf{F}}
\newcommand{\jnt}{\uparrow}
\newcommand{\ou}{\ensuremath{\mathbf{ou}\ }}
\newcommand{\non}{\ensuremath{\mathbf{non}}}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\eq}{\stackrel{?}{=}}
\newcommand{\cro}{[\!\![}
\newcommand{\crf}{]\!\!]}
\newcommand{\aco}{\{\!\!\{}
\newcommand{\acf}{\}\!\!\}}
\newcommand{\Nat}{\mathbb{N}}

\newcommand{\field}[1]{\mathbb{#1}}


\newcommand{\un}[1]{{\underline{#1}}}
\newcommand{\id}{{\mathrm{id}}}
\newcommand{\shift}{{\uparrow}}
\newcommand{\lift}{\mathop{\Uparrow}}
\newcommand{\liftn}[1]{\mathop{\Uparrow^{#1}}}
\newcommand{\comp}{\mathrel{\circ}}

%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix @C 15pt {\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix @C 15pt {\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix @C 15pt {\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 @C 15pt {\ar@{>}[r]_{#1} &}}
\newcommand{\subar}[1]{\xymatrix @C 15pt {\ar@{<-}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix @C 15pt {\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix @C 15pt {\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix @C 15pt {\ar@{>}[r]^{#1} &}}
\newcommand{\supar}[1]{\xymatrix @C 15pt {\ar@{<-}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix @C 15pt {\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix @C 15pt {\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\rarasupsub}[2]{\xymatrix @C 15pt {\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\cv}[1]{\xymatrix @C 20pt {\ar@{<->}[r]_{#1} &}}
\newcommand{\conv}[1]{\xymatrix @C 20pt {\ar@{<->}[r]_{#1}^{*} &}}
\newcommand{\convplus}[1]{\xymatrix @C 20pt {\ar@{<->}[r]_{#1}^{+} &}}

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

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\Rar}{\subar{R}}
\newcommand{\rastarR}{\rasupsub{*}{R}}
\newcommand{\raraR}{\rarasub{R}}
\newcommand{\raS}{\rasub{S}}
\newcommand{\raT}{\rasub{T}}
\newcommand{\Sar}{\subar{S}}
\newcommand{\rastarS}{\rasupsub{*}{S}}
\newcommand{\raraS}{\rarasub{S}}
\newcommand{\plusararR}{\xymatrix @C 15pt {&\ar@{>>}[l]^{R}_+}}
\newcommand{\plusraraR}{\rarasupsub{+}{R}}
\newcommand{\rapar}{\xymatrix @ -1.5pc {\ar@{>}[rr]&||&}}
\newcommand{\rarapar}{\xymatrix @ -1.5pc {\ar@{>>}[rr]&||&}}

%\pagestyle{empty}


\title{Magistère d'Informatique et Modélisation}
\author{Partiel de réécriture}

\date{\emph{Mars 2002}}

\newcommand{\infer}[2]{
 \begin{array}{c}
   #1\\
   \hline \noalign{\vskip 1pt}#2
  \end{array}}

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

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

 \newcommand{\inferSideLabel}[4]{
 {#1} \;\; 
  \begin{array}{c}
  #2 \\
  \hline \noalign{\vskip 1pt}#3
  \end{array}
  \quad {\textrm{#4}}}

\begin{document}
\maketitle 
\thispagestyle{empty}

\centerline{\textit{Documents autorisés.}}

\section*{Exercice 1}
On considère le système~\footnote{Extrait d'un système plus complet
lié aux calculs de substitutions explicites.  Ceci dit, si la syntaxe
vous gène, vous pouvez la traduire en une syntaxe plus classique.} de réécriture :
  \begin{align*}
    (\lambda a)\,b &  \ra  a[b/] \tag{B} \\
    (a\,b)[s] &  \ra  a[s]\,b[s] \tag{App} \\
    (\lambda a)[s] &  \ra  \lambda a[\lift(s)] \tag{Lambda} \\
    a[s][t] &  \ra  a[s \comp t] \tag{Clos} \\
    (s \comp t) \comp u &  \ra  s \comp (t \comp u)
    \tag{AssEnv} \\
    a/ \comp s &  \ra  \lift(s) \comp a[s]/ \tag{MapSl} \\
     \shift \comp (\lift(s) \comp t) &  \ra  s \comp
    (\shift \comp t) \tag{ShiftLift} \\
    \end{align*}

qui correspond à la syntaxe :
  \begin{align*}
    a, b & ::= \lambda a \mid a\,b \mid a[s] \tag{Termes} \\
    s, t & ::= a/ \mid s \comp t \mid \lift(s)  \mid \shift \tag{Substitutions}
  \end{align*}

\begin{enumerate}
\item Ce système admet-il une superposition? Si oui quelle est la
  paire critique correspondante?  Est-ce que cette paire critique est
  convergente?
\item Montrer que $\shift \comp (a/ \comp (\shift \comp b/))
  \ra \shift \comp (b/ \comp (\shift \comp a[\shift \comp b/]/))$.
\item Ce système termine-t-il ?
\end{enumerate}
\newpage
\section*{Exercice 2 sur les relations abstraites}

Soit un ensemble $E$ muni de deux relations $\raR$ et  $\raS$ et d'une
fonction $x\mapsto \bar{x}$  de $E$ dans $E$
telles
que
\begin{itemize}
  
\item $\raS\subseteq\raR$,
\item $x \rastarR \bar{x}$,
\item $x \raR y \quad \Rightarrow \quad \bar{x}\rastarS \bar{y}$.
\end{itemize}


\begin{enumerate}
\item Montrer que si $\raS$ est confluente alors $\raR$ est
  confluente.
\item Peut-on affaiblir ces conditions?
\end{enumerate}

\end{document}

