# An invitation to game comonads

Samson Abramsky  and  Luca Reggio  Department of Computer Science, University
College London66–72 Gower Street, London, WC1E 6EAUnited Kingdom

###### Abstract.

Game comonads offer a categorical view of a number of model-comparison games
central to model theory, such as pebble and Ehrenfeucht–Fraïssé games.
Remarkably, the categories of coalgebras for these comonads capture
preservation of several fragments of resource-bounded logics, such as
(infinitary) first-order logic with $n$ variables or bounded quantifier rank,
and corresponding combinatorial parameters such as tree-width and tree-depth.
In this way, game comonads provide a new bridge between categorical methods
developed for semantics, and the combinatorial and algorithmic methods of
resource-sensitive model theory.

We give an overview of this framework and outline some of its applications,
including the study of homomorphism counting results in finite model theory,
and of equi-resource homomorphism preservation theorems in logic using the
axiomatic setting of arboreal categories. Finally, we describe some
homotopical ideas that arise naturally in the context of game comonads.

††journalvolume: 0††journalnumber: 0††article: 0††journalyear:
0000††publicationmonth: 0

###### Contents

  1. 1 Introduction
    1. 1.1 Finite and resource-sensitive model theory
    2. 1.2 Game comonads
    3. 1.3 A guided bibliography
    4. 1.4 Outline of the paper
  2. 2 Deception and logical resources
    1. 2.1 Finite-variable logic
    2. 2.2 Bounded quantifier rank
    3. 2.3 Modal logic and modal depth
  3. 3 Model-comparison games
    1. 3.1 Bisimulation games
    2. 3.2 Ehrenfeucht–Fraïssé games
    3. 3.3 Pebble games
  4. 4 A new perspective: Game comonads
    1. 4.1 Categories of relational structures
    2. 4.2 The modal comonad
    3. 4.3 The Ehrenfeucht–Fraïssé comonad
    4. 4.4 The pebbling comonad
  5. 5 The Kleisli category and the first logical equivalences
    1. 5.1 The Kleisli category
    2. 5.2 The equality symbol
    3. 5.3 Existential positive fragments
    4. 5.4 Fragments with counting quantifiers
  6. 6 Coalgebras and combinatorial parameters
    1. 6.1 Coalgebras, forest covers and combinatorial parameters of structures
      1. 6.1.1 Coalgebras for the modal comonad
      2. 6.1.2 Coalgebras for the Ehrenfeucht–Fraïssé comonad
      3. 6.1.3 Coalgebras for the pebbling comonad
    2. 6.2 Homomorphism counting results _à la_ Lovász
  7. 7 Paths, open maps, and more logical equivalences
    1. 7.1 Existential fragments and pathwise embeddings
    2. 7.2 Full fragments and open maps
    3. 7.3 Positive fragments and positive bisimulations
  8. 8 An axiomatic perspective: Arboreal categories
    1. 8.1 Arboreal categories
      1. 8.1.1 Proper factorisation systems and paths
      2. 8.1.2 Arboreal categories defined
    2. 8.2 Games in arboreal categories
      1. 8.2.1 The functor $\operatorname{\mathbb{P}}$
      2. 8.2.2 The arboreal game $\mathscr{G}$
  9. 9 Arboreal adjunctions
    1. 9.1 $F$-bisimilarity
    2. 9.2 The bisimilar companion property and homomorphism preservation theorems
  10. 10 Towards a homotopical view on logical resources
    1. 10.1 Quillen model categories
    2. 10.2 A model category for modal logic
    3. 10.3 Through the lens of modal logic: presheaves over forests

##  1\. Introduction

The traditional divide in theoretical computer science between formal methods
and semantics on the one hand, and algorithms and computational complexity on
the other, runs deep, as can be seen e.g. in the division into two volumes of
the _Handbook of theoretical computer science_ (van Leeuwen, 1990a, b). The
first strand is exemplified by categorical semantics, while the second strand
is exemplified by finite model theory and descriptive complexity. The aim of
this survey article is to introduce the reader to the framework of game
comonads, which bridges these two strands by bringing the tools of category
theory to the field of finite and resource-sensitive model theory. This
research programme was initiated in early 2017 and has been an active area of
research since then.111As witnessed by the ever-increasing length of surveys
on the subject! Contributors to this programme include (in alphabetical order)
Adam Ó Conghaile, Anuj Dawar, Tomáš Jakl, Thomas Laure, Dan Marsden, Yoàv
Montacute, Tom Paine, Colin Riba, Nihil Shah and Pengming Wang.

###  1.1. Finite and resource-sensitive model theory

Finite model theory studies theories and their classes of _finite_ models, and
has sparked researchers’ interest since the early days of model theory, cf.
e.g. (Trakhtenbrot, 1950). It has flourished and grown rapidly into an
independent field in the 1970s–80s thanks to its connections with complexity
theory and database theory. Nowadays, finite model theory is a subfield of
mathematical logic which beautifully exemplifies the convergence of
mathematics and computer science, see e.g. (Libkin, 2004; Grädel et al.,
2007). Many results of classical model theory fail when restricted to finite
models. These include Gödel’s Completeness Theorem, stating that a sentence is
true in all models of a theory $T$ just when it can be proved from the axioms
in $T$, and the Compactness Theorem, stating that $T$ has a model just when
every finite subset of $T$ does. Model-theoretic tools can be used to study
classes of finite models. This is the subject of _pseudo-finite model theory_
(Chatzidakis, 1997; Hrushovski, 2002; Väänänen, 2003), but this approach
inevitably leads to considering infinite models. For example, the theory of
finite fields (i.e., the collection of all sentences true in all finite
fields) has infinite models, the pseudo-finite fields. On the other hand,
finite model theory has developed its own methods, largely based on
combinatorial and probabilistic techniques.

The deep link between finite model theory and complexity theory has its origin
in Fagin’s theorem, showing that the problems in the complexity class NP are
exactly those definable in existential second-order logic (Fagin, 1974). This
result initiated the subject of descriptive complexity, which classifies
computational problems according to the logical language required to express
them (Immerman, 1999). The idea of stratifying by logical resources, typically
represented as complexity measures of formulas such as _quantifier rank_ or
_number of variables_ , has had great success and is central to finite model
theory, see e.g. (Immerman, 1999, Theorem 7.21 and Corollary 7.22) for a
stratification by number of blocks of second-order quantifiers. It is
reflected in the use of model-comparison games, such as Ehrenfeucht–Fraïssé
(Ehrenfeucht, 1960; Fraïssé, 1954) or pebble games (Barwise, 1977; Immerman,
1982), to determine if two models are equivalent in a given logic fragment.
Here, the logical resources correspond to the resources available to the two
players, Spoiler and Duplicator, such as the number of rounds or the number of
pebbles (cf. §3).

This method, wherein logical resources are placed centre stage, applies to
both finite and infinite structures, leading to what we shall call _resource-
sensitive model theory_. It can also be thought of as “model theory without
compactness”, since it avoids the use of the Compactness Theorem. This
viewpoint is at the heart of most preservation and inexpressibility results in
finite model theory, and it has also led to remarkable resource-sensitive
refinements of classical results such as the Equirank Homomorphism
Preservation Theorem (Rossman, 2008); cf. §9.

###  1.2. Game comonads

In 2017, a novel approach to logical resources based on game comonads,
providing categorical accounts of key constructions in finite model theory,
was initiated in (Abramsky et al., 2017; Abramsky and Shah, 2018). The key
insight is that model-comparison games can be naturally organised into
endofunctors on categories of relational structures that carry the structure
of comonads (these are the dual notion to monads, which are widely used in
functional programming). Intuitively, given a type of game $G$ and a resource
parameter $k$, the game comonad $\mathbb{G}_{k}$ assigns to a structure $A$ a
new structure $\mathbb{G}_{k}A$ which can be thought of as a _forest cover_
(or forest-ordered decomposition) of $A$, abstracting the idea of
$k$-unravelling from modal logic. The universe of $\mathbb{G}_{k}A$ is the set
of all possible plays in the structure $A$ in the game $G$ in which the
appropriate notion of resources is bounded by $k$. Thus, game comonads arise
by viewing games not as external artefacts, but as semantic constructions in
their own right. The first key observation is that Duplicator winning
strategies for the existential $G$-game from $A$ to $B$ are recovered as
Kleisli morphisms

$\mathbb{G}_{k}A\to B.$

Duplicator winning strategies for the back-and-forth game, and variants
thereof, can also be recovered. In this manner, the notion of local
approximation built into the game is internalised into the category of
relational structures.

Remarkably, this idea applies to a number of games central to finite model
theory, leading e.g. to _Ehrenfeucht–Fraïssé_ and _pebbling comonads_ ,
corresponding to Ehrenfeucht–Fraïssé and pebble games, respectively. In fact,
game comonads cover a range of logics, including first-order, modal, guarded
and hybrid logics, and logics with generalised quantifiers (Abramsky and Shah,
2021; Ó Conghaile and Dawar, 2021; Abramsky and Marsden, 2021, 2022). See
(Abramsky, 2022b) for a survey. In each case, the categories of coalgebras for
the comonads encode, in a syntax-free fashion, important logical resources and
combinatorial parameters of structures; cf. Figure 1.

[ columns-width=5cm, hvlines-except-borders, rules=color=white,width=1pt ] ccc
cyan1 [color=white] Game comonads & Logical resources Combinatorial parameters
pebble comonad number of variables tree-width
Ehrenfeucht–Fraïssé comonad quantifier rank tree-depth
modal comonad modal depth synchronization-tree depth
guarded comonad guarded-quantifier depth $\mathfrak{g}$-guarded tree-width

Figure 1. Examples of game comonads, with corresponding logical resources and
combinatorial parameters.

Having established a common ground for various notions of logical resources in
the form of game comonads and their coalgebras, the possibility opens up of
treating logical resources uniformly, and comparing them by studying the
structural properties of the corresponding game comonads. This can be done by
working with arboreal categories, which provide an axiomatic approach to game
comonads (Abramsky and Reggio, 2021, 2023). From this axiomatic perspective,
interesting “dividing lines” can be identified, such as the _bisimilar
companion property_ (see §9).

###  1.3. A guided bibliography

In addition to the present one, surveys on game comonads include (Abramsky,
2020, 2022b); the first one is aimed more at theoretical computer scientists,
the second at mathematical logicians. The “first wave” in this research
programme consisted in establishing the paradigm and finding many examples:

  * •

the first paper (Abramsky et al., 2017) introduced comonads for pebble games;

  * •

this approach was further developed and extended to Ehrenfeucht–Fraïssé and
bisimulation games in (Abramsky and Shah, 2018). We recommend the extended
version (Abramsky and Shah, 2021).

  * •

More game comonads, including those for guarded and hybrid fragments, and
generalised quantifiers, were defined in (Abramsky and Marsden, 2021, 2022; Ó
Conghaile and Dawar, 2021).

The first wave culminated in the axiomatic framework of arboreal categories
(Abramsky and Reggio, 2021); a more complete account can be found in the
extended version (Abramsky and Reggio, 2023). In the second wave, we see an
emerging landscape in which structural features and dividing lines begin to
appear, leading to:

  * •

homomorphism counting results _à la_ Lovász using game comonads (Dawar et al.,
2021); the general pattern was extended beyond finite structures in (Reggio,
2022).

  * •

