We now prove that the revised algorithm presented in section 6.2 for non-strict comparisons is correct. The proof is only a slight extension of the proof of theorem 1, given above. Recall that the revised algorithm in section 6.2 replaces the line of solve_constraints
H := the connected components of the shorts of Swith the following code:
1. H := the shorts of S; 2. repeat H := the connected components of H; 3. for each weak constraint od(a,b) <<= od(c,d) 4. if cd is in H then add ab to H endif endfor 5. until no change has been made to H in the last iteration.
We need the following new lemmas and proofs:
Lemma 20: Let S be a set of strict comparisons, and let W be a set of non-strict comparisons. Let H be the set of edges output by the above code. If S union W is consistent, then there is an edge in S that is not in H.
Proof: As in the proof of lemma 5, let Z be a valuation satisfying S union W and let pq be an edge in S such that od( Z(p), Z(q)) is maximal. We wish to show that, for every edge ab in H, od( Z(a), Z(b)) << od( Z(p), Z(q)), and hence ab <> pq. Proof by induction: suppose that this holds for all the edges in H at some point in the code, and that ab is now to be added to H. There are three cases to consider.
Lemma 21: Let W contain the constraint od(a,b) <<= od(c,d). Suppose that the algorithm returns a cluster tree T. Let M be the least common ancestor of a and b in T, and let N be the least common ancestor of c and d. Then M.label <= N.label.
Proof: By lemma 13, N is assigned a label in the first iteration where H does not include the edge cd. In all previous iterations, since cd is in H, ab will likewise be put into H. Hence M does not get assigned a label before N, so M.label <= N.label.
The remainder of the proof of the correctness of the revised algorithm is exactly the same as the proof of theorem 1.