begin
A<><>!N1;
[](P1 v N1) & []!P1
end