\begin{frame}{Reminder: Models and Environments}
  Let \vspace{-.5ex}
  \begin{itemize}\setlength{\itemsep}{0ex}
    \item $\asetfuncs$ be a set of function symbols,  
    \item $\asetpreds$ a set of predicate symbols.
  \end{itemize}
  
  \begin{block}{}  
    A \emph{model} $\model{\amodel}$ for $\pair{\asetfuncs}{\asetpreds}$
    consists of:
    \begin{itemize}
      \item 
        a non-empty set~$\model{\adomain}$, called \emph{domain} or \emph{universe},
      \item
        an \emph{interpretation operation} $(\cdot)^{\model{\amodel}}$
        for the symbols in $\asetfuncs$, $\asetpreds$.

        \begin{enumerate}[(i)]
        \item
          \alert{$\interpretin{f}{\model{\amodel}} : A^n \to A$}
          for every $n$-ary function symbol $f \in \asetfuncs\,$ 
          \vspace*{0.75ex}
        \item
          \alert{$\interpretin{P}{\model{\amodel}} \subseteq A^n$}
          for every $n$-ary predicate symbols $P \in \asetpreds$
        \end{enumerate}
    \end{itemize}
  \end{block}
  A symbol is \alert{$n$-ary} if it has $n$ arguments.      
  \medskip

  \begin{goal}{}
    An \emph{environment}~(look-up function)
    \begin{talign}
      \saluf \funin \textbf{var} \to \adomain
    \end{talign} 
    interprets \alert{free} variables in the domain. 
  \end{goal}
\end{frame}