compatible with the strategy $\mathsf{s}_{\mathsf{A}}$ (and the minimum of
their values w.r.t. the valuation $v$ is $v_{H}>0$). Hence, by assumption, all
these BSCCs are even-colored, that is they have value 1. It follows that all
states in $H_{\mathsf{s}_{\mathsf{B}}}$ have value 1. Hence, the second
condition of [5, Lemma 17] is ensured, and this lemma can be applied.

###  C.4 Proof of Lemma 21

######  Proof.

The first equivalence comes from [4, Lemma 16] and the fact that positional
deterministic strategies are enough (for Player $\mathsf{B}$) to play
optimally in finite MDPs with parity objectives [7]. Now assume that $u>0$.
Assume that the strategy $\mathsf{s}_{Y}^{\mathsf{A}}(\sigma_{\mathsf{A}})$
parity dominates the valuation $v_{Y}^{u}$ in the game $\mathcal{G}_{Y}$. In
particular, it dominates this valuation, i.e. item $(ii.1)$ of Lemma 21 is
ensured. Consider now some action $b\in\mathsf{Act}_{\mathsf{B}}$ such that
$\mathsf{out}_{\langle\mathcal{F},p(\cdot)[p_{[0,1]}]\rangle}(\sigma_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}(q_{0}))=0$
and a Player-$\mathsf{B}$ positional and deterministic strategy
$\mathsf{s}_{\mathsf{B}}$ such that $\mathsf{s}_{\mathsf{B}}(q_{0}):=b$. Since
we have
$\mathsf{out}_{\langle\mathcal{F},p(\cdot)[p_{[0,1]}]\rangle}(\sigma_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}(q_{0}))=0$,
no stopping state can be reached under
$\mathsf{s}_{Y}^{\mathsf{A}}(\sigma_{\mathsf{A}})$ and
$\mathsf{s}_{\mathsf{B}}$. Consider the Markov chain
$\mathcal{M}_{\mathsf{s}_{Y}^{\mathsf{A}}(\sigma_{\mathsf{A}}),\mathsf{s}_{\mathsf{B}}}$.
Besides stopping states, it is reduced to a BSCC $H$ whose states are
$q_{\mathsf{init}}$ and all states $k_{i}$ reachable with that action $b$.
That is, $H=\\{q_{\mathsf{init}}\\}\cup\\{k_{i}\mid i\in\llbracket
0,e\rrbracket,\;\mathsf{out}_{\langle\mathcal{F},p(\cdot)(i)\rangle}(\sigma_{\mathsf{A}},b)>0\\}$.
Furthermore, $q_{\mathsf{init}}$ is colored with $c$. The value of this BSCC
$H$ is in $\\{0,1\\}$ and it is equal to $1$ if and only if $H$ is even-
colored (since every state in a BSCC is almost-surely seen infinitely often).
Since $u>0$, the value of $H$ cannot be 0, thus $H$ is even-colored and the
maximum of the colors seen with that action is even. This exactly corresponds
to item $(ii.2)$ of Lemma 21.

Assume now that the $\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ satisfies
both items $(ii.1)$ and $(ii.2)$. Consider a positional deterministic
Player-$\mathsf{B}$ strategy $\mathsf{s}_{\mathsf{B}}$ in the game
$\mathcal{G}_{Y}$. Let $b:=\mathsf{s}_{\mathsf{B}}(q_{0})\in\mathsf{Act}_{B}$.
Consider a BSCC $H$ in the induced Markov chain
$\mathcal{M}_{\mathsf{s}_{Y}^{\mathsf{A}}(\sigma_{\mathsf{A}}),\mathsf{s}_{\mathsf{B}}}$
that is not reduced to a stopping state. In particular, this implies that
$\mathsf{out}_{\langle\mathcal{F},p(\cdot)[p_{[0,1]}]\rangle}(\sigma_{\mathsf{A}},b)=0$.
Then, as previously, we have $H=\\{q_{\mathsf{init}}\\}\cup\\{k_{i}\mid
i\in\llbracket
0,e\rrbracket,\;\mathsf{out}_{\langle\mathcal{F},p(\cdot)(i)\rangle}(\sigma_{\mathsf{A}},b)>0\\}$.
The fact that $\sigma_{\mathsf{A}}$ satisfies item $(ii.2)$ ensures that the
BSCC $H$ is even-colored. It follows that the strategy
$\mathsf{s}_{Y}^{\mathsf{A}}(\sigma_{\mathsf{A}})$ parity dominates the
valuation $v_{Y}^{u}$.

###  C.5 Proof of Lemma 28

######  Proof.

Consider such a strategy $\mathsf{s}_{\mathsf{A}}$. Let us show that it parity
dominates the valuation $\chi_{\mathcal{G}}$. First, note that it dominates
the valuation $\chi_{\mathcal{G}}$ since, for all $u\in
V_{\mathcal{G}}\setminus\\{0\\}$, the strategy $\mathsf{s}_{\mathsf{A}}^{u}$
dominates $\chi_{\mathcal{G}}$ in $\mathcal{G}^{u}$ (recall that the stopping
states in $\mathcal{G}^{u}$ have the values of the original states in
$\mathcal{G}$). Consider now a BSCC $H$ compatible with
$\mathsf{s}_{\mathsf{A}}$ such that $\min\chi_{\mathcal{G}}[H]>0$. By Theorem
13, there is a value $u_{H}\in(0,1]$ such that
$\chi_{\mathcal{G}}[H]=\\{u_{H}\\}$. That is, $H\subseteq Q_{u_{H}}$. It
follows that $H$ is compatible with $\mathsf{s}_{\mathsf{A}}^{u_{H}}$. Since
$\mathsf{s}_{\mathsf{A}}^{u_{H}}$ parity dominates the valuation
$\chi_{\mathcal{G}}$ in $\mathcal{G}^{u_{H}}$, we can deduce that $H$ is even-
colored. Overall, the strategy $\mathsf{s}_{\mathsf{A}}$ parity dominates the
valuation $\chi_{\mathcal{G}}$. By Theorem 13, the strategy
$\mathsf{s}_{\mathsf{A}}$ guarantees it (i.e. it is optimal).

##  Appendix D Proof of Theorem 25

In this section, we give all the technical details used to prove Theorem 25.
The proof of this theorem is given in Page 49, provided that Lemmas 44, 47, 48
and 49 hold. We already stated and argued why these lemmas hold, however we
have not given a detailed proof of them. This is what we do in this section.
However, we first state and prove results that we use in this section.

We first state and prove properties on the update of colors $\mathsf{NewCol}$.
This is done in Page D.1. Then, we give the complete definition of
faithfulness, see Page D.2. We also state and prove three lemmas, that relate
local and global behaviors, see Page D.3. We finally prove the lemmas
mentioned above: we prove Lemma 44 in Page D.4, Lemma 47 in Page D.5, Lemma 48
in Page D.6 and Lemma 49 in Page D.7.

###  D.1 Properties ensured by the local operator $\mathsf{NewCol}$

We introduce a useful notation which will allow us to rewrite Lemma 21 in our
context.

######  Definition 63.

Consider a state $q\in Q$, a virtual coloring function
$\mathsf{vcol}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$, a color
$n\in\llbracket 0,e\rrbracket$ and two $\mathsf{GF}$-strategies
$(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\in\Sigma_{\mathsf{A}}(\mathsf{F}(q))\times\Sigma_{\mathsf{B}}(\mathsf{F}(q))$.
We denote by $\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{B})$
the set of colors reachable in one step with positive probability w.r.t.
$(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$ in the local game
$\mathcal{G}_{q,\mathsf{vcol}}^{n}$ (regardless of the color $n\in\llbracket
0,e\rrbracket$ considered). That is:

$\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{B}):=\\{i\in\llbracket
0,e\rrbracket\mid\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p_{q,\mathsf{vcol}}^{-1}[k_{i}]}\rangle}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})>0\\}$

In particular,
$\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},b)=\mathsf{Color}(\mathsf{F}(q),p_{q,\mathsf{vcol}},\sigma_{\mathsf{A}},b)$
for all $b\in\mathsf{Act}_{\mathsf{B}}$ (notation from Lemma 21).

Then, the set of colors
$\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},\sigma_{B})$ is
defined by:

$\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},\sigma_{B}):=\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{B})\cup\\{\max(\mathsf{vcol}(q),c_{n})\\}$

with $c_{n}:=n-1$ is $n$ is even and $c_{n}:=n+1$ is $n$ is odd.

We obtain a corollary of Lemma 21 (which only consists in writing Lemma 21 in
the context of a local game $\mathcal{G}_{q,\mathsf{vcol}}^{n}$).

######  Corollary 64.

Consider a state $q\in Q$, a virtual coloring function
$\mathsf{vcol}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$, a color
$n\in\llbracket 0,e\rrbracket$ and a local strategy
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathsf{F}(q))$. A
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathcal{F})$ is _optimal_ w.r.t.
$Y:=(\mathsf{F}(q),E_{q,\mathsf{vcol}}^{n})$ if and only if, letting
$u:=\chi_{\mathcal{G}_{Y}}(q_{\mathsf{init}})$, either (i) $u=0$, or (ii) the
positional Player-$\mathsf{A}$ strategy
$\mathsf{s}^{Y}_{\mathsf{A}}(\sigma_{\mathsf{A}})$ parity dominates the
valuation $v_{Y}^{u}$.

Furthermore (ii) is equivalent to:

  * •

(1): the Player-$\mathsf{A}$ positional strategy
$\mathsf{s}^{Y}_{\mathsf{A}}(\sigma_{\mathsf{A}})$ dominates the valuation
$v_{Y}^{u}$; and

  * •

(2): for all $b\in\mathsf{Act}_{\mathsf{B}}$, if
$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[0,1]}\rangle}(\sigma_{\mathsf{A}},b)=0$,
then $\max\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},\sigma_{B})$
is even.

This is symmetrical for Player $\mathsf{B}$.

Let us now state a proposition we will use to prove that the update of colors
cannot decrease the colors of the states.

######  Proposition 65.

Let $q\in Q_{u}$ and some virtual coloring function
$\mathsf{vcol}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$, some color
$n\in\llbracket 0,e\rrbracket$ and a positive value $z\in(0,1]$. Let
$p:=p_{q,\mathsf{vcol}}$ and $Y:=(\mathsf{F}(q),E_{q,\mathsf{vcol}}^{n})$. For
all Player-$\mathsf{A}$ $\mathsf{GF}$-strategies
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathsf{F}(q))$, the positional
Player-$\mathsf{A}$ strategy
$\mathsf{s}_{Y}^{\mathsf{A}}(\sigma_{\mathsf{A}})$ dominates the valuation
$v_{Y}^{z}$ if and only if for all $b\in\mathsf{Act}_{\mathsf{B}}$: if
$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{Q\setminus
Q_{u}}\rangle}(\sigma_{\mathsf{A}},b)>0$, then:

$\mathsf{out}_{\langle\mathsf{F}(q),\mu^{z}\rangle}(\sigma_{\mathsf{A}},b)\geq
0$

where $\mu^{z}:Q\rightarrow[0,1]$ is such that, for all $q\in Q$:

$\mu^{z}(q):=\begin{cases}0&\text{ if }q\in Q_{u}\\\
\chi_{\mathcal{G}}(q)-z&\text{ otherwise}\end{cases}$

######  Proof.

In the game $\mathcal{G}_{Y}$, the Player-$\mathsf{A}$ strategy
$\mathsf{s}_{Y}^{\mathsf{A}}(\sigma_{\mathsf{A}})$ dominates the valuation
$v_{Y}^{z}$ — property we denote $(1)$ — if and only if:

$\displaystyle z=v_{Y}^{z}(q_{\mathsf{init}})$
$\displaystyle\leq\mathsf{val}{\langle\mathsf{F}(q),v_{Y}^{z}\rangle}(\mathsf{s}_{Y}^{\mathsf{A}}(\sigma_{\mathsf{A}})(q_{\mathsf{init}}))$
$\displaystyle=\mathsf{val}{\langle\mathsf{F}(q),v_{Y}^{z}\rangle}(\sigma_{\mathsf{A}})$

In addition,
$\mathsf{val}{\langle\mathsf{F}(q),v_{Y}^{z}\rangle}(\sigma_{\mathsf{A}})=\min_{b\in\mathsf{Act}_{\mathsf{B}}}\mathsf{out}_{\langle\mathsf{F}(q),v_{Y}^{z}\rangle}(\sigma_{\mathsf{A}},b)$.
Furthermore, for all $b\in\mathsf{Act}_{\mathsf{B}}$, we have that

$\displaystyle\mathsf{out}_{\langle\mathsf{F}(q),v_{Y}^{z}\rangle}(\sigma_{\mathsf{A}},b)$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[\\{q_{\mathsf{init}}\\}\cup
K_{e}]}\rangle}(\sigma_{\mathsf{A}},b)\cdot z$ $\displaystyle+\sum_{x\in
V_{Q\setminus
Q_{u}}}\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[x]}\rangle}(\sigma_{\mathsf{A}},b)\cdot
x$

It follows that, if
$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{Q\setminus
Q_{u}}\rangle}(\sigma_{\mathsf{A}},b)=0$, we have
$\mathsf{out}_{\langle\mathsf{F}(q),v_{Y}^{z}\rangle}(\sigma_{\mathsf{A}},b)=z$
since $\cup_{x\in V_{Q\setminus Q_{u}}}p^{-1}[x]=Q\setminus Q_{u}$. However,
if $\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{Q\setminus
Q_{u}}\rangle}(\sigma_{\mathsf{A}},b)>0$, we have that

$\displaystyle
z\leq\mathsf{out}_{\langle\mathsf{F}(q),v_{Y}^{z}\rangle}(\sigma_{\mathsf{A}},b)\Leftrightarrow
0$ $\displaystyle\leq\sum_{x\in V_{Q\setminus
Q_{u}}}\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[x]}\rangle}(\sigma_{\mathsf{A}},b)\cdot(x-z)$
$\displaystyle 0$
$\displaystyle\leq\mathsf{out}_{\langle\mathsf{F}(q),\sum_{x\in V_{Q\setminus
Q_{u}}}\mathbbm{1}_{p^{-1}[x]}\cdot(x-z)\rangle}(\sigma_{\mathsf{A}},b)$
$\displaystyle 0$
$\displaystyle\leq\mathsf{out}_{\langle\mathsf{F}(q),\mu^{z}\rangle}(\sigma_{\mathsf{A}},b)$

The result follows.

The update of colors does not decrease the color. Let us show that the local
operator $\mathsf{NewCol}$ does not decrease (w.r.t. the usual order $<$ on
natural numbers) the previous color of the state $q$ given by a (virtual)
coloring function $\mathsf{vcol}$.

######  Proposition 66.

Consider a state $q\in Q_{u}$ and a coloring function
$\mathsf{vcol}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$. We have
$\mathsf{NewCol}(q,\mathsf{vcol})\geq\mathsf{vcol}(q)$.

######  Proof.

We let $p:=p_{q,\mathsf{vcol}}$ and, for all $n\in\llbracket 0,e\rrbracket$,
we let $Y_{n}:=(\mathsf{F}(q),E_{q,\mathsf{vcol}}^{n})$. Note that
$p_{[0,1]}\subseteq V_{Q\setminus Q_{u}}$.

There are two cases: either $\mathsf{vcol}(q)=e$ or $\mathsf{vcol}(q)<e$.
First, assume that $\mathsf{vcol}(q)=e$. Let us show that in that case
$\mathsf{NewCol}(q,\mathsf{vcol})=e$. Assume towards a contradiction that
$\chi_{\mathcal{G}_{Y_{e}}}(q_{\mathsf{init}})=u^{\prime}<u$ for some
$u^{\prime}\in[0,1]$. Consider a Player-$\mathsf{B}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{B}}$ that is optimal w.r.t. $Y_{e}$. For all
$a\in\mathsf{Act}_{\mathsf{A}}$, we have
$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q\setminus
Q_{u}}\rangle}(a,\sigma_{\mathsf{B}})>0$. Indeed, otherwise, in the game
$\mathcal{G}_{q,\mathsf{vcol}}^{e}$ where Player $\mathsf{B}$ plays the
strategy defined by $\sigma_{\mathsf{B}}$, Player $\mathsf{A}$ could loop
indefinitely on $q_{\mathsf{init}}$ thus ensuring winning with probability 1
(since the color of the state $q_{\mathsf{init}}$ is $e$ — as
$\mathsf{vcol}(q)=e$ — which is both the highest color appearing in the game
and even). We let:

$p_{\mathsf{Exit}}:=\min_{a\in\mathsf{Act}_{\mathsf{A}}}\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q\setminus
Q_{u}}\rangle}(a,\sigma_{\mathsf{B}})>0$

Now, consider some $a\in\mathsf{Act}_{\mathsf{A}}$. By Proposition 65 for
Player $\mathsf{B}$, we have:
$\mathsf{out}_{\langle\mathcal{F},\mu^{u^{\prime}}\rangle}(a,\sigma_{\mathsf{B}})\leq
0$ where $\mu^{u^{\prime}}:Q\rightarrow[0,1]$ comes from Proposition 65.
Hence, we have:

$\sum_{x\in V_{Q\setminus
Q_{u}}}\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q_{x}}\rangle}(a,\sigma_{\mathsf{B}})\cdot
x\leq\sum_{x\in V_{Q\setminus
Q_{u}}}\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q_{x}}\rangle}(a,\sigma_{\mathsf{B}})\cdot
u^{\prime}$

Letting $v:=\chi_{\mathcal{G}}$ be the value vector in the game $\mathcal{G}$,
we have:

$\displaystyle\sum_{q^{\prime}\in
Q}\mathbb{P}^{q,q^{\prime}}{}(a,\sigma_{\mathsf{B}})\cdot v(q^{\prime})$
$\displaystyle=\sum_{q^{\prime}\in
Q}\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{q^{\prime}}\rangle}(a,\sigma_{\mathsf{B}})\cdot
v(q^{\prime})$
$\displaystyle=\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q_{u}}\rangle}(a,\sigma_{\mathsf{B}})\cdot
u+\sum_{x\in V_{Q\setminus
Q_{u}}}\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q_{x}}\rangle}(a,\sigma_{\mathsf{B}})\cdot
x$
$\displaystyle\leq\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q_{u}}\rangle}(a,\sigma_{\mathsf{B}})\cdot
u+\sum_{x\in V_{Q\setminus
Q_{u}}}\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q_{x}}\rangle}(a,\sigma_{\mathsf{B}})\cdot
u^{\prime}$
$\displaystyle=\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q_{u}}\rangle}(a,\sigma_{\mathsf{B}})\cdot
u+\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q\setminus
Q_{u}}\rangle}(a,\sigma_{\mathsf{B}})\cdot u^{\prime}$
$\displaystyle=u-\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{Q\setminus
Q_{u}}\rangle}(a,\sigma_{\mathsf{B}})\cdot(u-u^{\prime})$ $\displaystyle\leq
u-p_{\mathsf{Exit}}\cdot(u-u^{\prime})<u=v(q)$

Hence, letting $\delta:=p_{\mathsf{Exit}}\cdot(u-u^{\prime})/2>0$ and
considering, in the original game $\mathcal{G}$, a Player-$\mathsf{B}$
strategy $\mathsf{s}_{\mathsf{B}}\in\mathsf{S}_{\mathsf{B}}^{\mathcal{C}}$
such that $\mathsf{s}_{\mathsf{B}}(q):=\sigma_{\mathsf{B}}$ and for all
$q^{\prime}\in Q$, we have $\mathsf{s}_{\mathsf{B}}(q\cdot q^{\prime})$ a
$\delta$-optimal Player-$\mathsf{B}$ strategy from $q^{\prime}$, it follows
that, for all Player-$\mathsf{A}$ strategy $\mathsf{s}_{\mathsf{A}}$ in the
game $\mathcal{G}$, we have:

