{A(ν l i
) < A(ν j+1 i), A(ν j+1 i) < A(ν l i
)}, l > j, will be implied by O ∪ {Ap < At < Ac}**, and it**
contradicts with the assumption that O ∪ {Ap < At < Ac} **is consistent.**
(3) The ordering constraints are consistent if no two operators Ai and Aj **are such that**
O implies {{Ai < Aj}, {Aj < Ai}}. In what follows, Ai **will be used to denote an arbitrary**
operator affecting variable vi.

First note that each ordering constraint added in Step 4 or Step 6 is either between operators affecting the same variable or between operators affecting a variable and its child
(with respect to the causal graph). In particular, if Ai < Aj **was added in Step 4 then either**
vi = vj or vi ∈ pred(vj ), whereas if Ai < Aj **was added in Step 6 then** vj ∈ pred(vi).

Assume, to the contrary that O implies Ai < Aj and Aj < Ai**. From the argument**
above, we know that there is a, possibly empty, path between vi and vj **in the undirected**
graph induced by the causal graph. By our structural assumption, we know that such an undirected path between vi and vj **is unique, and thus the situation is as follows: We have**
two chains of operators

$\alpha:A_{i}=A_{i_{0}}^{1}<\ldots<A_{i_{0}}^{x_{0}}<A_{i_{1}}^{1}<\ \ldots\ <A_{i_{1}}^{x_{1}}<\ldots\ldots<A_{i_{m}}^{1}<\ldots<A_{i_{m}}^{x_{m}}=A_{j}$  $\beta:A_{i}=\bar{A}_{i_{0}}^{1}>\ldots>\bar{A}_{i_{0}}^{y_{0}}>\bar{A}_{i_{1}}^{1}>\ \ldots\ >\bar{A}_{i_{1}}^{y_{1}}>\ldots\ldots>\bar{A}_{i_{m}}^{1}>\ldots>\bar{A}_{i_{m}}^{y_{m}}=A_{j}$
such that, for 0 ≤ k ≤ m, both xk ≥ 1 and yk ≥ **1. The corresponding unique undirected**
path between vi and vj is:

$$v_{i}=v_{i_{0}}\cdot v_{i_{1}}\cdot\ldots\cdot v_{i_{m-1}}\cdot v_{i_{m}}=v_{j}$$

Without loss of generality, the internal elements of α and β **are disjoint. Otherwise, if there**
is an operator B that belongs to the internal parts of both α and β **then we can reduce**
these chains and deduce Ai < B and Ai > B.

The proof of consistency is as follows:

(a) We prove that if such α and β **exist then at least one of them should have at least**
one internal element.
(b) We show some useful property of α and β**, that is exploited in (c).**
(c) We show that for 0 ≤ k ≤ m, A
xk ik and A¯yk ik are different except when x0 = y0 **= 1.**

Note that (a) together with (c) contradicts our assumption that A
t $\,A^{x_{m}}_{i_{m}}=\bar{A}^{y_{m}}_{i_{m}}$. 
.

(a) Assume, to the contrary, that both α and β **do not contain any internal elements.**
If so, then the algorithm actually adds to O ordering constraints Ai < Aj and Aj < Ai.

If vi and vj are the same variable then Ai < Aj **can only stem from Step 4 and only**
because Ai has the precondition of Aj as its effect. However, by definition of forwardcheck, Aj can not have the same role w.r.t. Ai and thus it is impossible that Aj < Ai was added to O. Alternatively, if viis a parent of vj then Ai < Aj **can stem only from Step 4**
because Ai has the prevail condition of Aj **as its effect. Suppose that** Ai = A(b j i
) and thus b j i ∈ prv(Aj ). In turn, Aj < Ai can be added only in Step 6 because Aj **has the precondition**
of Ai **as the prevail condition. But if** b j i ∈ prv(Aj **) then** Ai = A(w j i
), and this contradicts