\begin{frame}
  \frametitle{Polynomial interpretations}
  
  \begin{definition}
  A \emph{polynomial interpretations} over $\nat$ consists of:
  \begin{itemize}
    \item $\Sigma$-algebra is $(\nat,\interpret{\cdot})$,
    \item $>$ defined as usual on $\nat$,
    \item the interpretations $\interpret{f}$ are polynomials.
  \end{itemize}
  \end{definition}
  \bigskip
  \pause
  
  The first two conditions of well-founded monotone $\Sigma$-algebras are fulfilled:
  \begin{itemize}
  \pause
    \item $(\nat,\interpret{\cdot})$ is a $\Sigma$-algebra
  \pause
    \item \structure{$>$ is well-founded}
  \end{itemize}
  \pause
  
  \begin{block}{}
  However, to prove termination we need to check:
  \begin{itemize}
  \pause
    \item \alert{monotonicity} of the polynoms \alert{$\interpret{f}$}, and
  \pause
    \item \alert{${R} \subseteq {>}$}, that is, $\interpret{\ell,\alpha} > \interpret{r,\alpha}$ for all $\ell \to r \in R$ and $\alpha : \VV \to A$
  \end{itemize}
  \end{block}
\end{frame}