$\displaystyle\mathbb{P}^{\mathcal{C},q}_{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}{}[W]$
$\displaystyle=\sum_{q^{\prime}\in
Q}\mathbb{P}^{q,q^{\prime}}{}(\mathsf{s}_{\mathsf{A}}(q),\sigma_{\mathsf{B}})\cdot\mathbb{P}^{\mathcal{C},q^{\prime}}_{\mathsf{s}_{\mathsf{A}}^{q},\mathsf{s}_{\mathsf{B}}^{q}}{}[W]$
$\displaystyle\leq\sum_{q^{\prime}\in
Q}\mathbb{P}^{q,q^{\prime}}{}(\mathsf{s}_{\mathsf{A}}(q),\sigma_{\mathsf{B}})\cdot(v(q^{\prime})+\delta)\leq
v(q)-2\delta+\delta=v(q)-\delta$

where $W:=(\mathsf{col}^{\omega})^{-1}[W(\mathsf{col})]\subseteq Q^{\omega}$.
Thus, the value from $q$ is less than $u=v(q)$. Hence the contradiction. In
fact, $\chi_{\mathcal{G}_{q,\mathsf{vcol}}^{e}}(q_{\mathsf{init}})\geq u$ and
$\mathsf{NewCol}(q,\mathsf{vcol})=e$.

Consider now the case where $\mathsf{vcol}(q)<e$. Assume towards a
contradiction that $\mathsf{NewCol}(q,\mathsf{vcol})<\mathsf{vcol}(q)$. Let
$n:=\mathsf{NewCol}(q,\mathsf{vcol})$.

Assume that $n$ is even. By assumption, we have
$\chi_{\mathcal{G}_{Y_{n}}}(q_{\mathsf{init}})\geq u$. Consider a
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ that is
optimal w.r.t. $Y_{n}$. First, the positional Player-$\mathsf{A}$ strategy
$\mathsf{s}_{\mathsf{A}}:=\mathsf{s}_{Y_{n}}^{A}(\sigma_{\mathsf{A}})=\mathsf{s}_{Y_{n+2}}^{A}(\sigma_{\mathsf{A}})$
defined by $\sigma_{\mathsf{A}}$ dominates the valuation
$v_{Y_{n}}^{u}=v_{Y_{n+2}}^{u}$ in the game $\mathcal{G}_{Y_{n}}$ and it also
does in the game $\mathcal{G}_{Y_{n+2}}$. Consider now an action
$b\in\mathsf{Act}_{\mathsf{B}}$ and assume that
$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[0,1]}\rangle}(\sigma_{\mathsf{A}},b)=0$.
By Corollary 64, it follows that, in the game $\mathcal{G}_{Y_{n}}$, we have
$\max\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},b)$ even with
$\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},b)=\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},b)\cup\\{e_{n}\\}$
with $e_{n}=\max(\mathsf{vcol}(q),c_{n})$ and $c_{n}=n-1$ since $n$ is even.
Since $n<\mathsf{vcol}(q)$, we have
$e_{n}=\max(\mathsf{vcol}(q),c_{n})=\mathsf{vcol}(q)$. Furthermore,
$e_{n+2}=\max(\mathsf{vcol}(q),c_{n+2})$ with $c_{n+2}=n+1$ since $n$ is even.
Since $n<\mathsf{vcol}(q)$, we also have $e_{n+2}=\mathsf{vcol}(q)=e_{n}$.
That is,
$\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},b)=\mathsf{ColBSCC}(q,\mathsf{vcol},n+2,\sigma_{\mathsf{A}},b)$.
Hence, $\mathsf{ColBSCC}(q,\mathsf{vcol},n+2,\sigma_{\mathsf{A}},b)$ is also
even. By Corollary 64, the Player-$\mathsf{A}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}$ strongly dominates the valuation $v_{Y_{n+2}}^{u}$.
Hence, by Proposition 13, the Player-$\mathsf{A}$ positional strategy
$\mathsf{s}_{Y_{n+2}}^{\mathsf{A}}(\sigma_{\mathsf{A}})$ guarantees the
valuation $v_{Y_{n+2}}^{u}$. Hence the contradiction since this implies
$\mathsf{NewCol}(q,\mathsf{vcol})\geq n+2$.

When $n$ is odd, the reasoning is symmetrical, by taking the point-of-view of
Player $\mathsf{B}$: we compare what happens in the games
$\mathcal{G}_{Y_{m}}$ and $\mathcal{G}_{Y_{m}}$ for $m:=\mathsf{Succ}(n)$.

The update of colors is not affected by small changes of colors. Let us now
tackle another property ensured by the local operator $\mathsf{NewCol}$.
Assume that the new color of a state $q$ is $n\in\llbracket 0,e\rrbracket$
w.r.t. a coloring function $\mathsf{vcol}$. Now, consider another coloring
function $\mathsf{vcol}^{\prime}$ that coincide with $\mathsf{vcol}$ on colors
at least $n$, and may differ for smaller colors. In that case, the new color
of $q$ will still be $n$ w.r.t. the coloring function
$\mathsf{vcol}^{\prime}$. This is (almost) what we prove here. First, we
introduce the notion of equivalent and prevailing coloring functions.

######  Definition 67 (Equivalent and Prevailing coloring functions).

Consider two coloring functions
$\mathsf{vcol},\mathsf{vcol}^{\prime}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$ and some color $n\in\llbracket 0,e\rrbracket$. The coloring
functions $\mathsf{vcol},\mathsf{vcol}^{\prime}$ are _equivalent down to_ $n$
if, for all $k\in\llbracket n,e\rrbracket$, we have
$\mathsf{vcol}^{-1}[k]=\mathsf{vcol}^{\prime-1}[k]$.

Furthermore, $\mathsf{vcol}^{\prime}$ is said to be $(n-1)$-_prevailing
compared to_ $\mathsf{vcol}$ if $\mathsf{vcol}$ and $\mathsf{vcol}^{\prime}$
are equivalent down to $n$ and
$\mathsf{vcol}^{-1}[n-1]\subseteq\mathsf{vcol}^{\prime-1}[n-1]$.

Let us first state a lemma that we will use to prove the proposition (of
interest for us) that we state below.

######  Lemma 68.

Consider a state $q\in Q_{u}$ and some color $n\in\llbracket 0,e\rrbracket$.
Let $\mathsf{vcol},\mathsf{vcol}^{\prime}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$ be two virtual coloring functions with $\mathsf{vcol}^{\prime}$
$n$-prevailing compared to $\mathsf{vcol}$. Consider a pair of
$\mathsf{GF}$-strategies
$(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\in\Sigma_{\mathsf{A}}(\mathsf{F}(q))\times\Sigma_{\mathsf{B}}(\mathsf{F}(q))$.
We have:

$\displaystyle\max\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\geq
n\Rightarrow$
$\displaystyle\max\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=\max\mathsf{ColBSCC}(q,\mathsf{vcol}^{\prime},n,\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$

######  Proof.

Letting $c_{n}:=n-1$ if $n$ is even and $c_{n}:=n+1$ if $n$ is odd, we have
(recall Definition 63):

$\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\cup\\{\max(\mathsf{vcol}(q),c_{n})\\}$

and

$\mathsf{ColBSCC}(q,\mathsf{vcol}^{\prime},n,\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=\mathsf{Col}(q,\mathsf{vcol}^{\prime},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\cup\\{\max(\mathsf{vcol}^{\prime}(q),c_{n})\\}$

By assumption, we have that, for all $i\in\llbracket n+1,e\rrbracket$:

$\mathsf{vcol}^{-1}[i]=\mathsf{vcol}^{\prime-1}[i]$

Thus:

$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p_{q,\mathsf{vcol}}^{-1}[k_{i}]}\rangle}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p_{q,\mathsf{vcol}}^{-1}[k_{i}]}\rangle}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$

Furthermore:

$\mathsf{vcol}^{-1}[n]\subseteq\mathsf{vcol}^{\prime-1}[n]$

Thus:

$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p_{q,\mathsf{vcol}}^{-1}[k_{n}]}\rangle}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})>0\Rightarrow\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p_{q,\mathsf{vcol}^{\prime}}^{-1}[k_{n}]}\rangle}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})>0$

We therefore obtain that for any $k\in\llbracket n,e\rrbracket$:

  * (i)

If
$\max\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\leq
k$, then
$\max\mathsf{Col}(q,\mathsf{vcol}^{\prime},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\leq
k$;

  * (ii)

If
$\max\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=k$,
then
$\max\mathsf{Col}(q,\mathsf{vcol}^{\prime},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=k$.

Furthermore:

  * (i’)

If $\mathsf{vcol}(q)\leq k$, then $\mathsf{vcol}^{\prime}(q)\leq k$;

  * (ii’)

If $\mathsf{vcol}(q)=k$, then $\mathsf{vcol}^{\prime}(q)=k$.

We have three cases, letting $n\leq
j:=\max\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\cup\\{\max(\mathsf{vcol}(q),c_{n})\\}$:

  * •

If $j=c_{n}$, then
$\max\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}}),\mathsf{vcol}(q)\leq
j$. Hence, by (i) and (i’), we have
$\max\mathsf{Col}(q,\mathsf{vcol}^{\prime},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}}),\mathsf{vcol}^{\prime}(q)\leq
j$.
That is,
$\max\mathsf{ColBSCC}(q,\mathsf{vcol}^{\prime},n,\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=j$.

  * •

If $j=\mathsf{vcol}(q)$ then
$\max\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}}),c_{n}\leq
j$. Hence, by (ii’), we have $j=\mathsf{vcol}^{\prime}(q)$ and, by (i), we
have
$\max\mathsf{Col}(q,\mathsf{vcol}^{\prime},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\leq
j$.
That is,
$\max\mathsf{ColBSCC}(q,\mathsf{vcol}^{\prime},n,\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=j$.

  * •

If
$j=\max\mathsf{Col}(q,\mathsf{vcol},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$
then $\mathsf{vcol}(q),c_{n}\leq j$. Hence, by (ii), we have
$j=\max\mathsf{Col}(q,\mathsf{vcol}^{\prime},\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$
and, by (i’), we have $\mathsf{vcol}^{\prime}(q)\leq j$. That is,
$\max\mathsf{ColBSCC}(q,\mathsf{vcol}^{\prime},n,\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})=j$.

The lemma follows.

######  Proposition 69.

Consider a state $q\in Q_{u}$ and a coloring function
$\mathsf{vcol}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$. Let
$n:=\mathsf{NewCol}(q,\mathsf{vcol})\in\llbracket 0,e\rrbracket$. Assume that
another coloring function $\mathsf{vcol}^{\prime}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$ is $n$-prevailing compared to $\mathsf{vcol}$. In that case,
$\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})=n$.

######  Proof.

Let us consider two such coloring functions $\mathsf{vcol}$ and
$\mathsf{vcol}^{\prime}$. We have
$n=\mathsf{NewCol}(q,\mathsf{vcol})\in\llbracket 0,e\rrbracket$. Consider a
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ that is
optimal w.r.t. $Y$ for $Y:=(\mathsf{F}(d),E_{q,\mathsf{vcol}}^{n})$. Let
$Y^{\prime}:=(\mathsf{F}(d),E_{q,\mathsf{vcol}^{\prime}}^{n})$,
$p:=p_{q,\mathsf{vcol}}$ and $p^{\prime}:=p_{q,\mathsf{vcol}^{\prime}}$. Let
us show that
$n\preceq_{\mathsf{par}}\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})$. This
straightforwardly holds if $n=e-1$. Assume now that $n\neq e-1$. The
Player-$\mathsf{A}$ strategy
$\mathsf{s}_{Y}^{\mathsf{A}}(\sigma_{\mathsf{A}})$ dominates the valuations
$v_{Y}^{u}=v_{Y^{\prime}}^{u}$.

Consider an action $b\in\mathsf{Act}_{\mathsf{B}}$ and assume that
$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[0,1]}\rangle}(\sigma_{\mathsf{A}},b)=0$.
By Corollary 64, we have
$j:=\max\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},b)$ is even
with
$\max\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},b)\geq\max(\mathsf{vcol}(q),c_{n})$
for $c_{n}=n-1$ if $n$ is even and $c_{n}=n+1$ otherwise. Since $n-1$ is odd,
it follows that, in any case,
$\max\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},b)\geq n$. Then,
by Lemma 68, we have
$\max\mathsf{ColBSCC}(q,\mathsf{vcol}^{\prime},n,\sigma_{\mathsf{A}},b)=\max\mathsf{ColBSCC}(q,\mathsf{vcol},n,\sigma_{\mathsf{A}},b)$,
which is even. As this holds for all $b\in\mathsf{Act}_{\mathsf{B}}$, the
$\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ strongly dominates the valuation
$v_{Y^{\prime}}^{u}$, hence, by Theorem 13, the value of the state
$q_{\mathsf{init}}$ in the game $\mathcal{G}_{Y^{\prime}}$ is at least $u$:
$\chi_{\mathcal{G}_{Y^{\prime}}}[q_{\mathsf{init}}]\geq u$. Hence,
$n\preceq_{\mathsf{par}}\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})$.

Let us now show that
$\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})\preceq_{\mathsf{par}}n$, which
straightforwardly holds if $n=e$. Hence, assume that $n\neq e$ and let
$m:=\mathsf{Succ}(n)\in\llbracket 0,e\rrbracket$. The proof is very similar to
the previous case. Let $Z:=(\mathsf{F}(d),E_{q,\mathsf{vcol}}^{m})$. Let also
$Z^{\prime}:=(\mathsf{F}(d),E_{q,\mathsf{vcol}^{\prime}}^{m})$. The value of
the state $q_{\mathsf{init}}$ in the game $\mathcal{G}_{Z}$ is at most
$u^{\prime}$ for some $u^{\prime}<u$:
$\chi_{\mathcal{G}_{Z}}[q_{\mathsf{init}}]\leq u^{\prime}<u$. Consider a
Player-$\mathsf{B}$ $\mathsf{GF}$-strategy $\sigma_{\mathsf{B}}$ that is
optimal w.r.t. $Z$. The Player-$\mathsf{B}$ strategy
$\mathsf{s}_{Z}^{\mathsf{B}}(\sigma_{\mathsf{B}})$ dominates the valuation
$v_{Z}^{u^{\prime}}=v_{Z^{\prime}}^{u^{\prime}}$. Consider an action
$a\in\mathsf{Act}_{\mathsf{A}}$ and assume that
$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[0,1]}\rangle}(a,\sigma_{\mathsf{B}})=0$.
We have $\max\mathsf{ColBSCC}(q,\mathsf{vcol},m,a,\sigma_{\mathsf{B}})$ odd
with
$j:=\max\mathsf{ColBSCC}(q,\mathsf{vcol},m,a,\sigma_{\mathsf{B}})\geq\max(\mathsf{vcol}(q),c_{m})$
for $c_{m}=m-1$ if $m$ is even and $c_{m}=m+1$ otherwise. Let us show that
$j\geq n$.

  * •

If $m$ is odd (and $n=m+2$), we have $c_{m}=m+1=n-1$ which is even. Hence,
$j\geq n$.

  * •

If $m=0$ (and $n=1$), since $j$ is odd, it must be that $j\geq n$.

  * •

If $m\geq 2$ is even (and therefore $n=m-2$), we have $c_{m}=m-1=n+1$. Hence,
we have $j\geq n+1$.

We can apply Lemma 68 to obtain that
$\max\mathsf{ColBSCC}(q,\mathsf{vcol}^{\prime},m,a,\sigma_{\mathsf{B}})=\max\mathsf{ColBSCC}(q,\mathsf{vcol},m,a,\sigma_{\mathsf{B}})$,
which is odd. As this holds for all $a\in\mathsf{Act}_{\mathsf{A}}$, we have
that the $\mathsf{GF}$-strategy $\sigma_{\mathsf{B}}$ strongly dominating the
valuation $v_{Z^{\prime}}^{u^{\prime}}$, hence, by Theorem 13, the value of
the state $q_{\mathsf{init}}$ in the game $\mathcal{G}_{Z^{\prime}}$ is at
most $u^{\prime}$: $\chi_{\mathcal{G}_{Z^{\prime}}}[q_{\mathsf{init}}]\leq
u^{\prime}$. Hence,
$\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})\prec_{\mathsf{par}}m$.

In any case, we have $n=\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})$.

###  D.2 Complete definition of faithfulness

We want to formally give the definition of faithfulness that we will use in
the proof. First, we define the notion of coherent coloring and environment
functions. Informally, for each state $q\in Q_{u}$: the colors given by the
coloring function correspond to the environment provided at each state (the
environments being defined from coloring functions as in Definition 34).

######  Definition 70 (Coherent coloring and environment functions).

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, some color $n\in\llbracket 0,e\rrbracket$ and let
$Q_{n}:=\mathsf{vcol}^{-1}[n]$. Consider an environment function
$\mathsf{Ev}:Q_{n}\rightarrow\mathsf{Env}(Q)$ and, for all $q\in Q_{n}$, let
$\mathsf{vcol}_{q}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$ be the coloring
function associated with the environment $\mathsf{Ev}(q)$. Let $q\in Q_{n}$.
We say that $(\mathsf{vcol},\mathsf{Ev})$ is _coherent_ at state $q$ if,
letting $n_{q}:=\mathsf{NewCol}(q,\mathsf{vcol}_{q})$:

  * •

$\mathsf{col}(q),\mathsf{vcol}_{q}(q),n_{q}\leq n$ and the coloring function
$\mathsf{vcol}$ is $n$-prevailing compared to the coloring function
$\mathsf{vcol}_{q}$;

  * •

$n\equiv n_{q}\mod 2$ and
$\mathsf{Ev}(q)=\mathsf{CreateEnv}(n_{q},q,\mathsf{vcol}_{q})$ where
$\mathsf{CreateEnv}$ corresponds to Algorithm 12.

If this holds for all $q\in Q_{n}$, $(\mathsf{vcol},\mathsf{Ev})$ is
_coherent_ at color $n$.

######  Definition 71 (Faithful pair of coloring and environment functions).

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, some $n\in\llbracket 0,e+1\rrbracket$ and a partial
environment function $\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$ defined on
$\mathsf{vcol}^{-1}[\llbracket n,e\rrbracket]$. We say that
$(\mathsf{vcol},\mathsf{Ev})$ is _faithful down to_ $n$ if:

  * 1f.

for all $k\in\llbracket n,e\rrbracket$, the pair $(\mathsf{vcol},\mathsf{Ev})$
witnesses the color $k$;

  * 2f.

for all $k\in\llbracket n,e\rrbracket$, the pair $(\mathsf{vcol},\mathsf{Ev})$
is coherent at color $k$;

  * 3f.

for all $q\in Q_{u}$, if $\mathsf{vcol}(q)<n$, then we have
$\mathsf{col}(q)=\mathsf{vcol}(q)$ and $\mathsf{NewCol}(q,\mathsf{vcol})<n$;

When $n=0$, we say that the pair $(\mathsf{vcol},\mathsf{Ev})$ is _completely
faithful_.

###  D.3 Three central lemmas

In the following, we state three lemmas that we will use in remainder of this
chapter. The first lemma relates probability distributions in a local game and
in a global game. This is particularly useful as it allows to use the
assumptions made on the local strategies to obtain various properties on
global games where such local strategies are used.

The second lemma states that any Player-$\mathsf{A}$ positional strategy
generated by an environment such that the new color (w.r.t. that environment)
is even dominates a specific valuation. This is similar for Player
$\mathsf{B}$.

Finally, the third lemma states that any Player-$\mathsf{A}$ local strategy
defined by local strategies that are optimal w.r.t. to an even color ensure
that in a BSCC $H$ compatible with such a strategy, if some high enough color
occurs in $H$, then $H$ is even-colored. This is similar for Player
$\mathsf{B}$.

