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) 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:
- The leaf of b' is a move by O, or
- The leaf of b' is a move by P, but there is a legal continuation of the branch according to E.
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:
b round n (P's move) b* / \ round n+1: E-violating move by O round n+1: E-non-violating move by O And hence, contra assumption, n is not a leaf in b'.
round n (P's move) | round n+1: E-non-violating move by O
Friday, June 24, 2011
Proof of BC #2
Proving the second bold conjecture from yesterday turned out to be straightforward: