§ INTRODUCTION

§ PRELIMINARIES

§ LOWER BOUNDS

§ OPEN OBJECTIVES

§ PREFIX-INDEPENDENT PI_2 OBJECTIVES

In this section, we show that step-counter strategies suffice for for objectives $\MPsupge$ and $\TPsupinf$.
In fact, we give a sufficient condition for when step-counter strategies suffice for in finitely branching games where the objectives are prefix-independent and in $\PiTwo$.

Recall that an objective is in $\PiTwo$ if it can be written as $\bigcap_{m\in\IN} \objective_m$ for some open objectives $\objective_m$.

Let $\objective = \bigcap_{m\in\IN} \objective_m \subseteq \colours^\omega$ be a prefix-independent $\PiTwo$ objective such that the objectives $\objective_m$ are open and step-monotonic.
Then, step-counter strategies suffice uniformly for $\objective$ over finitely branching arenas.

Let $\arena = \arenaFull$ be a finitely branching arena, and let $\vertex_0\in\vertices$ be an initial vertex.
Let $\winning \subseteq \vertices$ be the winning region of $\arena$ for $\objective$.
We assume that $\vertex_0$ is in the winning region $\winning$, and build a winning step-counter strategy from $\vertex_0$.

We build a winning step-counter strategy $\strat\colon \vertices_1 \times \IN\to \edges$ from $\vertex_0$ by induction on parameter $m$ used in the definition of $\objective=\bigcap_{m\in\IN} \objective_m$.
We consider the product arena $\arena \product \SC$, and fix a strategy for increasingly high step values.
The inductive scheme is as follows: for every $m\in\IN$, we fix $\strat$ on $\vertices_1 \times \{0,\ldots, k_m - 1\}$ for some step bound $k_m\in\IN$.
We ensure that

* along all histories from $\vertex_0$ consistent with $\strat$ of length at most $k_m$, the history does not leave $\winning$ (i.e., for all reachable $(\vertex, \step)$, we have $\vertex\in\winning$), and

