\begin{frame}{ But: \, $\formula{\forallst{x}{(\logor{\unpred{LL}{x}}{\unpred{C}{x}})}} \;\lognotequiv\; \formula{\logor{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$ } \uncover<2->{% \begin{exampleblock}{} Define $\model{\amodel}$ as follows: % \begin{center} $ \begin{aligned} \text{domain } \model{\adomain} & = \{1,2\} & & & \intin{\sunpred{LL}}{\model{\amodel}} & = \setexp{1} & & & \intin{\sunpred{C}}{\model{\amodel}} & = \setexp{2} \end{aligned} $ \end{center} \end{exampleblock} } \uncover<3->{Then:} \begin{itemize}\vspace*{0.3ex}\setlength{\itemsep}{0.3ex} \item<3-> $\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{(\logor{\unpred{LL}{x}}{\unpred{C}{x}})}}$, because: \begin{itemize}\vspace*{0.2ex}\setlength{\itemsep}{0.3ex} \item<4-> $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto 1]} \formula{\unpred{LL}{\freevar{x}}}$ and thus $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto 1]} \formula{\logor{\unpred{LL}{\freevar{x}}}{\unpred{C}{\freevar{x}}}}$ % $\M \mw_{[x\mapsto 1]} Gx$ en dus $\M \mw_{[x\mapsto 1]} Gx \of Dx$ \item<5-> $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto 2]} \formula{\unpred{C}{\freevar{x}}}$ and thus $\model{\amodel} \satisfieslookup{\saluf[\freevar{x}\mapsto 2]} \formula{\logor{\unpred{LL}{\freevar{x}}}{\unpred{C}{\freevar{x}}}}$ % $\M \mw_{[x\mapsto 2]} Dx$ en dus $\M \mw_{[x\mapsto 2]} Gx \of Dx$ \item<6-> Hence: $\model{\amodel} \satisfieslookup{\saluf} \formula{\forallst{x}{(\logor{\unpred{LL}{x}}{\unpred{C}{x}})}}$ %Conclusie: $\M \mw \alle x (Gx \of Dx)$ \end{itemize} \vspace*{0.5ex} \item<7-> But $\model{\amodel} \satisfiesnotlookup{\saluf} \formula{\logor{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$, because: \begin{itemize}\vspace*{0.2ex}\setlength{\itemsep}{0.3ex} \item<8-> $\model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto 2]} \formula{\,\unpred{LL}{\freevar{x}}}$ % $\M \not\mw_{[x\mapsto 2]} Gx$ en dus and thus $\model{\amodel} \satisfiesnotlookup{\saluf} \formula{\forallst{x}{\,\unpred{LL}{x}}}$ % $\M \not\mw \alle x Gx$ \item<9-> $\model{\amodel} \satisfiesnotlookup{\saluf[\freevar{x}\mapsto 1]} \formula{\unpred{C}{\freevar{x}}} $ and thus $\model{\amodel} \satisfiesnotlookup{\saluf} \formula{\forallst{x}{\,\unpred{C}{x}}}$ % $\M \not\mw_{[x\mapsto 1]} Dx$ en dus % $\M \not\mw \alle x Dx$ \end{itemize} \end{itemize} \smallskip \uncover<10->{ \begin{block}{Follow-up question:} What about distribution of $\,\formula{\exists}\,$ over $\,\formula{\slogand}\,$ and $\,\formula{\slogor}\,$?} % Hoe zit het met de distributie van $\,\eris\,$ over $\,\en\,$ en $\of\;$? \end{block} \end{frame}