\begin{frame}<1-7>[label=Toyama]
  \small
  
  \begin{theorem}
  \smallskip
  Termination is \alert{not} modular for disjoint TRSs.
  \smallskip
  \end{theorem}
  
  \bigskip
  
  \begin{example}<2->
  \smallskip
  \[
  \begin{array}{c@{\qquad\qquad}c}
  \GREEN{\begin{array}{r@{~}c@{~}l}
  \m{f}(\m{a},\m{b},x) & \to & \m{f}(x,x,x)
  \end{array}} &
  \BlUE{\begin{array}{r@{~}c@{~}l}
  \m{g}(x,y) & \to & x \\[.5ex]
  \m{g}(x,y) & \to & y
  \end{array}} \\
  \\[-1ex]
  \onslide<7->{\alert{\text{duplicating}}} &
  \onslide<7->{\alert{\text{collapsing \alt<8->{\& not confluent}{}}}}
  \end{array}
  \]
  
  \smallskip
  
  \onslide<3->
  \GREEN{
  \begin{align*}
  \m{f}(\m{a},\m{b},\BlUE{\m{g}(\mG{a},\mG{b})}) 
  &\uncover<4->{ \to
  \m{f}(\BlUE{\m{g}(\mG{a},\mG{b})},\BlUE{\m{g}(\mG{a},\mG{b})},
  \BlUE{\m{g}(\mG{a},\mG{b})})
  }\\[.5ex]
  &\uncover<5->{\BlUE{\to}
  \m{f}(\m{a},\BlUE{\m{g}(\mG{a},\mG{b})},\BlUE{\m{g}(\mG{a},\mG{b})})
  }\\[.5ex]
  &\uncover<6->{\BlUE{\to}
  \m{f}(\m{a},\m{b},\BlUE{\m{g}(\mG{a},\mG{b})})
  }\end{align*}
  }
  \vspace{-1ex}
  \end{example}
\end{frame}