57/155
\begin{frame}[t]{Interpreting Formulas with Equality}
  \examplemodel
  \bigskip
    
  \begin{itemize}\setlength{\itemsep}{0.4ex} 
    \item
      $\model{\amodel} 
         \malt[1]{\gray{\satisfiesblack}}{\satisfies}
      \formula{\existsst{x}{\exists{y}{\existsst{z}{(\logand{\notequalto{x}{y}}{\logand{\notequalto{x}{z}}{\notequalto{y}{z}}})}}}}$ 
  \updatepause
    \item
      $\model{\amodel} 
         \malt[1]{\gray{\satisfiesblack}}{\satisfiesnot}
       \formula{\forallst{x}{\forallst{y}{(\logimp{\logand{\unpred{\mediumblue{P}}{x}}{\unpred{\mediumblue{P}}{y}}}{\equalto{x}{y}})}}}$ 
  \updatepause
    \item
      $\model{\amodel} 
         \malt[1]{\gray{\satisfiesblack}}{\satisfies}
       \formula{\forallst{x}{\forallst{y}{(\logimp{\logand{\binpred{\black{R}}{x}{x}}{\binpred{\black{R}}{y}{y}}}{\equalto{x}{y}})}}}$  
  \updatepause
    \item
      $\model{\amodel}
         \malt[1]{\gray{\satisfiesblack}}{\satisfiesnot}
       \formula{\forallst{x}{(\logor{\binpred{\black{R}}{x}{\const{\orange{b}}}}{\binpred{\black{R}}{x}{\const{\forestgreen{c}}}})}}$
  \updatepause
    \item
      $\model{\amodel}
         \malt[1]{\gray{\satisfiesblack}}{\satisfies}
       \formula{\forallst{x}{( \equalto{x}{\const{\orange{b}}} \logorinf \binpred{\black{R}}{x}{\const{\forestgreen{c}}} )}}$
  \updatepause
    \item
      $\model{\amodel}
         \malt[1]{\gray{\satisfiesblack}}{\satisfies}
       \formula{\existsst{x}{\forallst{y}{(\equalto{y}{x} \logorinf \binpred{\black{R}}{x}{y})}}}$
  \end{itemize}  
\end{frame}

\theme{Model Cardinality}