\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}