\begin{frame}
  \frametitle{Symmetric Frames: $q \to \all\some q$}
  
  \begin{goal}{Theorem}
    \begin{malign}
      \F \models q \to \all\some q \quad\iff\quad \text{the frame $\F$ is symmetric}
    \end{malign}
  \end{goal}
  \hint{Note that the formula characterises a property of the frame!}
  \pause
  
  \alt<-5>{
  \begin{block}{Proof ($\Leftarrow$)}
    Let $\F = \pair{W}{R}$ be symmetric. \pause
    We show that $\F \models q \to \all\some q$.
    \pause\smallskip
    
    That is: $\M \models q \to \all\some q$
    for $\M = \langle W,R,L \rangle$ with arbitrary $L$.
    \pause\smallskip
    
    Let $x \in W$ be a world. Then (we reason as before)
    \begin{itemize}  
      \item Assume that $q \not\in L(x)$, \\
            then $x \fc q \to\all\some  q$ \tabto{3.5cm} since $\;x \not\fc q$
      \item Assume that $q \in L(x) $,  \\
            then $x \fc q \to \all\some q$ 
            \tabto{3.5cm} since $\;x \fc \all\some q$
            \tabto{3.5cm} since $\;x' \fc \some q$ for all $x'$ with $R(x,x')$
            \tabto{3.5cm} since $\;x\fc q$
    \end{itemize}
    Hence $x \fc q \to \all\some q$.
  \end{block}
  }{
  \pause[6]
  \begin{block}{Proof ($\Rightarrow$)}
    Let $\F \models q \to \all\some q$. \pause
    We show that $\F$ is symmetric.
    \pause\smallskip
    
    For a contradiction, assume that $\F$ is not symmetric.
    \begin{itemize}
      \pause
      \item Let $a,b \in W$ with $R(a,b)$ and $\neg R(b,a)$.
      \pause
      \item Define $\M = \langle W,R,\lab{L} \rangle$ with labelling $\lab{L}$ given by\pause
        \begin{malign}
          \lab{L}(a) &= \{\;q\;\} &&& \lab{L}(x) = \emptyset \quad\text{for all $x \ne a$}
        \end{malign}
      \item \pause Then 
        \begin{itemize}
      \pause
          \item $a \fc q$ \tabto{2cm}since $q \in \lab{L}(a)$
      \pause
          \item $b \not\fc \some q$ \tabto{2cm}since $q$ is valid only in $a$ \;and\; $\neg R(b,a)$ 
      \pause
          \item $a \not\fc \all\some q$ \tabto{2cm}since $b \not\fc \some q$ \;and\; $R(a,b)$ 
        \end{itemize}
      \pause
      \item Hence $\F \not\models q \to \all\some q$; a contradiction.
    \end{itemize}
  \end{block}
  }
  \bigskip
  \onslide<15>{}
\end{frame}