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:

  b		round n (P's move)		b*
  	/		\
  round n+1: E-violating move by O				round 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'.

QED