% All messages d are (once they have been read through action r1)
% inevitably sent through action s4, if not permanently lost (via
% internal action i).
%
% Essentially this is the same property as the one in
% "read_then_eventually_send.mcf", but it adds a fairness assumption
% (a message is not lost infinitely often).

nu X.
(
[true]X

&&

forall d:D.
             ([r1(d)]( nu Y. mu Z. ([!(exists m: Nat . val(m < 2*n) && c3(d,m)) && !i]Z && [i]([!(exists m: Nat . val( m < 2*n) && c3(d,m))]false => Y) ) ))
)