######  Lemma 72.

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, some color $n\in\llbracket 0,e\rrbracket$ and a partial
environment function $\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$ defined
over $Q_{n}:=\mathsf{vcol}^{-1}[\\{n\\}]$. Let $q\in Q_{n}$ and
$\mathsf{vcol}_{q}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$ be the coloring
function associated with environment $\mathsf{Ev}(q)$. We also let
$p:=p_{q,\mathsf{vcol}_{q}}$. Then, for all Player-$\mathsf{A}$ and
Player-$\mathsf{B}$ strategies $\mathsf{s}_{\mathsf{A}}$ and
$\mathsf{s}_{\mathsf{B}}$ in the arena $\mathcal{C}_{\mathsf{vcol}}^{n}$, we
have:

$\forall x\in V_{Q\setminus
Q_{u}},\;\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[x]=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[x]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
(1)

and

$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{n}\cup
K^{n}]=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[\\{q_{\mathsf{init}}\\}\cup
K_{e}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$ (2)

Furthermore, if $\mathsf{vcol}$ is equivalent down to $n+1$ to
$\mathsf{vcol}_{q}$:

$\forall i\in\llbracket
n+1,e\rrbracket,\;\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[k_{i}^{n}]=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[k_{i}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
(3)

and if, in addition, $\mathsf{vcol}$ is $n$-prevailing compared to
$\mathsf{vcol}_{q}$:

$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[\mathsf{vcol}_{q}^{-1}[n]\setminus\\{q\\}]=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[k_{n}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
(4)

######  Proof.

By Definition 30, we have:

  * •

for all $q^{\prime}\in Q_{n}$,
$p_{n,\mathsf{vcol}}^{-1}[q^{\prime}]=\\{q^{\prime}\\}$;

  * •

for all $i\in\llbracket 0,e\rrbracket$:
$p_{n,\mathsf{vcol}}^{-1}[k_{i}^{n}]=\mathsf{vcol}^{-1}[i]\setminus Q_{n}$;

  * •

for all $x\in V_{Q\setminus Q_{u}}$, $p_{n,\mathsf{vcol}}^{-1}[x]=Q_{x}$.

Furthermore, from Definition 34, we have:

  * •

$p^{-1}[q_{\mathsf{init}}]=\\{q\\}$;

  * •

for all $i\in\llbracket 0,e\rrbracket$:
$p^{-1}[k_{i}]=\mathsf{vcol}^{-1}[i]\setminus\\{q\\}$;

  * •

for all $x\in V_{Q\setminus Q_{u}}$,
$p^{-1}[x]=Q_{x}=p_{n,\mathsf{vcol}}^{-1}[x]$.

By Definition 31, for all $x\in V_{Q\setminus Q_{u}}$. We have:

$\displaystyle\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}(x)$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p_{n,\mathsf{vcol}}^{-1}[x]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[x]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$

This proves Equation (1).

Furthermore, using this Equation for the second equality, we have:

$\displaystyle\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{n}\cup
K^{n}]$
$\displaystyle=1-\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[V_{Q\setminus
Q_{u}}]$
$\displaystyle=1-\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[V_{Q\setminus
Q_{u}}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),1-\mathbbm{1}_{p^{-1}[V_{Q\setminus
Q_{u}}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[\\{q_{\mathsf{init}}\\}\cup
K_{e}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$

This proves Equation (2).

Assume now that $\mathsf{vcol}$ is equivalent down to $n+1$ to
$\mathsf{vcol}_{q}$. Let $i\in\llbracket n+1,e\rrbracket$. We have
$\mathsf{vcol}^{-1}[i]=\mathsf{vcol}_{q}^{-1}[i]$ (recall Definition 67).
Furthermore, for all $q^{\prime}\in Q_{n}$, we have
$\mathsf{vcol}(q^{\prime})=n\neq i$. Hence, $\mathsf{vcol}^{-1}[i]\setminus
Q_{n}=\mathsf{vcol}^{-1}[i]=\mathsf{vcol}^{-1}[i]\setminus\\{q\\}$. Hence we
have, again by Definition 31, for all $i\in\llbracket n+1,e\rrbracket$:

$\displaystyle\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}(k_{i}^{n})$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p_{n,\mathsf{vcol}}^{-1}[k_{i}^{n}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathsf{vcol}^{-1}[i]\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[k_{i}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$

This gives Equation (3). Assume in addition that $\mathsf{vcol}$ is
$n$-prevailing compared to $\mathsf{vcol}_{q}$ (recall Definition 67). That
is, $\mathsf{vcol}_{q}^{-1}[n]\subseteq\mathsf{vcol}^{-1}[n]=Q_{n}$ . Hence,
$\mathsf{vcol}_{q}^{-1}[n]\setminus\\{q\\}\subseteq Q_{n}$. It follows that:

$\displaystyle\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[\mathsf{vcol}_{q}^{-1}[n]\setminus\\{q\\}]$
$\displaystyle=\sum_{q^{\prime}\in\mathsf{vcol}_{q}^{-1}[n]\setminus\\{q\\}}\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p_{n,\mathsf{vcol}}^{-1}[q^{\prime}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=\sum_{q^{\prime}\in\mathsf{vcol}_{q}^{-1}[n]\setminus\\{q\\}}\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{q^{\prime}}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{\mathsf{vcol}_{q}^{-1}[n]\setminus\\{q\\}}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[k_{n}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$

We obtain Equation (4).

######  Lemma 73.

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, some color $n\in\llbracket 0,e\rrbracket$ and let
$Q_{n}:=\mathsf{vcol}^{-1}[n]$. Consider an environment function
$\mathsf{Ev}:Q_{n}\rightarrow\mathsf{Env}(Q)$. Assume that
$(\mathsf{vcol},\mathsf{Ev})$ is coherent at color $n$. In the arena
$\mathcal{C}_{\mathsf{vcol}}^{n}$:

  * •

if $n$ is even, then all positional Player-$\mathsf{A}$ strategies generated
by the environment $\mathsf{Ev}$ dominate the valuation
$v_{n,\mathsf{vcol}}^{u}$ in the arena $\mathcal{C}^{n}_{\mathsf{vcol}}$ (see
Definition 40);

  * •

if $n$ is odd, then there is some $y<u$ such that, for all $z\geq y$, all
positional Player-$\mathsf{B}$ strategies generated by the environment
$\mathsf{Ev}$ dominate the valuation $v_{n,\mathsf{vcol}}^{z}$ in the arena
$\mathcal{C}^{n}_{\mathsf{vcol}}$ (see Definition 40).

######  Proof.

For all states $q\in Q_{n}$, we let
$\mathsf{vcol}_{q}:Q_{u}\rightarrow\llbracket 0,e\rrbracket$ be the coloring
function associated with the environment $\mathsf{Ev}(q)$ and we let
$p:=p_{q,\mathsf{vcol}_{q}}$. Let $q\in Q_{n}$. For all Player-$\mathsf{A}$
and $\mathsf{B}$ strategies $\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}$
in the arena $\mathcal{C}_{\mathsf{vcol}}^{n}$, for all $z\in[0,1]$, we have:

$\displaystyle\mathsf{out}_{\langle\mathsf{F}(q),v_{n,\mathsf{vcol}}^{z}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=z\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{n}\cup
K]+\sum_{x\in V_{Q\setminus
Q_{u}}}x\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}(x)$

Assume that $n$ is even and consider a Player-$\mathsf{A}$ positional strategy
$\mathsf{s}_{\mathsf{A}}$ generated by the environment function $\mathsf{Ev}$.
Letting $Y_{q}:=(\mathsf{F}(q),\mathsf{Ev}(q))$, in the game
$\mathcal{G}_{Y_{q}}$, the positional Player-$\mathsf{A}$ strategy
$\mathsf{s}_{Y_{q}}^{\mathsf{A}}(\mathsf{s}_{\mathsf{A}}(q))$ dominates the
valuation $v_{Y_{q}}^{u^{\prime}}$ for
$u^{\prime}:=\chi_{\mathcal{G}_{Y_{q}}}[q_{\mathsf{init}}]\geq u$ (recall
Lemma 21) since $(\mathsf{vcol},\mathsf{Ev})$ is coherent at color $n$. Hence:

$\displaystyle u^{\prime}$
$\displaystyle\leq\mathsf{out}_{\langle\mathsf{F}(q),v_{Y_{q}}^{u^{\prime}}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[\\{q_{\mathsf{init}}\\}\cup
K_{e}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))\cdot
u^{\prime}$ $\displaystyle+\sum_{x\in V_{Q\setminus
Q_{u}}}\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{p^{-1}[x]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))\cdot
x$
$\displaystyle=u^{\prime}\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{n}\cup\mathsf{K}^{n}]+\sum_{x\in
V_{Q\setminus
Q_{u}}}x\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[x]$

Then, we have (since $u^{\prime}\geq u$):

$\displaystyle u=u^{\prime}+(u-u^{\prime})$ $\displaystyle\leq
u^{\prime}\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{n}\cup
K^{n}]+\sum_{x\in V_{Q\setminus
Q_{u}}}x\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[x]+(u-u^{\prime})$
$\displaystyle\leq
u^{\prime}\cdot\mathbb{P}^{\mathcal{C}_{\mathsf{vcol}}^{n},q}_{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{n}\cup
K^{n}]+\sum_{x\in V_{Q\setminus
Q_{u}}}x\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[x]+(u-u^{\prime})\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{n}\cup
K^{n}]$
$\displaystyle=u\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{n}\cup
K^{n}]+\sum_{x\in V_{Q\setminus
Q_{u}}}x\cdot\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[x]$
$\displaystyle=\mathsf{out}_{\langle\mathsf{F}(q),v_{n,\mathsf{vcol}}^{u}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$

Since this holds for all Player-$\mathsf{B}$ positional strategies strategies
$\mathsf{s}_{\mathsf{B}}$ and for all $q\in Q_{n}$, it follows that the
Player-$\mathsf{A}$ strategy $\mathsf{s}_{\mathsf{A}}$ dominates the valuation
$v_{n,\mathsf{vcol}}^{u}$ in the arena $\mathcal{C}_{\mathsf{vcol}}^{n}$.

In the case where $n$ is odd, the proof is analogous, from
Player-$\mathsf{B}$’s point-of-view.

######  Lemma 74.

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, some $n\in\llbracket 0,e\rrbracket$ and
$Q_{n}:=\mathsf{vcol}^{-1}[\\{n\\}]$. Consider an environment function
$\mathsf{Ev}:Q_{n}\rightarrow\mathsf{Env}(Q)$ and assume that
$(\mathsf{vcol},\mathsf{Ev})$ is coherent at the color $n$. Then, denoting
$K^{\geq n}:=\\{k_{i}^{n}\mid i\in\llbracket n,e\rrbracket\\}$:

  * •

if $n$ is even, then in the arena $\mathcal{C}_{\mathsf{vcol}}^{n}$, all
positional Player-$\mathsf{A}$ strategies generated by the environment
$\mathsf{Ev}$ ensure that for all BSCCs $H$ compatible with
$\mathsf{s}_{\mathsf{A}}$, if $K^{\geq n}$ occurs in $H$, then $H$ is even-
colored;

  * •

if $n$ is odd, then in the arena $\mathcal{C}_{\mathsf{vcol}}^{n}$, all
positional Player-$\mathsf{B}$ strategies generated by the environment
$\mathsf{Ev}$ ensure that for all BSCCs $H$ compatible with
$\mathsf{s}_{\mathsf{B}}$, if $K^{\geq n}$ occurs in $H$, then $H$ is odd-
colored.

######  Proof.

Assume that $n$ is even and consider a Player-$\mathsf{A}$ positional strategy
$\mathsf{s}_{\mathsf{A}}$ generated by the environment $\mathsf{Ev}$ in the
game $\mathcal{L}^{n}_{\mathsf{vcol}}$ (recall Definition 31). Consider a
Player-$\mathsf{B}$ positional deterministic strategy
$\mathsf{s}_{\mathsf{B}}$ and consider a BSCC $H$ compatible with
$\mathsf{s}_{\mathsf{A}}$ and $\mathsf{s}_{\mathsf{B}}$.

For all $q\in Q_{n}$, let $\mathsf{vcol}_{q}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$ be the coloring function associated with the environment
$\mathsf{Ev}(q)$. Let $q\in Q_{n}$ and
$n_{q}:=\mathsf{NewCol}(q,\mathsf{vcol}_{q})$. Since
$(\mathsf{vcol},\mathsf{Ev})$ is coherent at $n$, $n_{q}$ is even and less
than or equal to $n$. Recall that
$\mathcal{G}_{q,\mathsf{vcol}}^{n_{q}}=\mathcal{G}_{Y_{q}}$, for
$Y_{q}:=(\mathsf{F}(q),E^{n_{q}}_{q,\mathsf{vcol}_{q}})$ (see Definition 34).
Recall also that
$E^{n_{q}}_{q,\mathsf{vcol}_{q}}=\langle\max(c_{n_{q}},\mathsf{vcol}_{q}(q)),e,p_{\\{q\\},\mathsf{vcol}_{q}}\rangle$
(also see Definition 34) with $c_{n_{q}}=n_{q}-1$ as $n_{q}$ is even. Let
$p^{q}:=p_{q,\mathsf{vcol}_{q}}$. Note that $p^{q}_{[0,1]}\subseteq
V_{Q\setminus Q_{u}}$ (recall Definition 34). By Equation
$(\ref{eqn:prob_in_V_Q_Q_u_equal})$ from Lemma 72, if $q$ is in $H$, then
$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{Q\setminus
Q_{u}}\rangle}(\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))=0$. In
that case, since the Player-$\mathsf{A}$ $\mathsf{GF}$-strategy
$\mathsf{s}_{\mathsf{A}}(q)$ is optimal w.r.t. $Y_{q}$ (recall Lemma 21), we
have the following.:

$\max(\mathsf{Color}(\mathsf{F}(q),p^{q},\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q)),n_{q}-1,\mathsf{vcol}_{q}(q))\text{
is even }$ (5)

Since $(\mathsf{vcol},\mathsf{Ev})$ is coherent (see Definition 70) at $n$, we
have $\mathsf{col}(q)\leq n$ for all $q\in Q_{n}$. Hence, our goal is to show
that:

$K^{\geq n}\text{ occurs in }H\Rightarrow\max M\text{ is even }$

with $M:=\\{i\in\llbracket n,e\rrbracket\mid k_{i}^{n}\text{ occurs in }H\\}$.

To prove this, we use the following characterization: for all colors
$i\in\llbracket n+1,e\rrbracket$, by Equation
$(\ref{eqn:prob_ki_if_equiv_equal})$ in Lemma 72 since $\mathsf{vcol}$ and
$\mathsf{vcol}_{q}$ are equivalent down to $n+1$, we have the following
equivalence:

$k_{i}^{n}\text{ occurs in }H\Leftrightarrow\exists q\in
H,\;i\in\mathsf{Color}(\mathsf{F}(q),p^{q},\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))$
(6)

Furthermore, for all $q\in H$, by assumption (the pair
$(\mathsf{vcol},\mathsf{Ev})$ being coherent), $\mathsf{vcol}_{q}(q)\leq n$.
Hence, since $n_{q}\leq n$, Equation (5) gives that, for all $q\in H$:

$\max\mathsf{Color}(\mathsf{F}(q),p^{q},\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))\geq
n+1\Rightarrow\max\mathsf{Color}(\mathsf{F}(q),p^{q},\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))\text{
is even }$ (7)

Furthermore, if $\max M=n$, then $n$ is the highest color appearing in $H$
(since $\mathsf{vcol}$ and $\mathsf{Ev}$ are coherent at $n$) and $H$ is then
even-colored. Otherwise:

$\displaystyle K^{\geq n}\text{ occurs in }H$ $\displaystyle\Leftrightarrow
M\neq\emptyset$ $\displaystyle\Rightarrow M\neq\emptyset\wedge k_{m}^{n}\text{
occurs in }H\text{ for }m:=\max M$ $\displaystyle\Rightarrow
M\neq\emptyset\wedge\exists q_{m}\in
H,\;m\in\mathsf{Color}(\mathsf{F}(q_{m}),p,\mathsf{s}_{\mathsf{A}}(q_{m}),\mathsf{s}_{\mathsf{B}}(q_{m}))$
by Equation (6) $\displaystyle\Rightarrow M\neq\emptyset\wedge\exists q_{m}\in
H,\;\max\mathsf{Color}(\mathsf{F}(q_{m}),p^{q_{m}},\mathsf{s}_{\mathsf{A}}(q_{m}),\mathsf{s}_{\mathsf{B}}(q_{m}))=m$
$\displaystyle\text{ since }m=\max M\text{ and by
Equation~{}(\ref{eqn:equiv_in_bscc}) }$ $\displaystyle\Rightarrow
M\neq\emptyset\wedge m=\max M\text{ is even }$ $\displaystyle\text{ since
}m\geq n+1\text{ and by Equation~{}(\ref{eqn:if_Iq_at_least_n_then_max_even})
}$

We obtain the desired result.

The case of $n$ odd is analogous by reversing the instances of ’odd’ and
’even’. However, the arguments for obtaining the analogue of Equation (5) is
slightly different. Indeed, letting
$Y_{q}:=(\mathsf{F}(q),E^{\mathsf{Succ}(n_{q})}_{\\{q\\},\mathsf{vcol}_{q}})$,
the Player-$\mathsf{B}$ $\mathsf{GF}$-strategy $\mathsf{s}_{\mathsf{B}}(q)$ is
optimal w.r.t. $Y_{q}$ (recall Lemma 21 and the definition of
$\mathsf{CreateEnv}$ (i.e. Algorithm 12)). Recall that
$E^{\mathsf{Succ}(n_{q})}_{\\{q\\},\mathsf{vcol}_{q}}=\langle\max(c_{\mathsf{Succ}(n_{q})},\mathsf{vcol}_{q}(q)),e,\mathsf{vcol}_{q}\rangle$
where $c_{\mathsf{Succ}(n_{q})}=-1$ if $n_{q}=1$ and
$c_{\mathsf{Succ}(n_{q})}=n_{q}-1$ otherwise (i.e. if $n_{q}\geq 3$). Overall,
from Lemma 21, we do obtain:

$\max(\mathsf{Color}(\mathsf{F}(q),p,\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q)),n_{q}-1,\mathsf{vcol}_{q}(q))\text{
is odd }$ (8)

with $n_{q}-1$ even.

###  D.4 Proof of Lemma 44, Page 44

Let us define a notion which is slightly weaker then being faithful: being
non-deceiving.

######  Definition 75 (Non-deceiving environment and coloring functions).

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, a partial environment function
$\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$ and some color $n\in\llbracket
0,e+1\rrbracket$. We say that the pair $(\mathsf{vcol},\mathsf{Ev})$ is _non-
deceiving down to_ $n$ if:

  * 1n-d.

for all $k\in\llbracket n,e\rrbracket$, the pair $(\mathsf{vcol},\mathsf{Ev})$
witnesses the color $k$;

  * 2n-d.

for all $k\in\llbracket n,e\rrbracket$, the pair $(\mathsf{vcol},\mathsf{Ev})$
is coherent at color $k$;

  * 3n-d.

for all $q\in Q_{u}$, if $\mathsf{vcol}(q)<n$, then we have
$\mathsf{col}(q)=\mathsf{vcol}(q)$ and $\mathsf{NewCol}(q,\mathsf{vcol})\leq
n$.

The difference with being faithful lies in the fact that some state $q\in
Q_{u}$ with $\mathsf{vcol}(q)<n$ could be such that
$\mathsf{NewCol}(q,\mathsf{vcol})=n$ (which is not possible with a faithful
pair). When $n=0$, being non-deceiving down to $n$ is equivalent to being
faithful down to $n$ (i.e. to being completely faithful).

