v 6∈ τ[T ]. (Remark that this case is irrelevant to condition C4.) We remove v **from** τ[T ].

For each i 6∈ lb(S) such that τ[Xi] = v we remove i from τ[S**]. With C1 we are sure that** none of the i in lb(S) have τ[Xi] = v**, thanks to property P7 and the fact that** v 6∈ lb(T ).

With C3 we are sure that none of the i in lb(S) have τ[Xi] = v**, thanks to property P5**
and the fact that v 6∈ lb(T ). There remains to check C2. For each i ∈ lb(S**), we know** that ∃v
′ 6= v, v′ ∈ D(Xi) ∩ ub(T **), thanks to properties P3 and P5. We set** Xi to v
′
in τ**, we add** v
′
to τ[T ] and add all k with τ[Xk] = v
′
to τ[S**]. We are sure that** k ∈ ub(S)
because v
′ ∈ ub(T **) plus condition C2 and property P8.**
Completeness on ub(T ), lb(S), ub(S) and Xi**'s are shown with similar proofs. Let**
v ∈ ub(T ) \ τ[T **]. (Again C4 is irrelevant.) We show that there exists a solution with** v ∈ τ[T ]. Add v to τ[T ] and for each i ∈ ub(S), if τ[Xi] = v, put i in τ[S**]. C2 is solved** thanks to property P8 and the fact that v ∈ ub(T **). C3 is solved thanks to property** P6 and the fact that v ∈ ub(T ). There remains to check C1. For each i 6∈ ub(S**) and** τ[Xi] = v**, we know that** ∃v
′ 6= v, v′ ∈ D(Xi) \ lb(T **) (thanks to properties P4 and P6).**
We set Xi to v
′
in τ **and remove** v
′
from τ[T ]. Each k with τ[Xk] = v
′
**is removed**
from τ[S**], and this is possible because we are in condition C1,** v
′ 6∈ lb(T **), and thanks to**
property P7.

Let v ∈ D(Xi) and τ[Xi] = v
′
, v′ 6= v. (C3 is irrelevant.) Assign v to Xiin τ**. If**
both v and v
′ or none of them are in τ[T **], we are done. There remain two cases. First,**
if v ∈ τ[T **] and** v
′ 6∈ τ[T ], the two alternatives to satisfy Roots are to add i in τ[S**] or**
to remove v from τ[T ]. If i ∈ ub(S), we add i to τ[S] and we are done. If i 6∈ ub(S**), we** know that v 6∈ lb(T ) thanks to property P4. So, v is removed from τ[T **] and we are sure**
that the Xj **'s can be updated consistently for the same reason as in the proof of** lb(T ).

Second, if v 6∈ τ[T **] and** v
′ ∈ τ[T ], the two alternatives to satisfy Roots **are to remove** i from τ[S] or to add v to τ[T ]. If i /∈ lb(S), we remove i from τ[S**] and we are done. If** i ∈ lb(S), we know that v ∈ ub(T ) thanks to property P3. So, v is added to τ[T **] and we**
are sure that the Xj**'s can be updated consistently for the same reason as in the proof**
of ub(T ) \ τ[T ].

Let i 6∈ lb(S) and i ∈ τ[S]. We show that there exists a solution with i 6∈ τ[S**]. We**
remove i from τ[S]. Thanks to property P1, we know that D(Xi) 6⊆ lb(T **). So, we set**
Xi **to a value** v
′ ∈ D(Xi) \ lb(T **). With C4 we are done because we are sure** v
′ 6∈ τ[T ].

With conditions C1, C2, and C3, if v
′ ∈ τ[T ], we remove it from τ[T **] and we are sure**
that the Xj **'s can be updated consistently for the same reason as in the proof of** lb(T ).

Let i ∈ ub(S) \ τ[S]. We show that there exists a solution with i ∈ τ[S**]. We add** i to τ[S]. Thanks to property P2, we know that D(Xi) ∩ ub(T ) 6= ∅. So, we set Xi **to a**
value v
′ ∈ D(Xi)∩ub(T **). With condition C4 we are done because we are sure** v
′ ∈ τ[T ].

With conditions C1, C2, and C3, if v
′ 6∈ τ[T ], we add it to τ[T **] and we are sure that the**
Xj **'s can be updated consistently for the same reason as in the proof of** ub(T ) \ τ[T ]. ✷

## 5.4 Bound Consistency

In addition to being able to enforce HC on Roots **in some special cases, enforcing HC**
on the decomposition always enforces a level of consistency at least as strong as BC. In fact, in any situation (even those where enforcing HC is intractable), enforcing BC on the decomposition enforces BC on the Roots **constraint.**