- - - - CENAPAD-MGCO

A seguir: Theorem 1: Initial Conditions Acima: O Algoritmo de Naimi-Trehel Anterior: Progress: the Graph

Theorem 1

The root node:

Let root be a state predicate such that root(i) = TRUE iff $\not\exists$no other node j such that i j.

THEOREM 1

A2 There is always one and only one root node, i.e., a node i such that root(i) = TRUE;

A3 The relation always define one and only one acyclic path from any non-root node to the root.

We must add A4 and A5 bellow in order to get an inductive invariant:

A4 (HasToken[i] $\vee$ $\in$ IN[i]) $\Leftrightarrow$ root(i)

A5 For any non-root node i, there is one and just one node j such that i j, and one and just one condition among ${\cal D} 1$, ..., ${\cal D} 6$ holds between i and j.