All of these transformations are just tautologies of temporal logic and independent of fairness.
Concerning strong fairness: I'll write F for ENABLED <<A>>_v and G for <<A>>_v.
(1) => (3):
(<>F => <>G)
=> <>F => <>G by the temporal logic rule (A => B) => (A => B)
=> <>F => <>G since A <=> A
(3) => (1): I'll reason semantically because it looks simpler.
Assume that a behavior sigma satisfies (3), i.e. <>F => <>G.
We need to show that sigma also satisfies (<>F => <>G).
So assume that there is some suffix tau of sigma for which <>F is true, we need to show that tau satisfies <>G.
Since <>F is true for tau, it is also true (a fortiori) for sigma, and by (3) we obtain that <>G is true for sigma.
Therefore <>G is true for tau.
The equivalence of (2) and (3) is simply a consequence of the equivalence of F => G and ~F \/ G, plus of pushing negation across temporal operators (~F <=> <>~F, ~<>F <=> ~F).
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/BF7136CB-531A-4117-991C-4D09C3F13E15%40gmail.com.