174/365
\begin{frame}
  \small
  
  \begin{example}
  \begin{itemize}
  \item
  rewrite system
  \[
  \GREEN{
  \begin{array}{r@{~\to~}l}
  \makebox[20mm][r]{$\m{0}+y$} & \makebox[20mm][l]{$y$} \\[.5ex]
  \mS(x)+y & \mS(x+y)
  \end{array}
  }
  \]
  \item<2->
  interpretations
  \[
  \begin{array}{r@{~=~}l}
  \makebox[20mm][r]{$\GREEN{\m{0}}_{\AA}$} &
  \makebox[20mm][l]{$\alt<8>{0}{\RED{a}}$}
  \\[.5ex]
  \GREEN{\mS}_{\AA}(x) & \alt<8>{x+1}{\RED{b}x+\RED{c}} \\[.5ex]
  \GREEN{+}_{\AA}(x,y) & \alt<8>{2x+y+1}{\RED{d}x+\RED{e}y+\RED{f}} \\[.5ex]
  \end{array}
  \]
  \item<3->
  \alt<6->{diophantine}{polynomial} constraints
  \quad \onslide<3-5>{$\forall x, y \in \NN$}
  \vspace{-1ex}
  \[
  \begin{array}{r@{~>~}l}
  \makebox[20mm][r]{$\alt<6->{\RED{e}-1 \geqslant 0 \quad
  \RED{d}\RED{a}+\RED{f}}
  {\alt<5>{(\RED{e}-1)y+\RED{d}\RED{a}+\RED{f}}
  {\RED{d}\RED{a}+\RED{e}y+\RED{f}}}$} &
  \makebox[20mm][l]{$\alt<5->{0}{y}$}
  \\[.5ex]
  \makebox[20mm][r]{$\alt<6->{
  \RED{e}-\RED{b}\RED{e} \geqslant 0 \quad
  \RED{d}\RED{c}+\RED{f}-\RED{b}\RED{f}-\RED{c}}
  {\alt<5>{(\RED{e}-\RED{b}\RED{e})y+
  \RED{d}\RED{c}+\RED{f}-\RED{b}\RED{f}-\RED{c}}
  {\RED{d}\,(\RED{b}x+\RED{c})+\RED{e}y+\RED{f}}}$}
  &
  \makebox[20mm][l]{$\alt<5->{0}
  {\RED{b}\,(\RED{d}x+\RED{e}y+\RED{f})+\RED{c}}$}
  \\[.5ex]
  \multicolumn{2}{c}{\makebox[0mm]{$
  \onslide<4->
  \RED{a} \geqslant 0 \quad
  \RED{b} \geqslant 1 \quad
  \RED{c} \geqslant 0 \quad
  \RED{d} \geqslant 1 \quad
  \RED{e} \geqslant 1 \quad
  \RED{f} \geqslant 0
  $}}
  \end{array}
  \]
  \item<7->
  possible solution
  \vspace{-1ex}
  \[
  \RED{a} = 0 \quad
  \RED{b} = 1 \quad
  \RED{c} = 1 \quad
  \RED{d} = 2 \quad
  \RED{e} = 1 \quad
  \RED{f} = 1
  \]
  \vspace{-4ex}
  \end{itemize}
  \end{example}
\end{frame}