From now on, we assume that the enumerations $\safeComp{x}_1,\dots, \safeComp{x}_{k_x}$ correspond to these orders: $\safeComp{x}_i <_x \safeComp{x}_j$ if $i<j$.

Structured signature automata.
The "preorders" of the "signature automaton" we plan to build will correspond to the following semantic properties:

* Preorder $0$ given by inclusion of residuals. Preorder  $\leqSig{0}$ corresponds to the inclusion of "residuals":

\[q\leqSig{0} p \;\iff \; \Lang{\initialAut{\A}{q}}\subseteq \Lang{\initialAut{\A}{p}}.\]

* Odd layers correspond to safe components. For $x\geq 2$ even, we define $\leqSig{x-1}$ by:

\[
q\leqSig{x-1}p \; \iff \;{q\lSig{x-2}p} \tor [{q\eqSig{x-2}p} \tand q \in \safeComp{x}_i \tand p\in\safeComp{x}_j \text{ with } i\leq j].
\]

In particular, $q\eqSig{x-1}p$ if and only if ${q\eqSig{x-2}p}$ and there is a path $q\lrp{w:\geq x} p$.

* Even preorders given by inclusion of safe languages. For $x\geq 2$, $x$ even, we define $\leqSig{x-1}$ by:

\[
q\leqSig{x} p \; \iff  \; {q\lSig{x-1}p} \tor [{q\eqSig{x-1}p} \tand \safeSig{x}{q}\subseteq \safeSig{x}{p}].
\]

These preorders already ensure some of the properties required to be a "signature automaton"; mainly, the "local monotonicity" of transitions using large priorities (Item <ref>), as well as the "congruence for" ${\geq}x$-transitions at $\eqSig{x}$-classes.
Note, however, that it is not clear (and will be an important part of our proof) that $\leqSig{x}$ is total for even $x$.

Given an (even or odd) "priority"  $d\in \NN$, we say that a "parity automaton" $\A$ in "normal form" together with "nested preorders" $\leq_0,\leq_1,\dots,\leq_d$ as above is a ""$d$-structured signature automaton"" if these "preorders" are "total@@preord" and moreover:

*  Strong congruence of $({\leq}x)$-priorities over even classes. Let $0\leq x\leq d$, $x$ even. For every $y\leq x$:

\[q\eqSig{x}q',\; q\re{a:y}p \;\tand \; q'\re{a:z}p' \; \implies \;  z=y \;\tand \; p = p'.\]

*  Classes at layer $x$ are $({>}x)$-connected. For $0\leq x\leq d$ and $q\eqSig{x}q'$, we have:

\[ q\neq q' \; \implies  \; \text{ there is a path } q\lrp{u:>x}q'.\footnotemark\]

We remark that, for $x$ odd, this property is already implied by Item <ref>.

* Safe centralisation. Let $2\leq x\leq d$ be an even "priority", and let $q\eqSig{x-2}p$. Then:

\[q\neqSig{x-1}p  \; \implies \; \safeSig{x}{q}\nsubseteq \safeSig{x}{p}.\]

We say that $\A$ is a ""structured signature automaton"" if it is a "$d$-structured signature automaton", for $d$ the maximal "priority" appearing in $\A$.

We draw the reader's attention to the fact that in Item <ref> we do not only require $p \eqSig{x} p'$, but impose $p = p'$. This will be necessary to guarantee that the relations $\eqSig{y}$ for even priorities $y>x$ are also "congruences for" "$x$-transitions".

A "deterministic" "$d$-structured signature automaton" is a "$d$-signature automaton".

The fact that $\leq_0$ refines the inclusion of residuals is ensured by Item <ref>.
Also, the "$({<}x)$-safe separation" at odd levels (Item <ref>) is directly implied by the fact that odd layers correspond to safe components (Item <ref>).

We now show by induction on $x$ that for each $x \leq d$, $x$ even, $\eqSig{x}$ is a "$[0,x]$-faithful congruence".
Consider two states $q \eqSig{x} q'$, which rewrites as $q \eqSig{x-1} q'$ and $\safeSig{x}{q} = \safeSig{x}{p}$, and pick a transition $q \re{a:y} p$.
There are two cases.

* If $y \leq x$, then by Item <ref>, we have $q' \re{a:y} p$.

* If $y > x$, then by monotonicity of safe languages (Lemma <ref>), we have $q' \re{a:\geq x} p'$ with $\safeSig{x}{p'} = \safeSig{x}{p}$, and by induction, $p' \sim_{x-2} p$.
From Item <ref>, it follows that $p' \sim_{x-1} p$ and thus $p' \sim_x p$, as required.

We conclude that $\eqSig{x}$ is a "$[0,x]$-faithful congruence".

Finally, the "local monotonicity of $({\geq} x)$-transitions" follows from the fact that even preorders correspond to the inclusion of safe languages (Item <ref>) and the monotonicity of safe languages (Lemma <ref>).

§.§ From half-positionality to signature automata

This section is devoted to the proof of the implication <ref> $\implies$ <ref> in Theorem <ref>.
Many of the ideas in this proof have already appeared in the warm-up section.
However further technical issues stem from the fact that we manipulate general "parity automata".
Details for a number of proofs are relegated to Appendix <ref>.

In the whole section, $W$ stands for an "objective" that is "half-positional over" finite, "$\ee$-free" "Eve-games".
These hypotheses will not necessarily be recalled in the statements of propositions.

§.§.§ Outline of the induction

Given a "deterministic" "parity automaton" "recognising" a "half-positional" objective, we will recursively define the "preorders" and equivalence relations making $\A$ a "structured signature automaton". The base case consists in showing that the  preorder $\leqSig{0}$ given by the inclusion of residuals is total, and ensuring Item <ref> of the definition for this preorder.
For the recursion step, we suppose that we have a "deterministic" "$(x-2)$-structured signature automaton" $\A$ "recognising" $W$, for $x$ even, and we define preorders $\leqSig{x-1}$ and $\leqSig{x}$ over $\A$ as imposed by Items <ref> and <ref>.
Then, we apply a sequence of operations, after which we obtain an "equivalent@@aut" "deterministic" "automaton", that is either "$x$-structured signature", or has strictly less states than $\A$.
In the first case, we continue to define preorders $\leqSig{x+1}$ and $\leqSig{x+2}$; in the second case, we restart the structuration procedure from the beginning, with a strictly smaller automaton. In both cases, we conclude by induction.

We conjecture that we can sequentially obtain all the preorders, without having to restart the construction at each step. However, we have not been able to overcome some technical difficulties preventing us to do so. We refer to the final subsection of Appendix <ref> for more details.

We give a more detailed account on the specific operations we apply to obtain the different items of the definition of a "structured signature automaton" and their order:

* Relation $\eqSig{x-1}$ and safe centralisation. We define $\eqSig{x-1}$, as determined by Item <ref>. Applying a generalisation of the procedure from <cit.>, we "$({<}x)$-safe centralise" $\A$, obtaining an equivalent automaton satisfying Item <ref>. The resulting automaton is no longer "deterministic", but it is "history-deterministic" and has a very restricted and controlled amount of "non-determinism".

* Total order in safe components.
We prove that the states of each "$({<}x)$-safe component" are totally ordered by inclusion of "$({<}x)$-safe languages" (for which we rely on the "safe centralisation@@sig" hypothesis).
This shows that the preorder $\leqSig{x}$ given by the inclusion of "safe languages@@sig" (Item <ref>) is total.

* Re-determinisation. We determinise automaton $\A$, while preserving previously obtained properties. For this, the fact that $\leqSig{x}$ is total will be key.

* Uniformity of $x$-transitions. Finally, we show that either $\A$ already satisfies Items <ref> and <ref>, or we can trim the automaton to an "equivalent@@aut" strictly smaller one.

Moreover, we show that all these transformations can be performed in polynomial time.

This establishes that an objective $W$ that is "half-positional over" finite, "$\ee$-free" "Eve-games" can be "recognised" by a "deterministic" "structured signature" automaton.
At the end of the section, we show that such an automaton must be "fully progress consistent" (Lemma <ref>).

§.§.§ Constructing structured signature automata for half-positional languages

Let $\A = (Q, \SS, q_{\mathsf{init}}, [0,d_{\max}], \DD, \parity)$ be a "deterministic" "parity automaton" "recognising" $W$, and suppose that $W$ is "half-positional over" finite, "$\ee$-free" "Eve-games".
We assume that $\A$ is in "normal form".

In this subsection, we will apply successive transformations to the automaton $\A$, ensuring an increasing list of properties.
At the beginning of each paragraph, we clearly state the properties that are assumed.
We allow ourselves to omit these hypotheses in the statements of propositions inside the paragraphs.

*Base case: Preorder $\leqSig{0}$.

We define $q\leqSig{0} p$ if $\Lang{\initialAut{\A}{q}}\subseteq \Lang{\initialAut{\A}{p}}$, as imposed by Item <ref>.
In Lemma <ref>, we showed that "half-positionality" of $W$ implies that this order is total. However, in our proof we used infinite, and not necessarily "$\ee$-free" games. It is not difficult to modify the proof to adapt to this set of minimal hypotheses, using "$\oo$-regularity" of $W$. We give all details in Appendix <ref> (Lemma <ref>).
Items <ref>, <ref>, and <ref> are trivially satisfied.
Therefore, it suffices to show that we can obtain an automaton such that $\eqSig{0}$ is a "strong congruence for transitions" producing "priority" $0$ (Item <ref>), and that $\eqSig{0}$-equivalent states can be connected by paths producing priority ${>}x$ (Item <ref>). For this, we apply exactly the same method presented in Section <ref>: we obtain a "polished automaton@@buchi" and show that it satisfies the desired properties. This proof will be covered in the recursive step; the case $x=0$ does not present any particularity.

Moving on to the inductive step, for the rest of the subsection, we let $x$ be an even priority such that $2<x\leq d_{\max}$ and assume that $\A$ is a "deterministic" "$(x-2)$-structured signature automaton".

*Safe centrality and relation $\eqSig{x-1}$.
We say that an automaton with a "preorder" $\leqSig{x-2}$  is ""$({<}x)$-safe centralised"" if $\eqSig{x-2}$-equivalent states that are comparable for the inclusion of "$({<}x)$-safe languages" are in the same "$({<}x)$-safe component".

For automata in "normal form" "$({<}x)$-safe centrality"  can be stated as:
if $q\eqSig{x-2} p$ and there is no "$({<}x)$-safe path" connecting $q$ and $p$, then $\safeSig{x}{q} \nsubseteq \safeSig{x}{p}$.

[$({<}x)$-safe centralisation]lemmalemnecSafeCentralisation
There exists a "$(x-2)$-structured signature" automaton $\A'$ "equivalent to" $\A$ which is:

* "deterministic over" transitions with "priority" different from $x-1$,

* "homogeneous",

* "history-deterministic", and

* "$({<}x)$-safe centralised".

Moreover, $\A'$ can be obtained in polynomial time from $\A$ and $\sizeAut{\A'}\leq \sizeAut{\A}$.

Lemma <ref>.

The proof of this lemma is a refinement of the corresponding result for "coBüchi automata" presented in the warm-up (Lemma <ref>): we saturate $\eqSig{x-2}$-classes of the original automaton $\A$ with "$(x-1)$-transitions@@out", and then remove "redundant@@safeCentr" "$({<}x)$-safe components" recursively until obtaining a "$({<}x)$-safe centralised" automaton.  We include all details in Appendix <ref> (page lemma-p4-nec:safe-centralisation-pageApp).

Lemma <ref> allows us to define $\eqSig{x-1}$ satisfying all required properties:
for $q\eqSig{x-2}p$, we define $q\leqSig{x-1} p$ if and only if $q\in \safeComp{x}_i$ and $p\in \safeComp{x}_j$ with $i\leq j$, where $\safeComp{x}_i$ are the "$({<}x)$-safe components" of $\A$ enumerated following the order described in Section <ref>.
By definition,  Item <ref> is satisfied, and by "$({<}x)$-safe centralisation" of $\A$, so is Item <ref>.

*Preorder $\leqSig{x}$: Total order given by safe languages

In all this paragraph we assume that $\A$ is an automaton as obtained in the previous paragraph, that is: it has "nested preorders" defined up to $\leqSig{x-1}$ making it a "$(x-2)$-structured signature automaton" and satisfying Items <ref> and <ref> for relation $\eqSig{x-1}$. Moreover, it is  "history-deterministic", "homogeneous", and the only non-determinism of $\A$ appears in "$(x-1)$-transitions@@out".

We define "preorder" $\leqSig{x}$ as imposed by Item <ref>:

\[  q\leqSig{x} p \; \iff q \lSig{x-1} p \tor [ q \eqSig{x-1} p \tand  \; \safeSig{x}{q}\subseteq \safeSig{x}{p} ],\]

and recall that it follows that $q \eqSig x p $ if and only if $q \eqSig{x-1} p$ and there is a "$(<x)$-safe path" from $q$ to $p$.

Using Item <ref> for priorities $y \leq x-2$ and Lemma <ref> for transitions with priority $\geq x$, we get that
relation $\eqSig{x}$ is a "congruence for" transitions with a priority different from $x-1$.
Moreover, over each $\eqSig{x-1}$-class, transitions with priority ${\geq}x$ are "monotone for" $\leqSig{x}$.

Our objective is now to show that $\leqSig{x}$ is "total@@order" over each $\eqRes{x-1}$-class. The proof of this statement uses the same ideas as the corresponding result from the warm-up (Lemma <ref>). In particular, the main technical point resides in proving that, for two states $q_1 \nleqSig{x} q_2$, we can force to produce priority $x-1$ from $q_1$ while remaining "${<}x$-safe@@path" from $q_2$, and then resynchronise both paths in a same $\eqSig{x}$-class. This result, stated in Lemma <ref>, is the analogue to Lemma <ref> from the warm-up. For its proof we strongly rely on the "$({<}x)$-safe centralisation" of $\A$ and the fine control of its non-determinism.

In the proofs of Lemmas <ref> and <ref> we will reason at the level of $\eqSig{x}$-classes. As we only suppose that $\A$ is "$(x-2)$-structured", we do not have the "uniformity@@trans" of $x$-transitions over $\eqSig{x}$-classes yet. Lemma <ref> below provides a weaker version of this uniformity that will suffice for the arguments in the upcoming lemmas.

We say that a word $w$ ""produces priority $y$ uniformly"" in a class $\classSig{x}{q}$ if for every $q'\in \classSig{x}{q}$ all runs from $q'$ are of the form $q'\lrp{w:y}$.
In that case, we write $\classSig{x}{q}\lrp{w:y}$.
We say that such a word "produces priority $x$ uniformly in" $\classSig{x}{q}$ ""leading to@@class"" $\classSig{x}{p}$ if for every $q' \in \classSig{x}{q}$ we have $q' \lrp{w:y} p'$ with $p' \in \classSig{x}{p}$.
In that case, we write $\classSig{x}{q} \lrp{w:y} \classSig{x}{p}$.

We note that whenever $\A$ contains a path $q\lrp{w:\geq x} p$, a "run over" $w$ is unique, as $\A$ is "homogeneous" and its restriction to transitions coloured with priorities $\geq x$ is "deterministic".

The proof of the next lemma combines "normality" of $\A$ with ideas appearing in the proof of Claim <ref> from the warm-up; all the details can be found in Appendix <ref> (page lemma-p4-nec:uniformity-x-transitions-pageApp).

[Existence of uniform words]lemmalemNecExistenceUniformWords
Let $p$ and $q$ be two states from the same "$({<}x)$-safe component".
There is a word $w \in \SS^*$ "producing priority $x$ uniformly" in $\classSig{x}{q}$ "leading to@@class" $\classSig{x}{p}$.

We next state the result that allows us to synchronise runs in a same $\eqSig{x}$-class.
Its proof is analogous to that of Lemma <ref> and can be found in Appendix <ref>.

We let $\resolv$ be a "sound resolver" for $\A$, and assume that all states can be reached by a "run induced by@@resolv" this "resolver".
We recall that we write $q\lrpAllResolver{\resolv}{w:y}p$ if, for every word $u_0\in \SS^*$ such that the "induced run of $\resolv$ over $u_0$" arrives to $q$, the "induced run of $\resolv$ over" $u_0w$ ends in $p$ and produces $y$ as minimal "priority" in the part of the run corresponding to $w$.
Recall also that we write $\classSig{x}{q} \lrpAllResolver{\resolv}{w:y} \classSig{x}{p}$ if for any $q' \in \classSig{x}{q}$ we have $q' \lrpAllResolver{\resolv}{w:y} p'$ for some $p' \in \classSig{x}{p}$.

[Synchronisation of separating runs]lemmalemNecSynchronisation

