begin
N1;
<><>(N2 & P1);
E false v [](N1 v E true);
[](!P1 v N2:(N1 & !P1))
end