\begin{frame}{Proving Partial Correctness of \texttt{Fac2}}
  \hspace*{-3.5ex}
  \begin{minipage}{\textwidth}
  \begin{talign}
    \scalebox{.78}{
    \infer[c]{
      \hoaretriple{\formula{\true}}
                  {\underbrace{
                     \Assign{y}{1}; \Assign{z}{0}; 
                     \WhileDo{(\boolnotequalto{z}{x})}{\Assign{z}{z+1};\Assign{y}{y*z}}
                   }_{\normalsize \forestgreen{\texttt{Fac2}}}}
                  {\formula{\equalto{y}{\fac{x}}}}
    }{
      \cdots
      &
      \infer[i]{
        \hoaretriple{\formula{\logand{\equalto{y}{1}}{\equalto{z}{0}}}}
                    {\WhileDo{(\boolnotequalto{z}{x})}{\Assign{z}{z+1};\Assign{y}{y*z}}}
                    {\formula{y=\fac{x}}}
      }{
        \infer[w]{
          \hoaretriple{\formula{\alert{\equalto{y}{\fac{z}}}}}
                      {\WhileDo{(\boolnotequalto{z}{x})}{\Assign{z}{z+1};\Assign{y}{y*z}}}
                      {\formula{\logand{\alert{\equalto{y}{\fac{z}}}}{\equalto{z}{x}}}}
        }{
          \infer[c]{
            \hoaretriple{\formula{\logand{\alert{\equalto{y}{\fac{z}}}}{\notequalto{z}{x}}}}
                        {\Assign{z}{z+1};\Assign{y}{y*z}}
                        {\formula{\alert{\equalto{y}{\fac{z}}}}}
          }{
            \infer[i]{
              \hoaretriple{\formula{\logand{\equalto{y}{\fac{z}}}{\notequalto{z}{x}}}}
                          {\Assign{z}{z+1}}
                          {\formula{y\cdot z = \fac{z}}}
            }{
              \infer[a]{
                \hoaretriple{\formula{y\cdot(z+1) = \fac{(z + 1)}}}
                         {\Assign{z}{z+1}}
                         {\formula{y\cdot z = \fac{z}}}
              }{
              }
            }
            &
            \infer[a]{
              \hoaretriple{\formula{y\cdot z = \fac{z}}}
                          {\Assign{y}{y*z}}
                          {\formula{\equalto{y}{\fac{z}}}}
            }{}
          }
        }
      }
    }
    }
  \end{talign}
  \end{minipage}
  \bigskip
  
  \begin{goal}{}
    \begin{malign}
      \rulewhile[\alert]
    \end{malign}
  \end{goal}
  (loop invariant $\alert{\psi}$)
\end{frame}