91
applied to a pair of address, (a, b). By induction we can assume that all pairs(c, d) <
wf (a, b)
are totally ordered under <
sa . Since (a, b)and(c, d) must be ordered by some clause of the
definition, we will just consider them in order. In the discussion of a case, I also sometimes
comment on the intent of that clause of the definition.
Case 1 is a base case, and orders the two addresses by the strict ordering <
d , preserving
the induction hypothesis.
Case 2 is a base case, and orders the two addresses by the normal strict order on inte-
gers. This only applies to two addresses involving the same insertion change. Cases 1 and 2
can never conflict, since their preconditions do not overlap.
Case 3 is true by induction since the addresses X,X’ are clearly less under <
d .
Case 4 is true by induction, sinceDest(I
1 )and Dest(I’
1 )are both less under<
wf . Any two
addresses created by different changes are ordered in terms of their destinations. Since Sis
unconflicted, these must be different.
Case 5 is also true by induction, since (I
2 …I
n , i)and(I’
2 …I’
n , j)are also smaller under
<
wf . If the two addresses to be compared are both part of the result of some move or copy
operation, they should be compared relative to its source. This final case completes the
proof, and establishes a total ordering on all legal addresses for a minimally consistent
change set. v
Theorem 4.3:nilis the minimal element under<
SA .
Proof: This is a consequence of Definition4.4.nilis minimal under the refers relation<
r ,
which means that for any non-empty change set there is one insertion Isuch that
Dest(I) = nil. Since every address in that insertion will be greater thannil, no subsequent
insertion or move operation that follows will be able to create an address that is less than
nil.v
A possible extension:
applied to a pair of address, (a, b). By induction we can assume that all pairs(c, d) <
wf (a, b)
are totally ordered under <
sa . Since (a, b)and(c, d) must be ordered by some clause of the
definition, we will just consider them in order. In the discussion of a case, I also sometimes
comment on the intent of that clause of the definition.
Case 1 is a base case, and orders the two addresses by the strict ordering <
d , preserving
the induction hypothesis.
Case 2 is a base case, and orders the two addresses by the normal strict order on inte-
gers. This only applies to two addresses involving the same insertion change. Cases 1 and 2
can never conflict, since their preconditions do not overlap.
Case 3 is true by induction since the addresses X,X’ are clearly less under <
d .
Case 4 is true by induction, sinceDest(I
1 )and Dest(I’
1 )are both less under<
wf . Any two
addresses created by different changes are ordered in terms of their destinations. Since Sis
unconflicted, these must be different.
Case 5 is also true by induction, since (I
2 …I
n , i)and(I’
2 …I’
n , j)are also smaller under
<
wf . If the two addresses to be compared are both part of the result of some move or copy
operation, they should be compared relative to its source. This final case completes the
proof, and establishes a total ordering on all legal addresses for a minimally consistent
change set. v
Theorem 4.3:nilis the minimal element under<
SA .
Proof: This is a consequence of Definition4.4.nilis minimal under the refers relation<
r ,
which means that for any non-empty change set there is one insertion Isuch that
Dest(I) = nil. Since every address in that insertion will be greater thannil, no subsequent
insertion or move operation that follows will be able to create an address that is less than
nil.v
A possible extension:
