signature { automatic } theory

{
 N1 : (<R1> N2);
 N2 : P1;
 N1 : [R1] !P1
}