Correct Answer.
To show that the CTL formula EF p 
EF q,
written in detail as (EF p) (EF q), is
equivalent to the CTL formula EF(p q),
we need to show two implications:
- Let s be any state in any model such that
(EF p) (EF q) holds in s.
Since this is a disjunction, we infer that
at least one of the two formula EF p and EF q holds at state s.
- Case 1: Assume that EF p holds at state s.
Then there exists a computation path Pi, beginning in s, such that
Pi has a state t which satisfies p. By the semantics of disjunction,
we infer that that state t also satisfies p
q. Since t is on the path Pi, we obtain that s satisfies
EF(p q).
- Case 2: Assume that EF q holds at state s.
Then there exists a computation path Pi, beginning in s, such that
Pi has a state t which satisfies q. By the semantics of disjunction,
we infer that that state t also satisfies p
q. Since t is on the path Pi, we obtain that s satisfies
EF(p q).
In any case, we infer that state s satisfies EF(p q).
- Let s be any state in any model such that
EF (p q) holds in s.
Since this an "EF" formula, we infer that there has to exist a
computation path Pi', beginning in s, such that some state t on
Pi' satisfies p q. But then
state t satisfies at least one of p and q.
- Case 1: Assume that state t satisfies p.
Then s satisfies EF p, since t is on a path beginning in s.
By the semantics of disjunction, s also satisfies
(EF p) (EF q).
- Case 1: Assume that state t satisfies q.
Then s satisfies EF q, since t is on a path beginning in s.
By the semantics of disjunction, s also satisfies
(EF p) (EF q).
In any case, we infer that state t satisfies (EF p) (EF q).
This shows that EF (p q) and
(EF p) (EF q) are equivalent.
Back to Question.
Next Question.