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

  The goal (conclusion) is decomposed into two subgoals:
  \begin{itemize}
  \pause\medskip
    \item if $\mb{\aboolexp}$ evaluates to true, the then-part $\aprogcxti{1}$ is executed
  \pause\medskip
    \item if $\mb{\aboolexp}$ evaluates to false, the else-part $\aprogcxti{2}$ is executed
  \end{itemize}
  \pause\medskip
  In both cases, $\bform$ has to hold after the execution.
  \vspace{10cm}
\end{frame}