\begin{frame} \small \begin{corollary} \smallskip Every orthogonal TRSs is confluent. \end{corollary} \medskip \begin{proof} \smallskip \begin{center} \begin{tikzpicture}[on grid] \node (1) {$\cdot$}; \onslide<2->{ \node (2) [right=of 1] {$\cdot$}; \node (3) [right=of 2] {$\cdot$}; \node (4) [right=of 3] {$\cdot$}; } \node (5) [right=of 4] {$\cdot$}; \onslide<2->{ \node (1a) [below=of 1] {$\cdot$}; \node (1b) [below=of 1a] {$\cdot$}; \node (1c) [below=of 1b] {$\cdot$}; } \onslide<3->{ \node (2a) [below=of 2] {$\cdot$}; } \onslide<4->{ \node (3a) [below=of 3] {$\cdot$}; } \onslide<5->{ \node (4a) [below=of 4] {$\cdot$}; } \onslide<6->{ \node (5a) [below=of 5] {$\cdot$}; \node (2b) [below=of 2a] {$\cdot$}; \node (3b) [below=of 3a] {$\cdot$}; \node (4b) [below=of 4a] {$\cdot$}; \node (5b) [below=of 5a] {$\cdot$}; \node (2c) [below=of 2b] {$\cdot$}; \node (3c) [below=of 3b] {$\cdot$}; \node (4c) [below=of 4b] {$\cdot$}; \node (5c) [below=of 5b] {$\cdot$}; } \alt<2->{ \draw[->] (1) -- (2); \draw[->] (2) -- (3); \draw[->] (3) -- (4); \draw[->] (4) -- (5); \draw[->] (1) -- (1a); \draw[->] (1a) -- (1b); \draw[->] (1b) -- (1c); }{ \draw[->>] (1) -- (5); \draw[->>] (1) -- (1c); } \onslide<3->{ \draw[->] (2) -- (2a) node[midway,sloped] {$\|$}; \draw[->] (1a) -- (2a) node[midway] {$\|$}; } \onslide<4->{ \draw[->] (3) -- (3a) node[midway,sloped] {$\|$}; \draw[->] (2a) -- (3a) node[midway] {$\|$}; } \onslide<5->{ \draw[->] (4) -- (4a) node[midway,sloped] {$\|$}; \draw[->] (3a) -- (4a) node[midway] {$\|$}; } \onslide<6->{ \draw[->] (5) -- (5a) node[midway,sloped] {$\|$}; \draw[->] (4a) -- (5a) node[midway] {$\|$}; \draw[->] (2a) -- (2b) node[midway,sloped] {$\|$}; \draw[->] (1b) -- (2b) node[midway] {$\|$}; \draw[->] (3a) -- (3b) node[midway,sloped] {$\|$}; \draw[->] (2b) -- (3b) node[midway] {$\|$}; \draw[->] (4a) -- (4b) node[midway,sloped] {$\|$}; \draw[->] (3b) -- (4b) node[midway] {$\|$}; \draw[->] (5a) -- (5b) node[midway,sloped] {$\|$}; \draw[->] (4b) -- (5b) node[midway] {$\|$}; \draw[->] (2b) -- (2c) node[midway,sloped] {$\|$}; \draw[->] (1c) -- (2c) node[midway] {$\|$}; \draw[->] (3b) -- (3c) node[midway,sloped] {$\|$}; \draw[->] (2c) -- (3c) node[midway] {$\|$}; \draw[->] (4b) -- (4c) node[midway,sloped] {$\|$}; \draw[->] (3c) -- (4c) node[midway] {$\|$}; \draw[->] (5b) -- (5c) node[midway,sloped] {$\|$}; \draw[->] (4c) -- (5c) node[midway] {$\|$}; } \end{tikzpicture} \end{center} \end{proof} \end{frame}