77/183
\begin{frame}[t]
  \frametitle{Distribution of $\,\formula{\sforall}\,$ over $\,\formula{\slogand}\,$ and $\,\formula{\slogor}\:$?}
  
  \begin{alertblock}{}
    Does it work for $\,\formula{\slogand}\,$ and $\,\formula{\slogor}\,$? 
    \begin{itemize}\vspace*{0.45ex}\setlength{\itemsep}{0.45ex}           
      \item
        $\formula{\forallst{x}{(\logand{\unpred{LL}{x}}{\unpred{C}{x}}})}
           \;\logequiv\;
         \formula{\logand{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$  $\;$ \alert{?}
      \item 
        $\formula{\forallst{x}{(\logor{\unpred{LL}{x}}{\unpred{C}{x}})}}
           \;\logequiv\;
         \formula{\logor{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$   $\;$ \alert{?}
    \end{itemize}
  \end{alertblock}
  \pause\bigskip  

  Are there counter models? 
  \pause\medskip
  
  In the first case, no, in the second case, yes!
  \pause\medskip

  \begin{block}{
    $\; \formula{\forallst{x}{\logand{(\unpred{LL}{x}}{\unpred{C}{x})}}}
        \;\logequiv\;
        \formula{\logand{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}}$
  }
    \begin{itemize}\vspace*{0.45ex}\setlength{\itemsep}{0.45ex}                           
      \item   
        For every model $\model{\amodel}$ with domain $\adomain$ it holds that:
        \begin{talign}
          \model{\amodel} \satisfies \formula{\forallst{x}{\logand{(\unpred{LL}{x}}{\unpred{C}{x})}}}
            \;\;\;\Longleftrightarrow\;\;\;
          \intin{\sunpred{LL}}{\model{\amodel}}
            =
          \intin{\sunpred{C}}{\model{\amodel}}
            = 
          \adomain
        \end{talign}                     
      \item
        The same is the case for 
          $\; \model{\amodel} \satisfies 
              \formula{\logand{\forallst{x}{\,\unpred{LL}{x}}}{\forallst{x}{\,\unpred{C}{x}}}} \;$
      \item
        Thus the two formulas hold in precisely the same models.
   \end{itemize}
  \end{block}
\end{frame}