Let us prove using induction.

Lemma : At all times, for all lines {j,k}:

[nv(j)>0 and nv(k)==0] "->" [there is a go() msg sent from j to k, currently in transit or at the input port of k]

Base Case: After initialization, nv(j)==0 for all j. So -> is true.

Inductive Case: Assume Lemma is true at some arbitrary snapshot. Let us prove the -> at the next snapshot, for any given line {j,k}.

For the given j and k, How can LHS of -> become true (change from false to True) as a result of the rule execution?

Case: At process j, R2 is executed by receiving a message sent from process k, and at the end, we changed from nv(j)==0 to nv(j) > 0.

notes:

R2. On receiving a go() from a neighbor j If (! visited) { visited=true; //we are officially visiting the node at this point. Send go() to each neighbor except j; I } In this problem we will assume that G is an undirected and connected graph. I A liveness property generally means that within a finite time, the system will reach a state where some specified property is true. Usually this specified property is some kind of good or desirable state. A safety property generally means that if we take a snapshot of the system state at some specified time instants, then in those snapshots, a certain specified property will be true. These specified time instants could be at the end of computation, i.e., on termination of system computation), at all time instants of those snapshots", etc. R2. On receiving a go() from a neighbor j If (! visited) { visited=true; //we are officially visiting the node at this point. Send go() to each neighbor except j; I } In this problem we will assume that G is an undirected and connected graph. I A liveness property generally means that within a finite time, the system will reach a state where some specified property is true. Usually this specified property is some kind of good or desirable state. A safety property generally means that if we take a snapshot of the system state at some specified time instants, then in those snapshots, a certain specified property will be true. These specified time instants could be at the end of computation, i.e., on termination of system computation), at all time instants of those snapshots", etc