CTL to mu calculus

Question

1. AF[a & Xa] = mu y. (a | []y) & [](a | y)

 From slides we know that, #1 is correct but in solution of February 2017, 8b it is written as following:

AF[a & Xa] = mu y. (a | []y) & (!a | [](a | y))

Please confirm which one is correct.

https://es.cs.uni-kl.de/teaching/vrs/exams/2017.02.15.vrs/2017.02.15.vrs.exam.pdf

Answer 1

I think that both are correct.

And I can justify this claim also: Just consider the two body formulas (a | []y) & [](a | y) and (a | []y) & (!a | [](a | y)) and make a case distinction to prove (a | []y) & [](a | y) = (a | []y) & (!a | [](a | y)):

1. a=0: then, we get ([]y) & [](y) = ([]y) which is true
2. a=1: then, we get (1) & [](1) = (1) & ([](1)) which is also true

So, the fixpoints are the same.