As mentioned earlier, we want to calculate the sources relative to a particular control word. The following lemmas allow us to do this. Note that these apply only to the commuting/inverse structures, they are not general properties of structures with an equivalence relation.
Lemma .conflict
For structures with commuting and inverse directions, if u and v
are legal (contain no inverse directions) then where
.
Proof: follows directly from the fact that the
equivalence relation is of the form of a set of string rewriting
rules.
does depend on the nature of the rules. Let us
suppose
. Since the rules only allow for the
transposition of commuting directions, and x = x, we infer that u
and v must contain the same set of letters. Now, if u and v only
contain commuting directions then we have the result. Let us assume
otherwise, that there is a pair of non-commuting directions in u. We
observe that in x.u any non-commuting pairs must retain the same
strict order when we apply rules to convert it to x.v. This same
order will be preserved when we compare u and v. Therefore all
non-commuting pairs in u and v will retain the same relative
order, thus
.
Definition 1183
Two control words V and V' conflict , if one reads a value
that the other writes to, i.e. Data Data(V'.W).
Lemma .conflict
If V and V' conflict then, , X.V and
X.V' conflict.
Proof: Follows from Lemma 1, since Data Data(A).Data(B).
Lemma .conflict
If X'.W is the source of X.R, then ,if V.X'.W is executed then it is the source of V.X.R.
Proof: X'.W being the source of X.R means that they conflict and
X'.W < X.R, and if Y.W and X.R conflict, for any ,then Y.W < X'.W.
Firstly V.X'.W < V.X.R and V.X'.W conflicts with V.X.R, from Lemma 2. Now suppose that there exists a Z, such that V.X'.W < Z.W < V.X.R, and Z.W conflicts with V.X.R. The inequalities imply that Z is of the form V.K for some K. Since Z = V.K conflicts with V.X, K must conflict with X, from Lemma 2. This implies that K.W should be the source of X.W, which is a contradiction, hence the result.