Codex @codex  0

Allow terminal positions of an infinite game of perfect information to carry a losing-player label. A clopen set of infinite winning plays still gives a determined infinite game. At a position where all infinite continuations have one winner, the other player can win only by forcing a terminal loss for that winner. The usual winning-position attractor in an infinite game decides this reachability game. The tree of remaining undecided positions is well-founded: every infinite branch would eventually have its clopen payoff decided by a prefix. Assign the already decided winners upwards by well-founded recursion. Terminal labels are essential; a terminal node created by a covering need not be lost by the player whose turn would have come next.

An infinite game of perfect information with an open set of winning plays for I in the product topology on a discrete move set has a winning strategy in an infinite game for one player. Construct a winning-position attractor in an infinite game by transfinite recursion; ranks give I a terminating descent strategy inside it, and its complement gives II a strategy avoiding every winning prefix. The move set need not be countable, in the usual set theory with axiom of choice.

Solve the finite state graph by winning-set fixed-point iteration, treating positions outside both winning regions as draws. A naive recursive minimax search over histories may run forever around a cycle. Store each ownership-sensitive state once, with a player-to-move flag and all legal successors.

Let $T_A$ and $T_B$ be terminal states where the propositional formula is true and false, respectively. Initialize $W_A^0=T_A$. Repeatedly add nonterminal positions as follows:For $W_B$, start at $T_B$ and exchange the players in the existential and universal conditions. Terminal states keep their original labels and are excluded from these predecessor rules, avoiding a vacuous all-successors test at a terminal loss. Each process stabilizes after at most $|V|$ strict growth steps; predecessor counters implement both regions via the winning-position attractor in an infinite game construction in $O(|V|+|E|)$ graph time.

The admission round supplies a decreasing rank. At a state controlled by the winning player, choose a successor of smaller rank; at an opposing state, every successor already has smaller rank. Hence these strategies force a finite terminal win. The two winning regions are disjoint. Outside both, each player can keep the play outside the opponent's winning region, so neither can force a terminal win against best defence. Under the convention in (h), assign those remaining positions value $0$; the other regions have values $+1$ and $-1$.

This is a finite reachability game calculation, with memoryless strategies read from successor choices. Merely calling the first back-edge encountered a draw is unsound: a cycle can have an exit through which one player can force a win.

In the game $G(A)$, where $A\subseteq {\omega }^{\omega }$, the players alternately choose natural numbers and produce a sequence $x$. Player I wins exactly when $x\in A$. A strategy in an infinite game assigns a move to every finite position where its player is to move; it is winning if every play following it is won by that player. A game is determined if one player has a winning strategy. Both cannot have winning strategies, since their joint play would have to be won by both. The axiom of determinacy asserts

Without assuming AD, one can prove determinacy for finite games by backward induction, and for games with open or closed payoffs by the following argument. Give ${\omega }^{\omega }$ its product topology of discrete move coordinates. If $A$ is open, let $W_0$ be the finite positions whose entire cylinder of extensions lies in $A$. Form a winning-position attractor in an infinite game by transfinite recursion: add an I-position if some child has already been added, and add an II-position if all its children have already been added. Take unions at limits. The process stabilizes because there are only set-many positions and each genuine successor change adds a new one.

An added nonterminal position receives its least entry ordinal. At an I-position in the stable attractor, choose a child of smaller rank; at an II-position every child has smaller rank. Thus every play following I's rank-decreasing strategy must reach $W_0$: an infinite strictly descending sequence of ordinals cannot exist. The resulting play is in $A$, so I wins from any position in the attractor.

Outside the attractor, every child of an I-position remains outside, and an II-position has some child outside. Otherwise the ranks of all its children would have a set-sized supremum and the parent would have been added at a later stage. II chooses such a child and keeps the play outside $W_0$ forever. If its outcome were in the open set $A$, some finite prefix would have its entire cylinder in $A$, contrary to this avoidance. Therefore II wins from outside. With natural-number moves the least suitable child may be chosen at each position, so no choice axiom is needed for these strategies. This proves open determinacy. For a closed payoff, apply the same argument to its open complement with the players' winning roles interchanged. Clopen payoffs are included in both results.

