\begin{block}{Proof Stats - summary}
\begin{tabular}{|l|r|r|r|r|}
\hline
                          & \# Rule Apps & \# Interactive & LoSpec & LoC \\ \hline
total                     & 2.966.522    & 28.291 (0.95\%)& 526    & 536
\\ \hline
w/o \lstinline|mergeLo|   & 1.510.604    &  8.087 (0.54\%)& 460    & 442
\\ \hline
\only<1>{
\lstinline|mergeLo|       & 1.455.918    & 20.204\ \ \ \ \ \ \ \ \ \ \ \   &  66    &  94
\\ \hline
\lstinline|mergeHi|       &   460.409    &  3.312\ \ \ \ \ \ \ \ \ \ \ \ &  62    &  98
\\ \hline
\lstinline|mergeCollapse| &   348.774    &  1.849\ \ \ \ \ \ \ \ \ \ \ \          &  48    &  14
\\ \hline
\lstinline|pushRun|       &    42.142    &    129\ \ \ \ \ \ \ \ \ \ \ \ &  18    &   5
\\ \hline
}
\end{tabular}
Verification effort: $\approx$ 3 man-months
\end{block}