[contravariant]

If you ask me requiring at least one blink in each step is a bit awkward as it is a global requirement as opposed to a local one.

But you can add the requirement Next(World) <> World if you really want to. Then you just get two sets:

- Next(World) <> World

- Next(World).x in (World.x, !World.x)

and

- Next(World) <> World

- Next(World).y in (World.y, !World.y)

and if you combine them you get

- Next(World) <> World

- Next(World).x in (World.x, !World.x)

- Next(World).y in (World.y, !World.y)

which seems to do what you want.

Adding global constraints seems like an easy way to shoot yourself in the foot though.