are S1 and S2 equal?

Question

The given formulas S1 and S2 are not equivalent. Construct a Kripke structure or a path that satisfies only one of the formulas, and explain why one is satisfied, while the other one is not satisfied.

S1 = AF(¬a ∧ X¬a)

S2 = AF(¬a ∧ AX¬a) .

In the above question it's mentioned that S1 and S2 are not equal. But we know that

X=AX=AXA.

i.e S2 = AF(¬a ∧ X¬a)

isn't it contradicting itself?

Question source : https://es.cs.uni-kl.de/teaching/vrs/exams/2017.08.29.vrs/2017.08.29.vrs.solutions.pdf (8.e)

Answer 1

S1 and S2 mentioned above are not equivalent. You can find a Kripke structure that distinguishes between the two formulas in the solution of the above mentioned exam. 

Your argument "X=AX=AXA" is not correct. What is correct is "AXp = AXAp", but if there is just an X, you cannot simply add an A in front of it. AX phi is a state formula that holds on states, while X phi is a path formula that holds on paths. They cannot be equivalent.