in line 4 is similar to the corresponding condition in *searchPCwit* and thus, if it is true, the search for PC-witness is correctly overriden. Regarding the second part, the failure means that no alternative PC-support for aiin D(xk) was found.

In more detail, the search for a PC-support starts from max(**LastP C**xi,ai,xk
+1, LastACxi,ai,xk
) or max(**LastP C**xi,ai,xk
+1, **LastAC**xi,ai,xk
+1), depending on the existence of **LastAC**xi,ai,xk
. This is correct since no ealier value can be a PCsupport. If there is no consistent (ai, ak) pair or *searchPCwit* returns *false* for all consistent pairs found, then ai has no PC-support in D(xk) and is thus correctly deleted.

Completeness. To prove the completeness of maxRPC3 we need to show that if a value is not maxRPC then the algorithm will delete it. The initialization function checks all values of all variables one by one in a brute-force manner and removes any value that is not maxRPC. Values that are maxRPC have their **LastP C** pointers set to the discovered PC-supports. Thereafter, the effects of such removals are propagated by calling Algorithm 1 and as a result new value deletions may occur. Now consider a value ai ∈ D(xi) that was not removed by the initialization function but after propagation is no longer maxRPC. This is either because of PC-support or PC-witness loss.

In the first case assume that xj is the variable in which ai no longer has a PCsupport. Since the previously found PC-support of ai has been deleted, xj must have been added to Q at some point. When xj is removed from Q all neighboring variables, including xi will be checked. Function *searchPCsup* will find that LastP Cxi,ai,xj is no longer valid and will search for a new PC-support concluding that there is none. Therefore, it will return *false* and ai will be deleted.

In the second case assume that the pair of values (ai,aj ), where aj is the last PC-support of aiin D(xj ), has lost its last PC-witness ak in variable xk. If LastP Cxi,ai,xj is not valid, which means that xj was added to Q, then we have the same case as above. Therefore, after xj is removed from Q, *searchPCsup* will find out that there is no PC-support for aiin D(xj ) and will delete it. If **LastP C**xi,ai,xj is valid then *searchPCsup* will return *true* (line 2). Since ak was deleted, xk was added to Q at some point. When xk is removed from Q all neighboring variables, including xi will be checked. If ai has no longer a PC-support in D(xk),
this will be detected by *searchPCsup* and ai will be deleted. Otherwise, function checkPCwit will be called. The for loop in line 1 will go through every variable constrained with both xi and xk, including xj . Since **LastP C**xi,ai,xj is valid, a new PC-witness for (ai,aj ) in D(xk) will be seeked (lines 3-11). Since ak was the last PC-witness, none will be found and as a result a new PC-support for ai in D(xj ) will be seeked (lines 13-24). Since aj was the last PC-support for aiin D(xj ), none will be found, *checkPCwit* will return *false*, and ai will be deleted.