Next we prove the correctness of MUSE AC-1.
Proof:
, and it is unsupported by all of the nodes
which immediately follow i in the DAG, then it cannot
participate in any MUSE arc consistent instance of MUSE CSP. In line
23 of Figure 24, if (i,j) is removed
from Local-Next-Support(i,a) set then [(i,j),a] must have been popped
off List. The removal of (i,j) from Local-Next-Support(i,a)
indicates that, in the segment containing i and j, is inadmissible.
It remains to be shown that [(i,j),a] is put on List
if is unsupported by every segment which
contains i and j. This is proven by induction on the number of
iterations of the while loop in Figure 23.
Base case: The initialization routine only puts [(i,j),a]
on List if is incompatible with every label in
(line 17 of Figure 22). Therefore, is unsupported by all segments containing i and j.
Induction step: Assume that at the start of the kth
iteration of the while loop all [(x,y),c] which have ever been put
on List indicate that 
is inadmissible in every
segment which contains x and y. It remains to show that during
the kth iteration, if [(i,j), a] is put on List, then is unsupported by every segment which contains i and j.
There are several ways in which a new [(i,j), a] can be put on List:
which were once compatible with have been eliminated. This item could have been placed on
List either during initialization (see line 17 in
Figure 22) or during a previous iteration of the while
loop (see line 6 in Figure
23)), just as in the CSP AC-4 algorithm.
It is obvious that, in this case, is
inadmissible in every segment containing i and j.
(see line 10 in Figure
24) indicating that is incompatible with
all nodes k for 
Prev-Edge 
. The only way for
[(i,j),a] to be placed on List for this reason (at line
11) is because all tuples of the form [(i,k),a] (where
Prev-Edge ) were already put on List. By the
induction hypothesis, these [(i,k), a] items were placed on the
List because is inadmissible in with all segments
containing i and k in the DAG. But if a is not supported by
any node which immediately precedes j in the DAG, then a is
unsupported by every segment which contains j. Therefore, it is
correct to put [(i,j), a] on List. (see line 4 in Figure
24) indicating that is incompatible with
all nodes k for 
Next-Edge . The only way for
[(i,j),a] to be placed on List (at line 5) for this
reason is because all tuples of the form [(i,k),a] (where Next-Edge ) were already put on List. By the induction
hypothesis, these [(i,k), a] items were placed on the List because
is inadmissible in all segments containing i and k
in the DAG. But if a is not supported by any node which
immediately follows j in the DAG, then a is inadmissible in
every segment which contains j. Therefore, it is correct to put
[(i,j), a] on List.
(see line 24 in
Figure 24) indicating that is incompatible with
all nodes k such that 
Next-Edge 
. The only
way for [(i,j),a] to be placed on List (at line
29) for this reason is because no node which
follows i in the DAG supports a, and so all pairs (i,k) have
been legally removed from Local-Next-Support(i,a) during previous
iterations. Because there is no segment containing i which supports
a, it follows that no segment containing i and j supports that
label. (see line 15 in
Figure 24) indicating that is incompatible with
all nodes k such that 
Prev-Edge . The only
way for [(i,j),a] to be placed on List (at line
20) for this reason is because no node which
precedes i in the DAG supports a, and so all pairs (i,k) have
been legally removed from Local-Prev-Support(i,a) during previous
iterations. Because there is no segment containing i which supports
a, it follows that no segment containing i and j supports that
label.
At the beginning of the (k+1)th iteration of the while loop, every [(x,y), c] on List implies that c is not supported by any segment which contains x and y. Therefore, by induction, it is true for all iterations of the while loop in Figure 23. Hence, if a label's local support sets become empty, that label cannot participate in a MUSE arc consistent instance of MUSE CSP.
by
the MUSE arc consistency algorithm, then
it must be MUSE arc consistent. For a to be MUSE arc consistent,
there must exist at least one path from start to end which
goes through node i such that all nodes n on that path contain at
least one label which is compatible with .
If a is not deleted after MUSE AC-1, then
Local-Next-Support 
and Local-Prev-Support .
Hence, i must be preceded and followed by at least one node which
supports ; otherwise, a would have been deleted.
As depicted in Figure 25, we know that there must be
some node j which precedes i such that, if it is not start,
it must
contain at least one label b which supports a, and
Next-Support[(i,j),a] and Prev-Support[(i,j),a] must be non-empty.
Similarly, there must be some node k which follows i such that, if
it is not end, it must
contain at least one label c which supports a, and
Next-Support[(i,k),a] and Prev-Support[(i,k),a] must be
non-empty.
Figure 25: If after MUSE AC-1, it must be preceded by
some node j and followed by some node k which support a.
To show there is a path through the DAG, we must show that there is a
path beginning at start which reaches i such that all the
nodes along that path support , and that there is a
path beginning at i which reaches end such that all the
nodes along that path support . We will show the
necessity of the path from i to end such that all nodes along
that path support given that a remains after MUSE
AC-1; the necessity of the path
from start to i can be shown in a similar way.
Base case: If after MUSE AC-1, then there must
exist at least one node which follows i, say k, such that
[(i,k),a] has never been placed on List. Hence,
for at least one 
and
Next-Support[(i,k),a] and Prev-Support[(i,k),a] must be
non-empty.
Induction Step: Assume that there is a path of n nodes that
follows i that supports , but none of those
nodes is the end node. This implies that each of
the n nodes contains at least one label compatible with a and that
Next-Support[(i,n),a] and Prev-Support[(i,n),a] must be non-empty
for each of the n nodes.
Next, we show that a path of length (n+1)
must also support ; otherwise, the label
a would have been deleted by MUSE AC-1. We have already noted that
for the nth node on the path in the induction step,
Next-Support[(i,n),a] must be non-empty; hence, there must exist at
least one node, say n', which follows the nth node in the path of
length n which supports . If n' is the end node, then
this is the case. If n' is not end, then the only way that
(i,n') can be a member of Next-Support[(i,n),a] is if [(i,n'),a]
has not been placed on List. If it hasn't, then 
for at least one 
and
Next-Support[(i,n'),a] and Prev-Support[(i,n'),a] must be
non-empty. If this were not the case, then (i,n') would have been
removed from Next-Support[(i,n),a], and n would no longer support
.
Hence, if after MUSE AC-1, then there must be a path of
nodes to end such that for each node n which is not the
end node,
for at least one 
and
Next-Support[(i,n),a] and Prev-Support[(i,n),a] must be
non-empty. Hence a is MUSE arc consistent.
From this theorem, we may conclude that MUSE AC-1 builds the largest MUSE arc consistent structure. Because MUSE arc consistency takes into account all of its segments, if a single CSP were selected from the MUSE CSP after MUSE arc consistency is enforced, CSP arc consistency could eliminate additional labels.