\begin{frame}[fragile,t]{Proof Rules for Partial Correctness}
  \begin{goal}{}\vspace{1.5ex}
    \begin{malign}
    \ruleassignment
    \end{malign}
  \end{goal}
  \pause\bigskip

  \begin{exampleblock}{}
    For $\psi$ is $\equalto{x}{5}$ we get:\pause
    \begin{talign}
     \hoaretriple{\equalto{6}{5}}
                 {\Assign{x}{6}}
                 {\equalto{x}{5}}
    \end{talign} \pause{}             
    For $\psi'$ is $\equalto{x}{6}$ we get:
    \begin{talign}
     \hoaretriple{\equalto{6}{6}}
                 {\Assign{x}{6}}
                 {\equalto{x}{6}}
    \end{talign}  
  \end{exampleblock}
  \pause\medskip

  \begin{alertblock}{}
    The reverse form with conclusion
    \begin{talign}
     \hoaretriple{\bform}
                 {\Assign{x}{\aexp}}
                 {\substforin{\aexp}{x}{\bform}}
    \end{talign}             
    does not make sense! \pause E.g.\ for $\aform$ is $\equalto{x}{5}$ it would entail:
    \begin{talign}
    \hoaretriple{\equalto{x}{5}}
                 {\Assign{x}{6}}
                 {\equalto{6}{5}} \quad \alert{\xmark} 
    \end{talign}
  \end{alertblock}
  \vspace{10cm}
\end{frame}