There are some lines with a bit sloppiness in the argumentation that refer to the reachable states only and not to the real product structure, and some refer to the original structure and not the the product.
The first example solution is fine up to the following line
Kx |= p -> !a | AFG!(p&b)
From here, I suggest a slighly different argumentation. The above is equivalent to the following two statements
Kx |= p -> !a | !EGF(p&b)
Kx |= p -> !a | !nu y. <>(mu x.(y & (p&b) | <>x))
That can be easily checked with our tools, and we get
〖 nu y. <> mu x. (y & p & b | <> x)〗 = {SQ0;SQ1;SQ3}
〖!nu y. <> mu x. (y & p & b | <> x)〗 = {SQ2}
〖!a〗 = {SQ0}
〖!a | !nu y...〗 = {SQ0,SQ2}
〖p〗 = {SQ2,SQ3}
〖p -> !a | !nu y.〗 = {SQ0,SQ1,SQ2}
Hence, the intitial states {SQ3} are not contained, so that the product structure does not satisfy the above formula, and therefore K does not satisfy A(ψ ∨ φ) which is equivalent to this.
Now, consider the alternative solution that starts as follows
K |= A(ψ ∨ φ)
⇔ K |= A(¬a ∨ φ)
⇔ K |= A(a → φ)
⇔ K |= A(¬a ∨ φ)
⇔ K |= ¬a ∨ Aφ
At the next point, it is argued that the above should be equivalent to K |= Aφ. However, in structure K, we have two initial states s2 and s3 where s3 satisfies "a" and s2 does not. So, we should better continue as follows:
⇔ K,s3 |= ¬a ∨ Aφ & K,s2 |= ¬a ∨ Aφ
⇔ K,s3 |= ¬a ∨ Aφ
⇔ K,s3 |= Aφ
⇔ K,s3 |= ¬E¬φ
⇔ K,s3 |= ¬EA∃(Q,φI,φR,φF)
⇔ K×,SQ3 |= ¬EφF
⇔ K×,SQ3 |= ¬EGF(p ∧ b)
⇔ K×,SQ3 |= ¬nu y. <>(mu x.(y & (p&b) | <>x))
As before, we have
〖 nu y. <> mu x. (y & p & b | <> x)〗 = {SQ0;SQ1;SQ3}
〖!nu y. <> mu x. (y & p & b | <> x)〗 = {SQ2}
Hence, the intitial states {SQ3} are not contained, so that the product structure does not satisfy the above formula in SQ3, and therefore K does not satisfy A(ψ ∨ φ) which is equivalent to this.
As you wrote above, there is a path from the initial SQ3 that satisfies GF(p ∧ b), and since that is the only path, we have A¬GF(p ∧ b) which means ¬EGF(p ∧ b).
