Это работает только в вашем конкретном случае, потому что p и q являются атомарными суждениями.Как правило, может быть трудно решить, какие формулы допускают распределение операторов, а какие нет (см. Samer & Veith: «О распределении спецификаций LTL, 2010»).Другой способ доказать ваше конкретное утверждение - с помощью автомата Buechi, который во всех трех случаях выглядит следующим образом (см. http://www.lsv.fr/~gastin/ltl2ba/index.php). Как правило, эквивалентность формул LTL полна PSpace, поэтому зачастую без Buechi не так легко ответить на вопросыавтоматы.
