Stabilizing nodes from an anchor

[I got this problem from Jay Misra, who had received it from Edsger Dijkstra. This particular description of the problem borrows from a description given by Michael Jackson.]

In a finite, undirected, connected graph, an integer variable v(n) is associated with each node n. One node is distinguished as the _ anchor_. An operation OP(n) is defined on nodes:

OP(_n_):
if node _n_ is the anchor, then do nothing,
else set v(_n_) to the value 1 + min{v(_m_)}, where _m_ ranges over all neighbors of _n_ that are distinct from _n_.

An infinite sequence of operations <OP(n),OP(m), …> is executed, the node arguments n, m, … for the operations being chosen arbitrarily and not necessarily fairly. Show that eventually all v(n) stabilize. That is, that after some finite prefix of the infinite sequence of operations, no further operation changes v(n) for any node n.