CTL, LTL, CTL* [02.2019 9a part 5]

Question

I do not understand the 3rd step here, is it in general valid for G!a &(FGa | Fb) to be equivalent to G!a & Fb ?

Answer 1

Well, if you have G!a (i.e. globally !a) this means that neither now nor in the future a will ever hold (this is also reasoned by G!a = !Fa). For this reason FGa can also never hold thus this term effectively reduces to 0 in this combination:

G!a & (FGa | Fb) = G!a & (0 | Fb) = G!a & Fb

or if you apply the distributive rule first you get:

G!a & (FGa | Fb) = (G!a & FGa) | (G!a & Fb) = 0 | (G!a & Fb)  = G!a & Fb

So yes, these two terms are equivalent (similar to c & (!c | d) being equivalent to c & d as c and !c can never hold at the same time obviously).