\begin{frame}
  \small
  
  \begin{definition}[Termination \emph{$\SN(R)$}]\strut
  A rewrite system $R$ is \alert<1>{terminating} 
  if there are no infinite rewrite sequences.
  \end{definition}
  
  \bigskip
  
  \begin{block}<2->{Termination Methods \qquad
  \only{\onslide<2-7>{\alt<7->{2000s}{\alt<6>{1990s}{\alt<5>{1980s}%
  {\alt<4>{1979}{\alt<3>{1975}{1967}}}}}}}}\strut
  Knuth-Bendix order\onslide<3->, %1967
  \alert<8>{polynomial interpretations}\onslide<4->, %1975
  multiset order, %1978
  simple path order\onslide<5->, %1979
  \alert<8>{lexicographic path order}, %1980
  semantic path order, %1980
  recursive decomposition order, %1981
  multiset path order, %1982
  recursive path order, %1983
  transformation order\onslide<6->, %1990
  elementary interpretations, %1992
  type introduction, %1992
  \alert<8>{well-founded monotone algebras}, %1992
  general path order, %1995
  semantic labeling, %1995
  dummy elimination, %1995
  \alert<8>{dependency pairs}, %1997
  freezing, %1998
  top-down labeling\onslide<7->, %1998
  monotonic semantic path order, %2000
  context-dependent interpretations, %2001
  match-bounds, %2003
  size-change principle, %2003
  matrix interpretations, %2006
  predictive labeling, %2006
  uncurrying, %2006
  bounded increase, %2007
  quasi-periodic interpretations, %2007
  arctic interpretations, %2008
  increasing interpretations, %2008
  root-labeling, %2008
  \dots
  \end{block}
  
\end{frame}