A uniform approach to homomorphism preservation theorems in logic based on
arboreal categories (Abramsky and Reggio, 2024), following the comonadic
analysis of the Equirank-variable homomorphism preservation theorem in (Paine,
2020).

  * •

An axiomatic study of Feferman–Vaught type theorems and Courcelle’s theorem
(Jakl et al., 2022, 2023), and of graph parameters via density comonads
(Abramsky et al., 2022).

  * •

Refinements of the axiomatic setting in the form of linear arboreal categories
(Abramsky et al., 2024b), and the study of the expressive power of arboreal
categories (Reggio and Riba, 2023).

  * •

The use of sheaf-theoretic and cohomological methods in constraint
satisfaction problems (Abramsky, 2022a; Ó Conghaile, 2022), and the axiomatic
study of further fragments of resource-sensitive logics (Abramsky et al.,
2024a).

In this paper we will outline the basic ideas underlying the theory of game
comonads, and touch upon some of the more advanced topics, with the aim of
giving the reader a glimpse of the rich landscape described above.

###  1.4. Outline of the paper

The paper is structured as follows. In §§2–3 we introduce our running examples
of logical resources and model-comparison games, and in §4 we define the
corresponding game comonads. The first examples of logical equivalences that
can be recovered from game comonads, and in particular those corresponding to
the existential versions of the games, are illustrated in §5. In §6 we explain
how coalgebras for game comonads encode combinatorial parameters of
structures, and show how this can be used to obtain a uniform approach to
_homomorphism counting results_ in finite model theory. The main focus of §7
is on Duplicator winning strategies in back-and-forth games, which can be
encoded via an appropriate notion of _open map bisimulation_ between
coalgebras. Finally, in §§8–9 we give an overview of arboreal categories and
their application to homomorphism preservation theorems in logic, and in §10
we discuss some emerging links between resource-sensitive model theory and
abstract homotopy.

##  2\. Deception and logical resources

In logic, models are typically studied not as they really are, i.e. up to
isomorphism, but only up to definable properties; e.g., two models are
elementarily equivalent if they satisfy the same first-order sentences. This
idea is pervasive in mathematics and computer science: we may not want to
distinguish between two topological spaces that are homotopy equivalent, or
two programs that on the same input give the same output. From a logical
viewpoint, every fragment $\mathcal{L}\subseteq\mathrm{FO}$ of first-order
logic induces an equivalence relation $\equiv_{\mathcal{L}}$ on structures
given by

$A\equiv_{\mathcal{L}}B\ \ \Longleftrightarrow\ \ \text{for all
}\varphi\in\mathcal{L}\ (A\models\varphi\ \Leftrightarrow\ B\models\varphi).$

The relation $\equiv_{\mathcal{L}}$ allows us to compare structures up to
$\mathcal{L}$-definable properties.

When $\mathcal{L}=\mathrm{FO}$, the relation $\equiv_{\mathcal{L}}$ coincides
with elementary equivalence. As any two elementarily equivalent finite
structures are isomorphic, the main focus in finite model theory is on
relations $\equiv_{\mathcal{L}}$ that are strictly coarser than elementary
equivalence. This can be achieved, for instance, by considering resource-
bounded fragments of first-order logic. Intuitively, given a resource
parameter $k\in\mathbb{N}$, we will define a corresponding stratification of
$\mathrm{FO}$, i.e. an increasing chain of logic fragments

$\mathcal{L}_{0}\subseteq\mathcal{L}_{1}\subseteq\mathcal{L}_{2}\subseteq\cdots\subseteq\mathrm{FO}$

whose union is all of $\mathrm{FO}$. Typically, the equivalence relations
$\equiv_{\mathcal{L}_{k}}$ are strictly coarser than $\equiv_{\mathrm{FO}}$,
i.e. than elementary equivalence, but we recover the latter as

$\bigcap_{k\in\mathbb{N}}{\equiv_{\mathcal{L}_{k}}}\ =\ \
{\equiv_{\mathrm{FO}}}.$

We illustrate two such stratifications of first-order logic, in which the
resource parameters are given by the number of variables and the quantifier
rank, respectively. We then outline a similar stratification in the case of
modal logic. Throughout, we fix a countably infinite set of (pairwise
distinct) first-order variables

$x_{1},x_{2},x_{3},\dots$

from which all first-order formulas are built. Moreover, for simplicity, we
shall restrict ourselves to the case of finite relational signatures, i.e.
signatures $\sigma$ containing finitely many relation symbols and constant
symbols, but no function symbols.

###  2.1. Finite-variable logic

For each $n\in\mathbb{N}$, denote by

$\mathrm{FO}^{n}$

the set of all first-order sentences that only use the variables
$x_{1},\ldots,x_{n}$. In particular, $\mathrm{FO}^{0}$ consists of the atomic
sentences (such as $c_{1}=c_{2}$, $S(c_{1},c_{2},c_{3})$ and Boolean
combinations thereof, where $c_{1},c_{2},c_{3}$ are constant symbols and $S$
is a relation symbol). Despite the severe syntactic restriction, the finite-
variable fragments $\mathrm{FO}^{n}$ are remarkably expressive. This
expressiveness comes from the fact that variables can be _reused_. For
example, for each integer $\ell\geq 1$ there is a three-variable sentence
$\varphi_{\ell}\in\mathrm{FO}^{3}$ in the language of graphs expressing the
existence of a path of length $\ell$. Such a $\varphi_{\ell}$ can be defined
as $\exists x_{1},x_{2}.\psi_{\ell}$, where the formula
$\psi_{\ell}(x_{1},x_{2})$ expresses the existence of a path of length $\ell$
from $x_{1}$ to $x_{2}$ and is defined as follows:

$\psi_{1}(x_{1},x_{2})\coloneqq R(x_{1},x_{2})$

and, for all $\ell>1$,

$\psi_{\ell}(x_{1},x_{2})\coloneqq\exists x_{3}.(R(x_{1},x_{3})\wedge\exists
x_{1}.(x_{1}=x_{3}\wedge\psi_{\ell-1}(x_{1},x_{2}))).$

###  2.2. Bounded quantifier rank

The _quantifier rank_ of a formula is the maximum number of nested quantifiers
in the formula. For example, the formulas

$R(x_{1},x_{2}),\ \ \exists x_{2}.R(x_{1},x_{2})\wedge\exists
x_{3}.R(x_{3},x_{1})$

have quantifier rank $0$ and $1$, respectively, whereas the following has
quantifier rank $2$:

$\forall x_{2}\exists x_{3}.(R(x_{1},x_{3})\wedge(R(x_{1},x_{2})\to
R(x_{3},x_{2}))).$

For each $k\in\mathbb{N}$, write

$\mathrm{FO}_{k}$

for the collection of all first-order sentences of quantifier rank at most
$k$. The following observation about the logic fragments $\mathrm{FO}_{k}$
will be important in the following; see e.g. (Libkin, 2004, Lemma 3.13) for a
proof. (Recall that we are considering only _finite_ relational signatures.)

###### Lemma 2.1.

For each $k\in\mathbb{N}$ there are, up to logical equivalence, finitely many
formulas of quantifier rank at most $k$.

In particular, the quotient of $\mathrm{FO}_{k}$ with respect to logical
equivalence is finite. The analogous statement for the $n$-variable fragments
$\mathrm{FO}^{n}$ is false in general: for example, for any two distinct
integers $\ell,m\geq 1$, the sentences
$\varphi_{\ell},\varphi_{m}\in\mathrm{FO}^{3}$ stating the existence of a path
of length $\ell$ and $m$, respectively, are not equivalent.

###### Remark 2.2.

We note in passing that logically equivalent formulas may have different
quantifier rank or use a different number of variables. For example, the
sentence

$\exists x_{1},\dots,x_{4}.(R(x_{1},x_{2})\wedge R(x_{2},x_{3})\wedge
R(x_{3},x_{4}))$

uses $4$ variables and has quantifier rank $4$; it expresses the existence of
a path of length $3$, so it is equivalent to the sentence $\varphi_{3}=\exists
x_{1},x_{2}.\psi_{3}$, which uses $3$ variables and has quantifier rank $6$.

###  2.3. Modal logic and modal depth

We consider modal logic as a fragment of first-order logic (in one free
variable) via its standard translation. In more detail, let $\sigma$ be a
_modal signature_ , i.e. a finite signature consisting of relation symbols of
arity either $1$ or $2$. Each unary relation symbol ${P\in\sigma}$ yields a
propositional variable $p$, and each binary relation symbol
$R_{\alpha}\in\sigma$ yields modalities $\Box_{\alpha}$ and
$\Diamond_{\alpha}$. Then a $\sigma$-structure $A$ corresponds to a Kripke
structure for this (multi-)modal logic: the interpretation $P^{A}\subseteq A$
gives the valuation for the propositional variable $p$, and
$R_{\alpha}^{A}\subseteq A^{2}$ gives the accessibility relation for
$\Box_{\alpha}$ and $\Diamond_{\alpha}$.

Each formula $\varphi$ in this modal logic admits a translation into a first-
order formula $\llbracket\varphi\rrbracket_{x}$ in one free variable $x$; this
is known as the _standard translation_ , see e.g. (Blackburn et al., 2002,
§2.4). We let $\llbracket p\rrbracket_{x}\coloneqq P(x)$ and let
$\llbracket-\rrbracket_{x}$ commute with Boolean connectives. Further, set

$\llbracket\Box_{\alpha}\varphi\rrbracket_{x}\coloneqq\forall
y.\,R_{\alpha}(x,y)\to\llbracket\varphi\rrbracket_{y}\ \ \text{ and }\ \
\llbracket\Diamond_{\alpha}\varphi\rrbracket_{x}\coloneqq\exists
y.\,R_{\alpha}(x,y)\wedge\llbracket\varphi\rrbracket_{y}$

where $y$ is a fresh variable. Modal formulas are evaluated in _pointed Kripke
structures_ , that is pairs $(A,a)$ where $A$ is a $\sigma$-structure and
$a\in A$. Then $A,a\models\varphi$ according to Kripke semantics if, and only
if, $A\models\llbracket\varphi\rrbracket_{x}[a/x]$ in the standard model-
theoretic sense.

In analogy with the quantifier rank of a first-order formula, we define the
_modal depth_ of a modal formula as the maximum nesting of modalities in the
formula. For example, $\neg p$, $\Diamond_{\alpha}p$ and
$\Box_{\alpha}\Diamond_{\beta}p$ have modal depth $0$, $1$ and $2$,
respectively. For each $k\in\mathbb{N}$, we denote by

$\mathrm{ML}_{k}$

the collection of all modal formulas with modal depth at most $k$. The modal
depth of a modal formula coincides with the quantifier rank of its standard
translation, hence Lemma 2.1 implies that each modal fragment
$\mathrm{ML}_{k}$ contains only finitely many formulas, up to logical
equivalence.

##  3\. Model-comparison games

In this section we will introduce three examples of model-comparison games:
the bisimulation game for modal logic, and the Ehrenfeucht–Fraïssé and pebble
games for first-order logic. All are two-player games, played by Spoiler and
Duplicator on $\sigma$-structures $A$ and $B$. While Spoiler aims to show that
$A$ and $B$ are different, Duplicator aims to show that they are similar, i.e.
that they satisfy the same definable properties.

As before, we assume that $\sigma$ is a finite relational signature (or a
modal signature, in the case of modal logic).

