From: rtrimana <rtrimana@uci.edu>
Date: Tue, 16 Aug 2016 22:38:56 +0000 (-0700)
Subject: Cleaning up proof part
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=iotcloud.git;a=commitdiff_plain;h=f86a19b02daba474e44589ef4f72f6cf365a76c1

Cleaning up proof part
---

f86a19b02daba474e44589ef4f72f6cf365a76c1
diff --cc doc/iotcloud.tex
index a0e8abe,af1b1bb..f92126a
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@@ -969,17 -951,12 +951,14 @@@ call them $\mathsf{t}$ and $\mathsf{u}
  Then $\mathsf{t}$ is in the path of $\mathsf{u}$. 
  \end{lem}
  \begin{proof}
- By contradiction, we will prove that if $\mathsf{t}$ is not in the path of 
- $\mathsf{u}$, then it is impossible for client $\mathsf{C}$ to receive both
- messages without throwing any errors. Clearly $\mathsf{C}$ will throw an error 
- if $\mathsf{s_t = s_u}$. So $\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ 
- receives $\mathsf{u}$ before $\mathsf{t}$, this will cause it to throw an 
- error, so $\mathsf{t}$ is received before $\mathsf{u}$.
- 
- Assume that $\mathsf{t}$ is not in the path of $\mathsf{u}$. Take $\mathsf{u}$ 
- to be the packet of smallest sequence number for which this occurs, and 
- $\mathsf{t}$ be the packet with greatest sequence number for this $\mathsf{u}$. 
- We will prove that an error occurs upon receipt of $\mathsf{u}$.
 -Assume otherwise. Then there are some pairs $\mathsf{(t,u)}$ that violate this lemma. Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized and $\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$.
++Assume otherwise. Then there are some pairs $\mathsf{(t,u)}$ that violate this lemma. 
++Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized and 
++$\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$.
+ 
+ Clearly $\mathsf{C}$ will throw an error if $\mathsf{s_t = s_u}$. So 
+ $\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ receives $\mathsf{u}$ before 
+ $\mathsf{t}$, this will cause it to throw an error, so $\mathsf{t}$ is received 
+ before $\mathsf{u}$. We will prove that an error occurs upon receipt of $\mathsf{u}$.
  
  Let $\mathsf{r_1}$ be the earliest member of the path of $\mathsf{t}$ that is 
  not in the path of $\mathsf{u}$, and $\mathsf{q}$ be its parent. Message