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