###  3.1. Bisimulation games

Fix $k\in\mathbb{N}$. The $k$-round bisimulation game for modal logic is
played by Spoiler and Duplicator on pointed Kripke structures $(A,a)$ and
$(B,b)$ as follows. The initial position is $(a_{0},b_{0})\coloneqq(a,b)$. At
round $i+1$ (with $0\leq i<k$) with current position $(a_{i},b_{i})$, Spoiler
chooses one of the two structures and a binary relation symbol in the
signature, say $A$ and $R_{\alpha}$, and an element $a_{i+1}\in A$ such that
$R^{A}_{\alpha}(a_{i},a_{i+1})$. Duplicator must respond by choosing an
element in the other structure, in this case $b_{i+1}\in B$, such that
$R^{B}_{\alpha}(b_{i},b_{i+1})$. If Duplicator has no such response available,
they lose. Otherwise, Duplicator wins the $k$-round bisimulation game if, for
all unary predicates $P$ in the signature, we have

$\forall i\in\\{0,\ldots,k\\},\ \ P^{A}(a_{i})\Leftrightarrow P^{B}(b_{i}).$

The following classical result links the existence of a Duplicator winning
strategy in this game with equivalence in the bounded-depth fragment of modal
logic:

###### Theorem 3.1 ((Hennessy and Milner, 1980)).

Duplicator has a winning strategy in the $k$-round bisimulation game played
between $(A,a)$ and $(B,b)$ if, and only if, $(A,a)$ and $(B,b)$ satisfy the
same formulas in $\mathrm{ML}_{k}$.

###  3.2. Ehrenfeucht–Fraïssé games

As before, fix $k\in\mathbb{N}$. The $k$-round Ehrenfeucht–Fraïssé game,
played by Spoiler and Duplicator on structures $A$ and $B$, can be described
as follows. In the $i$th round (with $1\leq i\leq k$), Spoiler chooses an
element in one of the two structures, say $a_{i}\in A$, and Duplicator
responds by choosing an element in the other structure, say $b_{i}\in B$.
Duplicator wins after $k$ rounds if the relation

$\\{(a_{i},b_{i})\mid 1\leq i\leq k\\}$

is a partial isomorphism, i.e. the map $a_{i}\mapsto b_{i}$ yields an
isomorphism between the induced substructures of $A$ and $B$ determined by the
sets $\\{a_{1},\ldots,a_{k}\\}$ and $\\{b_{1},\ldots,b_{k}\\}$, respectively.
In particular, note that Duplicator wins the $0$-round game precisely when $A$
and $B$ satisfy the same atomic sentences. Furthermore, for any
$j\in\mathbb{N}$, Duplicator wins the $(j+1)$-round game if, and only if, the
following conditions are satisfied:

  1. (i)

For every $a\in A$ there exists $b\in B$ such that Duplicator wins the
$j$-round game between the pointed structures $(A,a)$ and $(B,b)$;222In other
words, we expand the signature by adding a fresh constant symbol
$\mathfrak{c}$, and regard $A$ and $B$ as structures for this new signature by
setting $\mathfrak{c}^{A}\coloneqq a$ and $\mathfrak{c}^{B}\coloneqq b$. The
$j$-round game is then played on the extended structures.

  2. (ii)

For every $b\in B$ there exists $a\in A$ such that Duplicator wins the
$j$-round game between the pointed structures $(A,a)$ and $(B,b)$.

The existence of a winning strategy for Duplicator captures precisely
equivalence in first-order logic with bounded quantifier rank:

###### Theorem 3.2 ((Ehrenfeucht, 1960; Fraïssé, 1954)).

Duplicator has a winning strategy in the $k$-round Ehrenfeucht–Fraïssé game
played between $A$ and $B$ if, and only if, $A$ and $B$ satisfy the same
first-order sentences in $\mathrm{FO}_{k}$.

We briefly sketch a proof of Theorem 3.2, which proceeds by induction on $k$.
The base case $k=0$ is obvious because the first-order sentences with
quantifier rank $0$ are exactly the atomic ones. Next, we show that if Theorem
3.2 holds for $k$, it also holds for $k+1$. To this end, for all elements $a$
of a structure $A$, denote by $\operatorname{tp}_{k}(a)$ the _rank- $k$ type
of $a$_, i.e. the set of all first-order formulas $\varphi(x)$ with quantifier
rank $\leq k$ such that $A\models\varphi(a)$.

In one direction, suppose $A$ and $B$ satisfy the same first-order sentences
with quantifier rank $\leq k+1$. We must show that Duplicator has a winning
strategy in the $(k+1)$-round game between $A$ and $B$. We will check
condition (i) above; the proof of (ii) is similar. Pick an arbitrary element
$a\in A$ and consider its rank-$k$ type $\operatorname{tp}_{k}(a)$. We have

$A\models\bigwedge{\operatorname{tp}_{k}(a)}.$

Although the latter conjunction is infinite, it follows from Lemma 2.1 that it
is equivalent to a single formula $\varphi_{a}(x)$ of quantifier rank $\leq
k$. Hence

$A\models\exists x.\varphi_{a}(x),$

and since the sentence $\exists x.\varphi_{a}(x)$ has quantifier rank $\leq
k+1$ we get

$B\models\exists x.\varphi_{a}(x).$

If $b\in B$ is a witness for the latter existential quantifier, we have
$\operatorname{tp}_{k}(a)=\operatorname{tp}_{k}(b)$. Thus $(A,a)$ and $(B,b)$
satisfy the same first-order sentences with quantifier rank $\leq k$ and so,
by inductive hypothesis, Duplicator wins the $k$-round game between $(A,a)$
and $(B,b)$.

The other direction follows by observing that every sentence in
$\mathrm{FO}_{k+1}$ is a Boolean combination of sentences of the form $\exists
x.\varphi(x)$ where $\varphi(x)$ has quantifier rank $\leq k$, and using items
(i)–(ii) above. Cf. e.g. (Libkin, 2004, Theorem 3.18).

###  3.3. Pebble games

Fix $n\in\mathbb{N}$. In the $n$-pebble game between structures $A$ and $B$,
Spoiler and Duplicator each have $n$ pebbles available. In the $i$th round,
Spoiler places some pebble $p_{i}$ on an element of one of the two structures,
say $a_{i}\in A$, and Duplicator responds by placing their corresponding
pebble $p_{i}$ on an element of the other structure, say $b_{i}\in B$. If the
pebble $p_{i}$ was previously placed on some other element, the effect is to
move it to the newly chosen element (this corresponds to the fact that
variables in a formula can be reused). After $k$ rounds have been played, we
have sequences

$[(p_{1},a_{1}),\ldots,(p_{k},a_{k})]\ \ \text{ and }\ \
[(p_{1},b_{1}),\ldots,(p_{k},b_{k})]$

that record the placings of pebbles on elements during the play. The current
placing of pebble $p$ is the last element in the sequence with first component
$p$.333The current placings of the pebbles can be thought of as “windows” of
size bounded by $n$ onto the structures. These windows can slide around over
different parts of the structures as moves are played. Duplicator wins the
round if the relation determined by the current placings of the pebbles is a
partial isomorphism. Duplicator wins the $n$-pebble game if they have a
strategy that is winning after $k$ rounds, for all $k\in\mathbb{N}$.

Note that, whereas the resource parameter in the bisimulation and
Ehrenfeucht–Fraïssé games is the number of rounds, pebble games are infinite
and the relevant resource parameter is the number of pebbles. The infinite
nature of pebble games entails that the existence of a winning strategy for
Duplicator captures equivalence in an _infinitary extension_ of first-order
logic:

###### Definition 3.3.

Let $L_{\infty,\omega}$ be the set of all sentences using, in addition to the
usual first-order connectives, conjunctions and disjunctions of any
cardinality.444The two subscripts in $L_{\infty,\omega}$ indicate that we
allow infinitary conjunctions and disjunctions ($\infty$) but only finitary
quantifications ($\omega$). Note that for all sentences $\varphi\in
L_{\infty,\omega}$, each subformula of $\varphi$ contains only finitely many
variables. We write $L^{n}_{\infty,\omega}$ for the fragment of
$L_{\infty,\omega}$ consisting of those sentences in the variables
$x_{1},\ldots,x_{n}$.

###### Theorem 3.4 ((Barwise, 1977; Immerman, 1982)).

Duplicator has a winning strategy in the $n$-pebble game played between $A$
and $B$ if, and only if, $A$ and $B$ satisfy the same sentences in
$L^{n}_{\infty,\omega}$.

If the structures $A$ and $B$ are finite, then every infinite strategy in the
$n$-pebble game is determined by a $k$-round strategy for a sufficiently large
$k$, namely the one in which all finitely many possible placings of the
pebbles appeared. Therefore, the equivalence relations
$\equiv_{L^{n}_{\infty,\omega}}$ and $\equiv_{\mathrm{FO}^{n}}$ coincide over
finite structures; cf. e.g. (Kolaitis and Vardi, 1992, Corollary 2.19) or
(Libkin, 2004, Proposition 11.8).

###### Corollary 3.5.

Let $A$, $B$ be finite structures. Duplicator has a winning strategy in the
$n$-pebble game played between $A$ and $B$ if, and only if, $A$ and $B$
satisfy the same sentences in $\mathrm{FO}^{n}$.

##  4\. A new perspective: Game comonads

Game comonads arise from the insight that model-comparison games can be viewed
as semantic constructions in their own right. More precisely, given a notion
of game $G$ and a resource parameter $k$, for each structure $A$ we construct
a structure $\mathbb{G}_{k}A$ (in the same signature) whose universe consists
of all possible plays in $A$ in the game $G$ with $k$ resources. What is more,
the assignment $A\mapsto\mathbb{G}_{k}A$ is functorial and yields a _comonad_
on the appropriate category of structures.

We start by recalling the notion of comonad, which is dual to that of a monad:

###### Definition 4.1.

A _comonad (in Kleisli form)_ on a category $\operatorname{\mathscr{C}}$ is
given by:

  * •

an object map
$\mathbb{G}\colon\mathrm{Ob}(\operatorname{\mathscr{C}})\to\mathrm{Ob}(\operatorname{\mathscr{C}})$,

  * •

a morphism $\varepsilon_{A}\colon\mathbb{G}A\to A$ for every object $A$,

  * •

and a _coextension operation_ associating with each morphism
$f\colon\mathbb{G}A\to B$ a morphism $f^{*}\colon\mathbb{G}A\to\mathbb{G}B$,

such that for all morphisms $f\colon\mathbb{G}A\to B$ and
$g\colon\mathbb{G}B\to C$, the following equations hold:

$\varepsilon_{A}^{*}=\mathrm{id}_{\mathbb{G}A},\ \ \ \ \ \varepsilon_{B}\circ
f^{*}=f,\ \ \ \ \ (g\circ f^{*})^{*}=g^{*}\circ f^{*}.$

We can always extend a comonad in Kleisli form $\mathbb{G}$ to a functor
$\operatorname{\mathscr{C}}\to\operatorname{\mathscr{C}}$ by setting
$\mathbb{G}f\coloneqq(f\circ\varepsilon_{A})^{*}$ for every morphism $f\colon
A\to B$. Moreover, setting $\delta_{A}\coloneqq\mathrm{id}_{\mathbb{G}A}^{*}$
for every $A$ in $\operatorname{\mathscr{C}}$, the tuple
$(\mathbb{G},\varepsilon,\delta)$ is a comonad in the more traditional sense,
where the natural transformations $\varepsilon$ and $\delta$ are the _counit_
and the _comultiplication_ of the comonad, respectively. In fact, these two
formulations are equivalent.