Then, Algorithm 15 is composed of Algorithm 13 and Algorithm 14. In fact,
Algorithm 13 transforms a faithful pair into a non-deceiving one (one level
below). And Algorithm 14 transforms a non-deceiving pair into a faithful one
(at the same level). We state one lemma per algorithm formally stating the
specifications of these algorithms.

######  Lemma 76.

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, some color $n\in\llbracket 1,e+1\rrbracket$ and a partial
environment function $\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$ defined on
$\mathsf{vcol}^{-1}[\llbracket n,e\rrbracket]$. Assume that
$(\mathsf{vcol},\mathsf{Ev})$ is faithful down to $n$. Let
$\mathsf{Ev}^{\prime}\leftarrow\mathsf{UpdCurSta}(n-1,\mathsf{vcol},\mathsf{Ev})$.
Then, $(\mathsf{vcol},\mathsf{Ev}^{\prime})$ is non-deceiving down to $n-1$.

######  Proof.

For all $q\in Q_{u}$, such that $\mathsf{vcol}(q)\geq n-1$, we denote by
$\mathsf{vcol}_{q}$ the coloring function corresponding to the environment
$\mathsf{Ev}^{\prime}(q)$.

  * 2n-d.

Let us show that $(\mathsf{vcol},\mathsf{Ev}^{\prime})$ is coherent at $n-1$.
We let $Q_{n-1}:=\mathsf{vcol}^{-1}[n-1]$ and $q\in Q_{n-1}$. Since
$(\mathsf{vcol},\mathsf{Ev})$ is faithful down to $n$, we have
$\mathsf{vcol}(q)=\mathsf{col}(q)=n-1$. Furthermore,
$\mathsf{vcol}_{q}=\mathsf{vcol}$. Hence,
$\mathsf{vcol}_{q}(q)=\mathsf{col}(q)=n-1$. In addition, since the pair
$(\mathsf{vcol},\mathsf{Ev})$ is faithful down to $n$, we have
$\mathsf{NewCol}(q,\mathsf{vcol})<n$. By Proposition 66, we have
$n-1=\mathsf{vcol}(q)\leq\mathsf{NewCol}(q,\mathsf{vcol})<n$. Hence,
$\mathsf{vcol}(q)=\mathsf{NewCol}(q,\mathsf{vcol})=n-1$. By definition of
Algorithm 12, we have
$\mathsf{Ev}^{\prime}(q)=\mathsf{CreateEnv}(n-1,q,\mathsf{vcol})$. As this
holds for all $q\in Q_{n-1}$, $(\mathsf{vcol},\mathsf{Ev})$ is coherent at
$n-1$.

  * 3n-d.

This condition straightforwardly holds since the coloring function has not
changed and the pair $(\mathsf{vcol},\mathsf{Ev})$ is faithful down to $n$.

  * 1n-d.

This condition straightforwardly holds for $k\geq n$ since the pair
$(\mathsf{vcol},\mathsf{Ev})$ is faithful down to $n$. Note that since
$(\mathsf{vcol},\mathsf{Ev}^{\prime})$ is coherent at $n-1$, both Lemma 73 and
Lemma 74 can be applied to $(\mathsf{vcol},\mathsf{Ev}^{\prime})$ at $n-1$.

Assume that $n-1$ is even. Consider a Player-$\mathsf{A}$ positional strategy
$\mathsf{s}_{\mathsf{A}}$ generated by the environment $\mathsf{Ev}$ in the
game $\mathcal{L}^{n-1}_{\mathsf{vcol}}$. By Lemma 73, this strategy dominates
the valuation $v_{n-1,\mathsf{vcol}}^{u}$ in the arena
$\mathcal{C}_{\mathsf{vcol}}^{n-1}$. Consider a Player-$\mathsf{B}$ positional
deterministic strategy $\mathsf{s}_{\mathsf{B}}$ and consider a BSCC $H$ in
$\mathcal{C}_{\mathsf{vcol}}^{n-1}$ compatible with $\mathsf{s}_{\mathsf{A}}$
and $\mathsf{s}_{\mathsf{B}}$. By Lemma 74, if $K^{\geq n-1}$ occurs in $H$,
then $H$ is even-colored. Assume now that $K^{\geq n-1}$ does not occur in
$H$. In that case, there are some states in $H$ in
$Q_{n-1}\subseteq\mathsf{col}^{-1}[n-1]$ and possibly some states in
$\\{k_{i}^{n-1}\mid i\in\llbracket 0,n-2\rrbracket\\}$ occur in $H$ with
$\mathsf{vcol}_{n-1}(k_{i}^{n-1})=n-2$ for all $i\in\llbracket
0,n-2\rrbracket$ and $\mathsf{vcol}_{n-1}[Q_{n-1}]=\\{n-1\\}$. Hence, the
highest color appearing in $H$ is $n-1$ and therefore $H$ is even-colored.
Thus, $\mathsf{s}_{\mathsf{A}}$ parity dominates the valuation
$v_{n-1,\mathsf{vcol}}^{u}$.

The case where $n-1$ is odd is analogous, from Player-$\mathsf{B}$’s point-of-
view.

######  Lemma 77.

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, some color $n\in\llbracket 0,e\rrbracket$, and a partial
environment function $\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$ defined on
$\llbracket n,e\rrbracket$. Assume that the pair $(\mathsf{vcol},\mathsf{Ev})$
is non-deceiving down to $n$. Let
$(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})\leftarrow\mathsf{UpdNewSta}(n,\mathsf{vcol},\mathsf{Ev})$.
Then, $(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$ is faithful down to $n$.

######  Proof.

For all $q\in Q_{u}$ such that $\mathsf{vcol}(q)\geq n$, we denote by
$\mathsf{vcol}_{q}$ the coloring function associated with the environment
$\mathsf{Ev}^{\prime}(q)$. Let $Q_{n}:=(\mathsf{vcol}^{\prime})^{-1}[n]$.

  * 2f.

For all $k\in\llbracket n+1,e\rrbracket$, the pair
$(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$ is coherent at $k$ since the
pair $(\mathsf{vcol},\mathsf{Ev})$ is non-deceiving down to $n$. Now, let
$q\in Q_{n}$. If $\mathsf{vcol}(q)=n$, then straightforwardly,
$(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$ is coherent at state $q$ since
$(\mathsf{vcol},\mathsf{Ev})$ is non-deceiving down to $n$, hence
$\mathsf{vcol}$ is $n$-prevailing compared to $\mathsf{vcol}_{q}$ and
$\mathsf{vcol}^{\prime}$ is also $n$-prevailing compared to $\mathsf{vcol}$.
Consider now a state $q\in Q_{n}$ such that $\mathsf{vcol}(q)<n$. By
definition of Algorithm 14, we have
$\mathsf{vcol}(q)=\mathsf{vcol}_{q}(q)\leq\mathsf{NewCol}(q,\mathsf{vcol}_{q})=n$
(by Proposition 66). That is, $\mathsf{vcol}_{q}(q)\leq n-1$. Since
$(\mathsf{vcol},\mathsf{Ev})$ is non-deceiving down to $n$, we have
$\mathsf{col}(q)=\mathsf{vcol}(q)=\mathsf{vcol}_{q}(q)\leq n-1$. Furthermore,
by definition of Algorithm 14, the colors of the states in
$\mathsf{vcol}^{-1}[\llbracket n,e\rrbracket]$ is not changed and more and
more states are colored with $n$. Hence, $\mathsf{vcol}^{\prime}$ is
$n$-prevailing compared to $\mathsf{vcol}_{q}$. In addition,
$n=\mathsf{NewCol}(q,\mathsf{vcol}_{q})$ and
$\mathsf{Ev}(q)=\mathsf{CreateEnv}(n,q,\mathsf{vcol}_{q})$. It follows that
the pair $(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$ is coherent at state
$q$, and this holds for all $q\in Q_{n}$.

  * 3f.

By definition of Algorithm 14, for all $k<n$ and state $q\in Q_{u}$ such that
$\mathsf{vcol}^{\prime}(q)=k$, we have
$\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})\neq n$ and
$\mathsf{vcol}^{\prime}(q)=\mathsf{vcol}(q)=\mathsf{col}(q)$ (since
$(\mathsf{vcol},\mathsf{Ev})$ is non-deceiving down to $n$). Furthermore,
assume towards a contradiction that a state $q\in Q_{u}$ is such that
$\mathsf{vcol}^{\prime}(q)=k=\mathsf{vcol}(q)$ and
$\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})=m>n$. In that case, by Proposition
69, since $\mathsf{vcol}$ and $\mathsf{vcol}^{\prime}$ are equivalent down to
$m$, we would have $\mathsf{NewCol}(q,\mathsf{vcol})=m>n$, which is not
possible since $(\mathsf{vcol},\mathsf{Ev})$ is non-deceiving down to $n$. In
fact, $\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})<n$.

  * 1f.

Let $k\geq n+1$. We have
$\mathsf{vcol}^{-1}[k]=(\mathsf{vcol}^{\prime})^{-1}[k]$ and for all
$q\in\mathsf{vcol}^{-1}[k]$, we have $\mathsf{Ev}(q)=\mathsf{Ev}^{\prime}(q)$.
Hence, the first condition for faithfulness holds for $k$ since
$(\mathsf{vcol},\mathsf{Ev})$ is non-deceiving down to $n$. We consider now
the case where $k=n$. Assume that $n$ is even. Consider a Player-$\mathsf{A}$
positional strategy $\mathsf{s}_{\mathsf{A}}$ generated by the environment
function $\mathsf{Ev}$ in the game $\mathcal{L}^{n}_{\mathsf{vcol}^{\prime}}$.
Let us show that this strategy parity dominates the valuation
$v_{n,\mathsf{vcol}^{\prime}}^{u}$ in the game
$\mathcal{L}^{n}_{\mathsf{vcol}^{\prime}}$. By Lemma 73, this strategy
dominates the valuation $v_{n,\mathsf{vcol}^{\prime}}^{u}$. Now, fix a
Player-$\mathsf{B}$ positional deterministic strategy
$\mathsf{s}_{\mathsf{B}}$ and consider a BSCC $H$ compatible with
$\mathsf{s}_{\mathsf{A}}$ and $\mathsf{s}_{\mathsf{B}}$ in
$\mathcal{L}^{n}_{\mathsf{vcol}^{\prime}}$. If $K^{\geq n}$ occurs in $H$,
then by Lemma 74, the BSCC $H$ is even-colored. Assume now that $K^{\geq n}$
does not occur in $H$. Let $X_{n}^{0}:=\mathsf{vcol}^{-1}[n]$ and let
$j:=|Q_{n}|-|X_{n}^{0}|$. For all $1\leq i\leq j$, we denote by $q_{i}$ the
$i$-th element of $Q_{n}$ whose color was changed by Algorithm 14 and
$X_{n}^{i}:=X_{n}^{0}\cup\cup_{1\leq k\leq i}\\{q_{i}\\}$. In particular,
$X_{n}^{j}=Q_{n}$ and:

$\forall i\in\llbracket
1,j\rrbracket,\;\mathsf{vcol}_{q_{i}}^{-1}[n]=X_{n}^{i-1}$ (9)

First, assume that $H\subseteq X_{n}^{0}$. In that case, this is a BSCC
compatible with the strategy $\mathsf{s}_{\mathsf{A}}$ in the game
$\mathcal{L}^{n}_{\mathsf{vcol}}$ in which this strategy, by assumption,
parity dominates the valuation $v_{n,\mathsf{vcol}}^{u}$. Hence, this BSCC is
even-colored. Second, assume that $H\not\subseteq X_{n}^{0}$ and let
$C_{n}:=Q_{n}\cap\mathsf{col}^{-1}[n]$. For all $i\in\llbracket
0,j\rrbracket$, let $H_{i}:=H\cap X_{n}^{i}$. Let us show by induction on
$i\in\llbracket 0,j\rrbracket$ the following property $\mathcal{P}(i)$: for
all $q\in H_{i}\setminus C_{n}$, there is a positive probability to visit
$C_{n}$ from $q$ while only visiting states in $H_{i}$, that is:

$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[H_{i}^{*}\cdot
C_{n}]>0$

Assume towards a contradiction that $\mathcal{P}(0)$ does not hold. That is,
there is some $q\in H_{0}\setminus C_{n}$ such that
$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[H_{0}^{*}\cdot
C_{n}]=0$. Let $Z\subseteq H_{0}$ be the set of states in $H_{0}$ defined by
$Z:=\\{q\\}\cup\\{q^{\prime}\in
H_{0}\mid\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[H_{0}^{*}\cdot
q^{\prime}]>0\\}$. Note that $Z\cap C_{n}=\emptyset$. Our goal is now to
exhibit a BSCC in $\mathcal{L}^{n}_{\mathsf{vcol}}$ that is compatible with
$\mathsf{s}_{\mathsf{A}}$ and that is odd-colored. This will be a
contradiction with the fact that $\mathsf{s}_{\mathsf{A}}$ parity dominates
the valuation $v_{n,\mathsf{vcol}}^{u}$ in the game
$\mathcal{L}^{n}_{\mathsf{vcol}}$. Consider a Player-$\mathsf{B}$ strategy
$\mathsf{s}_{\mathsf{B}}^{\prime}$ such that, for all $q^{\prime}\in
X_{n}^{0}=\mathsf{vcol}^{-1}[n]$,
$\mathsf{s}_{\mathsf{B}}^{\prime}(q^{\prime}):=\mathsf{s}_{\mathsf{B}}(q^{\prime})$
and for all $i\in\llbracket 0,n-1\rrbracket$, we have
$\mathsf{s}_{\mathsf{B}}(k_{i}^{n})$ playing deterministically to reach $q$.
By construction, we do have a BSCC $H^{\prime}$ compatible with
$\mathsf{s}_{\mathsf{A}}$ and $\mathsf{s}_{\mathsf{B}}^{\prime}$ in
$\mathcal{L}^{n}_{\mathsf{vcol}}$ that is included in $Z\cup\\{k_{i}^{n}\mid
i\in\llbracket 0,n-1\rrbracket\\}$. Furthermore, since the BSCC $H$ in the
game $\mathcal{L}^{n}_{\mathsf{vcol}^{\prime}}$ is not equal to $H_{0}$
(because this would imply $H\subseteq X_{n}^{0}$), it must be that at least
one state in $\\{k_{i}^{n}\mid i\in\llbracket 0,n-1\rrbracket\\}$ is in
$H^{\prime}$ (recall that in the game $\mathcal{L}^{n}_{\mathsf{vcol}}$ any
edge leading to a state in $Q_{u}\setminus X_{n}^{0}$ in $\mathcal{G}$ leads
to a state in $\\{k_{i}^{n}\mid i\in\llbracket 0,e\rrbracket\\}$). Then, since
each state in $\\{k_{i}^{n}\mid i\in\llbracket 0,n-1\rrbracket\\}$ is colored
with $n-1$ and no state in $Z$ is in $C_{n}$, it follows that the highest
color in $H$ is $n-1$, which is odd. That is, the BSCC $H^{\prime}$ his odd-
colored, which is a contradiction. In fact, $\mathcal{P}(0)$ holds.

Assume now that $\mathcal{P}(i)$ holds for some $0\leq i\leq j-1$. Consider
some state $q\in H_{i+1}\setminus C_{n}$. If $q\in H_{i}$, then we can apply
$\mathcal{P}(i)$. Assume now that $q\notin H_{i}$, that is $q\notin
X^{i}_{n}$. Hence, $q=q_{i+1}$. Since $q\notin C_{n}$, we have
$\mathsf{col}(q)\neq n$, and therefore $\mathsf{col}(q)\leq n-1$555We have
shown that $(\mathsf{vcol},\mathsf{Ev})$ is coherent at $n$, hence all states
in $Q_{n}$ are such that $\mathsf{col}(q)\leq n$.. Furthermore, letting
$Y_{q}:=(\mathsf{F}(q),E^{n}_{\\{q\\},\mathsf{vcol}_{q}})$, the
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy $\mathsf{s}_{\mathsf{A}}(q)$ is
optimal w.r.t. $Y_{q}$ (recall Lemma 21). Hence, letting
$p^{q}:=p_{q,\mathsf{vcol}_{q}}$, we have:

$\max(\mathsf{Color}(\mathsf{F}(q),p^{q},\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q)),n-1)\text{
is even }$ (10)

with $n-1$ odd. Recall that
$\mathsf{Color}(\mathsf{F}(q),p^{q},\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q)):=\\{i\in\llbracket
0,e\rrbracket\mid\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{(p^{q})^{-1}[k_{i}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),b)>0\\}$.
In addition, since we assume that $K^{\geq n}$ does not occur in $H$, it
follows that we have
$\max\mathsf{Color}(\mathsf{F}(q),p^{q},\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))\leq
n$ by Equation (3) from Lemma 72. We can conclude that we have
$\max\mathsf{Color}(\mathsf{F}(q),p^{q},\mathsf{s}_{\mathsf{A}}(q),\mathsf{s}_{\mathsf{B}}(q))=n$.
Hence, by definition, we have that
$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{(p^{q})^{-1}[k_{n}]}\rangle}(\mathsf{s}_{\mathsf{A}}(q),b)>0$.
It follows that, by Equation (4) in Lemma 72 and since
$\mathsf{vcol}^{\prime}$ is $n$-prevailing compared to $\mathsf{vcol}_{q}$, we
have
$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[\mathsf{vcol}_{q}^{-1}[n]\setminus\\{q\\}]>0$.
Since $\mathsf{vcol}_{q}^{-1}[n]=X^{i}_{n}$ (by Equation 9), this is
equivalent to:
$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[X_{n}^{i}]>0$.
That is, from $q$, there is a positive probability to reach a state
$q^{\prime}\in X_{n}^{i}$ for which, by $\mathcal{P}(i)$, we have:
$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q^{\prime}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[H_{i}^{*}\cdot
C_{n}]>0$. It follows that
$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[H_{i+1}^{*}\cdot
C_{n}]>0$ and $\mathcal{P}(i+1)$ holds. We can conclude that from all states
in $H$ there is a positive probability to reach $C_{n}$, that is $H\cap
C_{n}\neq\emptyset$. Hence, $n$ is the highest color in $H$ and it is even.
Thus, $H$ is even-colored.

The case where $n$ is odd is symmetrical, from Player-$\mathsf{B}$’s point-of-
view.

The proof of Lemma 44 is now straightforward.

######  Proof.

By Lemma 76, we have $(\mathsf{vcol},\mathsf{Ev}^{\prime})$ non-deceiving down
to $n-1$. Then, by Lemma 77, the pair of coloring and environment functions
that Algorithm UpdNewSta (i.e. Algorithm 14) outputs is faithful down to
$n-1$.

###  D.5 Proof of Lemma 47, Page 47

######  Proof.

We let $C:=\mathsf{vcol}[Q]$, $k:=\min C$ and we assume that $k\leq e-2$.