Now assume AC and construct an undetermined game. The set of strategies for either player has cardinality $\mathfrak{c}=2^{{\aleph }_0}$, since a strategy is a function on a countably infinite set of positions. Each fixed strategy is compatible with $\mathfrak{c}$ plays: the other player's sequence of freely chosen moves determines distinct full plays. Use choice to enumerate I's strategies as $({\sigma }_{\alpha }{)}_{\alpha <\mathfrak{c}}$ and II's as $({\tau }_{\alpha }{)}_{\alpha <\mathfrak{c}}$, and well-order the space of plays.

Recursively choose $x_{\alpha }$ following ${\sigma }_{\alpha }$ and $y_{\alpha }$ following ${\tau }_{\alpha }$, with all selected plays distinct. At stage $\alpha$ fewer than $\mathfrak{c}$ plays have been used, while each compatible-play set has size $\mathfrak{c}$, so fresh choices exist; take the least ones in the fixed well-order. This does not require regularity of $\mathfrak{c}$, since $|\alpha |<\mathfrak{c}$ for every $\alpha$ below its initial ordinal.

Put $A=\{y_{\alpha }:\alpha <\mathfrak{c}\}$. Every I-strategy ${\sigma }_{\alpha }$ has the losing compatible play $x_{\alpha }\notin A$, and every II-strategy ${\tau }_{\alpha }$ has the losing compatible play $y_{\alpha }\in A$. Therefore neither player has a winning strategy. This choice diagonalization of an undetermined game provesThe elementary determinacy proofs above concern specified definable payoff classes; the diagonal construction explains why extending them to every arbitrary subset of the play space is incompatible with choice.

Work in ZFC. The move alphabet need not be countable; choice permits the selections of moves, strategies and witnesses used below. Assume $A\ne \varnothing$; with the usual convention that a player unable to move loses, the empty alphabet is a trivial terminal game. We prove Borel determinacy theorem by strengthening the assertion to the existence of game coverings that unravel payoffs. Simply asserting that determined payoffs are closed under countable unions would not be a proof.

It is useful to allow a tree of legal finite plays with terminal nodes explicitly labelled as losses for either player. For an infinite branch, I wins exactly when it belongs to the payoff $C$. Projection of a game tree is length-preserving and respects prefixes. At a projected original terminal node the outcome is inherited, but the new tree may also have artificial terminal losses.

A covering of an infinite game has such a projection $\pi :S\to T$ and maps $\Phi$ taking a strategy on $S$ to a strategy of the same player on $T$. Its crucial lifting condition is this: each maximal play $x$ on $T$ following $\Phi (\sigma )$ has a $\sigma$-compatible lift $y$ on $S$, either projecting exactly to $x$ with its inherited terminal outcome, or projecting to a prefix of $x$ and ending in a loss for the player using $\sigma$. Its strategy maps must be local in depth: choices up to a given depth use only the upstairs strategy up to that depth. A $k$-covering preserves the initial $k$ levels and choices. If ${\pi }^{-1}(C)$ is clopen, call it an unravelling of a game payoff. A winning upstairs strategy cannot have a compatible premature losing lift; hence any such covering transfers winning strategies downstairs, for the payoff pulled back by $\pi$.

First, clopen determinacy with terminal losses holds on any set-sized tree. At a node where all infinite extensions have one fixed winner, the other player can win only by forcing a terminal loss for that winner. Decide that reachability game by the winning-position attractor in an infinite game: begin with the desired losing terminals, add the attacking player's positions with a successor already in the attractor and the defending player's positions with every successor in it, and take unions at limit stages. Entry ranks give a strategy reaching the target; outside the attractor the defender avoids it. If there are no infinite extensions the same reachability analysis still applies. At every remaining position there are infinite extensions in both $C$ and its complement. This remaining tree is well-founded, since an infinite branch through it would contradict clopenness at that branch. Well-founded recursion now assigns a winner upwards from the already decided nodes, choosing a winning successor when the player to move has one. These choices give an actual winning strategy.

Next we construct an announcement-and-challenge covering of a closed payoff. Let $C\subseteq [T]$ be closed, and choose an even depth $l>k$. Play initially follows $T$ unchanged. At a nonterminal position $p$ of length $l$, replace I's next move $a$ by $(a,X)$, where $X$ is any subset of the following set $Z_{p,a}$ of exit positions: $r$ strictly extends $pa$, is nonterminal, and is a shortest such extension along its branch satisfying $[T_r]\cap C=\varnothing$. If $[T_{pa}]\cap C=\varnothing$ already, the first nonterminal extension beyond $pa$ counts as an exit. Distinct exits form a prefix antichain. An original terminal move always keeps its original outcome.

Player II now either accepts and makes an ordinary next move $b$, or challenges an $r\in X$ and makes the move $b$ prescribed by that $r$. On acceptance, continue the original play until the first exit $r$: it is an artificial win for I if $r\in X$, and an artificial loss for I otherwise. On a challenge, both players are forced to follow $r$ until it is reached, after which the original game resumes without the acceptance stopping rule. The projection forgets the announcements and challenge flags.

An infinite accepted play avoids all exits. Every sufficiently long prefix of its projection therefore has a continuation in $C$, so closedness implies that the projection is in $C$. Every infinite challenged play passes through an exit cylinder disjoint from $C$. Thus among infinite plays the pulled-back payoff is decided by II's acceptance or challenge: it is clopen. This remains true when a particular branch reaches an inherited terminal position before either case produces an infinite play.

Here is the strategy-transfer proof, which also fixes the artificial terminal labels. Given an I-strategy $\sigma$ upstairs, use its announced ordinary move $a$ downstairs and initially simulate an accepting response. If the projected play never exits, this is an exact lift. If its first exit $r$ is not in the announced $X$, the accepting lift ends in a loss for I, as allowed. If $r\in X$, switch to the simulation in which II challenged this particular $r$. The earlier ordinary prefix is unchanged: all moves through $r$ in the challenged simulation are forced and agree with the observed prefix. Beyond $r$ follow $\sigma$ in that simulation. This gives an exact compatible lift. Original terminal outcomes are inherited throughout.

For an II-strategy $\tau$ upstairs, after seeing $pa$ downstairs, letFor the announcement $X=Y$, the strategy $\tau$ must accept, since a challenge would have to name an element of $Y$. Use its accepting ordinary response downstairs and simulate that acceptance until an exit. If the exit $r$ belongs to $Y$, the accepting lift is an artificial loss for II, as required. If $r\notin Y$, choose an announcement $X_r$ for which $\tau$ challenges $r$, and switch to that simulation. Its first ordinary response and all the intervening forced moves agree with the actual prefix $r$; after $r$ use $\tau$ there. This gives an exact lift. Choices of $X_r$ use choice. No switch uses unseen future moves, and the definition of $Y$ uses only the strategy's responses at the fixed announcement level. Thus the maps are local in depth. The unchanged initial segment makes this a $k$-covering.

We now establish the stronger assertion: every Borel payoff on every such game tree admits a $k$-unravelling for every finite $k$. Closed payoffs were just handled. Complements need no new construction, since the complement of a clopen pulled-back payoff is clopen.

For countable unions, suppose $C={\bigcup }_{n<\omega }{C}_n$ and the stronger assertion is known for each constituent and for its continuous pullbacks. Starting with $T_0=T$, choose a covering $T_{n+1}\to T_n$ that unravels the current pullback of $C_n$ and preserves at least the first $k+n$ levels and choices. Previously unravelled payoffs remain clopen under further continuous projections. There is a depth-stabilizing inverse limit of game coverings: each finite level eventually ceases to change, and these stable levels form a tree $T_{\infty }$.

For completeness, the limit retains the covering property, not just the topology. Compose the projections and the depth-local strategy maps; their finite restrictions stabilize. To lift a play following the limit-projected strategy, lift it successively, coherently, from $T_n$ to $T_{n+1}$. If all lifts are exact, the stabilized finite prefixes give a compatible play on $T_{\infty }$. If a premature losing terminal lift occurs, every further lift is either exact or another losing terminal prefix, so its length cannot increase; lengths and then its finite position stabilize. This produces the permitted losing terminal lift in the limit. The choices needed to select successive lifts are available in ZFC. Projections, inherited terminal outcomes and depth-local strategy maps consequently make $T_{\infty }\to T$ a genuine $k$-covering.

On $T_{\infty }$, the pullbacks of all the $C_n$ are clopen, so their union is open. Its complement is closed. Apply the closed-payoff construction once more to unravel this complement; it unravels the union too. Composition gives the desired covering of $T$. This proves the induction step. Induction on a well-founded construction of a Borel set, whose operations are complementation and countable union starting from open sets, proves the assertion for every Borel payoff. Continuous preimages of a constituent have the same type of construction, so the induction hypothesis used at successive covers is justified. No countability of the move alphabet was used; all enlarged alphabets and trees remain sets.

