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}