Let us consider $(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$ to be the new
environment and coloring functions obtained with Algorithm 16 before calling
Algorithm 14. Let us show that $(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$
is non-deceiving down to $n:=k+2$. First, note that $\mathsf{vcol}^{\prime}$
is $n$-prevailing compared to $\mathsf{vcol}$. Let
$Q_{n}:=(\mathsf{vcol}^{\prime})^{-1}[n]$. For all $q\in Q_{n}$, we let
$\mathsf{vcol}_{q}$ be the virtual coloring function associated with the
environment $\mathsf{Ev}^{\prime}(q)$.

  * 2n-d.

Let $q\in Q_{n}$. We have either $\mathsf{vcol}(q)=n-2$ or
$\mathsf{vcol}(q)=n$. In both cases, since $(\mathsf{vcol},\mathsf{Ev})$ is
completely faithful and therefore coherent at colors $n-2$ and $n$, it holds
that $\mathsf{col}(q)\leq n$, $\mathsf{vcol}_{q}(q)\leq n$, $n_{q}\leq n$
(with $n_{q}:=\mathsf{NewCol}(q,\mathsf{vcol})$). Furthermore,
$\mathsf{vcol}^{\prime}$ is $n$-prevailing compared to $\mathsf{vcol}$, which
is $n$-prevailing compared to $\mathsf{vcol}_{q}$. Finally, $n\equiv n-2\mod
2$ and therefore this condition for being non-deceiving holds.

  * 3n-d.

This condition for being non-deceiving also straightforwardly holds. Indeed,
assume towards a contradiction that a state $q\in Q_{u}$ such that
$\mathsf{col}(q)=k=\mathsf{vcol}^{\prime}(q)<n$ is such that
$\mathsf{NewCol}(q,\mathsf{vcol}^{\prime})=m>n$. We have $\mathsf{vcol}$ that
is equivalent down to $m$ to $\mathsf{vcol}^{\prime}$. This implies by Lemma
69, that we have $\mathsf{NewCol}(q,\mathsf{vcol})=m>n$, which is not possible
since $(\mathsf{vcol},\mathsf{Ev})$ is assumed completely faithful.

  * 1n-d.

Consider now the first condition for being non-deceiving. It holds for all
$k>n$, since $\mathsf{vcol}^{-1}[k]=(\mathsf{vcol}^{\prime})^{-1}[k]$, and in
both games $\mathcal{L}_{\mathsf{vcol}}^{k}$ and
$\mathcal{L}_{\mathsf{vcol}^{\prime}}^{k}$, the states in
$\mathsf{vcol}^{-1}[\llbracket
0,k-1\rrbracket]=\mathsf{vcol}^{\prime-1}[\llbracket 0,k-1\rrbracket]$ are
colored with $k-1$.

Assume that $n$ is even. Consider a Player-$\mathsf{A}$ positional strategy
$\mathsf{s}_{\mathsf{A}}$ generated by the environment function $\mathsf{Ev}$
in the game $\mathcal{L}^{n}_{\mathsf{vcol}^{\prime}}$. Let us show that this
strategy parity dominates the valuation $v_{n,\mathsf{vcol}^{\prime}}^{u}$ in
the game $\mathcal{L}^{n}_{\mathsf{vcol}^{\prime}}$. By Lemma 73, this
strategy dominates the valuation $v_{n,\mathsf{vcol}^{\prime}}^{u}$. Now, fix
a Player-$\mathsf{B}$ positional deterministic strategy
$\mathsf{s}_{\mathsf{B}}$ and consider a BSCC $H$ compatible with
$\mathsf{s}_{\mathsf{A}}$ and $\mathsf{s}_{\mathsf{B}}$ in
$\mathcal{L}^{n}_{\mathsf{vcol}^{\prime}}$. If $K^{\geq n}$ occurs in $H$, by
Lemma 74, $H$ is even-colored. Assume now that $K^{\geq n}$ does not occur in
$H$. Let $S_{n}:=(\mathsf{vcol})^{-1}[n]$ (before running the algorithm, the
set colored by $n$) and $T_{n}:=Q_{n}\setminus S_{n}=\mathsf{vcol}^{-1}[n-2]$
(before running the algorithm, the set colored by $n-2$). Assume that $H\cap
S_{n}=\emptyset$. In that case, this is a BSCC compatible with the strategy
$\mathsf{s}_{\mathsf{A}}$ in the game $\mathcal{L}^{n-2}_{\mathsf{vcol}}$ in
which this strategy, by assumption, parity dominates the valuation
$v_{n-2,\mathsf{vcol}}^{u}$. Furthermore, consider the state $k_{n-1}^{n}$ in
$\mathcal{L}^{n}_{\mathsf{vcol}}$ and the state $k_{n-1}^{n-2}$ in
$\mathcal{L}^{n-2}_{\mathsf{vcol}}$. These states are colored by $n-1$ and
exactly the same edges in both games $\mathcal{L}^{n}_{\mathsf{vcol}}$ and
$\mathcal{L}^{n-2}_{\mathsf{vcol}}$ lead to these states. (These correspond to
the states $q\in Q_{u}$ such that $\mathsf{vcol}(q)=n-1$.) Hence, since the
BSCC $H$ is even-colored in $\mathcal{L}^{n-2}_{\mathsf{vcol}}$, it also is in
$\mathcal{L}^{n}_{\mathsf{vcol}}$666Note that this is why we increase the
least color, and not an intermediate color. Indeed, if there were a state
colored by the coloring function $\mathsf{vcol}$ by $n-3$, then the state
$k_{n-3}^{n-2}$ would be colored by $n-3$ in
$\mathcal{L}^{n-2}_{\mathsf{vcol}}$, whereas its counterpart $k_{n-3}^{n}$
would be colored by $n-1$ in $\mathcal{L}^{n}_{\mathsf{vcol}}$. Hence, we
could not deduce anymore that since the BSCC $H$ is even-colored in
$\mathcal{L}^{n-2}_{\mathsf{vcol}}$, it also is in
$\mathcal{L}^{n}_{\mathsf{vcol}}$.. Assume now that $H\cap T_{n}=\emptyset$.
In that case, this is a BSCC compatible with the strategy
$\mathsf{s}_{\mathsf{A}}$ in the game $\mathcal{L}^{n}_{\mathsf{vcol}}$ in
which this strategy, by assumption, parity dominates the valuation
$v_{n,\mathsf{vcol}}^{u}$. Hence, this BSCC is even-colored. Finally, assume
that $H\cap T_{n}\neq\emptyset$ and $H\cap S_{n}\neq\emptyset$. Let
$C_{n}:=Q_{n}\cap\mathsf{col}^{-1}[n]$. Let us show that for all $q\in(H\cap
S_{n})\setminus C_{n}$, there is a positive probability to visit $C_{n}$ from
$q$ while only visiting states in $H\cap S_{n}$, that is:

$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[(H\cap
S_{n})^{*}\cdot C_{n}]>0$

Assume towards a contradiction that this does not hold. That is, there is some
$q\in(H\cap S_{n})\setminus C_{n}$ such that
$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[(H\cap
S_{n})^{*}\cdot C_{n}]=0$. Let $Z\subseteq H\cap S_{n}$ be the set of states
in $H\cap S_{n}$ such that $Z:=\\{q\\}\cup\\{q^{\prime}\in H\cap
S_{n}\mid\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[(H\cap
S_{n})^{*}\cdot q^{\prime}]>0\\}$. Note that $Z\cap C_{n}=\emptyset$. Our goal
is now to exhibit a BSCC in $\mathcal{L}^{n}_{\mathsf{vcol}}$ that is
compatible with $\mathsf{s}_{\mathsf{A}}$ and odd-colored. This would be a
contradiction with the fact that $\mathsf{s}_{\mathsf{A}}$ parity dominates
the valuation $v_{n,\mathsf{vcol}}^{u}$ in the game
$\mathcal{L}^{n}_{\mathsf{vcol}}$. Consider a Player-$\mathsf{B}$ strategy
$\mathsf{s}_{\mathsf{B}}^{\prime}$ such that, for all $q\in S_{n}$,
$\mathsf{s}_{\mathsf{B}}^{\prime}(q):=\mathsf{s}_{\mathsf{B}}(q)$ and for all
$i\in\llbracket 0,n-1\rrbracket$, we have $\mathsf{s}_{\mathsf{B}}(k_{i}^{n})$
playing in a deterministic way to reach $q$. By construction, we do have a
BSCC $H^{\prime}$ compatible with $\mathsf{s}_{\mathsf{A}}$ and
$\mathsf{s}_{\mathsf{B}}^{\prime}$ in $\mathcal{L}^{n}_{\mathsf{vcol}}$ that
is included in $Z\cup\\{k_{i}^{n}\mid i\in\llbracket 0,n-1\rrbracket\\}$.
Furthermore, since the BSCC $H$ in the game
$\mathcal{L}^{n}_{\mathsf{vcol}^{\prime}}$ is not equal to $H\cap S_{n}$, it
must be that at least one state in $\\{k_{i}^{n}\mid i\in\llbracket
0,n-1\rrbracket\\}$ is in $H^{\prime}$. Then, since each state in
$\\{k_{i}^{n}\mid i\in\llbracket 0,n-1\rrbracket\\}$ is colored with $n-1$ and
no state in $Z$ is in $C_{n}$, it follows that the highest color in
$H^{\prime}$ is $n-1$, which is odd. That is, the BSCC $H^{\prime}$ is odd-
colored. This is a contradiction. In fact, from all states $q\in(H\cap
S_{n})\setminus C_{n}$, we have
$\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}^{\prime}}^{n},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[(H\cap
S_{n})^{*}\cdot C_{n}]>0$. Furthermore, the colors of all states in $H$ are at
most $n$ (recall what we shown above in 2n-d). Hence, the highest color in $H$
is $n$, which is even (the color of the states in $C_{n}$). Therefore the BSCC
$H$ is even-colored. That is, the Player-$\mathsf{A}$ strategy
$\mathsf{s}_{\mathsf{A}}$ parity dominates the valuation
$v_{n,\mathsf{vcol}^{\prime}}^{u}$ in the game
$\mathcal{L}^{n}_{\mathsf{vcol}^{\prime}}$.

The case where $n$ is odd is identical.

Hence, the pair $(\mathsf{vcol}^{\prime},\mathsf{Ev}^{\prime})$ is non-
deceiving down to $n$. The result then follows from Lemma 77.

###  D.6 Proof of Lemma 48, Page 48

Let us first introduce a way to build games with stopping states.

######  Definition 78.

Consider a parity game $\mathcal{G}$. For all subsets of states $S\subseteq
Q$, we denote by $\mathcal{G}^{S}$ the game $\mathcal{G}$ restricted to $S$
where all states in $Q\setminus S$ are stopping states with, for all $q\in
Q\setminus S$, $q\leftarrow\chi_{\mathcal{G}}[q]$. (In particular, the set of
states in $\mathcal{G}$ and $\mathcal{G}^{S}$ is the same.)

For all $x\in[0,1]$, we also let $v_{S}^{x}:Q\rightarrow[0,1]$ such that
$\left.v_{S}^{x}\right|_{Q\setminus
S}:=\left.\chi_{\mathcal{G}}\right|_{Q\setminus S}$ and
$v_{S}^{x}[S]:=\\{x\\}$.

######  Lemma 79.

Consider a parity game $\mathcal{G}$ and a subset of states $S\subseteq Q$.
Then: $\chi_{\mathcal{G}}=\chi_{\mathcal{G}^{S}}$.

######  Proof.

The equality straightforwardly holds for all $q\in Q\setminus S$. Consider now
a state $q\in S$. Let $\varepsilon>0$ and let $\mathsf{s}_{\mathsf{A}}$ be a
Player-$\mathsf{A}$ strategy that is $\varepsilon$-optimal from $q$ in the
game $\mathcal{G}$. This strategy can be seen as a strategy in the game
$\mathcal{G}^{S}$, the game ending as soon as the set $Q\setminus S$ is
reached. Consider any Player-$\mathsf{B}$ strategy $\mathsf{s}_{\mathsf{B}}$
in the game $\mathcal{G}^{S}$. Since the games $\mathcal{G}$ and
$\mathcal{G}^{S}$ coincide on $S^{*}$ (and $S^{\omega}$) and considering a
Player-$\mathsf{B}$ strategy $\mathsf{s}_{\mathsf{B}}^{\prime}$ in the game
$\mathcal{G}$ that coincides with the strategy $\mathsf{s}_{\mathsf{B}}$ on
$S^{*}$ and that plays a $\varepsilon$-optimal strategy as soon as a state in
$Q\setminus S$ is reached. We have:

$\displaystyle\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}_{\mathcal{C}^{S},q}[W(\mathsf{col})]$
$\displaystyle=\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}_{\mathcal{C}^{S},q}[W(\mathsf{col})\cap
S^{\omega}]+\sum_{q^{\prime}\in Q\setminus
S}\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}_{\mathcal{C}^{S},q}[S^{*}\cdot
q^{\prime}]\cdot\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}_{\mathcal{C},q^{\prime}}[W(\mathsf{col})]$
$\displaystyle=\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\prime}}_{\mathcal{C},q}[W(\mathsf{col})\cap
S^{\omega}]+\sum_{q^{\prime}\in Q\setminus
S}\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\prime}}_{\mathcal{C},q}[S^{*}\cdot
q^{\prime}]\cdot\chi_{\mathcal{G}}[q^{\prime}]$
$\displaystyle\geq\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\prime}}_{\mathcal{C},q}[W(\mathsf{col})\cap
S^{\omega}]+\sum_{q^{\prime}\in Q\setminus
S}\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\prime}}_{\mathcal{C},q}[S^{*}\cdot
q^{\prime}]\cdot(\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\prime}}_{\mathcal{C},q^{\prime}}[W(\mathsf{col})]-\varepsilon)$
$\displaystyle\geq\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\prime}}_{\mathcal{C},q}[W(\mathsf{col})]-\varepsilon\geq\chi_{\mathcal{G}}[q^{\prime}]-2\varepsilon$

As this holds for all Player-$\mathsf{B}$ strategies
$\mathsf{s}_{\mathsf{B}}$, it follows
that.$\chi_{\mathcal{G}^{S}}[\mathsf{s}_{\mathsf{A}}](q)\geq\chi_{\mathcal{G}}(q)-2\varepsilon$.
As this holds for all $\varepsilon>0$, we have
$\chi_{\mathcal{G}^{S}}(q)\geq\chi_{\mathcal{G}^{S}}[\mathsf{s}_{\mathsf{A}}](q)\geq\chi_{\mathcal{G}}(q)$.
By symmetry of the players, we have
$\chi_{\mathcal{G}^{S}}(q)=\chi_{\mathcal{G}}(q)$.

We can proceed to the proof of Lemma 48.

######  Proof.

Assume towards a contradiction that $\min C=e-1$. Let
$Q_{e-1}:=\mathsf{vcol}^{-1}[e-1]$. Consider a Player-$\mathsf{B}$ strategy
$\mathsf{s}_{\mathsf{B}}$ generated by the environment function $\mathsf{Ev}$.
Because the pair $(\mathsf{vcol},\mathsf{Ev})$ is completely faithful and
$e-1$ is odd, it follows that $\mathsf{s}_{\mathsf{B}}$ parity dominates the
valuation $v_{e-1,\mathsf{vcol}}^{u^{\prime}}$ in the game
$\mathcal{L}^{e-1}_{\mathsf{vcol}}$ for some $u^{\prime}\leq u$. Consider the
game $\mathcal{G}^{Q_{e-1}}$ from Definition 78 (we do not mention any player
since the game has a value). Lemma 79 gives that all states have the same
values in $\mathcal{G}$ and $\mathcal{G}^{Q_{e-1}}$. Let us show that there is
some $x\in[0,1]$ such that $x<u$ and such that the strategy
$\mathsf{s}_{\mathsf{B}}$ parity dominates the valuation $v_{Q_{e-1}}^{x}$ in
the game $\mathcal{G}^{Q_{e-1}}$. First, note that for all $y\in[0,1]$, if
$\mathsf{s}_{\mathsf{B}}$ dominates the valuation $v_{Q_{e-1}}^{y}$, then it
also parity dominates it (since $\mathsf{s}_{\mathsf{B}}$ parity dominates the
valuation $v_{e-1,\mathsf{vcol}}^{u^{\prime}}$ in the game
$\mathcal{L}^{e-1}_{\mathsf{vcol}}$).

Now, consider some state $q\in Q_{e-1}$. Let $\mathsf{vcol}_{q}$ be the
coloring function associated with the environment $\mathsf{Ev}(q)$. Denoting
$Y_{q}:=(\mathsf{F}(q),\mathsf{Ev}(q))$ and $p^{q}:=p_{q,\mathsf{vcol}_{q}}$,
we have that the Player-$\mathsf{B}$ $\mathsf{GF}$-strategy
$\mathsf{s}_{\mathsf{B}}(q)$ is optimal w.r.t. $Y_{q}$. Hence, by Lemma 21 for
Player $\mathsf{B}$, we have that for all Player-$\mathsf{A}$ actions
$a\in\mathsf{Act}_{\mathsf{A}}$, if
$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{(p^{q})^{-1}[p^{q}_{[0,1]}]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))=0$
then
$\mathsf{Color}(\mathsf{F}(q),p^{q},a,\mathsf{s}_{\mathsf{B}}(q))\cup\\{e-2\\}$
is odd with
$\mathsf{Color}(\mathsf{F}(q),p^{q},a,\mathsf{s}_{\mathsf{B}}(q)):=\\{i\in\llbracket
0,e\rrbracket\mid\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{(p^{q})^{-1}[k_{i}]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))>0\\}$.
Since $e$ is even, it must be that, for all states $q\in Q_{e-1}$ and
$a\in\mathsf{Act}_{\mathsf{A}}^{q}$:

$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{(p^{q})^{-1}[p^{q}_{[0,1]}]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))=0\Rightarrow\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{(p^{q})^{-1}[k_{e}]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))=0$
(11)

For $q\in Q_{e-1}$, let
$\mathsf{NZ}(q):=\\{a\in\mathsf{Act}_{\mathsf{A}}^{q}\mid\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{(p^{q})^{-1}[p^{q}_{[0,1]}]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))>0\\}$.
Then, we let:

$p_{m}:=\min_{q\in
Q_{e-1}}\min_{a\in\mathsf{NZ}(q)}\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{(p^{q})^{-1}[p^{q}_{[0,1]}]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))>0$
(12)

and

$x:=u+p_{m}\cdot(u^{\prime}-u)<u$ (13)

