\begin{frame}{\scalebox{.8}{$\derivespar \hoaretriple{\formula{\aform}}
                                                     {\WhileDo{\booltrue}{\Assign{x}{x - 1}}}
                                                     {\formula{\bform}}$}}

  \hspace*{-2.5ex}
  \scalebox{0.85}{  
  \begin{minipage}{\textwidth}
    \begin{talign}
      \infer[\textsf{\small i}]{
        \hoaretriple{\phi}
                    {\WhileDo{\booltrue}{\Assign{x}{x - 1}}}
                    {\psi}
      }{
        \derivablein{\firebrick{AR}}{\formula{\logimp{\phi}{\true}}}
        &
        \infer[\textsf{\small w}]{
          \hoaretriple{\formula{\true}}
                      {\WhileDo{\booltrue}{\Assign{x}{x - 1}}}
                      {\formula{\logand{\true}{\lognot{\true}}}}
        }{
          \infer[\textsf{\small i}]{
            \hoaretriple{\formula{\logand{\true}{\true}}}
                        {\Assign{x}{x - 1}}
                        {\formula{\true}}
          }{
            \derivablein{\firebrick{AR}}{\formula{\logimp{\logand{\true}{\true}}{\true}}}
            &
            \infer[\textsf{\small a}]{
              \hoaretriple{\formula{\true}}{\Assign{x}{x - 1}}{\formula{\true}}
            }{}
          }
        }
        &
        \derivablein{\firebrick{AR}}{\formula{\logimp{\logand{\true}{\lognot{\true}}}{\psi}}}
      }
    \end{talign}
  \end{minipage}
  }  
  \bigskip
  
  \begin{goal}{}\begin{malign}
    \ruleimplied
  \end{malign}\end{goal}
\end{frame}