begin
 (@ n2 (p2 v p1) -> @n1 p3)
end