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