* the open objectives $\objective_{m'}$ for $m'\le m$ are already satisfied within $k_m$ steps (i.e., any history of length $k_m$ consistent with $\strat$ only has winning continuations for $\objective_{m'}$).

For the base case, we may assume that we start the induction at $m = -1$ with $k_{-1} = 0$ and $\objective_{-1} = \colours^\omega$.
We indeed have that from $(\vertex_0, 0)$, the winning region is not left within $k_{-1} = 0$ step and that the open objective $\objective_{-1}$ is already satisfied.

Now, assume that for some $m\ge 0$, the above properties hold, so we have already fixed the moves of $\strat$ in $\arena\product\SC$ on $\vertices_1\times\{0,\ldots,k_m - 1\}$, yielding arena $(\arena \product \SC)_m$.
We first show that in arena $(\arena \product \SC)_m$ the vertex $(\vertex_0, 0)$ still belongs to the winning region.
We have assumed by induction that the winning region $\winning$ is not left within $k_m$ steps.
This means that for all $(\vertex, k_m)$ reachable from $(\vertex_0, 0)$ in $(\arena \product \SC)_m$, $\vertex$ is in $\winning$.
As $\objective$ is prefix-independent, no matter the history from $(\vertex_0, 0)$ to $(\vertex, k_m)$, there is still a winning strategy from $(\vertex, k_m)$ (recall that no choice for has been fixed beyond step $k_m$).
Hence, no matter how plays in the first $k_m$ steps, there is still a way to win for $\objective$ from $(\vertex_0, 0)$.

We therefore take an (arbitrary) winning strategy $\strat'_{m+1}$ of from $(\vertex_0, 0)$ in $(\arena \product \SC)_m$.
As $\strat'_{m+1}$ is winning for $\objective = \bigcap_{m\in\IN} \objective_m$, $\strat'_{m+1}$ wins in particular for the open $\objective_{m+1}$.
Since the arena is finitely branching and $\objective_{m+1}$ is open, applying <ref>, there is $k'_{m+1}\in\IN$ such that for all histories $\history'$ of length $\ge k'_{m+1}$ consistent with $\strat_{m+1}'$, $\history'$ already satisfies $\objective_{m+1}$ (i.e., $\col(\history')\colours^\omega \subseteq \objective_{m+1}$).
As $\objective_{m+1}$ is step-monotonic, by <ref>, there is a step-counter strategy $\strat_{m+1}$ such that for every history $\history$ from $(\vertex_0, 0)$ consistent with $\strat_{m+1}$, there is a history $\history'$ from $(\vertex_0, 0)$ consistent with $\strat'_{m+1}$ such that $\card{\history'} = \card{\history}$, $\too(\history') = \too(\history)$, and $\history' \prefixOrd_{\objective_{m+1}} \history$.

To ensure that we fix at least one extra step of the strategy in the inductive step, let $k_{m+1} = \max\{k'_{m+1}, k_m + 1\}$.
We extend the definition of $\strat$ to play the same moves as $\strat_{m+1}$ on $\vertices_1\times\{k_m, \ldots, k_{m+1} - 1\}$, which also defines $(\arena \product \SC)_{m+1}$.
We prove the two items of the inductive scheme.

First, $\strat$ still does not leave $\winning$ up to step $k_{m+1}$: indeed, for every history consistent with $\strat_{m+1}$, there is a history consistent with $\strat'_{m+1}$ reaching the same vertex.
Since $\strat'_{m+1}$ is winning and $\objective$ is prefix-independent, no such vertex can be outside of the winning region.

Second, strategy $\strat$ then guarantees $\objective_{m+1}$ within $k_{m+1}$ steps: after $k_{m+1}$ steps, every history consistent with $\strat_{m+1}$ is at least as good for $\prefixOrd_{\objective_{m+1}}$ as a history of length $k_{m+1}$ of $\strat'_{m+1}$.
But every history $\history'$ of length $k_{m+1}$ consistent with $\strat'$ is such that $\col(\history')\colours^\omega \subseteq \objective_{m+1}$, and therefore has only winning continuations.

This concludes the induction argument and shows the existence of a winning step-counter strategy from $\vertex_0$ as we iterate this process for $m\to\infty$.

We now know that for any vertex from the winning region, there is a winning step-counter strategy.
The existence of a uniformly winning step-counter strategy can be shown using prefix-independence of $\objective$; this part of the proof is standard and is detailed in <ref>.

This theorem applies to $\MPsupge$ and $\TPsupinf$ (see <ref> for a full proof).

Step-counter strategies suffice uniformly for $\MPsupge$ and $\TPsupinf$.

To illustrate <ref> further, we apply it to a non-quantitative objective.

Let $\colours$ be at most countable
and $\objective\subseteq\colours^\omega$ be the objective requiring that all colours are seen infinitely often (it is an intersection of Büchi conditions).
Formally, $\objective = \bigcap_{\clr\in\colours}\bigcap_{i\ge 1}\bigcup_{j\ge i} \left\{ \word = \clr_1\clr_2\ldots \in\colours^\omega\mid \clr_j = \clr\right\}$.
This objective is prefix-independent and in $\PiTwo$: it is the countable intersection of the open, step-monotonic objectives $\objective_{\clr, i} = \bigcup_{j\ge i} \left\{ \word = \clr_1\clr_2\ldots \in\colours^\omega\mid \clr_j = \clr\right\}$.
By <ref>, step-counter strategies suffice over finitely branching arenas for $\objective$.
This result is relatively tight: finite-memory strategies do not suffice over finitely branching arenas when $\colours$ is infinite, and step-counter strategies do not suffice over infinitely branching arenas when $\card{\colours} = 2$ (see <ref>, <ref> for details).

§ A NON-PREFIX-INDEPENDENT PI_2 OBJECTIVE

In this section, we consider objective
\TPsupge
= \bigcap_{m\ge 1} \bigcap_{i \ge 1} \bigcup_{j \ge i} \left\{\word \in \colours^\omega \mid \TP(\word_{\le j}) \ge \frac{-1}{m} \right\}
$ (in $\PiTwo$).
Its definition is very close to the one of $\MPsupge$ from the previous section, but one important difference is that it is not prefix-independent (for instance, $0^\omega\in\TPsupge$, but $-1,0^\omega\notin\TPsupge$).
Hence, <ref> does not apply.

As argued in <ref>, it turns out that step-counter strategies do not suffice for $\TPsupge$, even over finitely branching arenas.
We show a second example, only suited for this particular objective, illustrating more clearly the trade-off to consider to build simple winning strategies.

[node distance=1cm and 2.5cm, on grid]

[Min,initial,initial where=left] (v) at (0,0) $\vertex_0$;
[Min,right=1.2cm of v] (v0) $\vertex_1$;
[Max,right=of v0] (u0) $u_1$;
($(v0)!0.5!(u0)-(0,.5)$) node[Min,Imp] (v00) ;
[Max,right=of v0] (u0) $u_1$;
[Min,right=of u0] (v1) $\vertex_2$;
($(u0)!0.5!(v1)-(0,.5)$) node[Max,Imp] (u00) ;
[right=1.cm of v1] (dots) $\cdots$;
[Min,right=1.cm of dots] (vi) $\vertex_i$;
[Max,right=of vi] (ui) $u_i$;
($(vi)!0.5!(ui)-(0,.5)$) node[Min,Imp] (vi0) ;
[Min,right=of ui] (vi1) $\vertex_{i+1}$;
($(ui)!0.5!(vi1)-(0,.5)$) node[Max,Imp] (ui0) ;

(v) edge node[label,swap] $-1$ (v0);
(v0) edge[bend left=20,squish] node[label] $0$ (u0);
(v0) edge[bend right=15,squish] node[label,below left] $1$ (v00);
(v00) edge[squish,bend right=15] node[label,below] $-2$ (u0);
(u0) edge[bend left=20,squish] node[label] $0$ (v1);
(u0) edge[bend right=15,squish] node[label,below left] $1$ (u00);
(u00) edge[squish,bend right=15] node[label,below] $-2$ (v1);
(vi) edge[bend left=20,squish] node[label] $0$ (ui);
(vi) edge[squish,bend right=15] node[label,below left] $i$ (vi0);
(vi0) edge[squish,bend right=15] node[label,below] $-i-1$ (ui);
(ui) edge[bend left=20,squish] node[label] $0$ (vi1);
(ui) edge[squish,bend right=15] node[label,below left] $i$ (ui0);
(ui0) edge[squish,bend right=15] node[label,below] $-i-1$ (vi1);

Arena $\arena$ used in <ref>.
has a winning $1$-bit strategy for $\TPsupge$, but no winning step-counter strategy.

Consider the arena $\arena$ in <ref>.
We assume that a play starts in $\vertex_0$, hence reaching sum of weights $-1$ in $\vertex_1$.
We assume that a play is decomposed into rounds, where round $i$ corresponds to the choice of and in $\vertex_i$ and $u_i$ respectively.
At each round $i$, and then choose either $0$, or $i$ followed by $-i-1$.
As previously, we can assume that this arena only uses weights in $\colours = \{-1, 0, 1\}$, and that all histories from $\vertex_0$ reaching the same vertex have the same length.

has a winning strategy, consisting of playing “the opposite” of what just played: if played the sequence of $0$ (resp. $i, -i-1$), then replies with $i, -i-1$ (resp. the sequence of $0$).
This ensures that $(i)$ the current sum of weights in $\vertex_i$ is exactly $-i$ (it starts at $-1$ in $\vertex_1$ and decreases by $1$ at each round), and $(ii)$ the current sum of weights reaches exactly $0$ once during each round, after $i$ is played.
This shows that this strategy is winning for $\TPsupge$.
Such a strategy can be implemented with two memory states that simply remember the choice of at each round.

As all histories leading to vertices $u_i$ have the same length, a step-counter strategy cannot distinguish the choices of (<ref>).
Any step-counter strategy is losing:

* either only plays $0$, in which case wins by only playing $0$, thereby ensuring that the current sum of weights is $-1$ from $\vertex_1$ onwards;

* or plays $i, -i-1$ at some $u_i$.
In this case, wins by only playing $i, -i-1$.
This means that the sum of weights decreases by at least $1$ at every round, but decreases by $2$ in round $i$.
Hence, for $j\ge i$, the sum of weights at round $j$ is at most $-j-1$.
Such a sum can never go above $0$ again when a player plays $j, -j-1$.

This example shows that in general, there is a trade-off between “obtaining a high value for a short time, to go above $0$ temporarily” and “playing safe in order not to decrease the value too much”.
Two memory states sufficed: if the opponent just saw a high sum of weights ($\ge 0$), then we can play it safe temporarily; if the opponent played it safe, we may need to aim for a high value, even if the overall sum decreases.
This reasoning generalises to all finitely branching arenas: in general, step-counter + $1$-bit strategies suffice for $\TPsupge$.

Step-counter + $1$-bit strategies suffice for $\TPsupge$ over finitely branching arenas.

We provide a proof sketch here (full proof in <ref>).
It follows the same scheme as the proof of <ref>, where we inductively fix choices for ever longer histories.
However, we need to be more careful not to leave the winning region.
As the objective is not prefix-independent, the winning region $\winningExtended$ is described not just by a set of vertices, but by pairs of a vertex and current total payoff (i.e., the current sum of weights), i.e, $\winningExtended \subseteq \vertices \times \IQ$.

We start with a lemma about the sufficiency of memoryless strategies to stay in this winning region.
Staying in $\winningExtended$ is necessary but not sufficient to win for $\TPsupge$.

Let $\arena = \arenaFull$ be a finitely branching arena.
There exists a memoryless strategy $\strat_{\mathsf{safe}}$ of in $\arena$ such that, for every $(\vertex_0, \reward)\in\winningExtended$, $\strat_{\mathsf{safe}}$ never leaves $\winningExtended$ from $\vertex_0$ with initial weight value $\reward$.

The following lemma is an analogue of <ref>, but ensures a stronger property with a more complex memory structure (using an extra bit).
It says that locally, with a step-counter + $1$-bit strategy, we can guarantee a high value temporarily while staying in the winning region $\winningExtended$, generalising the phenomenon of <ref>. The bit is used to aim for a high value (bit value $0$) or stay in the winning region (bit value $1$) by playing $\strat_{\mathsf{safe}}$ from <ref>.

We use a rewriting of $\TPsupge$: observe that

\begin{align}
\TPsupge = \bigcap_{m\ge 1} \bigcup_{j \ge m} \left\{\word \in \colours^\omega \mid \TP(\word_{\le j}) \ge \frac{-1}{m} \right\}, \label{eq:TPsupge}
\end{align}

where the variable $m$ is used both for the $-\frac{1}{m}$ lower bound and for the $m$ lower bound on the step count.
Indeed, this also enforces that, for arbitrarily long prefixes, the current total payoff goes above values arbitrarily close to $0$.
For $m\ge 1$, let $\objective_m = \bigcup_{j \ge m} \{\word \mid \TP(\word_{\le j}) \ge \frac{-1}{m} \}$ be the open set used in the definition of $\TPsupge$ in (<ref>).

Let $\arena = \arenaFull$ be an arena and $\vertex_0\in\vertices$ be an initial vertex in the winning region of for $\TPsupge$.
For all $m\ge 1$, there exists a step-counter + $1$-bit strategy $\strat_m$ such that $\strat_m$ is winning for $\objective_m$ from $\vertex_0$ and never leaves $\winningExtended$ (i.e., for all histories $\history$ from $\vertex_0$ consistent with $\strat_m$, $(\too(\history), \TP(\history))\in\winningExtended$).

The inductive scheme used in the proof of <ref> is similar to that of <ref>, building a step-counter + 1-bit strategy $\strat\colon \vertices_1 \times \IN \times \{0, 1\} \to \edges$.

For $\memory$ a step-counter and $1$-bit memory structure, consider the product arena $\arena' = \arena\product \memory$ (in which the bit updates are not fixed yet, and will be fixed inductively).
We have that $(\vertex_0, (0, 0))$ is in the winning region of $\arena'$.
The inductive scheme is as follows: for infinitely many $m\in\IN$, for some step bound $k_m\in\IN$, we fix $\strat$ on $\vertices_1 \times \{0,\ldots, k_m - 1\} \times \{0, 1\}$, yielding arena $\arena'_m$.
Using <ref>, we ensure that

* along all histories $\history$ from $\vertex_0$ consistent with $\strat$ of length at most $k_m$, $\winningExtended$ is not left, and

* the open objective $\objective_{m}$ is already satisfied within $k_m$ steps (i.e., any history of length $k_m$ consistent with $\strat$ only has winning continuations for $\objective_{m}$).

Iterating this procedure defines a step-counter + $1$-bit strategy $\strat$ that satisfies $\objective_m$ for infinitely many $m\ge 1$.
Since the sequence $(\objective_m)_{m\ge 1}$ is decreasing ($\objective_1 \supseteq \objective_2 \supseteq \ldots$), we have that $\strat$ is winning for $\objective_m$ for all $m\ge 1$.
Hence, $\strat$ is winning for $\TPsupge$.

Unlike for <ref>, the upper bound in this section does not apply uniformly in general (an arena illustrating this is in <ref>, <ref>).

Over integer weights ($\colours\subseteq\IZ$), $\TPsupg = \overline{\TP}_{\ge 1} \in \PiTwo$.
As $\overline{\TP}_{\ge 1}$ behaves like $\TPsupge$ (<ref>), the results from this section apply to $\TPsupg$ over integer weights.
Up to some scaling factor, this also applies to rational weights with bounded denominators.
However, for general rational weights, $\TPsupg$ can only be shown to be in $\SigmaThree$, so the above does not apply.

§ CONCLUSION

We established whether step-counter strategies (possibly with finite memory) suffice for the objectives $\MPsupge$, $\TPinfg$, $\TPinfge$, $\TPsupinf$, and $\TPsupge$.
We used the structure of these objectives as sets in the Borel hierarchy, and pinpointed the strategy complexity for all classical quantitative objectives on the second level of Borel hierarchy.
This leaves open the cases of $\MPsupg$, $\MPinfge$, $\TPsupg$ (over $\IQ$), and $\TPinfinf$, all on the third level.
The sufficiency of other less common infinite memory structures, such as reward counters <cit.>, could also be investigated.

§ MISSING PROOFS FOR SECTION <REF>

We give formal proofs of <ref>.

Let $\arena_1$, depicted in <ref>, be the arena with three vertices, $s$ controlled by and $t,q$ controlled by , with weights $\colours=\IZ$ and edges $E = (\{s\}\x(-\N)\x\{t\}) \cup (\{t\}\x\N\x\{q\})\cup \{(q,0,q)\}$. In this arena, has a strategy to win for any total-payoff objective with threshold $0$: given the choice of $-i$ by , can respond with $i+1$, thus winning for $\TPinfg$, $\TPinfge$, $\TPsupg$, and $\TPsupge$.
Notice that, at $t$, the step-counter value is always $1$, providing no useful information.
Consider any finite-memory strategy of . There must be a maximum number $k$ chosen by this strategy at $t$, against any possible choices of . Against such a strategy, wins by playing $-k-1$.

We now show the claim for $\MPsupg$, $\MPsupge$, and $\TPsupinf$. Consider $\arena_1'$ (see <ref>), which repeats the process of $\arena_1$. Vertices $t$ and $s$ are controlled by and respectively, with weights $\colours=\IZ$ and edges $E = (\{s\}\x(-\N)\x\{t\}) \cup (\{t\}\x\N\x\{s\})$.
That is, the structure enforces strict alternation and each step has an arbitrary finite weight.

Notice that regardless of the players' choices, the number of steps up to round $i$ is always $2i$.
Every strategy based on a step counter and finite memory thus defines a function $f\colon\N\to\N$ where $f(i)$ denotes the maximum number chosen in round $i$. can counter such a strategy by always picking $-f(i) - 1$ in round $i$ and thereby ensure a mean payoff $\le -\frac{1}{2}$ and a total payoff of $-\infty$.

By induction on $k$.
We show that the length of any path from $s_0$ to $t_k$ is $3(k+1)$.
For $k=0$, there is only one path of length $3=3(k+1)$.
For $k+1$, the “direct” path $s_0\hops s_{k+1}\to t_{k+1}$ evidently has the stated length: $k+1$ steps to reach $s_{k+1}$ then $2(k+1)+3$ steps down to $t_{k+1}$.
Consider any other path $s_0\hops t_{j}\hops t_{k+1}$
with $j<k+1$ maximal, i.e., the suffix $t_j\hops t_{k+1}$
went through the delay gadget from $t_j$. By induction hypothesis, the prefix up to vertex $t_j$ has length $l_1 = 3(j+1)$. The suffix from $t_j\to t_j^1\hops t_j^{k+1-j}\to t_{k+1}$ has length
$l_2=(k+1-j) + 2(k+1-j)$.
The total length of the path is thus $l_1+l_2 = 3(j+1) + 3(k+1-j) = 3(k+2)$ as required.

§ MISSING PROOFS FOR SECTION <REF>

In this section, we prove <ref>.

Let $\strat$ be a strategy winning from $\vertex_0$ for $\objective$.
Let $T_\strat$ be the set of all histories $\history$ from $\vertex_0$ consistent with $\strat$ such that $\col(\history)\colours^\omega \not\subseteq \objective$.
We have that $T_\strat$ is a tree, since if $\col(\history)\colours^\omega \subseteq \objective$, then for $\history'$ a longer history with $\history$ as a prefix, we also have $\col(\history')\colours^\omega \subseteq \objective$.

Assume that, for all $\step\in\IN$, there is $\history$ of length $\ge \step$ such that $\col(\history)\colours^\omega \not\subseteq \objective$.
Then, $T_\strat$ is an infinite tree.
By Kőnig's lemma, this tree has an infinite branch.
Hence, there is an infinite play $\play$ consistent with $\strat$ such that all finite prefixes $\history$ of $\play$ are such that $\col(\history)\colours^\omega \not\subseteq \objective$.
As $\objective$ is open, this means that $\col(\play) \not\in\objective$, so $\strat$ is not winning from $\vertex_0$.

We define $\strat\colon \vertices_1 \times \IN \to \edges$ and prove the required property on $\strat$ by induction on $\IN$.
The property is trivially true for histories of length $0$ (i.e., just fixing an initial vertex).

We assume that $\strat$ has been defined on $\vertices_1 \times \{0, \ldots, \step - 1\}$ for some $\step \ge 0$, and that the property holds for histories up to length $\step$.
We define $\strat$ on histories of length $\step$ and prove the properties on histories of length $\step + 1$ at the same time.

Let $\history$ be any history from $\vertex_0$ consistent with $\strat$ of length $\step$.
Let $\vertex = \too(\history)$.
By induction hypothesis, there is a history $\history'$ from $\vertex_0$ consistent with $\strat'$ such that $\card{\history'} = \step$, $\too(\history') = \vertex$, and $\history' \prefixOrd_\objective \history$.

If $\vertex\in\vertices_2$, we consider any outgoing edge $\edge$ of $\vertex$ (which could be a move played by after $\history$).
The history $\history\edge$ has length $\step+1$ and is consistent with $\strat$.
Since $\history'$ also ends in $\vertex\in\vertices_2$, the history $\history'\edge$ is also consistent with $\strat'$.
As we had $\history' \prefixOrd_\objective \history$, we also have $\history'\edge \prefixOrd_\objective \history\edge$ (using that $\prefixOrd_\objective$ is a congruence).
Hence, history $\history'\edge$ satisfies all the required properties: it is consistent with $\strat'$, it is of length $\step+1$, it ends in $\too(\history\edge)$, and it is such that $\history'\edge \prefixOrd_\objective \history\edge$.

If $\vertex\in\vertices_1$, we need to define $\strat(\vertex, \step)$ to see how history $\history$ is extended.
For $\vertex_1\in\vertices$, we define a history $\history_{\vertex, \step}'$ as one of the elements of

\[
\min_{\prefixOrd_\objective}
\{\history''\in\histories(\arena) \mid \text{$\history''$ is consistent with $\strat'$, $\from(\history'') = \vertex_0$, $\card{\history''} = \step$, and $\too(\history'') = \vertex$}\}.
\]

The set being minimised over is non-empty, as $\history'$ is in it.
It is also finite, as $\arena$ is finitely branching and there are therefore only finitely many histories of fixed length from $\vertex_0$.
Moreover, a minimum exists as all histories of the same length are comparable for $\prefixOrd_\objective$ due to step-monotonicity.
Since $\prefixOrd_\objective$ is a preorder, there may be multiple histories that are minimal but equivalent with respect to $\prefixOrd_\objective$, in which case we can pick any of them.

We define $\strat(\vertex, \step) = \strat'(\history_{\vertex, \step}')$.
Let $\history\edge$ be the one-move continuation of $\history$, where $\edge = \strat(\vertex, \step)$.
We have that $\history_{\vertex, \step}'\edge$ is consistent with $\strat'$, and satisfies $\card{\history_{\vertex, \step}'\edge} = \card{\history\edge}$ and $\too(\history_{\vertex, \step}'\edge) = \too(\history\edge)$.
Moreover, we had $\history'\prefixOrd_\objective \history$ (by the induction hypothesis) and we have $\history_{\vertex, \step}' \prefixOrd_\objective \history'$ by the choice of minimum.
Therefore, $\history_{\vertex, \step}' \prefixOrd_\objective\history$, so $\history_{\vertex, \step}'\edge \prefixOrd_\objective \history\edge$, which ends the proof.

§ UNIFORMLY WINNING STRATEGIES

In this section, we prove that winning step-counter strategies can be “uniformised” for prefix-independent objectives.
This result easily follows from the following known result <cit.> on the uniformisation of memoryless strategies for prefix-independent objectives.
We rephrase this lemma with our notations.
This result was originally stated for both players at the same time, but its proof applies to one player at a time.

Let $\objective$ be a prefix-independent objective, and $\arena = \arenaFull$ be an arena.
If, for all $\vertex\in\winning$ in the winning region of , there is a winning memoryless strategy from $\vertex$, then has a uniformly winning memoryless strategy in $\arena$.

We obtain a similar result for step-counter strategies by reducing to the memoryless case through the construction of the product arena $\arena \product \SC$.

Let $\objective$ be a prefix-independent objective and $\arena = \arenaFull$ be an arena in which, from every $\vertex\in\winning$ of the winning region of , has a winning step-counter strategy.
Then has a uniformly winning step-counter strategy.

Consider the product arena $\arena \product \SC$.
The fact that, from every vertex $\vertex\in\winning$, has a winning step-counter strategy is equivalent to the fact that, from every $(\vertex, 0)$ in $\arena \product \SC$ for $\vertex\in\winning$, has a winning memoryless strategy.
The proof of this equivalence is standard; full details can be found in <cit.>.

As $\objective$ is prefix-independent, we can apply <ref> to arena $\arena\product\SC$ and find a memoryless strategy $\strat$ of that wins from all vertices in the winning region of $\arena\product\SC$.
In particular, it wins from all vertices $(\vertex, 0)$ with $\vertex\in\winning$.
Going back to $\arena$, we find that there is a step-counter strategy that wins from all $\vertex\in\winning$.

§ MISSING DETAILS FOR SECTION <REF>

We prove <ref>.

Let $\colours = \IQ$.
Recall that both $\MPsupge$ and $\TPsupinf$ are prefix-independent.

We first focus on $\MPsupge$.
A natural way to write $\MPsupge$ as a $\PiTwo$ objective, starting from its definition, is as the set of infinite words that have infinitely many finite prefixes with mean payoff above $\frac{-1}{m}$ for all $m\ge 1$. Formally,

\[
\MPsupge = \bigcap_{m\ge 1} \bigcap_{i \ge 1} \bigcup_{j \ge i} \left\{\word \in\colours^\omega\mid \MP(\word_{\le j}) \ge \frac{-1}{m}\right\}.
\]

For $m, i\ge 1$, let $\objective_{m, i} = \bigcup_{j \ge i} \{\word \mid \MP(\word_{\le j}) \ge \frac{-1}{m}\}$.
Such sets are open, as whether a word belongs to it is witnessed by a finite prefix.
Observe that the objectives $\objective_{m, i}$ are also step-monotonic. Indeed, if we consider two finite words of the same length, either one has already satisfied $\objective_{m, i}$, or the one with the greatest current mean payoff has more winning continuations than the other (a similar reasoning was used in <ref>).

Therefore, $\MPsupge$ is the countable intersection of open, step-monotonic objectives.
By <ref>, we conclude that a step counter suffices for $\MPsupge$ in finitely branching arenas.

The claim for $\TPsupinf$ can be shown analogously: observe that

\[
\TPsupinf
= \bigcap_{m\ge 1} \bigcap_{i \ge 1} \bigcup_{j \ge i} \left\{\word\in\colours^\omega \mid \TP(\word_{\le j}) \ge m \right\}
\]

is in $\PiTwo$ and fix $\objective_{m, i} = \bigcup_{j \ge i} \left\{\word\in\colours^\omega \mid \TP(\word_{\le j}) \ge m \right\}$.

The $\objective_{\clr, i}$ are open because whether an infinite word is in such an objective is witnessed by a finite prefix of the word.
Also, the objectives $\objective_{\clr, i}$ are step-monotonic: if we take two finite words of the same length, either one already satisfies the objective (in which case, this word is larger for $\prefixOrd_{\objective_{\clr, i}}$), or none of the words has already satisfied the objective, in which case both words have exactly the same winning continuations.

We show that finite-memory strategies do not suffice over finitely branching arenas when $\colours$ is infinite: consider the arena in <ref>.
In this arena, can see all colours infinitely often, but any finite-memory strategy either only stays on the top horizontal line, or never goes beyond some $\clr_i$.

We show that step-counter strategies do not suffice over infinitely branching arenas when $\card{\colours} = 2$: consider the arena in <ref>.
Clearly, wins by playing $\clr_2$ followed by $\clr_1$ every time the play reaches $v$.
However, using only a step-counter strategy $\strat$, there needs to be infinitely many $\step$ such that $\strat(v, \step) = (v, \clr_2, v)$ and infinitely many $\step$ such that $\strat(v, \step) = (v, \clr_1, u)$.
For any given step-counter strategy, can therefore have a winning counterstrategy by ensuring that the play reaches $v$ only in those steps where plays $(v, \clr_1, u)$ immediately.

With $\colours = \{\clr_1, \clr_2, \ldots\}$, arena in which wins for $\objective$ but finite memory is insufficient to do so.

With $\colours = \{\clr_1, \clr_2\}$, arena in which wins for $\objective$ but a step counter is insufficient to do so.
The arrow with label $\clr_1^+$ indicates that can choose any word in language $\clr_1^+$.

Arenas illustrating that memory is insufficient for objective $\objective$ in <ref>.

§ MISSING PROOFS FOR SECTION <REF>

This section is dedicated to the proof of <ref>.

For an arena $\arena = \arenaFull$, let $\winningExtended \subseteq \vertices \times \IQ$ be the set of pairs $(\vertex, \reward)$ such that there is a winning strategy from $\vertex$ for $\TPsupge$, assuming the current sum of weights is $\reward$.
Formally, $(\vertex, \reward)\in\winning'$ if there is a strategy $\strat$ such that for all plays $\play$ consistent with $\strat$, $\reward + \limsup_j(\TP(\col(\play)_{\le j})) \ge 0$.
For example, in <ref> (<ref>), we have $(\vertex_i, -i)\in\winningExtended$, but $(\vertex_i, -i-1)\notin\winningExtended$.
We say that a strategy never leaves $\winningExtended$ from $\vertex_0$ with initial weight value $r$ if for all histories $\history$ from $\vertex_0$ consistent with the strategy, $(\too(\history), r + \TP(\history))\in\winningExtended$.

We start by proving <ref> about the sufficiency of memoryless strategies to stay in this winning region.
Note that staying in $\winningExtended$ is necessary but not sufficient for a strategy to be winning for $\TPsupge$.

We define a memoryless strategy $\strat_{\mathsf{safe}}\colon \vertices_1 \to \edges$ with the required properties.
Let $\vertex\in\vertices_1$.
Assume that the set $R_\vertex = \{\reward\in\IQ \mid (\vertex, \reward)\in\winningExtended\}$ is not empty (if it is, we define $\strat(\vertex)$ arbitrarily).
Notice that $R_\vertex$ is upwards closed (i.e., if $\reward\in R_\vertex$ and $\reward' \ge \reward$, then $\reward'\in R_\vertex$).
Let $r_v = \inf R_v$.
If $r_v\in R_v$, there exists a strategy $\sigma^v$ that wins for $\TPsupge$ from $\vertex$ with current weight value $r_v$; we fix $\strat_{\mathsf{safe}}(\vertex) = \strat^v(\emptyHistory_\vertex)$ (we recall that $\emptyHistory_\vertex$ is the empty history from $\vertex$).
If $r_v\notin R_v$, for every $n \ge 1$, as $(\vertex, r_v + \frac{1}{n})\in\winningExtended$, there exists a strategy $\sigma_n^v$ that wins for $\TPsupge$ from $\vertex$ with current weight value $r_v + \frac{1}{n}$.
Consider the infinite sequence of edges $\strat_1^v(\emptyHistory_\vertex), \strat_2^v(\emptyHistory_\vertex), \ldots$; as $\arena$ is finitely branching, one of the edges outgoing from $\vertex$ appears infinitely often along this sequence.
We define $\strat_{\mathsf{safe}}(\vertex)$ to be such an edge.

We now show that $\strat_{\mathsf{safe}}$ satisfies the property from the statement.
Let $(\vertex_0, r)\in\winningExtended$.
Let $\history$ be a history from $\vertex_0$ consistent with $\strat_{\mathsf{safe}}$.
We show by induction on the length of $\history$ that $\reward + \TP(\history) \in R_{\too(\history)}$.
For the base case, we have that $\reward \in R_{\vertex_0}$.

Assume now that $\history\edge$ is a history from $\vertex_0$ consistent with $\strat_{\mathsf{safe}}$ of length $\card{\history} + 1$ and that $\reward + \TP(\history) \in R_{\too(\history)}$.
We have that $\inf R_{\too(\history)} \le \reward + \TP(\history)$.
If $\inf R_{\too(\history)} \in R_{\too(\history)}$, then $\inf R_{\too(\history)} + \col(\edge) \in R_{\too(\edge)}$ by definition of $\strat_{\mathsf{safe}}(\too(\history))$, so $\reward + \TP(\history\edge) \in R_{\too(\edge)}$ (as $R_{\too(\edge)}$ is upwards closed).
If $\inf R_{\too(\history)} \notin R_{\too(\history)}$, then $\inf R_{\too(\history)} < \reward + \TP(\history)$.
So we can find $n\in\IN$ such that $\inf R_{\too(\history)} + \frac{1}{n} \le \reward + \TP(\history)$ and such that $\strat_{\mathsf{safe}}(\too(\history)) = \strat^{\too(\history)}_n(\history_{\too(\history)})$.
With a similar observation as the previous case, we obtain that $\reward + \TP(\history\edge) \in R_{\too(\edge)}$.

<ref> is an analogue of <ref>, but ensures a stronger property with a more complex memory structure (using an extra bit).
It says that locally, with a step-counter + $1$-bit strategy, we can guarantee a high value temporarily while staying in the winning region $\winningExtended$.
It generalises the phenomenon of <ref>, in which we observed that $1$ bit is exactly what we need to either stay in the winning region or aim for a high value.
We will later use it in the induction step in the proof of <ref>.

As explained in <ref>, we recall that

\begin{align*}
\TPsupge = \bigcap_{m\ge 1} \bigcup_{j \ge m} \left\{\word \in \colours^\omega \mid \TP(\word_{\le j}) \ge \frac{-1}{m} \right\},
\end{align*}

and that for $m\ge 1$, we let $\objective_m = \bigcup_{j \ge m} \{\word \mid \TP(\word_{\le j}) \ge \frac{-1}{m} \}$.
To better understand $\prefixOrd_{\objective_m}$, recall that as in <ref>, for any two words $\word_1, \word_2\in\colours^*$ with $\card{\word_1} = \card{\word_2}$, we have $\word_1\prefixOrd_{\objective_m}\word_2$ if and only if

\begin{align} \label{eq:prefixOrdOm}
\word_2\colours^\omega \subseteq \objective_m\quad \text{or}\quad (\word_1\colours^\omega \not\subseteq \objective_m\ \text{and}\ \TP(\word_1) \le \TP(\word_2)).
\end{align}

The first term of the disjunction corresponds to the case where $\word_2$ has a prefix that already satisfies $\objective_m$, and hence every continuation is winning for $\objective_m$.
The second term then covers the case where none of the two words has satisfied $\objective_m$ so far and $\word_2$ has a current sum of weights at least as high as $\word_1$.

Let $\strat'$ be an arbitrary winning strategy from $\vertex_0$ (which exists as $\vertex_0$ is in the winning region, i.e., $(\vertex_0, 0) \in \winningExtended$).
Let $\strat_{\mathsf{safe}}$ be a memoryless strategy on $\arena$ staying in $\winningExtended$ given by <ref>.
We consider the “step-counter + $1$-bit” memory structure $\memory = (\IN \times \{0, 1\}, (0, 0), \memUpd)$ (we have not yet defined how and when $\memUpd$ updates the bit, which will come later in the proof).

We define the strategy $\strat_m$ based on $\memory$ inductively from $\vertex_0$, on the set $\vertices_1 \times \IN \times \{0, 1\}$.
As defined above, the initial memory bit is $0$.
The goal is to guarantee the following two properties: for all histories $\history$ consistent with $\strat_m$ from $\vertex_0$,

* we have $(\too(\history), \TP(\history)) \in \winningExtended$, that is, the strategy does not leave the winning region for $\TPsupge$;

* if the memory bit after $\history$ is $0$, there exists a history $\history'$ consistent with $\strat'$ from $\vertex_0$ such that $\card{\history'} = \card{\history}$, $\too(\history') = \too(\history)$, and $\history' \prefixOrd_{\objective_m} \history$.

The properties clearly hold on the empty history $\emptyHistory_{\vertex_0}$ from $\vertex_0$ (for which the bit value is still $0$).
We will prove the two properties inductively after defining the strategy $\strat_m$.
[As a side note, we briefly comment on how these two properties can be interpreted on the game of <ref> (<ref>).
Observe that following the $0$ edges guarantees <ref>. for (it ensures a higher sum of weights), but does not guarantee <ref>. (as $\history$ may not have already satisfied one of the $\objective_m$, unlike all histories $\history'$).
On the other hand, the first time plays $i, -i-1$, it ensures <ref>. (some $\objective_m$ is already satisfied during this round), but not <ref>. (it may leave the winning region $\winningExtended$ if also played $i, -i-1$).
This is why the bit is necessary to guarantee both <ref>. and <ref>.]

Assume that $\strat_m$ has already been defined on $\vertices_1 \times \{0,\ldots,\step-1\} \times \{0,1\}$.
Let $\history$ be a history from $\vertex_0$ consistent with $\strat_m$ of length $\step$.
We write $\vertex$ for $\too(\history)$ for brevity.
To extend $\strat_m$, we need to define $\strat_m(\vertex, \step, 0)$ and $\strat_m(\vertex, \step, 1)$ for $\vertex\in\vertices_1$, and we need to define when the memory bit is updated.
If the memory bit after $\history$ is $0$, we define a history

\[
\history'_{\vertex, \step} \in \min_{\prefixOrd_{\objective_m}}
\{\history' \mid \text{$\history'$ is consistent with $\strat'$, $\from(\history') = \vertex_0$, $\card{\history'} = \step$, and $\too(\history') = \vertex$}\}.
\]

This set is non-empty due to the induction hypothesis <ref>., and well-ordered due to step-monotonicity of $\objective_m$, so $\history'_{\vertex, \step}$ is well-defined.
If $\vertex\in\vertices_1$, we define $\strat_m(\vertex, \step, 0) = \strat'(\history'_{\vertex, \step})$ and $\strat_m(\vertex, \step, 1) = \strat_\mathsf{safe}(\vertex)$.

We now define the bit update.
Let $\edge$ be a possible edge taken from $\vertex$ after history $\history$ (either $\edge$ is the edge taken by $\strat_m$ after $\history$ if $\vertex\in\vertices_1$, or $\edge$ is any possible outgoing edge of $\vertex$ if $\vertex\in\vertices_2$).
When the bit is $1$, we never change the bit (i.e., $\memUpd((\step, 1), \edge) = (\step+1, 1)$).
Assume now that the bit of $\strat_m$ is $0$ after $\history$.
We update the bit from $0$ to $1$ (i.e., define $\memUpd((\step, 0), \edge) = (\step+1, 1)$) if and only if $\col(\history'_{\vertex, \step}\edge)\colours^\omega\subseteq\objective_m$.
Intuitively, this condition means that $\strat'$ has already satisfied $\objective_m$, which will be used to show that so does $\strat_m$.

Now that we have fully defined the next step of $\strat_m$ after $\history$, it is left to prove the two properties.
To do so, we first prove the following property:

\begin{align} \label{eq:unusualPreorder}
\text{if the memory bit after $\history$ is $0$, then $\TP(\history_{\vertex, \step}') \le \TP(\history)$.}
\end{align}

We prove the contrapositive.
Assume that $\TP(\history) < \TP(\history_{\vertex, \step}')$.
Observe that this cannot happen if $\card{\history} = 0$.
Let $\widetilde{\history}\edge$ be the shortest prefix of $\history$ such that $\TP(\history_{\too(\widetilde{\history}), \card{\widetilde{\history}}}') \le \TP(\widetilde{\history})$ but $\TP(\widetilde{\history}\edge) < \TP(\history_{\too(\widetilde{\history}\edge), \card{\widetilde{\history}\edge}}')$.
We have that $\history_{\too(\widetilde{\history}), \card{\widetilde{\history}}}'\edge$ is consistent with $\strat'$ and $\TP(\history_{\too(\widetilde{\history}), \card{\widetilde{\history}}}'\edge) \le \TP(\widetilde{\history}\edge)$.
Combining the last two inequalities, we obtain that $\TP(\history_{\too(\widetilde{\history}), \card{\widetilde{\history}}}'\edge) < \TP(\history_{\too(\widetilde{\history}\edge), \card{\widetilde{\history}\edge}}')$.
However, by definition of $\history_{\too(\widetilde{\history}\edge), \card{\widetilde{\history}\edge}}'$, we have that $\history_{\too(\widetilde{\history}\edge), \card{\widetilde{\history}\edge}}' \prefixOrd_{\objective_m} \history_{\too(\widetilde{\history}), \card{\widetilde{\history}}}'\edge$.

Using the discussion about $\prefixOrd_{\objective_m}$ from (<ref>), this necessarily implies that $\col(\history_{\too(\widetilde{\history}), \card{\widetilde{\history}}}'\edge)\colours^\omega \subseteq \objective_m$.
So the bit was set to $1$ after $\widetilde{\history}\edge$, which means that the bit is still $1$ after $\history$.

We now prove the two inductive properties.

* By induction hypothesis, we have $(\too(\history), \TP(\history)) \in \winningExtended$.

If $\vertex\in\vertices_2$, then for any possible edge $\edge$ from $\vertex$, we still have $(\too(\history\edge), \TP(\history\edge)) \in \winningExtended$ by definition of $\winningExtended$.
We now assume $\vertex\in\vertices_1$ and distinguish whether the bit value after $\history$ is $0$ or $1$.

If the bit is $0$ after $\history$, then by (<ref>), $\TP(\history_{\vertex, \step}') \le \TP(\history)$.
Let $\edge = \strat_m(\vertex, \step, 0) = \strat'(\history_{\vertex, \step}')$; we have $\TP(\history_{\vertex, \step}'\edge) \le \TP(\history\edge)$.
As $\strat'$ is a winning strategy for $\TPsupge$, necessarily, $(\too(\history_{\vertex, \step}'\edge), \TP(\history_{\vertex, \step}'\edge)) \in \winningExtended$.
As $\too(\history_{\vertex, \step}'\edge) = \too(\history\edge)$ and $\TP(\history_{\vertex, \step}'\edge) = \TP(\history_{\vertex, \step}') + \col(\edge) \le \TP(\history) + \col(\edge) = \TP(\history\edge)$, we have $(\too(\history\edge), \TP(\history\edge)) \in \winningExtended$.

If the bit is $1$ after history $\history$, then $\strat_m$ imitates $\strat_\mathsf{safe}$, so $(\too(\history\edge), \TP(\history\edge)) \in \winningExtended$ by definition of $\strat_\mathsf{safe}$.

* Let $\edge$ be a possible edge after $\history$.
Assume the memory bit after $\history\edge$ is $0$.
This implies that the bit was also $0$ after $\history$.
By induction hypothesis, there exists a history $\history'$ consistent with $\strat'$ from $\vertex_0$ such that $\card{\history'} = \card{\history}$, $\too(\history') = \too(\history)$, and $\history' \prefixOrd_{\objective_m} \history$.
We show that $\history_{\vertex, \step}'\edge$ satisfies the desired property for $\history\edge$; we already have by definition that $\card{\history_{\vertex, \step}'\edge} = \card{\history\edge}$ and $\too(\history_{\vertex, \step}'\edge) = \too(\history\edge)$.
Moreover, as the bit is $0$, $\edge = \strat_m(\vertex, \step, 0) = \strat'(\history_{\vertex, \step}')$, so $\history_{\vertex, \step}'\edge$ is also consistent with $\strat'$.
By definition of $\history_{\vertex, \step}'$, we also have $\history_{\vertex, \step}'\prefixOrd_{\objective_m} \history'$, therefore $\history_{\vertex, \step}' \prefixOrd_{\objective_m} \history$.
Hence, $\history_{\vertex, \step}'\edge \prefixOrd_{\objective_m} \history\edge$.

This shows the two inductive properties above.
We still have to show that $\strat_m$ is winning for $\objective_m$ from $\vertex_0$ and never leaves $\winningExtended$.

We prove that $\strat_m$ wins for $\objective_m$.
Observe that $\strat'$ wins in particular for $\objective_m$ (as $\strat'$ wins for $\TPsupge$).
As $\objective_m$ is open and $\arena$ is finitely branching, this means that all histories consistent with $\strat'$ already satisfy $\objective_m$ after a bounded number of steps (<ref>).
This means that for $\step$ sufficiently large, all histories $\history_{\vertex, \step}'$ used to define $\strat_m$ are such that $\col(\history_{\vertex, \step}')\colours^\omega \subseteq \objective_m$.
In particular, for $\step$ sufficiently large, due to how the bit update from $0$ to $1$ is defined, all histories $\history$ consistent with $\strat_m$ reach a bit value of $1$.
We show that any history $\history$ consistent with $\strat_m$ with bit value $1$ is such that $\col(\history)\colours^\omega \subseteq \objective_m$.
Let $\history$ be such a history, and let $\widetilde{\history}$ be its longest prefix with bit value still at $0$.
If $\col(\widetilde{\history})\colours^\omega \subseteq \objective_m$, we are done.
If $\col(\widetilde{\history})\colours^\omega \not\subseteq \objective_m$, as the bit value is still $0$, there is $\widetilde{\history}'$ consistent with $\strat'$ such that $\card{\widetilde{\history}'} = \card{\widetilde{\history}}$, $\too(\widetilde{\history}') = \too(\widetilde{\history})$, and $\widetilde{\history}' \prefixOrd_{\objective_m} \widetilde{\history}$.
We have that $\history'_{\too(\widetilde{\history}), \card{\widetilde{\history}}} \prefixOrd_{\objective_m} \widetilde{\history}'$, so $\history'_{\too(\widetilde{\history}), \card{\widetilde{\history}}} \prefixOrd_{\objective_m} \widetilde{\history}$.
In particular, $\col(\history'_{\too(\widetilde{\history}), \card{\widetilde{\history}}})\colours^\omega \not\subseteq \objective_m$ as well.
By (<ref>), this implies that $\TP(\history'_{\too(\widetilde{\history}), \card{\widetilde{\history}}}) \le \TP(\widetilde{\history})$.
Let $\edge$ be the next edge in $\history$ after $\widetilde{\history}$.
As the bit after $\widetilde{\history}\edge$ is $1$, this means that $\col(\history'_{\too(\widetilde{\history}), \card{\widetilde{\history}}}\edge)\colours^\omega \subseteq \objective_m$.
As additionally, $\card{\widetilde{\history}\edge} = \card{\history'_{\too(\widetilde{\history}), \card{\widetilde{\history}}}\edge}$ and $\TP(\widetilde{\history}\edge) \ge \TP(\history'_{\too(\widetilde{\history}), \card{\widetilde{\history}}}\edge) \ge -\frac{1}{m}$, we have that $\col(\widetilde{\history}\edge)\colours^\omega \subseteq \objective_m$.
As $\history$ is a continuation of $\widetilde{\history}\edge$, we also have that $\col(\history)\colours^\omega \subseteq \objective_m$.

We have shown that all histories consistent with $\strat_m$ reach bit value $1$ within a bounded number of steps, and that bit value $1$ indicates that any continuation is winning $\objective_m$.
This shows that $\strat_m$ is winning for $\objective_m$.

The fact that $\strat_m$ never leaves $\winningExtended$ from $\vertex_0$ is a direct consequence of <ref>.

Using the previous lemma, we now prove <ref>.
Let $\arena = \arenaFull$ be an arena and $\vertex_0\in\vertices$ be an initial vertex in the winning region of for $\TPsupge$.
Let the $\memory = (\IN \times \{0, 1\}, (0, 0), \memUpd)$ be the “step-counter + $1$-bit” memory structure (we still need to define how and when $\memUpd$ updates the bit).
We show that there is a winning step-counter + $1$-bit strategy $\strat$ (i.e., $\strat$ is based on $\memory$) from $\vertex_0$.

We build a winning step-counter + 1-bit strategy $\strat\colon \vertices_1 \times \IN \times \{0, 1\} \to \edges$ inductively.
Consider the product arena $\arena' = \arena\product \memory$ (in which the bit updates are not fixed yet, and will be fixed inductively).
We have that $(\vertex_0, (0, 0))$ is in the winning region of $\arena'$.
The inductive scheme is as follows: for infinitely many $m\in\IN$, for some step bound $k_m\in\IN$, we fix $\strat$ on $\vertices \times \{0,\ldots, k_m - 1\} \times \{0, 1\}$, yielding arena $\arena'_m$.
We ensure that

* along all histories $\history$ from $\vertex_0$ consistent with $\strat$ of length at most $k_m$, $\winningExtended$ is not left (i.e., $(\too(\history), \TP(\history))\in\winningExtended$), and

* the open objective $\objective_{m}$ is already satisfied within $k_m$ steps (i.e., any history of length $k_m$ consistent with $\strat$ only has winning continuations for $\objective_{m}$).

For the base case, we may assume that we start the induction at $m = -1$ with $k_{-1} = 0$ and $\objective_{-1} = \colours^\omega$.
We indeed have that from $(\vertex_0, (0, 0))$, the winning region $\winningExtended$ is not left within $k_{-1} = 0$ step and that the open objective $\objective_{-1}$ is already satisfied.

Assume that we have fixed $\strat$ in $\arena'$ (decisions and bit updates) up to some step bound $k_m$, that $\winningExtended$ is not left within $k_m$ steps, and that $\objective_m$ is already satisfied for all histories of length $k_m$.
We reset the bit to $0$ after exactly $k_m$ steps: for $\vertex\in\vertices$ and $b\in\{0, 1\}$, we define $\memUpd(\vertex, (k_m - 1, b)) = (k_m, 0)$.
Fixing $\strat$ up to bound $k_m$ defines an arena $\arena'_m$.

Since $\winningExtended$ is not left within the first $k_m$ steps, and since no decisions have been fixed after $k_m$ steps, vertex $(\vertex_0, (0, 0))$ is still in the winning region for $\TPsupge$.
Let $m' = k_m + 1$.
We apply <ref>: there exists a step-counter + 1-bit strategy $\strat_{m'}$ such that $\strat_{m'}$ is winning for $\objective_{m'}$ from $(\vertex_0, (0, 0))$ and never leaves $\winningExtended$.
Observe that there are no decisions to make in $\arena'_m$ before $k_m$ steps have elapsed, and that the bit is set to $0$ after exactly $k_m$ steps.
By <ref>, as $\arena'_m$ is finitely branching and $\objective_{m'}$ is open, there is a bound $k_{m'}$ such that any history consistent with $\strat_{m'}$ of length $k_{m'}$ already satisfies $\objective_{m'}$.
Since $\objective_{m'}$ cannot be already satisfied before step $m'$, we have $k_{m'} \ge k_m + 1$.
We define $\arena'_{m'}$ by fixing strategy $\strat'_{m'}$ up to step $k_{m'}$.

Iterating this procedure defines a step-counter + 1-bit strategy $\strat$ such that, for infinitely many $m\ge 1$, $\strat$ is winning for $\objective_m$.
As the sequence $\objective_m$ is decreasing ($\objective_1 \supseteq \objective_2 \supseteq \ldots$), we have that $\strat$ is winning for $\objective_m$ for all $m\ge 1$.
Hence, $\strat$ is winning for $\TPsupge$.

In general, this proof does not apply uniformly: in the arena of <ref>, has no uniformly winning strategy based on a step counter and finite memory from all $s_i$ simultaneously, since needs to exit to $r_0$ arbitrarily far to the right.

Arena in which has no uniformly winning step-counter + $1$-bit strategy.