70/145
\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}