+\begin{prop} \r
+\label{prop:seqnumb}\r
+$\mathsf{C}$ does not receive any message with a\r
+sequence number strictly between $\mathsf{s_t}$ and $\mathsf{s_u}$. \r
+\end{prop}\r
+\r
+\begin{proof} If there were such a message with sequence number smaller than \r
+$\mathsf{s_u}$, it would contradict the assumption that $\mathsf{u}$ is the \r
+message with the least sequence number that violates Lemma \ref{lem:twomessages}. \r
+\end{proof}\r
+\r
+There are two cases:\r
+\begin{itemize}\r
+\item Case 1: $\mathsf{J}$ did not send a message in $\mathsf{L}$. Then, where $\mathsf{s_{t_J}}$ \r
+is the greatest sequence number of the messages that client $\mathsf{J}$ sent in \r
+the path of message $\mathsf{t}$, $\mathsf{s_{t_J} > s_{q_J} = s_{u_J}}$.\r
+\begin{itemize}\r
+\item Case 1.1: $\mathsf{C}$ never updates its slot sequence list $\mathsf{SS}$ \r
+between receiving $\mathsf{t}$ and receiving $\mathsf{u}$; this can only happen if \r
+$\mathsf{s_t = s_u - 1}$. Since $\mathsf{t}$ is not the parent of $\mathsf{u}$, \r
+$\mathsf{hmac_p(u) \neq hmac_c(t)}$, causing $\mathsf{C}$ to throw an error.\r
+\item Case 1.2: Case 1.1 does not occur; therefore, $\mathsf{C}$ must update \r
+its slot sequence list $\mathsf{SS}$ at some point between receiving $\mathsf{t}$ \r
+and $\mathsf{u}$. \r
+The latest sequence number of $\mathsf{J}$ decreases during this time, which \r
+means it must decrease when some message is received, which means $\mathsf{C}$ \r
+throws an error in the $\mathsf{CheckLastSeqN()}$ subroutine.\r
+\end{itemize}\r
+\r
+\item Case 2: $\mathsf{J}$ sent at least one message in $\mathsf{L}$. Call the \r
+first one $\mathsf{m}$. We know that $\mathsf{s_m > s_{r_1}}$, since \r
+$\mathsf{J \neq K}$ and $\mathsf{m \neq l_1}$. Message $\mathsf{r_1}$ must be sent \r
+either before or after $\mathsf{m}$.\r
+\begin{itemize}\r
+\item Case 2.1: Client $\mathsf{J}$ sends $\mathsf{m}$, and then $\mathsf{r_1}$. \r
+Before sending $\mathsf{m}$, the greatest sequence number of a message that \r
+$\mathsf{J}$ has received, $\mathsf{{s_{last}}_J}$, must be equal to \r
+$\mathsf{s_m - 1 \ge s_{r_1}}$. Since $\mathsf{{s_{last}}_J}$ never decreases, \r
+client $\mathsf{J}$ cannot then send a message with sequence number \r
+$\mathsf{s_{r_1}}$, a contradiction.\r
+\item Case 2.2: Client $\mathsf{J}$ sends $\mathsf{r_1}$, and then $\mathsf{m}$. \r
+Let $\mathsf{X = (r_1 = x_1, \dots , x_n)}$ be the list of messages $\mathsf{J}$ sends \r
+starting before $\mathsf{r_1}$ and ending before $m$; clearly these all have sequence \r
+number $\mathsf{s_p = s_q + 1}$.\r
+\begin{itemize}\r
+\item Case 2.2.1: Some message in $\mathsf{X}$ was accepted. Before sending $\mathsf{m}$, \r
+$\mathsf{J}$'s value in $\mathsf{MS_J}$ for its own latest sequence number would \r
+be strictly greater than $\mathsf{s_{q_J}}$. If there is a sequence of messages with \r
+contiguous sequence numbers that $\mathsf{J}$ receives between $\mathsf{r_1}$ and \r
+$\mathsf{m}$, $\mathsf{J}$ throws an error for a similar reason as Case 1.1. Otherwise, \r
+when preparing to send $\mathsf{m}$, $\mathsf{J}$ would have received an update of its \r
+own latest sequence number as at most $\mathsf{s_{q_J}}$. $J$ throws an error before \r
+sending $\mathsf{p}$, because its own latest sequence number decreases.\r
+\item Case 2.2.2: All messages in $\mathsf{X}$ were rejected, making $\mathsf{m}$ \r
+the first message of $\mathsf{J}$ that is accepted after $\mathsf{r_1}$.\r
+\r
+We will show that $\mathsf{C}$ sees $\mathsf{r_1}$. Assume not. Then $\mathsf{(r_2, ..., u)}$ \r
+must have at least $\mathsf{{max_g}_C} \geq 2$ messages for $\mathsf{r_1}$ to fall off the \r
+end of the queue. Consider the sender of $\mathsf{r_3}$ and call it $\mathsf{H}$. \r
+$\mathsf{H \neq J}$ by Proposition \ref{prop:bothmessages} and the existence of $\mathsf{m}$. \r
+Since $\mathsf{H \neq J}$, then by Proposition \ref{prop:bothmessages} it could not also \r
+have sent a message in $\mathsf{(l_2,..., u)}$. Therefore, $\mathsf{s_{u_H} < s_q + 2 = s_{t_H}}$, \r
+so upon receipt of $\mathsf{u}$, $\mathsf{C}$ will throw an error by the decrease in a \r
+last sequence number similar to Case 1, a contradiction.\r
+\r
+Now that we know that $\mathsf{C}$ sees $\mathsf{r_1}$, note that C receives $\mathsf{u}$ \r
+immediately after $\mathsf{t}$ by Proposition \ref{prop:seqnumb}. Therefore, \r
+$\mathsf{C}$ could not have seen a message after $\mathsf{t}$ with sequence number less \r
+than $\mathsf{s_m}$. In the $\mathsf{PutDataEntries()}$ subroutine, $\mathsf{J}$ adds every \r
+$\mathsf{cr}$ entry that contains sequence number $\mathsf{s}$ and machine ID \r
+$\mathsf{id}$ of the messsages that win in the collisions before $\mathsf{m}$ into \r
+$\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{i}$, $\mathsf{1 \leq i < |X|}$, \r
+the collision winner that has collided with $\mathsf{x_i}$ 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}$ \r
+is received, and $\mathsf{C}$ sees $\mathsf{r_1}$, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the \r
+collision against ${r_1}$.\r
+\r
+When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$ \r
+has seen the $\mathsf{cr}$ entry that records the collision at index $\mathsf{s_q + 1}$, it will 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
+\r
+\end{itemize}\r
+\end{itemize}\r
+\r
+\end{itemize}\r
+\end{proof}\r
+\r
+\begin{lem} \r
+\label{lem:pathmessages}\r
+If there are two messages $\mathsf{t}$ and $\mathsf{u}$, with \r
+$\mathsf{s_t \leq s_u}$, such that $\mathsf{t}$ is in the path of $\mathsf{u}$, \r
+then for any message $\mathsf{p}$ with $\mathsf{s_p \leq s_t}$, iff $\mathsf{p}$ is in \r
+the path of $\mathsf{t}$, it is in the path of $\mathsf{u}$. \r
+\end{lem}\r
+\r
+\begin{proof}\r
+If $\mathsf{s_t = s_u}$ or $\mathsf{s_p = s_t}$, then we are done, because the two \r
+relevant messages are the same. If they are different messages, then:\r
+\begin{itemize}\r
+\item Reverse direction: The definition of $\mathsf{t}$ being in the path of \r
+$\mathsf{u}$ is the existence of a message sequence $\mathsf{(\dots, t, \dots, u)}$ \r
+such that each message except $\mathsf{u}$ is the parent of the succeeding message. \r
+The path of $\mathsf{u}$ must contain some message with sequence number $\mathsf{s_p}$; \r
+because $\mathsf{p}$ is in the path of $\mathsf{u}$, this message is $\mathsf{p}$ \r
+itself. The path of $\mathsf{t}$ is then the prefix of this path ending at $\mathsf{t}$, \r
+which clearly contains $\mathsf{p}$.\r
+\r
+\item Forward direction: The path of $\mathsf{t}$ is a substring of the path of \r
+$\mathsf{u}$, so if the path of $\mathsf{t}$ contains $\mathsf{p}$, so does the path \r
+of $\mathsf{u}$.\r
+\end{itemize}\r
+\end{proof}\r