\begin{frame} \small \begin{theorem} \smallskip Every weakly orthogonal TRSs is confluent. \end{theorem} %AM proof can be skipped as it is subsumed by proof on next slide \begin{proof}<2->[Proof Sketch] \begin{itemize} \item ${\mparr \cdot \parr} \subseteq {\parr \cdot \mparr}$ \vspace{-3ex} \begin{center} \begin{tikzpicture}[on grid,node distance=9mm] \node (1) {$\cdot$}; \node (2) [right=of 1] {\alt<3->{$\cdot$}{}}; \node (3) [right=of 2] {}; \node (4) [right=of 3] {$\cdot$}; \node (4a) [below=of 4] {}; \node (4b) [below=of 4a] {}; \alt<3->{ \draw[->] (1) -- (2); \draw[->] (2) -- (4) node[midway] {$\|$}; }{ \draw[->] (1) -- (4) node[midway] {$\|$}; } \node (1a) [below=of 1] {\alt<3->{$\cdot$}{}}; \node (1b) [below=of 1a] {}; \node (1c) [below=of 1b] {$\cdot$}; \alt<3->{ \draw[->] (1) -- (1a); \draw[->] (1a) -- (1c) node[midway,sloped] {$\|$}; }{ \draw[->] (1) -- (1c) node[midway,sloped] {$\|$}; } \onslide<4->{ \path (1a) -- (2) node[midway,sloped] {$=$}; } \onslide<5->{ \draw[->] (1a) -- (4) node[midway,sloped] {$\|$}; } \onslide<6->{ \node (4c) [below=of 4b] {$\cdot$}; \draw[->] (4) -- (4c) node[midway,sloped] {$\|$}; \draw[->] (1c) -- (4c) node[midway] {$\|$}; \path (1) -- (4c) node[midway,anchor=north] {IH}; } \end{tikzpicture} \qquad \raisebox{15mm}{\onslide<3->{\makebox[0mm][l]{interesting case}}} \end{center} \vspace{-3ex} \item<7-> ${\to} \subseteq {\parr} \subseteq {\to^*}$ \smallskip \end{itemize} \end{proof} \end{frame}