PBCS@ wrote:a) If, in RS3, the left-linking or any t- or z- candidate of CSP-Variable Vp has been asserted, then Z and/or the previous Rk(’s) to which Lp is linked must have been eliminated by ECP in the passage from RS2 to RS3 (if it was not yet eliminated in RS2); if Z is among these eliminations, there remains nothing to prove; otherwise, the procedure has already been successfully terminated by case f of the first such k.

b) If, in RS3, left-linking candidate Lp has been eliminated (but not asserted) (it can therefore no longer be used as a left-linking candidate in a braid) and if CSPVariable Vp still has a z- or a t- candidate Cp, then replace Lp by Cp; now, up to Cp, B’ is a partial braid in RS3 with target Z. Notice that, even if Lp was linked to Rp-1 (as it would if B was a whip), this may not be the case for Cp; therefore trying to prove a similar theorem for whips would fail here (see section 5.10.3 for an example of non-confluence of the Wn theories). [As it missed this point, the proof given for zt-chains in HLS1 was not correct.]

c) If, in RS3, any t- or z- candidate of Vp has been eliminated (but not asserted), this has not changed the basic structure of B (at stage p). Continue with the same B’.

d) If, in RS3, right-linking candidate Rp has been asserted (p can therefore not be the last index of B’), it can no longer be used as an element of a braid, because it is no longer a candidate. Notice that all the left-linking and t- candidates for CSPVariables of B after p that were incompatible in B with Rp, i.e. linked to it, if still present in RS2, must have been eliminated by ECP somewhere between RS2 and RS3. But, considering the braid structure of B upwards from p, more eliminations and assertions must have been done by rules from BRT between RS2 and RS3. Let q be the smallest number strictly greater than p such that, in RS3, CSPVariable Vq still has a (left-linking, t- or z-) candidate Cq that is not linked to any of the Ri for p ≤ i < q (by definition of a braid, Cq is therefore linked to Z or to some Ri with i < p). Between RS2 and RS3, the following rules from BRT must have been applied for each of the CSP-Variables Vu of B with index u increasing from p+1 to q-1 included: eliminate its left-linking candidate (Lu) by ECP, assert its right-linking candidate (Ru) by S, eliminate by ECP all the left-linking and t-candidates for CSPVariables after u that were incompatible in B with the newly asserted candidate (Ru). In RS3, excise from B’ the part related to CSP-Variables p to q-1 (included) and (if Lq has been eliminated in the passage from RS1 to RS3) replace Lq by Cq; for each integer s ≥ p, decrease by q-p the index of CSP-Variable Vs and of its candidates in B’; in RS3, B’ is now, up to p (the ex q), a partial braid in Bn with target Z.

e) If, in RS3, left-linking candidate Lp has been eliminated (but not asserted) and if CSP-Variable Vp has no t- or z- candidate in RS3 (complementary to case b), then Vp has only one possible value in RS3, namely Rp; Rp must therefore have been asserted by S somewhere between RS1 and RS3; this case has therefore been dealt with by case d (because the assertion of Rp also entails the elimination of Lp).

f) If, in RS3, right-linking candidate Rp of B has been eliminated (but not asserted), in which case p cannot be the last index of B’, then replace B’ by its initial part: {L1 R1} – {L2 R2} – …. – {Lp .}. At this stage, B’ is in RS3 a shorter braid with target Z. Return B’ and stop.

Notice that the above proof works only because the notion of being linked does not depend on the resolution state.

Notice also that what we have proven is indeed the following: given RS1, B and RS2 as above, if RS3 is the resolution state obtained from RS2 by the repeated application of rules from BRT until quiescence, then: – either a contradiction has been detected by CD somewhere between RS2 and RS3 (and, due to consistency preservation between RS1 and RS2, it can only be because a contradiction inherent in the givens of P has been made manifest by CD); – or Z has been eliminated by ECP somewhere between RS2 and RS3; – or Z can be eliminated in RS3 by a braid B’ possibly shorter than B, with target Z, with CSP-Variables a sub-sequence W’ of those of B, with right-linking candidates those of B belonging to the sub-sequence W’, with left-linking candidates those of B belonging to the sub-sequence W’, each of them possibly replaced by a z- or t- candidate of B for the same CSP-Variable.

Does this mean that the B found in RS1 is the shortest? Also, is the search process of B all terminated by case f?