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