\begin{frame}
  \frametitle{Interpretation of terms}
  
  \begin{definition}[Interpretation of Terms]
    Let $\alpha : {\cal X} \to A$ be an interpretation of the variables.\\
    We define the evaluation of terms 
    \vspace{-1ex}
    $$\interpret{\cdot,\alpha} : \TTlong \to A$$
    \vspace{-2ex}
    inductively:
    \begin{align*}
      \interpret{x,\alpha} &= \alpha(x) && \text{if $x \in {\cal X}$} \\
      \interpret{f(t_1,\ldots,t_n),\alpha} &= \interpret{f}(\interpret{t_1,\alpha},\ldots,\interpret{t_n,\alpha})
    \end{align*}
    \vspace{-1.5em}
  \end{definition}
  \pause
  
  \begin{example}
  \vspace{-1em}
  \begin{align*}
    \interpret{0} &= 1 & \interpret{{\rm s}}(x) &= x+1 & \interpret{{\rm A}}(x,y) &= x + 2\cdot y
  \end{align*}
  \vspace{-1.5em}
  
  Let $\alpha(x) = 1$, $\alpha(y) = 3$, we calculate:
  \begin{itemize}
  \pause
    \item $\interpret{{\rm A}(0,{\rm s}(0)),\alpha} = \pause 5$,
  \pause
    \item $\interpret{{\rm A}({\rm s}(x),y),\alpha} = \pause 8$.
  \end{itemize}
  \end{example}
\end{frame}