Proof of algorithm for non-strict comparisons

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

with the following code:H:= the connected components of the shorts ofS

1.H:= the shorts ofS; 2.repeatH:= the connected components ofH; 3.foreach weak constraint od(a,b) <<= od(c,d) 4.ifcdis inHthen addabtoHendif endfor5.untilno change has been made toHin 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.

*ab*is added in step [1]. Then, as in lemma 5, there is a constraint od(*a*,*b*) << od(*c*,*d*) in*S*. Hence od(*Z*(*a*),*Z*(*b*)) << od(*Z*(*c*),*Z*(*d*)) <<= od(*Z*(*p*),*Z*(*q*)).*ab*is added in step [2]. Then there is a path*a*_{1}=*a*,*a*_{2}...*a*_{k}=*b*such that the edge*a*_{i}*a*_{i+1}is in*H*for*i*=1 ...*k*-1. By the inductive hypothesis, od(*Z*(*a*_{i}),*Z*(*a*_{i+1})) << od(*Z*(*p*),*Z*(*q*)). By the om-triangle inequality, od(*Z*(*a*),*Z*(*b*)) <<=*max*_{i=1 .. k-1}(od (*Z*(*a*_{i}),*Z*(*a*_{i+1}))) <<od(*Z*(*p*),*Z*(*q*)).*ab*is added in step [4]. Then there is a constraint od(*a*,*b*) <<= od(*c*,*d*) in*W*such that*cd*is in*H*. By the inductive hypothesis, od(*Z*(*c*),*Z*(*d*)) << od(*Z*(*p*),*Z*(*q*)).

**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.