contraction: are agents related by the contraction pre-order?

contraction(A,B);

Notes

whenever P -a-> P' there exists Q' s.t. Q =^a=> Q' and P' C Q' and

whenever Q -a-> Q' there exists P' s.t. (P -a-> P' or P -^a-> P') and P' C Q'

(P and Q are weakly bisimilar, and P need never do more tau moves than Q)

See Milner "Contractions", RM 13, Handwritten notes, dated 23 March 1990.