[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*.

©2019 K.R.M. Leino - Split Template by One Page Love