VRS Exam [August 25th, 2020], Problem 8b. Part 1

Question

Translate the following formula to an equivalent µ-calculus formula.

EFEGb 

According to the cheatsheet provided, I get the following answer:

EF(νx.b ∧ ♦x)
µx.(νy.♦y ∧ (νx.(b ∧ ♦x)) ∨ ♦x)

The solution provided is:

µy.(νx.♦x ∧ (νx.(b ∧ ♦x)) ∨ ♦y)

Are both of these equal and correct?

Answer 1

If you treat the inner formula as "phi := (vx.b ∧ ♦x)" then your solution reduces to:

µx.(vy.♦y ∧ phi ∨ ♦x)

while the sample solution is reduced to:

µy.(vx.♦x ∧ phi ∨ ♦y)

which are both equivalent because the only difference is that the variables x and y are switched. The important part is that the variable x in the formula phi does not depend on the variables outside of phi because the variable is rebound in phi, so instead you could also use:

"phi := (vz.b ∧ ♦z)"

instead without changing the meaning.