Sequential Computation of a Spanning Tree
Proof:
TerminationThis system is noetherian because executing a rewriting step implies that (|G|N,|G|M) is decreasing for >2 .
Correctness
- If an edge is incident with N-labelled vertex then it is labelled with 0,
- The set of vertices not labelld with N is connected by 1-edges,
- The graph defined by the set of 1-labelled edges and incident vertices is without cycles,
- There is exactly one A-labelled vertex,
- The set of M-labelled vertices is a simple path from the Root to the A-labelled vertex and every edge of this path is labelled with 1,
- A F-labelled vertex has no neighbours labelled with N.