begin
   (<>(<>(<>(P1 <--> P2))));
   ([]P3);
   ([](P3 -> (P5 | P2)))
end