\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}