11institutetext: Max Planck Institute for Software Systems (MPI-SWS),
Kaiserslautern 11email<EMAIL_ADDRESS>
22institutetext: Department of Computer Science, University of Warwick, UK
33institutetext: Institute of Science and Technology ,Austria
33email<EMAIL_ADDRESS>
# Rabin Games and Colourful Universal Trees††thanks: This work is a part of
the project VAMOS that has received funding from the European Research Council
(ERC) under the European Union’s Horizon 2020 research and innovation
programme, grant agreements No 101020093. Rupak Majumdar was partially
supported by the DFG project 389792660 TRR 248—CPEC.††thanks: The full version
of the paper [25] is available on arXiv at http://arxiv.org/abs/2401.07548

Rupak Majumdar 11 0000-0003-2136-0542 Irmak Sağlam 11 K. S. Thejaswini 2233
0000-0001-6077-7514

###### Abstract

We provide an algorithm to solve Rabin and Streett games over graphs with $n$
vertices, $m$ edges, and $k$ colours that runs in
$\tilde{O}\left(mn(k!)^{1+o(1)}\right)$ time and $O(nk\log k\log n)$ space,
where $\tilde{O}$ hides poly-logarithmic factors. Our algorithm is an
improvement by a super quadratic dependence on $k!$ from the currently best
known run time of $O\left(mn^{2}(k!)^{2+o(1)}\right)$, obtained by converting
a Rabin game into a parity game, while simultaneously improving its
exponential space requirement.

Our main technical ingredient is a characterisation of progress measures for
Rabin games using _colourful trees_ and a combinatorial construction of
succinctly-represented, _universal_ colourful trees. Colourful universal trees
are generalisations of universal trees used by Jurdziński and Lazić (2017) to
solve parity games, as well as of Rabin progress measures of Klarlund and
Kozen (1991). Our algorithm for Rabin games is a progress measure lifting
algorithm where the lifting is performed on succinct, colourful, universal
trees.

###### Keywords:

Rabin gamesParity gamesColourful trees

##  1 Introduction

A _Rabin game_ is a two-player infinite-duration game played on a directed,
coloured graph, where each vertex has a finite set of _good_ colours and a
finite set of _bad_ colours associated with it [29]. The two players
Controller and Environment take turns to move a token along an edge to form a
_play_ , an infinite path in the graph. Such a play is winning for Controller
if there is a colour that is a good colour for some vertex seen infinitely
often along the path and is not a bad colour for any vertex seen infinitely
often. Rabin games lie at the core of reactive synthesis for omega-regular
specifications and efficient algorithms for Rabin games are of practical
interest in synthesis tools.

Rabin automata already appear in McNaughton’s solution of Church’s synthesis
problem [4, 26] and in Rabin’s proof of the decidability of SnS [29], where it
was first defined in the setting of infinite trees. To solve Church’s
synthesis problem for $\omega$-regular specifications, represented by non-
deterministic Büchi automata, there are two well-studied (polynomial-time
equivalent) approaches: either reduce it to the emptiness problem for Rabin
tree automata or solve a Rabin game.

Rabin conditions are also suitable specifications for _general fairness
constraints_ [15]. Klarlund and Kozen [20] defined Rabin measures over graphs
and applied them to prove program termination under a general fairness
constraint. Indeed, the acceptance condition that defines _strong fairness_ ,
i.e., if a given set of actions (edges) is enabled infinitely often (the
source vertex is seen infinitely often), it is taken infinitely often, is
naturally expressed by the complement of the Rabin condition, called the
Streett condition [30].

Algorithmically, the problem of solving Rabin games was shown to be
$\NP$-complete by Emerson and Jutla [11, 13] in the late 1980s. In the same
paper, Emerson and Jutla, and independently, Pnueli and Rosner [28], gave an
algorithm that takes time $O\left((nk)^{3k}\right)$ time, where $n$ is the
number of vertices of the game graph and $k$ the number of colours.

Steady progress was made to solve Rabin games, and within a decade, Kupferman
and Vardi [23] reduced the cubic dependence on $n^{k}$ to a quadratic one by
giving an algorithm to check non-emptiness in a Rabin tree automata in time
$O\left(mn^{2k}k!\right)$. Later, Horn [16] gave a different solution to solve
Streett games—and therefore Rabin games—with the same running time.

A lot of progress was simultaneously made on _parity games_ [12], a special
case of Rabin games where colours are assigned to each subset of states in a
chain of subsets. Inspired by fixpoint evaluation algorithms [12] and the
small progress measure algorithm [17] of Jurdziński for parity games, Piterman
and Pnueli [27] gave a fast $O\left(mn^{k+1}kk!\right)$-time, $O(nk)$-space,
algorithm for Rabin games. This algorithm used a concept of a measure to solve
Rabin games.

The work of Piterman and Pnueli remained state-of-the-art for Rabin games
until the quasi-polynomial breakthrough for parity games by Calude, Jain,
Khoussainov, Li, and Stephan [1]. They gave a fixed parameter tractable
algorithm (FPT) for Rabin games on $k$ colours by converting it to a parity
game and using the quasi-polynomial algorithm.

A Rabin game with $n$ vertices, $m$ edges, and $k$ colours, can be reduced to
a parity game over $N=nk^{2}k!$ vertices, $M=nk^{2}k!m$ edges, and $K=2k+1$
colours [12]. By combining the reduction from Rabin to parity games and state-
of-the-art algorithms for parity games [18, 8, 14, 9] in a “space-efficient”
manner, say of Jurdziński and Lazić [18], one can solve Rabin games in time
$O\left(\max\left\\{MN^{2.38},2^{O(K\log K)}\right\\}\right)$, but exponential
space (since the parity game is exponentially bigger).

On substitution of the values of $M$ and $N$, the algorithm of Jurdziński and
Lazić would take time at least proportional to $m(nk^{2}\cdot k!)^{3.38}$ for
games with $n$ vertices, $m$ edges and $k$ colours. However, observe that the
parity game obtained from a Rabin game is such that the number of vertices
$N=nk^{2}k!$ is much larger than the number of colours $K=2k+1$. Indeed, this
results in $K\in o\left(\log(N)\right)$. For cases where the number of
vertices of the resulting parity game is much larger than the number of
priorities, say the number of colours ($2k+1$) is
$o\left(\log\left(N\right)\right)$—which is the case above as $k$
grows—Jurdziński and Lazić also give an analysis of their algorithm that would
solve Rabin games in time $O\left(nmk!^{2+o(1)}\right)$. Closely matching this
are the run times in the work of Fearnley et al. [14] who provide, among other
bounds, a quasi-bi-linear bound of
$O\left(MN\mathfrak{a}(N)^{\log{\log{N}}}\right)$, where $\mathfrak{a}$ is the
inverse-Ackermann function. In either case above, this best-known algorithm
has at least a $(k!)^{2+o(1)}$ dependence in its run time, and takes space
proportional to $(nk^{2}k!)\log(nk^{2}k!)$, which has a $k!$ dependence again.

### Our Contribution.

