## 7 Proof of Correctness
: _Starting in an arbitrary system configuration, after \(n\) rounds all abnormal trees in the network vanish and all the processes not in the normal tree enter state \(Cc\). After a process enters state \(Cc\) or is in state \(Cc\) at system start, the process remains in state \(Cc\) until joining the normal tree._  
**Lemma 5** (Premature Feedback Safety). : _Upon starting in an arbitrary system configuration, premature feedback safety is never violated by the proposed algorithm._  
Proof. : Let \(i\) be a non-completed neighbor of a completed process and \(j\) is a non-completed neighbor of process \(i\) in an arbitrary initial state. We are to show that process \(i\) cannot receive the broadcast from process \(j\). Since process \(i\) is a non-completed process with a completed neighbor, it is a boundary process contained in a normal broadcast tree. Also, notice that since process \(i\) is contained in a normal broadcast tree, it is locked. Since locked process \(i\) may be unlocked only when the parent of \(i\) in legitimate tree \(T\) changes its state to \(C\) or broadcast is completed in the sub-tree rooted at the parent process of \(i\). Since process \(i\) is in a normal broadcast tree and the parent of process \(i\) does not change and enter state \(C\) until the broadcast is completed in the subtree rooted at the parent process of \(i\) in a normal broadcast tree, process \(i\) cannot receive the broadcast from process \(j\). Hence, the proof follows. **Lemma 6** (Liveness). : _After the system starts in an arbitrary initial system configuration, in any system configuration, if process \(i\) is a boundary process in state \(Cc\) in a normal tree \(T\) just before the secondary wave is initiated by process \(i\), then upon completion of the secondary wave, process \(i\) and all its ancestors enter state \(Bc\) and all neighbors of \(i\) not in \(T\) enter state \(Cc\) and assume a leaf in \(T\) as a parent and are locked in at most \(2D+1+n\) rounds if the secondary wave is initiated in the first \(n\) rounds after the system start and \(2D+1\) rounds if the secondary wave is initiated after the first \(n\) rounds after the system start._  
**Proof. ** Observe that when process \(i\) joins normal tree \(T\), it is in state \(Cc\), locked, and its parent is in state \(Bc\). Then, process \(i\) starts the secondary wave by entering state \(Cf\) and collects neighborhood information by assigning all its neighbors to \(NeighInfo_{i}\). Subsequently, when all the children of \(i\)'s parent \(j\) enter state \(Cf\), then \(j\) enters state \(Bf\) and (includes its id and level \(l\) to \(NeighInfo_{j}\)). Phase \(Bf\) moves in a bottom-up manner towards the root as each process \(j\) enters state \(Bf\) and gathers the neighborhood information coming from the leaves and the parents of the leaves in \(T\) to \(NeighInfo_{j}\) from its children. It is easy to see that starting from the leaves, \(Cf\) phase takes \(D-1\) rounds to reach children of root \(r\). When all the children of the root enter state \(Bf\) (or \(Cf\) if the child is a leaf in \(T\)), then root \(r\) gathers the neighborhood information from its children. Upon copying the neighborhood information, root \(r\) knows all the leaves, all the neighbors of the leaves, and all the neighbors of the parents of the leaves. Using the collected information, root \(r\) removes the leaves and the neighbors of the parents of the leaves from the neighbors of the leaves to obtain the neighbors of the leaves not in \(T\). Subsequently, for each neighbor of the leaves not in \(T\), root \(r\) designates a leaf in \(T\) as a parent, stores the designation for the neighbor of the leaves not in \(T\) in \(CorrInfo_{r}\) and enters state \(Bb\) in one round. Then root \(r\) broadcasts the information stored in \(CorrInfo_{r}\) in \(b\)-phase moves in a top-down manner. In phase \(Bb\), upon discovering that \(i\)'s parent is in state \(Bb\), \(i\) copies the information stored in \(CorrInfo_{i}\) to \(CorrInfo_{i}\) and enters state \(Bb\).