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