  The replicated list object is frequently used to model the core functionality
of replicated collaborative text editing systems. Since 1989, the convergence
property has been a common specification of a replicated list object. Recently,
Attiya et al. proposed the strong/weak list specification and conjectured that
the well-known Jupiter protocol satisfies the weak list specification. The
major obstacle to proving this conjecture is the mismatch between the global
property on all replica states prescribed by the specification and the local
view each replica maintains in Jupiter using data structures like 1D buffer or
2D state space. To address this issue, we propose CJupiter (Compact Jupiter)
based on a novel data structure called $n$-ary ordered state space for a
replicated client/server system with $n$ clients. At a high level, CJupiter
maintains only a single $n$-ary ordered state space which encompasses exactly
all states of each replica. We prove that CJupiter and Jupiter are equivalent
and that CJupiter satisfies the weak list specification, thus solving the
conjecture above.
