[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:

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

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