% If an r1 action is enabled infinitely often, then it is also
% taken infinitely often, independent of the message d
% Taken from: "Modal logics and mu-calculi: an introduction",
% by Bradfield and Stirling.
%
% This formula is not true for abp_bw, as there is no
% fairness assumption.
forall d:D . ([true*] nu X. mu Y. nu Z. ([r1(d)]X && ([r1(d)]false || [!r1(d)]Y) && [!r1(d)]Z))
