\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}