I am looking for references and hopefully enlightening proofs of the following statement(s) concerning the determinacy of not-necessarily-well-founded (i.e., possibly infinite, possibly loopy) combinatorial / perfect-information games:

Let $G$ be a directed graph and $x_0$ a vertex of $G$, and consider the game where two players, starting at $x_0$, take turn in choosing an out-neighbor of the current state, thus producing an oriented path $x_0,x_1,x_2,x_3,\ldots$ in $G$ (i.e., Alice chooses an edge from $x_0$ to $x_1$, then Bob from $x_1$ to $x_2$ then Alice from $x_2$ to $x_3$, etc.): the player who cannot play loses, whereas if the game is continued indefinitely then it is a draw.

Then exactly one of the following three statements holds:

the first player has a winning strategy,

the second player has a winning strategy,

both players have a surviving (i.e., non-losing) strategy.

Furthermore, if $\Phi\colon G \rightharpoonup \{\mathrm{P},\mathrm{N}\}$ is the least (for the partial order given by inclusion=restriction) partial function on $G$ with values in the 2-element set $\{\mathrm{P},\mathrm{N}\}$ such that

$\Phi(x) = \mathrm{P}$ iff for all all out-neighbors $y$ of $x$ the value $\Phi(y)$ is defined and is $\mathrm{N}$, and

$\Phi(y) = \mathrm{N}$ iff for all some out-neighbor $y$ of $x$ the value $\Phi(y)$ is defined and is $\mathrm{P}$,

(part of the statement is the fact that this least $\Phi$ is, indeed, well-defined; additionally, we can replace "iff" by "if" in both conditions above and the least $\Phi$ still exists and is the same),

—then the first player has a winning strategy starting from $x_0$ iff $\Phi(x_0) = \mathrm{N}$, the second has one iff $\Phi(x_0) = \mathrm{P}$, and both have a surviving strategy iff $\Phi(x_0)$ is undefined.

By "strategy" in the above I mean a positional strategy (i.e., one which decides the move to be taken in function of the state $x \in G$), but perhaps the equivalence with historical strategies (i.e., strategies which are allowed to depend on the past history) could be considered part of the statement.

These statements are not terribly difficult to prove, but the draws do complicate the matter somewhat in comparison to well-founded (=forward-finite, =terminating) graphs, where one player necessarily has a winning strategy (and $\Phi$ is defined by well-founded induction). The proofs I have found are unpleasantly messy.

So I am looking for precise references with hopefully enlightening proofs. By "enlightening", I mean that I am interested in knowing, for example, how much of the axiom of choice is needed to prove various (weaker, or classically equivalent) forms of the statement, whether the statements can be deduced from fixed point principles (e.g., the existence of $\Phi$ can be deduced from the (constructive) fixed point theorem 3.2 of this paper by Andrej Bauer and Peter LeFanu Lumsdaine), whether we need to mention ordinals, etc.

I am also interested in knowing the history of the above result (some people seem to attribute it to Zermelo, who proved that the game of chess satisfies a conclusion of this sort, but I don't know *exactly* what he proved).

More generally, any comments on the matter will be appreciated.