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