\r
\begin{algorithmic}[1]\r
\Function{Put}{$KV_s,\tuple{k_s,v_s}$} \Comment{Interface function to update a key-value pair}\r
-\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV,k_s)$\r
+\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV_s,k_s)$\r
\If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
\State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
\State $ck_p \gets ck_p + 1$\r
Then $\mathsf{t}$ is in the path of $\mathsf{u}$. \r
\end{lem}\r
\begin{proof}\r
-Assume otherwise. Then there are some pairs $\mathsf{(t,u)}$ that violate this lemma. \r
-Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized and \r
-$\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$.\r
+Assume that there are some pairs of messages $\mathsf{(t,u)}$ that violate this lemma. \r
+Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized, and \r
+$\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$. We will show that $\mathsf{C}$\r
+cannot receive both $\mathsf{t}$ and $\mathsf{u}$ without throwing an error.\r
\r
Clearly $\mathsf{C}$ will throw an error if $\mathsf{s_t = s_u}$. So \r
$\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ receives $\mathsf{u}$ before \r