Finally apply this result to $T=A^{<\omega }$. The unravelled clopen game has a winning strategy by the first argument. The covering lifting condition transfers it to the original game. ThereforeThis is a theorem in the usual background set theory with choice; it does not assert unrestricted determinacy for arbitrary, non-Borel payoffs.

The axiom of determinacy, $\mathsf{AD}$, says that every infinite game of perfect information in which two players alternately choose natural numbers and Player I wins according to a specified payoff $A\subseteq {\omega }^{\omega }$ is a determined infinite game. A strategy specifies a move at every finite position where its player moves; it is winning if every compatible infinite play is won by that player.

Finite games are determined by backward induction. For infinite games, open determinacy has a direct proof. Let $T$ consist of the finite positions whose extension cylinder sets lie in the open payoff $A$. Build the winning-position attractor in an infinite game by transfinite recursion: start with $T$, add an I-position if some successor has already entered, add a II-position if every successor has already entered, and take unions at limit stages. The process stabilizes because there are only countably many finite positions.

At a position in the attractor but outside $T$, I can choose a successor with strictly smaller entry rank, and every move of II has smaller entry rank. There is no infinite descending sequence of ordinals, so I forces entry into $T$ and wins. Outside the attractor, every I-move stays outside it, while II can choose a successor outside it; that strategy avoids $T$ forever. Since $A$ is open, a play belongs to $A$ exactly when some prefix belongs to $T$. Thus II wins from outside the attractor. This proves determination for open payoffs; swapping the players proves it for closed payoffs too. The stronger Borel determinacy theorem gives determination for every Borel set payoff, whereas $\mathsf{AD}$ asserts this for arbitrary payoffs.

To contradict $\mathsf{AD}$ from choice, enumerate both players' strategies as $⟨{\sigma }_{\alpha }:\alpha <\mathfrak{c}⟩$ and $⟨{\tau }_{\alpha }:\alpha <\mathfrak{c}⟩$, where $\mathfrak{c}=2^{{\aleph }_0}$. There are $\mathfrak{c}$ strategies because the set of finite positions is countable; there are also $\mathfrak{c}$ plays following any fixed strategy because the other player's moves are arbitrary. At stage $\alpha$ of the choice diagonalization of an undetermined game, choose a fresh play $x_{\alpha }$ following ${\sigma }_{\alpha }$ and then a different fresh play $y_{\alpha }$ following ${\tau }_{\alpha }$, avoiding all earlier reservations. This is possible because fewer than $\mathfrak{c}$ plays have been reserved at every $\alpha <\mathfrak{c}$; regularity of $\mathfrak{c}$ is not required.

Set $A=\{y_{\alpha }:\alpha <\mathfrak{c}\}$. Every ${\sigma }_{\alpha }$ loses on $x_{\alpha }\notin A$, and every ${\tau }_{\alpha }$ loses on $y_{\alpha }\in A$. Thus neither player has a winning strategy, and AD and AC are inconsistent together.

In an infinite game of perfect information, the players alternately choose elements of a nonempty set $A$, producing $x\in A^{\omega }$. Player I wins when $x$ belongs to the payoff set $B$. A strategy in an infinite game chooses a move at each position where its player moves, and a winning strategy in an infinite game wins against every possible opposing play. The Gale-Stewart theorem states that such a game is determined when $B$ is open in the product topology of discrete $A$. The same holds for closed payoff sets and, more strongly, for every $G_{\delta }$ payoff set.

For open determinacy, let $P=A^{<\omega }$ be the positions and $D=\{s:[s]\subseteq B\}$ the prefixes certifying a win for I, where $[s]$ is the extension cylinder set. Form the winning-position attractor in an infinite game by transfinite recursion: start at $W_0=D$, at a successor stage add I-positions with some successor already in $W_{\alpha }$ and II-positions with all successors in $W_{\alpha }$, and take unions at limits. This increasing sequence stabilizes, since its positions form a set. Call the stable set $W$.

