\begin{frame}[t]{Interpreting Formulas with Equality} \examplemodel \bigskip \begin{itemize}\setlength{\itemsep}{0.4ex} \pause \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfiesnot} \formula{\equalto{\const{\orange{b}}}{\const{\forestgreen{c}}}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfies} \formula{\equalto{\const{\orange{b}}}{\const{\orange{b}}}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfieslookupblack{\saluf[\freevar{x} \mapsto a_1]}}}{\satisfieslookup{\saluf[\freevar{x} \mapsto a_1]}} \formula{\notequalto{\freevar{x}}{\const{\forestgreen{c}}}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfieslookupblack{\saluf[\freevar{x} \mapsto a_1]}}}{\satisfieslookup{\saluf[\freevar{x} \mapsto a_1]}} \formula{\equalto{\freevar{x}}{\freevar{x}}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfies} \formula{\forallst{x}{\:\equalto{x}{x}}}$ \updatepause \item $\model{\amodel} \malt[1]{\gray{\satisfiesblack}}{\satisfies} \formula{\forallst{x}{\,\existsst{y}{\,\notequalto{x}{y}}}}$ \end{itemize} \end{frame}