Our result breaks through the $2+o(1)$ barrier, while simultaneously using
polynomial space, to give a fixed-parameter tractable algorithm for Rabin
games. We show a new algorithm for Rabin games on graphs that runs in time
$\tilde{O}(mn(k!)^{1+o(1)})$ time and $O(nk\log k\log n)$ space, for a game on
$n$ vertices, $m$ edges, and $k$ colours. Our algorithm improves the quadratic
$(k!)^{2}$ dependence in the number of colours in the best current algorithms,
while simultaneously using only polynomial space.

Our first technical contribution is a characterisation of winning states in
Rabin games using “ _colourful trees_ ”, by generalizing previous work on
Rabin measures on graphs by Klarlund and Kozen [20]. Using our
characterisation, we provide an algorithm to compute winning states and
strategies as a fixed point of a lifting function over the lattice of
functions from vertices of a game to nodes of a colourful tree.

Our second contribution is the construction of a _universal_ colourful tree
that embeds any colourful tree with a given number of leaves and fixed set of
colours. Universal trees are found underlying all the quasi-polynomial
algorithms for parity games [18, 6, 19, 8, 21]. Our construction uses the
theory of universal trees developed for parity games, especially that of
Jurdziński and Lazić [18]. From our construction of universal colourful trees,
we can also naturally construct an instance of universal graphs for Rabin
objectives, where the definition of universal graph is as introduced by
Colcombet and Fijalkow. Although constructing universal graphs directly give
us a lifting algorithm, for the sake of completeness, we also provide a
lifting algorithm that uses our construction of colourful universal trees.
Therefore, we show how to construct a small universal colourful tree (our
upper bound is tight up to a polynomial factor) that can be succinctly encoded
and efficiently navigated.

By applying the lifting algorithm to our succinct universal colourful tree, we
get our time and space bounds.

Just as Piterman and Pnueli’s result generalized ranking techniques and
progress measures for parity games, we generalize the notion of measures [20]
and universal trees [18] central to the fastest algorithms for parity games to
obtain our algorithm.

##  2 Preliminaries

We use $\mathbb{N}$ to denote the set of all natural numbers
$\\{0,1,2,\dots\\}$. A directed graph consists of a finite set of vertices $V$
along with a binary relation $E$ over the set of vertices called the _edge
set_. We write $u\rightarrow v$ to denote an edge $(u,v)\in E$. A finite
(resp. infinite) _path_ in a directed graph is a finite (resp. infinite)
sequence of vertices such that a tuple formed by any two consecutive vertices
in this sequence is an edge in $E$.

###  $(c_{0},C)$-Colourful Ordered Trees.

Let $C$ be a finite set of colours and let $c_{0}\notin C$ be a distinguished
_root colour_. Informally, a $(c_{0},C)$-colourful ordered tree with root
colour $c_{0}$ is an ordered tree of height at most $|C|+1$ whose root is
associated with the colour $c_{0}\notin C$, and whose every other node has a
colour from $C$ associated to it. As an exception, we allow some leaves to be
left uncoloured, denoted by a “dummy colour” $\bot\notin C$. We also require
that along any path from the root to a leaf, each node must have a different
colour.

Formally, for a finite set $C$, we recursively define $(c_{0},C)$-colourful
trees

  * •

if $C=\emptyset$, $(c_{0},\left\langle\right\rangle)$ and
$\left(c_{0},\left\langle\left(\bot,\left\langle\right\rangle\right),\dots,\left(\bot,\left\langle\right\rangle\right)\right\rangle\right)$
are $(c_{0},\emptyset)$-colourful trees.

  * •

if $C\neq\emptyset$, we say $\mathcal{T}$ is $(c_{0},C)$-colourful tree if it
is either

    * –

a $(c_{0},C^{\prime})$-colourful tree rooted at $c_{0}$ for some
$C^{\prime}\subsetneq C$; or

    * –

$\mathcal{T}=\left(c_{0},\left\langle\mathcal{T}_{1},\dots,\mathcal{T}_{\ell}\right\rangle\right)$,
and for all $i\in\left\\{\,1,\ldots,\ell\,\right\\}$, either there is a
$c_{i}\in C$ and $\mathcal{T}_{i}$ is a
$(c_{i},C\setminus\\{c_{i}\\})$-colourful ordered tree, or
$\mathcal{T}_{i}=(\bot,\left\langle\right\rangle)$. Note that these $c_{i}$
need not be different from one another.

We define the _concatenation_ of a $(c_{0},C_{1})$-colourful tree
$\mathcal{T}_{1}=\left(c_{0},\left\langle\mathcal{T}^{1}_{1},\dots,\mathcal{T}^{m}_{1}\right\rangle\right)$
and a $(c_{0},C_{2})$-colourful tree
$\mathcal{T}_{2}=\left(c_{0},\left\langle\mathcal{T}^{1}_{2},\dots,\mathcal{T}^{\ell}_{2}\right\rangle\right)$
as the $(c_{0},C_{1}\cup C_{2})$-colourful tree denoted by
$\mathcal{T}_{1}\cdot\mathcal{T}_{2}$ as
$\left(c_{0},\left\langle\mathcal{T}^{1}_{1},\dots,\mathcal{T}^{m}_{1},\mathcal{T}^{1}_{2},\dots,\mathcal{T}^{\ell}_{2}\right\rangle\right)$.
For a root colour $c_{0}$, a number $\ell\in\mathbb{N}$, and a
$(c,C)$-colourful ordered tree $\mathcal{T}$, we denote $\mathcal{T}^{\ell}$
to be the tree with $\ell$ many copies of $\mathcal{T}$,
$\left(c_{0},\left\langle\mathcal{T},\mathcal{T},\dots,\mathcal{T}\right\rangle\right)$.
When $(c_{0},C)$ is clear from context, we simply say “colourful tree.”

### Embedding Colourful Trees.

Given a $(c_{0},C)$-colourful tree $\mathcal{U}$ and a
$(c_{0},C^{\prime})$-colourful tree $\mathcal{T}$, such that
$C^{\prime}\subseteq C$, we say $\mathcal{U}$ _embeds_ $\mathcal{T}$ if
$\mathcal{T}=(c_{0},\left\langle\right\rangle)$, or
$\mathcal{T}=\left(c_{0},\left\langle\mathcal{T}_{1},\dots,\mathcal{T}_{\ell}\right\rangle\right)$
and
$\mathcal{U}=\left(c_{0},\left\langle\mathcal{U}_{1},\dots,\mathcal{U}_{m}\right\rangle\right)$
for some $\ell,m$, and there is some increasing sequence of indices $1\leq
i_{1}<i_{2}<\dots<i_{\ell}\leq m$ such that $\mathcal{U}_{i_{j}}$ embeds
$\mathcal{T}_{j}$ recursively. Notice both $\mathcal{U}_{i_{j}}$ and
$\mathcal{T}_{j}$ must be rooted at the same colour, say $c_{j}$ and both are
$\left(c_{j},C\setminus\\{c_{j}\\}\right)$-colourful and
$\left(c_{j},C^{\prime}\setminus\\{c_{j}\\}\right)$-colourful trees
respectively.

### Labelled Colourful Trees.

In what follows, we shall additionally label colourful trees with labels from
some linearly ordered set. It is more convenient to define such labelled
colourful trees as prefix-closed sets of sequences, using the isomorphism
between a (recursively defined) tree and its set of paths.

