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

          \alert{$\interpretin{f}{\model{\amodel}} : A^n \to A$}
          for every $n$-ary function symbol $f \in \asetfuncs\,$ 
          \alert{$\interpretin{P}{\model{\amodel}} \subseteq A^n$}
          for every $n$-ary predicate symbols $P \in \asetpreds$
  A symbol is \alert{$n$-ary} if it has $n$ arguments.      

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