A gradual valuation with tuples for general graphs

Using the definitions given in Sections 3.2.1 and 3.2.2, the gradual valuation with tuples given by Definition 10 is applicable for arbitrary graphs after the rewriting process.

Let us apply the rewriting process and Definition 10 on different examples.

Example 7 - Unattacked cycle (continuation)
Consider the following graph:

The rewriting of this graph has been given in Section 3.2.2.

Definition 10 produces:

Applying Definition 10 for different arguments in the rewritten graph produces the following equalities:

• for each
• for each
• for each n and

So, using the above equalities in the formulae giving and , we define two sequences of tuples : a sequence (, ) of infinite tuples of even integers, and a sequence (, ) of infinite tuples of odd integers

From the results stated in Property 7, it is easy to prove that and for each , .

Similarly, and for each , .

These equations enable to prove that :

For each even integer , belongs to each tuple .

For each odd integer , belongs to each tuple , .

The proof is done by induction on p.

So, .

Then, .

Note that all the above results can be readily extended to an unattacked cycle of length n, .

Property 8 (Properties of unattacked cycles)
For each unattacked cycle, for each argument of the cycle, .

Example 8 - Attacked cycle (continuation)Consider the following graph:

The rewriting of this graph has been given in Section 3.2.2.

Definition 10 produces:

and also

for each

As done in the treatment of Example 7, the formulae giving and can be rewritten in order to bring to light some interesting sequences of tuples.

Then, it is easy to prove that and for each , .

Similarly, and for each , .

The first equation enables to prove that is the empty tuple21.

The second equation has already been solved and produces .

So, . For , we can reason as for , and we have . Then, , .

Notation: in order to simplify the writing, we will not repeat the values inside the tuples (we will just indicate under each value how many times it appears). For example:

will be denoted by

In appendix B, we introduce an algorithm for computing these tupled values. It uses a process of value propagation and is parameterised by a maximum number of runs through a cycle''. This number will be used in order to stop the propagation mechanism and to obtain finite (thus incomplete) tupled values.