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