We have a robot moving around on an $(x,y)$-grid, with $x$ and $y$ both being non-negative integers. I.e., the robot is moving in the space $\mathbb{N} \times \mathbb{N} = \mathbb{N}^2$.
The robot terminates when reaching $(0,0)$. If the robot is not at $(0,0)$, it must make a move with one of two transition rules. It can freely choose which rule to use (maybe at random), provided that applying the rule does not cause the robot to leave the grid:
1) Move West: $(x,y) \rightarrow (x-1, y)$, for $x > 0$, or
2) Move South, with a potential jump to the East: $(x,y) \rightarrow (z, y-1)$, with $z$ being an arbitrary jump, $z\ge x$.
We want to prove that the robot will terminate, i.e. that it will reach $(0,0)$.
Playing around with it on a small grid, it quickly becomes clear intuitively that it will eventually reach $(0,0)$ and terminate. However the number of steps to termination is not deterministic, as the robot can make arbitrarily large jumps to the East (as long as $y>0$), thereby delaying termination by an arbitrarily high number of steps.
To actually prove, mathematically, that it will terminate, the robot can be modelled as a state machine.
We want to define a derived variable, $v$, mapping the robot's states $(x,y)$ into elements in a well-ordered set, $\mathbb{S}$. I.e. we want to define $v: \mathbb{N}^2 \rightarrow \mathbb{S}$.
If we can map the states into numbers in a well-ordered set, and then show that $v$ is strictly decreasing, we can then prove that the machine will terminate.
Here is the question: Any hints / suggestions for how to derive such a mapping?
Thank you very much in advance!
Best regards,
Here is another approach:
Suppose we start from $(x_0,y_0)$. Look for invariants.
Note that for all moves $(x_n,y_n) \to (x_{n+1},y_{n+1})$ we have $0 \le y_{n+1} \le y_n$.
It follows that there can be at most $y_0 $ south moves.
One proof:
$ $