Stefan Milius and Thorsten Wißmann

# Finitary Corecursion for the
Infinitary Lambda Calculus111This work is supported by the Deutsche
Forschungsgemeinschaft (DFG) under project MI 717/5-1

Stefan Milius  Lehrstuhl für Theoretische Informatik, FAU Erlangen-Nürnberg,
Germany  Thorsten Wißmann  Lehrstuhl für Theoretische Informatik, FAU
Erlangen-Nürnberg, Germany

###### Abstract.

Kurz et al. have recently shown that infinite λ-trees with finitely many free
variables modulo α-equivalence form a final coalgebra for a functor on the
category of nominal sets. Here we investigate the rational fixpoint of that
functor. We prove that it is formed by all rational λ-trees, i.e. those
λ-trees which have only finitely many subtrees (up to isomorphism). This
yields a corecursion principle that allows the definition of operations such
as substitution on rational λ-trees.

###### Key words and phrases:

rational trees, infinitary lambda calculus, coinduction

###### 1991 Mathematics Subject Classification:

F.3.2 Semantics of Programming Languages, F.4.1 Mathematical Logic, D.3.1
Formal Definitions and Theory

##  1\. Introduction

One of the most important concepts in computer science is the
$\lambda$-calculus. It is a very simple notion of computation because its
syntax consists only of three constructs: variables, $\lambda$-abstraction and
function application, and its semantics consists of only two concepts
$\alpha$-conversion for renaming of bound variables and $\beta$-conversion for
executing function applications. Yet it is very powerful since it is Turing
complete and allows to define many notions of higher level programming
languages such as booleans, if-then-else, natural numbers, arithmetic
operations, lists including mapping and folding, recursion etc.222Depending on
the application a third semantic concept, $\eta$ conversion, may be of
interest. But this is neither needed for Turing completeness nor for our work.

However, whenever one wants to deal with inductive and coinductive definitions
in the presence of variable binding subtle issues arise and one has to be
careful not to mess up the variable binding. One solution to these problems
has been proposed by Gabbay and Pitts [12]. They use _nominal sets_ as a
framework for dealing with binding operators, abstraction and structural
induction. Nominal sets go back to Fraenkel’s and Mostowski’s permutation
model for set theory devised in the 1920s and 1930s. They are sets equipped
with an action of the group of finite permutations on a given fixed set
$\mathcal{V}$ of atoms (here these play the role of variables). For an
arbitrary nominal set one can then define the notions of “free” and “bound”
variables using the notion of support (we recall this in Section 2.2). Gabbay
and Pitts then consider the functor

$L_{\alpha}X=\mathcal{V}+[\mathcal{V}]X+X\times X$

expressing the type of the term constructors of the $\lambda$-calculus (note
that the abstraction functor $[\mathcal{V}]X$ is a quotient of
$\mathcal{V}\times X$ modulo renaming “bound” variables). And they prove that
the initial algebra for $L_{\alpha}$ is formed by all $\lambda$-terms modulo
$\alpha$-equivalence.

Recently, Kurz et al. [18] have characterized the final coalgebra for
$L_{\alpha}$ (and more generally, for functors arising from so-called binding
signatures): it is carried by the set of all infinitary $\lambda$-terms (i.e.
finite or infinite $\lambda$-trees) with finitely many free variables modulo
$\alpha$-equivalence. This then allows to define operations on infinitary
$\lambda$-terms by coinduction, for example substitution and operations that
assign to an infinitary $\lambda$-term its normal form computations (e.g. the
Böhm, Levy-Longo, and Berarducci trees of a given infinitary $\lambda$-term).

Our contribution in this paper is to give a characterization of the _rational
fixpoint_ of the functor $L_{\alpha}$. In general, the rational fixpoint for a
functor $F$ lies between the initial algebra and the final coalgebra for $F$.
If one thinks of it as a coalgebra, it is characterized as the final locally
finitely presentable $F$-coalgebra. Intuitively, one may think of it as
collecting all behaviours of “finite” (more technically, finitely presentable
carried) $F$-coalgebras. Examples include regular languages, eventually
periodic and rational streams, rational formal power-series etc. For a
polynomial endofunctor $F_{\Sigma}$ on sets associated to the signature
$\Sigma$, the rational fixpoint consists of regular $\Sigma$-trees of Elgot
[10], i.e. those (finite and infinite) $\Sigma$-trees having only finitely
many different subtrees (up to isomorphism). We will prove in Section 3 that
the rational fixpoint for $L_{\alpha}$ on $\mathsf{Nom}$ is carried by all
rational $\lambda$-trees modulo $\alpha$-equivalence. Before that we recall in
Section 2 preliminaries on the infinitary $\lambda$-calculus, nominal sets and
the rational fixpoint. The finality principle of the rational fixpoint may be
understood as a finitary corecursion principle. In Section 4 we show
applications of our main result, in particular, that the coinductive
definition of substitution given in [18] restricts to rational trees. We also
discuss coinductive definitions concerning normal form computations. We
conclude in Section 5.

Related work. The work presented here is based on the second author’s student
project reported in [27].

A related approach to variable binding operations which uses presheaves over
finite sets was proposed by Fiore, Plotkin and Turi [11]. By now this has
developed into a respectable body of work by these and other authors. Most
related to our work here is the coinductive approach to infinitary and
rational $\lambda$-terms studied by Adámek, Milius and Velebil [3]. This work
considers an endofunctor very similar to $L_{\alpha}$ but on the category of
presheafes on finite sets. Its final coalgebra is shown to be the presheaf of
all infinite $\lambda$-trees and the rational fixpoint the presheaf of all
rational trees – each of them modulo $\alpha$-equivalence.

##  2\. Preliminaries

We assume that readers are familiar with basic notions of category theory and
with algebras and coalgebras for an endofunctor. For a given endofunctor $F$
on the category $\mathcal{C}$ we will write $t:\nu F\to F(\nu F)$ for the
final coalgebra (assuming that it exists). Given an $F$-coalgebra $(C,c)$ we
write $c^{\dagger}:(C,c)\to(\nu F,t)$ for the unique $F$-coalgebra
homomorphism from $C$ to $\nu F$. The category of coalgebras for an
endofunctor $F$ is denoted by ${\mathsf{Coalg}}\,F$. For introductory texts on
coalgebras see [25, 16, 1].

We will now give some background on the (infinitary) $\lambda$-calculus, on
nominal sets and on the rational fixpoint of a functor as needed in the
present paper.

###  2.1. Infinitary $\lambda$-Calculus and Rational Trees

Before we talk about infinitary $\lambda$-terms (aka $\lambda$-trees) first
recall that ordinary $\lambda$-terms are defined starting from a fixed
countable set of variables $\mathcal{V}$ by the grammar

$T::=x\mid\lambda x.T\mid TT,$

where $x$ ranges over $\mathcal{V}$. We denote the set of all $\lambda$-terms
by $\Lambda$. Free and bound variables and substitution are defined as usual
with the operator $\lambda x.(-)$ binding $x$ in its argument. Often one
considers $\lambda$-terms modulo _$\alpha$ -equivalence_, i.e., the least
equivalence relation on $\lambda$-terms identifying two terms that arise by
consistently renaming bound variables. One can think of a term $\lambda x.T$
as representing a computation that takes a parameter $P$ that is used in all
free occurences of $x$ in $T$. Hence, the main computation rule of the
$\lambda$-calculus is $\beta$-reduction, i.e. the rule

$(\lambda x.T)P\to_{\beta}T[x\mapsto P].$

For example we have $(\lambda x.\lambda y.x)\,a\,b\rightarrow_{\beta}(\lambda
y.a)\,b\rightarrow_{\beta}a$, where $a$ cannot be reduced further. However,
terms may have infinite reduction sequences; a prominent example is $Yf$ for
the $Y$-combinator defined as $Y:=\lambda g.(\lambda x.g(x\,x))\,(\lambda
x.g(x\,x))$ we have:

$\displaystyle Yf$ $\displaystyle=(\lambda g.(\lambda x.g(x\,x))\,(\lambda
x.g(x\,x)))f$ $\displaystyle\rightarrow_{\beta}(\lambda x.f(x\,x))\,(\lambda
x.f(x\,x))\rightarrow_{\beta}f((\lambda x.f(x\,x))\,(\lambda x.f(x\,x)))$
$\displaystyle\rightarrow_{\beta}f(f((\lambda x.f(x\,x))\,(\lambda
x.f(x\,x))))\rightarrow_{\beta}\cdots$

Informally speaking, this “converges” to the infinite term $f(f(f(\cdots)))$.
If one takes such infinite terms as legal objects of the $\lambda$-calculus
one is led to _infinitary_ $\lambda$-calculus. There one replaces
${\lambda}$-terms by (finite and infinite) $\lambda$-trees. A _$\lambda$
-tree_ is a rooted and ordered tree with leaves labelled by variables in
$\mathcal{V}$ and with two sorts of inner nodes: nodes with one successor
labelled by $\lambda x$ for some variable $x\in\mathcal{V}$ and nodes with two
successors labelled by $@$. For example, we have the $\lambda$-trees

@${\lambda}x$@$x$$x$${\lambda}x$@$x$$x$ @$f$@$f$@$f$$\ddots$ (2.1)

representing the $\lambda$-term $({\lambda}x.xx)({\lambda}x.xx)$ and the
infinite term $f(f(f(\cdots)))$, respectively. Let $\Lambda^{\infty}$ be the
set of all $\lambda$-trees. The notions of free and bound variables of a
$\lambda$-tree are clear: a variable $x$ is bound in a $\lambda$-tree $t$ if
there is a path from a leave labelled by $x$ to the root of $t$ that contains
a node labelled by $\lambda x$, and $x$ is free in $t$ if there is a path from
an $x$-labelled leaf to the root of $t$ that does not contain any node
labelled by ${\lambda}x$.

The classic approach to defining operations such a substitution on
$\lambda$-trees uses that $\Lambda^{\infty}$ is the metric completion of
$\Lambda$ under a natural metric; this idea of using a metric approach to
dealing with infinite trees goes at least back to Arnold and Nivat [5]. Thus,
every infinite $\lambda$-tree is regarded as the limit of the Cauchy sequence
of its truncations at level $n$. Notions such as $\alpha$-equivalence and
substitution of $\lambda$-trees are then defined by extending the
corresponding notions on finite $\lambda$-trees (i.e. $\lambda$-terms)
continuously. More concretely, two $\lambda$-trees $s$ and $t$ are
$\alpha$-equivalent iff for every natural number $n$ the pair of truncations
at level $n$ of $s$ and $t$ are $\alpha$-equivalent $\lambda$-terms (see [18,
Definition 5.17]).

Our aim in this paper is to give a coalgebraic characterization of an
important subclass of all $\lambda$-trees, the so called _rational_
$\lambda$-trees. The following definition follows Ginali’s characterization
[15] of regular $\Sigma$-trees for a signature $\Sigma$:

######  Definition 2.1.

A $\lambda$-tree having only finitely many subtrees (up to isomorphism) is
called _rational_. A $\lambda$-tree modulo $\alpha$-equivalence, i.e. an
$\alpha$-equivalence class of $\lambda$-trees, is called _rational_ if it
contains at least one rational $\lambda$-tree.

Intuitively, the rational $\lambda$-trees are those $\lambda$-trees that admit
a finite representation as a $\lambda$-tree with “uplinks”. All finite
$\lambda$-trees are, of course, rational, and so is the right-hand
$\lambda$-tree in (2.1). Other examples are in Figure 1.

@$f$ | @$f$@$f$ | ${\lambda}x$@${\lambda}x$@$x$ | @${\lambda}x$@${\lambda}y$$y$$x$ | ${\lambda}x$${\lambda}y$@
---|---|---|---|---
Figure 1. Finite representations of rational $\lambda$-trees