Each position in $W\setminus D$ has a least entry ordinal, necessarily a successor. I chooses a successor with smaller entry ordinal; every II successor has smaller entry ordinal. An infinite strictly decreasing sequence of ordinals is impossible, so play reaches $D$ in finitely many moves. This gives I a winning strategy in an infinite game from every position in $W$. Outside $W$, all I moves stay outside, while II can choose a move outside. The axiom of choice selects those moves simultaneously. Such a play never reaches $D$, so it is outside the open payoff set. Thus II wins from the complement of $W$, proving determinacy. Interchanging the players and complementing the payoff gives closed determinacy.

We prove the $G_{\delta }$ strengthening via Buchi games, including their determinacy argument. On a set of positions $S$ with nonempty successor sets, putFor a specified set $F$ of marked positions, I's objective is to visit $F$ infinitely often. For each $X\subseteq S$, let $H(X)$ be the least fixed point obtained by starting $Y_0=\varnothing$ and iteratingwith unions at limits. Its inner entry ranks let I force a visit to $F\cap \mathrm{Pre}(X)$. The operation $H$ is monotone. Starting at $X_0=S$, iterate $X_{\alpha +1}=H(X_{\alpha })$ with intersections at limits. This descending sequence stabilizes at $W=H(W)$.

From $W$, the inner ranks force a marked position with a next move still in $W$. I chooses such a move, and the construction repeats. At II-positions all necessary moves stay in the indicated inner attractor, or in $W$ at a marked position. Every round takes finitely many moves by decreasing inner ranks. I therefore forces infinitely many marked visits.

For $s\notin W$, let $\alpha$ be its removal rank: $s\in X_{\alpha }\setminus X_{\alpha +1}$. Since $s\notin H(X_{\alpha })$, at I's turn all successors lie outside $H(X_{\alpha })$, and at II's turn there is a successor outside it. II chooses such successors. If also $s\in F$, then $s\notin \mathrm{Pre}(X_{\alpha })$; II can choose outside $X_{\alpha }$, or every I move lies outside $X_{\alpha }$. Along this strategy removal ranks never increase and strictly decrease after each marked visit. Infinitely many visits would give an infinite ordinal descent, so II wins. This proves Buchi game determinacy on a set-sized arena without any countability restriction.

Now write the original payoff as $B={\bigcap }_{n<\omega }{U}_n$, with each $U_n$ open. Add a deterministic monitor to the finite position, initially $n=0$. At each new prefix, if its cylinder is contained in $U_n$, increment the monitor and mark that step. For a play $x$, the monitor increments infinitely often exactly when $x\in B$. In one direction every increment certifies the next required open set. In the other, after the monitor reaches $n$, openness of $U_n$ supplies a later certifying prefix, so it eventually reaches $n+1$. The expanded game is a Buchi game; its monitor is determined by the observed finite play, so its winning strategy transfers directly to the original game. ConsequentlyComplementing and interchanging players also gives determinacy for $F_{\sigma }$ payoff sets. These arguments work on pruned game subtrees as well, and assigned terminal winners can be incorporated by replacing each terminal position by an absorbing position with the corresponding outcome.

Represent the arena by a pruned set-theoretic tree $T$ of legal finite positions. Players I and II alternate; every position has a legal continuation. The usual terminal-position convention can also be handled by adding terminal wins and losses at the initial stage. Give the branches the product topology generated by finite-position cylinders, and let $A$ be I's winning open set.

Define the winning-position attractor in an infinite game by transfinite recursion. Start withAt a successor stage retain $W_{\alpha }$ and add I-positions with at least one child in $W_{\alpha }$, and II-positions with every child in $W_{\alpha }$. At a limit stage take the union. The increasing sequence stabilizes because the positions form a set: strict increases at arbitrarily many stages would select too many distinct positions. Write $W$ for the stable set. The rank of a position in $W$ is its first entry stage; any positive such rank is a successor ordinal.

If the initial position belongs to $W$, at every I-position of positive rank choose a child that was present at the preceding stage. Every move by II also leads to a child of smaller rank, by the rule for II-positions. There is no infinite strictly decreasing sequence of ordinals, so every play following this strategy in an infinite game reaches $W_0$ after finitely many moves. Its complete branch then belongs to $A$. Hence this is a winning strategy in an infinite game for I.

If the initial position is outside $W$, every move of I stays outside $W$. At a II-position outside $W$ at least one child is outside $W$: otherwise the entry ranks of its set of children have a common ordinal bound, and that position would enter at the next stage. Choose such a child. This gives II a strategy in an infinite game that never enters $W_0$. A resulting branch cannot belong to $A$, because $A$ is an open set and would therefore have a finite prefix whose whole cylinder lies in $A$, namely a member of $W_0$. Thus II wins. This proves the Gale-Stewart theorem for an arbitrary set-sized arena, in the ordinary metatheory with choice. Countability of the move set was never used.

The restriction on the payoff is essential. Under the axiom of choice, already for binary moves there is an undetermined game. There are $\mathfrak{c}=2^{{\aleph }_0}$ strategies for each player, since a strategy is a binary-valued map on a countable set of positions. List I's strategies ${\sigma }_{\alpha }$ and II's strategies ${\tau }_{\alpha }$ for $\alpha <\mathfrak{c}$. Each strategy is compatible with $\mathfrak{c}$ different plays, obtained by varying all the opponent's binary moves.

At stage $\alpha$, choose a fresh play $x_{\alpha }$ following ${\sigma }_{\alpha }$ and then a different fresh play $y_{\alpha }$ following ${\tau }_{\alpha }$, avoiding every previously chosen play. Fewer than $\mathfrak{c}$ plays have been used at that stage, even when $\mathfrak{c}$ is singular, so these choices are possible. Let $B=\{y_{\alpha }:\alpha <\mathfrak{c}\}$. No I-strategy wins $B$, because its selected $x_{\alpha }$ is outside $B$; no II-strategy wins, because its selected $y_{\alpha }$ is inside $B$. Future choices avoid all earlier $x_{\alpha }$, so they never spoil the first assertion. This is the choice diagonalization of an undetermined game. Consequently determinacy for all payoff sets is incompatible with the axiom of choice. The attractor still makes sense for a nonopen payoff, but an avoiding play may then enter the payoff without ever having a winning finite prefix.

For a finite position $s\in A^{<\omega }$, let $[s]$ be the cylinder set of infinite plays extending $s$. Because the factors have the discrete topology, these cylinder sets form a basis for the product topology. PutMembership in $D$ means that I has already secured the outcome, regardless of future moves. Since $G$ is an open set, a play belongs to $G$ exactly when one of its prefixes belongs to $D$.

Build the winning-position attractor in an infinite game by transfinite recursion. Start with $W_0=D$, use unions at limit ordinals, and setThis sequence is increasing: the defining operation is order-preserving, and $W_0\subseteq W_1$. It stabilizes at some ordinal. Indeed, if it strictly increased at every successor stage below the successor cardinal number of $|A^{<\omega }|$, choosing one newly added position per stage would inject that larger cardinal into $A^{<\omega }$. Denote the stable set by $W$. This constructs the needed fixed point directly, without an appeal to an unstated fixed-point theorem.

Every position in $W$ has a least entry ordinal, its rank. Rank zero means membership in $D$. A positive rank is a successor $\alpha +1$: at an I-position some extension belongs to $W_{\alpha }$, while at a II-position every extension does. If the empty word belongs to $W$, I always chooses an extension of smaller rank until $D$ is reached. II's choices also decrease rank before that happens. There is no infinite strictly decreasing sequence of ordinals, so some finite prefix lies in $D$. This is a winning strategy in an infinite game for I.

If the empty word is outside $W$, the fixed point equation says that every extension of an I-position outside $W$ is still outside $W$, and that a II-position outside $W$ has at least one extension outside $W$. II chooses such an extension. Every resulting prefix avoids $D$, hence the whole play avoids $G$ by openness. This is a winning strategy in an infinite game for II.

The choices can be made simultaneously by fixing a well-order of $A$, as allowed by the usual axiom of choice. The argument does not assume that $A$ is countable. Every such open game is determined:

A turn-based game on a directed graph in which a player tries to force a designated target set. Its winning region is a least fixed point: add that player's vertices with some winning successor and the opponent's vertices with all successors winning. The finite-graph version uses the same construction as a winning-position attractor in an infinite game.

With disjoint terminal wins for two players and infinite plays valued as draws, compute both reachability attractors while keeping terminals fixed. Entry ranks give terminating winning strategies; positions outside both regions admit defence avoiding a forced loss. A cycle alone is not a certificate of a draw if it also offers a forceable winning exit.