\begin{frame}[t]{Model plus Environments}
  \examplemodelwith{
    \begin{goal}{}
      An \alert{environment}~
      \begin{talign}
        \saluf \funin \textbf{var} \to \adomain
      \end{talign}
      (look-up function) 
      interprets \alert{free} variables in the domain. 
    \end{goal}
    \medskip
  }
  \pause\medskip
  
  Example environment:
  \begin{talign}
    \aluf{\freevar{x}} = a_1 && 
    \aluf{\freevar{y}} = a_3
  \end{talign}
  \pause
  Let us determine whether
  \begin{itemize}\setlength{\itemsep}{0pt}
    \item<3->  
      \parbox{17ex}{$\model{\amodel} \alt<3| handout:0>{\satisfieslookupblack{\saluf}}{\satisfieslookup{\saluf}} \formula{\unpred{P}{\freevar{x}}}$}
        % $\M \;\mw_\saluf \; Px$  
        \hspace{3em}
        \pause{}
      \uncover<5->{$\model{\amodel} \alt<5| handout:0>{\satisfieslookupblack{\saluf}}{\satisfiesnotlookup{\saluf}} \formula{\unpred{P}{\freevar{y}}}$}
        % $\M \;\not\mw_\saluf \; Py$   
      \pause
      
    \item<7-> 
      \parbox{17ex}{$\model{\amodel} \alt<7| handout:0>{\satisfieslookupblack{\saluf}}{\satisfiesnotlookup{\saluf}} \formula{\binpred{R}{\freevar{x}}{\freevar{x}}}$}
        % $\M \;\not\mw_\saluf \; Rxx$  
      \hspace{3em}
      \pause{}
      \uncover<9->{$\model{\amodel} \alt<9| handout:0>{\satisfieslookupblack{\saluf}}{\satisfieslookup{\saluf}} \formula{\binpred{R}{\freevar{y}}{\freevar{y}}}$} 
        % $\M \;\mw_\saluf \; Ryy$  
      \pause
      
    \item<11-> 
      \parbox{17ex}{$\model{\amodel} \alt<11| handout:0>{\satisfieslookupblack{\saluf}}{\satisfieslookup{\saluf}} \formula{\binpred{R}{\freevar{x}}{\freevar{y}}}$}
        % $\M \;\mw_\saluf \; Rxy$  
      \pause
      
    \item<13->
      \parbox{17ex}{$\model{\amodel} \alt<13| handout:0>{\satisfieslookupblack{\saluf}}{\satisfiesnotlookup{\saluf}} \formula{\binpred{R}{\freevar{y}}{\freevar{x}}}$}
        % $\M \;\not\mw_\saluf \; Ryx$   
      \pause
      
    \item<15-> 
      \parbox{17ex}{$\model{\amodel} 
                       \alt<15| handout:0>{\satisfieslookupblack{\saluf[\freevar{x}\mapsto a_2]}}{\satisfieslookup{\saluf[\freevar{x}\mapsto a_2]}} 
                     \formula{\binpred{R}{\freevar{y}}{\freevar{x}}}$}  
        % $\M \;\mw_{\saluf[x\mapsto a_2]} \;  Ryx$ 
      \hspace{3em}  
      \pause
      \uncover<17->{$\model{\amodel} \alt<17| handout:0>{\satisfieslookupblack{\saluf}}{\satisfieslookup{\saluf}} \formula{\existsst{x}{\,\binpred{R}{\freevar{y}}{x}}}$}
        % $\M \;\mw_\saluf \eris x Ryx$
        \onslide<18->{}
  \end{itemize}  
  \bigskip
\end{frame}