\begin{frame}[t]{Towards Proving Partial Correctness of \texttt{Fac2}}
  \begin{goal}{}\vspace{1ex}\begin{malign}
    \ruleassignment
  \end{malign}\end{goal}
  \begin{goal}{}\begin{malign}
    \ruleimplied
  \end{malign}\end{goal}
  \begin{goal}{}\begin{malign}
    \rulecomposition
  \end{malign}\end{goal}
  
  \begin{exampleblock}{}
  \medskip
  \hspace*{-.8ex}
  \scalebox{0.85}{  
  \begin{minipage}{\textwidth}
  %
  \AxiomC{\mbox{}}
  \RightLabel{$a$}
  \UnaryInfC{$\hoaretriple{\formula{\equalto{1}{1}}}
                          {\Assign{y}{1}}
                          {\formula{\equalto{y}{1}}}$}  
  \RightLabel{$i$}
  \UnaryInfC{\uncover<1->{$
              \hoaretriple{\formula{\true}}
                          {\Assign{y}{1}}
                          {\formula{\equalto{y}{1}}}$}} 
  %        
  \AxiomC{\mbox{}}
  \RightLabel{$a$}  
  \UnaryInfC{$\hoaretriple{\formula{\formula{\logand{\equalto{y}{1}}{\equalto{0}{0}}}}}
                          {\Assign{z}{0}}
                          {\formula{\logand{\equalto{y}{1}}{\equalto{z}{0}}}}$}                       
  \RightLabel{$i$}                        
  \UnaryInfC{\uncover<1->{
             $\hoaretriple{\formula{\equalto{y}{1}}}
                          {\Assign{z}{0}}
                          {\formula{\logand{\equalto{y}{1}}{\equalto{z}{0}}}}$}}                        
  \RightLabel{\uncover<1->{$c$}}
  \BinaryInfC{\uncover<1->{$
              \hoaretriple{\formula{\true}}
                          {\Assign{y}{1}; \Assign{z}{0}}
                          {\formula{\logand{\equalto{y}{1}}{\equalto{z}{0}}}}$}}
  \DisplayProof                        
  %
  \end{minipage}}  
  \end{exampleblock}
  \bigskip
\end{frame}