I tried solving it as follows:
A([d U 0] ∧ F [d U b])
= A(Gd ∧ F [d U b])
= A(Gd ∧ (FGd ∨ Fb))
= A ( (Gd ∧ FGd) ∨ (Gd ∧ Fb))
= A (Gd ∨ (Gd ∧ Fb)) {s.t FGd = Gd}
Why are we avoiding (Gd ∧ Fb)?
The solution provided is as follows:
1) A([d U 0] ∧ F [d U b])
2) A(Gd ∧ F [d U b])
3) A(Gd ∧ (FGd ∨ Fb))
4) AGd
From Step 3 to Step 4, how is
Gd ∧ (FGd ∨ Fb) = Gd ?