From a312472839952d4ddb1489b976e32a986e3cce99 Mon Sep 17 00:00:00 2001
From: Jeff Burdges <burdges@gnunet.org>
Date: Mon, 12 Nov 2018 01:52:34 +0100
Subject: [PATCH] Explain first sentence of
 lem:message-monotonicity-completed-estimate

---
 pdf/grandpa.tex | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/pdf/grandpa.tex b/pdf/grandpa.tex
index f2f9bc9..f05ebb5 100644
--- a/pdf/grandpa.tex
+++ b/pdf/grandpa.tex
@@ -357,12 +357,15 @@ We define $V_{r,v,t}$ be the set $V_{r,v}$ at time $t$ and similarly for $C_{r,v
 
 
 \begin{lemma} \label{lem:message-monotonicity-completed-estimate}
+Assume $3f < n-1$.
 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',t'}$ and $C_{r,v,t} \subseteq C_{r,v',t'}$, 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}
 
 \begin{proof} 
-Since $v$ sees that $r$ is completable at time $t$, both $V_{r,v,t}$ and $C_{r,v,t}$ contain votes from $n-f$ voters and so the same holds for $V_{r,v',t'}$ and $C_{r,v',t'}$. 
+Since $v$ sees that $r$ is completable at time $t$, 
+either $E_{r,v} < g(V_{r,v})$ requiring $(n+f+1)/2 > 2f + 1$ votes, or else it is impossible for $C_{r,v}$ to have a supermajority for any children of $g(V_{r,v})$, requiring $2f + 1$ votes.
+In either case, both $V_{r,v,t}$ and $C_{r,v,t}$ contain votes from $2f + 1$ voters and so the same holds for $V_{r,v',t'}$ and $C_{r,v',t'}$. 
 By Lemma \ref{lem:ghost-monotonicity} (ii), $g(V_{r,v',t'}) \geq g(V_{r,v,t})$.
 As it is impossible for $C_{r,v,t}$ to have a supermajority for any children of $g(V_{r,v,t}$, it follows from Lemma \ref{lem:impossible} (i \& ii) that it is impossible for $C_{r,v',t'})$ as well, and so $E_{r,v',t'} \leq g(V_{r,v,t})$.
 But now $E_{r,v,t}$ and $E_{r,v',t'}$ are the last blocks on $\textrm{chain}(g(V_{r,v,t}))$ for which it is possible for $C_{r,v,t}$ and $C_{r,v',t'}$ respectively to have a supermajority.