[CST-2] Bisimulation

[Peter Taylor]

> If we define p phi(R) q to hold when the strong bisimulation conditions
> hold then then phi(R) is a bisimulation (by definition).

I'm not convinced that phi(R) is a bisimulation, but I've found a simple
proof.

Let the predicate BI(p, R, q) be the strong bisimulation conditions (FORALL
a, p' etc.).

Then R strong bisim <==> (p R q ==> BI(p, R, q)) by defn

p phi(R) q <==> BI(p, R, q) by defn

Suppose R \subseteq phi(R). Then p R q ==> p phi(R) q ==> BI(p, R, q) so R
strong bisim.

Now suppose instead that R strong bisim.  Then p R q ==> BI(p, R, q) ==> p
phi(R) q.  Thus R \subseteq phi(R).

Peter
=====
Peter Taylor
pjt33@cam.ac.uk