% The protocol does not duplicate messages
% Obtained from: "Tools for parameterized Boolean Equation Systems",
% S. Janssen, MSc. thesis
[true*] forall d:D. [r1(d).(!r1(d) && !s4(d))*.s4(d).(!r1(d))*.s4(d)]false
