Validation of algorithm solve_constraints2

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