Suppose that $q \eqSig{x-1} q'$ and $q \nleqSig{x} q'$ and let $p\in \classSig{x-1}{q}$.
There is a word $w\in \SS^+$ such that $\classSig{x}{q} \lrpAllResolver{\resolv}{w:x-1} \classSig{x}{p}$ and $\classSig{x}{q'} \lrpAllResolver{\resolv}{w:x} \classSig{x}{p}$.

We can now deduce that $\leqSig{x}$ is "total@@order" over each $\eqRes{x-1}$-class.

Let $q,q'\in Q$ be two states such that $q\eqRes{x-1}q'$.

Then, either $q\leqSig{x} q'$ or $q'\leqSig{x} q$.

Suppose by contradiction that $\safeSig{x}{q} \nsubseteq \safeSig{x}{q'}$ and $\safeSig{x}{q'} \nsubseteq \safeSig{x}{q}$.
Let $p$ be a state in $\classSig{x-1}{q}=\classSig{x-1}{q'}$, and apply Lemma <ref> to obtain words $u,u'\in \SS^*$ such that $\classSig{x}{p}\lrp{u:x}\classSig{x}{q}$ and $\classSig{x}{p}\lrp{u':x}\classSig{x}{q'}$.

By Lemma <ref>, there are words $w,w'\in \SS^\oo$ such that:

$\classSig{x}{q}\lrpAllResolver{\resolv}{w:x}\classSig{x}{p}$,     $\classSig{x}{q}\lrpAllResolver{\resolv}{w':x-1}\classSig{x}{p}$,

$\classSig{x}{q'}\lrpAllResolver{\resolv}{w:x-1}\classSig{x}{p}$,     $\classSig{x}{q'}\lrpAllResolver{\resolv}{w':x}\classSig{x}{p}$.

The situation is analogous to the one depicted in Figure <ref> in the warm-up.
We obtain that:

* $(w'u)^\oo\notin \Lang{\initialAut{\A}{q}}$,

* $(wu')^\oo\notin \Lang{\initialAut{\A}{q}}$,

* $(wu'w'u)^\oo\in \Lang{\initialAut{\A}{q}}$.

Let $u_0\in \SS^*$ be a word such that the "run induced by $\resolv$" over $u_0$ ends in $q$ (it exists, as we have supposed that all states are "reachable using $\resolv$").
It suffices to consider the "game" where there is path labelled $u_0$ leading to  a vertex controlled by "Eve" with two self loops; one of them producing $w'u$ and the other $wu'$. By the previous remarks, she can "win" such game by alternating both loops, but she cannot "win positionally".

*Re-obtaining determinism
In this paragraph we assume that $\A$ is a "parity automaton" "recognising" $W$  equipped with "nested total preorders" defined up to $\leqSig{x}$ with all properties obtained until now:

* it is a "$(x-2)$-structured signature automaton",

* preorder $\leqSig{x-1}$ satisfies properties from Items <ref> and <ref> from the definition of a "structured signature automaton",

* preorder $\leqSig{x}$ satisfies the property from Item <ref> from the definition of a "structured signature automaton",

* it is "deterministic over" transitions with priorities different from $x-1$,

* it is "homogeneous", and

* it is "history-deterministic".

We claim that we can obtain a "deterministic" "equivalent@@aut" "automaton" preserving the entire structure of "total preorders". Moreover, in the obtained automaton we guarantee that relation $\eqSig{x}$ satisfies Item <ref> from the definition of a "structured signature automaton" for priorities $y<x$.

There is a "deterministic" "parity automaton" $\A'$ "equivalent to" $\A$ with "nested total preorders" defined up to $\leqSig{x}$ satisfying that:

* it is a "$(x-2)$-structured signature automaton",

* preorder $\leqSig{x-1}$ satisfies properties from Items <ref> and <ref> from the definition of a "structured signature automaton", and

* preorder $\leqSig{x}$ is a "congruence" and satisfies the property from Item <ref> and, for priorities $y<x$, also that from Item <ref> .

Moreover, automaton $\A'$ can be computed in polynomial time from $\A$ and $\sizeAut{\A'}\leq \sizeAut{\A}$.

The idea of the proof is a direct generalisation of the one presented in the warm-up for "coBüchi automata" (page par-p4-warm:determinisation): we redefine the $(x-1)$-transitions of the automaton in such a way that we ensure that a run that changes of "${<}x$-safe component" infinitely often passes through all these components in a round-robin fashion. The total order $\leqSig{x}$ allows us to identify a maximal state in each component, so we can make a deterministic choice.
Formal details can be found in Appendix <ref> (page lemma-p4-nec:re-determinisation-pageApp).

*Uniformity of $x$-transitions over $\eqSig{x}$-classes

We assume that $\A$ is a "deterministic" "parity automaton" "recognising" $W$ with "nested total preorders" defined up to $\leqSig{x}$ satisfying all conditions stated in Lemma <ref>.
The objective of this paragraph is to obtain the remaining properties of a "$x$-structured signature automaton" (Items <ref>
and <ref>).

[Uniformity of $x$-transitions over $\eqSig{x}$-classes]lemmalemNecUniformity
There is a "deterministic" "parity automaton" $\A'$ "equivalent to" $\A$ such that either:

* $\A'$ is an "$x$-structured signature automaton" with $\sizeAut{\A'}\leq \sizeAut{\A}$, or

* $\sizeAut{\A'}< \sizeAut{\A}$.

In both cases, such an automaton can be computed in polynomial time from $\A$.

The proof of this lemma generalises the techniques introduced in Section <ref> of the warm-up. Details can be found in Appendix <ref> (from page lemma-p4-nec:uniformity-x-transitions-pageApp).
We introduce the "local automaton of a $\eqSig{x}$-class" $\classSig{x}{q}$: the automaton originated by keeping the states of $\classSig{x}{q}$ and paths connecting them producing priorities $\geq x$.
Using "half-positionality" and ideas analogous to those from Lemma <ref>, we show that these "local automata" admit a well-defined set of "super letters", that is, there are letters that, if read infinitely often in such a "local automaton", must produce an "accepting word".
These letters are exactly the ones carrying priority $x$ when read from $\classSig{x}{q}$ in the final automaton $\A'$.

To obtain the uniformity of $x$-transitions, we might need to simplify the automaton: we introduce "$x$-polished automata", the target form of automata that will allow us to obtain "uniformity@@cong" of $x$-transitions.
Using the existence of "super letters", we show that we can "polish@@sig" automaton $\A$ by removing "redundant@@sig" parts of it.
This operation might break the "normal form" of automaton $\A$, but this is not a problem, since in any case it strictly decreases the number of states of the automaton, as desired.

In fact, we believe that the "polishing operation" does preserve "normality", but we have not been able to prove it.

This ends the induction step of the proof, establishing existence of a "deterministic" "structured signature" automaton "recognising" $W$.

§.§.§ Full progress consistency

We show that a "structured signature automaton" "recognising" a "half-positional" objective must be "fully progress consistent".
Since we showed how to obtain such a "structured signature automaton" in the previous section, this ends the proof of the implication <ref> $\implies$ <ref> from Theorem <ref>.

Let $W\subseteq \SS^\oo$ be "half-positional" over finite, "$\ee$-free" "Eve-games".
Any "structured" "signature automaton" "recognising" $W$ is "fully progress consistent".

Suppose by contradiction that $\A$ is a "structured signature automaton" for $W$ that is not "fully progress consistent". By definition, for some priority $x$ even, there are $q\lSig{x} p$ and a word $w\in \SS^*$ such that $q\lrp{w:\geq x} p$, but $w^\oo \notin \Lang{\initialAut{\A}{q}}$.
As $\eqSig{x}$ is a "$[0,x]$-faithful congruence", we can work with $\eqSig{x}$-classes and write $\classSig{x}{q}\lrp{w:\geq x}\classSig{x}{p}$.
We study first the case $x>0$.
By Lemma <ref>, there is a word $u\in \SS^+$ such that $\classSig{x}{q}\lrp{u:x-1}\classSig{x}{q}$ and $\classSig{x}{p}\lrp{u:x}\classSig{x}{q}$.
Let $u_0\in \SS^+$ be a word reaching $q$ from the "initial state" of $\A$.[If $q$ is "initial", we omit $u_0$ and the state $v_0$ of the game from Figure <ref> to ensure the use of an "$\ee$-free" game.] We obtain:

* $u_0w^\oo\notin W$,

* $u_0u^\oo \notin W$, and

* $u_0(wu)^\oo\in W$.

We consider the game depicted in Figure <ref>. "Eve" can "win from $v_0$" by alternating loops labelled $w$ and $u$ when the play arrives to $v_{\mathsf{choice}}$. However, she cannot "win positionally" from $v_0$.

A game $\G$ in which "Eve" cannot "play optimally using positional strategies" if $\A$ is not "fully progress consistent".

For the case $x=0$, the proof is almost identical to that of Lemma <ref>; we just need to ensure that the "game" in Figure <ref>  (page fig-p4-warm:game-prog-cons) can be supposed finite and "$\ee$-free". Finiteness of the game can be obtained by using ultimately periodic words. To guarantee that we do not include $\ee$-transitions, if $u_0=\ee$, we remove vertex $v_0$ from the game.

§.§ From signature automata to half-positionality through $\ee$-complete automata

We now complete the proof of Theorem <ref> by showing the two implications <ref> $\implies$ <ref> and <ref> $\implies$ <ref>.
The implication <ref> $\implies$ <ref> follows from Proposition <ref> (taken from <cit.>)  and <ref> $\implies$ <ref> is trivial.

§.§.§ $\ee$-complete automata

We start with our crucial definition.

An ""$\ee$-complete"" automaton $\A$ is a "non-deterministic" "parity automaton" (with "$\ee$-transitions@@aut") with priorities ranging between 0 and $d+1$, where $d$ is even, such that

* the relations $\re{\ee:1}, \re{\ee:3},\dots,\re{\ee,d+1}$ all define total preorders, each refining the previous one;

* for each even $x \in \{0,2,\dots,d\}$, the relation $\re{\ee:x}$ is the strict variant of $\re{\ee:x+1}$: for any $q,q'$, it holds that $q \re{\ee:x} q'$ if and only if $q' \re{\ee:x+1} q$ does not hold.

We say that an automaton $\A$ (which will usually be taken deterministic) is ""$\ee$-completable"", if one may add $\ee$-transitions to $\A$ so as to make it "$\ee$-complete", without augmenting the language.
We say that the resulting (generally non-deterministic) automaton $\A'$ is an ""$\ee$-completion"" of $\A$; note that if $\A$ is deterministic, then $\A'$ is "history-deterministic" (it is even determinisable by pruning).
We refer to Figure <ref> in Section <ref> for an example.

§.§.§ From signature automata to $\ee$-completable automata

We now prove the implication <ref> $\implies$ <ref> from Theorem <ref>, which can be stated as follows.

Let $\A$ be a "fully progress consistent" "deterministic" "signature automaton".
Then $\A$ is "$\ee$-completable".

We prove Lemma <ref>. We refer to the discussion at the end of Section <ref> (Figure <ref>) for an example on the ideas of this proof.
Let $\A$ be a "fully progress consistent" "deterministic" "signature" automaton with "nested preorders" $\leqSig{0},\leqSig{1},\dots, \leqSig{d}$ and let $W=\Lang{\A}$.
Consider the automaton $\A'$ obtained from $\A$ by adding, for all even priorities $x \in [0,d]$, transitions $q \re{\ee:x+1} q'$ whenever $q' \leqSig{x} q$ and $q \re{\ee:x} q'$ whenever $q' \lSig{x} q$.
Note that $\A'$ (potentially) has transitions with priorities up to $d+1$.

Note that, for $x$ even, $q \re{\ee: \geq x} p$ in $\A'$ entails $p \leqSig{x} q$.

Since by definition, $q' \lSig{x} q$ is the negation of $q \leqSig{x} q'$, it follows immediately that $\A'$ is "$\ee$-complete". Moreover, as $\A$ is a "subautomaton" of $\A'$, the inclusion $W\subseteq \Lang{\A'}$ is trivial. The difficulty lies in showing that $\Lang{\A'}\subseteq W$.

If $q\lrp{w:x} q$ is a cycle in $\A'$ producing an even minimal priority, then $w$ is not composed exclusively of "$\ee$-letters".

For a priority $x$ (even or odd), we say that a transition $q \re{\ee} q'$ in $\A'$ is an ""$x$-jump"" if $q' \lSig{x} q$.
We remark that if $x'\leq x$, an "$x'$-jump" is an "$x$-jump".

We start with a useful technical lemma.

Fix a path $q' \lrp{w':\geq x} p'$ in $\A'$, with $x$ even, such that  and consider a "run" $q \lrp{w\phantom{.}} p$ in $\A$, where $w$ is obtained from $w'$ by removing "$\ee$-letters" (where $p=q$ if $w'$ is empty).

*  Assume that there is no "$x$-jump" on $q' \lrp{w':\geq x} p'$ and that $q \eqSig{x} q'$.
Then $p \eqSig{x} p'$ and $q \lrp{w:\geq x} p$ in $\A$.
Moreover, if $q' \lrp{w':x} p'$, then $q \lrp{w:x} p$ in $\A$.

*  Assume that there is no "$(x-1)$-jump" on $q' \lrp{w':\geq x} p'$, that $q' \eqSig{x-1} q$ and $q' \leqSig{x} q$. Then $p' \eqSig{x-1} p$, $p' \leqSig{x} p$ and $q \lrp{w:\geq x} p$ in $\A$.

*  We have that $p'\leqSig{x-1}q'$.

In the two first cases we deal with the case of a letter and conclude by induction.

* There are two possibilities, depending on whether  the letter is $\ee$ or not.

* Transition $q' \re{a:\geq x} p'$ with $a \in \SS$.
Then "$[0,x]$-faithfulness" of $\eqSig{x}$ gives $p \eqSig{x} p'$ and $q \re{a:\geq x} p$.
Moreover if $q' \re{a:x} p'$, then by "$[0,x]$-faithfulness", $q \re {a:x} p$.

* Transition $q' \re{\ee:\geq x} p'$.
Then $p' \leqSig{x} q'$ and since there is no "$x$-jump", $p' \eqSig{x} q'$. Thus $p=q \eqSig{x} q' \eqSig{x} p'$.

* We distinguish the  two same cases.

* Transition $q' \re{a:\geq x} p'$ with $a \in \SS$.
Then "local monotonicity of $({\geq}x)$-transitions" in $\A$ yields $q \re{a:\geq x} p$ in $\A$ with $p' \leqSig{x} p$. By Remark <ref>, $p' \eqSig{x-1} p$.

* Transition $q' \re{\ee:\geq x} p'$.
This implies $p' \leqSig{x} q'$ and since there is no "$(x-1)$-jump", we have $p' \eqSig{x-1} q'$.
Thus we conclude that $p' \leqSig{x} q' \leqSig{x} q=p$ and $p=q \eqSig{x-1} q' \eqSig{x-1} p'$.

* Suppose by contradiction that $p'\gSig{x-1} q'$, and let $q_1'$ be the first state in the run such that $q'\lSig{x-1}q_1'$. We have:

\[q' \lrp{w_1':\geq x} q_2' \re{a:\geq x} q_1' \lrp{w_2'} p',\]

with $q_2'\lSig{x-1}q_1'$.  As in particular $q_2'\lSig{x}q_1'$, $a\neq \ee$ (Remark <ref>). However, this contradicts Item <ref> from the definition of "signature automaton".

We now state the key result for deriving Lemma <ref>.

Consider a cycle $q' \lrp{w':x} q'$ in $\A'$ with $x$ even, and let $w$ be obtained from $w'$ by removing "$\ee$-letters".
Then, $w^\omega$ is accepted from $q'$ in $\A$.

We note that by Remark <ref>, $w$ is not empty.
Let $y$ be minimal such that an "$y$-jump" appears on the path $q' \lrp{w':x} q'$.

* If $y \geq x$.
Then there is no $\re{\ee:x}$ transition on the path $q' \lrp{w':x} q'$ (otherwise it would produce an "$x$-jump").
Thus Lemma <ref>.<ref> proves $q' \lrp{w:x} q_1$ in $\A$ with $q_1 \eqSig{x} q'$.
Then, since the $\eqSig{x}$-class is preserved, successive applications of Lemma <ref>.<ref> give $q'\lrp{w:x} q_1 \lrp{w:x} q_2 \lrp{w:x} q_3 \lrp{w:x} \dots$ in $\A$, and thus $w^\oo$ is "accepted@@aut" from $q'$ in $\A$.

* If $y < x$ and $y$ odd. We show that this case cannot happen. Let $p'_1 \re {\ee} p'_2$ denote the first "$y$-jump" on the path $q' \lrp{w} q'$ in $\A'$, that is, we have

\[
q' \lrp{w'_1:> y} p'_1 \re{\ee:> y} p'_2 \lrp{w'_2:> y} q' \tin \A', \quad p_2'\lSig{y}p_1'.
\]

By Lemma <ref>.<ref>, we have that $p_1'\leqSig{y} q'$, so $p_2'\lSig{y}q'$. The existence of a path $p'_2 \lrp{w'_2:\geq y} q'$ contradicts Lemma <ref>.<ref>.

* If $y < x$ and $y$ even.
Let $p'_1 \re {\ee} p'_2$ denote the last "$y$-jump" on the path $q' \lrp{w} q'$ in $\A'$, that is, we have

\[
q' \lrp{w'_1:\geq y} p'_1 \re{\ee:\geq y} p'_2 \lrp{w'_2:\geq y} q' \tin \A', \quad p_2'\lSig{y}p_1',
\]

and there is no "$y$-jump" on $p'_2 \lrp{w_2} q'$. We let $w_1,w_2$ be obtained, respectively, from $w'_1$ and $w'_2$ by removing $\ee$'s.
By Lemma <ref>.<ref>, we get that $p'_2 \lrp{w_2:\geq y} {q}$ in $\A$ for some $q \sim_{y} q'.$
As there is no "$(y-1)$-jump" in the path, by  Lemma <ref>.<ref>, we get that $q \lrp{w_1:\geq y} p_1$ in $\A$ for $p_2' \lSig{y} p_1' \leqSig{y} p_1$. See Figure <ref> for an illustration of the situation.

Situation in the third case of Lemma <ref>. Dashed lines represent paths in $\A'$ and solid lines those in $\A$. States that are $\eqSig{y}$-equivalent are encircled together.

All in all, we have obtained a path

\[p_2' \lrp{w_2:\geq y} q \lrp{w_1: \geq y} p_1 >_{y} p'_2 \quad \text{ in } \A.\]

