\begin{frame}[fragile,t]{Proof Rules for Partial Correctness}
  \vspace*{-1ex}
  \begin{goal}{}
    \begin{tgather}
      \rulecomposition \\[2ex]
      \ruleassignment \\[2ex]
      \ruleif \\[2ex]
      \rulewhile \\[2ex]
      \ruleimplied
    \end{tgather}
  \end{goal}
\end{frame}