Let $\mathbb{L}$ be a set of labels with a linear ordering
$<_{\mathbb{L}}\subseteq\mathbb{L}\times\mathbb{L}$. An $\mathbb{L}$-labelled
$(c_{0},C)$-colourful tree is a prefix-closed set of sequences over
$\mathbb{L}\times(C\cup\\{\bot\\})$ where $\mathbb{L}\times(C\cup\\{\bot\\})$
is the Cartesian product of $\mathbb{L}$ and $(C\cup\\{\bot\\})$.

Given an element $\tau_{0}\in\mathbb{L}\times(C\cup\\{\bot\\})$ and a sequence
$\left(\tau_{1},\tau_{2},\dots,\tau_{j}\right)$ in
$\left(\mathbb{L}\times(C\cup\\{\bot\\})\right)^{*}$, we use $\odot$ to denote
concatenation to the tuple, where we say
$\tau_{0}\odot\left(\tau_{1},\tau_{2},\dots\tau_{j}\right)\>=(\tau_{0},\tau_{1},\tau_{2},\dots\tau_{j})$.
We extend this notation to sets of sequences $\mathcal{L}$, by also defining
$\tau_{0}\odot\mathcal{L}=\left\\{\,(\tau_{0},\tau_{1},\tau_{2},\dots\tau_{j})\mid(\tau_{1},\tau_{2},\dots\tau_{j})\in\mathcal{L}\,\right\\}$.

We say a prefix-closed set
$\mathcal{L}\subseteq(\mathbb{L}\times(C\cup\left\\{\,\bot\,\right\\}))^{*}$
is an $\mathbb{L}$-labelling of a $(c_{0},C)$-colourful ordered tree
$\mathcal{T}$

  * •

if
$\mathcal{T}=\left(c_{0},\left\langle\left(\bot,\left\langle\right\rangle\right)^{m}\right\rangle\right)$,
and $\mathcal{L}$ is the prefix closure of the set
$\left\\{\,(\alpha_{1},\bot),\dots,(\alpha_{m},\bot)\,\right\\}$ for some
$\alpha_{1}<_{\mathbb{L}}\alpha_{2}<_{\mathbb{L}}\dots<_{\mathbb{L}}\alpha_{m}\in\mathbb{L}$,

  * •

if
$\mathcal{T}=\left(c_{0},\left\langle\mathcal{T}_{1},\dots,\mathcal{T}_{m}\right\rangle\right)$
then $\mathcal{L}$ is the prefix closure of the set

$(\alpha_{1},c_{1})\odot\mathcal{L}_{1}\cup(\alpha_{2},c_{2})\odot\mathcal{L}_{2}\cup\dots\cup(\alpha_{m},c_{m})\odot\mathcal{L}_{m}$

for some
$\alpha_{1}\leq_{\mathbb{L}}\alpha_{2}\leq_{\mathbb{L}}\dots\leq_{\mathbb{L}}\alpha_{m}$
in $\mathbb{L}$, such that for all $j$,

    * –

$\mathcal{T}_{j}$ is a $C\setminus\\{c_{j}\\}$-colourful tree rooted at
$c_{j}$ and $\mathcal{L}_{j}$ is an $\mathbb{L}$-labeling of
$\mathcal{T}_{j}$,

    * –

$c_{j}\in C\cup\\{\bot\\}$, and

    * –

whenever $\alpha_{j}=\alpha_{j+1}$, we have $c_{j}\neq c_{j+1}$

Note that the root colour $c_{0}$ of $\mathcal{T}$ does not appear in
$\mathcal{L}$; instead of tracking $c_{0}$ along with $\mathcal{L}$
explicitly, we implicitly assume the root colour of the tree $\mathcal{L}$
above is $c_{0}$.

We refer to elements of the prefix-closed set $\mathcal{L}$ of a labelled tree
as _nodes_ of the tree. For two nodes $n_{1}$ and $n_{2}$ in $\mathcal{L}$, we
define _the greatest common ancestor_ , written $\mathsf{GCA}(n_{1},n_{2})$,
as the longest common prefix of $n_{1}$ and $n_{2}$. We define $n_{1}$ to be
an _ancestor_ of $n_{2}$ if $n_{1}=\mathsf{GCA}(n_{1},n_{2})$. In particular,
$n_{1}$ is a parent of $n_{2}$, written $n_{1}=\mathrm{parent}(n_{2})$, if
$n_{1}$ is the largest node other than $n_{2}$ such that
$n_{1}=\mathsf{GCA}(n_{1},n_{2})$; we then say $n_{2}$ is a child of $n_{1}$.

The colouring of a node is defined to be the last colour occurring in the
sequence: For the empty sequence $\left(\right)$, we define
$\mathsf{colour}(\left(\right))=c_{0}$, and
$\mathsf{colour}((\alpha_{1},c_{i_{1}}),\dots,(\alpha_{j},c_{i_{j}}))=c_{i_{j}}$.
Furthermore we define $\mathsf{ColourSet}:\mathcal{L}\rightarrow
2^{C\cup\left\\{\,c_{0}\,\right\\}}$, which maps a node to the set of colours
seen from the root to that node:
$\mathsf{ColourSet}(n)=\left\\{\,\mathsf{colour}(n^{\prime})\mid
n^{\prime}=\mathsf{GCA}(n^{\prime},n)\,\right\\}\setminus\left\\{\,\bot\,\right\\}$.

### Ordering.

We define an ordering $\prec_{\mathcal{L}}$ on $\mathcal{L}$. First, we fix
some arbitrary linear order on the set $C$ and set colour $\bot$ to be larger
than all the colours in $C$ in the ordering. We compare elements by extending
the linear order $<_{\mathbb{L}}$ over $\mathbb{L}$ and an arbitrary fixed
order $<$ over $C$ to a linear order over the set
$\mathbb{L}\times(C\cup\\{\bot\\})$ lexicographically as follows: for two
elements in $\mathbb{L}\times(C\cup\\{\bot\\})$, we declare
$(\alpha_{1},c_{1})<(\alpha_{2},c_{2})$ if either
$\alpha_{1}<_{\mathbb{L}}\alpha_{2}$ or $\alpha_{1}=\alpha_{2}$ and
$c_{1}<c_{2}$.

For two nodes $n_{1},n_{2}\in\mathcal{L}$, we define
$n_{1}\prec_{\mathcal{L}}n_{2}$ if either $n_{1}$ is a strict prefix of
$n_{2}$, or if $n_{1}$ is lexicographically smaller than $n_{2}$ when viewed
as sequences over $\mathbb{L}\times(C\cup\left\\{\,\bot\,\right\\})$.

###### Example 1

Figure 1 depicts a $(\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\left\\{\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\right\\})$-colourful
tree, where the nodes denoted by  represents uncoloured nodes. A fixed
ordering on the set of colours $\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}<\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}<\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}<\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$, a labelling of this
tree over $\mathbb{L}=\\{1,2\\}\subseteq\mathbb{N}$ is the prefix closure of
the set $\\{(1\,\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$,
$(1\,\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},2\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$,
$(1\,\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},2\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},2\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$,
$(1\,\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$,
$(1\,\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},2\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},2\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$,
$(1\,\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$,
$(2\,\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},2\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$,
$(2\,\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$,
$(2\,\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},2\,\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})\\}$. The ordering
$\prec_{\mathcal{L}}$, (represented by $\prec$) on some nodes is as follows:
$()\prec(1\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})\prec(1\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},1\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})\prec(1\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})\prec(2\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},2\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$. The ordering in
the nodes of the tree in the figure decreases when we go from a child to a
parent, or we go “left” in the tree, but otherwise increases.

