188/191
\begin{frame}{\scalebox{.8}{$\derivespar \hoaretriple{\formula{\true}}
                                                     {\WhileDo{\booltrue}{\Assign{x}{x - 1}}}
                                                     {\formula{\equalto{x}{0}}}$}}

  \pause
  \bigskip
  
  \hspace*{-2.5ex}
  \scalebox{0.8}{  
  \begin{minipage}{\textwidth}
    \begin{talign}
      \uncover<2->{\infer[\uncover<3->{\textsf{\small Implied}}]{
        \hoaretriple{\formula{\true}}
                    {\WhileDo{\booltrue}{\Assign{x}{x - 1}}}
                    {\formula{\equalto{x}{0}}}
      }{
        \uncover<6->{\infer[\uncover<8->{\textsf{\small Partial-while}}]{
          \hoaretriple{\formula{\true}}
                      {\WhileDo{\booltrue}{\Assign{x}{x - 1}}}
                      {\formula{\logand{\true}{\lognot{\true}}}}
        }{
          \uncover<10->{\infer[\uncover<11->{\textsf{\small Implied}}]{
            \hoaretriple{\formula{\logand{\true}{\true}}}
                        {\Assign{x}{x - 1}}
                        {\formula{\true}}
          }{
            \uncover<13->{\derivablein{\firebrick{AR}}{\formula{\logimp{\logand{\true}{\true}}{\true}}}}
            &
            \uncover<14->{\infer[\uncover<16->{\textsf{\small Assign}}]{
              \hoaretriple{\formula{\true}}{\Assign{x}{x - 1}}{\formula{\true}}
            }{}}
          }}
        }}
        &
        \uncover<5->{\derivablein{\firebrick{AR}}{\formula{\logimp{\logand{\true}{\lognot{\true}}}{\equalto{x}{0}}}}}
      }}
    \end{talign}
  \end{minipage}
  }  
  \bigskip
  
  \uncover<7->{\small%
    \alert{Note:} We ignored trivial premises $\derivablein{\chocolate{AR}}{\formula{\logimp{\cform}{\cform}}}$  of {\sf Implied}
  } 
  \bigskip
  
  \onslide<4->{%\only<4-7,12-15>{
    \begin{goal}{}\begin{malign}
      \ruleimplied
    \end{malign}\end{goal}\vspace{-1ex}
  }%
  \onslide<9->{%\only<9-10>{
    \begin{goal}{}\begin{malign}
      \rulewhile
    \end{malign}\end{goal}\vspace{-1ex}
  }%
  \onslide<16->{%\only<16>{          
    \begin{goal}{}\vspace{1.5ex}\begin{malign}
      \ruleassignment
    \end{malign}\end{goal}
  }%
\end{frame}