\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 $\Rightarrow$]
    Let $\atrs$ be WCR.
    \pause\medskip
    
    Assume that there exists a non-convergent critical pair $s \cp t$.
    \pause\medskip
    
    Then $s \from \cdot \to t$, and not $s \join t$.
    \pause
    This would contradict WCR.
  \end{proof}
\end{frame}