\begin{frame}[t] \frametitle{Local Confluence} \begin{block}{Critical Pair Lemma} \smallskip A TRS is locally confluent (WCR) \quad$\iff$\quad all critical pairs are convergent. \end{block} \medskip\pause \begin{theorem} WCR and CR are decidable properties for terminating, finite TRSs. \end{theorem} \pause \begin{proof} For terminating $R$ we have $\text{CR} \Leftrightarrow \text{WCR}$. \pause We decide WCR as follows: \pause \smallskip For every $s \cp t \in \CP(\atrs)$ we check $s \join t$ by computing: \begin{itemize} \item the set of reducts of $s$: $\to(s) = \{s' \mid s\to^* s'\}$, and \item the set of reducts of $t$: $\to(t) = \{t' \mid t\to^* t'\}$. \end{itemize} (In a finite, terminating TRS every term has only only finitely many reducts.) \pause\smallskip Then $s \join t$ if and only if ${\to(s)} \cap {\to(t)} \ne \emptyset$. \end{proof} \end{frame}