Solution (source code)

= Solution

Let $S$ be the <causal rank-raising map on well-order codes> obtained by tagging a coded relation and adjoining a new least element. Player II follows the online rule $y=S(x)$. If $x\in\mathrm{WF}$, then
$$
y\in\mathrm{WF},
\qquad
\lVert y\rVert=\lVert x\rVert+1>\lVert x\rVert,
$$
so II wins. If $x\notin\mathrm{WF}$, the tagged recoding ensures $y\ne x$, which is again precisely II's winning condition. Therefore
$$
\boxed{\text{Player II has a winning strategy}.}
$$