Common use of Lemma 4 Clause in Contracts

Lemma 4. 1 of Section 4) For all r > 0, every process p, and every correct process q, if p executes round r until the end, then q executes round r until the end. Proof (sketch): This follows from a simple induction on r. We only proof the inductive step: assume that the lemma holds for r − 1, and that p executes round r > 1 until the end; we show that every correct process executes round r until the end. From the inductive hypothesis, all cor- rect processes execute round r− 1 until the end, and so, execute W-ABroadcast(r, −) in round r. From validity of the ordering oracles, all correct processes eventually execute W-ADeliver(r, −). It also follows that since there are n − f correct processes that execute send(first, r, −) at line 12, no correct process remains blocked forever at the wait statement at line 13, and executes round r until the end, concluding the proof. Q Lemma C.2 (Lemma 4.2 of Section 4) For all r > 0, every process p that executes round r until the end, and every process q that executes round r +1 until the end, deliveredr is a prefix of deliveredr+1. Proof (sketch): Assume p executed round r until the end. Then, p received at line 13 n − f messages of the type (first, r, v), and from lines 16 and 19, allSeqp and deliveredr are prefixes of v. Since there are n − f processes that execute send(first, r, v), and f < n/3, for every process u that executes lines 14–15, we have that allSeqp and deliveredr are prefixes of estimater , where estimater is the value of estimateu right after process u executes line 14–15. Let q be a process that executes line 13 of round r + 1. Then q receives n − f messages of the type (first,r + 1, vj), where vj = estimater , and so, allSeqp and deliveredr are prefixes of