# Proof of cancellation of nodes

Proposition (Completeness for shuffles). If [[s1]] [[s2]] then s1 = s2.

Proposition (Cancellation of nodes). For any:

we can find h such that:
=

Proof. First, show a result about bisimulation on graphs; if:
then either:
or we can find h such that:
We now proceed by induction on f, which (by normalization) we can assume is in normal form. We have three cases:

- If f is:
  then we have a contradiction, since f is bisimilar to a graph with a node connected to an outgoing edge.

- If f is:
  then:
  then find permutation q such that:
  =
  so we have:
  By induction, we can find h1 such that:
  =
  so:
  = = = = =
  and:
- If f is:
  then by the above result about bisimulation either:

  - we have:
    and we are finished,

  - or we can find g1 such that:
    so by induction we can find h1 such that:
    =
    Then we have two cases depending on the relative positions of c and d, but the proofs are identical:
    = = =
    and:

Back