Therefore, "full progress consistency" yields $(w_2w_1)^\omega \in \Lang{\initialAut{\A}{p_2'}}$.
As $\Lang{\initialAut{\A}{p_2'}} \subseteq \Lang{\initialAut{\A}{q'}}= \Lang{\initialAut{\A}{q}}$, we conclude that $w^\omega = (w_1w_2)^\oo \in \Lang{\initialAut{\A}{q}}$.

We are now ready conclude the proof of Lemma <ref>.

As mentioned above, the inclusion $	W\subseteq \Lang{\A'}$ is trivial, as $\A$ is a subautomaton of $\A'$. This shows that, if the converse inclusion holds, $\A'$ is determinisable by pruning and therefore it is also "history-deterministic".

We show $\Lang{\A'}\subseteq W$.
Take an accepting run in $\A'$ over $w'\in \SS^\oo$ and decompose it as:

\[
q_0 \lrp{w'_0} q' \lrp{w'_1:x} q' \lrp{w'_2:x} q' \lrp{w'_3:x} \cdots,
\]

where $x$ is even.
For each $i$, let $w_i$ be obtained from $w'_i$ by removing $\ee$'s (which is non-empty by Remark <ref>), and consider the corresponding run in $\A$:

\[
q_0 \lrp{w_0} q_1 \lrp{w_1} q_2 \lrp{w_2} q_3 \lrp{w_3} \cdots,
\]

It follows by induction that $q' \leqSig{0} q_i$, so, as order $\leqSig{0}$ "refines" the order of residuals (property <ref> of a "signature automaton"), words that are accepted from $q'$ in $\A$ are also "accepted@@aut" from  $q_i$.
By Lemma <ref>, it holds that for each pair of indices $j\leq j'$ we have $(w_jw_{j+1}\dots w_{j'})^\omega \in q^{-1}W$, so these words are also accepted from $q_i$, for all $i$.

Let $i_1,i_2,\dots$ be a sequence of indices such that $q_{i_j} = q_{i_{j+1}}$ for all $j$, and let $\tilde{q}=q_{i_1}$ be such recurring state.
Each word $w_{i_j}\dots w_{i_{j+1}}$ forms a cycle over $\tilde{q}$, that, by the previous remark, must be accepting, so the minimal priority produced on it is even. Therefore, we have found a decomposition of the run over $w$ in $\A$ of the form

\[
q_0 \lrp{w_0w_1\dots} \tilde{q} \lrp{w_{i_1}\dots w_{i_2} : x_1} \tilde{q} \lrp{w_{i_2}\dots w_{i_3} : x_2}  \cdots,
\]

with all $x_i$ even. We conclude that  $w_0w_1 \dots \in W$.

§.§.§ Universal graphs from $\ee$-complete automata

We now move on to implication <ref> $\implies$ <ref> in Theorem <ref>.
We even prove a stronger result: "history-determinism" is sufficient here.

If there is a "$\ee$-complete" "history-deterministic" automaton "recognising" $W$, then there is a "well-ordered" "monotone@@univ" "$(\kappa,W)$-universal" graph for each cardinal $\kappa$.

For the rest of the section, we let $\A$ be an "$\ee$-complete" "history-deterministic" automaton "recognising" $W$, and we let $d$ be even such that $\A$ has priorities up to $d+1$, as in the above section.

*Closure of an $\ee$-complete automaton

We define the order $\intro*\cleq$ over "priorities" in $[0,d+1]$ that sets $y\cleq x$ if $x$ is “preferable” to $y$, that is:  $1 \cleq 3 \cleq \dots \cleq d+1 \cleq d \cleq \dots \cleq 2 \cleq 0$.

For any pair of infinite words $w, w' \in [0,d+1]^\oo$ satisfying that for all $i$  $w_i \cleq w'_i$, it holds that:

\[w\in \parity_{[0,d+1]} \implies  w'\in \parity_{[0,d+1]}.
%\limsup_i(w_i) \text{ is even } \implies \limsup_i(w'_i) \text{ is even}.
\]

We say that an automaton $\A$ is ""priority-closed"" if:

* for any states $q,q'$, priorities $y' \cleq y$, and $a \in \SS \cup \{\ee\}$

\[
q \re{a:y} q' \implies q \re{a:y'} q'
\]

* for any states $p,p',q,q'$ and $a \in \SS \cup \{\ee\}$,

\[
p \re {\ee:y_1} q \re{a:y_2} q' \re{\ee:y_3} p' \implies p \re {a:\min_{\cleq}(y_1,y_2,y_3)} p'.
\]

It is easy to turn any automaton into a "priority-closed@@aut" one.

Let $\A$ be an automaton recognising $W$.
There is an automaton $\A'$ recognising $W$ which is "priority-closed@@aut".
Moreover, if $\A$ is "history-deterministic" and "$\ee$-complete", then so is $\A'$.

Let $\A'$ be obtained by adding to $\A$ all transitions of the form $q \re {a:y'} q'$, when $q \re{a:y} q'$ is a transition in $\A$ and $y' \cleq y$, and all transitions of the form $p \re {a:\min_{\cleq}(y_1,y_2,y_3)} p'$, whenever a path $p \re {\ee:y_1} q \re{a:y_2} q' \re{\ee:y_3} p'$ appears in $\A$.
Clearly, $\A'$ is "priority-closed@@aut", $\Lang{\A} \subseteq \Lang{\A'}$ and if $\A$ is  "$\ee$-complete", then so is $\A'$.
The fact that this operation preserves "history-determinism" is also clear, once the equality of languages is obtained.
To prove that $\Lang{\A'} \subseteq \Lang{\A}$, take an accepting "run over" $w\in\SS^\oo$ in $\A'$. We build a run over $w$ in $\A$ by replacing any newly added transition $q \re {a:y'} q'$ by $q \re{a:y} q' $,  and $p \re {a:\min_{\cleq}(y_1,y_2,y_3)} p'$ by $p \re {\ee:y_1} q \re{a:y_2} q' \re{\ee:y_3} p'$, respectively. By Remark <ref>, the obtained run is "accepting@@run" in $\A$.

In a "priority-closed@@aut" automaton, for each "priority" $y$, transitions $\re{\ee:y}$ define a transitive relation.
If the automaton is moreover "$\ee$-complete", then for each even priority $x$, transitions of the form $\re{\ee:x+1}$ define "total preorders".

We define $q \intro*\geqHM{x} q'$ if $q \re{\ee:x+1} q'$.

Note that, since $\A$ is "priority-closed@@aut", these preorders are "nested@@preorder": $q \geq_{x+2} q'$ implies $q \geqSig{x} q'$.
Moreover, since $\A$ is "$\ee$-complete", for any even $x$:

\[
q \gHM{x} q' \implies q \re{\ee:x} q'.
\]

Finally, observe that, by "priority-closure", states $q,q'$ that are $\leqHM{d}$-equivalent have exactly the same incoming and outgoing transitions, and can thus be merged without altering the language (this transformation preserves "history-determinism").
Therefore, we may assume that $\leqHM{d}$ is antisymmetric and thus defines a total order on $Q$.

We write $\intro*\classHM{x}{q}$ to denote the equivalence class of $q$ associated to preorder $\leqHM{x}$. That is, $\classHM{x}{q}$ contains the states $q'$ such that $q\leqHM x q'$ and $q'\leqHM x q$.

*Definition of the graph

For the remainder of the section, we fix a cardinal $\kappa$.
Let us first recall the construction of the "$(\kappa,\parity)$-universal" graph $\UPar$ for the "parity objective" over $\{0,\dots,d+1\}$ (see Example <ref> for a proof of universality). Its vertices are of the form $(\lambda_1,\lambda_3,\dots,\lambda_{d+1}) \in \kappa^{d/2+1}$, ordered lexicographically, and its edges are given by

\[
(\lambda_1,\dots,\lambda_{d+1}) \re x (\lambda'_1,\dots,\lambda'_{d+1}) \iff \begin{cases}
(\lambda'_1,\dots,\lambda'_{x-1})\leq (\lambda_1,\dots,\lambda_{x-1}),  &\tif x \text{ is even}, \\
(\lambda'_1,\dots,\lambda'_{x})<(\lambda_1,\dots,\lambda_{x}), &\tow.
\end{cases}
\]

Fix a "priority-closed@@aut" "$\ee$-complete" and "history-deterministic" automaton $\A$ with states $Q$  such that $\leqHM{d}$ defines a total order on $Q$.

We define a "$\SS$-graph" $\intro*\UAut$ as follows.
Vertices of $\UAut$ are the tuples $v = (q,\lambda_{1},\lambda_3,\dots,\lambda_{d+1}) \in Q \times \kappa^{d/2+1}$.
We associate to each such vertex the ""extended tuple""

\[\intro*\ext(v) = (\classHM{0}{q},\lambda_1,\classHM{2}{q},\lambda_3,\dots,\classHM{d-1}{q},\lambda_{d+1}).\]

We use it to define the total order: $v\leq v'$ if $\ext(v)$ is smaller than $\ext(v')$ for the lexicographic order.
This is therefore a well-order.

Edges in $\UAut$ are given by:

\[(q,\lambda_{1},\dots,\lambda_{d+1}) \re {a} (q',\lambda_{1},\dots,\lambda_{d+1}) \; \iff \; \exists y \,
\left\{\begin{array}{l}
q \re {a:y} q' \tin \A,\;\; \tand \\[2mm]
(\lambda_1,\dots,\lambda_{d+1}) \re {y} (\lambda'_1,\dots,\lambda_{d+1}) \tin \UPar.
\end{array}\right.
\]

Paths in $\UAut$ are well-behaved with respect to $W$, as stated below.

Let $(q,\lambda_1,\dots,\lambda_{d+1}) \lrp{w\phantom{..}}$ be an infinite path in $\UAut$. Then, $w \in q^{-1}W$.

Consider a path

\[
(q^0,\lambda_1^0,\dots,\lambda_{d+1}^0) \re {w_0} (q^1,\lambda_1^1,\dots,\lambda_{d+1}^1) \re {w_1} \dots \tin \UAut.
\]

By definition, there are priorities $y_0,y_1,\dots$ such that

\[
q^0 \re {w_0:y_0} q^1 \re{w_1:y_1} \dots \tin \A, \; \tand \;\; (\lambda_1^0,\dots,\lambda_{d+1}^0) \re {y_0} (\lambda_1^1,\dots,\lambda_{d+1}^1) \re {y_1} \dots \tin \UPar.
\]

Since vertices in $\UPar$ satisfy the parity objective, $\liminf(y_0y_1\dots)$ is even, thus the above run in $\A$ is accepting, and so $w_0 w_1 \dots \in (q^0)^{-1}W$.

"Monotonicity@@@univ" of $\UAut$ follows from the structural assumptions over $\A$.

The graph $\UAut$ is "monotone@@univ".

\[
(q,\lambda_1,\dots,\lambda_{d+1}) \re {a} (q',\lambda'_1,\dots,\lambda'_{d+1}) > (q'',\lambda''_1,\dots,\lambda''_{d+1}) \tin \UAut.
\]

We aim to prove that $(q,\lambda_1,\dots,\lambda_{d+1}) \re {a} (q'',\lambda''_1,\dots,\lambda''_{d+1}) \tin \UAut$.
By definition of the transitions of $\UAut$, there is a priority $y$ such that $q \re{a:y} q' \tin \A$ and $(\lambda_0,\dots,\lambda_{d+1}) \re{y} (\lambda'_0, \dots, \lambda'_{d+1}) \tin \UPar$.
We remark that, by definition of the order in $\UAut$, we have that $(\classHM{0}{q''},\lambda''_1,\dots,\lambda''_{y-1},\classHM{y}{q''}) \leq (\classHM{0}{q'},\lambda'_1,\dots,\lambda'_{y-1},\classHM{y}{q'})$ (for $y$ even, similar if $y$ odd).
We distinguish four cases:

* If $y$ is even and $(\classHM{0}{q'},\lambda'_1,\dots,\lambda'_{y-1},\classHM{y}{q'}) = (\classHM{0}{q''},\lambda''_1,\dots,\lambda''_{y-1},\classHM{y}{q''})$.
Then in $\A$, $q \re {a:y} q' \re{\ee:y+1} q''$ thus $q \re{a:y} q''$, and in $\UAut$, $(\lambda_1,\dots,\lambda_{y-1}) \geq (\lambda'_1,\dots,\lambda'_{y-1}) = (\lambda''_1,\dots,\lambda''_{y-1})$, which concludes.

* If $y$ is odd and $(\classHM{0}{q'},\lambda'_1,\dots,\classHM{y-1}{q'},\lambda'_y) =(\classHM{0}{q''},\lambda''_1,\dots,\classHM{y-1}{q''},\lambda''_y)$.
Then, in $\A$, $q \re{a:y} q' \re{\ee:y} q''$ thus $q \re{a:y} q''$, and in $\UAut$, $(\lambda_1,\dots,\lambda_{y})>(\lambda'_1,\dots,\lambda'_y) = (\lambda''_1,\dots,\lambda''_y)$ which concludes.

* If for some even $x\leq y$ it holds that $(\classHM{0}{q'},\lambda'_1, \classHM{2}{q'}, \dots,\lambda'_{x-1})=(\classHM{0}{q''},\lambda''_1, \classHM{2}{q'}, \dots,\lambda''_{x-1})$ and $\classHM{x}{q''} < \classHM{x}{q'}$.
Then in $\A$, $q \re{a:y} q' \re{\ee:x} q''$ thus $q \re{a:x} q''$ and in $\UAut$, $(\lambda_1,\dots,\lambda_{x-1}) \geq (\lambda'_1,\dots,\lambda'_{x-1}) = (\lambda''_1,\dots,\lambda''_{x-1})$ thus $(\lambda_1,\dots,\lambda_{d+1}) \re x (\lambda''_1,\dots,\lambda''_{d+1})$ which concludes.

* If for some even $x< y$ it holds that $(\classHM{0}{q'},\lambda'_1,\dots,\classHM{x}{q'})=(\classHM{0}{q''},\lambda''_1,\dots,\classHM{x}{q''})$ and $\lambda'_{x+1} > \lambda''_{x+1}$.
Then, in $\A$, $q \re{a:y} q' \re{\ee:x+1} q''$ thus $q \re{a:x+1} q''$ and in $\UAut$, $(\lambda_1,\dots,\lambda_{x+1}) \geq (\lambda'_1,\dots,\lambda'_{x+1}) > (\lambda''_1,\dots,\lambda''_{x+1})$ thus $(\lambda_1,\dots,\lambda_{d+1}) \re{x+1} (\lambda''_1,\dots,\lambda''_{d+1})$ which concludes.

The other implication $v > v' \re a v'' \implies v \re a v''$ in $\UAut$ follows exactly the same lines.

*Universality of $\UAut$

To prove Proposition <ref>, there remains to establish "universality" of $\UAut$, which follows easily from "history-determinism" of $\A$ and "universality" of $\UPar$.

The graph $\UTop{\UAut}$ is "$(\kappa,W)$-universal".

We show "universality for trees" of $\UAut$ and conclude by Lemma <ref>.
Let $T$ be a "$\SS$-tree" of size $<\kappa$ that "satisfies@@univTree" $W$.
Let $\resolv$ be a "sound resolver" for $\A$. We define in a top-down fashion a labelling $\resolv_T :T \to Q$ such that, if $w_1w_2\dots w_k$ is the labelling of the path from the "root@@univ" to a vertex $t$, then $\resolv_T(t)$ is the target state of the "run induced by@@aut" $\resolv$ in $\A$.
In particular, $t \re{a} t' \tin T$ implies that $\resolv_T(t) \re {a:x} \resolv_T(t') \tin \A$ for some priority $x$, and, on each infinite branch $t_0 \re{a_0} t_1 \re{a_1} \dots$, the "run" $\resolv_T(t_0) \re{a_0:x_0} \resolv_T(t_1) \re{a_1:x_1} \dots$ is "accepting@@run" in $\A$.
Stated differently, the "$[0,d+1]$-tree" $\intro*\TPar$ obtained from $T$ by replacing each edge $t \re a t'$ with the corresponding edge $t \re x t'$ such that $\resolv_T(t) \re{a:x} \resolv_T(t')$, "satisfies@@univ" the "parity objective".

By "$(\kappa,\parity)$-universality" of $\UPar$,  there exists a "morphism@@univ" $\intro*\phiPar : \TPar \to \UPar$.
As $\TPar$ has the same set of vertices than $T$, $\phiPar$ defines a mapping from $T$ to $\UPar$.
We consider the product mapping $\phi=\resolv_T \times \phiPar\colon T \to \UAut$ that sends $t\mapsto (\resolv_T(t),\phiPar(t))$.
It defines a "morphism@@univ", as for any edge $t \re a t'$ in $T$ it holds that, for some $x$, $\resolv_T(t) \re {a:x} \resolv_T(t') \tin \A$ and $\phiPar(t) \re{x} \phiPar(t') \tin \UAut$.

This completes the proofs of the  implications <ref> $\implies$ <ref> $\implies$ <ref> from Theorem <ref>, providing a characterisation of "half-positionality" for $\oo$-regular languages.

§ TWO DECISION PROCEDURES

We now establish decidability of "half-positionality" of "$\oo$-regular languages" in polynomial time, stated as Theorem <ref>.
We propose two decision procedures.

The first one follows our proof of Theorem <ref> and attempts to build a "deterministic" "signature" automaton from a given deterministic parity automaton.
We believe that the techniques used in such a procedure may prove interesting also in other contexts (see conclusion in Section <ref>).

The second procedure is simpler to describe: we give a direct proof that any (non-deterministic) automata recognising a half-positional language is "$\ee$-completable".
However, the proof itself relies on Theorem <ref>, and more specifically its consequence Theorem <ref> about the closure under union.

§.§ Procedure 1: Recursive decomposition

The first decision procedure we present consists in, given a "deterministic" "parity automaton" $\A$, applying the construction from Section <ref> to decide whether $W=\L(\A)$ is half-positional.
The general idea is simply to go through that construction, either ending up with a failure indicating that $W$ is not positional, or with a "deterministic" "structured signature automaton".
If such an automaton is successfully obtained, it suffices to check "full progress consistency", which can be done in polynomial time, as explained below.

*Complexity of building a signature automata

Most proofs have been already given in Section <ref>; we also require the following easy lemma.

Let $\A$ be a "parity automaton" and $x$ a priority. Assume that $\A$ is "deterministic over" ${\geq}x$-transitions. Given two states $q, p$ in $\A$, we can decide in polynomial time whether $\safeSig{x}{q}\subseteq \safeSig{x}{p}$.

We now detail the polynomial-time procedure.
Let $\A$ be a "deterministic" "parity automaton" "recognising" $W$.

* First, we check for each pair of states $q,p$ whether $\Lang{\initialAut{\A}{q}}\subseteq \Lang{\initialAut{\A}{p}}$, or $\Lang{\initialAut{\A}{p}}\subseteq \Lang{\initialAut{\A}{q}}$. If for some pair of states these languages are incomparable, then "residuals" of $W$ are not totally ordered, and we can conclude that $W$ is not "half-positional".

Suppose that we have defined total preorders up to $\leqSig{x-2}$ making $\A$ a "$(x-2)$-structured signature" automaton.

* We "${<}x$-safe centralise" $\A$, which can be done in polynomial time by Lemma <ref>.
The obtained automaton is "deterministic over" ${\geq}x$-transitions.

* We compute the "${<}x$-safe components" of $\A$, which can be done by doing a decomposition in "SCCs" of $\autGeq{\A}{x}$.
We check whether, for each "${<}x$-safe component" $S$ and state $q$, the states in $S\cap \classSig{x-2}{q}$ are "totally preordered" by inclusion of "${<}x$-safe languages", which can be done in polynomial time by Lemma <ref>.
If this is not the case, we conclude that $W$ is not "half-positional".

* We remove the non-determinism from $\A$ – in polynomial time and without increasing the number of states – by applying Lemma <ref>.

* We compute (in polynomial time) the automaton $\A'$ given by Lemma <ref> (see last subsection of Appendix <ref> for details).
We check whether $\Lang{\A'}=W$, which can be done in polynomial time (testing equivalence of "deterministic" "parity automata" <cit.>).
If this is not the case, we conclude that $W$ is not "half-positional".

After these operations, if we have not yet found that $W$ is not "half-positional", we obtain an "equivalent@@aut" "deterministic" automaton $\A'$ that is either "$x$-structured signature", or strictly smaller than $\A$.[As mentioned before, we conjecture that the obtained automaton $\A'$ is always "$x$-structured signature".] In the former case, we continue defining preorders $\leqSig{x+1}$ and $\leqSig{x+2}$; in the latter, we restart from the beginning.
In total, we repeat at most $d\cdot|Q|$ times a sequence of operations that take polynomial time.

*Checking full progress consistency

Assume that we have a "deterministic" "structured signature automaton" "recognising" $\A$. We cannot yet conclude that $W$ is "half-positional", as we do not know whether $\A$ is "fully progress consistent", however, by Lemma <ref>, if $W$ is "half-positional" this must be the case. By Theorem <ref>, this condition is also sufficient.
We show now that we can check "full progress consistency" of $\A$ in polynomial time, finishing the proof of Theorem <ref>. For this, we generalise the method from <cit.>.

Let $\A$ be a deterministic "structured signature automaton". We can decide in polynomial time whether $\A$ is "fully progress consistent".

The proof crucially relies on the following lemma.

A "deterministic" "structured signature automaton" $\A$ is "fully progress consistent" if and only if, for each even priority $x$ and each pair of states $q, p$ in $\A$ such that $q\lSig{x}p$ we have:

\[  q\lrp{w:\geq x} p \; \tand \; p\lrp{w:y} p \; \implies \; y \text{ is even}. \tag{1} \label{eq:1}\]

It follows directly from the definition that a "deterministic" "fully progress consistent" automaton satisfies this property.
To show the converse, assume that (<ref>) holds; we aim to prove "full progress consistency".
Consider an even priority $x$ and a word $w\in \SS^*$ such that $q\lSig{x}p$ and $q\lrp{w:\geq x}p$, we should prove $w^\oo \in \Lang{\initialAut{\A}{q}}$.
We take $x$ to be minimal such that $q \lSig{x} p$, and thus we have $q \eqSig{x-2} p$.
For $x=0$, the proof is identical to the one appearing in Lemma <ref>, we assume that $x\geq 2$.
Therefore, there is a "${<}x$-safe path" connecting $q$ and $p$, so we have $q\eqSig{x-1}p$ (Item <ref> from the definition of "structured signature automaton"), thus since $q \lSig{x} p$ we get $\safeSig{x}{q}\subseteq \safeSig{x}{p}$ (Item <ref>).
Consider the "run over $w^\oo$" from $q$ in $\A$:

\[ \rr = q\lrp{w:\geq x} p \lrp{w: y_1} p_2 \lrp{w: y_2} p_3 \lrp{w: y_3} \cdots .\]

Since $w \in \safeSig{x}{p}$ and $q \lSig{x} p$, Lemma <ref> yields $\safeSig{x}{p} \subseteq \safeSig{x}{p_2}$, and hence $y_1 \geq x$.
Since $\eqSig{x-2}$ is "$[0,x-2]$-faithful" and $q \lrp{w:\geq x-2} p \eqSig{x-2} q$, it follows that $p_2 \eqSig{x-2} p$.
Then it follows from $p \lrp{w:\geq x} p_2$ that $p \eqSig{x-1} p_2$, and thus $p \leqSig{x} p_2$.
Applying the same reasoning by induction yields $y_i \geq x$ and $p \leqSig{x} p_i$ for all $i$, and thus $q \lSig{x} p_i$

Eventually, $\rr$ closes a cycle: there are $N$ and $k$ such that, for every $i\geq N$, $p_i = p_{i+k}$.
We let $p' = p_{kN}$ and let $y$ denote the minimal priority produced by the cycle.
Then it holds that:

\[ q\lSig{x} p ', \;\; q\lrp{w^{kN}:\geq x} p',  \; \tand \; p' \lrp{w^{kN}:y} p'. \]

Thus thanks to (<ref>), $y$ is even, and so $w^\oo = (w^{kN})^\oo \in \Lang{\initialAut{\A}{q}}$.

We can now deduce Lemma <ref>.

For each pair of states $q,p\in Q$ and each priority $x$, we define the languages of finite words

\[ L_{q\re{}p}^x = \{w\in \SS^* \mid q\lrp{w:x} p \tin \A  \}, \quad \tand \quad    L_{q\re{}p}^{\geq x} = \{w\in \SS^* \mid q\lrp{w: \geq x} p \tin \A\}. \]

By Lemma <ref>, $\A$ is "fully progress consistent" if and only if, for each even priority $x\in [0,d]$ and each pair of states $q,p\in Q$ such that $q\lSig{x}p$:

\[  L_{q\re{}p}^{\geq x} \; \bigcap \; \big(\bigcup_{y \text{ odd}} L_{p\re{}p}^y \big) = \emptyset.  \]

We show that for all pair of states, languages $L_{q\re{}p}^{\geq x}$ and $L_{q\re{}p}^x$ are regular and we can obtain deterministic finite automata for them in polynomial time.
This implies that we can check the emptiness of intersections above in polynomial time, concluding the proof.

For $L_{q\re{}p}^{\geq x}$ the previous claim is clear: the finite automaton obtained by taking the "automaton structure" of $\autGeq{\A}{x}$ and taking $q$ and $p$ as initial and final states, respectively, is a finite automaton recognising $L_{q\re{}p}^{\geq x}$.

For $L_{q\re{}p}^{x}$, we consider the automaton over finite words that has as states $(Q\times [0,d])\cup \{(q,\init)\}$, and $(q,\init)$ and $(p,x)$ as initial and final states, respectively.
Transitions of the automaton are of the form $(q_1,x_1)\re{a}(q_2,x_2)$ if the transition $q_1\re{a:y}q_2$ in $\A$ is such that $x_2 = \min\{x_1, y\}$.
In words, this automaton keeps track of the run in $\A$ from $q$ and of the minimal priority produced in the way. It accepts a word if it arrives to $p$ while producing as minimal priority $x$, as we wanted.

§.§ Procedure 2: $\ee$-completion

We now prove the following result.

Let $\A$ be a "non-deterministic" "parity automaton" recognising a "half-positional" language $W$.
Then for each pair of states $q,q'\in Q$, and for each even priority $x$, one may add (at least) one of the transitions

\[
q \re{\ee:x} q' \qquad \tor \qquad q' \re{\ee:x+1} q
\]

without augmenting the language of $\A$.

Before proving Theorem <ref>, we argue that decidability of "half-positionality" in polynomial time (Theorem <ref>) follows.
Let $\A_0$ be a "deterministic" "parity automaton" recognising a language $W$ and using $d$ as maximal "priority" (assumed even).
We build an "$\ee$-completion" of $\A_0$ as follows.
At each step, pick a pair of states $(q,q')$ such that neither $q \re{\ee:x} q'$ nor $q' \re{\ee:x+1} q$ belongs to the current automaton, for $x\leq d$ even.
Then try to add one of these transitions, and see if the language increases (checking whether $\Lang \A \subseteq W$ can be done in polynomial time since $W$ is "recognised" by the "deterministic" automaton $\A_0$ <cit.>).
If the language does not increase for one of the two transitions, then proceed to the next step; otherwise conclude that $W$ is not "half-positional" thanks to Theorem <ref>.

After polynomially-many steps, we obtain an automaton such that for each pair of states $(q,q')$ and for each even $x$, either $q \re{\ee:x} q'$ or $q' \re{\ee:x+1} q$.
Now for each priority $y$, close the relations $\re{\ee:y}$ by transitivity, which does not augment the language.
Moreover, for priorities $y \cleq y'$ (recall that $1 \cleq 3 \cleq \dots \cleq d+1 \cleq d \cleq \dots \cleq 2 \cleq 0$) add transition $q \re{\ee:y} q'$ whenever $\A$ contains $q \re{\ee:y'} q'$; this also does not augment the language.
Then it holds that the relations $\re{\ee:1},\re{\ee:3},\dots,\re{\ee:d+1}$ are "total preorders" "refining" one another, and that for each even $x$, $\re{\ee:x}$ is the strict variant of $\re{\ee:x+1}$.
Stated differently, the obtained automaton $\A$ is an "$\ee$-completion" of $\A_0$, which implies that $W$ is "half-positional" thanks to Theorem <ref>.

Note that on the way, we obtain the following result as an interesting consequence.

Any "non-deterministic" "parity automaton" "recognising" a "half-positional" language is "$\ee$-completable".

We now prove Theorem <ref>.
The proof is inspired by that of <cit.>, but it is more involved, because we now deal with "parity automata" rather than graphs (or safety automata).
This difficulty is overcome thanks to Theorem <ref>.

Fix a pair of states $q,q' \in Q$ and an even "priority" $x$.
Consider the "game" $\G$ defined as follows (see also Figure <ref> below).

* The alphabet is $C=(\Sigma\cup\{\ee\}) \times \{0,1,\dots,d+1\} \times \{\ent,\sma,\neut\}$.
Therefore, each edge has a letter in $\Sigma\cup \{\ee\}$, a priority in $\{0,1,\dots,d+1\}$, and a type in $\{\ent,\sma,\neut\}$.
For a word $w \in C^\omega$, we write $w_\Sigma,w_\prio$ and $w_\type$ for the respective projections.
For conciseness, we generally omit the type and write edges in the game as $\re{a:y}$, just like in the automaton.

* The set of vertices consists in two copies of $\A$ indexed by $q$ and $q'$, together with an additional vertex $q_?$.
Formally, $V=Q \times \{q,q'\} \cup \{q_?\}$.
All vertices belong to "Adam" except for $q_?$ which belongs to "Eve".

* The edges in the copy indexed by $q$ (resp. $q'$) follow exactly the transitions in $\A$, except those leading to $q'$ (resp. $q$), which are instead redirected to $q_?$ (but keep the same letter and priority).

* The vertex $q_?$ has exactly two outgoing edges: $q_? \re{\ee:x+1} (q,q)$ and $q_? \re{\ee:x} (q',q')$.

* The edge $q_? \re{\ee:x+1} (q,q)$ has type $\ent$, and edges with priority $\leq x$ inside the copy indexed by $q$ have type $\sma$. All other edges are neutral.

* The objective is

\[
W_\G = W_\SS \cup \oddparity \cup \gtype,
\]

where $W_\SS$ is the set of words $w$ such that $w_\Sigma \in W$, $\oddparity$ is the set of words whose minimal priority appearing infinitely often is odd, and $\gtype$ is the set of words with infinitely many occurrences of type $\ent$ and finitely many occurrences of type $\sma$.

The "game" $\G$. Edges which are crossed out are those that are redirected (while keeping the same label). Note that $(q',q)$ and $(q,q')$ are not reachable; these vertices could be removed from the game.

Clearly $W_\SS$ is "half-positional" and so is $\oddparity$; likewise, $\gtype$ rewrites as a "parity condition" (by mapping $\sma$ to 1, $\ent$ to 2 and $\neut$ to 3), and thus it is also "half-positional".
Moreover, $\oddparity$ and $\gtype$ are "prefix-independent". It follows from Theorem <ref> that $W'$ is positional.

"Eve" wins from $(q_\init,q)$ and from $(q_\init,q')$ in $\G$.

Consider the "strategy" which, whenever reaching $q_?$ from an edge of the form $(p,q') \re{} q_?$, reads the edge $q_? \re{\ee:x+1} (q,q)$ and whenever reaching $q_?$ from an edge of the form $(p,q) \re q_?$, reads the edge $q_? \re{\ee:x} (q',q')$.
Take an infinite path $\pi_\G$ in $\G$ from $(q_\init,q)$ which is "consistent with@@strat" the above strategy.
It is of the form

\[
\pi_\G : (q_\init,q) \rp{w_0:y_0} (p_0,q) \re{a_0:z_0} q_? \re{\ee:x} (q',q') \rp{w_1:y_1} (p_1,q') \re{a_1:z_1} q_? \re{\ee:x+1} (q,q) \rp{w_2:y_2} \dots,
\]

where $w_0,p_0,a_0,w_1,p_1,a_1,\dots$ is either infinite (and the $w_i$'s are finite) or it ends with some $w_i$ which is infinite.
We aim to prove that $\pi_\G$ is "winning@@play", that is, its label belongs to $W_\G$.

Observe that

\[
\pi_\A : q_\init \rp{w_0:y_0} p_0 \re{a_0:z_0} q' \rp{w_1:y_1} p_1 \re{a_1:z_1} q \rp{w_2:z_2} \dots
\]

defines a path in $\A$.
If $\pi_\A$ satisfies $W$, then $\pi_\G$ satisfies $W_\SS$ (since we only add some occurrences of $\ee$ to the projections on $\Sigma \cup \{\ee\}$).
Thus we assume that $\pi_\A$ does not satisfy $W$, which means that the "run" in the automaton is "rejecting@@run".
If $\pi_\G$ satisfies $\gtype$ then it is "winning@@play", so we assume otherwise: there are either finitely many occurrences of $\ent$ or infinitely many occurrences of $\sma$.

* If there are finitely many occurrences of $\ent$ in $\pi_\G$, then the "priorities" in $\pi_\G$ eventually coincide with those in $\pi_\A$, and since this is a "rejecting run" in $\A$, $\pi_\G$ satisfies $\oddparity$.

* If there are infinitely many occurrences of $\sma$, then the minimal "priority" appearing infinitely often in $\pi_\A$ is $\leq x$, therefore adding (even infinitely many) priorities $x$ and $x+1$ does not change the fact that the run is rejecting.
Therefore $\pi_\G$ satisfies $\oddparity$.

Since "Eve" wins and $W_\G$ is "half-positional", she has a "winning@@strat" "positional strategy" $\sigma$.

If $\sigma(q_?) = q_? \re{\ee:x} q'$, then adding the transition $q \re{\ee:x} q'$ to $\A$ does not augment the language.

Let $\A'$ be the automaton obtained by adding to $\A$ the transition $q \re{\ee:x} q'$.
Consider an "accepting run" $\pi_{\A'}$ from $q_\init$ in $\A'$.
Decompose it around the occurrences of $q \re {\ee:x} q'$ as follows:

\[
\pi_{\A'} : q_\init \rp{w_0:y_0} p_0 \re{a_0:z_0} q \re{\ee:x} q' \rp{w_1:y_1} p_1 \re{a_1:z_1} q \re{\ee:x} q' \rp{w_2:y_2} \dots,
\]

where the sequence $w_0,p_0,a_0,w_1,p_1,a_1,\dots$ is either infinite (and the $w_i$ are finite), or it is finite and ends with some $w_i$ which is infinite.

\[
\pi_{\G} : (q_\init,q') \rp{w_0:y_0} (p_0,q') \re{a_0:z_0} q_? \re{\ee:x} (q',q') \rp{w_1:y_1} p_1 \re{a_1:z_1} q_? \re{\ee:x} (q',q') \rp{w_2:y_2} \dots
\]

defines a path in $\G$ which is consistent with $\sigma$.
Therefore the label of $\pi_\G$ satisfies $W_\G$.
Note that "priorities" in $\pi_{\A'}$ and $\pi_\G$ are the same, and $\pi_{\A'}$ is accepting, therefore $\pi_\G$ does not satisfy $\oddparity$.
Moreover, $\pi_\G$ has no occurrence of $\ent$, thus it does not satisfy $\gtype$.
We conclude that $\pi_\G$ satisfies $W_\SS$, and thus $w_0a_0w_1a_1 \dots \in W$, so $\Lang {\A'} \subseteq W$.

The proof of the other case is similar to the previous one, with a slight difference in the analysis.

If $\sigma(q_?) = q_? \re{\ee:x+1} q$, then adding the transition $q' \re{\ee:x+1} q$ to $\A$ does not augment the language.

Let $\A'$ be the automaton obtained by adding to $\A$ the transition $q' \re{\ee:x+1} q$.
Consider an "accepting run" $\pi_{\A'}$ from $q_\init$ in $\A'$.
Decompose it around the occurrences of $q' \re {\ee:x+1} q$ as follows:

\[
\pi_{\A'} : q_\init \rp{w_0:y_0} p_0 \re{a_0:z_0} q' \re{\ee:x+1} q \rp{w_1:y_1} p_1 \re{a_1:z_1} q' \re{\ee:x+1} q \rp{w_2:y_2} \dots,
\]

where the sequence $w_0,p_0,a_0,w_1,p_1,a_1,\dots$ is either infinite (and the $w_i$ are finite), or it is finite and ends with some $w_i$ which is infinite.

\[
\pi_{\G} : (q_\init,q) \rp{w_0:y_0} (p_0,q) \re{a_0:z_0} q_? \re{\ee:x+1} (q,q) \rp{w_1:y_1} p_1 \re{a_1:z_1} q_? \re{\ee:x+1} (q,q) \rp{w_2,y_2} \dots
\]

defines a path in $\G$ which is consistent with $\sigma$.
Therefore the label of $\pi_\G$ satisfies $W_\G$.
Note that "priorities" in $\pi_{\A'}$ and $\pi_\G$ are the same, and $\pi_{\A'}$ is "accepting@@run", therefore $\pi_\G$ does not satisfy $\oddparity$.

Now note that $\pi_{\A'}$ has infinitely many occurrences of priority $x+1$ and yet it is "accepting@@run", therefore it has infinitely many occurrences of priorities $\leq x$.
Thus $\pi_\G$ has infinitely many occurrences of $\sma$, so it does not satisfy $\gtype$.
We conclude that $\pi_\G$ satisfies $W_\SS$, and therefore the label $w_0a_0w_1a_1\dots$ of $\pi_{\A'}$ belongs to $W$.

This concludes the proof.

It is interesting to remark that our proof relies on the fact that for any "$\omega$-regular" "half-positional" "objective" $W$, the "objective" $W \cup \parity$ is "half-positional".
We do not know a direct proof of this fact (without using Theorem <ref> which relies on the machinery employed to prove Theorem <ref>).
Such a direct proof would give, together with Theorem <ref>, an easier path to the main characterisation and the polynomial time decidability (though it would fall short of establishing the 1-to-2-player lift and the finite-to-infinite lift).

§ BIPOSITIONALITY OF ALL OBJECTIVES

In this section we provide a characterisation of all "bipositional" objectives, without "$\oo$-regularity" or "prefix-independence" assumptions.
This characterisation extends the result of Colcombet and Niwiński <cit.>, who showed that the only "prefix-independent" "bipositional" objective (over all game graphs) is the "parity objective".
Recently, Bouyer, Randour and Vandenhove <cit.> generalised that result in an orthogonal direction: they proved that the only objectives for which both players can "play optimally using" finite chromatic memory are "$\oo$-regular objectives".

§.§ Characterisation of bipositionality and consequences

We say that an objective $W\subseteq \SS^\oo$ is ""bi-progress consistent"" if both $W$ and its complement are "progress consistent", that is, if it satisfies that for all "residual class" $\resClass{u}$ and finite word $w\in \SS^*$:

* $\resClass{u} \lRes \resClass{uw} \implies uw^\oo \in W$, and

* $\resClass{uw} \lRes \resClass{u} \implies uw^\oo \notin W$.

An objective $W\subseteq \SS^\oo$ is "bipositional" (over all games) if and only if:

* $W$ has a finite number of "residuals", totally ordered by inclusion, and

* $W$ is "bi-progress consistent", and

* $W$ can be "recognised" by a "parity automaton on top of" the "automaton of residuals".

This characterisation only holds for infinite games, as there are non "$\oo$-regular" "objectives" that are "bipositional" over finite games, as, for example, energy objectives <cit.> and their generalisation <cit.>. However, we deduce from Theorem <ref> that in the case of "$\oo$-regular" objectives these conditions do also characterise "bipositionality" over finite games.

An "$\oo$-regular" objective $W\subseteq \SS^\oo$ is "bipositional" over finite games if and only if it satisfies the three conditions from Theorem <ref>.

*Consequences: Lifts and decidability
For "$\oo$-regular objectives", we can directly lift the corollaries of Theorem <ref> obtained for "half-positionality" to "bipositionality". For non-$\oo$-regular ones, the finite-to-infinite lift does not hold, as commented above. On the other hand, a combination with a recent result from Bouyer, Randour and Vandenhove <cit.> implies that the 1-to-2-player lift holds for any objective.

We say that an objective $W\subseteq \SS^\oo$ is ""bipositional over (finite) one-player games"" if $W$ is "half-positional" over (finite) "Eve-games" and its complement $\SS^\oo\setminus W$ is "half-positional" over (finite) "Adam-games".

An objective $W\subseteq \SS^\oo$ is "bipositional" (over all games) if and only if it is "bipositional over one-player games".

An "$\oo$-regular" objective $W\subseteq \SS^\oo$ is "bipositional" (over all games) if and only if it is "bipositional over finite one-player games".

We obtain decidability for "bipositionality" in polynomial time from its counterpart in the case of "half-positionality" (Theorem <ref>). We observe that Theorem <ref> provides an alternative way to check "bipositionality".

Given a "deterministic" "parity automaton" $\A$, we can decide in polynomial time whether $\Lang{\A}$ is "bipositional".

*An example
[Parity over occurrences]
We let $\SS = [0,d]$ and let $\intro*\WOccParity$ be the language of words such that the minimal "priority" appearing on them is even:

\[ \WOccParity = \{w\in [0,d]^\oo \mid \min (w) \text{ is even}\}. \]

An automaton "recognising" $W$ is depicted in Figure <ref>. It has one state per "residual", which are totally ordered, and it is immediate to check that it is "bi-progress consistent". Therefore, $\WOccParity$ is a "bipositional" objective.

Automaton "recognising" $\WOccParity$, for $d=4$. The initial state is $q_4$.  This automaton is in fact what is sometimes called a weak automaton: runs that finally end in an even state are "accepting@@run", and those ending in an odd state are "rejecting@@run".

Some more complex examples can be generated by, for example, adding some output priorities to the automaton above without breaking the "bi-progress consistency" condition. However, the combination of being recognisable by the "automaton of residuals" with "bi-progress consistency" greatly restricts the possibilities of generating examples of "bipositional" languages. We wonder whether a more precise characterisation of languages satisfying these three properties can be obtained.

§.§ Proof of the characterisation

*Necessity of the conditions

The necessity of the total order over the residuals of $W$ is given by Lemma <ref>, and the necessity of "bi-progress consistency" is given by Lemma <ref>.
The following lemma provides the necessity of the last condition of Theorem <ref>.
It can be obtained by instantiating the first item of <cit.> for the case of "bipositional" objectives.

If $W\subseteq \SS^\oo$ is "bipositional over one-player games", then $W$ is "$\oo$-regular" and can be "recognised" by a "parity automaton" on top of the "automaton of residuals".

*Sufficiency of the conditions

The sufficiency of conditions of Theorem <ref> can be shown by providing "well-ordered@@univ" "monotone@@univ" "universal" graphs for $W$ and its complement.
An even simpler option – now that we have already done such construction for "half-positional" objectives – is to provide "fully progress consistent" "signature automata" recognising these languages, and then use the characterisation of "half-positionality" given by Item <ref> from Theorem <ref>.

We show that the "parity automaton on top" of the "automaton of residuals" is a "fully progress consistent" "signature automata". Since by hypothesis $\ResW$ is totally ordered, the order $\leqSig{0}$ given by inclusion of "residuals" satisfies the first requirement of the definition of "signature automaton". As the "residual classes" of this automaton are trivial, we can define all relations $\eqSig{x}$ to be trivial too, so this automaton satisfies all the requirements to be a "signature automaton".
Moreover, as $W$ is "progress consistent" and the $\eqSig{x}$-classes of the automaton are trivial, it is also "fully progress consistent".
The argument is symmetric for $\SS^\oo\setminus W$.

§ HALF-POSITIONALITY OF CLOSED AND OPEN OBJECTIVES

§.§ Closed objectives

We recall that an objective $W$ is "closed" if

\[ W =\Safe{L} = \{w \mid w \text{ does not contain any prefix in } L\}, \]

for some language of finite words $L$.
Half-positional "closed objectives" were first characterised by Colcombet, Fijalkow and Horn <cit.>, as those that have a totally ordered set of residuals.
However, as they already remarked, this characterisation only holds for finite branching "game graphs".

We now give a characterisation of half-positionality over all game graphs for "closed objectives".
Namely, a "closed objective" $W$ is "half-positional" if and only if $\ResW$ is well-ordered by inclusion (Theorem <ref>) (in fact, the well-foundedness of $\ResW$ is a necessary condition for finite memory determinacy of any objective.)

This (and its generalisation to memory) was already observed in <cit.>.

§.§.§ Well-foundedness of residuals

Next example, taken from <cit.>,  shows that total order over residuals does not suffice to ensure "half-positionality" of arbitrary "closed objectives".

[Outbidding game <cit.>: Total order does not suffice]
Let $\SS = \{a,b,c\}$ and $L$ be the language of finite words:

\[ L = \{ w\in \SS^* \mid \text{ for some } u\in \SS^* \text{ with } \countLetters{u}{a}\leq \countLetters{u}{b}, uc \text{ is a prefix of } w \},\]

where $\intro*\countLetters{u}{x}$ is the number of occurrences of $a$ in $u$.
We consider the "closed objective" $W = \Safe{L}$.
The "residuals" of $W$ are totally ordered by inclusion:

\[ \emptyset=\lquotW{c} < \dots < \lquotW{(a^n)} <\cdots <  \lquotW{a} <  \lquotW{\ee} <  \lquotW{b} < \cdots  .\]

However, $W$ is not "half-positional", as witnessed by the game in Figure <ref>.

Outbidding game. First, a sequence $a^n$ is produced, for some $n\in \NN$. In order to win, "Eve" needs to answer with $b^m$, with $m>n$. Therefore, she can win from any vertex in the game, but no "positional strategy" guarantees the victory from all states.

Let $W\subseteq \SS^\oo$ be an "objective" that is "half-positional" over "$\ee$-free" "Eve-games". Then, $\ResW$ is well-ordered by inclusion.

We have already seen (Lemma <ref>), that if $W$ is "half-positional", then $\ResW$ is totally ordered. We need to prove that $\ResW$ is well-founded.

Let $W\subseteq \SS^\oo$ be an "objective" such that "Eve" can "play optimally using positional strategies" (or using finite memory strategies) over "$\ee$-free" "Eve-games". Then, $\ResW$ is well-founded (for the order given by inclusion of "residuals").

Suppose by contradiction that there is an infinite strictly decreasing sequence of "residuals":

\[ \lquotW{u_1} \supsetneq \lquotW{u_2} \supsetneq  \cdots , \; u_i\in \SS^*.\]

(We suppose without loss of generality that $\ee\neq u_i$ for all $i$.)
Let $w_i\in \SS^\oo$ such that $w_i\in \lquotW{u_i} \setminus \lquotW{u_{i+1}}$.
We consider the game – similar to the outbidding game from Figure <ref> – in which a word $u_i$ labels a path from a vertex $v_i$ to $v_{\mathsf{choice}}$, for each $i$. From this latter vertex, "Eve" can choose a between paths labelled by $\{w_i\mid i\in \NN\}$.
"Eve" can win be answering $w_i$ to $u_i$. However, any "positional@@strat" (or finite memory) strategy will only consider a finite number of responses $w_{j_1},\dots,w_{j_n}$. Therefore, such a strategy is "losing@@strat" from $v_K$ for $K> \max \{j_t \mid 1\leq t\leq n\}$.

§.§.§ Characterisation for closed objectives

Let $W\subseteq \SS^\oo$ be a "closed objective". Then, $W$ is "half-positional" (over all "game graphs") if and only if $\ResW$ is well-ordered by inclusion.

We have already shown that this condition is necessary. To prove sufficiency, we give, for each cardinal $\kk$, a "$(\kk,W)$-universal" "well-ordered@@univ" "monotone@@univ" graph. We conclude by Proposition <ref>.

Let $U$ be the "$\SS$-graph" that has as vertices $\ResW\setminus \{\emptyset\}$, ordered by inclusion. By hypothesis, this is a well-order. For each $a\in \SS$, we let

\[ \lquotW{u} \re{a} \lquotW{u'} \;\; \text{ iff } \; \; \lquotW{u'}\leq \lquotW{(ua)}. \]

We note that if $ua$ is already losing ($\lquotW{ua} =\emptyset$), then transition $\lquotW{u} \re{a} \lquotW{u'}$ does not appear in $U$.
By Lemma <ref>, graph $U$ is "monotone@@univ".
The hypothesis of "closeness@@obj" of $W$ is fundamentally used in next claim.

A vertex $\lquotW{u}$ of $U$ "satisfies@@univ" $W$ if and only if $\lquotW{u} \subseteq \lquotW{\ee}=W$.

Let $L\subseteq \SS^*$ such that $W = \Safe{L}$. Let
$\lquotW{u_1} \re{a_1} \lquotW{u_2} \re{a_2} \dots$
be a path in $U$ from $u_1=u$. By induction we obtain $\emptyset\neq \lquotW{u_i} \subseteq \lquotW{(u_1a_1\dots a_{i-1})}$.
Therefore, for all $i$, $ua_1\dots a_i \notin L$, so, by definition of $W$, the infinite word $ua_1a_2\dots$ belongs to $W$.

We show that $U$ is "$(\kk,W)$-universal for trees", for every cardinal $\kk$, and conclude by Lemma <ref>.
Let $T$ be a "$\SS$-tree" which "satisfies@@tree" $W$. For each node $t\in T$, let $\phi(t) = \lquotW{u_t}$ be the minimal "residual" such that $t$ "satisfies@@univ" $\lquotW{u_t}$. In particular, for the "root@@univ" $t_0$, $\phi(t_0)$ "satisfies@@univ" $W$ by the previous claim.
We claim that $\phi$ is a "morphism@@univ". Indeed, if $t\re{a} t'$ in $T$ and $t$ "satisfies@@univ" $\lquotW u$, then $t'$ "satisfies@@univ" $\lquotW{(ua)}$. Therefore, $\lquotW{u_t'}\leq \lquotW{(u_ta)}$, so $ \phi(t) = \lquotW{u_t} \re a \lquotW{u_{t'}} = \phi(t')$ is an edge in $U$.

§.§ Open objectives

We recall that an objective $W$ is "open" if

\[ W =\Reach{L} = \{w \mid w \text{ contains some prefix in } L\}, \]

for some $L\subseteq \SS^*$.

§.§.§ Reset-stability

In Section <ref>, we showed that "half-positional" "$\oo$-regular" "open" objectives are exactly those with residuals totally ordered and that are "progress consistent". However, for "non-$\oo$-regular" objectives, these conditions do not suffice, even if residuals are well-ordered.

[Progress consistency does not suffice]
Let $\SS = \NN$ and  let $W$ be the set of non strictly increasing sequences:

\[ W = \{ a_1a_2\dots \in \NN^\omega \mid a_{i+1} \leq a_i \text{ for some } i \ \}. \]

This objective is "open", as $W=\Reach{\text{two consecutive non-increasing numbers}}$.
Its residuals are:

\[ \lquotW{\ee} < \lquotW 0 < \lquotW 1 < \lquotW 2 < \cdots < \lquotW{(00)} = \SS^\oo.\]

Therefore, $\ResW$ is well-ordered. Moreover, $W$ is "progress consistent": any repetition of factors induces a non-strict inequality $<$ between consecutive letters.

However, we claim that $W$ is not "half-positional". Consider the game in Figure <ref>.
"Eve" can win this game: no matter what is the vertex $v_i$ chosen by "Adam", she can first move one position to the right, producing $i$, and then go down producing letter $1$. This ensures two consecutive non-increasing numbers.
However, she cannot "win positionally". Indeed, if such a strategy tells her to go always to the left, the sequence produced will be strictly increasing. If she choses to go down in vertex $v_i$, Adam can win by initialising the play in that vertex.

Game in which Eve wins if  she produces a non-strictly increasing sequence of numbers. She can win from every vertex, but not positionally.

We say that an "objective" $W\subseteq \SS^\oo$ is ""reset-stable"" if, for each sequence of finite words $u_1,u_2,u_3,\dots\in \SS^+$ and of residuals $\lquotW{s_0}, \lquotW{s_1}, \lquotW{s_2},\dots \in \ResW$:

\[\lquotW{s_{i}} \lRes \lquotW{(s_{i-1}u_{i})} \;\text{ for all } i\geq 1 \;\; \implies \;\; u_1u_2u_3\dots \in \lquotW{s_0}.\]

An intuitive idea of "reset-stability" is the following. Consider the (potentially infinite) "automaton of residuals" of $W$, which inherits the order over residuals. Add to it all $\ee$-transitions going backwards: $\lquotW s \re{\ee} \lquotW{s'}$ for $\lquotW{s'}<\lquotW{s}$. When a run takes an $\ee$-transition, we say that it ""makes a reset"".
What "reset-stability" tells us is that any run making infinitely many resets must be accepting.  The words $u_1,u_2,\dots$ in the definition above correspond to fragments where no "reset@@make" takes place, and $\lquotW{s_i}$ is the "residual" where we land after the ith "reset@@make".
(See also the notion of "$0$-jumps" in the proof of Lemma <ref>).

If $W$ is "reset-stable", it is "progress consistent". The converse holds if $\ResW$ is finite and totally ordered.

We note that all "closed objectives" are "reset-stable".

Let $W\subseteq \SS^\oo$ be a "half-positional" "objective" over "$\ee$-free" "Eve-games". Then, $W$ is "reset-stable".

Suppose by contradiction that $W$ is not "reset-stable". That is, there are $u_1,u_2,\dots \SS^+$   and $\lquotW{s_0},\lquotW{s_1} \dots$ such that $\lquotW{s_{i}} < \lquotW{(s_{i-1}u_{i})}$, but  $u_1u_2\dots \notin \lquotW{s_0}$.

Let $w_{i}\in \SS^\omega$ such that $w_i\in \lquotW{(s_{i-1}u_{i})} \setminus \lquotW{s_{i}}$.
We consider the game pictured in Figure <ref> (to ensure it to be "$\ee$-free", we just remove vertex $v_i$ if $s_i=\ee$).

Game in which Eve wins if  she produces a non-strictly increasing sequence of numbers. She can win from every $v_i$, but not positionally.

"Eve" can win $\G$ from any vertex $v_i$ (and from $v_i'$ if $s_i=\ee$), as she can produce the word $s_iu_{i+1}w_{i+1}$, which belongs to $W$, as we have taken $w_{i+1}\in \lquotW{(s_{i}u_{i+1})}$.
However, we show that no "positional strategy" ensures to win from all these vertices.
We distinguish two cases. If this "strategy" takes the path $v_i'\lrp{u_{i+1}} v_{i+1}'$ for all $i$, then it is not "winning from" $v_0$, as by hypothesis $u_1u_2\dots \notin \lquotW{s_0}$.
If on the contrary this strategy takes a path $v_i'\lrp{w_{i}}$, then it is not "winning from" $v_i$.

§.§.§ Characterisation for open objectives

Let $W\subseteq \SS^\oo$ be an "open objective". Then, $W$ is "half-positional" (over all "game graphs") if and only if:

* $\ResW$ is well-ordered by inclusion, and

* $W$ is "reset-stable".

The necessity of the conditions has already been established in Lemmas <ref> and <ref>. To prove the sufficiency, we give, for each cardinal $\kk$, a "well-ordered@@univ" "monotone@@univ" graph that is "$(\kappa,W)$-universal for trees", and conclude by Proposition <ref> and Lemma <ref>.

We let $U$ be the "$\SS$-graph" having as set of vertices $(\ResW \setminus \{\emptyset\}) \times \kappa$, ordered lexicographically. This graph is "well-ordered", as by hypothesis so is $\ResW$. The edges are given by:

\[ (\lquotW u , \lambda) \, \re a \,(\lquotW{u'} , \lambda') \quad\tif \quad \left\{\begin{array}{lc}
\lquotW{u'} = \lquotW{(ua)} \tand \lambda' < \lambda,& \tor \\[2mm]
\lquotW{u'} \lRes \lquotW{(ua)},& \tor \\[2mm]
\lquotW{u} = \SS^\oo.&
\end{array}\right. \]

By Lemma <ref>, this graph is "monotone@@univ". We show its "$(\kappa,W)$-universality for trees". The key ingredient for this is next claim, which strongly relies in the "reset-stability" hypothesis.
We let $L$ be the language of finite words such that $W=\Reach{L}$.

For each ordinal $\lambda < \kappa$ and each "residual" $\lquotW u$, vertex $(\lquotW u, \lambda)$ "satisfies@@univ" $\lquotW u$ in $U$.

Let $\rr= (\lquotW{u_0},\lambda_0)\re{a_1} (\lquotW{u_1},\lambda_1)\re{a_1} \cdots $ be an infinite path from $(\lquotW u, \lambda)$ in $U$, and consider its projection over the (infinite) "automaton of residuals" $\autRes{W}$. Whenever $\rr$ takes a transition $(\lquotW{u_i} , \lambda_i) \, \re a_i \,(\lquotW{u{i+1}} , \lambda_{i+1})$ with $\lquotW{u_{i+1}} = \lquotW{(u_ia_i)}$, this transition exists in $\autRes{W}$. If $\lquotW{u_{i+1}} \lRes \lquotW{(u_ia_i)}$, we say that this transition "makes a reset".
By induction, we obtain that $\lquotW{u_i} \leqRes \lquotW{(ua_1\dots a_{i})}$. We distinguish two cases:
(1) If $\rr$ "makes infinitely many resets", then we conclude by "reset-stability". (2) If $\rr$ "makes finitely many resets", then eventually $\lambda_{i+1}<\lambda_{i}$ for all $i$, unless $\lquotW{u_i}=\SS^\oo$. We conclude that eventually $\lquotW{u_i}=\SS^\oo \leqRes \lquotW{(ua_1\dots a_{i})}$. Therefore, $ua_1\dots a_i\in L$, so $ua_1a_2\dots\in W$.

Let $T$ be a "$\SS$-tree" whose "root@@univ" "satisfies@@univ" $W$.
We give a "morphism@@univ" $\phi\colon T \to U$, which we decompose in $\phi_1\colon T \to \ResW \setminus \{\emptyset\}$ and $\phi_2\colon T \to \kappa$.
For each $t\in T$, let $u_t$ be the word labelling the path from the "root" $t_0$ to $t$. We let $\phi_1(t) = \lquotW{u_t}$ for each $t$.
We define $\phi_2$ by transfinite induction.
By hypothesis, each branch eventually contains vertices $t$ such that $u_t\in L$ (that is, $\lquot{u_t} = \SS^\oo$). For all these vertices, we let $\phi_2(t) = 0$.
The tree obtained by removing these vertices, named $T_1$, does not have any infinite branch.
For an ordinal $\lambda<\kappa$, let $T_\lambda$ be the set of nodes for which we have not defined $\phi_2$ at step $\lambda$ of the induction.
For each leaf $t$ of $T_\lambda$, we let $\phi_2(t) = \lambda$.

This mapping has the two following properties:

* if $t\re a t'$ in $T$, then $\phi_1(t') = \lquotW{(u_ta)}$, and

* if $t\re a t'$ in $T$, either $\phi_2(t')<\phi_2(t)$, or $u_{t'}\in L$.

This ensures that $\phi = (\phi_1,\phi_2)$ is a "morphism@@univ", concluding the proof.

[Half-positional open objective]
Let $\SS = \NN$ and  let $W$ be the set of sequences that start by $123\dots n$, and eventually decrease. Formally:

\[ W = \{ a_1a_2\dots \in \NN^\omega \mid \text{there is } j \tst a_{i} = i \text{ for } i<j \tand a_j<j\}. \]

This objective is "recognised" by the infinite reachability automaton depicted in Figure <ref>.
Its residuals are well-ordered and it is "reset-stable", as after any reset we necessarily produce an word in $W$. Therefore, $W$ is "half-positional".

We remark that this objective is not "bipositional", as $\Res{\SS^\oo\setminus W}$ is not well-founded. This contrast with the case of "$\oo$-regular open" objectives, for which all "half-positional" "open objectives" are "bipositional" (Corollary <ref>).

Game in which Eve wins if  she produces a non-strictly increasing sequence of numbers. She can win, but not positionally.

§.§ 1-to-2-player lift and addition of neutral letters

Let $W\subseteq \SS^\oo$ be an "open" or "closed" "objective". If $W$ is "half-positional" over "$\ee$-free" "Eve-games", then $W$ is "half-positional" over all "game graphs".

We also obtain from our proofs that the Neutral letter conjecture (Conjecture <ref>) holds for "open" and "closed" objectives.

Let $W\subseteq \SS^\oo$ be an "open" or "closed" "objective". If $W$ is "half-positional", then $\addNeutral{W}$ is "half-positional".

In the proof of Theorems <ref> and <ref>, we obtained the positionality of objectives by providing "well-ordered@@univ" "monotone@@univ" "$(\kappa,W)$-universal" graphs. Proposition <ref> allows us to conclude.

We have therefore obtained the 1-to-2-player lift for $\oo$-regular objectives, as well as "open" and "closed" ones.
However, the 1-to-2-player lift does not hold for arbitrary objectives.
A counter-example is discussed in the PhD of Pierre Vandenhove <cit.>. The objective considered there (first appearing in <cit.>), is:

\[ \mathbf{MP}^\QQ = \{w\in \{0,1\}^\oo \mid \liminf_n \large(\sum_{i=0}^n w_i\large)\large/n \;\; \text{ is rational}\}. \]

In his PhD <cit.>, Vandenhove discusses the 1-to-2-player lift for finite "game graphs". The counter-example he gives also applies to infinite "game graphs".

We provide here a different example.

There is an objective $W\subseteq \SS^\oo$  that is "half-positional" over "Eve-games", but is not "half-positional" over all "game graphs".

Let $\SS$ be any infinite alphabet, and let $W$ be the following objective:

\[ \intro*\WInfMuller = \{ w\in \SS^\oo \mid \text{ the set of letters occurring infinitely often in } w \text{ is finite}\}. \]

To show that it is not "half-positional", we consider the game in Figure <ref>, in which "Eve" controls a single vertex, from which she can send the token to any vertex $v_i$ controlled by "Adam".

Game in which Eve wins if only finitely many letters are produced infinitely often. She can win by sending the token further and further away, but she cannot "win positionally".

We claim that "Eve" can win this game from every vertex by using the following "strategy": she keeps track of the maximal index $i_{\max}$ such that the play has passed trough vertex $v_{i_{\max}}$. Whenever Adam sends back the token to $v_{\Eve}$, she will go to vertex $v_{i_{\max}}$. This "strategy" ensures that only letter $1$ will be produced infinitely often.

However, "Eve" cannot win using a "positional@@strat" (or even finite memory) strategy. Such a strategy will only consider finitely many edges $v_{\Eve} \re 1 v_i$. Let $v_k$ be the maximal such vertex. "Adam" can win against such strategy by producing longer and longer paths, and then sending back the token to the vertex controlled by "Eve": $v_i\lrp{i(i+1)\dots} v_{k+j}\re 1 v_{\Eve}$. In this way, all numbers greater that $k$ will be produced infinitely often.

We show that $\WInfMuller$ is positional over "Eve-games".

For every "Eve-game" $\G$ with "winning condition" $\WInfMuller$ and every fixed vertex $v_0$, if "Eve" wins from $v_0$, she can "win from $v_0$" using a "positional strategy".

Assume that "Eve" "wins from $v_0$".
A "strategy" from $v_0$ is just an infinite path from $v$. Consider such a path. If this path does not visit a same vertex twice, it is already a positional strategy. On the contrary, let $v_k$ be the first vertex that repeats. Consider the first two occurrences of $v_{\mathsf{rep}}$:

\[ v_0 \re{a_0} v_1 \re{a_1} \cdots v_{k} \re{a_k} \cdots v_{k+j} \re{a_{k+j}} v_k. \]

Then, the "positional strategy" indicating to take the edge $v_i\re{a_i}v_{i+1}$ for $i\leq k+j$ is "winning@@strat".

We use this claim to prove that $\WInfMuller$ is ("uniformly") "half-positional" over "Eve-games".
Let $\G$ be an "Eve-game" with "winning condition" $\WInfMuller$. By "prefix-independence" of $\WInfMuller$, we can suppose without loss of generality that "Eve" "wins from" every vertex in $\G$. Let $v_1,v_2, \dots$ a (potentially transfinite) enumeration of vertices in $\G$. We will define a positional strategy $\strat\colon V \to E$ by transfinite induction. At step $\lambda$, let $\G_\lambda$ be the game obtained by removing vertices for which $\strat$ has already been defined. Let $i$ be the minimal index such that $v_i$ appears in $\G_\lambda$. By the previous claim, "Eve" has a positional strategy in $\G_\lambda$ that wins from $v_i$. Let $V_\lambda$ be the vertices reachable from $v$ by using this strategy, and for $v\in V_\lambda$ let $\strat(v)$ be the edge indicated by such strategy. We let $V_\lambda'$ be the vertices in $\G_\lambda\setminus V_\lambda$ from which "Eve" can reach $V_\lambda$, and fix a positional strategy doing so. We let $\strat(v')$ being given by this strategy for these vertices.
It is immediate that $\strat$ is a "positional strategy" in $\G$ that "wins from" all vertices.

§ CONCLUSIONS

The results presented in Section <ref> effectively address most open questions regarding "half-positionality" in the context of "$\oo$-regular languages".
Yet, it would be reasonable to seek a “better” characterisation.
One drawback of our approach is its conceptual complexity and its exclusive focus on automata; the characterisation is based on syntactic and combinatorial properties of "parity automata", rather than on intrinsic language-theoretical properties of the languages they "recognise".
In this respect, the insights gained about "half-positionality" are somewhat limited.
Therefore, we believe that there is still room for improvement and for a deeper understanding of the class of "half-positional" "$\oo$-regular" objectives.

To conclude, we discuss further research directions extending our results.

§.§ Positionality of $\BCSigma$ languages

A potential research direction consists in investigating "half-positionality" for broader classes of objectives.
We initiated this path in Section <ref> by studying "half-positionality" of "closed" and "open" objectives.
Going further in that direction,  the goal is to develop characterisations for more complex objectives defined by topological properties, mainly, higher classes in the Borel hierarchy.
A natural first step could be to look at objectives in $\intro*\SigmaTwo$ and $\intro*\PiTwo$, which are, respectively, unions of closed objectives and intersections of open objectives. These classes admit automata-oriented definitions: $\SigmaTwo$ are the objectives "recognised" by "deterministic" infinite "Büchi automata", and $\PiTwo$ those "recognised" by infinite "coBüchi automata" <cit.>.
Recently, Ohlmann and Skrzypczak proposed a characterisation of half-positionality for prefix-independent objectives in $\SigmaTwo$; however the cases of non-"prefix-independent" $\SigmaTwo$ "objectives" or $\PiTwo$ "objectives" are open.

The class of objectives "recognised" by infinite "deterministic" parity automata coincides with
$\intro*\BCSigma$: the class of boolean combinations of  objectives in $\SigmaTwo$ <cit.> (this is a strict subclass of $\Delta_3^0 = \Sigma_3^0 \cap \Pi_3^0$).  We hope to be able to give a characterisation for this class – as some of the constructions introduced in this work seems to generalise to automata with infinite states.
We believe that some properties of "half-positional" "$\oo$-regular objectives" could be lifted to $\BCSigma$ (or even to $\Delta_3$). In particular, we conjecture that the 1-to-2 player lift (false in general, see Proposition <ref>), holds for $\BCSigma$-objectives.

Let $W$ be an objective in $\BCSigma$ that is "half-positional over" "Eve-games". Then, it is "half-positional" over all games.

Decidability problems lose their relevance when dealing with classes of objectives defined by topological properties. Therefore, the question of what is a satisfactory characterisation becomes even harder to answer in this context – especially when  taking into account that we already have Ohlmann's characterisation based on "universal graphs" <cit.>.
A important steps forward would involve proving Conjecture <ref>, as well as "Kopczyński's conjecture" (Conjecture <ref>) or Ohlmann's "neutral letter conjecture" (Conjecture <ref>)  for the class $\BCSigma$.

§.§ Memory requirements of $\oo$-regular languages

An orthogonal research direction would be to maintain the focus on "$\oo$-regular languages", but attempt to characterise their memory requirements rather than just their "positionality".
A notable effort has already been made in this direction <cit.>,
however, only characterisations for fairly simple classes of languages are known (Muller <cit.> and "closed languages" <cit.>).
To this day, deciding whether "Eve" can "play optimally" in (finite or infinite) games using a given "$\oo$-regular objective" (even an "open" one) with $\leq k$ states of memory is not know to be decidable.
Also, the versions of the 1-to-2-players and finite-to-infinite lifts in the case of memory remain open (see <cit.>).

One difficulty is the multiplicity of models of memory: general, chromatic, $\ee$-memory... (we refer to <cit.> for details).
Recently, Bouyer, Fijalkow, Randour and Vandenhove showed that computing the chromatic memory requirements of "$\oo$-regular" "open@@obj" and "closed@@obj" objectives is $\NPc$ <cit.>.
This result, together with the $\NP$-completeness of the computation of the chromatic memory requirements of Muller objectives <cit.>, indicates that chromatic memory might be an ill-suited model for these purposes.
We believe that the most promising model to focus on in order to advance on this problem is $\ee$-memory, as discussed in <cit.>.
A first step required for moving forward involves characterising memory requirements for "open objectives". Nevertheless, progress in understanding the general memory for "open objectives" has remained elusive for more than 10 years <cit.>.

The generalisation of the theory of "monotone@@graph" "universal graphs" to characterise memory, presented in <cit.>, offers a promising tool to establish tight upper bounds on memory requirements, which could be valuable to overcome impediments in the advancement of the study of memory for "$\oo$-regular objectives".

§.§ Minimisation and canonisation of parity automata

For the proof of Theorem <ref> (Section <ref>), we have introduced new notions concerning congruences for parity automata, as well as different transformations of automata.

This transformations exhibit a flavour similar to what one might expect from minimisation algorithms, as their main purpose is to remove redundant states from automata.
We believe that this techniques will be valuable for the study of $\oo$-automata in other contexts, as they allow for a fine analysis of the structure of the automata.

Also, a key ingredient in our proof is the use of "history-deterministic" automata, in particular, a generalisation of the minimisation algorithm for "history-deterministic" "coBüchi automata" introduced by Abu Radi and Kupferman <cit.>. We see this fact as further evidence that "history-deterministic" automata provide canonicity properties.

In fact, we can derive actual concrete statements about the minimisation of automata from our results:

Deterministic (resp. "history-deterministic") parity automata "recognising" "bipositional" languages can be minimised in polynomial time.

A necessary condition for a language $L$ to be "bipositional" is that it must be recognised by a "parity automaton on top" of the "automaton of residuals" (Theorem <ref>). It turns out that such an automaton can be computed in polynomial time.

Deterministic (resp. "history-deterministic") "Büchi@@aut" and "coBüchi automata" "recognising" "half-positional" languages can be minimised in polynomial time.

In the case of "Büchi automata", a "half-positional" language can be "recognised" by the "automaton of residuals" (Propositions <ref>), which is necessary minimal amongst "history-deterministic" automata.

In the case of "coBüchi automata", we obtained that the minimal "history-deterministic" automaton of Abu Radi and Kupferman, computable in polynomial time, can be taken "deterministic" for "half-positional" languages (Section <ref>).

We conjecture that our methods may lead to similar results in the more general case of "parity automata", and that minimal automata for "half-positional" languages can be obtained just by merging states of "signature automata".

"Deterministic" and "history-deterministic" "parity automata" "recognising" "half-positional" languages can be minimised in polynomial time.
Moreover, "history-deterministic" "parity automata" for this class of languages are not more succinct than "deterministic" ones.

§ FULL PROOFS FOR SECTION <REF>

In this Appendix, we include full proofs for all the propositions and lemmas appearing in Section <ref>.
In order to be able to tackle these proofs and formalise them in the simplest and cleanest possible way, we first introduce some technical artillery that will come in handy to deal with the structure of layered total preorders of "signature automata".
We begin by introducing "nice transformations" of automata equipped with a "priority-faithful" relation in Section <ref>.
Then, in Section <ref> we give the full details of the induction constructing a "structured signature automaton" for a "half-positional" language.

§.§ Nice transformations of automata

To recursively build a "structured signature automaton", we will apply a sequence of transformations to a given "$d$-signature automaton" $\A$, by removing states and adding or redirecting edges in such a way that relations $\eqRes{x}$ are preserved in a strong sense formalised in this section.
Before presenting the proofs of the results from Section <ref>,  we introduce some notations and prove technical lemmas that will come in handy to reason about ("structured") "signature automata".

We recall that automata are assumed to be "complete" and "semantically deterministic".

*Automata with a common subautomaton

Let $\A$ be a "semantically deterministic" automaton with states $Q_\A$, and let $\eqRes{\A}$ be the "congruence" given by the equality of "residuals". We note that if $\B$ is an automaton with states $Q_\B\subseteq Q_\A$, relation $\eqRes{\A}$ induces an equivalent relation over $Q_\B$ (which, in general, is not a "congruence" nor coincides with the equality of "residuals" of $\B$).

Let $\A$ be a "semantically deterministic" "parity automaton" with states $Q_\A$ and let $\B$ be a "parity automaton" with states $Q_\B\subseteq Q_\A$. Assume that $\eqRes{\A}$ is a "congruence" over $\B$ and that $\quotAut{\B}{\A} = \quotAut{\A}{\A}$. Let $\A'$ be a "subautomaton" of both $\A$ and $\B$.
If a word $w\in \SS^\oo$ admits an "accepting run" in $\B$ that eventually remains in $\A'$, then $w$ is also "accepted by" $\A$.

\[q_0\re{w_0}q_1\re{w_1}q_2\re{w_2}\dots\re{w_{k-1}} q_k\re{w_k}q_{k+1}\re{w_{k+1}} \dots\]

be an "accepting run" over $w$ in $\B$ such that the suffix from $q_k$ is contained in $\A'$ (meaning that both the states and the transitions used are part of $\A'$).
We consider the "projection@@quot" of the prefix of size $k$ of the run in the "quotient automaton" $\quotAut{\B}{\A} = \quotAut{\A}{\A}$.  By Lemma <ref>, there is a "run over" $w_0\dots w_{k-1}$ in $\A$, $p_0\re{w_0}p_1\re{w_1}\dots p_k$ whose "projection@@quot" over the "quotient automaton" coincides with the previous one. Therefore, $p_k\eqRes{\A} q_k$, that is, $\Lang{\initialAut{\A}{p_k}} = \Lang{\initialAut{\A}{q_k}}$. Since $w_{k+1}w_{k+2}\dots$ admits an "accepting run" from $q_k$ in $\A$, it also admits an "accepting run" from $p_k$, and $w$ is "accepted@@aut" by $\A$.

*Nice transformations of automata

For $x\in \NN$, we denote by $\intro*\autGeq{\A}{x}$ the "subautomaton" of $\A$ induced by the set of transitions using a priority $\geq x$.

Let $\A$ be a "semantically deterministic" "parity automaton" over $\SS$ with states $Q$, let $x$ be a "priority", and let  $\sim$ be a "$[0,x-1]$-faithful congruence" over $\A$.
Let $\A'$ be a "parity automaton" over $\SS$ with states $Q'\subseteq Q$. We denote $\sim$ the induced relation over $Q'$.
We say that $\A'$ is a ""$\sim$-nice transformation of $\A$ at level $x$"" if:

* $\sim$ is a "$[0,x-1]$-faithful congruence" over $\A'$ and $\autLeq{\A}{}{x-1} = \autLeq{\A'}{}{x-1}$,

* $\eqRes{\A}$ is a "congruence" over $\A'$ and $\quotAut{\A'}{\A} = \quotAut{\A}{\A}$, and

* $\autGeq{\A'}{x+1}$ coincides with the "subautomaton" of $\autGeq{\A}{x+1}$ induced by the states in $Q'$.

Intuitively, if $\A'$ is a "nice transformation" of $\A$ at level $x$, it means that the only relevant modifications applied to $\A$ concern "$x$-transitions@@out". The structure of the "quotient automaton@@leq" for priorities ${<}x$ is left unchanged, and so is the acceptance of runs that eventually only produce priorities ${>}x$.

We note that if $\sim$ is an equivalence relation that "refines" $\eqRes{\A}$, then the second item of Definition <ref> is implied by the first one. This is in particular the case if $\sim$ is an equivalent relation $\eqSig{x}$ of a "$d$-signature automaton", for $0\leq x\leq d$.

Let $\A$ be a "semantically deterministic" "parity automaton" equipped with  a "$[0,x-1]$-faithful congruence" $\sim$. Suppose that $\A$ is "deterministic over" ${>}x$-transitions.
Let $\A'$ be a "$\sim$-nice transformation of $\A$ at level $x$". If $q\sim q'$ are two states of $\A'$ such that there is path $q\lrp{w:y}p$ in $\A$, then a path $q'\lrp{w:y'}p'$ in $\A'$ satisfies:

* $p\sim p'$,

* if $y<x$, then $y'=y$, and

* if $y\geq x$, then $y'\geq x$.

The equivalence $p\sim p'$ follows from the fact that $\sim$ is a "congruence" in $\A'$ and $\quotAut{\A'}{\A} = \quotAut{\A}{\A}$.
For $y\leq x-1$ or $y'\leq x-1$, the equality $y'=y$ follows from the equality of the "${\leq}(x-1)$-quotient automata".
This directly implies the third item.

Let $\A$ be a "$\ee$-completion" that admits  a "$[0,x]$-faithful congruence" $\sim$. If a word $w\in \SS^\oo$ admits a run such that the minimal priority produced infinitely often is $y\leq x$, then the  minimal priority produced infinitely often by any "run over $w$" is $y$. In particular, if $y$ is odd, $w$ "is rejected with priority" $y$.

Let $q_0\re{w_1:y_1}q_1\re{w_2:y_2}\dots $ and $q_0'=q_0\re{w_1:y_1'}q_1'\re{w_2:y_2'}\dots $ be two runs over the same word in $\A$ ($q_0=q_0'$ being the "initial state" of $\A$). Since $\sim$ is a congruence, we obtain by induction that $q_i\sim q_i'$ for every $i$. Moreover, as, for $y\leq x$,  $y$-transitions "act uniformly" over $\sim$-classes, each time that $y_i\leq x$, we have that $y_i'=x_i$.

Let $\A$ be a "semantically deterministic" "parity automaton" equipped with  a "$[0,x-1]$-faithful congruence" $\sim$.
Let $\A'$ be a "$\sim$-nice transformation of $\A$ at level $x$". We have:

* A word $w\in \SS^\oo$ can be "accepted with an even priority" $y<x$ in $\A'$ if and only if $w$ can be "accepted with priority" $y$ in $\A$.

* A word $w\in \SS^\oo$ is "rejected with an odd priority" $y<x$ in $\A'$ if and only if $w$ is "rejected with priority" $y$ in $\A$.

* If a word $w\in \SS^\oo$ can be "accepted with an even priority" $y>x$ in $\A'$, then it is "accepted by@@aut" $\A$.

If moreover $\A$ is "homogeneous" and "deterministic over" transitions using priorities $> x$, we have:

* If there is a "rejecting@@run" run over $w\in \SS^\oo$  in $\A'$ producing as minimal priority $y>x$, then $w$ is "rejected@@aut" by $\A$.

Let $w\in \SS^\oo$ be a word "accepted with a priority" $y<x$ in $\A$ (resp. $\A'$). Then, by Lemma <ref>, $w$ is "accepted by" the "quotient automaton@@leq" $\autLeq{\A}{}{x-1} = \autLeq{\A'}{}{x-1}$. Again by  Lemma <ref>, $w$ is "accepted by" $\A'$ (resp. $\A$). The second item is obtained using the same argument, combined with Lemma <ref>.

The third item is directly implied by Lemma <ref>, as $\autGeq{\A'}{x+1}$ is a "subautomaton" of $\autGeq{\A}{x+1}$.

For the last item, let $q_0\lrp{w_0}q'\lrp{w'}$ be a "rejecting@@run" "run over" $w$ in $\A'$ such that the suffix $q'\lrp{w'}$ does not produce any priority $\leq x$ (that is, it is contained in $\autGeq{\A'}{x+1}$). By determinism and "homogeneity", this is the only "run over" $w'$ from $q'$ in $\A$, and therefore $w'\notin\Lang{\initialAut{\A}{q'}}$. We conclude using the equality $\quotAut{\A'}{\A} = \quotAut{\A}{\A}$.

§.§ From half-positionality to structured signature automata: Full proofs for Section <ref>

We provide all the technical details for the proofs of the propositions appearing in Section <ref>.
We first state some useful simple lemmas.

Let $W\subseteq \SS^\oo$ be "half-positional" over finite, "$\ee$-free" "Eve-games". Then, for every word $u\in\SS^*$,  objective $\lquotW{u}$ is "half-positional" over finite, "$\ee$-free" "Eve-games".

Any game with vertices $V$ witnessing non-half-positionality of $\lquotW{u}$ can be turned into a game witnessing non-half-positionality of $W$ by adding, for every $v\in V$, a fresh vertex $v_u$ and a path $v_u\lrp{u}v$.

To check if a "parity automaton" is in "normal form", it suffices to verify that, if $q$ and $p$ are in a same "positive@@SCC" (resp. "negative@@SCC") "SCC" and there is a transition $q\re{x} p$ producing "priority" $x>0$ (resp. $x>1$), then there are two paths  $p\lrpE q$ producing as minimal "priority" $x$ and $x-1$, respectively.

We do the proof for the case of a "positive SCC".
Assume that there is a path $q=q_0 \re x_1 q_1 \re x_2 \dots \re x_n q_n = p$ with $x = \min x_i >0$. By hypothesis, for $1\leq i\leq n$, there are paths $q_i\ lrp{x_i-1} q_{i-1}$. Concatenating them, we obtain a path $p\lrp{x-1}q$. Iterating this process, we can obtain loops $q\lrpE p \lrpE q$ producing as minimal "priority" any number in $[0,x-1]$. To obtain a path $p\lrp{x}q$, we just use the existence of paths $q_i\ lrp{x_i} q_{i-1}$.

§.§.§ Base case: Total order of residual classes

Let $W\subseteq \SS^\oo$ be an "$\oo$-regular" objective that is "half-positional" over finite, "$\ee$-free" "Eve-games". Then, $\Res{W}$ is totally ordered by inclusion.

The proof is almost identical to that of Lemma <ref>.
We show the contrapositive.
Assume that $W$ has two incomparable "residuals", $\lquotW{u_1}$ and $\lquotW{u_2}$.
We consider first the case $u_1\neq \ee$ and $u_2\neq \ee$.
Take $w_1\in \lquot{u_1}{W}\setminus\lquot{u_2}{W}$ and $w_2\in \lquot{u_2}{W}\setminus\lquot{u_1}{W}$. Thanks to $\oo$-regularity, we can take these words of the form $w_i = u_i'(w_i')^\oo$, with $u_i',w_i'\in \SS^+$, for $i=1,2$.
We have

$u_1w_1\in W$,     $u_1w_2\notin W$,

$u_2w_1\notin W$,     $u_2w_2\in W$.

Consider the "$\ee$-free", finite, "Eve-game" $\G$ represented in Figure <ref>.
"Eve" "wins" $\G$ from $v_1$ and $v_2$: if a "play" starts in $v_i$, for $i=1,2$, she just has to take the path labelled $u_i'(w_i')^\oo$ from $v_{\mathsf{choice}}$. However, she cannot win from both $v_1$ and $v_2$ using a "positional strategy". Indeed, such "positional strategy" would choose one path $v_{\mathsf{choice}} \lrp{u_i(w_i')}$, and the "play" induced when starting from $v_{1-i}$ would be "losing@@play".

A game $\G$ in which "Eve" cannot "play optimally using positional strategies" if $\Res{W}$ is not totally ordered.

Finally, we take care of the case in which $\resClass{u_1} = \{\ee\}$ (symmetric for $u_2$). In that case, we cannot take $u_1\neq \ee$. We remark that, since $\resClass{u_1} \neq \resClass{u_2}$, we can take $u_2\neq \ee$.
We consider the game from Figure <ref> in which we simply remove vertex $v_1$. This game is "$\ee$-free", and "Eve" can win from both $v_2$ and $v_{\mathsf{choice}}$, but not "positionally@@win".

In all the rest of the subsection, we assume that $x\geq 2$.

§.§.§ Safe centrality and relation $\eqSig{x-1}$. Proof of Lemma <ref>

In this paragraph we give a proof of Lemma <ref>. We assume that $x\geq 2$ is an even priority and $\A$ is a "deterministic" "$(x-2)$-structured signature automaton" with initial state $q_\init$.

During the proof, we will lose the "determinism" of $\A$. However, in all the subsection we will maintain the three first required properties. In the statements of all lemmas, $\A$ will stand for an "$(x-2)$-structured signature" automaton that is:

* "deterministic over" transitions with "priority" different from $x-1$,

* "homogeneous", and

* "history-deterministic".

We say that an automaton $\A'$ is ""$(x-1)$-saturated"" if for every state $q$ and letter $a\in \SS$, if a transition $q\re{a:x-1} p$ exists in $\A'$, then $q\re{a:x-1} p'$ appears in $\A'$ for all $p'\eqSig{x-2} p$.
The "$(x-1)$-saturation" of $\A$ is the automaton obtained by adding all those transitions.

We note that this definition slightly differs from the definition of "$1$-saturation@@coB" used in the warm-up (Section <ref>). In particular, the definition of the warm-up does not preserve "homogeneity". We allow ourselves these small disagreements of definitions for the sake of clarity in the presentation in each respective subsection.

The "$(x-1)$-saturation" of $\A$ is "homogeneous" and "deterministic over" transitions with "priority" different from $x-1$.

The "$(x-1)$-saturation" of $\A$ is in "normal form".

We use the characterisation of "normal form" given in Lemma <ref>. Let $\A'$ be the "$(x-1)$-saturation" of $\A$.
The property of Lemma <ref> is satisfied for transitions already appearing in $\A$, as $\A$ is assumed to be in "normal form".
Let  $q\re{a:x-1}p$ be a transition added by the saturation process, and let $q\re{a:x-1} p'$ be a transition in $\A$ with $p\eqSig{x-2} p'$. By Item <ref> of the definition of "structured signature automaton", there is a path $p\lrp{u: >x-2} p'$ in $\A$. By "normality" of $\A$, there are also paths $p'\lrp{u_1:x-1} q$ and $p'\lrp{u_2:x-2} q$. We obtain the two desired paths in $\A'$:

\[p \lrp{u:>x-2} p' \lrp{u_1:x-1}q \;,  \quad \tand \quad  p \lrp{u:>x-2} p' \lrp{u_2:x-2}q.\qedhere\]

The following lemma states that "$(x-1)$-saturation" is a "$\eqSig{x-2}$-nice transformation at level $x-1$", so Lemmas <ref> and <ref> can be applied. We recall that $\eqSig{x-2}$ "refines" $\eqRes{\A}$, so congruence of $\eqRes{\A}$ is implied by that of $\eqSig{x-2}$.

The  "$(x-1)$-saturation" of $\A$  is a "$\eqRes{x-2}$-nice transformation of $\A$ at level $x-1$".

Let $\A'$ be the "$(x-1)$-saturation" of $\A$.
It is immediate that $\autGeq{\A}{x} = \autGeq{\A'}{x}$. Moreover, the restriction of $\A$ and $\A'$ to transitions using priorities $\leq x-2$ coincides, so for each $0\leq y\leq x-2$, relation $\eqRes{x-2}$ is a "congruence for" "$y$-transitions" in $\A'$ (and therefore these transitions "act uniformly" by "determinism"). The "congruence for" transitions using priority ${>}(x-2)$ is preserved as we have only added $(x-1)$-transitions that go to the same $\eqSig{x-2}$-class.
As $\eqSig{x-2}$ "refines" $\eqRes{\A}$, the latter relation is also a "congruence" in $\A'$ and $\quotAut{\A}{\A} = \quotAut{\A'}{\A}$.

The  "$(x-1)$-saturation" of $\A$ "recognises" $\Lang{\A}$. Moreover, it is "history-deterministic", "homogeneous" and "deterministic over transitions" using "priorities" different from $x-1$.

Let $\A'$ be the  "$(x-1)$-saturation" of $\A$. We have already noted that it is "homogeneous" and "deterministic over transitions" using "priority" different from $x-1$ (Remark <ref>).

If $w\in \SS^\oo$ is "accepted by" $\A'$ (resp. by $\A$), it is either "accepted with" an even priority $y<x-1$ or $y>x-1$. In the first case, since  $\A'$ is a "$\eqRes{x-2}$-nice transformation at level $x-1$", Lemma <ref> allows us to conclude. In the second case, it suffices to apply Lemma <ref>.

"History-determinism" of $\A'$ is clear: one can use a "resolver@@aut" for $\A$.

Redundant safe components.

From now on, we suppose that $\A$ is "$(x-1)$-saturated".

We say that a "$({<}x)$-safe component" $S$ of $\A$ is ""redundant@@sig"" if there is $q\in S$ and $q'\eqSig{x-2}q$, $q'\notin S$, such that $\safeSig{x}{q}\subseteq \safeSig{x}{q'}$.
We note that, by "normality" of $\A$, there are no "$({\geq}x)$-transitions" entering in $S$; that is, there are no transitions $p\re{a:\geq x} q$ with $p\notin S$ and $q\in S$.

Automaton $\A$ is "$({<}x)$-safe centralised" if and only if it does not contain any "redundant@@sig" "$({<}x)$-safe component".

If $\A$ contains some "redundant@@sig" "$({<}x)$-safe component", we can find one of them in polynomial time.

The computation of the "$({<}x)$-safe components" of $\A$ can be done by simply a decomposition in "SCC" of $\autGeq{\A}{x}$.
For each pair of states $q\eqSig{x-2}q'$ in different "$({<}x)$-safe components" we just need to check the inclusion $\safeSig{x}{q}\subseteq \safeSig{x}{q'}$, which can be done in polynomial time.

Let $S$ be a "redundant@@sig" "$({<}x)$-safe component" of $\A$, and let $S'$ be a different "$({<}x)$-safe component" such that there are $q_0\in S$ and  $q_0'\in S'$, with $q_0\eqSig{x-2}q_0'$ and $\safeSig{x}{q_0}\subseteq \safeSig{x}{q_0'}$.
Then, for each $q\in S$ there is $q'\in S'$ such that $q\eqSig{x-2}q'$ and $\safeSig{x}{q}\subseteq \safeSig{x}{q'}$.

For each $q\in S$, pick $u\in \SS^*$ such that $q_0\lrp{u:\geq x} q$. We let $q'$ be such that $q_0'\lrp{u} q'$. Since $u\in \safeSig{x}{q_0}\subseteq \safeSig{x}{q_0'}$, this latter path produces priority $\geq x$ and, by "normality", $q'$ is in $S'$.
As $\eqSig{x-2}$ is a "congruence for" "$({\geq}x-2)$-transitions", $q'\eqSig{x-2}q$. By monotonicity for safe languages (Lemma <ref>), we also have $\safeSig{x}{q}\subseteq \safeSig{x}{q'}$.

Removing redundant safe components.

For now on, fix $S$ to be a "redundant@@sig" "$({<}x)$-safe component" of $\A$, and $S'$ a different "$({<}x)$-safe component" as in the previous lemma.
For each $q\in S$, we let $\intro*\pick(q)\in S'$ such that $q\eqSig{x-2}\pick(q)$ and $\safeSig{x}{q}\subseteq \safeSig{x}{\pick(q)}$.
We extend $\pick$ to all of $Q$ by setting it to be the identity over $Q\setminus S$.

We define the automaton $\A'$ as follows:

* The set of states is $Q' = Q\setminus S$.

* The "initial state" is $\pick(q_\init)$.

* For each $p\in Q'$, if $p\re{a: y} q$ is a transition in $\A$, we let $p\re{a:y}\pick(q)$ in $\A'$.

We note that, if $q\notin S$, all transitions $p\re{a: y} q$ in $\A$ are left unchanged. In particular, the "$({\geq}x)$-transitions" of $\A'$ are the restriction of those appearing in $\A$, $\A'$ is "$(x-1)$-saturated", and "$({<}x)$-transitions" in $\A$ not entering in $S$ appear in $\A'$ too.
We say that transitions $p\re{a: y} q$ of $\A$ such that $q\in S$ have been ""redirected in $\A'$@@sc"".

Automaton $\A'$ is a "$\eqSig{x-2}$-nice transformation of $\A$ at level $x-1$".

We have that $\autGeq{\A'}{x}$ is the "subautomaton" of $\autGeq{\A}{x}$ induced by states in $Q'$. We show that $\eqSig{x-2}$ is "$[0,x-2]$-faithful" in $\A'$.
Transitions that have not been "redirected@@sc" satisfy the congruence requirements, as they satisfy them in $\A$.
Let $p\re{a:y}q$ and $p'\re{a:y'}q_0'$ be two transitions in $\A'$ such that $y\leq x-2$, $p\eqSig{x-2} p'$ and such that the second transition has been redirected from $p'\re{a:y'}q'$ (the first transition is possibly a redirected one too).
By the congruence property in $\A$, we have that $y'=y$ and $q\eqSig{x-2}q'$. Since $q'\eqSig{x-2}q_0'$, we conclude by transitivity.
The equality $\autLeq{\A'}{x-2}{x-1}=\autLeq{\A}{x-2}{x-1}$ simply follows from the fact that "redirected@@sc" transitions have been defined preserving the $\eqRes{x-2}$-classes.

As $\eqSig{x-2}$ "refines" $\eqRes{\A}$, the latter relation is also a "congruence" in $\A'$ and $\quotAut{\A}{\A} = \quotAut{\A'}{\A}$.

For every state $q'\in Q'$, we have $\Lang{\initialAut{\A'}{q'}} = \Lang{\initialAut{\A}{q'}}$.
In particular, these automata are "equivalent@@aut".
Moreover, automaton $\A'$ is "deterministic over" transitions with "priority" different from $x-1$, "homogeneous" and "history-deterministic".

The fact that $\A'$ is "deterministic over" transitions with "priority" different from $x-1$ and "homogeneous"  is immediate from its definition.
We show the equality of languages for the "initial state". The proof is identical for a different state.

The inclusion $\Lang{\A'}\subseteq \Lang{\A}$ directly follows from Lemma <ref>.

We describe a "sound resolver" witnessing $\Lang{\A}\subseteq \Lang{\A'}$ and "history-determinism". Take a "sound resolver" $\resolv$ in $\A$, let $w\in \SS^\oo$, and write

\[		\rho=p_0 \re{w_0} p_1 \re{w_1} \dots\]

for the run in $\A$ "induced by@@resolver" $\resolv$ over $w$.
We will build a "resolver" $\resolv'$ in $\A'$ satisfying the property that the "run induced over $w$@@res", $\rho'=p'_0 \re{w_0} p'_1 \re{w_1} \dots$ is in one of the following (non-excluding) cases:

*  produces priorities $<x-1$ infinitely often,

*  eventually produces only priorities $\geq x$,

*  $p_i \eqSig{x-2} p'_i$ and $\safeSig{x}{p_i}\subseteq \safeSig{x}{p_i'}$ for every $i$ sufficiently large.

A "resolver" $\resolv'$ satisfying the property above accepts all words in $\Lang{\A}$.

Suppose that $w\in \Lang{\A}$, that is, the run $\rr$ "induced by@@resolv" $\resolv$ is "accepting@@run". Let $\rr'$ be the "run induced over $w$@@res" by $\resolv'$ in $\A'$. We distinguish two cases, according to the priorities produced by the run $\rr$ in $\A$:

If $\rr$ produces priorities $<x-1$ infinitely often. Then Lemma <ref> allows us to conclude.

If $\rr$ eventually only produces priorities $\geq x-1$.

Then, the two first items of Lemma <ref> tells us that $\rr'$ eventually only produces priorities $\geq x-1$ too (so we are not in Case <ref>).
We show that $\rr'$ eventually only produces priorities $> x-1$; the last item of Lemma <ref> allows us to conclude (we recall that $\A'$ is a "$\eqSig{x-2}$-nice transformation at level $x-1$").
If we are in Case <ref>, this property is trivially satisfied. Suppose that we are in Case <ref>, and let $k>0$ be such that the suffix of $\rr$ from $q_k$ only produces priorities $\geq x$ and such that $\safeSig{x}{p_i}\subseteq \safeSig{x}{p_i'}$ for $i\geq k$. Therefore, there is a "run over $w_kw_{k+1}\dots$" from $p_k'$ producing exclusively priorities $\geq x$. By "determinism over transitions" with priority $\geq x$, this run is the one "induced by" $\resolv'$.

We finally show how to construct a "resolver" with this property.
We let $p'_0=f(p_0)$, and assume $\rho'$ constructed up to $p'_i$ satisfying that $p'_i\eqSig{x-2} p_i$.

If there is a transition $p'_i \re{w_i:y} p'_{i+1}$ with $y\neq x-1$, then we take this one (there is no other option),  which satisfies $p_{i+1} \eqSig{x-2} p_{i+1}'$ by Lemma <ref>.
Moreover, if $y\geq x$ and $\safeSig{x}{p_i}\subseteq \safeSig{x}{p_i'}$, then $\safeSig{x}{p_{i+1}}\subseteq \safeSig{x}{p_{i+1}'}$ by Lemma <ref>.
If there is a transition $p'_i \re{w_i:x-1}$,  we take $p_{i+1}'=f(p_{i+1})$ (this transition exists in $\A'$ by "$x-1$-saturation", as $p'_i\eqSig{x-2} p_i$).

We show that this "resolver" satisfies the desired property. Suppose that we are not in the two first cases, that is,  $\rr'$ eventually only produces priorities $\geq x-1$, and it produces priority $x-1$ infinitely often. Take a suffix $p'_k \re{w_k:y_k} p'_{k+1} \re{w_{k+1}:y_{k+1}} \dots$ of $\rr'$ such that no priority $<x-1$ is produced and such that $y_k=x-1$. Then, by definition of the transitions using $x-1$ chosen by the "resolver", $p_{k+1}'=f(p_{k+1})$, so $\safeSig{x}{p_{k+1}}\subseteq \safeSig{x}{p_{k+1}'}$. We conclude by induction, as transitions taken by the resolver using priorities $\geq x-1$ preserve the inclusion of "$({<}x)$-safe languages".

Transformation preserves being a structured signature automaton.

To be able to finish the proof of Lemma <ref>, we just need to show that $\A'$ is a "$(x-2)$-structured signature automaton". We give some technical lemmas that will help us show this.

Let $q$ and $p$ be two states of $\A'$. There is a path $q\lrp{w:x-1}p$ in $\A$ if and only if there is a path $q\lrp{w:x-1}p$ in $\A'$.

If a path $q\lrp{w:x-1}p$ appears in $\A'$, the very same path also exists in $\A$.

Suppose now that a path $\rr = q\lrp{w:x-1}p$ exists in $\A$.
Let $S$ be the "${<}x$-safe component" that has been removed from $\A$. If the path $\rr$ does not cross $S$, then it also appears in $\A$. Suppose that it enters in $S$. We remark that, by "normality" and by the definition of "safe component@@sig", each time that $\rr$ enters or exists $S$, it produces priority $x-1$. We consider the last time that $\rr$ enters and exists $S$:

\[ q\lrp{u_1:\geq x-1} q_1 \lrp{u_2:\geq x} q_2 \re{a:x-1} q_3 \lrp{u_3:\geq x-1}  p, \]

with $w=u_1u_2au_3$, $q_3\notin S$, and the path $q_3 \lrp{u_3}  p$ does not enter $S$ (so it also appears in $\A'$). Consider any "run over" $u_1u_2$ from $q$ in $\A'$:

\[ q\lrp{u_1:\geq x-1} q_1' \lrp{u_2:\geq x-1} q_2'.\]

As $\eqSig{x-2}$ is a "$[0,x-2]$-faithful congruence", we have that $q_2\eqSig{x-2}q_2'$. As $\A'$ is "$x-1$-saturated", there is a transition $q_2'\re{a:x-1} q_3$. Therefore, we obtain in $\A'$ the path:

\[ q\lrp{u_1:\geq x-1} q_1' \lrp{u_2:\geq x-1} q_2' \re{a:x-1} q_3 \lrp{u_3:\geq x-1}  p.\qedhere\]

Let $q$ and $p$ be two states of $\A'$ and let $y$ be any "priority". There is a path $q\lrp{w:y}p$ in $\A$ if and only if there is a path $q\lrp{w':y}p$ in $\A'$.

If $y\geq x$, $q$ and $p$ are in the same "$({<}x-1)$-safe component". Since the "$({<}x-1)$-safe components" in $\A'$ are safe components in $\A$, the result is clear in this case.

If $y=x-1$, the result is assured by the previous Lemma <ref>.

Assume $y<x-1$.
Suppose that there is a path $q\lrp{w:y}p$ in $\A$ (the proof is analogous if we take this path in $\A'$), and let  $q\lrp{w:y'}p'$ be the "run over" $w$ from $q$ in $\A'$.
As $\A'$ is a "$\eqSig{x-2}$-nice transformation", by Lemma <ref>, we have that $y'=y$ and $p\eqSig{x-2}p'$. As $\A$ satisfies Item <ref> from the definition of a "structured signature automaton", there is a path $p'\lrp{u:\geq x-1}p$ in $\A$. By Lemma <ref>, such a path also exists in $\A'$, so we can take $w'=wu$, giving us a path $q\lrp{w:y}p'\lrp{u:>y}p$.

Previous lemma tells us, in particular, that for every "$({<})y$-safe component" $\safeComp{y}_i$ of $\A$, the intersection of $\safeComp{y}_i$ with $Q'$ constitute the states of a "$({<})y$-safe component" in $\A'$.
Therefore, automaton $\A'$ inherits the decomposition in "$({<})y$-safe component" $\safeComp{y}_1,\dots, \safeComp{y}_{k_y}$ from $\A$, for each $y$; we simply remove those components whose intersection with $Q'$ is empty.

Automaton $\A'$ is a "$(x-2)$-structured signature automaton".

We go through all the conditions of the definition of a "$(x-2)$-structured signature automaton".
We recall that, by Lemma <ref>, the relation $\eqSig{x-2}$ is "$[0,x-2]$-faithful congruence" in $\A'$.

Normal form. We check that $\A'$ satisfies the hypothesis of the characterisation from Lemma <ref>. We let $q'\re{a:y} p'$ be a transition in $\A'$. If it is not a "redirected transition@@safec", it exists in $\A$, so we can conclude by "normalisation" of $\A$ and Lemma <ref>.
Assume that $q'\re{a:y} p'$ is a transition that has been "redirected from@@safec" $q'\re{a:y}p$. In particular, $p\eqRes{x-2}p'$ and $y<x$. By Item <ref> of the definition of "structured signature automaton" applied to $\A$, there is a path $p'\lrp{w:>y}p$ in $\A$, and by "normality", there is a returning paths $p\lrp{u_1:y}q$ and $p\lrp{u_2:y-1}q$. Again, Lemma <ref> allows us to find the desired returning paths in $\A'$.

Item <ref>. By Lemma <ref>, the residuals in $\A'$ correspond to those in $\A$, so "preorder" $\leqSig{0}$ correspond to their inclusion in $\A'$ too.

Item <ref>. By the previous remarks, for all $y$, the "$({<}y)$-safe components" of $\A'$ are obtaining by taking the intersection with those in $\A$. Therefore, odd preorders $\leqSig{y-1}$ correspond to the order of "$({<}y)$-safe components" on $\A'$.

Item <ref>. As $\A'$ is a "$\eqSig{x-2}$-nice transformation at level $x-1$", for every $y<x-1$ and state $q'$ in $\A'$, $\safeSigAut{y}{q'}{\A'} = \safeSigAut{y}{q'}{\A}$. Therefore, the preorders at even levels $\leqSig{y}$ correspond to the inclusion of safe languages in $\A'$, as they do in $\A$.

Item <ref>. Let $q$ and $q'$ be two states in $\A'$ such that $q\eqSig{y} q'$, for $y\leq x-2$ even, and let $q\re{a:y'}p$ for $y'\leq y$ and $q'\re{a:z}p'$.
As $\A'$ is a "nice transformation", $y'=z$.
If the first of these transitions is not a "redirected@@safec" one, then, by "strong congruence" of ${\leq}(x-2)$-priorities in $\A$, neither is the second one, and $p=p'$.
Assume that these transitions have been "redirected@@safec" from, $q\re{a:y'}p_1$ and $q'\re{a:y'}p'_1$. Then, as Item <ref> is satisfied in $\A$, $p_1=p'_1$, so $p=\pick(p_1)=\pick(p_1')=p'$.

Item <ref>. Directly follows from Lemma <ref> and the fact that $\A$ satisfies this property.

Item <ref>. Follows from the fact that if $q\neqSig{y-1}p$ in $\A'$, then $q\neqSig{y-1}p$ in $\A$; and the equality $\safeSigAut{y}{q}{\A'} = \safeSigAut{y}{q}{\A}$.

Obtaining Lemma <ref>.

We have all the necessary elements to deduce Lemma <ref>. Using Lemma <ref>, we can decide whether $\A$ contains a "redundant@@safec" "$({<}x)$-safe component" in polynomial time.
If it contains none, $\A$ is already "$({<}x)$-safe centralised".
While we can find "redundant@@safec" safe components, we remove them applying the transformation described above. This transformation can clearly be done in polynomial time, and by Lemmas <ref> and <ref>, the obtained automaton "recognises" the correct language and preserves all the hypothesis assumed in the induction.

§.§.§ Existence of uniform words and synchronising separating runs

We now provide proofs for Lemmas <ref> and <ref>.
In Section <ref>, we derived totality of the order $\leqSig{x}$ in each $\eqSig{x-1}$-component from these lemmas (c.f. Lemma <ref>).

In all the subsection we assume that $x$ is an even priority and $\A$ is a "$(x-2)$-structured signature automaton" with initial state $q_\init$ that is moreover:

* "deterministic over" transitions with "priority" different from $x-1$,

* "homogeneous",

* "history-deterministic", and

* "$({<}x)$-safe centralised".

Words producing priority $x$ uniformly.

The fact that for such paths we must have $p_1\eqSig{x}p_2$ follows from the monotonicity of "safe languages@@sig" (Lemma <ref>) and the fact that $({\geq}x)$-transitions preserve $\eqSig{x-1}$-classes.

We let $\{q_1,q_2,\dots,q_k\}$ be an enumeration of the states of $\classSig{x}{q}$.
For each $q_i\in \classSig{x}{q}$ there is a word $u_i\in \SS^*$ such that $q_i\lrp{u_i:x}q_i$.

Since $q_i$ and $q$ are in the same "$({<}x)$-safe component", there is a word $u_i'$ such that $q_i\lrp{u_i':\geq x} q$. By "normality", there is a word $u_i''$ such that $q\lrp{u_i'':x}q_i$. We just take $u_i = u_i'u_i''$.

We will  define $k$ finite words $w_1,w_2\dots, w_k\in \SS^*$ satisfying:

* For $q'\in \classSig{x}{q}$ and for every $i\leq k$, $q' \lrp{w_1w_2\dots w_{i}:\geq x} \classSig{x}{q}$.

* $q_j \lrp{w_1w_2\dots w_{i}: x} \classSig{x}{q}$ for every $j\leq i$.

In order to obtain these properties, we just define recursively $w_1=u_1$ and $w_i =u_j$, for $u_j$ as given by the previous claim,  if:

\[  q_i \lrp{w_1w_2\dots w_{i-1}:\geq x} q_j.\]

Finally, we let $w=w_1w_2\dots w_kw$, which first produces priority $x$ when read from any state of $\classSig{x}{q}$, and then goes to the $\eqSig{x}$-class of $p$ producing priorities ${\geq}x$.

Resolvers implemented by finite memories.

For the upcoming proofs, we need to introduced the notion of memories for "resolvers".
Let $\A = (Q,\Sigma, q_\init, \DD, \colAut)$ be a "non-deterministic automaton". A ""memory structure@@aut"" for $\A$ is a tuple $(M,m_\init,\intro*\transMem,\nextmoveResolver)$, where $M$ is a set of memory states, $m_\init\in M$ is an initial state, $\transMem: M \times \DD \to M$ is an ""update function@@mem"" and $\intro*\nextmoveResolver\colon Q\times M \times \SS \to \DD$.
It ""implements@@resolver"" a "resolver@@aut" $\resolv$ if  for all $a\in \SS$, $\resolv(\ee,a) = \nextmoveResolver(q_\init,m_\init,a)$ and for all $\rr\in \DD^+$ ending in $p$, $\resolv(\rr,a) = \nextmoveResolver(p, \transMem(m_\init, \rr), a)$.

Every "history-deterministic@@aut" "$\ee$-completion" admits a "sound resolver@@aut" "implemented by@@resolver" a "finite memory structure@@resolv".