Forget about the A-quantifier, and consider G(a ↔ Xa) and let's find all of its models. Variable a may be initially either true or false. If it is false, then also ¬Xa must hold, since a ↔ Xa must be true at time 0. Same for time 1, and so on and by induction, we see that in that case G¬a holds.

If "a" would be initially true, the same arguments will prove that Ga holds.

Hence, G(a ↔ Xa) implies that we either have Ga or G¬a. Conversely, Ga and also G¬a imply G(a ↔ Xa).