signature { automatic } theory

{
  !(([R1](P1 & P2)) -> (([R1]P1) & ([R1]P2)))
}