begin

down x1 .  []<>x1 & -(<>[]p1 -> p1)

end