begin
([R1] p1 )<--> ([R3]p1 <--> <R2>[R1]!p3);
n1: [R2]<R1>p1 <--> p2 --> p3;
false --> (false <--> n1:n3)
end