The question 9b, from 2018 Feb 14th exam, asks to translate E F X ([b SU a]).

The solution says:

(0) E F X ([b SU a])

(1) = E X F ([b SU a])

(2) = E X E F (E[b SU a])

// E[b SU a] = µx.(φinf ∧ a) ∨ b ∧ <>x

(3) = <>(µy.((E [b SU a] = µx.a ∨ b ∧ <>x) ∨ <>y))

1) I was not able to find the equivalences E F X φ = E X F φ and E X F φ = E X E F (Eφ), how are they created?

2) How is performed the translation from (2) to (3)?

Thanks!