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