Lemma 16: If S1 and S2 are consistent sets of constraints, and S1 is a superset of S2 then reduce_constraints(S1) is a superset (not necessarily proper) of reduce_constraints(S2).
Proof: Immediate by construction. The value of H in the case of S1 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 S1 and S2are consistent sets of constraints, and S1 is a superset of S2 then num_labels(S1) >= num_labels(S2).
Proof by induction on num_labels(S2). If num_labels(S2) = 0, the statement is trivial. Suppose that the statement holds for all S', where num_labels(S') = k. Let num_labels(S2) = k+1. Then k+1 = num_labels(S2) = 1 + num_labels(reduce_constraints(S2)), so k =num_labels(reduce_constraints(S2)). Now, suppose S1 contains S2. By lemma 16 reduce_constraints(S1) contains reduce_constraints(S2). But then by the inductive hypothesis num_labels(reduce_constraints(S1)) >=num_labels(reduce_constraints(S2)), so num_labels(S1) >= num_labels(S2).
Lemma 18: Let S be a set of constraints, and let Z be a solution of S. For any graph G over the symbols of S, let nd(G,Z) 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), Z) >=num_labels(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_labels(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,Z) be the set of all edges ab in E for which od( Z(a), Z(b)) << od( Z(p), Z(q)). 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,Z), Z) = nd(E,Z) - 1. Let G be the complete graph over all the symbols in S. By the same argument as in lemma 5, small-edges(G,Z) contains H, where H is the connected components of the shorts of S, as computed in reduce_constraints(S). Let S' be the set of constraints whose longs are in small-edges(G,Z). It follows that S' contains reduce_constraints(S). Now small-edges(G,Z) contains edges(S'), which contains edges(reduce_constraints(S)). Hence nd(edges(S), Z) = nd(G,Z) = nd(small-edges(G,Z), Z) + 1 >= nd(edges(reduce_constraints(S))) + 1 >= (by the inductive hypothesis) num_labels(reduce_constraints(S)) + 1 = num_labels(S).
Theorem 2: Out of all solutions to the set of constraints S, the instantiations of solve_constraints(S) have the fewest number of different values of od(a,b), where a,b range over the symbols in S. This number is given by num_labels(S).
Proof: Immediate from lemma 18.
Corollary 19: Let O have all the properties of an om-space except that it has only k different orders of magnitude. A system of constraints S has a solution in O if and only if the tree returned by solve_constraints(S) uses no more than k different labels.
Proof: Immediate from theorems 1 and 2.