signature { automatic } theory
{
n2:n1;
n1 v <R1>(n1:(n2 & !p1));
<R1>(n1:p1);
!n2 
}