August 2021 - 8a - A small clarification

[a U GF(b)]

= (a SU b) V Gb

= (a SU b) V (true SU a)

I tried to write this as solution. Is it also valid solution?If not please explain.

From lecture i understand LTL has only pure path formulas state formulas: P ::= VΣ I was trying to satisfy.