\begin{frame}[fragile,t]{Proof Rules for Partial Correctness}
  \begin{goal}{}\vspace{1.5ex}
    \begin{malign}
    \ruleassignment
    \end{malign}
  \end{goal}
  \pause\smallskip
  
  \begin{itemize}
    \item
      is best applied backwards
  \pause
    \item
      \alert{note} the necessity of \alert{capture avoiding} in substitution!
  \end{itemize}
  \pause

  \begin{goal}{}
    \emph{Hint} for understanding:
    if $\aform$ holds when replacing $x$ by $E$, then 
    after the assignment $x = E$, the formula $\aform$ holds.
  \end{goal}

  
  \begin{itemize}\setlength{\itemsep}{0ex}
  \pause
    \item $\hoaretriple{\equalto{2}{y}}{\Assign{x}{2}}{\equalto{x}{y}}$
  \pause
    \item $\hoaretriple{\equalto{2}{4}}{\Assign{x}{2}}{\equalto{x}{4}}$
  \pause
    \item $\hoaretriple{{2}\mathrel{\dm{>}}{2}}{\Assign{x}{2}}{2\mathrel{\dm{>}}x}$
  \pause
    \item $\hoaretriple{\equalto{x+1}{y}}{\Assign{x}{x+1}}{\equalto{x}{y}}$
  \pause
    \item $\hoaretriple{\equalto{x + 1 + 5}{y}}{\Assign{x}{x+1}}{\equalto{x+5}{y}}$
  \pause
    \item $\hoaretriple{x + 1 > 0 \logandinf y > 0}{\Assign{x}{x+1}}{x > 0 \logandinf y > 0}$
  \end{itemize}
  \vspace{10cm}
\end{frame}