p U q
p U (q U r)
! (p U (q U r))
[]<>p -> []<>q
<>p U []q
[]p U q
! (<><>p <-> <>p)
! ([]<>p -> []<>q)
! ([]<>p <-> []<>q)
p V (p \/ q)
(X p U X q) \/ ! X(p U q)
(X p U q) \/ ! X(p U (p /\ q))
[](p -> <>q) /\ ((X p U q) \/ ! X(p U (p /\ q)))
[](p -> <>q) /\ ((X p U X q) \/ ! X(p U q))
[](p -> <>q)
! [](p -> X(q V r))
! ([]<>p \/ <>[]q)
[](<>p /\ <>q)
<>p /\ <> ! p
(X q /\ r) V X(((s U p) V r) U (s V r))
([](q \/ []<>p) /\ [](r \/ []<> ! p)) \/ []q \/ []r
([](q \/ <>[]p) /\ [](r \/ <>[] ! p)) \/ []q \/ []r
! (([](q \/ []<>p) /\ [](r \/ []<> ! p)) \/ []q \/ []r)
! (([](q \/ <>[]p) /\ [](r \/ <>[] ! p)) \/ []q \/ []r)
[](q \/ X []p) /\ [](r \/ X [] ! p)
[](q \/ (X p /\ X ! p))
(p U q) \/ (q U p)