From 77f03b38bf11ab6f0ac307e4192205f3d6ca2664 Mon Sep 17 00:00:00 2001
From: rtrimana <rtrimana@uci.edu>
Date: Mon, 8 Aug 2016 10:35:48 -0700
Subject: [PATCH] A few more minor fixes in proof 2.2.2

---
 doc/iotcloud.tex | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index 3d71c11..876935a 100644
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -898,7 +898,9 @@ $\mathsf{\{p \in P | s_p \le n\}}$ is a partial sequence of $\mathsf{T}$.
 Transitive closure set at sequence number $\mathsf{s_n}$ is a set 
 $\mathsf{\mathscr{S}}$ of clients comprising a connected component of an 
 undirected graph, where two clients are connected by an edge if they both 
-received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t > n}$.
+received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t < s_n}$.
+%TODO: Check with Thomas whether this is $\mathsf{s_t > s_n}$ or it should be
+%$\mathsf{s_t < s_n}$
 \end{defn}
 
 \subsubsection{Lemmas and Proofs}
@@ -1052,11 +1054,13 @@ $\mathsf{id}$ of the messsages that win in the collisions before $\mathsf{p}$ in
 $\mathsf{CR}$; $\mathsf{CR}$ keeps the collection of live $\mathsf{cr}$ entries, namely
 those which not all clients have seen. Hence, for every $\mathsf{s}$, $\mathsf{1 \leq s < |X|}$, 
 the collision winner that has collided with $\mathsf{s}$-th element of $\mathsf{X}$ 
-will be recorded in $\mathsf{CR}$. Since all the $\mathsf{cr}$ entries before 
-$\mathsf{p}$ will also be seen when $\mathsf{u}$ is received, ${l_1}$ will be recorded 
-in $\mathsf{CR_C}$ as the winner in the collision against ${r_1}$. When $\mathsf{C}$ 
-receives $\mathsf{u}$, $\mathsf{C}$ will throw an error from the match 
-$\mathsf{\tuple{s_q+1, id_K}}$ in $\mathsf{CR_C}$.
+will be recorded appropriately. Since all the $\mathsf{cr}$ entries that record 
+the results of the collisions before $\mathsf{p}$ will also be seen when $\mathsf{u}$ 
+is received, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the 
+collision against ${r_1}$. When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$ 
+has seen the $\mathsf{cr}$ entry that records the collision, it will already throw 
+an error from the mismatch of $\mathsf{\tuple{s_q+1, id_J}}$ with 
+$\mathsf{\tuple{s_q+1, id_K}}$ in the corresponding $\mathsf{cr}$ entry.
 \item Case 2.2.2.1: 
 \end{itemize}
 \end{itemize}
-- 
2.34.1