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