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: