Terminal reachability and residual positions

All strategies in all fixed-history subgames are subsets of a fixed set of position/move pairs. A1 selects legal default moves at all nonterminal positions, and a winning reachability strategy ${\sigma }_p$ for each $p\in W_P$, from its nonempty set of such strategies. A terminal position belongs to $W_P$ exactly when its label is taboo for $Q$: the already finished play is the only maximal play.

At a nonterminal $P$-position $p\in W_P$, the first move of ${\sigma }_p$ chooses a child $q$; restricting the strategy beyond that move proves $q\in W_P$. Conversely if a child $q\in W_P$ exists, choose that move and then follow ${\sigma }_q$, with defaults elsewhere. Every consistent maximal play then reaches a $Q$ taboo. Thus the some-child equivalence holds.

At a nonterminal $Q$-position $p\in W_P$, the opponent may choose any child; restricting ${\sigma }_p$ after each such choice shows every child belongs to $W_P$. Conversely, if every child belongs to $W_P$, after the opponent's first move to $q$ use the already selected ${\sigma }_q$. Each consistent play follows one fixed winning continuation and thus terminates at a $Q$ taboo. This proves the every-child equivalence, without requiring a uniform time bound.

If $p\in W_I\cap W_{II}$, follow the two respective winning strategies from the fixed history $p$. At each nonterminal stage the parity determines one prescribed legal move. Recursion F2, stopping at a terminal node if one occurs, yields a unique maximal play; if no terminal is reached, the union of its prefixes is an infinite branch. This play is consistent with both strategies, so each strategy forces it to terminate at a taboo for its opponent. A terminal cannot have both labels by F1. Hence the intersection is empty, and all assertions follow. QED.