Theorem 1: The algorithm solve_constraints( S ) returns a cluster tree satisfying S if S is consistent, and returns false if S is inconsistent. Proof: If solve constraints( S ) returns false, then it is inconsistent (lemma 9). If it does not return false, then it returns a cluster tree T (lemma 12). Since T has an instantiation
(lemma 2) and since every instantiation of T is a solution of S (lemma 15), it follows that S is consistent and T satisfies S. □

## Proof Of Theorem 2

Lemma 16: If S 1 and S 2 are consistent sets of constraints, and S 1 D S 2 then reduce constraints( S 1 ) 
Proof: Immediate by construction. The value of H in the case of S 1 is a superset of its value in the case of S2, and hence reduce constraints( S1 ) is a superset of reduce constraints( S2 ).

Lemma 17: If S 1 and S 2 are consistent sets of constraints, and S 1 ⊃ S 2 then num labels( S 1 )
≥ num labels( S 2 ). Proof by induction on num labels( S 2 ). If num labels( S 2 ) = 0, the statement is trivial. Suppose that the statement holds for all S ′ , where num labels( S ′ ) = k .

Let num labels( S 2 ) = k + 1 . Then k + 1 = num labels( S 2 ) = 1 + num labels(reduce constraints( S 2 )), so k =num labels(reduce constraints( S 2 )). Now, suppose S 1 ⊃ S 2 . By lemma 16 reduce constraints( S 1 ) ⊃ reduce constraints( S 2 ). But then by the inductive hypothesis nmmmmmme num labels( S 1 ) ≥  num labels( S 2 ).  □ Lemma 18: Let S be a set of constraints, and let Γ be a solution of S. For any graph G
over the symbols of S, let nd( G, Γ) be the number of different non-zero values of od( a, b )
where edge ab is in G. Let edges( S ) be the set of edges in S. Then nd(edges( S ), Γ) ≥
num Jabels( S ).

Proof: by induction on num labels( S ). If num labels( S ) = 0, then the statement is trivial. Suppose for some k , the statement holds for all S ′ where num Jabels( S ′ ) = k , and suppose num labels( S ) = k + 1. Let pq be the edge in S of maximal length. For any set of edges E ,
let small-edges( E, Γ) be the set of all edges ab in E for which od(Γ(α), Γ(δ)) ≪ od(Γ(ρ), Γ(φ)).  Since small-edges( E ) contains edges of every order of magnitude in E except the order of magnitude of pq, it follows that nd(small-edges( E, Γ), Γ) = nd( E, Γ) − 1. Let G be the complete graph over all the symbols in S .  By the same argument as in lemma 5, small-edges( G, Γ) D H, where H is the connected components of the shorts of S t as computed in reduce_constraints( S ). Let S t be the set of constraints whose longs are in small-edges( G, Γ). It follows that S ′ D reduce constraints( S ). Now small-edges( G, Γ) Ξ edges( S ′ ) ニ edges( reduce_constraints( S )). Hence nd(edges( S ), Γ) = nd( G, Γ) = nd(small-edges( G, Γ), Γ) + 1 ≥ nd(edges(reduce_constraints( S ))) + 1 ≥ (by the inductive hypothesis) num labels(reduce constraints( S )) + 1 = num labels( S ). □