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