$1$$1$$1$$1$$1$$2$$1$$2$$2$$2$$1$$2$$2$$2$$2$$1$$1$$2$ Figure 1: A colourful
tree.

Figure 2: A colourful Rabin graph $\mathcal{G}$ where all infinite paths
satisfy the Rabin condition

##  3 Rabin measure and Colourful Decompositions

In this section, our aim is to understand the Rabin acceptance condition on
graphs. We define such acceptance conditions and provide a local witness
called a _Rabin measure_ for graphs where all paths satisfy the Rabin
condition.

A $(c_{0},C)$-colourful _Rabin graph_ $\mathcal{G}$ consists of (1) a directed
graph $(V,E)$, (2) a finite set $C$ of _colours_ and a special colour
$c_{0}\notin C$, and (3) for each vertex $v\in V$, a set of _good_ colours
$G_{v}\subseteq C\cup\left\\{\,c_{0}\,\right\\}$ for $v$ and a set of _bad_
colours $B_{v}\subseteq C$ for $v$. Observe that $c_{0}\notin B_{v}$ for any
$v$. We call each colour $c$ in $G_{v}$ a _good_ colour for $v$, and each
colour in $B_{v}$ a _bad_ colour for $v$.

We assume every vertex has some outgoing edge in the directed graph. An
infinite path in $\mathcal{G}$ satisfies the _Rabin condition_ if there is
some colour $c$ in $C\cup\\{c_{0}\\}$ such that $c$ is a good colour for some
$v$ seen infinitely often along the path and $c$ is not a bad colour for any
$v$ seen infinitely often along the path.

###### Example 2

Consider the $(\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\\{\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\})$-colourful Rabin
game in Fig. 2. The colours that are in the good set of each vertex are
represented with a smiley face in the same colour and those that are bad
colours appear with a sad face. Although a vertex can have more than one
colour assigned to it as a good colour (or a bad colour), we only consider at
most one good and bad colour per vertex for this example. In our example, the
leftmost vertex in the graph $\mathcal{G}$ in Fig. 2 has the singleton set
$\\{\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\}$ as the set of
good colours and the set $\\{\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\}$ as the set of bad
colours. Similarly, the topmost vertex in Fig. 2 has the set
$\\{\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\}$ as the set of
good colours and an empty set of bad colours. Observe that in the graph
$\mathcal{G}$, any infinite path satisfies the Rabin condition. Indeed, for
any infinite path there is some colour that is not a bad colour for any of the
vertices that occur infinitely often and is a good colour for some vertex that
occurs infinitely often. For example, if a path is such that all the vertices
of $\mathcal{G}$ are visited infinitely often, then the colour  is not a bad
colour of any vertex and the same colour  is a good colour of the topmost
vertex.

As opposed to preexisting definition in literature of Rabin games that use
Rabin pairs to represent the acceptance condition, we instead define two sets
of colours associated to a vertex rather than a pair of subsets of vertices
associated to a colour. This does not add more than a constant factor in terms
of representation size.

### A Measure for Rabin Graphs.

We fix a $(c_{0},C)$-colourful Rabin graph $\mathcal{G}$ with the underlying
graph $(V,E)$ with good colours for a vertex $v$ denoted by $G_{v}$ and the
bad colours denoted by $B_{v}$. Let $\mathbb{L}$ be a linearly ordered set of
labels, and let $\mathcal{L}$ be an $\mathbb{L}$ labelled $(c_{0},C)$
-coloured tree. We define
$\mathcal{L}^{\top}=\mathcal{L}\cup\left\\{\,\top\,\right\\}$ by adjoining an
element $\top$ to $\mathcal{L}$ and we extend the ordering
$\prec_{\mathcal{L}}$ (denoted henceforth by $\prec$) to $\mathcal{L}^{\top}$,
by declaring $t\prec\top$ for all $t\in\mathcal{L}$.

Consider a map $\mu:V\rightarrow\mathcal{L}^{\top}$. We call an edge
$u\rightarrow v$ _consistent_ with respect to $\mu$, if either $\mu(u)$ is
mapped to $\top$ or it satisfies the condition ($\mathsf{G}_{\succ}$ OR
$\mathsf{G}_{\downarrow}$) AND $\mathsf{B}$; for $\mathsf{G}_{\succ}$,
$\mathsf{G}_{\downarrow}$, and $\mathsf{B}$ defined below.

  * ($\mathsf{G}_{\succ}$)

$\mu(u)\succ\mu(v)$

  * ($\mathsf{G}_{\downarrow}$)

$\mathsf{GCA}(\mu(u),\mu(v))=\mu(u)$ and $\mathsf{colour}(\mu(u))\in G_{u}$.

  * ($\mathsf{B}$)

$\mathsf{ColourSet}(\mu(u))\cap B_{u}=\emptyset$

In words, $\mathsf{G}_{\succ}$ conveys that the measure $\mu$ decreases along
the edge $u\rightarrow v$ and $\mathsf{G}_{\downarrow}$ says that the measure
can increase along an edge but only into a descendent node and only when the
colour of the node that is currently mapped to is a good colour for $u$. The
condition represented by $\mathsf{B}$ says that none of the colours assigned
to any ancestor of $u$ is a bad colour for it.

If the map $\mu$ is clear from the context, we call an edge or a vertex
consistent without mentioning the mapping. We say the relation and function
$\mathsf{GCA}(\cdot,\top)$ and $\mathsf{colour}(\top)$ are undefined, and the
condition $\mathsf{G}_{\downarrow}$ or $\mathsf{B}$ are not satisfied when
$\mu(v)$ is mapped to $\top$ and $\mu(u)$ is not mapped to $\top$.

We say the map $\mu$ is a $(c_{0},C)$-colourful _Rabin measure_ for a graph
$\mathcal{G}$ if all edges in $E$ are consistent with respect to $\mu$. A
mapping from the vertices of a Rabin graph to the nodes of a tree ensures that
an infinite play corresponds to an infinite set of nodes in a tree. If a
mapping is consistent, then such a mapping serves as a witness to the fact
that an infinite path in the Rabin graph satisfies the Rabin condition.

Our definition is a modification of Klarlund and Kozen’s [20] notion of Rabin
measures, following recent approaches to faster algorithms for parity games
[18, 8].

### Colourful Decomposition.

The Rabin measure, as with other progress measures, is based exclusively on
local properties. Indeed, in the above case, we have a progress measure when
each edge satisfies certain conditions. Before we show that Rabin measures
capture winning sets of a graph, we define an intermediate structure, which we
call _colourful decompositions_. These colourful decompositions of a Rabin
graph highlight a recursive structure that captures the acceptance of all
paths in a way which relates naturally to colourful trees. Colourful
decompositions generalise attractor decompositions of parity games to Rabin
games [7, 19, 8].

