begin A[](([]!p1) v (<>p1)); n1:<><>p1 end