begin
n1:[](n2 <--> n3 v n5);
[](n1: (n2 <--> p1));
[][]<>(p1 <--> []p3) <--> <><>p4;
<><><>(p2 v n2:p3) <--> (<>[]p3 v <>[]p2)   
end