Consider a $(c_{0},C)$-colourful Rabin graph $\mathcal{G}$. A
$(c_{0},C)$-colourful decomposition $\mathcal{D}$ of $\mathcal{G}$ is a
recursive sub-division of vertices $V$ of $\mathcal{G}$ into subsets of
vertices defined as follows. If $C=\emptyset$, then we say
$\mathcal{D}\,:=\,\left\langle V\right\rangle$ is a $(c_{0},C)$-colourful
decomposition if and only if all infinite paths from all vertices in $V$ visit
a vertex $v$ such that $c_{0}\in G_{v}$. Else, if $C\neq\emptyset$ and if
$|V|\geq 1$, and

$\mathcal{D}\>=\left\langle
A,\left(c_{1},V_{1},\mathcal{D}_{1},A_{1}\right),\dots,\left(c_{j},V_{j},\mathcal{D}_{j},A_{j}\right)\right\rangle$

satisfies the following conditions:

  * •

$A$ is the set of all vertices in $V$ such that all infinite paths starting
from $A$ in $\mathcal{G}$ visit some vertex $v\in V$ such that $c_{0}\in
G_{v}$;

  * •

Set $W_{1}=V\setminus A$. For $i\in 1,\dots,j$,

    * –

$V_{i}$ is a set of vertices which has no path to $W_{i}\setminus V_{i}$ and
$c_{i}\notin B_{v}$ for all $v\in V_{i}$;

    * –

$\mathcal{D}_{i}$ is a $(c_{i},C\setminus\\{c_{i}\\})$-colourful decomposition
of $V_{i}$.

    * –

$A_{i}$ is the set of all vertices in $W_{i}$ such that all infinite paths
from $A_{i}$ within $W_{i}$ visits some vertex in $V_{i}$;

    * –

$W_{i+1}\>=W_{i}\setminus A_{i}$.

  * •

$W_{j+1}=\emptyset$.

(a) A colourful decomposition of a Rabin graph $\mathcal{G}$ where all paths
satisfy the Rabin condition

$0$$1$$0$$2$$2$$1$$1$ (b) A labelled colourful tree into which the graph
$\mathcal{G}$ has a Rabin measure.

Figure 3: A colourful decomposition and tree for Rabin measure

The crux of this section is Theorem 3.1 below which shows the equivalence
between Rabin measure, the existence of a colourful decomposition and a Rabin
graph where all paths satisfy the Rabin condition.

######  Theorem 3.1 ()

The following three statements are equivalent for a $(c_{0},C)$-colourful
Rabin graph $\mathcal{G}$.

  1. 1.

All infinite paths in $\mathcal{G}$ satisfy the Rabin condition.

  2. 2.

There is a $(c_{0},C)$-colourful decomposition $\mathcal{D}$ of the vertices
of $\mathcal{G}$.

  3. 3.

There is an $\mathbb{L}$-labelled $(c_{0},C)$-colourful Rabin measure for
$\mathcal{G}$, where no vertex is mapped to $\top$ for some linearly ordered
infinite set $\mathbb{L}$.

The theorem above is proved by showing 1$\implies$2 in Lemma 4, 2$\implies$3
in Lemma 5 and finally 3$\implies$1 in Lemma 6.

### Proof Sketch 1$\implies$2.

If $C$ is empty, then the decomposition is $\mathcal{D}=\left\langle
V\right\rangle$ for a $(c_{0},\emptyset)$-colourful graph where all paths
satisfy the Rabin condition. If $C$ is not empty, we first remove all vertices
$A$ from $\mathcal{G}$ that can visit a vertex for which $c_{0}$ is a good
colour. In the SCC decomposition of the graph induced by $V\setminus A$, each
infinite path satisfies the Rabin condition, and therefore especially the
infinite path which consists of all the vertices of some bottom SCC, $V_{1}$.
Hence, there must be one colour $c$ that is not a bad colour for any vertex
and is a good colour for at least some of the vertices $V_{1}$. One can
therefore inductively construct a $(c,C\setminus\\{c\\})$-colourful
decomposition $\mathcal{D}_{1}$ for the vertices of $V_{1}$. Later, in the
graph $\mathcal{G}$ without the vertices of $A$ and $V_{1}$ and all vertices
$A_{1}$ from which all paths lead to $V_{1}$, we again get an other graph
where all infinite paths satisfy the Rabin condition. This graph, again by
induction has a $(c_{0},C)$-colourful Rabin decomposition
$\mathcal{D}^{\prime}$. We finally ‘glue’ together $\left\langle
A,(c,V_{1},\mathcal{D}_{1},A_{1})\right\rangle$ and $\mathcal{D}^{\prime}$
obtained above.

### Proof Sketch 2$\implies$3.

