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

  \begin{block}{}
    $\derivablein{\firebrick{AR}}{\aform}$ is valid $\iff$
    \begin{itemize}
      \item []
        there is a natural deduction proof of $\aform$ where\\
        \alert{standard laws of arithmetic} may be used as premises
    \end{itemize}
  \end{block}
  \pause\bigskip
      
  When \emph{applied top-down}, this rule \emph{allows} to:
  \begin{itemize}
    \item \emph{strengthen} the precondition (assume more than we need)
    \item \emph{weaken} the postcondition (conclude less than we could)   
  \end{itemize}
\end{frame}