\begin{frame}
  \small
  
  \begin{definitions}
  \begin{itemize}
  \item
  An \alert{overlap} is a triple
  $\langle \ell_1 \to r_1, p, \ell_2 \to r_2 \rangle$ such that \\[-.5ex]
  \begin{enumerate}
  \pause
  \item
  $\ell_1 \to r_1$ and $\ell_2 \to r_2$ are rewrite rules
  \smallskip\pause
  \item
  $p \in \Pos_\FF(\ell_2)$ a non-variable position in $\ell_2$
  \smallskip\pause
  \item
  $\ell_1$ and ${\ell_2}|_p$ have a common instance
  \smallskip\pause
  
  Let $\sigma$ and $\tau$ substitutions such that $\ell_1 \sigma = {\ell_2}|_p \tau$ is the mgci.\\
  (w.l.o.g. $\mit{dom}(\tau) = \Var({\ell_2}|_p)$ and $\Var(({\ell_2}|_p)\tau) \cap \Var({\ell_2}[\Box]_p) = \emptyset$)
  \smallskip\pause
  \item
  if $p = \epsilon$ then $(\ell_1 \to r_1) \;\ne\; (\ell_2 \to r_2)$
  \end{enumerate}
  \pause
  Then we have steps
  $\ell_2\tau[r_1\alert<3>{\sigma}]_p
   \from
  \ell_2\tau[\ell_1\alert<3>{\sigma}]_p =
  \ell_2\tau \to
  r_2 \tau$.
  \medskip\pause
  
  We call $\ell_2\tau[r_1\alert<3>{\sigma}]_p
   \cp
  r_2 \tau$ \alert{critical pair}.
  \smallskip\pause
  
  \item<5->
  A critical pair $s \cp t$ is \alert{convergent} if $s \join t$.
  \smallskip
  \end{itemize}
  \end{definitions}
  
  \bigskip\pause
  
  \begin{block}<6->{Critical Pair Lemma (Huet 1980)}
  \smallskip
  A TRS is locally confluent (WCR) \quad$\iff$\quad all critical pairs are convergent.
  \end{block}
\end{frame}