begin
  !([R1](P1 | !P1))
end