A few more minor fixes in proof 2.2.2

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index 3d71c11b136fc676bb96cafe2c35bfcc1ee4c3bd..876935ac6921628bfa2ec20c8482bdf3bb56aa88 100644 (file)
--- 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 \r
 $\mathsf{\mathscr{S}}$ of clients comprising a connected component of an \r
 undirected graph, where two clients are connected by an edge if they both \r
-received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t > n}$.\r
+received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t < s_n}$.\r
+%TODO: Check with Thomas whether this is $\mathsf{s_t > s_n}$ or it should be\r
+%$\mathsf{s_t < s_n}$\r
 \end{defn}\r
 \r
 \subsubsection{Lemmas and Proofs}\r
@@ -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\r
 those which not all clients have seen. Hence, for every $\mathsf{s}$, $\mathsf{1 \leq s < |X|}$, \r
 the collision winner that has collided with $\mathsf{s}$-th element of $\mathsf{X}$ \r
-will be recorded in $\mathsf{CR}$. Since all the $\mathsf{cr}$ entries before \r
-$\mathsf{p}$ will also be seen when $\mathsf{u}$ is received, ${l_1}$ will be recorded \r
-in $\mathsf{CR_C}$ as the winner in the collision against ${r_1}$. When $\mathsf{C}$ \r
-receives $\mathsf{u}$, $\mathsf{C}$ will throw an error from the match \r
-$\mathsf{\tuple{s_q+1, id_K}}$ in $\mathsf{CR_C}$.\r
+will be recorded appropriately. Since all the $\mathsf{cr}$ entries that record \r
+the results of the collisions before $\mathsf{p}$ will also be seen when $\mathsf{u}$ \r
+is received, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the \r
+collision against ${r_1}$. When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$ \r
+has seen the $\mathsf{cr}$ entry that records the collision, it will already throw \r
+an error from the mismatch of $\mathsf{\tuple{s_q+1, id_J}}$ with \r
+$\mathsf{\tuple{s_q+1, id_K}}$ in the corresponding $\mathsf{cr}$ entry.\r
 \item Case 2.2.2.1: \r
 \end{itemize}\r
 \end{itemize}\r