97
• Claim 3 shows that even conflicting move operations will only rearrange, never delete,
data. This provides the most sensible results for conflicting moves (as identified in Sec-
tion 3.3.3).
• Claim 4 shows that conflict detection is simple, and that any non-conflicting change can
be added to a minimally consistent change set to produce a new minimally consistent
change set.
• Claim 5 shows that the addressing mechanism of P-sequences is fine-grained enough to
address every element of a sequence individually, as well as reinforcing the notion that
not every range of addresses actually contains a non-empty subsequence.
• Claim 6 shows that there is always an address for every gap in the state represented by a
P-sequence. This ensures that it is always possible to create a non-conflicting change for
a given change set.
Theorem 4.4:For a P-sequenceX
S , I e S, andDeleted(Dest(I)), thenC
X (a
1 , a
2 , S) = L,if:
1. Change(I) = I[a, s], and b
1 = (I,
0) £
SA a
1 and a
2 £
SA b
2 = (I, Length(s))
.
2. Change(I) = M[x
1 , x
2 , d],x
1 = (I’
1 …I’
n , i), x
2 = (I’’
1 …I’’
n , j), b
1 = (I
I’
1 …I’
n , i) £
SA a
1
and a
2 £
SA b
1 = (I
I’’
1 …I’’
n , j).
3. Change(I) = C[x
1 , x
2 , d],x
1 = (I’
1 …I’
n , i), x
2 = (I’’
1 …I’’
n , j), b
1 = (I
I’
1 …I’
n , i) £
SA a
1 and
a
2 £
SA b
1 = (I
I’’
1 …I’’
n , j).
Proof: By straightforward application ofDefinition4.8,Deleted(b
1 , b
2 ). Sincea
1 and a
2 are
contained in the same interval, they too are deleted.v
This lemma is important for implementers as it allows an implementation to ignore any
addresses created by a change if its destination is deleted.
Theorem 4.5:Assume there is a P-sequenceX
S , with a
1 = (I…I’
n , I), a
2 = (I…I’’
n , j),I e S,
and Change(I) = M[s, e, d]. If there are two addresses,aandb, witha £
SA Dest(I) £
SA b, and
Moved(a, b, S – RecessiveMoves(I, S)), thenC
X (a
1 , a
2 , S)) = L.
• Claim 3 shows that even conflicting move operations will only rearrange, never delete,
data. This provides the most sensible results for conflicting moves (as identified in Sec-
tion 3.3.3).
• Claim 4 shows that conflict detection is simple, and that any non-conflicting change can
be added to a minimally consistent change set to produce a new minimally consistent
change set.
• Claim 5 shows that the addressing mechanism of P-sequences is fine-grained enough to
address every element of a sequence individually, as well as reinforcing the notion that
not every range of addresses actually contains a non-empty subsequence.
• Claim 6 shows that there is always an address for every gap in the state represented by a
P-sequence. This ensures that it is always possible to create a non-conflicting change for
a given change set.
Theorem 4.4:For a P-sequenceX
S , I e S, andDeleted(Dest(I)), thenC
X (a
1 , a
2 , S) = L,if:
1. Change(I) = I[a, s], and b
1 = (I,
0) £
SA a
1 and a
2 £
SA b
2 = (I, Length(s))
.
2. Change(I) = M[x
1 , x
2 , d],x
1 = (I’
1 …I’
n , i), x
2 = (I’’
1 …I’’
n , j), b
1 = (I
I’
1 …I’
n , i) £
SA a
1
and a
2 £
SA b
1 = (I
I’’
1 …I’’
n , j).
3. Change(I) = C[x
1 , x
2 , d],x
1 = (I’
1 …I’
n , i), x
2 = (I’’
1 …I’’
n , j), b
1 = (I
I’
1 …I’
n , i) £
SA a
1 and
a
2 £
SA b
1 = (I
I’’
1 …I’’
n , j).
Proof: By straightforward application ofDefinition4.8,Deleted(b
1 , b
2 ). Sincea
1 and a
2 are
contained in the same interval, they too are deleted.v
This lemma is important for implementers as it allows an implementation to ignore any
addresses created by a change if its destination is deleted.
Theorem 4.5:Assume there is a P-sequenceX
S , with a
1 = (I…I’
n , I), a
2 = (I…I’’
n , j),I e S,
and Change(I) = M[s, e, d]. If there are two addresses,aandb, witha £
SA Dest(I) £
SA b, and
Moved(a, b, S – RecessiveMoves(I, S)), thenC
X (a
1 , a
2 , S)) = L.
