Taboo games reduce to pruned residual games

A root in $W_P$ has a strategy reaching an opponent taboo, which wins for $P$ independently of $A$. Otherwise the root belongs to $S$, and the all-prefix definition makes $S$ prefix closed. A node of $S$ cannot be terminal in $T$, since each terminal is winning for the player opposite its label.

At $p\in S$, suppose $P$ is to move and $Q$ is the other player. No child is in $W_P$, since the some-child implication would put $p$ in $W_P$. Some child is outside $W_Q$, since otherwise the every-child implication would put $p$ in $W_Q$. This child avoids both sets, and all its earlier prefixes are prefixes of $p$; hence it belongs to $S$. Thus $S$ is pruned.

Let $\sigma$ win for $P$ on $S$. Follow it as long as play stays in $S$. If the opponent $Q$ first exits at child $q$ of $p\in S$, then $q\mathrm{\notin }{W}_Q$ by the some-child clause at the $Q$-position $p$. Since this is the first exit, the only failing prefix is $q$ itself, so $q\in W_P$. Switch to the fixed $P$ reachability strategy at $q$. A1 provides default legal moves after any first inconsistent own move, making the strategy total without affecting consistent plays.

A consistent play that exits therefore terminates at an opponent taboo. A consistent play that never exits cannot terminate by step 1.1, so is a branch of $S$; its payoff membership is unchanged by replacing $A$ with $A\cap [S]$, and $\sigma$ wins it. This proves the strategy transfer for either player.

A cylinder of $[T]$ restricts to the corresponding cylinder of $[S]$, so opens restrict to opens. Moreover $([T]\setminus B)\cap [S]=[S]\setminus (B\cap [S])$ and $({\bigcup }_n{B}_n)\cap [S]={\bigcup }_n(B_n\cap [S])$. Induction over any positive-rank complement/union expression therefore preserves its Borel level, at limits as well as successors. Applying the hypothesized pruned-tree determinacy and step 4.1 proves the taboo direction; the reverse takes a pruned tree with both taboo sets empty. QED.