\begin{frame}[t] \vspace{-1ex} \begin{example} \vspace{-1em} \begin{align*} \minus(x,0) &\to x\\ \minus(\s(x),\s(y)) &\to \minus(x,y)\\ \quot(0,\s(y)) &\to 0\\ \quot(\s(x),\s(y)) &\to \s(\quot(\minus(x,y),\s(y))) \end{align*} \vspace{-3.5em} \pause \begin{align*} \DP(R) = \{\; \alert<5>{\minus_\#(\s(x),\s(y))} &\alert<5>{\to \minus_\#(x,y)}\\ \ungray{-3}{\alert<3>{\quot_\#(0,\s(y))}} &\ungray{-3}{\alert<3>{\to 0_\#}}\\ \ungray{-3}{\alert<3>{\quot_\#(\s(x),\s(y))}} &\ungray{-3}{\alert<3>{\to \s_\#(\quot(\minus(x,y),\s(y)))}}\\ \alert<5>{\quot_\#(\s(x),\s(y))} &\alert<5>{\to \quot_\#(\minus(x,y),\s(y))}\\ \alert<5>{\quot_\#(\s(x),\s(y))} &\alert<5>{\to \minus_\#(x,y)}\\ \ungray{-3}{\alert<3>{\quot_\#(\s(x),\s(y))}} &\ungray{-3}{\alert<3>{\to \s_\#(y)}} \;\} \end{align*} \vspace{-1.5em} \pause \alt<-3>{ We use the interpretation: \vspace{-.5em} \begin{gather*} \interpret{\minus_\#}(x,y) = 1 \quad \interpret{\quot_\#}(x,y) = 1 \quad \interpret{\minus}(x,y) = x \quad \interpret{\s}(x) = x\\ \interpret{{\rm f}}(\vec{x}) = 0 \text{ for all other symbols ${\rm f}$} \end{gather*} \vspace{-2ex} }{} \alt<4->{ The following interpretation removes the remaining DP rules: \vspace{-.5em} \begin{gather*} \interpret{\minus_\#}(x,y) = \interpret{\minus}(x,y) = \interpret{\quot_\#}(x,y) = \interpret{\quot}(x,y) = x \\ \interpret{\s}(x) = x+1 \quad\quad \interpret{0} = 0\\[-4.5ex] \end{gather*}% Thus we have proven termination. }{}% \end{example} \vspace{10cm} \end{frame}