A seguir: Progress: the Graph Acima: Aula 17 - O Anterior: Rules
Predicate A1 bellow is an inductive invariant.
![[*]](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}](img147.gif)