Friday, June 24, 2011

Proof of BC #2

Proving the second bold conjecture from yesterday turned out to be straightforward:
Let s be a winning D-strategy for \phi, and b a branch in s where E is violated. Let b' be the result of truncating b immediately before the first violation of E (so that the new leaf of b' is a P node). Let s' be the result of doing this for every branch b where E is violated. Claim: s' is a winning E-strategy.
  • s' is an E-strategy: All moves which violate E have been removed. All other rules are unaffected by truncation:
    • D10: If P has asserted an atom p in round n of b', then he asserted it at round n of b, and since b followed D10, O's assertion of occurred at some earlier round m. Since m < n, O's assertion of p is in b', so D10 is respected.
    • D11, D12, D13: Straightforward.
  • s' is a winning E-strategy. Suppose b' in s' is such that P has not won. Either:
    1. The leaf of b' is a move by O, or
    2. The leaf of b' is a move by P, but there is a legal continuation of the branch according to E.
    (1) is not possible, by construction of s'. (2)Suppose that at the leaf (let it be round n) O has a legal move. Any move that is legal under E is also legal under D, which means that this move already appeared in s, in some branch b* which diverged from b at round n:
    bround n (P's move)b*
    round n+1: E-violating move by Oround n+1: E-non-violating move by O
    Since b' is in s', we know that b* was not truncated before round n. Hence, the result of cutting b off at round n+1 looks like this:
    round n (P's move)
    round n+1: E-non-violating move by O
    And hence, contra assumption, n is not a leaf in b'.

No comments:

Post a Comment