begin
A (p1 ^ <>!p1)
end