@octachron’s solution is very nice, but there is an alternative (I would say dual) solution:
The only problem, that I see with the @octachon’s solution is that it gives to much power to the interface user, if x and y constructors are exposed. It could be addressed by abstracting them, as well as the representation of the state transition witness, and posting in the interface the set of valid state transitions.