%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{Extra Slide: Algorithm}
\vspace{0.3in}
\Blue{
\begin{center}
	\begin{figure*}
	\centerline{\epsfbox{Figures/fig8-disj-algo.eps}}
	\end{figure*}
\end{center}
\begin{tabbing}
xxxxxx\= \kill
repeat until done\\
\> find a \Red{crossable} pair of true and false intervals\\
\> if none exists then exit(``no controlling computation exists'')\\
\> advance to the least consistent global state that crosses the false interval\\
\> save the true interval in the chain
\end{tabbing}
}
%-------------------------------------------------------------------------------
\movedUpBody{-0.75in}{Extra Slide: Proof Hint - 1}
\vspace{0.3in}
\Blue{
no crossable pair exists $\implies$ no controlling computation exists
\vspace{0.3in}
\begin{center}
	\begin{figure*}
	\centerline{\epsfbox{Figures/fig9-proof-1.eps}}
	\end{figure*}
\end{center}
}
%-------------------------------------------------------------------------------

\movedUpBody{-0.75in}{Extra Slide: Proof Hint - 2}
\vspace{0.3in}
\Blue{
the chain of true intervals does not create any cycles
\vspace{0.3in}
\begin{center}
	\begin{figure*}
	\centerline{\epsfbox{Figures/fig10-proof-2.eps}}
	\end{figure*}
\end{center}
}
%-------------------------------------------------------------------------------