The structure $\mathbb{G}_{k}A$ can be thought of as a forest-ordered _cover_
, or _decomposition_ , of $A$. A fundamental example of this idea arises from
the unravelling construction in modal logic, which we now recall. Consider the
pointed Kripke model $(A,s)$ in Figure 2; the modal signature consists of a
single binary relation symbol (represented by an arrow) and two unary relation
symbols (represented as red and blue nodes). The _unravelling_ of $(A,a)$ is
the Kripke model of all possible finite paths in $A$ starting from $x$; see
§4.2 for a precise definition. For each $k\in\mathbb{N}$, the _$k$
-unravelling_ of $(A,a)$ is obtained by restricting to paths of length at most
$k$. Note that the universe of the $k$-unravelling of $(A,a)$ can be
identified with the set of all possible plays in $(A,a)$ in the $k$-round
bisimulation game.

$\leavevmode\hbox to65.19pt{\vbox
to73.76pt{\pgfpicture\makeatletter\hbox{\hskip
35.91457pt\lower-39.04694pt\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{
}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-29.27164pt}{-34.71211pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
5.69055pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.32813pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${e}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.99998pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
0.0pt\hfil&\hfil\hskip 17.69054pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.16377pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${c}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 17.89053pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{{}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.64294pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${a}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.89055pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
5.69055pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.14583pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${b}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.99998pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 17.69054pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.60243pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${d}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr\vskip 5.49994pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 17.69054pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.75pt}{-3.41666pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${A}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil&\hfil\hskip 17.69054pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}
{{}{}{{}}{}}{{}{}{{}}{}}{{}{}}{{}}
{{}{}{{}}{}}{{{}}{{}}}{{}}{{}{}{{}}{}}{{{}}{{}}}{{}}{}{{}}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{{{{{{}}{}{}{}{}{{}}}}}{}{}{}{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{{ {\pgfsys@beginscope
\pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{}
\pgfsys@moveto{-2.07988pt}{2.39986pt}\pgfsys@curveto{-1.69989pt}{0.95992pt}{-0.85313pt}{0.27998pt}{0.0pt}{0.0pt}\pgfsys@curveto{-0.85313pt}{-0.27998pt}{-1.69989pt}{-0.95992pt}{-2.07988pt}{-2.39986pt}\pgfsys@stroke\pgfsys@endscope}}
}{}{}{{}}{}{}{{}}\pgfsys@moveto{-26.52635pt}{-22.93243pt}\pgfsys@curveto{-35.71458pt}{-38.84695pt}{-11.44759pt}{-38.84695pt}{-20.43584pt}{-23.27881pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.5}{0.86603}{-0.86603}{-0.5}{-20.53583pt}{-23.10562pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{4.43794pt}{6.62328pt}\pgfsys@lineto{18.84181pt}{19.19463pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7534}{0.65755}{-0.65755}{0.7534}{18.99248pt}{19.32613pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{4.43794pt}{-1.12334pt}\pgfsys@lineto{18.84181pt}{-13.69469pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7534}{-0.65755}{0.65755}{0.7534}{18.99248pt}{-13.82619pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{23.58109pt}{17.44046pt}\pgfsys@lineto{23.58109pt}{-11.54056pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{-1.0}{1.0}{0.0}{23.58109pt}{-11.74054pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-4.43794pt}{-1.12334pt}\pgfsys@lineto{-18.84181pt}{-13.69469pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.7534}{-0.65755}{0.65755}{-0.7534}{-18.99248pt}{-13.82619pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-23.58109pt}{-11.94052pt}\pgfsys@lineto{-23.58109pt}{17.0405pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-23.58109pt}{17.24048pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-19.14314pt}{19.4577pt}\pgfsys@lineto{-4.73927pt}{6.88635pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.7534}{-0.65755}{0.65755}{0.7534}{-4.58861pt}{6.75485pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \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}}\ \ \
\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
3.0pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\kern
27.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}\ignorespaces{\hbox{\lx@xy@drawsquiggles@}}{\hbox{\kern
27.0pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces\ \
\ \leavevmode\hbox to11.38pt{\vbox
to11.38pt{\pgfpicture\makeatletter\hbox{\hskip 5.69055pt\lower-5.69055pt\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{
}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.69055pt}{-5.69055pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
5.69055pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.64294pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${a}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}}} \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 to46.14pt{\vbox
to31.76pt{\pgfpicture\makeatletter\hbox{\hskip
23.07172pt\lower-15.88107pt\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{
}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.07172pt}{-15.88107pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
5.69055pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.14583pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${b}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.16377pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${c}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.60243pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${d}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.64294pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${a}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{0.0pt}{-9.99052pt}\pgfsys@lineto{0.0pt}{-1.79054pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{0.0pt}{-1.59056pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{3.82234pt}{-11.39908pt}\pgfsys@lineto{13.2993pt}{-0.28635pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6489}{0.7609}{-0.7609}{0.6489}{13.42906pt}{-0.13419pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-3.82234pt}{-11.39908pt}\pgfsys@lineto{-13.2993pt}{-0.28635pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.6489}{0.7609}{-0.7609}{-0.6489}{-13.42906pt}{-0.13419pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \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 to63.52pt{\vbox
to52.14pt{\pgfpicture\makeatletter\hbox{\hskip 31.7623pt\lower-26.0716pt\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{
}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.7623pt}{-26.0716pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
5.69055pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.32813pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${e}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.14583pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${b}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.60243pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${d}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.14583pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${b}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.16377pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${c}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.60243pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${d}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 6.00006pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.64294pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${a}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{12.51292pt}{-21.5896pt}\pgfsys@lineto{21.98988pt}{-10.47687pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6489}{0.7609}{-0.7609}{0.6489}{22.11964pt}{-10.3247pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{8.69058pt}{-20.18105pt}\pgfsys@lineto{8.69058pt}{-11.98106pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{8.69058pt}{-11.78108pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{4.86824pt}{-21.5896pt}\pgfsys@lineto{-4.60872pt}{-10.47687pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.6489}{0.7609}{-0.7609}{-0.6489}{-4.73848pt}{-10.3247pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{8.69058pt}{0.2pt}\pgfsys@lineto{8.69058pt}{8.39998pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{8.69058pt}{8.59996pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-8.69058pt}{0.2pt}\pgfsys@lineto{-8.69058pt}{8.39998pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-8.69058pt}{8.59996pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.51292pt}{-1.20856pt}\pgfsys@lineto{-21.98988pt}{9.90417pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.6489}{0.7609}{-0.7609}{-0.6489}{-22.11964pt}{10.05634pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \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 to63.52pt{\vbox
to72.52pt{\pgfpicture\makeatletter\hbox{\hskip 31.7623pt\lower-36.26212pt\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{
}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{\offinterlineskip{}{}{{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}{{{}}}{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-31.7623pt}{-36.26212pt}\pgfsys@invoke{
}\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip
5.69055pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.64294pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${a}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.32813pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${e}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.14583pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${b}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
5.69055pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.32813pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${e}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.14583pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${b}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.60243pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${d}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.14583pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${b}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{1,0.8,0.8}\pgfsys@color@rgb@fill{1}{0.8}{0.8}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.16377pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${c}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip
5.69055pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.85,0.85,1}\pgfsys@color@rgb@fill{0.85}{0.85}{1}\pgfsys@invoke{
}\pgfsys@moveto{5.69055pt}{0.0pt}\pgfsys@curveto{5.69055pt}{3.14284pt}{3.14284pt}{5.69055pt}{0.0pt}{5.69055pt}\pgfsys@curveto{-3.14284pt}{5.69055pt}{-5.69055pt}{3.14284pt}{-5.69055pt}{0.0pt}\pgfsys@curveto{-5.69055pt}{-3.14284pt}{-3.14284pt}{-5.69055pt}{0.0pt}{-5.69055pt}\pgfsys@curveto{3.14284pt}{-5.69055pt}{5.69055pt}{-3.14284pt}{5.69055pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.60243pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${d}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr\vskip 8.99994pt\cr\hfil\hskip
0.0pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 6.00006pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
0.0pt\hfil&\hfil\hskip 11.69061pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{ }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.64294pt}{-2.15277pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${a}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip
5.69055pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}{{{{}}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}{{}}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{12.51292pt}{-31.78012pt}\pgfsys@lineto{21.98988pt}{-20.66739pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6489}{0.7609}{-0.7609}{0.6489}{22.11964pt}{-20.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{8.69058pt}{-30.37157pt}\pgfsys@lineto{8.69058pt}{-22.17159pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{8.69058pt}{-21.9716pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{4.86824pt}{-31.78012pt}\pgfsys@lineto{-4.60872pt}{-20.66739pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.6489}{0.7609}{-0.7609}{-0.6489}{-4.73848pt}{-20.51523pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{8.69058pt}{-9.99052pt}\pgfsys@lineto{8.69058pt}{-1.79054pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{8.69058pt}{-1.59056pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-8.69058pt}{-9.99052pt}\pgfsys@lineto{-8.69058pt}{-1.79054pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-8.69058pt}{-1.59056pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-12.51292pt}{-11.39908pt}\pgfsys@lineto{-21.98988pt}{-0.28635pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-0.6489}{0.7609}{-0.7609}{-0.6489}{-22.11964pt}{-0.13419pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-4.86824pt}{8.98196pt}\pgfsys@lineto{4.60872pt}{20.0947pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.6489}{0.7609}{-0.7609}{0.6489}{4.73848pt}{20.24686pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-8.69058pt}{10.39052pt}\pgfsys@lineto{-8.69058pt}{18.5905pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-8.69058pt}{18.79048pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{
}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-26.07175pt}{10.39052pt}\pgfsys@lineto{-26.07175pt}{18.5905pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{0.0}{1.0}{-1.0}{0.0}{-26.07175pt}{18.79048pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \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}}\qquad\cdots$
Figure 2. A pointed Kripke model $(A,a)$ and the first terms of its sequence
of $k$-unravellings (for $k=0,1,2,3$).

After introducing the relevant categories of relational structures on which
game comonads are defined, we will show that the unravelling construction
yields a comonad on pointed Kripke models, the so-called _modal comonad_ , and
introduce two further examples of game comonads: the _Ehrenfeucht–Fraïssé_ and
_pebbling comonads_. These comonads can be regarded as enrichments of the
_finite-list comonad_ on the category of sets, and variations thereof.

###  4.1. Categories of relational structures

Henceforth, we shall fix a finite relational signature $\sigma$; we will
assume for simplicity that $\sigma$ contains no constant symbols.555Note,
however, that this assumption prevents us from encoding the distinguished
element of a pointed Kripke model by means of a constant symbol in the
signature. Hence, a $\sigma$-structure consists of a set $A$ together with,
for each relation symbol $R\in\sigma$ of arity $n$ (with $n$ an integer
greater than $0$), a subset $R^{A}\subseteq A^{n}$. A _homomorphism_ from a
$\sigma$-structure $A$ to a $\sigma$-structure $B$ is given by a function
$h\colon A\to B$ such that, for each $R\in\sigma$ of arity $n$ and
$(a_{1},\ldots,a_{n})\in A^{n}$,

$(a_{1},\ldots,a_{n})\in R^{A}\ \Longrightarrow\ (h(a_{1}),\ldots,h(a_{n}))\in
R^{B}.$

Our setting will be the category

$\mathbf{Struct}(\sigma)$

of $\sigma$-structures and their homomorphisms. Note that this is _not_ the
usual setting for classical model theory, which is mainly concerned with
morphisms that preserve and reflect the validity of first-order sentences,
such as elementary embeddings. Nevertheless, homomorphisms of relational
structures are pervasive in computer science, e.g. in databases, constraint
satisfaction and finite model theory, and also in combinatorics (in the study
of graphs and graph homomorphisms).

When dealing with modal logic, we will assume that $\sigma$ is a modal
signature and consider the category

$\mathbf{Struct}_{\bullet}(\sigma)$

of pointed Kripke models whose morphisms are the homomorphisms that preserve
the distinguished elements.

###  4.2. The modal comonad

For each pointed Kripke model $(A,a)\in\mathbf{Struct}_{\bullet}(\sigma)$, we
define a new model
$\mathbb{M}_{\omega}(A,a)\in\mathbf{Struct}_{\bullet}(\sigma)$ as follows. The
underlying set of $\mathbb{M}_{\omega}(A,a)$ consists of all finite paths in
$A$ starting from $a$:

$a\xrightarrow{R_{1}}a_{1}\xrightarrow{R_{2}}a_{2}\xrightarrow{\phantom{R_{3}}}\cdots\xrightarrow{R_{\ell}}a_{\ell}$

where $R_{1},\ldots,R_{\ell}$ are binary relation symbols in $\sigma$. These
finite paths can be thought of as plays in the bisimulation game. The
distinguished element of $\mathbb{M}_{\omega}(A,a)$ is the trivial path $[a]$
of length $0$, and the interpretation in $\mathbb{M}_{\omega}(A,a)$ of the
relation symbols is defined as follows:

  * •

If $P\in\sigma$ is a unary relation symbol, its interpretation consists of the
paths whose last element is in $P^{A}$.

  * •

If $R\in\sigma$ is a binary relation symbol, its interpretations consists of
the pairs of paths $(p,p^{\prime})$ such that $p^{\prime}$ is obtained by
extending $p$ by one step along $R$.

The pointed Kripke model $\mathbb{M}_{\omega}(A,a)$ is the _(full) unravelling
of_ $(A,a)$.

The assignment $(A,a)\mapsto\mathbb{M}_{\omega}(A,a)$ gives an object map from
$\mathbf{Struct}_{\bullet}(\sigma)$ to itself, and moreover we have
homomorphisms of pointed Kripke models

$\varepsilon_{(A,a)}\colon\mathbb{M}_{\omega}(A,a)\to(A,a)$

sending a path to its last element. The coextension operation associating with
a morphism $f\colon\mathbb{M}_{\omega}(A,a)\to(B,b)$ in
$\mathbf{Struct}_{\bullet}(\sigma)$ a morphism

$f^{*}\colon\mathbb{M}_{\omega}(A,a)\to\mathbb{M}_{\omega}(B,b)$

is defined recursively: $f^{*}$ sends the trivial path $(a)$ to $(b)$, and if
$p^{\prime}\in\mathbb{M}_{\omega}(A,a)$ is obtained by extending $p$ by one
step along $R$ to $a^{\prime}\in A$, then $f^{*}(p^{\prime})$ is the sequence
that extends $f^{*}(p)$ by one step along $R$ to $f(p^{\prime})$. These data
yield a comonad on the category $\mathbf{Struct}_{\bullet}(\sigma)$ of pointed
Kripke models:

###### Proposition 4.2.

$\mathbb{M}_{\omega}$ is a comonad on $\mathbf{Struct}_{\bullet}(\sigma)$.

Intuitively, the comonad $\mathbb{M}_{\omega}$ corresponds to the _infinite_
bisimulation game. It is often useful to consider resource-bounded variants of
this construction, where the length of paths is bounded; this corresponds to
considering finite bisimulation games. Accordingly, for each $k\in\mathbb{N}$,
we let $\mathbb{M}_{k}(A,a)$ be the submodel of $\mathbb{M}_{\omega}(A,a)$
defined by the paths of length at most $k$—this is known as the _$k$
-unravelling_ of $(A,a)$. The morphisms $\varepsilon_{(A,a)}$ and the
coextension operation above restrict to $\mathbb{M}_{k}(A,a)$ in the obvious
manner. In fact,

###### Proposition 4.3.

$\mathbb{M}_{k}$ is a comonad on $\mathbf{Struct}_{\bullet}(\sigma)$, for each
$k\in\mathbb{N}$.

We refer to the comonads $\mathbb{M}_{\omega}$ and $\mathbb{M}_{k}$ as _modal
comonads_. Modal comonads have an important property that is not shared by all
game comonads: they are _idempotent_ , meaning that the components of the
comultiplication
$\delta\colon\mathbb{M}_{\omega}\Rightarrow\mathbb{M}_{\omega}\mathbb{M}_{\omega}$
are isomorphisms. Informally, this can be understood as the fact that the
unravelling construction gives a universal way of constructing a tree-like
Kripke model from an arbitrary one, and applying this construction to a model
that is already tree-like yields nothing new. In particular,
$\mathbb{M}_{\omega}(A,a)$ is isomorphic to
$\mathbb{M}_{\omega}\mathbb{M}_{\omega}(A,a)$.

###### Remark 4.4.

Note that the unravelling $\mathbb{M}_{\omega}(A,a)$ can be infinite even if
$A$ is finite; e.g., the unravelling of a model with one node and one loop is
a countably infinite chain. On the other hand, for each $k\in\mathbb{N}$, the
$k$-unravelling $\mathbb{M}_{k}(A,a)$ is finite whenever $A$ is.

In the other direction, it is possible that $A$ is infinite but
$\mathbb{M}_{\omega}(A)$ is finite; e.g., take $A$ to be the disjoint union of
a node $a$ (the distinguished element) and an infinite chain not reachable
from $a$. In fact, the unravelling construction ignores all parts of a model
that are not reachable from its distinguished element.

###  4.3. The Ehrenfeucht–Fraïssé comonad

For each relational structure $A\in\mathbf{Struct}(\sigma)$, we define a new
structure $\mathbb{E}_{\omega}(A)$ whose underlying set consists of all non-
empty finite sequences of elements from $A$. This choice is motivated by the
fact that, while in the bisimulation game the players can only move along
accessibility relations, in the Ehrenfeucht–Fraïssé game they can move freely
within the structures.

As before, we denote by

$\varepsilon_{A}\colon\mathbb{E}_{\omega}(A)\to A,\ \
\varepsilon_{A}[a_{1},\ldots,a_{\ell}]\coloneqq a_{\ell}$

the map sending a sequence to its last element. If $R\in\sigma$ is a relation
symbol of arity $n$, then its interpretation in $\mathbb{E}_{\omega}(A)$
consists of the tuples $(s_{1},\ldots,s_{n})$ of sequences verifying the
following two conditions:

  * •

the sequences $s_{1},\ldots,s_{n}$ are pairwise comparable in the prefix order
(i.e., for all $i,j\in\\{1,\ldots,n\\}$, either $s_{i}$ is a prefix of $s_{j}$
or vice versa), and

  * •

$(\varepsilon_{A}(s_{1}),\ldots,\varepsilon_{A}(s_{n}))\in R^{A}$, i.e. the
last elements of the sequences are $R$-related in $A$.

It then follows that the $\varepsilon_{A}$ are homomorphisms. The coextension
operation sends a homomorphism $f\colon\mathbb{E}_{\omega}(A)\to B$ to the
homomorphism

$f^{*}\colon\mathbb{E}_{\omega}(A)\to\mathbb{E}_{\omega}(B),\ \
f^{*}[a_{1},\ldots,a_{\ell}]\coloneqq[b_{1},\ldots,b_{\ell}]$

where $b_{i}\coloneqq f[a_{1},\ldots,a_{i}]$ for all $1\leq i\leq\ell$.

###### Proposition 4.5.

$\mathbb{E}_{\omega}$ is a comonad on $\mathbf{Struct}(\sigma)$.

In a similar way to the modal case, the comonad $\mathbb{E}_{\omega}$
corresponds to the infinite Ehrenfeucht–Fraïssé game. To capture finite games,
for each $k\in\mathbb{N}$ we consider the submodel $\mathbb{E}_{k}(A)$ of
$\mathbb{E}_{\omega}(A)$ consisting of sequences of length at most $k$. With
the obvious restrictions of the morphisms $\varepsilon_{A}$ and of the
coextension operation, we have that

###### Proposition 4.6.

$\mathbb{E}_{k}$ is a comonad on $\mathbf{Struct}(\sigma)$, for each
$k\in\mathbb{N}$.

We refer to the comonads $\mathbb{E}_{\omega}$ and $\mathbb{E}_{k}$ as
_Ehrenfeucht–Fraïssé comonads_.

###### Remark 4.7.

The structure $\mathbb{E}_{\omega}(A)$ is always infinite whereas, for each
$k\in\mathbb{N}$, $\mathbb{E}_{k}(A)$ is finite if, and only if $A$ is finite.
The “only if” part of the latter statement follows from the fact that the
components of the counit

$\varepsilon_{A}\colon\mathbb{E}_{k}(A)\to A$

are surjective. This feature distinguishes the Ehrenfeucht–Fraïssé comonads
from the modal comonads, for which the components of the counit are generally
not surjective because their images cannot contain unreachable parts of the
model (or even parts of the model only reachable in more than $k$ steps, in
the case of the comonads $\mathbb{M}_{k}$).

###  4.4. The pebbling comonad

To encode pebble games, we follow the same pattern we adopted for bisimulation
and Ehrenfeucht–Fraïssé games. For each $n\in\mathbb{N}$, let
$\mathbf{n}\coloneqq\\{1,\ldots,n\\}$. For each relational structure
$A\in\mathbf{Struct}(\sigma)$, we define a structure
$\mathbb{P}_{n}(A)\in\mathbf{Struct}(\sigma)$ whose underlying set consists of
all non-empty finite sequences of elements from the Cartesian product of sets
$\mathbf{n}\times A$. An element $(p,a)\in\mathbf{n}\times A$ can be thought
of as the move in which pebble $p$ is placed on $a$, and a finite sequence of
such moves corresponds to a play in the $n$-pebble game. We refer to $p$ as
the _pebble index_ of the move $(p,a)$.

As before, we have a map

$\varepsilon_{A}\colon\mathbb{P}_{n}(A)\to A,\ \
\varepsilon_{A}[(p_{1},a_{1}),\ldots,(p_{\ell},a_{\ell})]\coloneqq a_{\ell}$

sending a play to the element selected in the last move. For each relation
symbol $R\in\sigma$ of arity $j$, its interpretation in $\mathbb{P}_{n}(A)$
consists of the tuples of moves $(s_{1},\ldots,s_{j})$ satisfying the
following properties:

  * •

the sequences $s_{1},\ldots,s_{j}$ are pairwise comparable in the prefix
order,

  * •

for all $i,i^{\prime}\in\\{1,\ldots,j\\}$, whenever $s_{i}$ is a prefix of
$s_{i^{\prime}}$, the pebble index of the last move in $s_{i}$ does not appear
in the suffix of $s_{i}$ in $s_{i^{\prime}}$,666That is, the pebble has not
been moved and is therefore still “active”. and

  * •

$(\varepsilon_{A}(s_{1}),\ldots,\varepsilon_{A}(s_{j}))\in R^{A}$.

With this definition, the functions $\varepsilon_{A}$ are homomorphisms. The
coextension operation is the same, mutatis mutandis, as with
$\mathbb{E}_{\omega}$. We have:

###### Proposition 4.8.

$\mathbb{P}_{n}$ is a comonad on $\mathbf{Struct}(\sigma)$, for each
$n\in\mathbb{N}$.

We refer to the comonads $\mathbb{P}_{n}$ as _pebbling comonads_.

###### Remark 4.9.

Since there is no bound on the length of plays, $\mathbb{P}_{n}(A)$ is always
infinite, even when $A$ is finite. This cannot be avoided: there is no comonad
that captures pebble games and sends finite structures to finite structures
(for a formal statement, see (Abramsky et al., 2017, Theorem 7)).

On the other hand, we can stratify $\mathbb{P}_{n}(A)$ by considering the
submodels defined by sequences of length at most $k$, for each
$k\in\mathbb{N}$; this corresponds to playing $k$-round $n$-pebble games. The
ensuing comonads $\mathbb{P}_{n,k}$ on $\mathbf{Struct}(\sigma)$ do restrict
to finite structures.

##  5\. The Kleisli category and the first logical equivalences

Game comonads provide a categorical view on a number of model-comparison
games, which in turn capture in a combinatorial fashion preservation of
corresponding logic fragments. In this section and in §7 below, we will see
how preservation of many logic fragments can be detected directly at the
categorical level. In this section we look at the _Kleisli categories_ for
game comonads, and show that two natural relations in these categories—the
homomorphism preorder and the isomorphism relation—capture preservation of
_existential positive_ fragments and extensions with _counting quantifiers_ ,
respectively. These results hold uniformly for the game comonads we have
introduced (Ehrenfeucht–Fraïssé, pebbling and modal comonads) and the
corresponding logical resources (quantifier rank, number of variables and
modal depth).

In §7 we will see that other logic fragments, including the full fragments
$\mathrm{FO}_{k}$, $\mathrm{FO}^{n}$ and $\mathrm{ML}_{k}$, can be captured
categorically by working in an enlargement of the Kleisli categories, namely
the categories of coalgebras for the comonads.

###  5.1. The Kleisli category

###### Definition 5.1.

Let $\mathbb{G}$ be a comonad on a category $\operatorname{\mathscr{C}}$. The
_Kleisli category of $\mathbb{G}$_, denoted by $\mathbf{Kl}(\mathbb{G})$, is
defined as follows:

  * •

$\mathrm{Ob}(\mathbf{Kl}(\mathbb{G}))\coloneqq\mathrm{Ob}(\operatorname{\mathscr{C}})$.

  * •

An arrow $A\to B$ in $\mathbf{Kl}(\mathbb{G})$, called a _Kleisli arrow_ , is
an arrow $\mathbb{G}A\to B$ in $\operatorname{\mathscr{C}}$.

The Kleisli identity $A\to A$ is the arrow
$\varepsilon_{A}\colon\mathbb{G}A\to A$ in $\operatorname{\mathscr{C}}$, and
the composite of Kleisli arrows $A\to B\to C$ is defined using the coextension
operation: given $f\colon\mathbb{G}A\to B$ and $g\colon\mathbb{G}B\to C$ in
$\operatorname{\mathscr{C}}$, we get $g\circ
f^{*}\colon\mathbb{G}A\to\mathbb{G}B\to C$.

The Kleisli category $\mathbf{Kl}(\mathbb{G})$ effectively considers the same
objects as $\operatorname{\mathscr{C}}$ but with a different notion of
morphism. For example, an arrow $A\to B$ in the Kleisli category
$\mathbf{Kl}(\mathbb{E}_{k})$ for the Ehrenfeucht–Fraïssé comonad is a
homomorphism of $\sigma$-structures

$\mathbb{E}_{k}(A)\to B.$

The structure $\mathbb{E}_{k}(A)$ consists of “explorations of depth at most
$k$” of $A$, and reflects the finite amount of resources available to the
players (in this case, the number of rounds). Hence, the passage from the
category $\mathbf{Struct}(\sigma)$ to the Kleisli category for a game comonad
(and, more generally, to the category of coalgebras) allows us to work in a
setting that is intrinsically resource-sensitive. For instance, we shall see
in §5.3 that Kleisli arrows encode preservation of resource-bounded
existential positive fragments. Before that, we briefly explain how to deal
with the equality symbol.

###  5.2. The equality symbol

In their basic form, game comonads allow us to capture fragments of logics
_without_ equality. This is sufficient for modal logic, since the image of the
standard translation is contained in the equality-free fragment of
$\mathrm{FO}$. On the other hand, to model logics _with_ equality, such as
$\mathrm{FO}_{k}$ and $\mathrm{FO}^{n}$ (and variations thereof), we can
proceed as follows.

Consider a (finite) relational signature $\sigma$, a fresh binary relation
symbol $I$ and the expanded signature

$\sigma^{I}\coloneqq\sigma\cup\\{I\\}.$

There is a fully faithful functor
$J\colon\mathbf{Struct}(\sigma)\to\mathbf{Struct}(\sigma^{I})$ that upgrades a
$\sigma$-structure to a $\sigma^{I}$-structure by interpreting $I$ as the
diagonal relation. This functor has a left adjoint
$H\colon\mathbf{Struct}(\sigma^{I})\to\mathbf{Struct}(\sigma)$ that sends a
$\sigma^{I}$-structure $A$ to the quotient $\underline{A}\,/{\sim}$, where
$\underline{A}$ is the $\sigma$-reduct of $A$ and $\sim$ is the equivalence
relation generated by $I^{A}$. Intuitively, the functor $J$ introduces (the
interpretation of) the equality symbol, while $H$ eliminates it. Because a
generic game comonad $\mathbb{G}$ is defined uniformly for any relational
signature, we can consider its variant $\mathbb{G}^{I}$ over
$\sigma^{I}$-structures:

${\mathbf{Struct}(\sigma)}$$\top$${\mathbf{Struct}(\sigma^{I})}$$\scriptstyle{J}$$\scriptstyle{H}$$\scriptstyle{\mathbb{G}^{I}}$

The composite

$\mathbb{G}^{=}\coloneqq H\circ\mathbb{G}^{I}\circ
J\colon\mathbf{Struct}(\sigma)\to\mathbf{Struct}(\sigma)$

is also a comonad, and it is the one that will allow us to capture logics with
equality.

Consider e.g. the Ehrenfeucht–Fraïssé comonad $\mathbb{E}_{k}$. Note that, for
any $\sigma$-structure $A$, the interpretation of the relation $I$ in the
$\sigma^{I}$-structure $\mathbb{E}_{k}^{I}J(A)$ consists of those pairs
$(s,t)$ of sequences of length at most $k$ of elements of $A$ such that (i)
$s,t$ are comparable in the prefix order $\sqsubseteq$ and (ii) their last
elements are equal. In other words, the relation $I^{\mathbb{E}_{k}^{I}J(A)}$
detects repeating sequences. Given $\sigma$-structures $A$ and $B$, Kleisli
morphisms

$\mathbb{E}_{k}^{=}(A)\to B$

are in bijection with morphisms

$\mathbb{E}_{k}^{I}J(A)\to J(B)$

(because $H\dashv J$), which in turn are in bijection with Kleisli morphisms
$f\colon\mathbb{E}_{k}(A)\to B$ such that

$\text{$\forall s,t\in\mathbb{E}_{k}(A)$, \ if $s\sqsubseteq t$ and
$\varepsilon_{A}(s)=\varepsilon_{A}(t)$ then $f(s)=f(t)$},$

called _$I$ -morphisms_. In the case of the pebbling comonad, $I$-morphisms
are defined in a similar fashion.

###### Remark 5.2.

There is a fully faithful functor

$\mathbf{Kl}(\mathbb{G}^{=})\to\mathbf{Kl}(\mathbb{G}^{I})$

that sends a $\sigma$-structure $A$ to $J(A)$. So, given any two
$\sigma$-structures $A$ and $B$, there exists an (iso)morphism $A\to B$ in
$\mathbf{Kl}(\mathbb{G}^{=})$ if, and only if, there exists an (iso)morphism
$J(A)\to J(B)$ in $\mathbf{Kl}(\mathbb{G}^{I})$.

The approach outlined above for encoding the equality symbol, whereby one
“composes” a game comonad with the adjunction $H\dashv J$, is equivalent to
the one based on $I$-morphisms introduced in (Abramsky et al., 2017; Abramsky
and Shah, 2021) and is a special case of the notion of _relative adjunction_
(Ulmer, 1968).

###  5.3. Existential positive fragments

An _existential positive_ formula is a formula that contains no negations and
no universal quantifiers. In the case of modal formulas, this amounts to
barring the use of the negation symbol and the modalities $\Box_{\alpha}$.
Given a class of first-order formulas $\mathcal{L}$ or, more generally, of
formulas in infinitary first-order logic $L_{\infty,\omega}$, we denote by

$\exists^{+}\mathcal{L}$

the subset of $\mathcal{L}$ consisting of the existential positive formulas.

The next result states that the homomorphism preorder in the Kleisli
categories of game comonads captures precisely preservation of the existential
positive fragments. In this case, we do not need to consider the variant
$\mathbb{G}^{=}$ of a game comonad $\mathbb{G}$ because the existential
positive fragments admit _equality elimination_ ; see Remark 5.5. Given a
logic fragment $\mathcal{L}$ and structures $A$ and $B$, we write

$A\Rrightarrow_{\mathcal{L}}B$

provided that $A\models\varphi$ implies $B\models\varphi$ for all
$\varphi\in\mathcal{L}$. (Hence, the equivalence relation
$\equiv_{\mathcal{L}}$ is the symmetrization of the preorder
$\Rrightarrow_{\mathcal{L}}$.)

###### Theorem 5.3 ((Abramsky et al., 2017; Abramsky and Shah, 2021)).

The following statements hold for each $k,n\in\mathbb{N}$ and (pointed)
structures $A,B$:

  1. (1)

$A\Rrightarrow_{\exists^{+}\mathrm{FO}_{k}}B$ if, and only if, there is an
arrow $A\to B$ in $\mathbf{Kl}(\mathbb{E}_{k})$.

  2. (2)

$A\Rrightarrow_{\exists^{+}L^{n}_{\infty,\omega}}B$ if, and only if, there is
an arrow $A\to B$ in $\mathbf{Kl}(\mathbb{P}_{n})$.

  3. (3)

$(A,a)\Rrightarrow_{\exists^{+}\mathrm{ML}_{k}}(B,b)$ if, and only if, there
is an arrow $(A,a)\to(B,b)$ in $\mathbf{Kl}(\mathbb{M}_{k})$.

###### Remark 5.4.

If $A,B$ are finite, the relation
$A\Rrightarrow_{\exists^{+}L^{n}_{\infty,\omega}}B$ in item 2 above can be
replaced with $A\Rrightarrow_{\exists^{+}\mathrm{FO}^{n}}B$ (cf. §3.3 and
(Kolaitis and Vardi, 1995, Corollary 4.9)).

We briefly illustrate the idea behind Theorem 5.3 in the case of
Ehrenfeucht–Fraïssé games; the same reasoning applies, mutatis mutandis, to
the other cases.

It is well know that the relation
$A\Rrightarrow_{\exists^{+}\mathrm{FO}_{k}}B$ holds precisely when Duplicator
wins the _existential positive_ variant of the $k$-round Ehrenfeucht–Fraïssé
game played between $A$ and $B$. In this game, Spoiler is forced to play in
$A$ and Duplicator responds in $B$. The winning condition, after $k$ rounds,
is that the relation

$\\{(a_{i},b_{i})\mid 1\leq i\leq k\\}$

determined by the chosen elements is a partial homomorphism (rather than a
partial isomorphism), i.e. the map $a_{i}\mapsto b_{i}$ yields a homomorphism
between the induced substructures of $A$ and $B$ determined, respectively, by
the sets $\\{a_{1},\ldots,a_{k}\\}$ and $\\{b_{1},\ldots,b_{k}\\}$.

In turn, Duplicator has a winning strategy in this game if, and only if, there
exists a homomorphism $f\colon\mathbb{E}_{k}(A)\to B$. Just observe that
specifying such an $f$ is the same as specifying its coextension
$f^{*}\colon\mathbb{E}_{k}(A)\to\mathbb{E}_{k}(B)$. In turn, a map
$\mathbb{E}_{k}(A)\to\mathbb{E}_{k}(B)$ can be regarded as a Duplicator
strategy in the existential positive game (associating with a sequence of
Spoiler’s moves the corresponding sequence of Duplicator’s responses), and the
winning condition amounts to saying that this map is a homomorphism.

###### Remark 5.5.

There is a subtlety here: suppose a homomorphism
$\mathbb{E}_{k}(A)\to\mathbb{E}_{k}(B)$ sends a sequence $[a_{1},a_{2},a_{1}]$
to $[b_{1},b_{2},b_{3}]$ with $b_{1}\neq b_{3}$. This prevents the relation
$\\{(a_{1},b_{1}),(a_{2},b_{2}),(a_{1},b_{3})\\}$ from being functional, and
so it does _not_ define a Duplicator winning strategy. Yet, we can obtain a
Duplicator winning strategy by imposing that, if Spoiler plays the same
element twice (or more), Duplicator repeats their answer.

This issue can be solved by considering only the $I$-morphisms instead of all
Kleisli morphisms. In fact, there is a _bijection_ between $I$-morphisms
$\mathbb{E}_{k}(A)\to B$ (equivalently, Kleisli morphisms
$\mathbb{E}_{k}^{=}(A)\to B$) and Duplicator winning strategies in the
existential positive $k$-round Ehrenfeucht–Fraïssé game.

In logical terms, the reason why Theorem 5.3 holds in the form stated, with no
need to consider the comonads $\mathbb{G}^{=}$, is that the existential
positive fragments admit equality elimination. For example, in
$\exists^{+}\mathrm{FO}_{k}$ the only atomic (sub)formulas using the equality
symbol are those of the form $x=y$ with $x,y$ variables, and these can be
eliminated by substituting one variable for the other in the appropriate way.
A similar reasoning applies to the pebbling comonad.

Let us mention that the existential positive variant of pebble games was first
studied in (Kolaitis and Vardi, 1995) where it is called “existential pebble
game”, while the existential positive variant of bisimulation games is known
as the _simulation game_.

###  5.4. Fragments with counting quantifiers

In §5.3, we saw that the homomorphism preorder in the Kleisli categories for
game comonads captures preservation of existential positive fragments. We
shall now look at another natural relation between objects of the Kleisli
categories, namely the isomorphism relation.

If $\mathcal{L}$ is a class of first-order formulas, we write

$\mathcal{L}(\\#)$

for the extension of $\mathcal{L}$ with _counting quantifiers_. That is, for
each $i\in\mathbb{N}$ we add a quantifier $\exists_{\geq i}$ such that a
sentence $\exists_{\geq i}x.\varphi(x)$ is satisfied in a structure $A$ if,
and only if, there are at least $i$ elements of $A$ witnessing the fact that
$\varphi(x)$ is satisfiable in $A$. In the case of modal formulas, we add
_graded modalities_ $\Diamond_{\alpha}^{i}$ such that
$\Diamond_{\alpha}^{i}\varphi$ holds in a pointed Kripke model $(A,a)$ if, and
only if, the are at least $i$ elements of $A$ that are accessible from $a$
through $R_{\alpha}$ and satisfy $\varphi$.

We will restrict ourselves to the class of finite structures. In this case,
the isomorphism relation in the Kleisli category captures equivalence in the
counting extensions of the logic fragments:

###### Theorem 5.6 ((Abramsky et al., 2017; Abramsky and Shah, 2021)).

The following statements hold for each $k,n\in\mathbb{N}$ and finite (pointed)
structures $A,B$:

  1. (1)

$A\equiv_{\mathrm{FO}_{k}(\\#)}B$ if, and only if, there is an isomorphism
$A\cong B$ in $\mathbf{Kl}(\mathbb{E}_{k}^{=})$.

  2. (2)

$A\equiv_{\mathrm{FO}^{n}(\\#)}B$ if, and only if, there is an isomorphism
$A\cong B$ in $\mathbf{Kl}(\mathbb{P}_{n}^{=})$.

  3. (3)

$(A,a)\equiv_{\mathrm{ML}_{k}(\\#)}(B,b)$ if, and only if, there is an
isomorphism $(A,a)\cong(B,b)$ in $\mathbf{Kl}(\mathbb{M}_{k})$.

The previous result makes use of the fact that equivalence in the logics with
counting quantifiers $\mathrm{FO}_{k}(\\#)$, $\mathrm{FO}^{n}(\\#)$ and
$\mathrm{ML}_{k}(\\#)$ are known to be captured by variants of the usual
Ehrenfeucht–Fraïssé, pebble and bisimulation games that consider _bijections_
between structures.

For example, the _bijective Ehrenfeucht–Fraïssé game_ (Hella, 1996) played
between finite structures $A$ and $B$ proceeds as follows. If $A$ and $B$ have
different cardinalities, Duplicator loses the game. Otherwise, at round $i$,
Duplicator choses a bijection ${f_{i}\colon A\to B}$ and Spoiler responds by
choosing an element $a_{i}\in A$. After $k$-rounds, Duplicator wins if the
relation $\\{(a_{i},f_{i}(a_{i}))\mid 1\leq i\leq k\\}$ is a partial
isomorphism. We have $A\equiv_{\mathrm{FO}_{k}(\\#)}B$ if, and only if,
Duplicator has a winning strategy in this $k$-round game. In turn, such a
winning strategy induces arrows $A\to B$ and $B\to A$ in
$\mathbf{Kl}(\mathbb{E}_{k})$ that are inverse to each other and, conversely,
any isomorphism between $A$ and $B$ in $\mathbf{Kl}(\mathbb{E}_{k})$ induces a
Duplicator winning strategy.

Similarly, the fragments $\mathrm{FO}^{n}(\\#)$ and $\mathrm{ML}_{k}(\\#)$ are
captured, respectively, by _bijective $n$-pebble games_ (Hella, 1996) and
$k$-round _graded bisimulation games_ (cf. e.g. (Abramsky and Shah, 2021,
§5.3) or (Otto, 2023)). Let us point out that, in the case of the pebbling
comonad, we do not need to consider the infinitary extension of
$\mathrm{FO}^{n}(\\#)$ with arbitrary conjunctions and disjunctions because,
as with classical pebble games, the bijective $n$-pebble game between _finite_
structures is determined by a $k$-round strategy for $k$ large enough.

##  6\. Coalgebras and combinatorial parameters

###  6.1. Coalgebras, forest covers and combinatorial parameters of structures

In this section, we consider the categories of Eilenberg–Moore coalgebras for
game comonads and show that they encode in a structural way combinatorial
parameters of structures. We start by recalling the notion of coalgebra for a
comonad; the passage from the Kleisli category of a comonad to its
Eilenberg–Moore category can be understood, dually, as an abstraction of the
passage from free groups to all groups.

###### Definition 6.1.

Let $\mathbb{G}$ be a comonad on a category $\operatorname{\mathscr{C}}$. A
_coalgebra for $\mathbb{G}$_ (also called a _$\mathbb{G}$ -coalgebra_) is a
pair $(A,\alpha)$ where $A$ is an object of $\operatorname{\mathscr{C}}$ and
$\alpha$ is a _coalgebra structure on $A$_, i.e. an arrow $\alpha\colon
A\to\mathbb{G}A$ making the following diagrams commute:

${A}$${\mathbb{G}A}$${\mathbb{G}A}$${\mathbb{G}\mathbb{G}A}$$\scriptstyle{\alpha}$$\scriptstyle{\alpha}$$\scriptstyle{\delta_{A}}$$\scriptstyle{\mathbb{G}\alpha}$${A}$${\mathbb{G}A}$${A}$$\scriptstyle{\alpha}$$\scriptstyle{\mathrm{id}_{A}}$$\scriptstyle{\varepsilon_{A}}$

A _coalgebra morphism_ $(A,\alpha)\to(B,\beta)$ is an arrow $h\colon A\to B$
in $\operatorname{\mathscr{C}}$ compatible with the coalgebra structures,
meaning that $\beta\circ h=\mathbb{G}h\circ\alpha$. The _Eilenberg–Moore
category of $\mathbb{G}$_, denoted by $\mathbf{EM}(\mathbb{G})$, is the
category consisting of $\mathbb{G}$-coalgebras and their morphisms.

There is an obvious forgetful functor
$L\colon\mathbf{EM}(\mathbb{G})\to\operatorname{\mathscr{C}}$ that forgets the
coalgebra structures. In the converse direction, there is a functor
$F\colon\operatorname{\mathscr{C}}\to\mathbf{EM}(\mathbb{G})$ that sends an
object $A$ of $\operatorname{\mathscr{C}}$ to the _co-free coalgebra
$(\mathbb{G}A,\delta_{A})$ over $A$_. These functors form an adjunction

(1)
${\operatorname{\mathscr{C}}}$$\top$${\mathbf{EM}(\mathbb{G})}$$\scriptstyle{F}$$\scriptstyle{L}$

such that $L\circ F=\mathbb{G}$; this is the _Eilenberg–Moore adjunction_
associated with $\mathbb{G}$. Moreover, the Kleisli category
$\mathbf{Kl}(\mathbb{G})$ is isomorphic to the full subcategory of
$\mathbf{EM}(\mathbb{G})$ defined by the co-free coalgebras, via the functor
sending a Kleisli arrow $f\colon\mathbb{G}A\to B$ to its coextension
$f^{*}\colon\mathbb{G}A\to\mathbb{G}B$.

An important feature of game comonads is that they are defined uniformly with
respect to the resource parameters; in fact, they are _graded comonads_ , with
grades provided by the monoid $\mathbb{N}\cup\\{\infty\\}$ with the $\min$
operation. In particular, the resource-indexing allows us to define a notion
of _coalgebra number_ :

###### Definition 6.2.

Consider a sequence of comonads $(\mathbb{G}_{k})_{k\in\mathbb{N}}$ on a
category $\operatorname{\mathscr{C}}$. For each object $A$ of
$\operatorname{\mathscr{C}}$, the _coalgebra number_ of $A$, if it exists, is
the least $\ell\in\mathbb{N}$ such that $A$ admits a
$\mathbb{G}_{\ell}$-coalgebra structure $\alpha\colon A\to\mathbb{G}_{\ell}A$.

####  6.1.1. Coalgebras for the modal comonad

The modal comonads $\mathbb{M}_{k}$ are idempotent, hence the Eilenberg–Moore
categories $\mathbf{EM}(\mathbb{M}_{k})$ can be identified with full
(coreflective) subcategories of $\mathbf{Struct}_{\bullet}(\sigma)$.
Intuitively, this means that coalgebra structures for $\mathbb{M}_{k}$ are a
property of Kripke models, rather than extra structure; in particular, a
Kripke model admits at most one $\mathbb{M}_{k}$-coalgebra structure. To make
this precise, we recall the following notion.

###### Definition 6.3.

A _synchronization tree_ is a pointed Kripke model
$(A,a)\in\mathbf{Struct}_{\bullet}(\sigma)$ such that, for each $a^{\prime}\in
A$ distinct from $a$, there is a unique finite path from $a$ to $a^{\prime}$:

$a\xrightarrow{R_{1}}a_{1}\xrightarrow{R_{2}}a_{2}\xrightarrow{\phantom{R_{3}}}\cdots\xrightarrow{R_{\ell}}a^{\prime}.$

If each such path has length at most $k$, we say that the synchronization tree
has _height at most $k$_.

If $(A,a)$ is a synchronization tree of height at most $k$, we can define a
coalgebra structure $\alpha\colon(A,a)\to\mathbb{M}_{k}(A,a)$ as follows:

  * •

$\alpha(a)$ is the one-element sequence $[a]$, and

  * •

for each $a^{\prime}\in A$ distinct from $a$, $\alpha(a^{\prime})$ is the
unique path from $a$ to $a^{\prime}$.

In fact, it turns out that a Kripke model admits an $\mathbb{M}_{k}$-coalgebra
structure if, and only if, it a synchronization tree of height at most $k$.
This leads to the following characterisation of the Eilenberg–Moore categories
$\mathbf{EM}(\mathbb{E}_{k})$:

###### Theorem 6.4.

$\mathbf{EM}(\mathbb{M}_{k})$ is isomorphic to the full subcategory of
$\mathbf{Struct}_{\bullet}(\sigma)$ consisting of synchronization trees of
height at most $k$.

The Eilenberg–Moore adjunction in eq. (1) specialises to an adjunction

${\mathbf{Struct}_{\bullet}(\sigma)}$$\top$${\mathbf{EM}(\mathbb{M}_{k}).}$$\scriptstyle{F}$$\scriptstyle{L}$

By Theorem 6.4, we can identify $L$ with the inclusion of the subcategory of
synchronization trees of height $\leq k$, and $F$ sends a pointed Kripke model
to its $k$-unravelling.

Another way of looking at this is to say that the coalgebra structures are
“definable” and thus preserved by homomorphisms of Kripke models. To make
these definable structures explicit, we introduce the following terminology.

###### Definition 6.5.

Let $(X,\leq)$ be a poset.

  * •

We say that $(X,\leq)$ is a _forest_ if, for each $x\in X$, the down-set

${\downarrow}\,x\coloneqq\\{x^{\prime}\in X\mid x^{\prime}\leq x\\}$

is finite and linearly ordered by $\leq$. A minimal element of a forest is
called a _root_. A forest with exactly one root is a _tree_.

  * •

If $(X,\leq)$ is a forest, the _height_ of an element $x\in X$ is
$\operatorname{\mathrm{ht}}(x)\coloneqq|{\downarrow}\,x|-1$, and the height of
$(X,\leq)$ is $\sup{\\{\operatorname{\mathrm{ht}}(x)\mid x\in X\\}}$.

  * •

A _forest morphism_ is a monotone map between forests that preserves the
height of elements.

###### Remark 6.6.

The category of forests and forest morphisms between them is equivalent to its
full subcategory defined by the _non-empty_ trees. In one direction, a forest
is sent to the tree obtained by adding a new root, and in the other direction
we remove the unique root of a non-empty tree.

Given a synchronization tree $(A,a)$, consider the binary relation $\prec$ on
$A$ defined, for each $x,y\in A$, by

(M) $x\prec y\ \Longleftrightarrow\ R_{\alpha}(x,y)\ \text{ for a unique
$R_{\alpha}\in\sigma$}.$

The reflexive transitive closure $\leq$ of $\prec$ is a tree order on $A$
whose root is $a$; in fact, $\prec$ is the _covering relation_ associated with
$\leq$.777Given a partial order $\leq$, the associated covering relation
$\prec$ is defined by $x\prec y$ if, and only if, $x<y$ and there is no $z$
such that $x<z<y$. From this standpoint, an $\mathbb{M}_{k}$-coalgebra
structure on a pointed Kripke model $(A,a)$ is the same thing as a tree order
$\leq$ of height at most $k$ on $A$ such that $a$ is the root of the tree and
the associated covering relation $\prec$ satisfies condition (M) above.
Clearly, there is at most one such tree order on $A$. Moreover, homomorphisms
of Kripke models preserve these tree orders; i.e., a homomorphism of Kripke
models between synchronization trees is a forest morphism with respect to the
corresponding tree orders.

In the case of the modal comonads, the coalgebra number is simply the height
of a synchronization tree.

####  6.1.2. Coalgebras for the Ehrenfeucht–Fraïssé comonad

The Ehrenfeucht–Fraïssé comonads are not idempotent, so coalgebras for
$\mathbb{E}_{k}$ carry extra structure that need not be preserved by
homomorphisms of relational structures. As suggested by the case of coalgebras
for the modal comonads, this extra structure consists of a “compatible” forest
order. We thus define the category of _forest-ordered structures_ , denoted by

$\mathscr{R}(\sigma).$

Its objects are pairs $(A,\leq)$ where $A\in\mathbf{Struct}(\sigma)$ and
$\leq$ is a forest order on $A$, and morphisms are homomorphisms of
$\sigma$-structures that are also forest morphisms.

In order to specify the relevant notion of compatibility between the forest
order and the relations on a structure, it is convenient to use the concept of
Gaifman graph:

###### Definition 6.7.

The _Gaifman graph_ associated with a structure $A\in\mathbf{Struct}(\sigma)$
is the undirected graph $\mathfrak{G}(A)$ defined as follows:

  * •

the vertices of $\mathfrak{G}(A)$ are the elements of $A$;

  * •

vertices $a,b$ are adjacent in $\mathfrak{G}(A)$ if they are distinct and
appear in a tuple of related elements in $A$.

Given a forest-ordered structure $(A,\leq)$, the compatibility condition for
$\mathbb{E}_{k}$-coalgebras is the following:

(E) $\forall a,b\in A,\text{ if $a,b$ are adjacent in $\mathfrak{G}(A)$ then
they are comparable in the order $\leq$}.$

###### Theorem 6.8.

$\mathbf{EM}(\mathbb{E}_{k})$ is isomorphic to the full subcategory of
$\mathscr{R}$ defined by the forest-ordered structures of height at most $k$
satisfying condition (E).

The previous result entails that, in the Eilenberg–Moore adjunction

${\mathbf{Struct}(\sigma)}$$\top$${\mathbf{EM}(\mathbb{E}_{k})}$$\scriptstyle{F}$$\scriptstyle{L}$

obtained by specialising eq. (1), we can identify $L$ with the functor
forgetting the forest order, while $F$ sends a structure $A$ to the forest-
ordered structure $(\mathbb{E}_{k}(A),\sqsubseteq)$, where $\sqsubseteq$ is
the prefix order. In contrast to the modal case, the forest order of an
Ehrenfeucht–Fraïssé coalgebra is not determined by its underlying relational
structure.

Theorem 6.8 tells us, in particular, that $\mathbb{E}_{k}$-coalgebra
structures on $A\in\mathbf{Struct}(\sigma)$ are in bijection with _forest
covers_ of $A$ (i.e., forest orders on $A$ satisfying (E)) of height at most
$k$. The least height of a forest cover of $A$, referred to as the _tree-
depth_ of $A$, is an important combinatorial parameter of structures which was
first introduced for graphs in (Nešetřil and Ossona de Mendez, 2006). Thus, an
$\mathbb{E}_{k}$-coalgebra structure on $A$ is a witness to the fact that the
tree-depth of $A$ is at most $k$. This yields:

###### Proposition 6.9.

For the Ehrenfeucht–Fraïssé comonads $\mathbb{E}_{k}$, the coalgebra number of
a structure $A\in\mathbf{Struct}(\sigma)$ coincides with the tree-depth of
$A$.

####  6.1.3. Coalgebras for the pebbling comonad

To characterise the categories of Eilenberg–Moore coalgebras for the pebbling
comonads $\mathbb{P}_{n}$, we consider a slight variant of the category
$\mathscr{R}$ of forest-ordered structures that takes into account the
presence of pebbles. For each positive integer $n$, we define the category

$\mathscr{R}^{(n)}$

of _$n$ -pebble forest-ordered structures_: the objects are tuples
$(A,\leq,p)$ such that $(A,\leq)$ is a forest-ordered structure and $p\colon
A\to\mathbf{n}$ is a map, called _pebbling function_ , assigning to each
element of $A$ an integer between $1$ and $n$; the morphisms in
$\mathscr{R}^{(n)}$ are the morphisms of forest-ordered structures that also
preserve the pebbling functions.

For an $n$-pebble forest-ordered structure $(A,\leq,p)$, the compatibility
between the order and the pebbling function is captured by the following
condition:

(P) $\begin{split}\forall a,b\in A,\ \ &\text{if $a,b$ are adjacent in
$\mathfrak{G}(A)$ and $a<b$ in the forest order},\\\ &\text{then $p(a)\neq
p(x)$ for all $x\in A$ such that $a<x\leq b$}.\end{split}$

###### Theorem 6.10.

$\mathbf{EM}(\mathbb{P}_{n})$ is isomorphic to the full subcategory of
$\mathscr{R}^{(n)}$ defined by the $n$-pebble forest-ordered structures
satisfying conditions (E) and (P).

The previous result allows us to give a concrete description of the
Eilenberg–Moore adjunction between $\mathbf{Struct}(\sigma)$ and
$\mathbf{EM}(\mathbb{P}_{n})$: the left adjoint
$L\colon\mathbf{EM}(\mathbb{P}_{n})\to\mathbf{Struct}(\sigma)$ forgets both
the forest orders and the pebbling functions, whereas the right adjoint
$F\colon\mathbf{Struct}(\sigma)\to\mathbf{EM}(\mathbb{P}_{n})$ sends a
structure $A$ to $(\mathbb{P}_{n}(A),\sqsubseteq,p)$ where the pebbling
function $p\colon\mathbb{P}_{n}(A)\to\mathbf{n}$ sends a sequence
$[(p_{1},a_{1}),\ldots,(p_{\ell},a_{\ell})]$ to $p_{\ell}$.

It follows from Theorem 6.10 that $\mathbb{P}_{n}$-coalgebra structures on
$A\in\mathbf{Struct}(\sigma)$ are in bijection with _$n$ -pebble forest
covers_ of $A$, i.e. pairs of forest orders and pebbling functions on $A$
satisfying (E) and (P). Furthermore, it turns out that $A$ admits an
$n$-pebble forest cover if, and only if, it admits a _tree decomposition of