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:

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