Let us show that the strategy $\mathsf{s}_{\mathsf{B}}$ dominates the
valuation $v_{Q_{e-1}}^{x}$ in the game $\mathcal{G}^{Q_{e-1}}$. Let $q\in
Q_{e-1}$. We have
$\mathsf{val}{\langle\mathsf{F}(q),v\rangle}(\mathsf{s}_{\mathsf{B}}(q))=\max_{a\in\mathsf{Act}_{\mathsf{A}}^{q}}\mathsf{out}_{\langle\mathsf{F}(q),v\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$.
Consider some $a\in\mathsf{Act}_{\mathsf{A}}^{q}$ and a Player-$\mathsf{A}$
strategy $\mathsf{s}_{\mathsf{A}}$ with $\mathsf{s}_{\mathsf{A}}(q):=a$.
Denoting
$P_{a}[T]:=\mathbb{P}_{\mathcal{C}_{\mathsf{vcol}}^{e-1},q}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[T]$
for any $T\subseteq Q_{e-1}\cup\\{k^{e-1}_{e}\\}\cup V_{Q\setminus Q_{u}}$, we
have:

$\displaystyle\mathsf{out}_{\langle\mathsf{F}(q),v_{Q_{e-1}}^{x}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=x\cdot\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{Q_{e-1}}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle+u\cdot\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{Q_{e}}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle+\sum_{y\in V_{Q\setminus
Q_{u}}}y\cdot\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{Q_{y}}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=x\cdot P_{a}[Q_{e-1}]+u\cdot
P_{a}[\\{k_{e}^{e-1}\\}]+\sum_{y\in V_{Q\setminus Q_{u}}}y\cdot P_{a}[y]$

In addition, since the strategy $\mathsf{s}_{\mathsf{B}}$ dominates the
valuation $v^{u^{\prime}}_{e-1,\mathsf{vcol}}$ in the game
$\mathcal{L}^{e-1}_{\mathsf{vcol}}$, we have:

$\displaystyle u^{\prime}$
$\displaystyle\geq\mathsf{out}_{\langle\mathsf{F}(q),v^{u^{\prime}}_{e-1,\mathsf{vcol}}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=u^{\prime}\cdot P_{a}[Q_{e-1}\cup\\{k_{e}^{e-1}\\}]+\sum_{y\in
V_{Q\setminus Q_{u}}}y\cdot P_{a}[y]$

That is:

$\sum_{y\in V_{Q\setminus Q_{u}}}y\cdot P_{a}[y]\leq u^{\prime}\cdot
P_{a}[V_{Q\setminus Q_{u}}]$

By Equation (1) in Lemma 72, for all $y\in V_{Q\setminus Q_{u}}$, we have:

$P_{a}[y]=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{(p^{q})^{-1}[y]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$

Furthermore, by Equation (3) in Lemma 72 which can be applied since
$(\mathsf{vcol},\mathsf{Ev})$ is faithful down to $e-1$, it also is coherent
at $e-1$, we have:

$P_{a}[\\{k^{e}_{e-1}\\}]=\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{(p^{q})^{-1}[k_{e}]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$

Now, assume that
$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{(p^{q})^{-1}[V_{Q\setminus
Q_{u}}]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))=0$. That is, for all $y\in
V_{Q\setminus Q_{u}}$, we have $P_{a}[y]=0$. By Equation (11) it follows that
$P_{a}[\\{k^{e}_{e-1}\\}]=0$. Hence:
$v_{Q_{e-1}}^{x}(q)=x=\mathsf{out}_{\langle\mathsf{F}(q),v_{Q_{e-1}}^{x}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$.

Assume now that
$\mathsf{out}_{\langle\mathsf{F}(q),\mathbbm{1}_{(p^{q})^{-1}[V_{Q\setminus
Q_{u}}]}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))>0$ (i.e. $a\in\mathsf{NZ}(q)$).
By Equation (12), it implies that $P_{a}[V_{Q\setminus Q_{u}}]\geq p_{m}$. It
follows that, by Equation (13):

$\displaystyle\mathsf{out}_{\langle\mathsf{F}(q),v_{Q_{e-1}}^{x}\rangle}(a,\mathsf{s}_{\mathsf{B}}(q))$
$\displaystyle=x\cdot P_{a}[Q_{e-1}]+u\cdot
P_{a}[\\{k_{e-1}^{e}\\}]+\sum_{y\in V_{Q\setminus Q_{u}}}y\cdot P_{a}[y]$
$\displaystyle\leq u\cdot P_{a}[Q_{e-1}]+u\cdot
P_{a}[\\{k_{e-1}^{e}\\}]+u^{\prime}\cdot P_{a}[V_{Q\setminus Q_{u}}]$
$\displaystyle=u\cdot(1-P_{a}[V_{Q\setminus Q_{u}}])+u^{\prime}\cdot
P_{a}[V_{Q\setminus Q_{u}}]$ $\displaystyle=u+P_{a}[V_{Q\setminus
Q_{u}}]\cdot(u^{\prime}-u)\leq u+p_{m}\cdot(u^{\prime}-u)$
$\displaystyle=x=v_{Q_{e-1}}^{x}(q)$

As this holds for all $x\in Q_{e-1}$, it follows that the Player-$\mathsf{B}$
strategy $\mathsf{s}_{\mathsf{B}}$ dominates the valuation $v^{x}_{Q_{e-1}}$,
and therefore parity dominates it. Hence, for all $q\in Q_{e-1}$, we have
$\chi_{\mathcal{G}^{Q_{e-1}}}[q]\leq x<u$. That is a contradiction with Lemma
79.

###  D.7 Proof of Lemma 49, Page 49

First, let us formally define a way to compare coloring functions.

######  Definition 80.

We define the (transitive) relation $\prec_{\llbracket 0,e\rrbracket}$ on
coloring functions which corresponds to the lexicographic order. Specifically,
for all virtual coloring functions
$\mathsf{vcol}_{1},\mathsf{vcol}_{2}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$, we have $\mathsf{vcol}_{1}\prec_{\llbracket
0,e\rrbracket}\mathsf{vcol}_{2}$ if and only if there is some $k\in\llbracket
0,e\rrbracket$ such that:

  * •

for all $i\in\llbracket k+1,e\rrbracket$, we have
$|\mathsf{vcol}_{1}^{-1}[i]|=|\mathsf{vcol}_{2}^{-1}[i]|$;

  * •

$|\mathsf{vcol}_{1}^{-1}[k]|<|\mathsf{vcol}_{1}^{-1}[k]|$.

We write $\mathsf{vcol}_{1}=_{\llbracket 0,e\rrbracket}\mathsf{vcol}_{2}$ when
we have neither $\mathsf{vcol}_{1}\prec_{\llbracket
0,e\rrbracket}\mathsf{vcol}_{2}$ or $\mathsf{vcol}_{1}\prec_{\llbracket
0,e\rrbracket}\mathsf{vcol}_{2}$. We also write
$\mathsf{vcol}_{1}\preceq_{\llbracket 0,e\rrbracket}\mathsf{vcol}_{2}$ for
$\mathsf{vcol}_{1}=_{\llbracket 0,e\rrbracket}\mathsf{vcol}_{2}$ or
$\mathsf{vcol}_{1}\prec_{\llbracket 0,e\rrbracket}\mathsf{vcol}_{2}$.

Straightforwardly, this relation ensures the following proposition.

######  Proposition 81.

Let $n\in\mathbb{N}$. There is no infinite sequence
$(c_{k})_{k\in\mathbb{N}}\in(\llbracket 0,e\rrbracket^{n})^{\mathbb{N}}$ such
that $c_{k}\prec_{\llbracket 0,e\rrbracket}c_{k+1}$ for all $k\in\mathbb{N}$.

######  Proof.

This is because the relation $\prec_{\llbracket 0,e\rrbracket}$ corresponds to
a lexicographic order on vectors taking their values in $\llbracket
0,e\rrbracket$.

We can then consider all steps of Algorithm 17 one by one.

######  Lemma 82.

Consider a virtual coloring function $\mathsf{vcol}:Q_{u}\rightarrow\llbracket
0,e\rrbracket$ and some $k\in\llbracket 0,e\rrbracket$. For all partial
environment functions $\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$ defined on
$\llbracket k+1,e\rrbracket$:

  * •

for
$(\mathsf{vcol}_{\mathsf{upd}},\mathsf{Ev}_{\mathsf{upd}})\leftarrow\mathsf{UpdateColEnv}(k,\mathsf{vcol},\mathsf{Ev})$,
we have $\mathsf{vcol}\preceq_{\llbracket
0,e\rrbracket}\mathsf{vcol}_{\mathsf{upd}}$;

For all environment functions $\mathsf{Ev}:Q_{u}\rightarrow\mathsf{Env}(Q)$:

  * •

for
$(\mathsf{vcol}_{\mathsf{Inc}},\mathsf{Ev}_{\mathsf{Inc}})\leftarrow\mathsf{IncLeast}(\mathsf{vcol},\mathsf{Ev})$,
we have $\mathsf{vcol}\prec_{\llbracket
0,e\rrbracket}\mathsf{vcol}_{\mathsf{Inc}}$;

######  Proof.

The procedure $\mathsf{UpdateColEnv}$ consists in two part. First, the call
Algorithm 13. This does not change the coloring function. Then, there is the
call to Algorithm 14. By Proposition 66, if
$\mathsf{NewCol}(q,\mathsf{vcol})=k$, then $\mathsf{vcol}(q)\leq k$. Hence,
the change of colors of the states does not decrease the colors of the states.
It follows that the resulting coloring function $\mathsf{vcol}_{\mathsf{upd}}$
is such that $\mathsf{vcol}\preceq_{\llbracket
0,e\rrbracket}\mathsf{vcol}_{\mathsf{upd}}$ .

Consider now the procedure $\mathsf{IncLeast}$. By definition, before the call
of this algorithm, some states are colored with $c_{\min}$. Hence, the
coloring function resulting of the call to Algorithm 16 has more states
colored with $c_{\min}+2$, whereas states colored with a color higher than
$c_{\min}+2$ are left unchanged. Hence: $\mathsf{vcol}\prec_{\llbracket
0,e\rrbracket}\mathsf{vcol}_{\mathsf{Inc}}$.

We can now proceed to the proof of Lemma 49.

######  Proof.

By Lemma 82, each call to the procedure $\mathsf{IncLeast}$ strictly increase
(w.r.t. $\prec_{\llbracket 0,e\rrbracket}$) the coloring function.
Furthermore, each call to the procedure $\mathsf{UpdateColEnv}$ does not
decrease (w.r.t. $\prec_{\llbracket 0,e\rrbracket}$) the coloring function.
Hence, by Proposition 81, the call to the procedure $\mathsf{IncLeast}$ is
done only finitely many times.

##  Appendix E Proofs from Section 7

###  E.1 Proof of Proposition 51, Page 51

First, let us formally recall the definition of deterministic and of
determined game forms.

######  Definition 83 (Deterministic and determined game forms).

Consider a set of outcomes $\mathsf{O}$. A game form
$\mathcal{F}=\langle\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}},\mathsf{O},\varrho\rangle\in\mathsf{Form}(\mathsf{O})$
is _deterministic_ if, for all
$\sigma_{\mathsf{A}}\in\mathcal{D}(\mathsf{Act}_{\mathsf{A}})$ and
$\sigma_{\mathsf{B}}\in\mathcal{D}(\mathsf{Act}_{\mathsf{B}})$, the
probability distribution $\varrho(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})$ is
deterministic.

Furthermore, the game form $\mathcal{F}\in\mathsf{Form}(\mathsf{O})$ is
_determined_ if it is deterministic and, for all
$v:\mathsf{O}\rightarrow\\{0,1\\}$, either there is some
$a\in\mathsf{Act}_{\mathsf{A}}$ such that
$\varrho(a,\mathsf{Act}_{\mathsf{B}})=\\{1\\}$ or there is some
$b\in\mathsf{Act}_{\mathsf{B}}$ such that
$\varrho(\mathsf{Act}_{\mathsf{A}},b)=\\{0\\}$.

###### Proof.

In [2], it was shown that in all locally determined concurrent games (i.e.
concurrent games where game forms are determined), both players have
positional optimal strategies. Hence, determined game forms are positionally
optimizable.

Consider now a game form
$\mathcal{F}=\langle\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}},\mathsf{D},\varrho\rangle$
such that $|\mathsf{O}|=2$. Let $\mathsf{O}:=\\{x,y\\}$. Consider an
environment $E=\langle c,e,p\rangle$ and the induced parity game
$\mathcal{G}_{Y}$ for $Y:=(\mathcal{F},E)$. If $p(x),p(y)\in[0,1]$, then the
game cannot loop and both players have optimal positional strategies. Assume
that $p(x)\in[0,1]$ and $p(y)\notin[0,1]$. If there is a row of $y$ and $y$ is
mapped w.r.t. $p$ to an even integer (if it is mapped to $q_{\mathsf{init}}$,
we consider the integer $c$), then Player $\mathsf{A}$ can surely win by
playing the corresponding row. Similarly, if there is a column of $y$ and $y$
is mapped w.r.t. $p$ to an odd integer, then Player $\mathsf{B}$ can surely
win by playing the corresponding column. Otherwise, both players can play a
uniform distribution over all actions that do not only lead to $y$, thus
ensuring that the value of both strategies (and of the game) is equal to
$p(x)$. The reasoning is identical if $p(x)\notin[0,1]$ and $p(y)\in[0,1]$.
Finally, assume that $p(x),p(y)\notin[0,1]$ and assume that $x$ is mapped
w.r.t. $p$ to the highest integer among the two. If there is a row of $y$ and
$y$ is mapped to an even integer, then Player $\mathsf{A}$ can surely win by
playing the corresponding row. Similarly, if there is a column of $y$ and $y$
is mapped to an odd integer, then Player $\mathsf{B}$ can surely win by
playing the corresponding column. Otherwise, one of the players wins almost
surely by playing a uniform probability distribution over all actions: if $x$
is mapped to an even integer, then Player $\mathsf{A}$ wins almost-surely,
otherwise, Player $\mathsf{B}$ wins almost-surely. ∎

###  E.2 Proof of Proposition 57, Page 57

We prove the result for Player $\mathsf{A}$, the arguments are similar for
Player $\mathsf{B}$. In the remainder of this section, we fix a set of
outcomes $\mathsf{O}$ and a game form
$\mathcal{F}=\langle\mathsf{Act}_{\mathsf{A}},\mathsf{Act}_{\mathsf{B}},\mathsf{O},\varrho\rangle$.

######  Definition 84.

Consider some $n\geq 1$ and an (arbitrary) environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O})$ with
$p:\mathsf{O}\rightarrow\\{q_{\mathsf{init}}\\}\cup[0,1]\cup K_{e}$ with
$\mathsf{Sz}_{\mathsf{A}}(E)=n$. Assume that no outcome $o\in\mathsf{O}$ is
such that $p(o)=q_{\mathsf{init}}$. Let $\tilde{e}:=\mathsf{Even}(e)\geq 2$.
By definition, we have $n=\tilde{e}-c$. Let us define a relevant environment
$E^{\prime}=\langle
c^{\prime},e^{\prime},p^{\prime}\rangle\in\mathsf{Env}(\mathsf{O})$ of size
$n-1$.

We let:

$c^{\prime}:=\begin{cases}0&\text{ if }c\text{ is even }\\\ 1&\text{ otherwise
}\end{cases}$

We also let $\mathsf{Im}_{p}:=\\{n\in\llbracket
c+1,\tilde{e}-1\rrbracket\mid\exists o\in\mathsf{O},\;p(o)=k_{i}\\}$ and
$c=a_{0}<a_{1}<a_{2}<\ldots<a_{k}$ be such that
$\mathsf{Im}_{p}=\\{a_{1},a_{2},\ldots,a_{k}\\}$. In particular, we have
$\tilde{e}-1\geq c+k$. Let us define the function
$f_{E}:\\{a_{0},\ldots,a_{k}\\}\rightarrow\mathbb{N}$ such that, letting
$f_{E}(a_{0}):=c^{\prime}$, for all $1\leq i\leq k$:

$f_{E}(a_{i}):=\begin{cases}f_{E}(a_{i-1})&\text{ if }a_{i-1}\equiv a_{i}\mod
2\\\ f_{E}(a_{i-1})+1&\text{ otherwise }\end{cases}$

Since for all $1\leq i\leq k$, we have $f_{E}(a_{i})\leq f_{E}(a_{i-1})+1$, we
have $f_{E}(a_{k})\leq c^{\prime}+k$. We set $e^{\prime}:=f_{E}(a_{k})$. Note
also that, for all $1\leq i\leq k$, we have $f(a_{k})\geq c^{\prime}$. With
this choice, we have $\mathsf{Sz}(E^{\prime})=e^{\prime}-c^{\prime}\leq
k\leq\tilde{e}-1-c=\mathsf{Sz}_{\mathsf{A}}(E)-1=n-1$.

We can now define the function $p^{\prime}$. We let
$u:=\chi_{\mathcal{G}_{Y}}(q_{\mathsf{init}})$ for $Y:=(\mathcal{F},E)$. Then,
for all $o\in\mathsf{O}$, we let:

$p^{\prime}(o):=\begin{cases}p(o)\in[0,1]&\text{ if }p(o)\in[0,1]\\\
u\in[0,1]&\text{ if }p(o)=\tilde{e}\\\ k_{f_{E}(\max(c,n))}\in
K_{e^{\prime}}&\text{ if }p(o)=k_{n}\in K_{\tilde{e}-1}\end{cases}$

Let us now show a useful property about the function $f_{E}$ from Definition
84.

######  Lemma 85.

Consider an (arbitrary) environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O})$ and the function
$f_{E}:\\{a_{0},\ldots,a_{k}\\}\rightarrow\mathbb{N}$ from Definition 84. It
ensures the following: for all $0\leq i\leq k$, $a_{i}$ and $f_{E}(a_{i})$
have the same parity. In addition, for all
$X\subseteq\\{a_{0},\ldots,a_{k}\\}$, $\max X$ has the same parity as $\max
f_{E}(X)$.

###### Proof.

Let us show by induction on $i\in\llbracket 0,k\rrbracket$ the following
property $\mathcal{P}(i)$: $a_{i}$ and $f(a_{i})$ have the same parity. The
property $\mathcal{P}(0)$ straightforwardly holds since $a_{0}=c$ and
$f_{E}(a_{0})=c^{\prime}$ have the same parity. Assume now that
$\mathcal{P}(i-1)$ holds for some $1\leq i\leq k$. If $a_{i}$ has the same
parity as $a_{i-1}$, then $f_{E}(a_{i})=f_{E}(a_{i-1})$ which has the same
parity as $a_{i-1}$. Similarly, if $a_{i}$ does not have the same parity as
$a_{i-1}$, then $f_{E}(a_{i})=f_{E}(a_{i-1})+1$. Hence, $a_{i}$ and $f(a_{i})$
have the same parity. Overall, the property $\mathcal{P}(i)$ holds for all
$i\in\llbracket 0,k\rrbracket$. The second part of the lemma comes from the
fact that $f_{E}$ is non-decreasing. ∎

Let us now show that the value of local parity games with an arbitrary
environment $E$ is equal to the value of the parity game with the
corresponding relevant environment.

######  Lemma 86.

Consider an (arbitrary) environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O})$ and the relevant environment
$E^{\prime}=\langle c^{\prime},e^{\prime},p^{\prime}\rangle$ from Definition
84. Let $Y:=(\mathcal{F},E)$ and $Y^{\prime}:=(\mathcal{F},E^{\prime})$. Then,
$\chi_{\mathcal{G}_{Y}}(q_{\mathsf{init}})\leq\chi_{\mathcal{G}_{Y^{\prime}}}(q_{\mathsf{init}})$.

To prove this result we will use a result whose proof is not yet published.
Specifically, consider a game $\mathcal{G}=\langle\mathcal{C},W\rangle$ (with
$W\subseteq Q^{\omega}$ an arbitrary Borel winning objective), a finite set of
labels $\mathsf{Label}$ and a labeling function
$\mathsf{lb}:Q\rightarrow\mathsf{Label}$. Assume that $W$ is
$\mathsf{lb}$-uniform, that is, for all $\rho,\rho^{\prime}\in Q^{\omega}$, if
for all $i\in\mathbb{N}$, we have
$\mathsf{lb}(\rho_{i})=\mathsf{lb}(\rho^{\prime}_{i})$, then $\rho\in
W\Leftrightarrow\rho^{\prime}\in W$. In that case, the value of the game
$\mathcal{G}$ can be approximated (i.e. the value can approached arbitrarily
closely) by label-strategies (for both players), that is strategies that only
depend on the labels of the states visited (and the current state). For Player
$\mathsf{A}$, such a strategy $\mathsf{s}_{\mathsf{A}}$ would satisfy that,
for all $q\in Q$, for all $n\in\mathbb{N}$ and $\rho,\rho^{\prime}\in Q^{n}$
such that for all $0\leq i\leq n$, we have
$\mathsf{lb}(\rho_{i})=\mathsf{lb}(\rho^{\prime}_{i})$, then
$\mathsf{s}_{\mathsf{A}}(\rho\cdot
q)=\mathsf{s}_{\mathsf{A}}(\rho^{\prime}\cdot q)$. This result follows from an
adaptation of Martin’s proof of the determinacy of Blackwell games and should
be submitted in the next few months. We will explicitly mention in the next
proof when we use this result.

###### Proof.

We let $Q_{y}$ and $q_{Y}\in Q_{Y}$ (resp. $Q_{Y^{\prime}}$ and
$q_{Y^{\prime}}$) denote the set of non-stopping states in $\mathcal{C}_{Y}$
and the state $q_{\mathsf{init}}\in Q_{Y}$ (resp. $\mathcal{C}_{Y^{\prime}}$
and the state $q_{\mathsf{init}}\in Q_{Y^{\prime}}$).

