\begin{frame}[t]
  \frametitle{Proof of the Critical Pair Lemma}

  \begin{block}{Critical Pair Lemma}
  \smallskip
  A TRS is locally confluent (WCR) \quad$\iff$\quad all critical pairs are convergent.
  \end{block}

  \pause
  \begin{proof}[Proof of the Direction $\Leftarrow$]
  Consider a peak
  $t_0 \mathrel{\stackrel{s_0} {\leftarrow}} t \mathrel{\stackrel{s_1}{\to}} t_1$
  ($s_0$ and $s_1$ are the contracted redex occurrences).
  \pause\medskip
  
  We have to find a common reduct $t_2$ of $t_0$ and $t_1$.
  \pause\medskip
  
  Distinguish cases according to the
  relative positions of the redexes $s_0$ and $s_1$ in $t$.\\
  \end{proof}
\end{frame}