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