\begin{frame}[label=completeness] \small \begin{theorem} \smallskip \begin{itemize} \item termination is modular for disjoint \alert<1>{left-linear} confluent TRSs \item<2-> termination is modular for constructor-sharing confluent \alert<2>{CSs} \smallskip \end{itemize} \end{theorem} \medskip \begin{definition}<2-> \smallskip TRS $\RR$ over signature $\FF$ is \alert<2>{constructor system} (\alert<2>{CS}) if $\seq{l} \in \TT(\FF_\CC,\VV)$ for every left-hand side $f(\seq{l})$ of rewrite rules in $\RR$. \smallskip \end{definition} \medskip \begin{theorem}<3-> \smallskip \begin{itemize} \item weak normalization is modular for constructor-sharing TRSs \item<4-> local confluence is modular for constructor-sharing TRSs \item<5-> semi-completeness is modular for constructor-sharing TRSs \smallskip \end{itemize} \end{theorem} \end{frame}