\begin{frame}{Interpretation of Terms in Model with Environment} 
  Terms are built from variables, constants, and function symbols:\\
  \begin{itemize}
    \item variables are interpreted according to the environment $\saluf$
    \item constants are interpreted according to $(\cdot)^{\model{\amodel}}$
    \item function symbols are interpreted according to $(\cdot)^{\model{\amodel}}$
  \end{itemize}
  \pause\bigskip  

  Let $\model{\amodel}$ be a model and $\saluf$ an environment.  
  \begin{block}{Interpretation of terms}
    The interpretation  $\intin{\formula{t}}{\model{\amodel},\saluf}$
    of a term $\formula{\ater}$ is defined as:
    %
    \begin{align*}  
      \intin{\formula{\ater}}{\model{\amodel},\saluf} =
      \begin{cases}
        \aluf{\formula{\avarsynvar}} 
          & \text{if $\formula{\ater} = \formula{\avarsynvar}$ for a variable $\formula{\avarsynvar}$} 
        \\
        \intin{\aconstsynvar}{\model{\amodel}}
          & \text{if $\formula{\ater} = \aconstsynvar$ for a constant $\aconstsynvar$}
        \\
        \fap{\intin{\safuncsynvar}{\model{\amodel}}}
            {\intin{\formula{\ateri{1}}}{\model{\amodel},\saluf},
            \ldots,
            \intin{\formula{\ateri{n}}}{\model{\amodel},\saluf}}
          & \text{if $\formula{\ater} = \formula{\afuncsynvar{\ateri{1},\ldots,\ateri{n}}}$}    
      \end{cases}%  
    \end{align*}
    by induction on the term structure.          
  \end{block}
\end{frame}