Along the path s0 -> s0 -> s0 ... that never leaves s0, q is always false. Therefore q r is always false along this path, so AF(q r) is false at s0, for that formula means
"along all computation paths, q r is
true eventually".
Back to Question. Next Question.
Incorrect Answer.
r is always false along this path, so AF(q