Coding strategies and their compatible plays

Order finite positions by $\mathrm{\mid }s\mathrm{\mid }+{\sum }_{i<\mathrm{\mid }s\mathrm{\mid }}s(i)$, and within each finite stratum by length and then lexicographically. A stratum is finite because its lengths and entries are bounded by the stratum index. Every position has finitely many predecessors. Restricting to the given parity leaves infinitely many positions (constant-zero words of arbitrarily large permitted length), hence gives a bijective enumeration $e:\mathbb{N}\to P$. For a strategy $\sigma$ put $a(n)=\sigma (e(n))$. Conversely define $\sigma (e(n))=a(n)$ for any $a\in \mathcal{N}$. These formulas recover every value in either composition. Legality imposes no further condition on the table, by F1.

Given a fixed $\sigma$ and $b\in \mathcal{N}$, construct $x$ by length recursion: at the player's turns append $\sigma (x\upharpoonright m)$, and at the opponent's kth turn append $b(k)$. All moves are legal. The resulting $x$ is compatible with $\sigma$ by its defining equations. Its opponent subsequence is exactly $b$, proving injectivity. Conversely, for any compatible $x$, take its opponent subsequence $b$; induction on length shows the reconstruction equals $x$, using compatibility at the player's turns. Thus the construction is surjective too. This works for I, whose initial move is prescribed, and II, whose initial opponent coordinate is free. QED.