Recall the function $f_{E}$ from Definition 84. We let $f:=f_{E}$ and we
extend it such that $f(\tilde{e}):=d$ with $d$ the smallest integer of the
same parity than $e$ such that $d\geq e^{\prime}+1$. Then, we define an
alternate game
$\mathcal{G}_{Y}^{f}=\langle\mathcal{C}_{Y}^{f},\mathsf{col}^{f}\rangle$ which
differs from the game $\mathcal{G}_{Y}$ only in the coloring function and in
the objective. The coloring function $\mathsf{col}^{f}$ in the arena
$\mathcal{C}_{Y}^{f}$ is such that, for all states $q\in Q_{Y}$, we have:

$\mathsf{col}^{f}(q):=f(\max(c,\mathsf{col}(q)))$

where $\mathsf{col}$ refers to the coloring function in the game
$\mathcal{G}_{Y}$. Let us show that the value of both games
$\mathcal{G}_{Y}^{f}$ and $\mathcal{G}_{Y}$ is the same. Consider a pair of
strategies
$(\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}})\in\mathsf{S}_{\mathsf{A}}^{\mathcal{C}_{Y}}\times\mathsf{S}_{\mathsf{B}}^{\mathcal{C}_{Y}}=\mathsf{S}_{\mathsf{A}}^{\mathcal{C}_{Y}^{f}}\times\mathsf{S}_{\mathsf{B}}^{\mathcal{C}_{Y}^{f}}$.
First, we have:

$\sum_{x\in[0,1]}\mathbb{P}_{\mathcal{C}_{Y},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{Y}^{*}\cdot
x]\cdot
x=\sum_{x\in[0,1]}\mathbb{P}_{\mathcal{C}_{Y}^{f},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{Y}^{*}\cdot
x]\cdot x$

In addition, since all states $k_{i}$ loop back to $q_{Y}$ in
$\mathcal{C}_{Y}$ and $\mathcal{C}_{Y}^{f}$, we have:

$\mathbb{P}_{\mathcal{C}_{Y},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{Y}^{\omega}\setminus(Q_{Y}^{*}\cdot
q_{Y})^{\omega}]=0=\mathbb{P}_{\mathcal{C}_{Y}^{f},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{Y}^{\omega}\setminus(Q_{Y}^{*}\cdot
q_{Y})^{\omega}]$

Furthermore, consider some infinite path $\rho\in(Q_{Y}^{*}\cdot
q_{Y})^{\omega}$ visiting infinitely often the central state $q_{Y}$. Let
$X_{\rho}:=\\{\mathsf{col}[\mathsf{InfOft}(\rho)]\cap\llbracket
c,e\rrbracket\\}$ denote the set of colors, at least $c$, seen infinitely
often in $\rho$ in $\mathcal{G}_{Y}$. Note that $X_{\rho}\neq\emptyset$ since
$\mathsf{col}(q_{Y})=c$. We also let
$X_{\rho}^{f}:=\\{\mathsf{col}^{f}[\mathsf{InfOft}(\rho)]\cap\llbracket
c^{\prime},d\rrbracket\\}$ denote the set of colors, at least $c^{\prime}$,
seen infinitely often in $\rho$ in $\mathcal{G}_{Y}^{f}$. By definition of
$\mathsf{col}^{f}$, we have $X_{\rho}^{f}=f[X_{\rho}]$. Therefore, we have, by
Lemma 85 and by definition of $d$:

$\displaystyle\max X_{\rho}\text{ is even }\Leftrightarrow\max
f(X_{\rho})\text{ is even }\Leftrightarrow\max X_{\rho}^{f}\text{ is even }$

It follows that:

$\mathbb{P}_{\mathcal{C}_{Y},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[Q_{Y}^{\omega}\cap
W_{Y}]=\mathbb{P}_{\mathcal{C}_{Y}^{f},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[(Q_{Y}^{f})^{\omega}\cap
W_{Y}^{f}]$

As this holds for all pair of strategies
$(\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}})\in\mathsf{S}_{\mathsf{A}}^{\mathcal{C}_{Y}}\times\mathsf{S}_{\mathsf{B}}^{\mathcal{C}_{Y}}=\mathsf{S}_{\mathsf{A}}^{\mathcal{C}_{Y}^{f}}\times\mathsf{S}_{\mathsf{B}}^{\mathcal{C}_{Y}^{f}}$,
it follows that
$\chi_{\mathcal{G}_{Y}}(q_{Y})=\chi_{\mathcal{G}_{Y}^{f}}(q_{Y})$.

Let us now relate the games $\mathcal{G}_{Y}^{f}$ and
$\mathcal{G}_{Y^{\prime}}$. By using the unpublished result mentioned prior to
this proof, one can show that almost-optimal Player-$\mathsf{A}$ strategies
$\mathsf{s}_{\mathsf{A}}$ in $\mathcal{G}_{Y}^{f}$ can be chosen such that,
for all $\rho,\rho^{\prime}\in Q_{Y}^{*}$, if for all $i\in\mathbb{N}$, we
have $\mathsf{col}^{f}(\rho_{i})=\mathsf{col}^{f}(\rho^{\prime}_{i})$, then
for all $q\in Q_{Y}$, we have $\mathsf{s}_{\mathsf{A}}(\rho\cdot
q)=\mathsf{s}_{\mathsf{A}}(\rho^{\prime}\cdot q)$. Such strategies are called
$(\llbracket c^{\prime},d\rrbracket,\mathsf{col}^{f})$-uniform strategies.
Similarly, in $\mathcal{G}_{Y}$, almost-optimal strategies (for both players)
can be found among $(\llbracket
c^{\prime},e^{\prime}\rrbracket,\mathsf{col}^{\prime})$-uniform strategies in
$\mathcal{G}_{Y^{\prime}}$. Furthermore, any strategy $(\llbracket
c^{\prime},d\rrbracket,\mathsf{col}^{f})$-uniform strategy in
$\mathcal{C}_{Y}^{f}$ can be seen as a ($(\llbracket
c^{\prime},e^{\prime}\rrbracket,\mathsf{col}^{\prime})-$)strategy in
$\mathcal{C}_{Y^{\prime}}$. On the other hand, a $(\llbracket
c^{\prime},e^{\prime}\rrbracket,\mathsf{col}^{\prime})$-uniform strategy in
$\mathcal{C}_{Y^{\prime}}$ can be seen as a ($(\llbracket
c^{\prime},d\rrbracket,\mathsf{col}^{f})-$)strategy in $\mathcal{C}_{Y}^{f}$
up to defining what it does once the state $k_{\tilde{e}}$ — colored by $d$ —
occurs.

Consider any Player-$\mathsf{A}$ strategy
$\mathsf{s}_{\mathsf{A}}\in\mathsf{S}_{\mathsf{A}}^{\mathcal{C}_{Y}^{f}}$ that
is $(\llbracket c^{\prime},d\rrbracket,\mathsf{col}^{f})$-uniform in
$\mathcal{C}_{Y}^{f}$. As mentioned above, it can be seen as a
Player-$\mathsf{A}$ strategy in $\mathcal{C}_{Y^{\prime}}$. Let $\delta>0$ and
consider a $(\llbracket
c^{\prime},e^{\prime}\rrbracket,\mathsf{col}^{\prime})$-uniform
Player-$\mathsf{B}$ strategy in $\mathcal{C}_{Y^{\prime}}$. Consider the
Player-$\mathsf{B}$ strategy
$\mathsf{s}_{\mathsf{B}}^{\delta}\in\mathsf{S}_{\mathsf{B}}^{\mathcal{C}_{Y}^{f}}$
that mimics the strategy $\mathsf{s}_{\mathsf{B}}$ as long as $k_{\tilde{e}}$
is not seen. Once it is seen, the Player-$\mathsf{B}$ strategy
$\mathsf{s}_{\mathsf{B}}^{\delta}$ switches to a $\delta$-optimal strategy in
the game $\mathcal{G}_{Y}^{f}$. By definition of
$\mathsf{s}_{\mathsf{B}}^{\delta}$, and since
$u=\chi_{\mathcal{G}_{Y}}(q_{Y})=\chi_{\mathcal{G}_{Y}^{f}}(q_{Y})$, we have:

$\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\delta}}_{\mathcal{C}_{Y}^{f},q_{Y}}[W(\mathsf{col}^{f})\cap(Q_{Y}^{f})^{*}\cdot
k_{\tilde{e}}]\leq\mathbb{P}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\delta}}_{\mathcal{C}_{Y}^{f},q_{Y}}[(Q_{Y}^{f})^{*}\cdot
k_{\tilde{e}}]\cdot(u+\delta)$

Since the outcomes leading to $k_{\tilde{e}}$ in $\mathcal{C}_{y}^{f}$ lead to
the stopping state $u\in[0,1]$ in $\mathcal{C}_{Y^{\prime}}$, and all outcomes
leading to a stopping state in $\mathcal{C}_{y}^{f}$ lead to the same stopping
state in $\mathcal{C}_{Y^{\prime}}$, it follows that:

$\mathbb{P}_{\mathcal{C}_{Y}^{f},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\delta}}[W(\mathsf{col}^{f})\cap
Q_{Y}^{*}\cdot(k_{\tilde{e}}\cup[0,1])]\leq\mathbb{P}_{\mathcal{C}_{Y^{\prime}},q_{Y^{\prime}}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[W(\mathsf{col}^{\prime})\cap
Q_{Y^{\prime}}^{*}\cdot[0,1]]+\delta$

In addition, we have:

$\mathbb{P}_{\mathcal{C}_{Y}^{f},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\delta}}[(Q_{Y}\setminus\\{k_{\tilde{e}}\\})^{\omega}]=\mathbb{P}_{\mathcal{C}_{Y^{\prime}},q_{Y^{\prime}}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[(Q_{Y^{\prime}})^{\omega}]$

In addition, consider any outcome $o\in\mathsf{O}$ such that
$p^{\prime}(o)\notin[0,1]$ or equivalently such that
$p(o)\notin[0,1]\cup\\{k_{\tilde{e}}\\}$. Then, we have
$p^{\prime}(o)=k_{f(\max(c,n))}$ where $n\in\llbracket
0,\tilde{e}-1\rrbracket$ is such that $p(o)=k_{n}$. Then, we have
$\mathsf{col}^{\prime}\circ p^{\prime}(o)=f(\max(c,n))=\mathsf{col}^{f}\circ
p(o)$. Furthermore, we have
$\mathsf{col}^{\prime}(q_{Y^{\prime}})=c^{\prime}=\mathsf{col}^{f}(q_{Y})$. It
follows that, assuming that $[0,1]\cup\\{k_{\tilde{e}}\\}$ is not reached in
$\mathcal{C}_{Y}^{f}$ and that $[0,1]$ is not reached in
$\mathcal{C}_{Y^{\prime}}$, the colors seen with $\mathsf{s}_{\mathsf{A}}$ and
$\mathsf{s}_{\mathsf{B}}^{\delta}$ are the same as the colors seen with
$\mathsf{s}_{\mathsf{A}}$ and $\mathsf{s}_{\mathsf{B}}$ in
$\mathcal{C}_{Y}^{f}$ (because the strategies
$\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}},\mathsf{s}_{\mathsf{B}}^{\delta}$
only depend on the colors seen). Therefore:

$\mathbb{P}_{\mathcal{C}_{Y}^{f},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\delta}}[W(\mathsf{col}^{f})\cap(Q_{Y}\setminus\\{k_{\tilde{e}}\\})^{\omega}]=\mathbb{P}_{\mathcal{C}_{Y^{\prime}},q_{Y^{\prime}}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[W(\mathsf{col}^{\prime})\cap(Q_{Y^{\prime}})^{\omega}]$

Overall, we obtain that:

$\displaystyle\chi_{\mathcal{G}_{Y}}[\mathsf{s}_{\mathsf{A}}](q_{Y})\leq\mathbb{P}_{\mathcal{C}_{Y}^{f},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\delta}}[W(\mathsf{col}^{f})]$
$\displaystyle=\mathbb{P}_{\mathcal{C}_{Y}^{f},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\delta}}[W(\mathsf{col}^{f})\cap(Q_{Y})^{*}\cdot(k_{\tilde{e}}\cup[0,1])]$
$\displaystyle+\mathbb{P}_{\mathcal{C}_{Y}^{f},q_{Y}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\delta}}[W(\mathsf{col}^{f})\cap(Q_{Y}\setminus([0,1]\cup\\{k_{\tilde{e}}\\}))^{\omega}]$
$\displaystyle\leq\mathbb{P}_{\mathcal{C}_{Y^{\prime}},q_{Y^{\prime}}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[W(\mathsf{col}^{\prime})\cap(Q_{Y^{\prime}})^{*}\cdot[0,1]]+\delta$
$\displaystyle+\mathbb{P}_{\mathcal{C}_{Y^{\prime}},q_{Y^{\prime}}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}}[W(\mathsf{col}^{\prime})\cap(Q_{Y^{\prime}})^{\omega}]$
$\displaystyle=\mathbb{P}_{\mathcal{C}_{Y^{\prime}},q_{Y^{\prime}}}^{\mathsf{s}_{\mathsf{A}},\mathsf{s}_{\mathsf{B}}^{\delta}}[W(\mathsf{col}^{\prime})]+\delta$

Since this holds for all Player-$\mathsf{B}$ $(\llbracket
c^{\prime},e^{\prime}\rrbracket,\mathsf{col}^{\prime})$-uniform strategies,
and for all $\delta>0$, it follows that
$\chi_{\mathcal{G}_{Y}^{f}}[\mathsf{s}_{\mathsf{A}}](q_{Y})\leq\chi_{\mathcal{G}_{Y^{\prime}}}[\mathsf{s}_{\mathsf{A}}](q_{Y^{\prime}})+\delta\leq\chi_{\mathcal{G}_{Y^{\prime}}}(q_{Y^{\prime}})+\delta$.
Since this holds for all Player-$\mathsf{A}$ $(\llbracket
c,d\rrbracket,\mathsf{col})$-uniform strategies
$\mathsf{s}_{\mathsf{A}}\in\mathsf{S}_{\mathsf{A}}^{\mathcal{C}_{Y}}$, it
follows that
$\chi_{\mathcal{G}_{Y}}(q_{Y})=\chi_{\mathcal{G}_{Y}^{f}}(q_{Y})\leq\chi_{\mathcal{G}_{Y^{\prime}}}(q_{Y^{\prime}})$.
∎

We can now proceed to the proof of Proposition 57.

###### Proof.

Consider some $n\in\mathbb{N}$. First, consider the case where $n=0$. Then, an
environment $E=\langle c,e,p\rangle$ with $\mathsf{Sz}_{\mathsf{A}}(E)=0$ is
such that $c=e$ is even. That is, the corresponding parity game
$\mathcal{G}_{(\mathcal{F},E)}$ is, from Player $\mathsf{A}$’s point-of-view,
a safety game. Hence, positional optimal strategies exists for Player
$\mathsf{A}$ in $\mathcal{G}_{(\mathcal{F},E)}$ [9]. This is similar for
Player $\mathsf{B}$. Furthermore, there is no relevant environment of size at
most -1. Hence, the equivalence holds for $n=0$.

Assume now that $n\geq 1$. Consider any relevant environment $E$ with
$\mathsf{Sz}(E)\leq n-1$. Then, we have $\mathsf{Sz}_{\mathsf{A}}(E)\leq n$.
Therefore, if $\mathcal{F}$ is positionally maximizable w.r.t. Player
$\mathsf{A}$ up to $n$, then there is an optimal $\mathsf{GF}$-strategy in
$\mathcal{F}$ for Player $\mathsf{A}$ w.r.t. $(\mathcal{F},E)$.

Consider now an (arbitrary) environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O})$ with
$\mathsf{Sz}_{\mathsf{A}}(E)=n\geq 1$. Let $\tilde{e}:=\mathsf{Even}(e)$.
Clearly, the outcomes in $\mathsf{O}$ leading, w.r.t. $p$, to
$q_{\mathsf{init}}$ of color $c$, can be redirected to $k_{c}$ of color $c$
(which then loops back to $q_{\mathsf{init}}$) without changing the outcome of
the parity game induced by $E$. Hence, without loss of generality, we assume
that no outcome $o\in\mathsf{O}$ is such that $p(o)=q_{\mathsf{init}}$. We can
therefore consider the relevant environment
$E^{\prime}\in\mathsf{Env}(\mathsf{O})$ from Definition 84 of size
$\mathsf{Sz}(E^{\prime})=n-1$. Let $Y:=(\mathcal{F},E)$ and
$Y^{\prime}:=(\mathcal{F},E^{\prime})$ and assume that there is a
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathcal{F})$ that is optimal
w.r.t. $Y^{\prime}$. Let us show that $\sigma_{\mathsf{A}}$ is also optimal
w.r.t. to $Y$. We let $q_{Y}$ denote the state $q_{\mathsf{init}}$ in the game
$\mathcal{G}_{Y}$ and $q_{Y^{\prime}}$ denote the state $q_{\mathsf{init}}$ in
the game $\mathcal{G}_{Y^{\prime}}$. Let $u:=\chi_{\mathcal{G}_{Y}}(q_{Y})$
and $u^{\prime}:=\chi_{\mathcal{G}_{Y^{\prime}}}(q_{Y^{\prime}})$. By Lemma
86, we have $u\leq u^{\prime}$. We want to apply Lemma 21.

Let us show that the Player-$\mathsf{A}$ positional strategy
$\mathsf{s}^{Y}_{\mathsf{A}}(\sigma_{\mathsf{A}})$ ensures item $(i)$ of this
lemma, i.e. that it dominates the valuation $v_{Y}^{u}$ in the game
$\mathcal{G}_{Y}$. This amount to show that
$\mathsf{val}_{\langle\mathcal{F},v_{Y}^{u}\circ
p\rangle}(\sigma_{\mathsf{A}})\geq u$. Note that, again by Lemma 21, we have
that $\mathsf{val}_{\langle\mathcal{F},v_{Y^{\prime}}^{u^{\prime}}\circ
p^{\prime}\rangle}(\sigma_{\mathsf{A}})\geq u^{\prime}$. Furthermore, we have:

$v_{Y}^{u}\circ p+(u^{\prime}-u)\geq v_{Y^{\prime}}^{u^{\prime}}\circ
p^{\prime}$

Therefore, for any Player-$\mathsf{B}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{B}}\in\mathcal{D}(\mathsf{Act}_{\mathsf{B}})$, we have:

$\displaystyle\mathsf{out}_{\langle\mathcal{F},v_{Y}^{u}\circ
p\rangle}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})+u^{\prime}-u$
$\displaystyle\geq\mathsf{out}_{\langle\mathcal{F},v_{Y}^{u^{\prime}}\circ
p^{\prime}\rangle}(\sigma_{\mathsf{A}},\sigma_{\mathsf{B}})\geq\mathsf{val}_{\langle\mathcal{F},v_{Y}^{u^{\prime}}\circ
p^{\prime}\rangle}(\sigma_{\mathsf{A}})\geq u^{\prime}$

Since this holds for all Player-$\mathsf{B}$ $\mathsf{GF}$-strategies
$\sigma_{\mathsf{B}}\in\Sigma_{\mathsf{B}}(\mathcal{F})$, it follows that

$\mathsf{val}_{\langle\mathcal{F},v_{Y}^{u}\rangle}(\sigma_{\mathsf{A}})\geq
u$

