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