95
new address is created immediately preceding any data that may have originally followed it.
This new point follows the newly inserted data.
4.4 Some facts about P-sequences
The P-sequence has a number of properties that make it useful for modeling version
management, (collaborative) undo, merge, and non-sequential undo. The following lemma
summarizes a number of these properties.
Lemma 4.4:The following claims are true for a minimally consistent change set S:
For Id(c) = I, Refs(I)eS, A’(S) ˝ A’(S ¨ c).
1. IfX
S is a P-sequence, and a <
SA bin X, then givenId(c) = I, Refs(I)eS, andX’
S a P-
sequence for S ¨ c, then a <
SA binX’.
2. Any data that is the source only of move changes, appears exactly once in the P-
sequence.
3. ForId(c) = I, Refs(I)eS, A’(S ¨ c)is a causal change set.
4. IfXis a P-sequence forS, for any addressa e S,Length(C
X (a, P
X (I
X (a)+1))) £ 1.
5. IfXis a P-sequence for a setS, then for any values
i in the contents, s
1 …s
i …s
n of a
P-sequence, there is at least one pair of addresses a, a’ such that C
X (a, a’, S) = s, and
for which there exists no c e S, withDest(c) = aorDest(c) = a’.
Proof: Claim 1 can be verified by examination ofDefinition4.1, andDefinition4.9. New
changes never remove addresses.
Claim 2 is a consequence of Definition 4.8. For any addressesa, binS,their relative order
is determined entirely by changes already in S. The new change cannot either a target of a
destination of aorb(because S is minimal consistent), nor can its ID be in the path of any
address in A’(S). Therefore, the ordering of aandbcannot be affected in A’(S ¨ c).
Claim 3 is bit more complex. It depends on clauses 6 and 7 of
new address is created immediately preceding any data that may have originally followed it.
This new point follows the newly inserted data.
4.4 Some facts about P-sequences
The P-sequence has a number of properties that make it useful for modeling version
management, (collaborative) undo, merge, and non-sequential undo. The following lemma
summarizes a number of these properties.
Lemma 4.4:The following claims are true for a minimally consistent change set S:
For Id(c) = I, Refs(I)eS, A’(S) ˝ A’(S ¨ c).
1. IfX
S is a P-sequence, and a <
SA bin X, then givenId(c) = I, Refs(I)eS, andX’
S a P-
sequence for S ¨ c, then a <
SA binX’.
2. Any data that is the source only of move changes, appears exactly once in the P-
sequence.
3. ForId(c) = I, Refs(I)eS, A’(S ¨ c)is a causal change set.
4. IfXis a P-sequence forS, for any addressa e S,Length(C
X (a, P
X (I
X (a)+1))) £ 1.
5. IfXis a P-sequence for a setS, then for any values
i in the contents, s
1 …s
i …s
n of a
P-sequence, there is at least one pair of addresses a, a’ such that C
X (a, a’, S) = s, and
for which there exists no c e S, withDest(c) = aorDest(c) = a’.
Proof: Claim 1 can be verified by examination ofDefinition4.1, andDefinition4.9. New
changes never remove addresses.
Claim 2 is a consequence of Definition 4.8. For any addressesa, binS,their relative order
is determined entirely by changes already in S. The new change cannot either a target of a
destination of aorb(because S is minimal consistent), nor can its ID be in the path of any
address in A’(S). Therefore, the ordering of aandbcannot be affected in A’(S ¨ c).
Claim 3 is bit more complex. It depends on clauses 6 and 7 of