The uplink from some node $s$ to some other node $r$ indicates that the entire
tree starting at $r$ occurs as a subtree of $s$. In other words, such a
$\lambda$-tree with uplinks represents its tree unravelling, i.e. the first
and second tree on the left both represent the rational infinite
$\lambda$-tree shown in (2.1) on the right.

Things get more complicated, if abstractions come into play, as in the third
tree. Here the $x$ clearly refers to the ${\lambda}x$ in the root, but some of
the “copies” of $x$ are bound by the ${\lambda}x$ in the left branch and other
copies are bound to the abstraction in the root. Something similar can be
observed in the last but one tree, which has two free variables $x,y$, but all
“copies” of $x$ and $y$ are bound by the previous copy of ${\lambda}x$ and
${\lambda}y$ respectively. Finally, the rightmost tree represents a
$\lambda$-tree that consists of applications and abstractions only:

${\lambda}xy.({\lambda}y{\lambda}y\ldots)({\lambda}xy.({\lambda}y{\lambda}y\ldots)({\lambda}xy.({\lambda}y{\lambda}y\ldots)\ldots)).$

###  2.2. Nominal Sets

It was the idea of Gabbay and Pitts [12] to use nominal sets as a category-
theoretic framework in which to describe $\lambda$-terms modulo
$\alpha$-equivalence as the initial algebra for a functor $L_{\alpha}$. One
can then use its universal property to define operations such as substitution
of $\lambda$-terms. And Kurz et al. [18] characterized the final coalgebra for
$L_{\alpha}$; it is carried by the set of $\lambda$-trees with finitely many
free variables modulo $\alpha$-equivalence. Again, the universal property
allows one to define operations such as substitution – this time by
corecursion. We will now recall some background material on nominal sets and
the main result of [18].

We fix a countable set $\mathcal{V}$ of variable names. Let
$\mathfrak{S}(\mathcal{V})$ be the group of _finite permutations_ of
$\mathcal{V}$, where a permutation $\pi\in\mathfrak{S}(\mathcal{V})$ is called
finite iff $\\{v\in\mathcal{V}\mid\pi(v)\neq v\\}$ is a finite set. Now
consider a set $X$ together with a group action
$\cdot:\mathfrak{S}(\mathcal{V})\times X\to X$. Intuitively, one should think
of $X$ as a set of terms, and for a finite permutation of variable names $\pi$
and some term $x$, $\pi\cdot x$ denotes the new term obtained after renaming
the variables in $x$ according to $\pi$. In order to talk about variables
“occurring” in $x\in X$ we can check which variable renamings fix the term
$x$. This is captured by the notion of _support_ : a set
$S\subseteq\mathcal{V}$ _supports_ $x\in X$ if for all
$\pi\in\mathfrak{S}(\mathcal{V})$ with $\pi(v)=v$ for all $v\in S$ we have
$\pi\cdot x=x$. Some $x\in X$ is _finitely supported_ if there is a finite
$S\subseteq\mathcal{V}$ supporting $x$.

A _nominal set_ is a set $X$ together with a
$\mathfrak{S}(\mathcal{V})$-action such that all elements of $X$ are finitely
supported.

######  Example 2.2.

  1. (1)

The set $\mathcal{V}$ of variable names with the group action given by
$\pi\cdot v=\pi(v)$ is a nominal set; for each $v_{i}\in\mathcal{V}$ the
singleton $\\{v_{i}\\}$ supports $v_{i}$.

  2. (2)

Every ordinary set $X$ can be made a nominal set by equipping it with the
trivial action $\pi\cdot x=x$ for all $x\in X$ and
$\pi\in\mathfrak{S}(\mathcal{V})$. So each $x\in X$ can be thought of a term
not containing any variable, i.e. the empty set supports $x$.

  3. (3)

The set $\Lambda$ of all $\lambda$-terms forms a nominal set with the group
action given by renaming of free variables. Every $\lambda$-term is supported
by the set of its free variables. In contrast the set $\Lambda^{\infty}$ of
all $\lambda$-trees is not nominal since $\lambda$-trees with infinitely many
free variables do not have finite support. However, the set
$\Lambda^{\infty}_{\mathsf{ffv}}$ of all $\lambda$-trees with finitely many
free variables is nominal.

