 In the remainder of this discussion, we let  p, q,  …  denote  pointed graphs.    We write   p ≡b q  if there is a bisimulation between p and q.   We write  p ε q  if there is a pointed graph  (G,→, g)  and some g → h in G  so that 