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.