A seguir: Progress: the Graph Acima: O Algoritmo de Naimi-Trehel Anterior: Rules
Predicate A1 bellow is an inductive invariant.
-
-
-
-
CENAPAD-MGCO
A seguir: Progress: the Graph
Acima: O Algoritmo de Naimi-Trehel
Anterior: Rules
![[*]](http://www.dcc.ufmg.br/latex2html/icons/foot_motif.gif){kind=icon}
.
![\begin{displaymath}
A1 \equiv \left\{
\begin{array}
{l}
\forall i, eating[i] \L...
...all j, \neg HasToken[j]
\end{array} \right.
\end{array}\right.\end{displaymath}](img165.gif)