# Proof of completeness for cyclic graphs

Proposition (Completeness). If [[f]] [[g]] then f = g.

Proof. Let R be the bisimulation between [[f]] and [[g]]. We can regard this as a graph G:

- Nodes are pairs (N,N) R.

- Edges are pairs (E,E) R.

- Incoming edges, outgoing edges, and labellings inherited from [[f]] and [[g]] (since R is a graph relation, this is consistent).

By expressivity, let h be the term such that [[h]] G. Find normal forms for f, g and h:
Let E1...Em be the outgoing edges of [[f1]] which form the cycles in [[f]], and F1...Fn be the outgoing edges of [[h1]] which form the cycles in [[h]]. Construct a shuffle s with:

- Edges E1...Em.

- Incoming edges E1...Em.

- Outgoing edges E1...En, where Ei = Ej whenever Fi = (Ej,_).

- Labelling inherited from [[f1]].

We can then show that:
and since we have completeness for acyclic graphs, this means:
=
Then since trace is uniform wrt shuffles:
=
and so f = h. We can show g = h similarly.

Back