Notice that if $S\subseteq V$ supports $x\in X$, then $S^{\prime}\supseteq S$
also supports $x\in X$. So $S$ supporting $x$ only means that by not touching
the members of $S$ one does not modify the term $x$. But it is more
interesting to talk about the variables actually occurring in $x$. This is
achieved by considering the smallest set supporting $x$, which is denoted by
$\operatorname{\textsf{supp}}(x)$. If
$v\in\mathcal{V}\setminus\operatorname{\textsf{supp}}(x)$, we say that $v$ is
_fresh for_ $x$, denoted by $v\mathbin{\\#}x$.

######  Example 2.3.

The set ${\mathcal{P}_{f}}(\mathcal{V})$ of finite subsets of $\mathcal{V}$,
together with the point-wise action is a nominal set. The support of each
$u\in{\mathcal{P}_{f}}(\mathcal{V})$ is $u$ itself: $\pi\cdot u=\\{\pi\cdot
x\mid x\in u\\}$ and $\operatorname{\textsf{supp}}(u)=u$. Note that
${\mathcal{P}}(\mathcal{V})$ with the point-wise action is not a nominal set
because the infinite $\\{v_{0},v_{2},v_{4},\ldots\\}$ does not have any finite
support.

The morphisms of nominal sets are those maps which are equivariant: an
_equivariant map_ $f:(X,\cdot)\to(Y,\star)$ is a map $f:X\to Y$ with
$f(\pi\cdot x)=\pi\star f(x)$ for all $\pi\in\mathfrak{S}(\mathcal{V}),x\in
X$.

For example, the function
$\operatorname{\textsf{supp}}:X\to{\mathcal{P}_{f}}(\mathcal{V})$ mapping each
element to its (finite) support is an equivariant map.

######  Remark 1.

For any equivariant $f:(X,\cdot)\to(Y,\star)$, we have
$\operatorname{\textsf{supp}}(f(x))\subseteq\operatorname{\textsf{supp}}(x)$
for any $x\in X$.

The nominal sets – together with the equivariants as morphisms – form a
category, denoted by $\mathsf{Nom}$. As shown in [14], this category is
(equivalent to) a Grothendieck topos (the so-called Shanuel topos), and so it
has rich categorical structure. We only mention some facts needed for the
current paper.

Monomorphisms and epimorphisms in $\mathsf{Nom}$ are precisely the injective
and surjective equivariant maps, respectively. It is not difficult to see that
every epimorphism in $\mathsf{Nom}$ is strong, i.e., it has the unique
diagonalization property w.r.t. any monomorphism: given an epimorphism
$e:A\twoheadrightarrow B$, a monomorphism $m:C\hookrightarrow D$ and $f:A\to
C$, $g:B\to D$ with $g\cdot e=m\cdot f$, there exists a unique diagonal
$d:B\to C$ with $d\cdot e=f$ and $m\cdot d=g$.

Furthermore, $\mathsf{Nom}$ has image-factorizations; that means that every
equivariant map $f:A\to C$ factorizes as $f=m\cdot e$ for an epimorphism
$e:A\twoheadrightarrow B$ and a monomorphism $m:B\hookrightarrow C$. Note that
the intermediate object $B$ is (isomorphic to) the image $f[A]$ in $B$ with
the restricted action. For an endofunctor $F$ on $\mathsf{Nom}$ preserving
monos this factorization systems lifts to ${\mathsf{Coalg}}\,F$: every
$F$-coalgebra homomorphism $f$ has a factorization $f=m\cdot e$ where $e$ and
$m$ are $F$-coalgebra homomorphisms that are epimorphic and monomorphic in
$\mathsf{Nom}$, respectively.

Recall from [23, Section 2.2] that $\mathsf{Nom}$ is complete and cocomplete
with colimits and finite limits formed as in $\mathsf{Set}$. In fact,
$\mathsf{Nom}$ is a locally finitely presentable category in the sense of
Gabriel and Ulmer [13] (see also Adámek and Rosický [4]). We shall not recall
that notion here as it is not needed in the current paper; intuitively, a
locally finitely presentable category is a category with a well behaved
“finite” objects (called _finitely presentable_ objects) such that every
object can be build (as a filtered colimit) from these. Petrişan [22,
Proposition 2.3.7] has shown that the finitely presentable objects of
$\mathsf{Nom}$ are precisely the orbit-finite nominal sets.

######  Definition 2.4.

For a nominal set $(X,\cdot)$ and $x\in X$ the set $\\{\pi\cdot
x\mid\pi\in\mathfrak{S}(\mathcal{V})\\}$ is called the _orbit_ of $x$. A
nominal set $(X,\cdot)$ is said to be _orbit-finite_ if it has only finitely
many orbits.

The notion of orbit-finiteness plays a central role in our paper since the
rational $\lambda$-trees modulo $\alpha$-equivalence are described by
precisely all the coalgebras with an orbit-finite carrier for the functor
$L_{\alpha}$ further below (cf. Proposition 2.10 and Theorem 3.6).

We now collect a few easy properties of orbit-finite sets that we are going to
need. (The proofs can be found in the appendix.)

######  Lemma 2.5.

For any $x_{1},x_{2}\in X$ in the same orbit, we have
$|\operatorname{\textsf{supp}}(x_{1})|=|\operatorname{\textsf{supp}}(x_{2})|$.

######  Lemma 2.6.

For an element $x$ of a nominal set $X$, there are at most
$|\operatorname{\textsf{supp}}(x)|!$ many elements with support
$\operatorname{\textsf{supp}}(x)$ in the orbit of $x$.

######  Lemma 2.7.

For a finite set $W\subseteq\mathcal{V}$ and an orbit $\mathcal{O}$ of the
nominal set $X$ there are only finitely many elements in $\mathcal{O}$ whose
support is contained in $W$.

Let us now recall from Kurz et al. [18] how all $\lambda$-trees form a final
coalgebra in $\mathsf{Nom}$. First consider the following endofunctor on
$\mathsf{Nom}$:

$LX=\mathcal{V}+\mathcal{V}\times X+X\times X;$

its coproduct components describe the type of the term constructors of the
$\lambda$-calculus (variables, $\lambda$-abstraction and application,
respectively). As shown in [18], the final coalgebra for this functor is
carried by the set of all $\lambda$-trees containing finitely many (free and
bound) variables.333Note that this is different from the set
$\Lambda^{\infty}_{\mathsf{ffv}}$ mentioned in Example 2.9.3; $\lambda$-trees
in the latter may have infinitely many bound variables. Its coalgebra
structure is the obvious map decomposing a $\lambda$-tree at the root: a
single node $\lambda$-tree is mapped to its node label in $\mathcal{V}$, a
$\lambda$-tree whose root is labeled by $\lambda x$ to $(x,t)$, where $t$ is
the $\lambda$-tree defined by the successor of the root and a $\lambda$-tree
with root label $@$ to the pair of $\lambda$-trees defined by the successors
of the root.

Since this final coalgebra completely disregards $\alpha$-equivalence it is
not possible to define substitution as a total operation on it. The solution
is to replace the second component $\mathcal{V}\times X$ of $L$ by Gabbay and
Pitts abstraction functor [12, Lemma 5.1] that takes $\alpha$-equivalence into
account:

######  Definition 2.8.

Let $(X,\cdot)$ be a nominal set. We define $\alpha$-equivalence
$\sim_{\alpha}$ as the relation on $\mathcal{V}\times X$ as

$(v_{1},x_{1})\sim_{\alpha}(v_{2},x_{2})\ \text{if there exists
}z\mathbin{\\#}\\{v_{1},v_{2}\\},z\mathbin{\\#}x_{1},z\mathbin{\\#}x_{2}\text{
with }(v_{1}\ z)x_{1}=(v_{2}\ z)x_{2}.$

The $\sim_{\alpha}$-equivalence class of $(v,x)$ is denoted by
${\left<v\right>}x$. The abstraction $[\mathcal{V}]X$ of the nominal $X$ is
the quotient $(\mathcal{V}\times X)/\mathord{\sim_{\alpha}}$ with the group
action defined by

$\pi\cdot{\left<v\right>}x={\left<\pi(v)\right>}(\pi\cdot x).$

For an equivariant map $f:X\to Y$,
$[\mathcal{V}]f:[\mathcal{V}]X\to[\mathcal{V}]Y$ is defined by
${\left<v\right>}x\mapsto{\left<v\right>}(f(x))$.

Note that the abstraction functor $[\mathcal{V}](-)$ is _strong_ , i.e., we
have a natural transformation $\tau$ with components
$\tau_{X,Y}:[\mathcal{V}]X\times Y\to[\mathcal{V}](X\times Y)$ given by
$\tau_{X,Y}({\left<v\right>}x,y)={\left<v\right>}(x,y)$; we will need the
strength $\tau$ in Section 4.1. Now one considers the endofunctor $L_{\alpha}$
on $\mathsf{Nom}$ given by

$L_{\alpha}X=\mathcal{V}+[\mathcal{V}]X+X\times X.$

Gabbay and Pitts [12] showed that its initial algebra consists of all
$\lambda$-terms modulo $\alpha$-equivalence, and the main result of Kurz et
al. [18] is that the final coalgebra $\nu L_{\alpha}$ is carried by the set
$\Lambda^{\infty}_{\mathsf{ffv}}$ of all $\lambda$-trees with finitely many
free variables quotiented by $\alpha$-equivalence. The coalgebra structure is
the same as on the final coalgebra for $L$ – one can show that this is well-
defined on equivalence classes modulo $\alpha$-equivalence.

###  2.3. The Rational Fixpoint

Recall that by Lambek’s Lemma [19], the structure of an initial algebra and a
final coalgebra for a functor $F$ are isomorphisms, so both yield _fixpoints_
of $F$. Here we shall be interested in a third fixpoint that lies in between
initial algebra and final coalgebra called the _rational fixpoint_ of $F$.
This can on the one hand be characterized as the initial iterative algebra for
$F$ (see [2]) or as the final locally finitely presentable coalgebra for $F$
(see [20]). We will only recall the latter description since the former will
not be needed in this paper.

The rational fixpoint can be defined for any _finitary_ endofunctor $F$ on a
locally finitely presentable (lfp, for short) category $\mathcal{C}$, i.e. $F$
is an endofunctor on $\mathcal{C}$ that preserves filtered colimits. Examples
of lfp categories are $\mathsf{Set}$, the categories of posets and of graphs,
every finitary variety of algebras (such as groups, rings, and vector spaces)
and every Grothendieck topos (such as $\mathsf{Nom}$). The finitely
presentable objects in these categories are: all finite sets, posets or
graphs, those algebras presented by finitely many generators and relations,
and, as we mentioned before, the orbit-finite nominal sets.

Now let $F:\mathcal{C}\to\mathcal{C}$ be finitary on the locally finitely
presentable category $\mathcal{C}$ and consider the full subcategory
${\mathsf{Coalg}_{f}}\,F$ of ${\mathsf{Coalg}}\,F$ given by all $F$-coalgebras
with a finitely presentable carrier. In [20] the _locally finitely
presentable_ $F$-coalgebras were characterized as precisely those coalgebras
that arise as a colimit of a filtered diagram of coalgebras from
${\mathsf{Coalg}_{f}}\,F$. It follows that the _final_ locally finitely
presentable coalgebra can be constructed as the colimit of _all_ coalgebras
from ${\mathsf{Coalg}_{f}}\,F$. More precisely, one defines a coalgebra
$r:\varrho F\to F(\varrho F)$ as the colimit of the inclusion functor of
${\mathsf{Coalg}_{f}}\,F$: $(\varrho
F,r):=\operatorname{colim}({\mathsf{Coalg}_{f}}\,F\hookrightarrow{\mathsf{Coalg}}\,F).$
Note that since the forgetful functor ${\mathsf{Coalg}}\,F\to\mathcal{C}$
creates all colimits this colimit is actually formed on the level of
$\mathcal{C}$. The colimit $\varrho F$ then carries a uniquely determined
coalgebra structure $r$ making it the colimit above.

As shown in [2], $\varrho F$ is a fixpoint for $F$, i.e. its coalgebra
structure $r$ is an isomorphism. From [20] we obtain that local finite
presentability of a coalgebra $(C,c)$ has the following concrete
characterizations: (1) for $\mathcal{C}=\mathsf{Set}$ local finiteness, i.e.
every element of $C$ is contained in a finite subcoalgebra of $C$; (2) for
$\mathcal{C}=\mathsf{Nom}$, local orbit-finiteness, i.e. every element of $C$
is contained in an orbit-finite subcoalgebra of $C$; (3) for $\mathcal{C}$ the
category of vector spaces over a field $K$, local finite dimensionality, i.e.,
every element of $C$ is contained in a subcoalgebra of $C$ carried by a finite
dimensional subspace of $C$.

######  Example 2.9.

We list only a few examples of rational fixpoints; for more see [2, 20, 8].

  1. (1)

Consider the functor $FX=2\times X^{A}$ on $\mathsf{Set}$ where $A$ is an
input alphabet and $2=\\{0,1\\}$. The $F$-coalgebras are precisely the
deterministic automata over $A$ (without initial states). The final coalgebra
is carried by the set $\mathcal{P}(A^{*})$ of all formal languages and the
rational fixpoint is its subcoalgebra of regular languages over $A$.

  2. (2)

For $FX=\mathds{R}\times X$ on $\mathsf{Set}$ the final coalgebra is carried
by the set $\mathds{R}^{\omega}$ of all real streams and the rational fixpoint
is its subcoalgebra of all eventually periodic streams, i.e. streams
$uvvv\cdots$ with $u,v\in\mathds{R}^{*}$. Taking the same functor on the
category of real vector spaces we get the same final coalgebra
$\mathds{R}^{\omega}$ with the componentwise vector space structure, but this
time the rational fixpoint is formed by all rational streams (see [26, 20]).

  3. (3)

Let $\Sigma$ be a signature of operation symbols with prescribed arity, i.e. a
sequence $(\Sigma_{n})_{n<\omega}$ of sets. This give rise to an associated
polynomial endofunctor $F_{\Sigma}$ on $\mathsf{Set}$ given by
$F_{\Sigma}X=\coprod_{n<\omega}\Sigma_{n}\times X^{n}$. Its initial algebra is
formed by all $\Sigma$-terms and its final coalgebra by all (finite and
infinite) $\Sigma$-trees, i.e. rooted and ordered trees such that every node
with $n$ children is labelled by an $n$-ary operation symbol. And the rational
fixpoint consists precisely of all regular $\Sigma$-trees of Elgot [10] (see
also Courcelle [9]), i.e. those $\Sigma$-trees having only finitely many
different subtrees up to isomorphism (see Ginali [15]).

Note that in all the above examples the rational fixpoint $\varrho F$ allways
occurs as a subcoalgebra of the final coalgebra $\nu F$. But this need not be
the case in general (see [8, Example 3.15] for a counterexample). However, we
have the following result:

######  Proposition 2.10 ([8, Proposition 3.12]).

Suppose that in $\mathcal{C}$ finitely presentable objects are closed under
strong quotients and that $F$ is finitary and preserves monomorphisms. Then
the rational fixpoint $\varrho F$ is the subcoalgebra of $\nu F$ given by the
union of images of all coalgebra homomorphisms $c^{\dagger}:(C,c)\to(\nu F,t)$
where $(C,c)$ ranges over ${\mathsf{Coalg}_{f}}\,F$.444In a general lfp
category the _image_ of $c^{\dagger}$ is obtained by taking a strong epi-mono
factorization of $c^{\dagger}$, and the _union_ is then obtained as a directed
colimit of the resulting subobjects of $(\nu F,t)$.

In particular, for a finitary functor $F$ on $\mathsf{Set}$ (or $\mathsf{Nom}$
resp.) preserving monomorphisms the rational fixpoint is the union in $\nu F$
of images of all finite (or orbit-finite resp.) coalgebras; in symbols:

$\varrho F=\bigcup\limits_{\text{$(C,c)$ in
${\mathsf{Coalg}_{f}}\,F$}}c^{\dagger}[C]\ \subseteq\ \nu F.$

Note that it is sufficient to let $(C,c)$ range over those coalgebras in
${\mathsf{Coalg}_{f}}\,F$ where $c^{\dagger}$ is injective (or an inclusion
map) because for an arbitrary (orbit-)finite $(C,c)$ in
${\mathsf{Coalg}_{f}}F$ its image $c^{\dagger}[C]$ is an (orbit-)finite
$F$-coalgebra, too.

##  3\. The Rational Fixpoint in Nominal Sets

In this section we are going to prove the main result of our paper, a
characterization of the rational fixpoint for the functor $L_{\alpha}$ as the
rational $\lambda$-trees modulo $\alpha$-equivalence.

But we start with the rational fixpoint of the functor
$LX=\mathcal{V}+\mathcal{V}\times X+X\times X$. Note that both functors $L$
and $L_{\alpha}$ are finitary and preserve monomorphisms (to see this use [18,
Proposition 5.6] and the fact the forgetful functor from $\mathsf{Nom}$ to
$\mathsf{Set}$ creates colimits).

######  Proposition 3.1.

The rational fixpoint of the functor $L:\mathsf{Nom}\to\mathsf{Nom}$ is formed
by all rational $\lambda$-trees.

In the proof of the following theorem we will slightly abuse notation and
consider $LX=\mathcal{V}+\mathcal{V}\times X+X\times X$ as an endofunctor on
$\mathsf{Set}$. Note that its final coalgebra is formed by the set
$\Lambda^{\infty}$ of all $\lambda$-trees and its rational fixpoint by all
rational $\lambda$-trees (this follows from Example 2.9.3).

######  Theorem 3.2.

Let $X\xrightarrow{a}L_{\alpha}X$ be an orbit-finite coalgebra. Then for all
$\operatorname{\mathsf{root}}\in X$,
$a^{\dagger}(\operatorname{\mathsf{root}})\in\varrho L_{\alpha}$ is a rational
$\lambda$-tree.

######  Proof 3.3 (Proofsketch).

(for a full proof see the appendix)Let $m:=\max_{x\in
X}\big{|}\operatorname{\textsf{supp}}(x)\big{|}$ be the maximal number of free
variables in any element of $X$. This exists by 2.5 since $X$ is orbit-finite.
Let $W\subseteq\mathcal{V}$ be some set of $m+1$ variables containing
$\operatorname{\textsf{supp}}(\operatorname{\mathsf{root}})$. Hence for all
$x\in X$ there exists a $w\in W$ with $w\mathbin{\\#}x$.

In the following, one constructs a rational ${\lambda}$-tree in the
$\alpha$-equivalence class of $a^{\dagger}(\operatorname{\mathsf{root}})$.
First, define an $L$-coalgebra
$C\xrightarrow{c}LC=\mathcal{V}+\mathcal{V}\times C+C\times C$ in
$\mathsf{Set}$ with $C:=\\{x\in X\mid\operatorname{\textsf{supp}}(x)\subseteq
W\\}$ and

$c(x)=\begin{cases}w&\text{if }a(x)=w\in W\subseteq\mathcal{V}\\\
(\ell,r)&\text{if }a(x)=(\ell,r)\in X\times X\\\ (w,y)&\text{if
}a(x)={\left<v\right>}y^{\prime}\text{ and }y=(v\ w)y^{\prime}\text{ for some
}w\in W\setminus\operatorname{\textsf{supp}}(x)\end{cases}$

Next one readily verifies that $c$ is well-defined, i.e., its image really
lies in $LC$.

Furthermore, $C$ is finite because $X$ is orbit-finite and within any orbit
there are only finitely many elements with a support contained in $W$ by 2.7.
Let $c^{\dagger}$ denote the unique $L$-coalgebra homomorphism into the final
$L$-coalgebra in $\mathsf{Set}$. Since $C$ is finite, we know that
$c^{\dagger}:C\to\nu L$ factors through the rational fixpoint, i.e. for every
$x\in C$, $c^{\dagger}(x)$ is a rational $\lambda$-tree. One then proves that
$[c^{\dagger}(x)]_{\alpha}=a^{\dagger}(x)$ for all $x\in C\subseteq X$, where
$[-]_{\alpha}$ denotes $\alpha$-equivalence classes. This involves a non-
trivial induction argument using the _final chains_ of the set functor $L$ and
the functor $L_{\alpha}$ on $\mathsf{Nom}$ as well as technical details from
[18](see the appendix). It follows that
$a^{\dagger}(\operatorname{\mathsf{root}})$ is rational.

For the $L$-coalgebra $(C,c)$ in $\mathsf{Set}$ from the previous proof, we
know that for any $x\in C$, the resulting tree $c^{\dagger}(x)$ has at most
$|C|$ subtrees. This does not hold for an $L_{\alpha}$-coalgebra $(X,a)$ in
$\mathsf{Nom}$: if $X$ has a non-trivial action, then the cardinality of $X$
is at least infinite, i.e. the cardinality does not give a reasonable bound
for the number of subtrees. And the number of orbits $n$ is not a bound
either. The problem is that multiple elements from the same orbit may
represent different subtrees. For example, consider the rational tree

$t:=\leavevmode\hbox to35.9pt{\vbox
to22.47pt{\pgfpicture\makeatletter\hbox{\hskip
17.94896pt\lower-17.99678pt\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\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}} {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{-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{{@}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{-16.94896pt}{-15.19234pt}\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{{$v_{0}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-5.08893pt}{-3.80756pt}\pgfsys@lineto{-12.94595pt}{-9.68683pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{8.94293pt}{-15.19234pt}\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{{$v_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{5.08893pt}{-3.80756pt}\pgfsys@lineto{12.94594pt}{-9.68683pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}},$

and let $X:=\mathcal{V}+\\{(\ell,r)\in\mathcal{V}\times\mathcal{V}\mid\ell\neq
r\\}$ be equipped with the coalgebra structure

$X\xrightarrow{a}L_{\alpha}X,\quad a(x)=\begin{cases}v&\text{ if
}x=v\in\mathcal{V}\\\ (\ell,r)&\text{ if
}x=(\ell,r)\in\mathcal{V}\times\mathcal{V}.\end{cases}$

$X$ is constructed to have two orbits: one consisting of single variables and
one consisting of unequal ordered pairs of variables. We have
$(v_{0},v_{1})\in X$ and
$a^{\dagger}\big{(}(v_{0},v_{1})\big{)}=[t]_{\alpha}$. But $t$ has three
subtrees, namely $t$ itself, $v_{0}$, and $v_{1}$. This example is expanded
later in Example 3.8.

But when looking closer at the construction of $C$ in the previous proof, we
can give a bound on the number of its elements, i.e. the number of (up to
isomorphism) different subtrees of the rational tree
$c^{\dagger}(\operatorname{\mathsf{root}})$.

######  Proposition 3.4.

Let $(X,a)$ be an orbit-finite $L_{\alpha}$-coalgebra with $n$ orbits and let
$m=\max_{x\in X}\big{|}\operatorname{\textsf{supp}}(x)\big{|}$. Then the
number of elements of the coalgebra $C$ (as constructed in the previous proof)
is bounded by $n\cdot(m+1)!$.

######  Proof 3.5.

Recall from the proof of Theorem 3.2 that $C:=\\{x\in
X\mid\operatorname{\textsf{supp}}(x)\subseteq W\\}$, where $W$ is a set of
$m+1$ variables. Consider a fixed orbit $O$ whose elements have a support of
cardinality $k$: there are at most $\begin{pmatrix}m+1\\\ k\end{pmatrix}$
possibilities of choosing a $k$-element subset $S$ of $W$ and for any such $S$
there are at most $k!$ elements in $O$ with support $S$, by 2.6. Thus, the
number of elements of $O$ in $C$ is at most

${m+1\choose k}\cdot k!=\frac{(m+1)!}{k!\cdot(m+1-k)!}\cdot
k!=\frac{(m+1)!}{(m+1-k)!}\overset{k\leq
m}{\leq}\frac{(m+1)!}{(m+1-m)!}=(m+1)!.$

In total, the cardinality of $C$ is bounded by $n\cdot(m+1)!$.

That the number of orbits $n$ occurs linearly is not surprising, because if we
have some finite carrier set $X$ with the trivial action that “uses” all its
elements for the coalgebra structure, we have exactly one subtree per element
of $X$. In Example 3.8 we shall see that the factor is $(m+1)!$ is necessary.
But before that we state and prove our main result:

######  Theorem 3.6.

The rational fixed point $\varrho L_{\alpha}$ contains precisely the rational
$\lambda$-trees modulo $\alpha$-equivalence.

######  Proof 3.7.

After Theorem 3.2 it only remains to show that all $\alpha$-equivalence
classes of rational ${\lambda}$-trees are in $\varrho L_{\alpha}$. Let
$u_{\alpha}\in\nu L_{\alpha}$ be rational, witnessed by some rational
representative $u\in u_{\alpha}$ with only finitely many subtrees (up to
isomorphism). Let $C$ be the finite set of all subtrees of $u$ and define the
nominal set $X$ as

$X:=\bigcup_{s\in C}O([s]_{\alpha})\ \subseteq\ \nu L_{\alpha},$

where $[s]_{\alpha}\in\nu L_{\alpha}$ is the $\alpha$-equivalence class of the
subtree $s$ and $O(y)\subseteq\nu L_{\alpha}$ denotes the orbit of a given
element $y\in\nu L_{\alpha}$. Note that the group action of $\nu L_{\alpha}$
restricts to $X$ since it is a union of orbits.

Next we define a coalgebra structure $a:X\to L_{\alpha}X$ by restriction of
the structure $t:\nu L_{\alpha}\to L_{\alpha}(\nu L_{\alpha})$: set
$a(x):=t(x)$ for all $x\in X$. We need to check that this is well-defined,
i.e. that $t(x)$ really lies in $L_{\alpha}X$ for every $x\in X$. For this we
consider three cases:

  1. (1)

The case $t(x)\in\mathcal{V}$ is clear;

  2. (2)

Suppose that $t(x)={\left<v\right>}y\in[\mathcal{V}](\nu L_{\alpha})$ where
$x=\pi\cdot[{\lambda}w.s]_{\alpha}$ for some $\pi\in\mathfrak{S}(\mathcal{V})$
and some subtree ${\lambda}w.s$ of $u$. Then we have

${\left<w\right>}[s]_{\alpha}=t([{\lambda}w.s]_{\alpha})=t(\pi^{-1}\cdot
x)=\pi^{-1}\cdot
t(x)=\pi^{-1}\cdot{\left<v\right>}y={\left<\pi^{-1}(v)\right>}(\pi^{-1}\cdot
y).$

By the definition of abstraction, we have some $z\in\mathcal{V}$ with

$(w\ z)\cdot[s]_{\alpha}=(\pi^{-1}(v)\ z)\cdot\pi^{-1}\cdot y.$

Hence, $y$ is in the orbit of $[s]_{\alpha}$ and therefore $t(x)$ is in
$[\mathcal{V}]X$.

  3. (3)

For $t(x)=(\ell,r)\in\nu L_{\alpha}\times\nu L_{\alpha}$, let $x\in X$ be
$\pi\cdot[(s_{\ell},s_{r})]_{\alpha}$ for some
$\pi\in\mathfrak{S}(\mathcal{V})$ and subtrees $s_{\ell},s_{r}$ of $u$.
Analogously to the previous case, we have

$(\ell,r)=t(x)=t(\pi\cdot[(s_{\ell},s_{r})]_{\alpha})=\pi\cdot([s_{\ell}]_{\alpha},[s_{r}]_{\alpha})=(\pi\cdot[s_{\ell}]_{\alpha},\pi\cdot[s_{r}]_{\alpha})\in
X\times X.$

By construction, $u_{\alpha}\in X$ and $a^{\dagger}(x)=x$ holds for all $x\in
X$. By the finiteness of $C$, $X$ is orbit-finite and thus
$a^{\dagger}[X]\subseteq\varrho L_{\alpha}$, and in particular
$u_{\alpha}\in\varrho L_{\alpha}$.

The following example shows that the bound in 3.4 on the number of elements of
the $L$-coalgebra $C$ from the proof of Theorem 3.2 can essentially not be
improved even if we omit the usage of $\lambda$-abstraction.

######  Example 3.8.

Let $\ell\geq 1$ be a fixed natural number and let $m=2^{\ell-1}$. Further let
$V=\\{v_{1},\ldots,v_{m}\\}$ be a set of $m$ variables and consider the
rational $\lambda$-trees parametrized by permutations
$\sigma\in\mathfrak{S}(\mathcal{V})$ shown in Figure 2.

@$\mathrlap{\ =r_{\sigma}}$$\mathllap{h_{\sigma}=\ }@$$r_{\sigma\,(1\
2)}$$r_{\sigma\,(1\ \cdots\ m)}$@@@@@@@$\sigma v_{1}$$\sigma v_{2}$$\sigma
v_{m}$$\cdots$ $\ell$ levels Figure 2.

With $r_{\sigma}$ and $h_{\sigma}$ we denote the corresponding subtrees rooted
at the indicated nodes. Note that the $\alpha$-equivalence classes in $\varrho
L_{\alpha}$ of each $r_{\sigma}$ and of any of its subtrees are singletons
since $r_{\sigma}$ does not contain any $\lambda$-abstraction. For this reason
we shall henceforth abuse notation and denote those equivalence classes by
their representatives. Observe further that the group action on $\varrho
L_{\alpha}$ satisfies $\tau\cdot r_{\sigma}=r_{\tau\sigma}$ for any
$\tau,\sigma\in\mathfrak{S}(\mathcal{V})$. This implies that all $r_{\sigma}$
and $h_{\sigma}$, respectively, lie in the same orbit. Similarly, one can see
that all nodes on the same level in the right-hand maximal subtrees of every
$r_{\sigma}$ (indicated by the dotted rectangles) lie in the same orbit.

Now consider $r_{\text{id}}$ and the corresponding orbit-finite subcoalgebra
$X$ of $\varrho L_{\alpha}$ from the proof of Theorem 3.6. The elements of $X$
are all subtrees of $r_{\text{id}}$ with the group action inherited from
$\varrho L_{\alpha}$. By the above reasoning we see that $X$ has precisely
$\ell+2$ orbits. Hence, the number of orbits of $X$ is logarithmic in $m$. But
the number of subtrees of $r_{\text{id}}$ grows faster than $m!$. To see this,
notice first that the permutations $(1\ 2)$ and $(1\ 2\ \cdots\ m)$ generate
the group of all permutations of $m$ elements. Thus, we see that
$r_{\text{id}}$ has all $r_{\sigma}$ as subtrees where $\sigma$ is any
permutation that fixes $\mathcal{V}\setminus V$. For different $\sigma$ and
$\tau$ we have that $r_{\sigma}$, $h_{\sigma}$, $r_{\tau}$ and $h_{\tau}$ are
pairwise non-isomorphic. Thus, we see that $r_{\text{id}}$ has at least
$2\cdot m!$ subtrees. In addition, consider the $i$-th level (from 1 at the
bottom to $\ell$ at the top) on the right in Figure 2. Each node on that level
covers $k=2^{i-1}$ variables. Then for each permutation of those $k$ variables
there exists a subtree of the right-hand successor of some subtree
$r_{\sigma}$ of $r_{\text{id}}$ which is a complete binary tree of height $i$
with the front given by the permutation. Thus, the total number of subtrees of
$r_{\text{id}}$ is precisely

$2\cdot m!+\sum_{i=1}^{\ell}\left({m\choose
2^{i-1}}\cdot(2^{i-1})!\right)=2\cdot
m!+\sum_{i=1}^{\ell}\frac{m!}{(m-2^{i-1})!}.$

##  4\. Application: Corecursive Definitions on Rational $\lambda$-trees

Our result in Theorem 3.6 that rational $\lambda$-trees modulo
$\alpha$-equivalence form the final locally orbit-finite
$L_{\alpha}$-coalgebra yields a corecursion principle. In this section we
shall demonstrate this principle by considering two easy applications. First
we show that substitution as defined corecursively for all $\lambda$-trees in
[18] restricts to rational $\lambda$-trees. Secondly, we discuss the
corecursive definition of the computation of the Böhm tree of a given rational
$\lambda$-tree.

###  4.1. Substitution on Rational $\lambda$-trees

When performing operations known from (infinitary) $\lambda$-calculus on
rational $\lambda$-trees, it is not clear whether the resulting $\lambda$-tree
still is rational in general. One such operation is the substitution function
$\operatorname{\textsf{subs}}:\nu L_{\alpha}\times\mathcal{V}\times\nu
L_{\alpha}\longrightarrow\nu L_{\alpha}$, which for a given triple $(t,v,s)$
replaces each occurence of the variable $v$ in $t$ by $s$. Kurz et al. [18]
show how to define $\operatorname{\textsf{subs}}$ by coinduction: to do this
they define an $L_{\alpha}$-coalgebra whoose unique homomorphism into the
final coalgebra yields $\operatorname{\textsf{subs}}$. It is possible to adapt
this to the orbit-finite case as follows.

For arbitrary coalgebras $A\xrightarrow{a}L_{\alpha}A$ and
$B\xrightarrow{b}L_{\alpha}B$ with orbit-finite carriers, one defines
$\operatorname{\textsf{subs}}_{A,B}:A\times\mathcal{V}\times B\to\varrho
L_{\alpha}$. This map $\operatorname{\textsf{subs}}_{A,B}$ describes the
substitution of a variable within an element of the coalgebra $A$ by some
element of the coalgebra $B$. In the following

$B\xrightarrow{\mathsf{inl}}B+A\times\mathcal{V}\times
B\xleftarrow{\mathsf{inr}}A\times\mathcal{V}\times
B\qquad\text{and}\qquad\mathcal{V}\xrightarrow{\mathsf{in}_{1}}L_{\alpha}X\xleftarrow{\mathsf{in}_{2}}[\mathcal{V}]X$

denote coproduct injections. Now define $B+A\times\mathcal{V}\times
B\xrightarrow{[g,h]}L_{\alpha}(B+A\times\mathcal{V}\times B)$ with
$g=L_{\alpha}(\mathsf{inl})\circ b$ and
$h=[h_{\text{Var}},h_{\text{Abs}},h_{\text{App}}]\circ(a\times\text{id}\times\text{id})$
using distributivity and

  * •

$h_{\text{Var}}:\mathcal{V}\times\mathcal{V}\times B\to
L_{\alpha}(B+A\times\mathcal{V}\times B)$,
$h_{\text{Var}}(v,w,x)=\begin{cases}\mathsf{in}_{1}v&\text{if }v\neq w\\\
L_{\alpha}(\mathsf{inl})(\underbrace{b(x)}_{\mathclap{\in
L_{\alpha}(B)}})&\text{if }v=w\end{cases}$

  * •

$h_{\text{Abs}}:([\mathcal{V}]A)\times\mathcal{V}\times B\to
L_{\alpha}(B+A\times\mathcal{V}\times B)$,
$h_{\text{Abs}}:=\mathsf{in}_{2}\circ\tau_{A,\mathcal{V}\times B}$, using the
strength $\tau$ of the functor $[\mathcal{V}]$ with $\tau_{A,\mathcal{V}\times
B}:([\mathcal{V}]A)\times\mathcal{V}\times
B\to[\mathcal{V}](A\times\mathcal{V}\times B)$.

  * •

$h_{\text{App}}:A\times A\times\mathcal{V}\times B\to
L_{\alpha}(B+A\times\mathcal{V}\times B)$ is the composition of the obvious
steps $A\times A\times\mathcal{V}\times B\to(A\times\mathcal{V}\times
B)\times(A\times\mathcal{V}\times B)\to L_{\alpha}(B+A\times\mathcal{V}\times
B).$

$B+A\times\mathcal{V}\times B$ is orbit-finite, so we get a unique
$L_{\alpha}$-coalgebra homomorphism $[g^{\prime},h^{\prime}]$ into $\varrho
L_{\alpha}$, making the following diagram commute:

${B+A\times\mathcal{V}\times B}$${L_{\alpha}(B+A\times\mathcal{V}\times
B)}$${\varrho L_{\alpha}}$${L_{\alpha}(\varrho
L_{\alpha})}$${[g^{\prime},h^{\prime}]}$${[g,h]}$${L_{\alpha}([g^{\prime},h^{\prime}])}$${f_{\alpha}}$

Now we define $\operatorname{\textsf{subs}}_{A,B}:=h^{\prime}$. It remains to
extend this to the desired domain $\varrho
L_{\alpha}\times\mathcal{V}\times\varrho L_{\alpha}$. Let $I$ be the set of
all orbit-finite subcoalgebras $(X,a)$ of $(\nu L_{\alpha},t_{\alpha})$. Then
we know from (the discussion following) Proposition 2.10 that

$\varrho L_{\alpha}=\bigcup\limits_{(X,a)\text{ in }I}X.$

Hence, we can define substitution
$\operatorname{\textsf{subs}}_{\text{rat}}:\varrho
L_{\alpha}\times\mathcal{V}\times\varrho L_{\alpha}\to\varrho L_{\alpha}$ on
rational $\lambda$-trees by

$\operatorname{\textsf{subs}}_{\text{rat}}(x,v,y)=\operatorname{\textsf{subs}}_{A,B}(x,v,y),\text{for
some $A,B\in I$ with $x\in A$ and $y\in B$}.$

It remains to prove that the result does not depend on the choice of $A$ and
$B$. But if we have any other $(A^{\prime},a^{\prime})$ in $I$ with $x\in
A^{\prime}$ then since both $A$ and $A^{\prime}$ are subcoalgebras we have
$a(x)=t_{\alpha}(x)=a^{\prime}(x)$. Similarly for $B$ and $y\in B$.

Thus, since the function $h$ is defined by pattern matching, i.e. on the
alternatives indicated by $a$, it behaves independently from the choice of $A$
and $B$ as desired.

To summarize, we can say that one can define operations on $\varrho
L_{\alpha}$ if these $n$-ary operations can be defined restricted to $n$
orbit-finite subcoalgebras of $\nu L_{\alpha}$ as we have just seen for the
operation of substitution.

###  4.2. Normalization of Rational $\lambda$-trees

In the ${\lambda}$-calculus different kinds of normal forms play an important
role. One of them is the _head normal form_ (_hnf_ , for short). A
${\lambda}$-term is in hnf if it is of the form
${\lambda}x_{1}\ldots{\lambda}x_{n}.yN_{1}\ldots N_{m}$, where $y$ is a
variable and the $N_{i}$ are arbitrary terms. If one recursively requires the
$N_{i}$ to be in hnf as well, one gets the definition of _Böhm trees_. Adding
an additional constant symbol $\bot$ to the syntax of the ${\lambda}$-calculus
allows the following corecursive definition of the Böhm tree
$\operatorname{\mathsf{BT}}(M)$ of a $\lambda$-term $M$ (see [18]):

$\displaystyle\operatorname{\mathsf{BT}}(M)=\begin{cases}{\lambda}x_{1}\ldots{\lambda}x_{n}.y\operatorname{\mathsf{BT}}(N_{1})\ldots\operatorname{\mathsf{BT}}(N_{m})&\text{if
}M\twoheadrightarrow_{\beta}{\lambda}x_{1}\ldots{\lambda}x_{n}.yN_{1}\ldots
N_{m}\\\ \bot&\text{otherwise},\end{cases}$ (4.1)

where $\twoheadrightarrow_{\beta}$ denoted the reflexive, transitive closure
of $\beta$-reduction $\to_{\beta}$. So a Böhm tree of a term $M$ is the normal
form of $M$ in the infinitary ${\lambda}$-calculus, or $\bot$ if there is no
normal form [6, 17].

Kurz et al. [18] obtained the operation $\operatorname{\mathsf{BT}}$ by using
the final coalgebra $\Lambda_{\alpha}^{\infty}$ of the following endofunctor
${\mathsf{Lb}_{\alpha}}$ on $\mathsf{Nom}$ expressing the syntax of the
${\lambda}$-calculus extended by $\bot$:

${\mathsf{Lb}_{\alpha}}X=\mathcal{V}+\\{\bot\\}+[\mathcal{V}]X+X\times X.$

The nominal set $\Lambda_{\alpha}^{\infty}$ consists of all ${\lambda}$-trees
over $\bot$ modulo $\alpha$-equivalence, i.e. $\lambda$-trees where some
leaves are labelled by $\bot$ in lieu of a variable from $\mathcal{V}$. So
$\operatorname{\mathsf{BT}}:\Lambda_{\alpha}^{\infty}\to\Lambda_{\alpha}^{\infty}$
is defined as the unique coalgebra homomorphism from a coalgebra
$b:\Lambda_{\alpha}^{\infty}\to{\mathsf{Lb}_{\alpha}}(\Lambda^{\infty}_{\alpha})$,
where $b$ is defined by

$b(M)=\begin{cases}t(N)&\text{if $M\twoheadrightarrow_{\beta}N$ and $N$ is in
hnf}\\\ \bot&\text{else},\end{cases}$

into the final coalgebra $\nu{\mathsf{Lb}_{\alpha}}$.

The rational fixpoint $\varrho{\mathsf{Lb}_{\alpha}}$ consists of the rational
$\lambda$-trees over $\bot$ modulo $\alpha$-equivalence; in fact, it is easy
to extend to the proof of Theorem 3.6 to the functor ${\mathsf{Lb}_{\alpha}}$.

However, $\operatorname{\mathsf{BT}}$ does not restrict to
$\varrho{\mathsf{Lb}_{\alpha}}$. Consider the ${\lambda}$-term

$\displaystyle u:=Y_{({\lambda}g.{\lambda}x.x\,(g(x\,y)))},\text{ with
}Y_{f}:=({\lambda}z.f(z\ z))({\lambda}z.f(z\ z)).$ (4.2)

which is finite and therefore rational. In other words, $u$ represents an
element of $\varrho{\mathsf{Lb}_{\alpha}}$. Let us look at its Böhm tree, by
considering the $\beta$-reduction sequence of $u$ using
$Y_{f}\rightarrow_{\beta}f(Y_{f}f)$:

$\displaystyle u\,x$
$\displaystyle=Y_{({\lambda}g.{\lambda}x.x\,(g(x\,y)))}\,x\rightarrow_{\beta}({\lambda}g.{\lambda}x.x\,(g(x\,y)))\,\overbrace{Y_{({\lambda}g.{\lambda}x.x\,(g(x\,y)))}}^{\smash{u}}\,x\twoheadrightarrow_{\beta}x\,(u\,(x\,y))$

Applying $ux\twoheadrightarrow_{\beta}x\,(u\,(x\,y))$ multiple times yields
the following sequence:

$\leavevmode\hbox to47.85pt{\vbox
to31.11pt{\pgfpicture\makeatletter\hbox{\hskip 25.4969pt\lower-26.64261pt\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\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{ {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{31.50026pt}{-12.60167pt}\pgfsys@lineto{8.73805pt}{-12.60167pt}\pgfsys@curveto{7.16664pt}{-12.60167pt}{5.89278pt}{-13.87553pt}{5.89278pt}{-15.44695pt}\pgfsys@lineto{5.89278pt}{-24.79137pt}\pgfsys@curveto{5.89278pt}{-26.36278pt}{7.16664pt}{-27.63664pt}{8.73805pt}{-27.63664pt}\pgfsys@lineto{31.50026pt}{-27.63664pt}\pgfsys@curveto{33.07167pt}{-27.63664pt}{34.34554pt}{-26.36278pt}{34.34554pt}{-24.79137pt}\pgfsys@lineto{34.34554pt}{-15.44695pt}\pgfsys@curveto{34.34554pt}{-13.87553pt}{33.07167pt}{-12.60167pt}{31.50026pt}{-12.60167pt}\pgfsys@closepath\pgfsys@moveto{5.89278pt}{-27.63664pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.03026pt}{-20.11916pt}\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{\minipage[t]{10.1778pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{59.55359pt}{-32.72083pt}\pgfsys@lineto{-19.31528pt}{-32.72083pt}\pgfsys@curveto{-20.88669pt}{-32.72083pt}{-22.16055pt}{-33.99469pt}{-22.16055pt}{-35.5661pt}\pgfsys@lineto{-22.16055pt}{-44.91052pt}\pgfsys@curveto{-22.16055pt}{-46.48193pt}{-20.88669pt}{-47.7558pt}{-19.31528pt}{-47.7558pt}\pgfsys@lineto{59.55359pt}{-47.7558pt}\pgfsys@curveto{61.125pt}{-47.7558pt}{62.39886pt}{-46.48193pt}{62.39886pt}{-44.91052pt}\pgfsys@lineto{62.39886pt}{-35.5661pt}\pgfsys@curveto{62.39886pt}{-33.99469pt}{61.125pt}{-32.72083pt}{59.55359pt}{-32.72083pt}\pgfsys@closepath\pgfsys@moveto{-22.16055pt}{-47.7558pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.31528pt}{-40.23831pt}\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{\minipage[t]{78.86887pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{79.67274pt}{-52.83998pt}\pgfsys@lineto{-39.43443pt}{-52.83998pt}\pgfsys@curveto{-41.00584pt}{-52.83998pt}{-42.27971pt}{-54.11385pt}{-42.27971pt}{-55.68526pt}\pgfsys@lineto{-42.27971pt}{-65.02968pt}\pgfsys@curveto{-42.27971pt}{-66.60109pt}{-41.00584pt}{-67.87495pt}{-39.43443pt}{-67.87495pt}\pgfsys@lineto{79.67274pt}{-67.87495pt}\pgfsys@curveto{81.24416pt}{-67.87495pt}{82.51802pt}{-66.60109pt}{82.51802pt}{-65.02968pt}\pgfsys@lineto{82.51802pt}{-55.68526pt}\pgfsys@curveto{82.51802pt}{-54.11385pt}{81.24416pt}{-52.83998pt}{79.67274pt}{-52.83998pt}\pgfsys@closepath\pgfsys@moveto{-42.27971pt}{-67.87495pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-39.43443pt}{-60.35747pt}\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{\minipage[t]{119.10718pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{111.77466pt}{-110.36494pt}\pgfsys@lineto{-71.53635pt}{-110.36494pt}\pgfsys@curveto{-73.10776pt}{-110.36494pt}{-74.38162pt}{-111.63881pt}{-74.38162pt}{-113.21022pt}\pgfsys@lineto{-74.38162pt}{-121.7202pt}\pgfsys@curveto{-74.38162pt}{-123.29161pt}{-73.10776pt}{-124.56548pt}{-71.53635pt}{-124.56548pt}\pgfsys@lineto{111.77466pt}{-124.56548pt}\pgfsys@curveto{113.34607pt}{-124.56548pt}{114.61993pt}{-123.29161pt}{114.61993pt}{-121.7202pt}\pgfsys@lineto{114.61993pt}{-113.21022pt}\pgfsys@curveto{114.61993pt}{-111.63881pt}{113.34607pt}{-110.36494pt}{111.77466pt}{-110.36494pt}\pgfsys@closepath\pgfsys@moveto{-74.38162pt}{-124.56548pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-71.53635pt}{-117.46521pt}\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{\minipage[t]{183.311pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{} {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{-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{${@}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{{{}{}{{}{}}{{}{{}{}}}{{}{{}{}}}{{}{{}{}}}{{}{}{{{{}{}}{}}}{{{{}{}}{}}}{}{{}}}}}{{}{}{{}{}}{{}{{}{}}}{{}{{}{}}}{{}{{}{}}}{{}{}{{{{}{}}{}}}{{{{}{}}{}}}{}{{}}}}{{{}}{{}}{}{}{}}{{}\pgfsys@moveto{-18.4943pt}{-11.85434pt}\pgfsys@lineto{-25.2969pt}{-26.44261pt}\pgfsys@lineto{-11.69168pt}{-26.44261pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-21.35658pt}{-25.44263pt}\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{${u}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {
{}{}{}}{}{{}{}{{}{}}{{}{{}{}}}{{}{{}{}}}{{}{{}{}}}{{}{}{{{{}{}}{}}}{{{{}{}}{}}}{}{{}}}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-5.0889pt}{-3.13109pt}\pgfsys@lineto{-18.4943pt}{-11.3811pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{15.63666pt}{-13.53387pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{5.0889pt}{-2.20868pt}\pgfsys@lineto{18.4943pt}{-8.02834pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\
\twoheadrightarrow_{\beta}\ \leavevmode\hbox to68.19pt{\vbox
to42.74pt{\pgfpicture\makeatletter\hbox{\hskip 22.35193pt\lower-38.2683pt\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\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{ {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{31.50026pt}{-12.60167pt}\pgfsys@lineto{8.73805pt}{-12.60167pt}\pgfsys@curveto{7.16664pt}{-12.60167pt}{5.89278pt}{-13.87553pt}{5.89278pt}{-15.44695pt}\pgfsys@lineto{5.89278pt}{-24.79137pt}\pgfsys@curveto{5.89278pt}{-26.36278pt}{7.16664pt}{-27.63664pt}{8.73805pt}{-27.63664pt}\pgfsys@lineto{31.50026pt}{-27.63664pt}\pgfsys@curveto{33.07167pt}{-27.63664pt}{34.34554pt}{-26.36278pt}{34.34554pt}{-24.79137pt}\pgfsys@lineto{34.34554pt}{-15.44695pt}\pgfsys@curveto{34.34554pt}{-13.87553pt}{33.07167pt}{-12.60167pt}{31.50026pt}{-12.60167pt}\pgfsys@closepath\pgfsys@moveto{5.89278pt}{-27.63664pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.03026pt}{-20.11916pt}\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{\minipage[t]{10.1778pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{59.55359pt}{-32.72083pt}\pgfsys@lineto{-19.31528pt}{-32.72083pt}\pgfsys@curveto{-20.88669pt}{-32.72083pt}{-22.16055pt}{-33.99469pt}{-22.16055pt}{-35.5661pt}\pgfsys@lineto{-22.16055pt}{-44.91052pt}\pgfsys@curveto{-22.16055pt}{-46.48193pt}{-20.88669pt}{-47.7558pt}{-19.31528pt}{-47.7558pt}\pgfsys@lineto{59.55359pt}{-47.7558pt}\pgfsys@curveto{61.125pt}{-47.7558pt}{62.39886pt}{-46.48193pt}{62.39886pt}{-44.91052pt}\pgfsys@lineto{62.39886pt}{-35.5661pt}\pgfsys@curveto{62.39886pt}{-33.99469pt}{61.125pt}{-32.72083pt}{59.55359pt}{-32.72083pt}\pgfsys@closepath\pgfsys@moveto{-22.16055pt}{-47.7558pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.31528pt}{-40.23831pt}\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{\minipage[t]{78.86887pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{79.67274pt}{-52.83998pt}\pgfsys@lineto{-39.43443pt}{-52.83998pt}\pgfsys@curveto{-41.00584pt}{-52.83998pt}{-42.27971pt}{-54.11385pt}{-42.27971pt}{-55.68526pt}\pgfsys@lineto{-42.27971pt}{-65.02968pt}\pgfsys@curveto{-42.27971pt}{-66.60109pt}{-41.00584pt}{-67.87495pt}{-39.43443pt}{-67.87495pt}\pgfsys@lineto{79.67274pt}{-67.87495pt}\pgfsys@curveto{81.24416pt}{-67.87495pt}{82.51802pt}{-66.60109pt}{82.51802pt}{-65.02968pt}\pgfsys@lineto{82.51802pt}{-55.68526pt}\pgfsys@curveto{82.51802pt}{-54.11385pt}{81.24416pt}{-52.83998pt}{79.67274pt}{-52.83998pt}\pgfsys@closepath\pgfsys@moveto{-42.27971pt}{-67.87495pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-39.43443pt}{-60.35747pt}\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{\minipage[t]{119.10718pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{111.77466pt}{-110.36494pt}\pgfsys@lineto{-71.53635pt}{-110.36494pt}\pgfsys@curveto{-73.10776pt}{-110.36494pt}{-74.38162pt}{-111.63881pt}{-74.38162pt}{-113.21022pt}\pgfsys@lineto{-74.38162pt}{-121.7202pt}\pgfsys@curveto{-74.38162pt}{-123.29161pt}{-73.10776pt}{-124.56548pt}{-71.53635pt}{-124.56548pt}\pgfsys@lineto{111.77466pt}{-124.56548pt}\pgfsys@curveto{113.34607pt}{-124.56548pt}{114.61993pt}{-123.29161pt}{114.61993pt}{-121.7202pt}\pgfsys@lineto{114.61993pt}{-113.21022pt}\pgfsys@curveto{114.61993pt}{-111.63881pt}{113.34607pt}{-110.36494pt}{111.77466pt}{-110.36494pt}\pgfsys@closepath\pgfsys@moveto{-74.38162pt}{-124.56548pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-71.53635pt}{-117.46521pt}\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{\minipage[t]{183.311pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{} {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{-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{${@}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{-21.35193pt}{-13.53387pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-5.0889pt}{-2.20868pt}\pgfsys@lineto{-18.4943pt}{-8.02834pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{14.6054pt}{-14.85332pt}\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@moveto{5.0889pt}{-1.84567pt}\pgfsys@lineto{18.4943pt}{-6.7089pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{{{}{}{{}{}}{{}{{}{}}}{{}{{}{}}}{{}{{}{}}}{{}{}{{{{}{}}{}}}{{{{}{}}{}}}{}{{}}}}}{{}{}{{}{}}{{}{{}{}}}{{}{{}{}}}{{}{{}{}}}{{}{}{{{{}{}}{}}}{{{{}{}}{}}}{}{{}}}}{{{}}{{}}{}{}{}}{{}\pgfsys@moveto{4.26794pt}{-23.23544pt}\pgfsys@lineto{-2.53467pt}{-37.82372pt}\pgfsys@lineto{11.07056pt}{-37.82372pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{1.40565pt}{-36.82373pt}\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{${u}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {
{}{}{}}{}{{}{}{{}{}}{{}{{}{}}}{{}{{}{}}}{{}{{}{}}}{{}{}{{{{}{}}{}}}{{{{}{}}{}}}{}{{}}}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{13.4054pt}{-15.45161pt}\pgfsys@lineto{4.26794pt}{-22.7622pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{28.83179pt}{-26.23442pt}\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@moveto{23.58319pt}{-13.78058pt}\pgfsys@lineto{32.72069pt}{-18.09pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{20.3788pt}{-36.29608pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{27.63179pt}{-27.06923pt}\pgfsys@lineto{23.23643pt}{-30.79054pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{39.57414pt}{-35.32387pt}\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{${y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{37.80959pt}{-26.54765pt}\pgfsys@lineto{42.20494pt}{-29.81833pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\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}}\twoheadrightarrow_{\beta}\leavevmode\hbox
to75.3pt{\vbox to65.5pt{\pgfpicture\makeatletter\hbox{\hskip
22.35193pt\lower-61.0305pt\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\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{ {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{31.50026pt}{-12.60167pt}\pgfsys@lineto{8.73805pt}{-12.60167pt}\pgfsys@curveto{7.16664pt}{-12.60167pt}{5.89278pt}{-13.87553pt}{5.89278pt}{-15.44695pt}\pgfsys@lineto{5.89278pt}{-24.79137pt}\pgfsys@curveto{5.89278pt}{-26.36278pt}{7.16664pt}{-27.63664pt}{8.73805pt}{-27.63664pt}\pgfsys@lineto{31.50026pt}{-27.63664pt}\pgfsys@curveto{33.07167pt}{-27.63664pt}{34.34554pt}{-26.36278pt}{34.34554pt}{-24.79137pt}\pgfsys@lineto{34.34554pt}{-15.44695pt}\pgfsys@curveto{34.34554pt}{-13.87553pt}{33.07167pt}{-12.60167pt}{31.50026pt}{-12.60167pt}\pgfsys@closepath\pgfsys@moveto{5.89278pt}{-27.63664pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.03026pt}{-20.11916pt}\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{\minipage[t]{10.1778pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{59.55359pt}{-32.72083pt}\pgfsys@lineto{-19.31528pt}{-32.72083pt}\pgfsys@curveto{-20.88669pt}{-32.72083pt}{-22.16055pt}{-33.99469pt}{-22.16055pt}{-35.5661pt}\pgfsys@lineto{-22.16055pt}{-44.91052pt}\pgfsys@curveto{-22.16055pt}{-46.48193pt}{-20.88669pt}{-47.7558pt}{-19.31528pt}{-47.7558pt}\pgfsys@lineto{59.55359pt}{-47.7558pt}\pgfsys@curveto{61.125pt}{-47.7558pt}{62.39886pt}{-46.48193pt}{62.39886pt}{-44.91052pt}\pgfsys@lineto{62.39886pt}{-35.5661pt}\pgfsys@curveto{62.39886pt}{-33.99469pt}{61.125pt}{-32.72083pt}{59.55359pt}{-32.72083pt}\pgfsys@closepath\pgfsys@moveto{-22.16055pt}{-47.7558pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.31528pt}{-40.23831pt}\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{\minipage[t]{78.86887pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{79.67274pt}{-52.83998pt}\pgfsys@lineto{-39.43443pt}{-52.83998pt}\pgfsys@curveto{-41.00584pt}{-52.83998pt}{-42.27971pt}{-54.11385pt}{-42.27971pt}{-55.68526pt}\pgfsys@lineto{-42.27971pt}{-65.02968pt}\pgfsys@curveto{-42.27971pt}{-66.60109pt}{-41.00584pt}{-67.87495pt}{-39.43443pt}{-67.87495pt}\pgfsys@lineto{79.67274pt}{-67.87495pt}\pgfsys@curveto{81.24416pt}{-67.87495pt}{82.51802pt}{-66.60109pt}{82.51802pt}{-65.02968pt}\pgfsys@lineto{82.51802pt}{-55.68526pt}\pgfsys@curveto{82.51802pt}{-54.11385pt}{81.24416pt}{-52.83998pt}{79.67274pt}{-52.83998pt}\pgfsys@closepath\pgfsys@moveto{-42.27971pt}{-67.87495pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-39.43443pt}{-60.35747pt}\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{\minipage[t]{119.10718pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{111.77466pt}{-110.36494pt}\pgfsys@lineto{-71.53635pt}{-110.36494pt}\pgfsys@curveto{-73.10776pt}{-110.36494pt}{-74.38162pt}{-111.63881pt}{-74.38162pt}{-113.21022pt}\pgfsys@lineto{-74.38162pt}{-121.7202pt}\pgfsys@curveto{-74.38162pt}{-123.29161pt}{-73.10776pt}{-124.56548pt}{-71.53635pt}{-124.56548pt}\pgfsys@lineto{111.77466pt}{-124.56548pt}\pgfsys@curveto{113.34607pt}{-124.56548pt}{114.61993pt}{-123.29161pt}{114.61993pt}{-121.7202pt}\pgfsys@lineto{114.61993pt}{-113.21022pt}\pgfsys@curveto{114.61993pt}{-111.63881pt}{113.34607pt}{-110.36494pt}{111.77466pt}{-110.36494pt}\pgfsys@closepath\pgfsys@moveto{-74.38162pt}{-124.56548pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-71.53635pt}{-117.46521pt}\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{\minipage[t]{183.311pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{} {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{-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{${@}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{-21.35193pt}{-13.53387pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-5.0889pt}{-2.20868pt}\pgfsys@lineto{-18.4943pt}{-8.02834pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{14.6054pt}{-14.85332pt}\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@moveto{5.0889pt}{-1.84567pt}\pgfsys@lineto{18.4943pt}{-6.7089pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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.37904pt}{-26.23442pt}\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@moveto{13.4054pt}{-13.78058pt}\pgfsys@lineto{4.26794pt}{-18.09pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{-8.07394pt}{-36.29608pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-0.82095pt}{-27.06923pt}\pgfsys@lineto{-5.21631pt}{-30.79054pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{11.1214pt}{-35.32387pt}\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{${y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{9.35684pt}{-26.54765pt}\pgfsys@lineto{13.7522pt}{-29.81833pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{28.83179pt}{-26.23442pt}\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@moveto{23.58319pt}{-13.78058pt}\pgfsys@lineto{32.72069pt}{-18.09pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{}{}{}{}{}{}{}{}{}{}{}{}{}{{{}{}{{}{}}{{}{{}{}}}{{}{{}{}}}{{}{{}{}}}{{}{}{{{{}{}}{}}}{{{{}{}}{}}}{}{{}}}}}{{}{}{{}{}}{{}{{}{}}}{{}{{}{}}}{{}{{}{}}}{{}{}{{{{}{}}{}}}{{{{}{}}{}}}{}{{}}}}{{{}}{{}}{}{}{}}{{}\pgfsys@moveto{23.23643pt}{-34.61655pt}\pgfsys@lineto{16.43382pt}{-49.20482pt}\pgfsys@lineto{30.03905pt}{-49.20482pt}\pgfsys@closepath\pgfsys@stroke\pgfsys@invoke{
} }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.37415pt}{-48.20483pt}\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{${u}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {
{}{}{}}{}{{}{}{{}{}}{{}{{}{}}}{{}{{}{}}}{{}{{}{}}}{{}{}{{{{}{}}{}}}{{{{}{}}{}}}{}{{}}}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{28.82742pt}{-27.43442pt}\pgfsys@lineto{23.23643pt}{-34.14331pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{38.31604pt}{-37.61552pt}\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@moveto{37.80959pt}{-26.36137pt}\pgfsys@lineto{42.20494pt}{-29.4711pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{31.20285pt}{-48.99663pt}\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@moveto{37.2515pt}{-38.81552pt}\pgfsys@lineto{35.09175pt}{-40.8522pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{26.54356pt}{-59.05829pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{31.78017pt}{-50.19662pt}\pgfsys@lineto{29.4012pt}{-53.55275pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{38.1515pt}{-58.08607pt}\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{${y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{38.85939pt}{-50.19662pt}\pgfsys@lineto{40.7823pt}{-52.58054pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{46.68733pt}{-46.70497pt}\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{${y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{46.9145pt}{-38.81552pt}\pgfsys@lineto{49.31813pt}{-41.19943pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\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}}\twoheadrightarrow_{\beta}\leavevmode\hbox
to74.26pt{\vbox to65.5pt{\pgfpicture\makeatletter\hbox{\hskip
22.35193pt\lower-61.0305pt\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\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{ {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{31.50026pt}{-12.60167pt}\pgfsys@lineto{8.73805pt}{-12.60167pt}\pgfsys@curveto{7.16664pt}{-12.60167pt}{5.89278pt}{-13.87553pt}{5.89278pt}{-15.44695pt}\pgfsys@lineto{5.89278pt}{-24.79137pt}\pgfsys@curveto{5.89278pt}{-26.36278pt}{7.16664pt}{-27.63664pt}{8.73805pt}{-27.63664pt}\pgfsys@lineto{31.50026pt}{-27.63664pt}\pgfsys@curveto{33.07167pt}{-27.63664pt}{34.34554pt}{-26.36278pt}{34.34554pt}{-24.79137pt}\pgfsys@lineto{34.34554pt}{-15.44695pt}\pgfsys@curveto{34.34554pt}{-13.87553pt}{33.07167pt}{-12.60167pt}{31.50026pt}{-12.60167pt}\pgfsys@closepath\pgfsys@moveto{5.89278pt}{-27.63664pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.03026pt}{-20.11916pt}\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{\minipage[t]{10.1778pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{59.55359pt}{-32.72083pt}\pgfsys@lineto{-19.31528pt}{-32.72083pt}\pgfsys@curveto{-20.88669pt}{-32.72083pt}{-22.16055pt}{-33.99469pt}{-22.16055pt}{-35.5661pt}\pgfsys@lineto{-22.16055pt}{-44.91052pt}\pgfsys@curveto{-22.16055pt}{-46.48193pt}{-20.88669pt}{-47.7558pt}{-19.31528pt}{-47.7558pt}\pgfsys@lineto{59.55359pt}{-47.7558pt}\pgfsys@curveto{61.125pt}{-47.7558pt}{62.39886pt}{-46.48193pt}{62.39886pt}{-44.91052pt}\pgfsys@lineto{62.39886pt}{-35.5661pt}\pgfsys@curveto{62.39886pt}{-33.99469pt}{61.125pt}{-32.72083pt}{59.55359pt}{-32.72083pt}\pgfsys@closepath\pgfsys@moveto{-22.16055pt}{-47.7558pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.31528pt}{-40.23831pt}\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{\minipage[t]{78.86887pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{79.67274pt}{-52.83998pt}\pgfsys@lineto{-39.43443pt}{-52.83998pt}\pgfsys@curveto{-41.00584pt}{-52.83998pt}{-42.27971pt}{-54.11385pt}{-42.27971pt}{-55.68526pt}\pgfsys@lineto{-42.27971pt}{-65.02968pt}\pgfsys@curveto{-42.27971pt}{-66.60109pt}{-41.00584pt}{-67.87495pt}{-39.43443pt}{-67.87495pt}\pgfsys@lineto{79.67274pt}{-67.87495pt}\pgfsys@curveto{81.24416pt}{-67.87495pt}{82.51802pt}{-66.60109pt}{82.51802pt}{-65.02968pt}\pgfsys@lineto{82.51802pt}{-55.68526pt}\pgfsys@curveto{82.51802pt}{-54.11385pt}{81.24416pt}{-52.83998pt}{79.67274pt}{-52.83998pt}\pgfsys@closepath\pgfsys@moveto{-42.27971pt}{-67.87495pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-39.43443pt}{-60.35747pt}\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{\minipage[t]{119.10718pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{111.77466pt}{-110.36494pt}\pgfsys@lineto{-71.53635pt}{-110.36494pt}\pgfsys@curveto{-73.10776pt}{-110.36494pt}{-74.38162pt}{-111.63881pt}{-74.38162pt}{-113.21022pt}\pgfsys@lineto{-74.38162pt}{-121.7202pt}\pgfsys@curveto{-74.38162pt}{-123.29161pt}{-73.10776pt}{-124.56548pt}{-71.53635pt}{-124.56548pt}\pgfsys@lineto{111.77466pt}{-124.56548pt}\pgfsys@curveto{113.34607pt}{-124.56548pt}{114.61993pt}{-123.29161pt}{114.61993pt}{-121.7202pt}\pgfsys@lineto{114.61993pt}{-113.21022pt}\pgfsys@curveto{114.61993pt}{-111.63881pt}{113.34607pt}{-110.36494pt}{111.77466pt}{-110.36494pt}\pgfsys@closepath\pgfsys@moveto{-74.38162pt}{-124.56548pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-71.53635pt}{-117.46521pt}\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{\minipage[t]{183.311pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{} {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.8889pt}{-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{${@}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{-21.35193pt}{-13.53387pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-5.0889pt}{-2.20868pt}\pgfsys@lineto{-18.4943pt}{-8.02834pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{14.6054pt}{-14.85332pt}\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@moveto{5.0889pt}{-1.84567pt}\pgfsys@lineto{18.4943pt}{-6.7089pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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.37904pt}{-26.23442pt}\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@moveto{13.4054pt}{-13.78058pt}\pgfsys@lineto{4.26794pt}{-18.09pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{-8.07394pt}{-36.29608pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-0.82095pt}{-27.06923pt}\pgfsys@lineto{-5.21631pt}{-30.79054pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{11.1214pt}{-35.32387pt}\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{${y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{9.35684pt}{-26.54765pt}\pgfsys@lineto{13.7522pt}{-29.81833pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{28.83179pt}{-26.23442pt}\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@moveto{23.58319pt}{-13.78058pt}\pgfsys@lineto{32.72069pt}{-18.09pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{19.34753pt}{-37.61552pt}\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@moveto{27.63179pt}{-26.36137pt}\pgfsys@lineto{23.23643pt}{-29.4711pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{12.23434pt}{-48.99663pt}\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@moveto{18.28299pt}{-38.81552pt}\pgfsys@lineto{16.12325pt}{-40.8522pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{7.57506pt}{-59.05829pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{12.81166pt}{-50.19662pt}\pgfsys@lineto{10.4327pt}{-53.55275pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{19.183pt}{-58.08607pt}\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{${y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{19.89088pt}{-50.19662pt}\pgfsys@lineto{21.8138pt}{-52.58054pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{27.71883pt}{-46.70497pt}\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{${y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{27.946pt}{-38.81552pt}\pgfsys@lineto{30.34962pt}{-41.19943pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{43.40494pt}{-30.95276pt}\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{${\ddots}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\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}}\twoheadrightarrow_{\beta}\cdots$

The resulting infinite $\lambda$-tree is clearly not rational; in fact,
consider the subtrees defined by the left-hand cildren of every node on the
right-most path. Then the subtree rooted at the left-hand sucessor of the
$n$-th node on that path has the list $xy^{n}$ as its front of leaf labels.
And since this tree does not contain any $\lambda$-operators its
$\alpha$-equivalence class is a singleton, whence
$\operatorname{\mathsf{BT}}(u)\not\in\varrho{\mathsf{Lb}_{\alpha}}$.

Of course, there are also $\lambda$-terms, whose Böhm tree is infinitely large
but stays rational, for example:

$s:=Y_{({\lambda}g.{\lambda}x.{\lambda}y.x\,g\,y)))},\text{ with
}s\rightarrow_{\beta}({\lambda}g.{\lambda}x.{\lambda}y.x\,g\,y)))\,s\rightarrow_{\beta}{\lambda}x.{\lambda}y.x\,s\,y.\twoheadrightarrow_{\beta}\cdots\twoheadrightarrow_{\beta}\leavevmode\hbox
to76.07pt{\vbox to154.04pt{\pgfpicture\makeatletter\hbox{\hskip
28.45276pt\lower-96.93938pt\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\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{ {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{31.50026pt}{-12.60167pt}\pgfsys@lineto{8.73805pt}{-12.60167pt}\pgfsys@curveto{7.16664pt}{-12.60167pt}{5.89278pt}{-13.87553pt}{5.89278pt}{-15.44695pt}\pgfsys@lineto{5.89278pt}{-24.79137pt}\pgfsys@curveto{5.89278pt}{-26.36278pt}{7.16664pt}{-27.63664pt}{8.73805pt}{-27.63664pt}\pgfsys@lineto{31.50026pt}{-27.63664pt}\pgfsys@curveto{33.07167pt}{-27.63664pt}{34.34554pt}{-26.36278pt}{34.34554pt}{-24.79137pt}\pgfsys@lineto{34.34554pt}{-15.44695pt}\pgfsys@curveto{34.34554pt}{-13.87553pt}{33.07167pt}{-12.60167pt}{31.50026pt}{-12.60167pt}\pgfsys@closepath\pgfsys@moveto{5.89278pt}{-27.63664pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.03026pt}{-20.11916pt}\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{\minipage[t]{10.1778pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{ {}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{59.55359pt}{-32.72083pt}\pgfsys@lineto{-19.31528pt}{-32.72083pt}\pgfsys@curveto{-20.88669pt}{-32.72083pt}{-22.16055pt}{-33.99469pt}{-22.16055pt}{-35.5661pt}\pgfsys@lineto{-22.16055pt}{-44.91052pt}\pgfsys@curveto{-22.16055pt}{-46.48193pt}{-20.88669pt}{-47.7558pt}{-19.31528pt}{-47.7558pt}\pgfsys@lineto{59.55359pt}{-47.7558pt}\pgfsys@curveto{61.125pt}{-47.7558pt}{62.39886pt}{-46.48193pt}{62.39886pt}{-44.91052pt}\pgfsys@lineto{62.39886pt}{-35.5661pt}\pgfsys@curveto{62.39886pt}{-33.99469pt}{61.125pt}{-32.72083pt}{59.55359pt}{-32.72083pt}\pgfsys@closepath\pgfsys@moveto{-22.16055pt}{-47.7558pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.31528pt}{-40.23831pt}\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{\minipage[t]{78.86887pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{79.67274pt}{-52.83998pt}\pgfsys@lineto{-39.43443pt}{-52.83998pt}\pgfsys@curveto{-41.00584pt}{-52.83998pt}{-42.27971pt}{-54.11385pt}{-42.27971pt}{-55.68526pt}\pgfsys@lineto{-42.27971pt}{-65.02968pt}\pgfsys@curveto{-42.27971pt}{-66.60109pt}{-41.00584pt}{-67.87495pt}{-39.43443pt}{-67.87495pt}\pgfsys@lineto{79.67274pt}{-67.87495pt}\pgfsys@curveto{81.24416pt}{-67.87495pt}{82.51802pt}{-66.60109pt}{82.51802pt}{-65.02968pt}\pgfsys@lineto{82.51802pt}{-55.68526pt}\pgfsys@curveto{82.51802pt}{-54.11385pt}{81.24416pt}{-52.83998pt}{79.67274pt}{-52.83998pt}\pgfsys@closepath\pgfsys@moveto{-42.27971pt}{-67.87495pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-39.43443pt}{-60.35747pt}\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{\minipage[t]{119.10718pt}\endminipage}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{ {}{}{}}{{{
{}{}{}}}}{{{{}{}{}}}}{{{ {}{}{}}}}{{{ {}{}{}}}}{}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{} {\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\pgfsys@setdash{0.4pt,2.0pt}{0.0pt}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{111.77466pt}{-110.36494pt}\pgfsys@lineto{-71.53635pt}{-110.36494pt}\pgfsys@curveto{-73.10776pt}{-110.36494pt}{-74.38162pt}{-111.63881pt}{-74.38162pt}{-113.21022pt}\pgfsys@lineto{-74.38162pt}{-121.7202pt}\pgfsys@curveto{-74.38162pt}{-123.29161pt}{-73.10776pt}{-124.56548pt}{-71.53635pt}{-124.56548pt}\pgfsys@lineto{111.77466pt}{-124.56548pt}\pgfsys@curveto{113.34607pt}{-124.56548pt}{114.61993pt}{-123.29161pt}{114.61993pt}{-121.7202pt}\pgfsys@lineto{114.61993pt}{-113.21022pt}\pgfsys@curveto{114.61993pt}{-111.63881pt}{113.34607pt}{-110.36494pt}{111.77466pt}{-110.36494pt}\pgfsys@closepath\pgfsys@moveto{-74.38162pt}{-124.56548pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-71.53635pt}{-117.46521pt}\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{\minipage[t]{183.311pt}\endminipage} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{} {{}}{{{
{}{}{}}}}{}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{
{}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.7743pt}{-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{${{\lambda}x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{-5.54747pt}{-16.72638pt}\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{${{\lambda}y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{ {}{}{}}}}{}{
{}{}{}}{}{ {}{}{}} {}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{0.0pt}{-4.67221pt}\pgfsys@lineto{0.0pt}{-8.58194pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\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.88889pt}{-31.92497pt}\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@moveto{0.0pt}{-19.87082pt}\pgfsys@lineto{0.00002pt}{-23.78055pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{-13.37314pt}{-43.30608pt}\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@moveto{-5.08888pt}{-32.05193pt}\pgfsys@lineto{-9.48424pt}{-35.16165pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\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}{-19.45506pt}{-53.36774pt}\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{${x}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-13.62375pt}{-44.50607pt}\pgfsys@lineto{-16.59743pt}{-47.8622pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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.37105pt}{-51.21497pt}\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}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\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}{6.85347pt}{-41.01442pt}\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{${y}$}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{5.08891pt}{-32.2382pt}\pgfsys@lineto{9.48427pt}{-35.50888pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@beginscope\pgfsys@invoke{ }{ {}{}{}}{}{}{}{{}}{} {
{}{}{}}{}{{}}{}{}{}{}{{}}{} { {}{}{}}{}{ {}{}{}}{}{}{{}}{ {}{}{}}{}{}{
{}{}{}}{}{{}}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{{{{{{}}{
{}{}}{}{}{{}{}}}}}{}{}{}{}}{}\pgfsys@moveto{-4.81474pt}{-44.50607pt}\pgfsys@curveto{47.42128pt}{-96.73938pt}{28.45276pt}{56.90552pt}{2.33475pt}{4.67221pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

The rational $\lambda$-tree on the right above, call it $r$, is the Böhm tree
for $s$, i.e.
$\operatorname{\mathsf{BT}}(s)=r\in\varrho{\mathsf{Lb}_{\alpha}}$. In other
words the subcoalgebra $S$ of $(\Lambda^{\infty}_{\alpha},b)$ above generated
by $[s]_{\alpha}$ is orbit-finite, hence the restriction of
$\operatorname{\mathsf{BT}}$ to $S$ factorizes through
$\varrho{\mathsf{Lb}_{\alpha}}$.

Can one characterize the largest subcoalgebra of
$(\Lambda^{\infty}_{\alpha},b)$ whose image under $\operatorname{\mathsf{BT}}$
lies in $\varrho{\mathsf{Lb}_{\alpha}}$? We leave this question for further
work.

##  5\. Conclusion and Future Work

We have contributed to the abstract algebraic study of variable binding using
nominal sets. In particular, we have extended a recent coalgebraic approach to
infinitary $\lambda$-calculus due to Kurz et al. Whereas they proved in [18]
that $\lambda$-trees with finitely many variables modulo $\alpha$-equivalence
form the final coalgebra for the functor $L_{\alpha}$ on $\mathsf{Nom}$ we
have given a characterization of the rational fixpoint of that functor. It
contains precisely the rational $\lambda$-trees modulo $\alpha$-equivalence.

This characterization entails a corecursion principle for rational
$\lambda$-trees because the rational fixpoint is the final locally orbit-
finite coalgebra for $L_{\alpha}$. In this sense we have achieved finitary
corecursion for the infinitary $\lambda$-calculus. We have demonstrated the
new principle and its limitations with two applications: a corecursive
definition of substitution and of a normalform computation.

Our work is only a first step in the study of the coalgebraic approach to
finitary coinduction for infinitary terms with variable binding operators.