Consider now item $(ii)$ from Lemma 21. Consider some Player-$\mathsf{B}$
action $b\in\mathsf{Act}_{\mathsf{B}}$ and assume that
$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[0,1]}\rangle}(\sigma_{\mathsf{A}},b)=0$.
If we have
$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[k_{\tilde{e}}]}\rangle}(\sigma_{\mathsf{A}},b)>0$,
then it follows that
$\max(\mathsf{Color}(\mathcal{F},p,\sigma_{\mathsf{A}},b)\cup\\{c\\})$ is even
since $\tilde{e}$ is even and is the highest integer appearing the game
$\mathcal{G}_{Y}$. Assume now that
$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[k_{\tilde{e}}]}\rangle}(\sigma_{\mathsf{A}},b)=0$.
Then, it follows that, by definition of $p^{\prime}$, we have
$\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{(p^{\prime})^{-1}[0,1]}\rangle}(\sigma_{\mathsf{A}},b)=0$.
Therefore, by Lemma 21, it follows that
$\max(\mathsf{Color}(\mathcal{F},p^{\prime},\sigma_{\mathsf{A}},b)\cup\\{c^{\prime}\\})$
is even. Furthermore, by definition of $p^{\prime}$:

$\displaystyle f_{E}[$ $\displaystyle\\{i\in\llbracket
c,\tilde{e}-1\rrbracket\mid\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[k_{i}]}\rangle}(\sigma_{\mathsf{A}},b)>0\\}\cup\\{c\\}]$
$\displaystyle=$ $\displaystyle\\{i\in\llbracket
c^{\prime},e^{\prime}\rrbracket\mid\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{(p^{\prime})^{-1}[k_{i}]}\rangle}(\sigma_{\mathsf{A}},b)>0\\}\cup\\{c^{\prime}\\}$

We have $\max\\{i\in\llbracket
c^{\prime},e^{\prime}\rrbracket\mid\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{(p^{\prime})^{-1}[k_{i}]}\rangle}(\sigma_{\mathsf{A}},b)>0\\}\cup\\{c^{\prime}\\}=\max(\mathsf{Color}(\mathcal{F},p^{\prime},\sigma_{\mathsf{A}},b)\cup\\{c^{\prime}\\})$
is even. Therefore, by Lemma 85, we have $\max\\{i\in\llbracket
c,\tilde{e}-1\rrbracket\mid\mathsf{out}_{\langle\mathcal{F},\mathbbm{1}_{p^{-1}[k_{i}]}\rangle}(\sigma_{\mathsf{A}},b)>0\\}\cup\\{c\\}=\max(\mathsf{Color}(\mathcal{F},p,\sigma_{\mathsf{A}},b)\cup\\{c\\})$
is also even.

In fact, the Player-$\mathsf{A}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}\in\Sigma_{\mathsf{A}}(\mathcal{F})$ satisfies item $(ii)$
of Lemma 21. Therefore, it is optimal w.r.t. $Y$. ∎

###  E.3 Proof of Lemma 61, Page 61

###### Proof.

Consider a relevant environment $E=\langle
c,e,p\rangle\in\mathsf{Env}(\mathsf{O}_{n})$ and $Y_{n}:=(\mathcal{F}_{n},E)$.
We let $u:=\chi_{\mathcal{G}_{Y_{n}}}(q_{\mathsf{init}})$. Note that since $E$
is relevant, we have $c\in\\{0,1\\}$ and $p:\mathsf{O}_{n}\rightarrow[0,1]\cup
K_{n}$. For all $o\in\mathsf{O}$, if $p(o)\notin[0,1]$, we let
$n_{o}\in\llbracket 0,e\rrbracket$ denote the integer that $t$ is mapped to
w.r.t. $p$, i.e. the integer ensuring $p(o)=k_{n_{o}}$. Note that, since $E$
is relevant, for all $o\in\mathsf{O}_{n}$, we have $n_{o}\geq c$.

Let us introduce some notations. We let $X_{[0,1]}:=\\{o\in\mathsf{O}_{n}\mid
p(o)\in[0,1]\\}$, $X_{\mathsf{even}}:=\\{o\in\mathsf{O}_{n}\mid n_{o}\text{ is
even}\\}$ and $X_{\mathsf{odd}}:=p^{-1}[K_{n}]\setminus X_{\mathsf{even}}$. We
let $X_{\mathsf{Lp}}:=p^{-1}[K_{n}]=X_{\mathsf{even}}\uplus X_{\mathsf{odd}}$.
Note that we have $\mathsf{O}_{n}=X_{[0,1]}\uplus X_{\mathsf{Lp}}$. We define
the valuation $v:\mathsf{O}_{n}\rightarrow[0,1]$ mapping each outcome to its
value in the game $\mathcal{G}_{Y_{n}}$ such that, for all
$o\in\mathsf{O}_{n}$:

$v(o):=\begin{cases}p(o)&\text{ if }o\in X_{[0,1]}\\\ u&\text{ otherwise
}\end{cases}$

That is, $v=v_{y_{n}}^{u}\circ p$. For all $x\in\mathsf{O}_{n}$, we let:

$w(x):=\begin{cases}1&\text{ if }x\in X_{\mathsf{even}}\\\ 0&\text{ if }x\in
X_{\mathsf{odd}}\\\ p(x)&\text{ if }x\in X_{[0,1]}\end{cases}$

For all $x\in\mathsf{O}_{n}$, the value $w(x)\in[0,1]$ corresponds to the
value of the game $\mathcal{G}_{Y_{n}}$ if $x$ is seen (indefinitely, if it is
in $X_{\mathsf{Lp}}$). This can be generalized to a pair of outcomes: for all
$x,x^{\prime}\in\mathsf{O}_{n}$, we let:

$w(x,x^{\prime}):=\begin{cases}w(x)&\text{ if }x,x^{\prime}\in
X_{\mathsf{Lp}}\text{ and }n_{x}\leq n_{x^{\prime}}\\\ w(x^{\prime})&\text{ if
}x,x^{\prime}\in X_{\mathsf{Lp}}\text{ and }n_{x^{\prime}}\leq n_{x}\\\
p(x)&\text{ if }x\in X_{\mathsf{[0,1]}},x^{\prime}\in X_{\mathsf{Lp}}\\\
p(x^{\prime})&\text{ if }x^{\prime}\in X_{\mathsf{[0,1]}},x\in
X_{\mathsf{Lp}}\\\ \frac{1}{2}\cdot(p(x)+p(x^{\prime}))&\text{ if
}x,x^{\prime}\in X_{\mathsf{[0,1]}}\end{cases}$

Figure 18: The game form $\mathcal{T}_{n}$.

Finally, we let $\mathcal{T}_{n}$ denote the $2\times 2$ game form at the top
left of the game form $\mathcal{F}_{n}$ from Figure 9. It is depicted in
Figure 18. We let
$u^{\prime}:=\mathsf{val}_{\langle\mathcal{T}_{n},v\rangle}$. Now, there are
several cases:

  * •

Assume that $y,z\in X_{\mathsf{Lp}}$. Then, $u\in\\{0,1\\}$, and playing
$a_{\mathsf{Ex}}\in\mathsf{Act}_{\mathsf{A}}^{n}$ (resp.
$b_{\mathsf{Ex}}\in\mathsf{Act}_{\mathsf{B}}^{n}$) is optimal for Player
$\mathsf{A}$ (resp. $\mathsf{B}$) w.r.t. $Y_{n}$.

  * •

Assume now that $y\in X_{\mathsf{Lp}}$ and $z\in X_{[0,1]}$. Then, $u=p(z)$,
as argued in the proof sketch, and playing
$a_{\mathsf{Ex}}\in\mathsf{Act}_{\mathsf{A}}^{n}$ (resp.
$b_{\mathsf{Ex}}\in\mathsf{Act}_{\mathsf{B}}^{n}$) is optimal for Player
$\mathsf{A}$ (resp. $\mathsf{B}$) w.r.t. $Y_{n}$. This is similar if $y\in
X_{[0,1]}$ and $z\in X_{\mathsf{Lp}}$.

  * •

Assume that $p(y),p(z)\in[0,1]$ and $p(y)\leq p(z)$. In that case, we have
$u=\frac{3p(y)+p(z)}{4}$ and playing action $a_{\mathsf{Ex}}$ (resp.
$b_{\mathsf{Ex}}$) is optimal for Player $\mathsf{A}$ (resp. $\mathsf{B}$)
w.r.t. $Y_{n}$.

  * •

Let us now assume that $y,z\in X_{[0,1]}$ and $p(z)<p(y)$. In that case, we
have:

$\frac{3p(z)+p(y)}{4}\leq u\leq\frac{p(z)+3p(y)}{4}$

We argue that Player $\mathsf{B}$ always has an optimal $\mathsf{GF}$-strategy
w.r.t. $Y_{n}$.

    * –

If $u=\frac{p(z)+3p(y)}{4}$, then positionally playing action
$b_{\mathsf{Ex}}$ is optimal for Player $\mathsf{B}$. We now assume that
$u<\frac{p(z)+3p(y)}{4}$.

    * –

If, for some even $i\in\llbracket 0,n-1\rrbracket$, we have $w(x_{i})\leq u$,
then playing action $b_{i}$ is optimal. We now assume that for all even
$i\in\llbracket 0,n-1\rrbracket$, we have $w(x_{i})>u$ (i.e. $x_{i}$ is mapped
to either a real greater then $u$ or even integer). Furthermore, if for any
even $i\in\llbracket 2,n-1\rrbracket$, we have $w(x_{i},x_{i-1})\leq u$, then
playing action $b_{i,i-1}$ is optimal. We now assume that for all even
$i\in\llbracket 2,n-1\rrbracket$, we have $w(x_{i},x_{i-1})>u$.

    * –

It follows that, for any odd $i\in\llbracket 0,n-1\rrbracket$, $w(x_{i})\leq
u$ and $w(x_{i},x_{i-1})\leq u$ — otherwise Player $\mathsf{A}$ could ensure
that the value of the game is more than $u$ by playing the corresponding row,
i.e. action $a_{i}$ or $a_{i,i-1}$. It also implies that $u^{\prime}\leq u$.
Indeed, assume that it is not the case, i.e. $u^{\prime}>u$. Consider a
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}\in\mathcal{D}(\\{a_{\mathsf{t}},a_{\mathsf{b}}\\})$ whose
value in the game in normal form $\langle\mathcal{T}_{n},v\rangle$ is greater
than $u$. Then, the Player-$\mathsf{A}$ positional strategy
$\mathsf{s}_{\mathsf{A}}$ in the game $\mathcal{G}_{Y_{n}}$ that plays the
$\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ in $q_{\mathsf{init}}$ parity
dominates the valuation $v_{(\mathcal{F}_{n},E)}^{r}$ for some
$r>u$777Potentially, if it is not already the case, up to playing action
$a_{\mathsf{b}}$ with small yet positive probability., due to the assumptions
we made in the previous item. In fact, $u^{\prime}\leq u$.

Note that this implies $X_{\mathsf{Ex}}\neq\emptyset$. Indeed, assume that
$X_{\mathsf{Ex}}=\emptyset$. Let $\varepsilon>0$. Consider a
Player-$\mathsf{A}$ $\mathsf{GF}$-strategy $\sigma_{\mathsf{A}}$ in the game
form $\mathcal{T}_{n}$ that plays action $a_{\mathsf{t}}$ with probability
$1-\varepsilon$ and action $a_{\mathsf{b}}$ with probability $\varepsilon$.
Then, for some small enough, yet positive, $\varepsilon>0$ and since
$\frac{p(z)+3p(y)}{4}>u$ and $v(x_{0}),\ldots,v(x_{n-1})=u$, such a
$\mathsf{GF}$-strategy has value more than $u$ in the game in normal form
$\langle\mathcal{T}_{n},v\rangle$. Hence, $X_{\mathsf{Ex}}=\emptyset$.

    * –

Let us exhibit a Player-$\mathsf{B}$ $\mathsf{GF}$-strategy that is optimal
w.r.t. $Y_{n}$. Consider a Player-$\mathsf{B}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{B}}\in\mathcal{D}(\\{b_{\mathsf{l}},b_{\mathsf{r}}\\})$ that
is optimal in that game in normal form $\langle\mathcal{T}_{n},v\rangle$. Let
$\mathsf{s}_{\mathsf{B}}$ be the Player-$\mathsf{B}$ positional strategy in
the game $\mathcal{G}_{Y_{n}}$ that plays the $\mathsf{GF}$-strategy
$\sigma_{\mathsf{B}}$ at $q_{\mathsf{init}}$. Recall that we assume that for
any odd $i\in\llbracket 0,n-1\rrbracket$, $w(x_{i})\leq u$ and
$w(x_{i},x_{i-1})\leq u$, $\frac{3p(z)+p(y)}{4}\leq u$ and
$X_{\mathsf{Ex}}\neq\emptyset$. Therefore, the strategy
$\mathsf{s}_{\mathsf{B}}$ dominates the valuations $v_{Y_{n}}^{u}$ and no
Player-$\mathsf{A}$ action can, against the strategy
$\mathsf{s}_{\mathsf{B}}$, make the game loop indefinitely on
$q_{\mathsf{init}}$ while ensuring that the highest color seen is even,
almost-surely. In fact, this strategy $\mathsf{s}_{\mathsf{B}}$ parity
dominates the valuations $v_{Y_{n}}^{u}$. Hence, the Player-$\mathsf{B}$
$\mathsf{GF}$-strategy $\sigma_{\mathsf{B}}$ is optimal w.r.t. $(Y_{n})$,
recall Lemma 21.

Let us now consider the case of Player $\mathsf{A}$.

    * –

If $u=\frac{3p(z)+p(y)}{4}$, then playing action $a_{\mathsf{Ex}}$ is optimal.
We now assume that $\frac{3p(z)+p(y)}{4}<u$.

    * –

It follows that, for all even $i\in\llbracket 0,n-1\rrbracket$, we have
$w(x_{i})\geq u$ and for all even $i\in\llbracket 2,k-1\rrbracket$, we have
$w(x_{i,i-1})\geq u$. Otherwise Player $\mathsf{B}$ could play the action
$b_{i}$ or $b_{i,i-1}$ and ensure that the value of the game
$\mathcal{G}_{Y_{n}}$, from $q_{\mathsf{init}}$, is less than $u$.

    * –

Furthermore, for any odd $i\in\llbracket 1,n-1\rrbracket$, if either
$w(x_{i})\geq u$ or $w(x_{i},x_{i-1})\geq u$, then playing action $a_{i}$ or
action $a_{i,i-1}$ is optimal. We now assume that, for all odd $i\in\llbracket
A,k-1\rrbracket$, $w(x_{i})<u$ and $w(x_{i},x_{i-1})<u$.

    * –

Assume that $X_{\mathsf{Ex}}\neq\emptyset$. Then, we have $u^{\prime}\geq u$.
This is analogous to the previous case for Player $\mathsf{B}$. Indeed, assume
that $u^{\prime}<u$. Then, consider a Player-$\mathsf{B}$
$\mathsf{GF}$-strategy
$\sigma_{\mathsf{B}}\in\mathcal{D}(\\{b_{\mathsf{l}},b_{\mathsf{r}}\\})$ whose
value in the game in normal form $\langle\mathcal{T}_{n},v\rangle$ is less
than $u$. Then, a Player-$\mathsf{B}$ positional strategy
$\mathsf{s}_{\mathsf{B}}$ in the game $\mathcal{G}_{Y_{n}}$ that plays the
$\mathsf{GF}$-strategy $\sigma_{\mathsf{B}}$ in $q_{\mathsf{init}}$ parity
dominates the valuation $v_{Y_{n}}^{r}$ for some $r<u$, due to the assumptions
we made in the previous item and since we assume that
$\frac{3p(z)+p(y)}{4}<u$. In fact, $u^{\prime}\geq u$.

Therefore, in the case where $X_{\mathsf{Ex}}\neq\emptyset$, Player
$\mathsf{A}$ has an optimal $\mathsf{GF}$-strategy w.r.t. $Y_{n}$ that
consists in playing optimally (in
$\mathcal{D}(a_{\mathsf{t}},a_{\mathsf{b}})$) in the game in normal form
$\mathsf{val}{\langle\mathcal{T}_{n},v\rangle}$, due to the assumptions of the
previous item.

    * –

Let us now assume that $X_{\mathsf{Ex}}=\emptyset$. Since, for all even
$i\in\llbracket 0,n-1\rrbracket$, we have $w(x_{i})\geq u$, it follows that
$n_{x_{i}}$ is even and at least equal to $c$. Similarly, since for all odd
$i\in\llbracket 1,n-1\rrbracket$, we have $w(x_{i})<u$. That is, $m_{x_{i}}$
is odd or less than $c$. In addition, for all even $i\in\llbracket
2,n-1\rrbracket$, we have $w(x_{i,i-1})\geq u$. That is,
$n_{x_{i}}>n_{x_{i-1}}$. Similarly, for all odd $i\in\llbracket
1,n-1\rrbracket$, we have $w(x_{i},x_{i-1})<u$, it follows that
$n_{x_{i}}>n(x_{i-1})$. We have $c\leq
n_{x_{0}}<n_{x_{1}}<\ldots<n_{x_{n-2}}<n_{x_{n-1}}\leq e$. This cannot happen
if $e-c\leq n-2$.

Let us now exhibit a relevant environment $E$ of size $n-1$ w.r.t. which
Player $\mathsf{A}$ has no optimal strategy. Consider the environment where
$c:=0$, $e:=n-1$, $p(z):=0$, $p(y):=1$ and for all $i\in\llbracket
0,n-1\rrbracket$, we have $p(x_{i}):=k_{i}$. We do have $\mathsf{Sz}(E)=n-1$.
Furthermore, the value $u$ of the parity game $\mathcal{G}_{Y_{n}}$ from
$q_{\mathsf{init}}$ is equal to $\frac{p(z)+3p(y)}{4}=\frac{3}{4}$. Indeed,
Player $\mathsf{B}$ ensures that $u\leq\frac{3}{4}$ by playing action
$b_{\mathsf{Ex}}$. Furthermore, for all $\varepsilon>0$, Player $\mathsf{A}$
can play with probability $1-\varepsilon$ action $a_{\mathsf{t}}$ and with
probability $\varepsilon$ action $a_{\mathsf{b}}$, thus ensuring that
$u\geq\frac{3}{4}-\varepsilon$.

Consider now an arbitrary Player-$\mathsf{A}$ $\mathsf{GF}$-strategy
$\sigma_{\mathsf{A}}$ and the corresponding positional strategy
$\mathsf{s}_{\mathsf{A}}$ in the game $\mathcal{G}_{Y_{n}}$. If
$\sigma_{\mathsf{A}}$ plays with positive probability action $a_{\mathsf{b}}$
or action $a_{\mathsf{Ex}}$, then the value of $\mathsf{s}_{\mathsf{A}}$ is
less that $u$ since $\frac{p(y)+3p(z)}{4}<\frac{p(z)+3p(y)}{4}$ (Player
$\mathsf{B}$ can play the action $b_{\mathsf{r}}$). However, if
$\sigma_{\mathsf{A}}$ does not play these actions with positive probability,
then consider the Player $\mathsf{B}$ strategy $\mathsf{s}_{\mathsf{B}}$ that
plays action $b_{\mathsf{l}}$ with probability 1. It ensures that the value of
the strategy $\mathsf{s}_{\mathsf{A}}$ is 0. The reason why is the following:
the highest index that the variables $x_{0},x_{1},\ldots,x_{n-1}$ are mapped
to w.r.t. $p$ is $n-1$ and it is odd. Furthermore, all variables
$x_{1},x_{3},\ldots,x_{n-1}$ are mapped to odd indices. Finally, the highest
index that the variables $(x_{1},x_{0})$ are mapped to is $1$ and it is odd.
This is also the case for $(x_{3},x_{2})$, …,$(x_{n-1},x_{n-2})$. Hence, the
highest color seen infinitely often with $\mathsf{s}_{\mathsf{A}}$ and
$\mathsf{s}_{\mathsf{B}}$ is almost-surely odd, and surely no stopping state
is reached. ∎