\begin{frame}
  \small
  
  \begin{block}{Question}
  How to find suitable polynomials ?
  \end{block}
  
  \bigskip
  
  \begin{block}<2->{Modern Approach}
  \begin{enumerate}
  \item[(a)]~
  choose \alert<2>{abstract} polynomial interpretations
  (linear, quadratic, \dots)
  \item[(b)]<3->~
  transform rewrite rules into polynomial ordering constraints
  \item[(c)]<4->~
  add monotonicity and well-definedness constraints
  \item[(d)]<5->~
  eliminate universally quantified variables
  \item[(e)]<6->~
  translate resulting constraints to SAT or SMT problem
  \end{enumerate}
  \end{block}
\end{frame}