Proof of causal multicast algorithm? I'm reading Causal Memory:
Denitions, Implementation and
Programming and trying to get through the proof of liveliness of the algorithm around the middle of page 9, and I'm not really following it. There's almost certainly a typo/misprint when they refer to the $(s(q) \mathbin\bot 1)$st write. I assume they meant $(s(q) - 1)$st, but even then I'm not really following the reasoning of the proof.

Does anyone have a reference to this proof in the context of a causal multicast that I could look through instead? (or in any other context?)

Alternatively, can someone try to explain the proof. In particular I don't get:


"Let $\hat{w}$ be the $(s(q)\mathbin\bot1)$st write." Even assuming $s(q) - 1$, what if $s(q)$ is $0$ or $1$?
Why does lemma 1 say that $t(\hat{w}) \preceq t(w)$?
Even if we assume $t[j] \ge s[j] - 1$ (equivalently $s[j] \le t[j] + 1$), why is this sufficient? Don't we need to show $s[j] \mathbf{=} t[j] + 1$?


Sorry if this question isn't appropriate/is tagged incorrectly.
Basically you have been mislead by the errors in the proof in the edition of the paper you are referring to. Please refer to the published edition on "Distributed Computing'1995".


  There's almost certainly a typo/misprint when they refer to the $(s[q] \bot 1)$st write.


Yes, it is a typo. It should be "the $(s[i] - 1)$st write" (not $(s[j] - 1)$st either)


  "Let $\hat{w}$ be the $(s[j] - 1)$st write." Even assuming $s[j]−1$, what if $s[j]$ is 0 or 1?


It should be "Let $\hat{w}$ be the $(s[i] - 1)$st write."
By definition, $s$ is the timestamp of the write operation $w$ of process $i$. According to the rule of Write operation in Fig.3, we have $s[i] \ge 1$. The problem is what if $s[i] = 1$. Well, it seems that the authors have missed the edge case. Fortunately, it is obviously true that $t[i] = 0 = s[i] - 1$.


  Why does lemma 1 say that $ts(\hat{w}) \le ts(w)$?


$\hat{w}$ and $w$ are two consecutive write operations in process $i$ and $\hat{w}$ is the former one. According to the rule of Write operation in Fig.3, we have $ts(\hat{w}) \le ts(w)$. (Actually, we have $ts(\hat{w}) &lt; ts(w)$.)


  Even if we assume $t[i] \ge s[i]−1$, why is this sufficient? Don't we need to show $s[i]=t[i]+1$?


Yes, you are right. That is exactly what are proved in the DC edition.