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