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