\begin{frame}[fragile,t]{Proof Rules for Partial Correctness}
  \begin{goal}{}
    \begin{malign}
    \rulecomposition
    \end{malign}
  \end{goal}
  \pause\medskip
  
  Convenient to read bottom up (also for the other rules):
  \pause\medskip
  
  In order to prove 
  \begin{talign}
    \hoaretriple{\aform}{\SeqComp{\aprogcxti{1}}{\aprogcxti{2}}}{\bform}
  \end{talign}
  \pause 
  we need to find an \emph{appropriate midcondition} $\eform$, 
  and prove 
  \begin{talign}
    & 
    \hoaretriple{\aform}{\aprogcxti{1}}{\eform}
    & &  \text{ and }  & &  
    \hoaretriple{\eform}{\aprogcxti{2}}{\bform}
  \end{talign}
  \pause
  We thereby split the goal into two subgoals:
  \begin{itemize}\vspace*{0.3ex}\setlength{\itemsep}{0.3ex}
    \item 
      execution of $\aprogcxti{1}$ 
      in a state satisfying $\aform$,\\
      we get to a state satisfying $\eform$
    \item
      execution of $\aprogcxti{2}$ 
      in a state satisfying $\eform$,\\
      we get to a state satisfying $\bform$
  \end{itemize}
  \vspace{10cm}
\end{frame}