begin

<>p1;
<>(p1 & <>p1);
[] (p1 & (<>p1) & (<>(<>-p1 & []p2)));
[]-p2;
(p1 <--> p3);
[](p1 <--> p3);
(p11 v p12 v p13 v p14 v p15);
(-p11 v -p12 v -p13);
[][][](p11 <--> p12)

end