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