The proof follows a recursive construction of an $\mathbb{L}$-labelled
$(c_{0},C)$-colourful tree where the recursion is based on the structure of
the decomposition. An example of how such a mapping to a tree is obtained from
a picture is exemplified in Fig. 3. The decomposition $\mathcal{D}$ of the
game $\mathcal{G}$ is $\left(A,(\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},V_{1},\mathcal{D}_{1},A_{1}),(\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},V_{2},\mathcal{D}_{2},A_{2})\right)$.
Some of the sets of the decomposition are indicated in Fig. 3(a). The measure
obtained from the decomposition into the given tree is intuitive. For example,
the measure obtained from the given decomposition of the game $\mathcal{G}$ is
such that the vertex for which the colour  is a good colour is mapped to the
root of the tree. Similarly, this measure maps the vertex in $V_{1}$ for which
the colour  is a good colour to the node $1\leavevmode\hbox to4.71pt{\vbox
to4.71pt{\pgfpicture\makeatletter\hbox{\hskip 2.35277pt\lower-2.35277pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$ in the tree. The
only vertex in $A_{2}\setminus V_{2}$ is mapped to the node $2\leavevmode\hbox
to4.71pt{\vbox to4.71pt{\pgfpicture\makeatletter\hbox{\hskip
2.35277pt\lower-2.35277pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{}\pgfsys@moveto{2.15277pt}{0.0pt}\pgfsys@curveto{2.15277pt}{1.18895pt}{1.18895pt}{2.15277pt}{0.0pt}{2.15277pt}\pgfsys@curveto{-1.18895pt}{2.15277pt}{-2.15277pt}{1.18895pt}{-2.15277pt}{0.0pt}\pgfsys@curveto{-2.15277pt}{-1.18895pt}{-1.18895pt}{-2.15277pt}{0.0pt}{-2.15277pt}\pgfsys@curveto{1.18895pt}{-2.15277pt}{2.15277pt}{-1.18895pt}{2.15277pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$.

### Proof Sketch 3$\implies$1.

If there is a Rabin measure, each edge in the infinite path satisfies
$\mathsf{B}$, as well as $\mathsf{G}_{\succ}$ or $\mathsf{G}_{\downarrow}$.
For such an infinite path, we consider the infinite sequence of nodes of the
colourful tree, obtained by taking the image of $\mu$ on the run. In this
sequence obtained, consider the smallest node of the tree $t$ that is visited
infinitely often, and let $c=\mathsf{colour}(t)$. We show that $t$ is a common
ancestor for all elements of the sequence after a finite prefix. Since all
edges satisfy $\mathsf{G}_{\succ}$ or $\mathsf{G}_{\downarrow}$, $c$ is a
colour such that $c\in G_{v}$ for some $v$ visited infinitely often. As all
edges satisfy $\mathsf{B}$, we have $c\notin B_{v}$ for all vertices $v$ in
the run after some finite prefix.

###### Remark 1

A similar statement to the equivalence of item 1 and item 2 has been proved in
the work of Klarlund and Kozen [20], however, a reader familiar with their
work might have observed some differences in the definition of a measure as
well as a colourful tree. Our definition of colourful trees is more
restrictive than theirs. For instance, colourful trees in the work of Klarlund
and Kozen have no restrictions about the colours along a path in a tree, i.e,
in their definition, the trees can have the same colour along a path, and in
fact only a partial colouring is required. However, an examination of their
proof reveals that in the direction of the proof where they construct a Rabin
measure, they inherently use a construction which produces a mapping into
colourful trees as we have defined and therefore, it is enough to only
consider such trees. We make this explicit and also prove Theorem 3.1 in the
appendix to suit our situation.

##  4 A lifting algorithm

In this section, we define Rabin game formally and first show how such Rabin
games also have a notion of a Rabin measure.

Inspired by the breakthrough algorithms to solve parity games, Colcombet,
Fijalkow, Gawrychowski, and Ohlmann [5] proposed a formalism for algorithms
that solve games where one player has a positional strategy. They showed that
if there is a special kind of graph homomorphism into a graph with a total
order on its vertices, then one can obtain a lifting algorithm for such games.
From their work [5, Theorem 3.1] combined with Theorem 5.2, we can show that
Rabin measures defined in our previous section can also be used to provide a
lifting algorithm for Rabin games. However, to make this work self-contained
and to provide an explicit space-efficient algorithm using our non-trivial
totally ordered set, we show how such lifting is performed step-by-step in
this section. We believe our following section would help future
implementation of such algorithms.

A $(c_{0},C)$-colourful _Rabin game_ $\mathfrak{G}$ consists of an _arena_
which is a $(c_{0},C)$-colourful Rabin graph $\mathcal{G}$ with vertices $V$,
a _start vertex_ $v_{0}\in V$, and a partition of $V$ into $V_{c}$ and
$V_{e}$, the vertices of two players, whom we call Controller and Environment,
respectively.

A _positional strategy_ $\sigma$ for Controller over the game graph is a
subset of edges outgoing from each of Controller’s set of vertices $V_{c}$. We
denote the graph restricted to a strategy $\sigma$ for the Controller by
$\mathcal{G}|_{\sigma}$ and it is defined as the Rabin graph over the same
vertex set with a new edge relation which contains exactly the edges in
$\sigma$ along with all the edges from all vertices belonging to Environment.

The Rabin game $\mathfrak{G}$ is _winning_ for the Controller if and only if
there exists a positional strategy $\sigma$ for the Controller where, all
infinite paths starting from $v_{0}$ in $\mathcal{G}|_{\sigma}$ satisfy the
Rabin condition. We describe an algorithm that identifies whether a Rabin game
$\mathfrak{G}$ is winning for Controller, using Rabin measures on graphs.

###### Remark 2

We only consider strategies of the Controller that are positional, but this is
enough from the results of Emerson and Jutla [13], which shows that the
Controller always has a positional winning strategy in Rabin games if there is
any winning strategy at all.

### Consistency in games.

Consider a $(c_{0},C)$-colourful Rabin game $\mathfrak{G}$. Let $\mu$ be a
function from $V$, the vertices of the game graph to an $\mathbb{L}$-labelled
$(c_{0},C)$-colourful tree $\mathcal{L}$. We simply extend the definition of
consistency from graphs to games by defining a vertex to be _consistent_ with
respect to $\mu$ in $\mathfrak{G}$ if either it belongs to the Environment and
all outgoing edges from it are consistent in $\mathcal{G}$ or if it belongs to
the Controller and there is at least one outgoing edge that is consistent in
$\mathcal{G}$. A map $\mu$ from $V$ to a $\mathcal{L}^{\top}$ is a _Rabin
measure_ for a $(c_{0},C)$-colourful Rabin game $\mathfrak{G}$ if and only if
_all_ vertices are consistent with respect to $\mu$.

### An overview of the algorithm.

We describe an algorithm that identifies whether a Rabin game $\mathfrak{G}$
is winning for Controller, using Rabin measures defined earlier for Rabin
graphs. The basic principle in the algorithm is that given a colourful tree,
the algorithm finds if there is a Rabin measure that maps vertices of the game
into nodes of that tree. The algorithm does so by starting with the smallest
map (all vertices are mapped to the root of this tree) and then at each step,
if a vertex is not consistent, increase the value of this map just at this
vertex which is not consistent. The value is modified (increased) until either
all vertices are consistent, or the value cannot be increased anymore.

Toward our goal of formally defining this algorithm, we define monotonic,
inflationary operators on the set of all maps from vertices of a game to a
tree such that the simultaneous fixpoints of these operators exactly
correspond to a Rabin measure.

Consider a Rabin measure $\mu$ which is a function mapping the vertices $V$ of
a $(c_{0},C)$-colourful Rabin game $\mathfrak{G}$ into an
$\mathbb{L}$-labelled $(c_{0},C)$-colourful tree $\mathcal{L}$. We define a
function $\mathrm{lift}_{\mu}$, which maps edges $E$ of the arena of the game
to $\mathcal{L}^{\top}$. For an edge $u\rightarrow v$ of $\mathcal{G}$, we
define $\mathrm{lift}_{\mu}(u,v)$ to be the smallest element $t$ in
$\mathcal{L}^{\top}$ such that (1) $t\succeq\mu(u)$ and (2) edge $u\rightarrow
v$ is consistent with respect to the mapping $\mu[u:=t]$, where we use the
notation $\mu[u:=t]$ to indicate the mapping $\mu^{\prime}$ where
$\mu^{\prime}(x)=\mu(x)$ if $x\neq u$ and $\mu^{\prime}(x)=t$ if $x=u$.

For each vertex $v$, we define an operator $\mathrm{Lift}_{v}$ on the lattice
of all maps from $V$ to $\mathcal{L}^{\top}$. The operator $\mathrm{Lift}_{v}$
only modifies an input map $\mu$ at $v$ and nowhere else. We define

$\mathrm{Lift}_{v}(\mu)(u)=\begin{cases}\mu(u)&\text{for }u\neq v\\\
\min_{(v,w)\in E}\left\\{\mathrm{lift}_{\mu}(v,w)\right\\}&\text{if }u=v\in
V_{c}\\\ \max_{(v,w)\in E}\left\\{\mathrm{lift}_{\mu}(v,w)\right\\}&\text{if
}u=v\in V_{e}\end{cases}$

######  Proposition 1 ()

The function $\mathrm{Lift}_{v}$ is monotonic for each $v$.

The above proposition follows from our definition of the $\mathrm{Lift}_{v}$
function. Now that we know that each $\mathrm{Lift}_{v}$ is inflationary and
monotonic. Therefore, the simultaneous least fixpoint of $\mathrm{Lift}_{v}$
on the map $\mu$, which maps all vertices to the root of $\mathcal{L}$ exists
(from the Knaster-Tarski theorem [31]). We can moreover state the following
proposition that such fixpoints correspond to the Rabin measures, which almost
follows from our definitions.

######  Proposition 2 ()

For a $(c_{0},C)$-colourful Rabin game $\mathfrak{G}$ where the vertex set is
$V$ and a fixed $\mathbb{L}$-labelled $(c_{0},C)$-colourful tree
$\mathcal{L}$,

  * •

any simultaneous fixpoint of the set of functions $\mathrm{Lift}_{v}$ for all
$v\in V$ is a Rabin measure;

  * •

any Rabin measure is a simultaneous fixpoint of $\mathrm{Lift}_{v}$ for all
$v\in V$.

Our algorithm, like any other progress-measure algorithm, computes a fixpoint
and is described as follows.

Algorithm 1 The lifting algorithm on game $(c_{0},C)$-colourful Rabin game
$\mathfrak{G}$ with vertices $V$ to tree $\mathcal{L}$

1:For each $v\in V$, $\mu(v)$ is declared to be root in $\mathcal{L}$

2:while there is some vertex $v$ that is inconsistent with respect to $\mu$.
do

3: $\mu\leftarrow\mathrm{Lift}_{v}(\mu)$.

4:end while

5:return $\mu$

The correctness follows from Propositions 1 and 2.

###### Remark 3

If there is a $(c_{0},C)$-colourful Rabin game $\mathfrak{G}$ and an
$\mathbb{L}$-labelled $(c_{0},C)$-colourful tree $\mathcal{L}^{\prime}$, such
that there is a Rabin measure $\mu^{\prime}$ from $V$ to
$\mathcal{L}^{\prime}$, and $\mathcal{L}$ embeds $\mathcal{L}^{\prime}$, then
there is also a Rabin measure $\mu$ to $\mathcal{L}$ such that all the
elements that are not mapped to $\top$ by $\mu^{\prime}$ are still not mapped
to $\top$ by $\mu$. This map is obtained by composing $\mu^{\prime}$ with the
embedding of $\mathcal{L}^{\prime}$ into $\mathcal{L}$.

### Runtime.

For a finer analysis of the runtime, we need to understand the size of the
lattice where the lifting algorithm takes place. In this section however, we
restrict ourselves to analysing the runtime of our algorithm for a fixed
$\mathcal{L}$. We write $|\mathcal{L}|$ to represent the number of nodes in
the labelled tree $\mathcal{L}$. We write $n$ to denote the number of vertices
in a Rabin game, $m$ to denote the number of edges, and
$k=|C\cup\left\\{\,c_{0}\,\right\\}|$ to denote the number of colours.

######  Lemma 1 ()

Given a mapping from the vertices of a $(c_{0},C)$-colourful Rabin game
$\mathfrak{G}$ to an $\mathbb{L}$-labelled $(c_{0},C)$-colourful tree
$\mathcal{L}$, the value of $\mathrm{Lift}_{v}(\mu)(v)$ can be computed in
time $O\left(\deg(v)\cdot T_{\mathsf{next}}\right)$, where $\deg(v)$ is the
degree (number of outgoing edges) of $v$ and $T_{\mathsf{next}}$ is defined as
the maximum of the time taken to

  * •

make a linear pass on a node in $\mathcal{L}$ (assuming the node is
represented by a sequence of elements of $\mathbb{L}\times C$),

  * •

compute the next node in $\mathcal{L}$, and

  * •

find the next node that uses colours only from $C^{\prime}\cup\\{\bot\\}$ for
a given node $t\in\mathcal{L}$ and subset of colours $C^{\prime}\subseteq C$
such that $\mathsf{colour}(t)\in C^{\prime}$.

The proof of the above lemma reduces to arguing carefully by analysing cases,
that using these above subroutines, we can find the node larger than
$\mathrm{Lift}_{v}(\mu)(v)$ in the given tree that satisfies the conditions
$\mathsf{B}$ along with at least one of $\mathsf{G}_{\succ}$ or
$\mathsf{G}_{\downarrow}$.

First, we observe that performing $\mathrm{Lift}_{v}$ on the mapping strictly
increases the mapping for a vertex that is not consistent. Each operation of
$\mathrm{Lift}_{v}$ also calls at most $\deg(v)$ many calls of
$\mathrm{lift}_{\mu}(v,u)$ for some edge $v\rightarrow u$. Suppose each
operation $\mathrm{lift}_{\mu}(v)$ takes time $T_{\mathsf{next}}$, to find the
value of $\mathrm{Lift}_{v}(\mu)(v)$ takes time at most $\deg(v)\cdot
T_{\mathsf{next}}$. Since each non-trivial application of $\mathrm{Lift}_{v}$
strictly increases the value that $v$ is mapped to, it can be called at most
as many times as the number of nodes in tree $\mathcal{L}$, this ensures that
the time taken is

$\sum_{v\in V}\mathrm{deg}(v)|\mathcal{L}|\left(T_{\mathsf{next}}\right)\in
O\left(m|\mathcal{L}|T_{\mathsf{next}}\right)$

where $m$ denotes the number of edges. We finally conclude this section with
the following theorem, which follows from Lemma 1.

######  Theorem 4.1 ()

For a $(c_{0},C)$-colourful Rabin game $\mathfrak{G}$ with $n$ vertices and
$m$ edges, and an $\mathbb{L}$-labelled $(c_{0},C)$-colourful tree
$\mathcal{L}$, Algorithm 1 on $(\mathfrak{G},\mathcal{L})$ returns the
smallest Rabin measure to $\mathcal{L}^{\top}$ in time
$O\left(m|\mathcal{L}|T_{\mathsf{next}}\right)$ where $T_{\mathsf{next}}$ is
as defined in Lemma 1 and $|\mathcal{L}|$ denotes the number of nodes in
$\mathcal{L}$.

##  5 Small Colourful Universal Trees

In the previous section, we concluded that our algorithm identifies correctly
the smallest Rabin measure into a fixed labelled colourful tree $\mathcal{L}$.
However, from Theorem 3.1, _there exists_ a Rabin measure into an
$\mathbb{L}$-labelled $(c_{0},C)$-colourful tree $\mathcal{L}$ with at most
$n$ leaves. Observe that we only need to consider $n$ leaves of $\mathcal{L}$
which correspond exactly to the image of the Rabin measure. Therefore, for a
Rabin game, there is a Rabin measure into $\mathcal{L}^{\top}$ where all start
vertices from which the game is winning for Controller are not mapped to
$\top$. In order for the algorithm to successfully determine the winner of all
$(c_{0},C)$-colourful Rabin games with $n$ vertices, we need to ensure that
the tree $\mathcal{L}$ used in Algorithm 1 would be able to embed all
$(c_{0},C)$-colourful trees with $n$ leaves. Since the runtime is linearly
dependent on the tree size, smaller trees that satisfy the above property are
desirable.

We now show that we can obtain colourful _universal_ trees, i.e., colourful
trees that are large enough to embed _any_ $(c_{0},C)$-colourful $\mathcal{L}$
with $n$-nodes. We also modify the technique of succinct universal trees of
Jurdziński and Lazić [18] to encode each node of these colourful universal
trees using polynomial space, which helps navigate these labelled colourful
trees efficiently.

### Colourful universal trees.

A $(c_{0},C)$-colourful tree $\mathcal{U}$ is _$n$ -universal_, if it embeds
_any_ $(c_{0},C)$-colourful tree $\mathcal{T}$ with at most $n$ leaves. We
henceforth assume that the set $C$ consists exactly of the colours
$c_{1},\dots,c_{h}$, with the fixed ordering $c_{1}<c_{2}<\dots<c_{h}$ on the
colours, and use $k$ to denote $h+1$.

A näive attempt at constructing an $n$-universal $(c_{0},C)$-colourful tree
could be to take all possible $(c_{0},C)$-colourful trees with at most $n$
leaves with the root colour $c_{0}$ and concatenate them. Clearly, such an
$n$-universal $(c_{0},C)$-colourful tree can be created as there are only
finitely many such trees up to isomorphism (for a fixed $C$ and $n$). But of
course, this tree is not only large, but can also be difficult to navigate. A
more tractable attempt is to construct a tree that branches $n\cdot h$ many
times at the root. The subtrees at the root that occur from this $n\cdot h$
branching have $n$ repetitions of the $h$ colours $c_{1},c_{2},\dots,c_{h}$,
in that order. Each of the children in-turn branch into $n\cdot(h-1)$ many
times similarly, thus creating a tree of size bounded by $n^{h}h!$. We claim
that indeed such a tree was exactly the one underlying the algorithm of
Piterman and Pnueli [27], which led to their $O(mn^{k+1}kk!)$ algorithm.

$\mathcal{U}^{\ell-1}_{(\leavevmode\hbox to3.41pt{\vbox
to3.41pt{\pgfpicture\makeatletter\hbox{\hskip 1.70694pt\lower-1.70694pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{0.0pt}\pgfsys@curveto{1.50694pt}{0.83226pt}{0.83226pt}{1.50694pt}{0.0pt}{1.50694pt}\pgfsys@curveto{-0.83226pt}{1.50694pt}{-1.50694pt}{0.83226pt}{-1.50694pt}{0.0pt}\pgfsys@curveto{-1.50694pt}{-0.83226pt}{-0.83226pt}{-1.50694pt}{0.0pt}{-1.50694pt}\pgfsys@curveto{0.83226pt}{-1.50694pt}{1.50694pt}{-0.83226pt}{1.50694pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\\{\leavevmode\hbox
to3.41pt{\vbox to3.41pt{\pgfpicture\makeatletter\hbox{\hskip
1.70694pt\lower-1.70694pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{0.0pt}\pgfsys@curveto{1.50694pt}{0.83226pt}{0.83226pt}{1.50694pt}{0.0pt}{1.50694pt}\pgfsys@curveto{-0.83226pt}{1.50694pt}{-1.50694pt}{0.83226pt}{-1.50694pt}{0.0pt}\pgfsys@curveto{-1.50694pt}{-0.83226pt}{-0.83226pt}{-1.50694pt}{0.0pt}{-1.50694pt}\pgfsys@curveto{0.83226pt}{-1.50694pt}{1.50694pt}{-0.83226pt}{1.50694pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\leavevmode\hbox
to3.41pt{\vbox to3.41pt{\pgfpicture\makeatletter\hbox{\hskip
1.70694pt\lower-1.70694pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\pgfsys@color@rgb@stroke{0}{0}{1}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\definecolor[named]{pgffillcolor}{rgb}{0,0,1}\pgfsys@color@rgb@fill{0}{0}{1}\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{0.0pt}\pgfsys@curveto{1.50694pt}{0.83226pt}{0.83226pt}{1.50694pt}{0.0pt}{1.50694pt}\pgfsys@curveto{-0.83226pt}{1.50694pt}{-1.50694pt}{0.83226pt}{-1.50694pt}{0.0pt}\pgfsys@curveto{-1.50694pt}{-0.83226pt}{-0.83226pt}{-1.50694pt}{0.0pt}{-1.50694pt}\pgfsys@curveto{0.83226pt}{-1.50694pt}{1.50694pt}{-0.83226pt}{1.50694pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\leavevmode\hbox
to3.41pt{\vbox to3.41pt{\pgfpicture\makeatletter\hbox{\hskip
1.70694pt\lower-1.70694pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,1,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,1,0}\pgfsys@color@cmyk@stroke{0}{0}{1}{0}\pgfsys@invoke{
}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\definecolor[named]{pgffillcolor}{rgb}{1,1,0}\pgfsys@color@cmyk@fill{0}{0}{1}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{0.0pt}\pgfsys@curveto{1.50694pt}{0.83226pt}{0.83226pt}{1.50694pt}{0.0pt}{1.50694pt}\pgfsys@curveto{-0.83226pt}{1.50694pt}{-1.50694pt}{0.83226pt}{-1.50694pt}{0.0pt}\pgfsys@curveto{-1.50694pt}{-0.83226pt}{-0.83226pt}{-1.50694pt}{0.0pt}{-1.50694pt}\pgfsys@curveto{0.83226pt}{-1.50694pt}{1.50694pt}{-0.83226pt}{1.50694pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\\})}$$\mathcal{U}^{\ell-1}_{(\leavevmode\hbox
to3.41pt{\vbox to3.41pt{\pgfpicture\makeatletter\hbox{\hskip
1.70694pt\lower-1.70694pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\definecolor[named]{pgffillcolor}{rgb}{0,0,0}\pgfsys@color@gray@fill{0}\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{0.0pt}\pgfsys@curveto{1.50694pt}{0.83226pt}{0.83226pt}{1.50694pt}{0.0pt}{1.50694pt}\pgfsys@curveto{-0.83226pt}{1.50694pt}{-1.50694pt}{0.83226pt}{-1.50694pt}{0.0pt}\pgfsys@curveto{-1.50694pt}{-0.83226pt}{-0.83226pt}{-1.50694pt}{0.0pt}{-1.50694pt}\pgfsys@curveto{0.83226pt}{-1.50694pt}{1.50694pt}{-0.83226pt}{1.50694pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\\{\leavevmode\hbox
to3.41pt{\vbox to3.41pt{\pgfpicture\makeatletter\hbox{\hskip
1.70694pt\lower-1.70694pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\color[rgb]{1,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0,0}\pgfsys@color@rgb@stroke{1}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\definecolor[named]{pgffillcolor}{rgb}{1,0,0}\pgfsys@color@rgb@fill{1}{0}{0}\pgfsys@invoke{
}{}\pgfsys@moveto{1.50694pt}{0.0pt}\pgfsys@curveto{1.50694pt}{0.83226pt}{0.83226pt}{1.50694pt}{0.0pt}{1.50694pt}\pgfsys@curveto{-0.83226pt}{1.50694pt}{-1.50694pt}{0.83226pt}{-1.50694pt}{0.0pt}\pgfsys@curveto{-1.50694pt}{-0.83226pt}{-0.83226pt}{-1.50694pt}{0.0pt}{-1.50694pt}\pgfsys@curveto{0.83226pt}{-1.50694pt}{1.50694pt}{-0.83226pt}{1.50694pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},\leavevmode\hbox
to3.41pt{\vbox to3.41pt{\pgfpicture\makeatletter\hbox{\hskip
1.70694pt\lower-1.70694pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{{{}}{}{}{}{}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{