\begin{frame}
  \small
  
  \begin{block}{Validity Problem}
  \begin{tabbing}
  instance: \quad \= ES $\EE$ \quad terms $s, t$ \\
  question: \> $\EE \vDash s \approx t$ ?
  \end{tabbing}
  \end{block}
  
  \bigskip
  
  \begin{theorem}
  \smallskip
  The validity problem is
  \only{\alert<1->{\visible<1>{un}decidable}}
  \only{\alert<1->{decidable}}
  \onslide<2->for ES $\EE$ if \,$\exists$ finite TRS $\RR$ such that
  \begin{enumerate}
  \item~
  $\RR$ is \alert<2>{complete}
  (\alert<2>{confluent} and \alert<2>{terminating})
  \item<3->~
  \alert<3>{$\xleftrightarrow[\EE]{*} ~=~ \xleftrightarrow[\RR]{*}$}
  \end{enumerate}
  \end{theorem}
\end{frame}