30/53
\begin{frame}
  \small
  
  \begin{theorem}[Toyama's Theorem]
  \smallskip
  Confluence is modular for disjoint TRSs.
  \smallskip
  \end{theorem}
  
  \bigskip
  
  \begin{remark}<2->
  \smallskip
  Confluence is \alert{not} modular for constructor-sharing TRSs.
  \smallskip
  \end{remark}
  
  \bigskip
  
  \begin{example}<3->
  \smallskip
  \[
  \GREEN{\begin{array}{r@{~~}c@{~~}l}
  \m{f}(x,x) & \to & \m{a} \\
  \m{f}(x,\alert<4>{\m{g}}(x)) & \to & \m{b}
  \end{array}}
  ~\:\qquad\:~
  \BlUE{\begin{array}{r@{~~}c@{~~}l}
  \m{c} & \to & \alert<4>{\m{g}}(\m{c})
  \end{array}}
  \]
  \onslide<5->
  \[
  \GREEN{\begin{array}{c@{~~}c@{~~}c@{~~}c@{~~}c@{~~}c@{~~}c}
  \m{a} & \from & \m{f}(\BlUE{\m{c}},\BlUE{\m{c}}) & \BlUE{\to} &
  \m{f}(\BlUE{\m{c}},\m{g}(\BlUE{\m{c}})) & \to & \m{b}
  \end{array}}
  \]
  \vspace{-2ex}
  \end{example}
\end{frame}