Appendix

  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 $u \equiv v \iff x.u \equiv x.v$ where $x,u,v \in D^{*}$.

Proof: $\Rightarrow$ follows directly from the fact that the equivalence relation is of the form of a set of string rewriting rules. $\Leftarrow$ does depend on the nature of the rules. Let us suppose $x.u \equiv x.v$. 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 $u \equiv v$.

Definition 1183

Two control words V and V' conflict , if one reads a value that the other writes to, i.e. Data$(V.R) \equiv$ Data(V'.W).

Lemma .conflict

If V and V' conflict then, $\forall X \in C^{*}$, X.V and X.V' conflict.

Proof: Follows from Lemma 1, since Data$(A.B) \equiv$ Data(A).Data(B).

Lemma .conflict

If X'.W is the source of X.R, then $\forall V \in C^{*}$,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 $Y \in C^{*}$,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.