\begin{frame}
  \frametitle{Currying}

  \begin{example}
  Currying $A(x, S(y))$ gives $A\;x\;(Sy)$
  \end{example}
  \pause
  
  \begin{itemize}
    \item 
    One binary function symbol {$\Ap$} and for the rest only constants.
  \end{itemize}
  \pause
  \medskip
  
  \begin{definition}
  For each TRS $(\Sigma, R)$ we define a \emph{curried} version
  $(\Sigma,R)^{\cur}=  (\Sigma^{\cur},\;R^{\cur})$.\\
  \medskip
  $R^{\cur}$ has rules  $\cur(t) \to \cur(s)$ for $t \to s$ in $R$, where:
  \[\begin{array}{lll}
  \cur(x) & = &  x \\
  \cur(F(t_1,\ldots,t_n))& =& F \, \cur(t_1)\,\ldots\,\cur(t_n)
  \end{array}\]
  \end{definition}
\end{frame}