Validation of algorithm solve_constraints2

The proof of the correctness of algorithm solve_constraints2 is again analogous in structure to the proof of theorem 1. We sketch it below: the details are not difficult to fill in.

1.

(Analogue of lemma 2:) If T is an ordered cluster tree, then the revised version of instantiate(T) returns an instantiation of T. The proof is exactly the same as lemma 2, with the additional verification that instantiate2 preserves the orderings in T.

2.

(Analogue of lemma 5:) Let S be a set of order-of-magnitude constraints on distances, and let O be a set of ordering constraints on points. Let H be the graph given by the two statements

H := the connected components of the shorts of S;
H := incorporate_order(H, O);

If S and O are consistent, then H does not contain all the edges of S.

Proof: As in the proof of lemma 5, choose a valuation Z satisfying S,O and let pq be an edge in S for which od( Z(p), Z(q)) is maximal. Following the informal argument presented in section 6.3, it is easily shown that pq is longer than any of the edges added in these two statements, and hence it is not in H.

3.

(Analogue of lemma 9:) If solve_constraints2 returns false, then S,O is inconsistent. Proof: Immediate from (2).

4.

(Analogue of lemma 12:) If solve_constraints2(S,O) does not return false, then it returns a well-formed ordered cluster tree.

Proof: By merging the strongly connected components of G, incorporate_order always ensures that the ordering arcs between connected components of H form a DAG. These arcs are precisely the same ones that are later added among the children of node N as ordering arcs. Thus, the ordering arcs over the children of a node in the cluster tree form a DAG. Otherwise, the construction of the tree T is the same as in lemma 12.

The remainder of the proof is the same as the proof of theorem 1.