From 5d6ebdec23c34f18c9b2a3d290464e8c05d5a218 Mon Sep 17 00:00:00 2001 From: Jeff Burdges Date: Sun, 11 Nov 2018 10:32:48 +0100 Subject: [PATCH] t \leq l' I think formally we need not state this since the vote set increasing requires it, but it seemingly costs nothing and improves intuition. --- pdf/grandpa.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pdf/grandpa.tex b/pdf/grandpa.tex index ab1b9db..776d58f 100644 --- a/pdf/grandpa.tex +++ b/pdf/grandpa.tex @@ -357,7 +357,7 @@ Let's define $V_{r,v,t}$ be the set $V_{r,v}$ at time $t$ and similarly for $C_{ \begin{lemma} \label{lem:message-monotonicity-completed-estimate} -Let $v,v'$ be (possibly identical) honest participants, $t,t'$ be times and $r$ be a round. +Let $v,v'$ be (possibly identical) honest participants, $t,t'$ be times with $t \leq t'$, and $r$ be a round. Then if $V_{r,v,t} \subseteq V_{r,v',r'}$ and $C_{r,v,t} \subseteq C_{r,v',r'}$, all these sets are tolerant, and $v$ sees that $r$ is completable at time $t$, then $E_{r,v,t} \leq E_{r,v',t'}$ and $v'$ sees that $r$ is completable at time $t'$. \end{lemma}