Proof of Theorem 2

**Lemma 16:** If *S*_{1} and *S*_{2} are consistent sets of constraints, and
*S*_{1} is a superset of *S*_{2} then
reduce_constraints(*S*_{1}) is a superset (not necessarily
proper) of reduce_constraints(*S*_{2}).

**Proof:** Immediate by construction. The value of *H* in the case
of *S*_{1} is a superset of its value in the case of *S*_{2},
and hence reduce_constraints(*S*_{1}) is a superset of
reduce_constraints(*S*_{2}).

**Lemma 17:** If *S*_{1} and *S*_{2}are consistent sets of constraints, and
*S*_{1} is a superset of *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} contains *S*_{2}. By lemma 16
reduce_constraints(*S*_{1}) contains
reduce_constraints(*S*_{2}). But then by the inductive
hypothesis
num_labels(reduce_constraints(*S*_{1})) >=num_labels(reduce_constraints(*S*_{2})), so
num_labels(*S*_{1}) >= num_labels(*S*_{2}).

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