\begin{frame} \small \begin{lemma} \smallskip Every orthogonal TRS is locally confluent. \end{lemma} \pause \begin{proof} All critical pairs are convergent (are are none). \smallskip Hence we have WCR by the Critical Pair Lemma. \end{proof} \medskip\pause \begin{theorem} \smallskip Every orthogonal TRS is \alert<1>{confluent} \\[-3ex] \[ \qquad\qquad\qquad\begin{tikzpicture}[on grid,baseline=(1).baseline] \node (1) {$\strut s$}; \node (2) [below left=of 1] {$t$}; \node (3) [below right=of 1] {$u$}; \node (4) [below right=of 2] {$\strut \alert<2>{v}$}; \node (5) [left=of 1] {\makebox[3cm][l]{$\strut\forall s,t,u$}}; \node (6) [left=of 4] {\makebox[3cm][l]{$\strut\alert<2>{\exists v}$}}; \draw[->>] (1) -- (2); % node[midway,sloped,above] {${}_*$}; \draw[->>] (1) -- (3); % node[midway,sloped,above] {${}_*$}; \draw[dotted,->>] (2) -- (4); % node[midway,sloped,below] {${}^*$}; \draw[dotted,->>] (3) -- (4); % node[midway,sloped,below] {${}^*$}; \end{tikzpicture} \] \end{theorem} \pause For orthogonal TRSs there is a canonical way to compute common reduct\ldots \end{frame}