begin [](n1 <--> [](n2 <--> [](n3 <--> []n4))); <>[]<>(p1 <--> p2); [](p3 -> n1:!p1); (n1:n2) end