begin
n1:<>(n1 v (p1 ^ !p1));
n1:((<>true v (p1 --> (p2 --> p1)) v []false) --> p1);
!(n1:<>p1) 
end