16120 LABEL:LastPageOct. 12, 2018Feb. 18, 2020

# Recursion Schemes, the MSO Logic, and the $\mathsf{U}$ quantifier

Paweł Parys  Institute of Informatics, University of Warsaw
<EMAIL_ADDRESS>
###### Abstract.

We study the model-checking problem for recursion schemes: does the tree
generated by a given higher-order recursion scheme satisfy a given logical
sentence. The problem is known to be decidable for sentences of the MSO logic.
We prove decidability for an extension of MSO in which we additionally have an
unbounding quantifier $\mathsf{U}$, saying that a subformula is true for
arbitrarily large finite sets. This quantifier can be used only for
subformulae in which all free variables represent finite sets (while an
unrestricted use of the quantifier leads to undecidability).

We also show that the logic has the properties of reflection and effective
selection for trees generated by recursion schemes.

###### Key words and phrases:

higher-order recursion schemes, intersection types, WMSO+$\mathsf{U}$ logic,
boundedness

Work supported by the National Science Centre, Poland (grant no.
2016/22/E/ST6/00041).

##  1\. Introduction

_Higher-order recursion schemes_ (_schemes_ in short) are used to faithfully
represent the control flow of programs in languages with higher-order
functions [Dam82, KNU02, Ong06, Kob13]. This formalism is equivalent via
direct translations to simply-typed $\lambda Y$-calculus [SW16]. Collapsible
pushdown systems [HMOS08] and ordered tree-pushdown systems [CPSW15] are other
equivalent formalisms. Schemes cover some other models such as indexed
grammars [Aho68] and ordered multi-pushdown automata [BCCC96].

In our setting, a scheme is a finite description of an infinite tree. A useful
property of schemes is that the _MSO-model-checking problem_ for schemes is
decidable. This means that given a scheme ${\mathcal{G}}$ and an MSO sentence
$\varphi$, it can be algorithmically decided whether the tree generated by
${\mathcal{G}}$ satisfies $\varphi$. This result has several different proofs
[Ong06, HMOS08, KO09, SW14], and also some extensions like global model
checking [BO09], logical reflection [BCOS10], effective selection [CS12],
existence of lambda-calculus model [SW15a]. When the property of trees is
given as an automaton, not as a formula, the model-checking problem can be
solved efficiently, in the sense that there exist implementations working in a
reasonable running time [Kob13, Kob11, BK13, RNO14, NO14] (most tools cover
only a fragment of MSO, though).

Recently, an interest has arisen in model-checking trees generated by schemes
against properties not expressible in the MSO logic. These are properties
expressing boundedness and unboundedness of some quantities. More precisely,
it was shown that the _simultaneous unboundedness problem_ (aka.  _diagonal
problem_) for schemes is decidable [HKO16, CPSW16, Par17]. This problem asks,
given a scheme ${\mathcal{G}}$ and a set of letters $A$, whether for every
$n\in\mathbb{N}$ there exists a path in the tree generated by ${\mathcal{G}}$
such that every letter from $A$ appears on this path at least $n$ times. This
result turns out to be interesting, because it entails other decidability
results for recursion schemes, concerning in particular computability of the
downward closure of recognized languages [Zet15], and the problem of
separability by piecewise testable languages [CMvRZ15].

In this paper we show a result of a more general style. Instead of considering
a particular property, like in the simultaneous unboundedness problem, we
consider a logic capable to express properties talking about boundedness. More
precisely, we extend the MSO logic by the unbounding quantifier, $\mathsf{U}$
[Boj04]. A formula using this quantifier, $\mathsf{U}\mathsf{X}.\varphi$, says
that $\varphi$ holds for arbitrarily large finite sets $\mathsf{X}$. We impose
a restriction that $\mathsf{U}\mathsf{X}.\varphi$ can be used only in a
context where all free variables of $\varphi$ represent finite sets. We call
the resulting logic MSO+$\mathsf{U^{fin}}$.

The goal of this paper is to prove the following theorem.

######  Theorem 1.

It is decidable whether the tree generated by a given scheme satisfies a given
MSO+$\mathsf{U^{fin}}$ sentence.

We remark that the MSO+$\mathsf{U^{fin}}$ logic extends the WMSO+$\mathsf{U}$
logic, which was widely considered in the context of infinite words [Boj11]
and infinite trees [GK10, BT12, Boj14]. The difference is that in
WMSO+$\mathsf{U}$ only quantification over finite sets is allowed. In
consequence, WMSO+$\mathsf{U}$ cannot express all properties of MSO [HM12]. On
the other hand, in MSO+$\mathsf{U^{fin}}$ we allow quantification over
infinite sets like in standard MSO, and we only restrict the use of the
$\mathsf{U}$ quantifier to subformulae in which all free variables represent
finite sets.

Furthermore, we remark that some restriction for the $\mathsf{U}$ quantifier
is necessary. Indeed, the model-checking problem for the full MSO+$\mathsf{U}$
logic (where the $\mathsf{U}$ quantifier can be used in an unrestricted way)
is undecidable already over the infinite word without labels [BPT16], so even
more over all fancy trees that can be generated by higher-order recursion
schemes.

While proving Theorem 1, we depend on several earlier results. First, we
translate MSO+$\mathsf{U^{fin}}$ formulae to an equivalent automata model
using the notion of logical types (aka. composition method) following a long
series of previous work (some selection: [FV59, She75, Lä68, BCL08, GK10,
PT16]). Second, we use the logical-reflection property of schemes [BCOS10]. It
says that given a scheme ${\mathcal{G}}$ and an MSO sentence $\varphi$ one can
construct a scheme ${\mathcal{G}}_{\varphi}$ generating the same tree as
${\mathcal{G}}$, where in every node it is additionally written whether
$\varphi$ is satisfied in the subtree starting in this node. Third, we use an
analogous property for the simultaneous unboundedness problem, called _SUP
reflection_ [Par18b]: given a scheme ${\mathcal{G}}$ we can construct a scheme
${\mathcal{G}}_{\mathit{SUP}}$ generating the same tree as ${\mathcal{G}}$,
where every node is additionally annotated by the solution of the simultaneous
unboundedness problem in the subtree starting in this node. Finally, we use
the fact that schemes can be composed with finite tree transducers
transforming the generated trees; this follows directly from the equivalence
between schemes and collapsible pushdown systems [HMOS08].

Although our algorithm depends on a solution to the simultaneous unboundedness
problem, it is not known whether the simultaneous unboundedness problem itself
can be expressed in MSO+$\mathsf{U^{fin}}$. The difficulty is that every
$\mathsf{U}$ quantifier can entail unboundedness only of a single quantity,
and it seems difficult to express simultaneous unboundedness of multiple
quantities in MSO+$\mathsf{U^{fin}}$.

This paper is an extended version of a conference paper [Par18a], where the
result is shown for the WMSO+$\mathsf{U}$ logic. Besides the fact that we work
here with a slightly stronger logic (namely, with MSO+$\mathsf{U^{fin}}$
instead of WMSO+$\mathsf{U}$), our proofs follow basically the same ideas as
proofs contained in the conference paper [Par18a]. We remark that the
conference paper [Par18a] contained additionally a justification of the SUP-
reflection property for schemes. This justification was already expanded in
another paper [Par18b], and for this reason we do not include it here.

Our paper is structured as follows. In Section 2 we introduce all necessary
definitions. In Section 3 we show how to translate MSO+$\mathsf{U^{fin}}$
sentences to automata. In Section 4 we prove the main theorem. Section 5
contains a few extensions of the main theorem.

##  2\. Preliminaries

The powerset of a set $X$ is denoted ${\mathcal{P}}(X)$, and the set of finite
subsets of $X$ is denoted ${\mathcal{P}}^{\mathsf{fin}}(X)$. For a relation
$r$, we write $r^{*}$ for the reflexive transitive closure of $r$. When $f$ is
a function, by $f[x\mapsto y]$ we mean the function that maps $x$ to $y$ and
every other $z\in\mathrm{dom}(f)$ to $f(z)$.

### Infinitary lambda-calculus.

We consider infinitary, simply-typed lambda-calculus. In particular, each
lambda-term has an associated sort (aka. simple type). The set of _sorts_ is
constructed from a unique ground sort $\mathsf{o}$ using a binary operation
$\mathbin{\to}$; namely $\mathsf{o}$ is a sort, and if $\alpha$ and $\beta$
are sorts, so is $\alpha\mathbin{\to}\beta$. By convention, $\mathbin{\to}$
associates to the right, that is,
$\alpha\mathbin{\to}\beta\mathbin{\to}\gamma$ is understood as
$\alpha\mathbin{\to}(\beta\mathbin{\to}\gamma)$.

While defining lambda-terms we assume a set of variables
$\mathit{Vars}^{\lambda}=\\{x^{\alpha},y^{\beta},z^{\gamma},\dots\\}$
containing infinitely many variables of every sort (sort of a variable is
written in superscript). _Infinitary lambda-terms_ (or just _lambda-terms_)
are defined by coinduction, according to the following rules:

  * •

node constructor—if $K_{1}^{\mathsf{o}},\dots,K_{r}^{\mathsf{o}}$ are lambda-
terms, and $a$ is an arbitrary object, called a _letter_ , then $(a\langle
K_{1}^{\mathsf{o}},\dots,K_{r}^{\mathsf{o}}\rangle)^{\mathsf{o}}$ is a lambda-
term,

  * •

variable—every variable $x^{\alpha}\in\mathit{Vars}^{\lambda}$ is a lambda-
term,

  * •

application—if $K^{\alpha\mathbin{\to}\beta}$ and $L^{\alpha}$ are lambda-
terms, then $(K^{\alpha\mathbin{\to}\beta}\,L^{\alpha})^{\beta}$ is a lambda-
term, and

  * •

lambda-binder—if $K^{\beta}$ is a lambda-term and $x^{\alpha}$ is a variable,
then $(\lambda x^{\alpha}.K^{\beta})^{\alpha\mathbin{\to}\beta}$ is a lambda-
term.

Sets of letters are called _alphabets_. We use unranked letters; this subsumes
the setting of ranked letters. We naturally identify lambda-terms differing
only in names of bound variables. We often omit the sort annotations of
lambda-terms, but we keep in mind that every lambda-term (and every variable)
has a fixed sort. Free variables and subterms of a lambda-term, as well as
beta-reductions, are defined as usual. A lambda-term $K$ is _closed_ if it has
no free variables. We restrict ourselves to those lambda-terms for which the
set of sorts of all subterms is finite.

### Trees; Böhm trees.

A _tree_ is defined as a lambda-term that is built using only node
constructors, that is, not using variables, applications, nor lambda-binders.
For a tree $T=a\langle T_{1},\dots,T_{r}\rangle$, its set of nodes is defined
as the smallest set such that

  * •

$\varepsilon$ is a node of $T$, labeled by $a$, and

  * •

if $u$ is a node of $T_{i}$ for some $i\in\\{1,\dots,r\\}$, labeled by $b$,
then $iu$ is a node of $T$, also labeled by $b$.

A node $v$ is the _$i$ -th child_ of $u$ if $v=ui$. We say that two trees
$T,T^{\prime}$ are of _the same shape_ if they have the same nodes. A tree $T$
is _over alphabet $\Sigma$_ if all labels of its nodes belong to $\Sigma$, and
it has _maximal arity_ $r_{\max}\in\mathbb{N}$ if its every node has at most
$r_{\max}$ children. When both these conditions are satisfied, we say that $T$
is a _$(\Sigma,r_{\max})$ -tree_. For a tree $T$ and its node $u$, by
$T{\restriction}_{u}$ we denote the _subtree_ of $T$ starting at $u$, defined
in the expected way.

We consider Böhm trees only for closed lambda-terms of sort $\mathsf{o}$. For
such a lambda-term $K$, its _Böhm tree_ is constructed by coinduction, as
follows: if there is a sequence of beta-reductions from $K$ to a lambda-term
of the form $a\langle K_{1},\dots,K_{r}\rangle$, and $T_{1},\dots,T_{r}$ are
Böhm trees of $K_{1},\dots,K_{r}$, respectively, then $a\langle
T_{1},\dots,T_{r}\rangle$ is a Böhm tree of $K$; if there is no such sequence
of beta-reductions from $K$, then $\omega\langle\rangle$ is a Böhm tree of $K$
(where $\omega$ is a fixed letter). It is folklore that every closed lambda-
term of sort $\mathsf{o}$ has exactly one Böhm tree (the order in which beta-
reductions are performed does not matter); this tree is denoted by
$\mathit{BT}(K)$.

A closed lambda-term $K$ of sort $\mathsf{o}$ is called _fully convergent_ if
every node of $\mathit{BT}(K)$ is explicitly created by a node constructor
from $K$ (e.g., $\omega\langle\rangle$ is fully convergent, while $K=(\lambda
x^{\mathsf{o}}.x)\,K$ is not). More formally: we consider the lambda-term
$K_{-\omega}$ obtained from $K$ by replacing $\omega$ with some other letter
$\omega^{\prime}$, and we say that $K$ is fully convergent if in
$\mathit{BT}(K_{-\omega})$ there are no $\omega$-labeled nodes.

### Higher-order recursion schemes.

Our definition of schemes is less restrictive than usually, as we see them
only as finite representations of infinite lambda-terms. Thus a _higher-order
recursion scheme_ (or just a _scheme_) is a triple
${\mathcal{G}}=({\mathcal{N}},{\mathcal{R}},N_{\mathsf{0}}^{\mathsf{o}})$,
where

  * •

${\mathcal{N}}\subseteq\mathit{Vars}^{\lambda}$ is a finite set of
nonterminals,

  * •

${\mathcal{R}}$ is a function that maps every nonterminal $N\in{\mathcal{N}}$
to a finite lambda-term whose all free variables are contained in
${\mathcal{N}}$ and whose sort equals the sort of $N$, and

  * •

$N_{\mathsf{0}}^{\mathsf{o}}\in{\mathcal{N}}$ is a starting nonterminal, being
of sort $\mathsf{o}$.

We assume that elements of ${\mathcal{N}}$ are not used as bound variables,
and that ${\mathcal{R}}(N)$ is not a nonterminal for any $N\in{\mathcal{N}}$.

For a scheme ${\mathcal{G}}=({\mathcal{N}},{\mathcal{R}},N_{\mathsf{0}})$, and
for a lambda-term $K$ whose free variables are contained in ${\mathcal{N}}$,
we define the infinitary lambda-term _represented by_ $K$ with respect to
${\mathcal{G}}$, denoted $\Lambda_{\mathcal{G}}(K)$, by coinduction: to obtain
$\Lambda_{\mathcal{G}}(K)$ we replace in $K$ every nonterminal
$N\in{\mathcal{N}}$ with $\Lambda_{\mathcal{G}}({\mathcal{R}}(N))$. Observe
that $\Lambda_{\mathcal{G}}(K)$ is a closed lambda-term of the same sort as
$K$. The infinitary lambda-term _represented by_ ${\mathcal{G}}$, denoted
$\Lambda({\mathcal{G}})$, equals $\Lambda_{\mathcal{G}}(N_{\mathsf{0}})$.

By the _tree generated by ${\mathcal{G}}$_ we mean
$\mathit{BT}(\Lambda({\mathcal{G}}))$. We write $\Sigma_{\mathcal{G}}$ for the
finite alphabet containing $\omega$ and letters used in node constructors
appearing in ${\mathcal{G}}$, and $r_{\max}({\mathcal{G}})$ for the maximal
arity of node constructors appearing in ${\mathcal{G}}$. Clearly
$\mathit{BT}(\Lambda({\mathcal{G}}))$ is a
$(\Sigma_{\mathcal{G}},r_{\max}({\mathcal{G}}))$-tree.

In our constructions it is convenient to consider only schemes representing
fully-convergent lambda-terms, which is possible due to the following standard
result.

######  Fact 2 ([Had12, SW15b]).

For every scheme ${\mathcal{G}}$ we can construct a scheme
${\mathcal{G}}^{\prime}$ generating the same tree as ${\mathcal{G}}$, and such
that $\Lambda({\mathcal{G}}^{\prime})$ is fully convergent. ∎

######  Example 3.

Consider the scheme
${\mathcal{G}}_{1}=(\\{M^{\mathsf{o}},N^{\mathsf{o}\mathbin{\to}\mathsf{o}}\\},{\mathcal{R}},M)$,
where

$\displaystyle{\mathcal{R}}(N)=\lambda x^{\mathsf{o}}.a\langle x,N\,(b\langle
x\rangle)\rangle\,,$ and
$\displaystyle{\mathcal{R}}(M)=N\,(c\langle\rangle)\,.$

We obtain $\Lambda({\mathcal{G}}_{1})=K\,(c\langle\rangle)$, where $K$ is the
unique lambda-term for which it holds $K=\lambda x^{\mathsf{o}}.a\langle
x,K\,(b\langle x\rangle)\rangle$. The tree generated by ${\mathcal{G}}_{1}$
equals $a\langle T_{0},a\langle T_{1},a\langle
T_{2},\dots\rangle\rangle\rangle$, where $T_{0}=c\langle\rangle$ and
$T_{i}=b\langle T_{i-1}\rangle$ for all $i\geq 1$.

######  Remark.

An usual definition of schemes is more restrictive than ours: it is required
that ${\mathcal{R}}(N)$ is a of the form $\lambda x_{1}.\cdots{}.\lambda
x_{s}.K$, where $K$ is of sort $\mathsf{o}$ and does not use any lambda-
binders. We do not have this requirement, so possibly ${\mathcal{R}}(N)$ does
not start with a full sequence of lambda-binders, and possibly some lambda-
binders are nested deeper in the lambda-term. It is, though, not difficult to
convert a scheme respecting only our definition to a scheme satisfying these
additional requirements (at the cost of introducing more nonterminals). We
can, for example, use a translation between schemes and $\lambda Y$-terms from
Salvati and Walukiewicz [SW16]: their translation from schemes to $\lambda
Y$-terms works well with our definition of schemes, while the translation from
$\lambda Y$-terms to schemes produces schemes respecting the more restrictive
definition.

Another difference is that in the definition of the Böhm tree we allow
arbitrary beta-reductions, while it is sometimes assumed that only outermost
beta-reductions are allowed. It is a folklore that these two definitions are
equivalent.

There is one more difference: we expand a scheme to an infinite lambda-term,
and then we operate on this lambda-term, while often finite lambda-terms
containing nonterminals are considered, and appearances of nonterminals are
expanded only when needed. This is a purely syntactical difference.

### MSO+$\mathsf{U^{fin}}$.

For technical convenience, we use a syntax in which there are no first-order
variables. It is easy to translate a formula from a more standard syntax to
ours (at least when the maximal arity of considered trees is fixed). We assume
two infinite sets of variables, ${\mathcal{V}}^{\mathsf{fin}}$ and
${\mathcal{V}}^{\mathsf{inf}}$, and we let
${\mathcal{V}}={\mathcal{V}}^{\mathsf{fin}}\uplus{\mathcal{V}}^{\mathsf{inf}}$.
Variables from ${\mathcal{V}}^{\mathsf{fin}}$ are used to quantify over finite
sets, while variables from ${\mathcal{V}}^{\mathsf{inf}}$ over arbitrary
(potentially infinite) sets. In the syntax of MSO+$\mathsf{U^{fin}}$ we have
the following constructions:

$\displaystyle\varphi::=a(\mathsf{X})\mid\mathsf{X}\curlywedgedownarrow_{i}\mathsf{Y}\mid\mathsf{X}\subseteq\mathsf{Y}\mid\varphi_{1}\land\varphi_{2}\mid\neg\varphi^{\prime}\mid\exists\mathsf{Z}.\varphi^{\prime}\mid{\exists_{\mathsf{fin}}}\mathsf{F}.\varphi^{\prime}\mid\mathsf{U}\mathsf{F}.\varphi^{\prime}$

where $a$ is a letter, and $i\in\mathbb{N}_{+}$, and
$\mathsf{X},\mathsf{Y}\in{\mathcal{V}}$, and
$\mathsf{Z}\in{\mathcal{V}}^{\mathsf{inf}}$, and
$\mathsf{F}\in{\mathcal{V}}^{\mathsf{fin}}$. Free variables of a formula are
defined as usual; in particular $\mathsf{U}\mathsf{F}$ is a quantifier, hence
it bounds the variable $\mathsf{F}$. We impose the restriction that
$\mathsf{U}\mathsf{F}.\varphi^{\prime}$ can be used only when all free
variables of $\varphi^{\prime}$ are from ${\mathcal{V}}^{\mathsf{fin}}$.

The MSO logic is defined likewise, with the exception that the $\mathsf{U}$
quantifier is disallowed. (The fact that a set of tree nodes is finite is
expressible in MSO without using the ${\exists_{\mathsf{fin}}}$ quantifier,
thus presence of this quantifier does not change the expressive power of MSO).

We evaluate formulae of MSO+$\mathsf{U^{fin}}$ in $\Sigma$-labeled trees. In
order to evaluate a formula $\varphi$ in a tree $T$, we also need a
_valuation_ , that is, a partial function $\nu$ from ${\mathcal{V}}$ to sets
of nodes of $T$, such that $\nu(\mathsf{F})$ is finite whenever
$\mathsf{F}\in{\mathcal{V}}^{\mathsf{fin}}\cap\mathrm{dom}(\nu)$. The function
should be defined at least for all free variables of $\varphi$. The semantics
is defined as follows:

  * •

$a(\mathsf{X})$ holds when every node in $\nu(\mathsf{X})$ is labeled by $a$,

  * •

$\mathsf{X}\curlywedgedownarrow_{i}\mathsf{Y}$ holds when both
$\nu(\mathsf{X})$ and $\nu(\mathsf{Y})$ are singletons, and the unique node in
$\nu(\mathsf{Y})$ is the $i$-th child of the unique node in $\nu(\mathsf{X})$,

  * •

$\mathsf{X}\subseteq\mathsf{Y}$ holds when
$\nu(\mathsf{X})\subseteq\nu(\mathsf{Y})$,

  * •

$\varphi_{1}\land\varphi_{2}$ holds when both $\varphi_{1}$ and $\varphi_{2}$
hold,

  * •

$\neg\varphi^{\prime}$ holds when $\varphi^{\prime}$ does not hold,

  * •

$\exists\mathsf{Z}.\varphi^{\prime}$ holds when $\varphi^{\prime}$ holds for
an extension of $\nu$ that maps $\mathsf{Z}$ to some set of nodes of $T$,

  * •

${\exists_{\mathsf{fin}}}\mathsf{F}.\varphi^{\prime}$ holds when
$\varphi^{\prime}$ holds for an extension of $\nu$ that maps $\mathsf{F}$ to
some finite set of nodes of $T$, and

  * •

$\mathsf{U}\mathsf{F}.\varphi^{\prime}$ holds when for every $n\in\mathbb{N}$,
$\varphi^{\prime}$ holds for an extension of $\nu$ that maps $\mathsf{F}$ some
finite set of nodes of $T$ of cardinality at least $n$.

We write $T,\nu\models\varphi$ to denote that $\varphi$ holds in $T$ with
respect to the valuation $\nu$.

In order to see that our definition of MSO+$\mathsf{U^{fin}}$ is not too poor,
let us write a few example formulae.

  * •

The fact that $\mathsf{X}$ represents an empty set can be expressed as
$\mathit{empty}(\mathsf{X})\equiv a(\mathsf{X})\land b(\mathsf{X})$ (where
$a,b$ are any two different letters).

  * •

The fact that $\mathsf{X}$ represents a set of size at least $2$ can be
expressed as
$\mathit{big}(\mathsf{X})\equiv\exists\mathsf{Y}.(\mathsf{Y}\subseteq\mathsf{X}\land\neg(\mathsf{X}\subseteq\mathsf{Y})\land\neg\mathit{empty}(\mathsf{Y}))$.

  * •

The fact that $\mathsf{X}$ represents a singleton can be expressed as
$\mathit{sing}(\mathsf{X})\equiv\neg\mathit{empty}(\mathsf{X})\land\neg\mathit{big}(\mathsf{X})$.

  * •

When we only consider trees of a fixed maximal arity $r_{\max}$, the fact that
$\mathsf{X}$ and $\mathsf{Y}$ represent singletons $\\{x\\},\\{y\\}$,
respectively, such that $y$ is a child of $x$ can be expressed as

$\displaystyle(\mathsf{X}\curlywedgedownarrow_{1}\mathsf{Y})\lor\dots\lor(\mathsf{X}\curlywedgedownarrow_{r_{\max}}\mathsf{Y})\,,$

where $\varphi_{1}\lor\varphi_{2}$ stands for
$\neg(\neg\varphi_{1}\land\neg\varphi_{2})$.

  * •

Let $A=\\{a_{1},\dots,a_{k}\\}$ be a finite set of letters. The fact every
node in the set represented by $\mathsf{X}$ has label in $A$ can be expressed
as

$\displaystyle\forall\mathsf{Y}.(\mathit{sing}(\mathsf{Y})\land\mathsf{Y}\subseteq\mathsf{X})\mathbin{\to}(a_{1}(\mathsf{Y})\lor\dots\lor
a_{k}(\mathsf{Y}))\,,$

where $\forall\mathsf{Y}.\varphi$ stands for
$\neg\exists\mathsf{Y}.\neg\varphi$, and $\varphi_{1}\mathbin{\to}\varphi_{2}$
stands for $\neg(\varphi_{1}\land\neg\varphi_{2})$.

Like in most logics, in MSO+$\mathsf{U^{fin}}$ we can relativize formulae, as
described by Fact 4.

######  Fact 4.

Let $r_{\max}\in\mathbb{N}$. For every MSO+$\mathsf{U^{fin}}$ sentence
$\varphi$ we can construct an MSO+$\mathsf{U^{fin}}$ formula
$\widehat{\varphi}(\mathsf{X})$ with one free variable $\mathsf{X}$ such that
for every tree $T$ of maximal arity $r_{\max}$ and every valuation $\nu$, it
holds $T,\nu\models\widehat{\varphi}$ if and only if $\varphi$ holds in
$T{\restriction}_{u}$ for every $u\in\nu(\mathsf{X})$.

######  Proof 2.1 (Proof sketch).

Suppose first that we want to construct a formula
$\varphi^{\prime}(\mathsf{X})$ that satisfies the fact only for valuations
mapping $\mathsf{X}$ to singleton sets $\\{u\\}$. To this end, we need to
relativize quantification in $\varphi$ to the subtree starting in $u$. This
means that we replace subformulae of the form $\exists\mathsf{Y}.\psi$ (and
likewise ${\exists_{\mathsf{fin}}}\mathsf{Y}.\psi$ and
$\mathsf{U}\mathsf{Y}.\psi$) by
$\exists\mathsf{Y}.\eta(\mathsf{X},\mathsf{Y})\land\psi$, where
$\eta(\mathsf{X},\mathsf{Y})$ says that the set represented by $\mathsf{Y}$
contains only (not necessarily proper) descendants of the node represented by
$\mathsf{X}$.

We conclude by taking
$\widehat{\varphi}(\mathsf{X})\equiv\forall\mathsf{X}^{\prime}.(\mathit{sing}(\mathsf{X}^{\prime})\land\mathsf{X}^{\prime}\subseteq\mathsf{X})\mathbin{\to}\varphi^{\prime}(\mathsf{X}^{\prime})$,
saying that the formula $\varphi^{\prime}(\mathsf{X}^{\prime})$ holds whenever
$\mathsf{X}^{\prime}$ represents a singleton subset of the set represented by
$\mathsf{X}$.

##  3\. Nested $\mathsf{U}$-prefix MSO automata

In this section we give a definition of nested $\mathsf{U}$-prefix MSO
automata, a formalism equivalent to the MSO+$\mathsf{U^{fin}}$ logic. These
are compositions of $\mathsf{U}$-prefix automata and MSO automata, defined
below.

A _$\mathsf{U}$ -prefix automaton_ is a tuple
${\mathcal{A}}=(\Sigma,Q,Q_{\mathsf{imp}},\Delta)$, where $\Sigma$ is a finite
alphabet, $Q$ is a finite set of states, $Q_{\mathsf{imp}}\subseteq Q$ is a
set of _important_ states, and $\Delta\subseteq
Q\times\Sigma\times(Q\cup\\{\top\\})^{*}$ is a finite transition relation (we
assume $\top\not\in Q$). A _run_ of ${\mathcal{A}}$ on a $\Sigma$-labeled tree
$T$ is a mapping $\rho$ from the set of nodes of $T$ to $Q\cup\\{\top\\}$ such
that

  * •

there are only finitely many nodes $u$ such that $\rho(u)\in Q$, and

  * •

for every node $u$ of $T$, with label $a$ and $r$ children, it holds that
either $\rho(u)=\top=\rho(u1)=\dots=\rho(ur)$ or
$(\rho(u),a,\rho(u1),\dots,\rho(ur))\in\Delta$.

We use $\mathsf{U}$-prefix automata as transducers, relabeling nodes of $T$:
we define ${\mathcal{A}}(T)$ to be the tree of the same shape as $T$, and such
that its every node $u$ originally labeled by $a_{u}$ becomes labeled by the
pair $(a_{u},f_{u})$, where $f_{u}\colon Q\to\\{0,1,2\\}$ is the function that
assigns to every state $q\in Q$

  * •

$2$, if for every $n\in\mathbb{N}$ there is a run $\rho_{n}$ of
${\mathcal{A}}$ on $T{\restriction}_{u}$ that assigns $q$ to the root of
$T{\restriction}_{u}$, and such that for at least $n$ nodes $w$ it holds that
$\rho_{n}(w)\in Q_{\mathsf{imp}}$;

  * •

$1$, if the above does not hold, but there is a run of ${\mathcal{A}}$ on
$T{\restriction}_{u}$ that assigns $q$ to the root of $T{\restriction}_{u}$;

  * •

$0$, if none of the above holds.

######  Example 5.

Consider the $\mathsf{U}$-prefix automaton
${\mathcal{A}}_{1}=(\\{a\\},\\{q_{\exists\mathit{lf}},q_{\mathsf{fin}}\\},\\{q_{\mathsf{fin}}\\},\Delta)$,
where $\Delta$ contains transitions

$\displaystyle(q_{\mathsf{fin}},a),(q_{\mathsf{fin}},a,q_{\mathsf{fin}}),(q_{\mathsf{fin}},a,q_{\mathsf{fin}},q_{\mathsf{fin}}),(q_{\exists\mathit{lf}},a),$
and
$\displaystyle(q_{\exists\mathit{lf}},a,q),(q_{\exists\mathit{lf}},a,q,\top),(q_{\exists\mathit{lf}},a,\top,q)$
$\displaystyle\mbox{for }q\in\\{q_{\exists\mathit{lf}},q_{\mathsf{fin}}\\}\,.$

Suppose now that a $(\\{a\\},2)$-tree $T$ comes. When a state
$q_{\mathsf{fin}}$ is assigned to some node $u$ of $T$, then it has to be
assigned as well to all descendants of $u$. Thus, there is a run of
${\mathcal{A}}_{1}$ on $T$ with state $q_{\mathsf{fin}}$ in the root exactly
when the tree is finite. This is because the definition of a run allows to
assign states (other than $\top$) only to finitely many nodes of the tree.
Going further, there is a run of ${\mathcal{A}}$ on $T$ with state
$q_{\exists\mathit{lf}}$ in the root exactly when there is a leaf in the tree.
The run can assign $q_{\exists\mathit{lf}}$ to all nodes on the branch leading
to a selected leaf, and $\top$ to all other nodes. Alternatively, it can
assign $q_{\exists\mathit{lf}}$ to nodes on a branch leading to some node $u$,
and then $q_{\mathsf{fin}}$ to all descendants of $u$, assuming that the
subtree starting in $u$ is finite.

Let $B_{i}$ be the full binary tree of height $i$, for $i\in\mathbb{N}$. Let
$T_{1}$ be the tree consisting of an infinite branch, with tree $B_{i}$
attached below the $i$-th child of the branch; that is, we take
$T_{i}=a\langle T_{i+1},B_{i}\rangle$ for $i\in\mathbb{N}_{+}$. By definition,
${\mathcal{A}}_{1}(T_{1})$ has the same shape as $T_{1}$. Nodes inside all
$B_{i}$ become relabeled to $(a,[q_{\exists\mathit{lf}}\mapsto
1,q_{\mathsf{fin}}\mapsto 1])$. This is because every subtree of every $B_{i}$
is finite and has a leaf. Moreover, the number of nodes of this subtree to
which $q_{\mathsf{fin}}$ is assigned is bounded by the size of the subtree
(and hence we do not use the value $2$ in the new label). Nodes of the
leftmost branch of $T_{1}$ are, in turn, relabeled to
$(a,[q_{\exists\mathit{lf}}\mapsto 2,q_{\mathsf{fin}}\mapsto 0])$. The value
$2$ in the $i$-th node of the branch means that for every $n\in\mathbb{N}$
there is a run $\rho_{n}$ on $T_{i}$ that assigns $q_{\exists\mathit{lf}}$ to
the root of $T_{i}$, and assigns $q_{\mathsf{fin}}$ to at least $n$ nodes.
Such a run $\rho_{n}$ assigns $q_{\exists\mathit{lf}}$ on a branch entering
some $B_{j}$ with at least $n$ nodes, and assigns $q_{\mathsf{fin}}$ to all
nodes of this $B_{j}$.

An _MSO automaton_ is a triple ${\mathcal{A}}=(\Sigma,Q,(\varphi_{q})_{q\in
Q})$, where $\Sigma$ is a finite alphabet, $Q$ is a finite set of states, and
$(\varphi_{q})_{q\in Q}$ is a bundle of MSO sentences indexed by elements of
$Q$. An effect of running such an automaton ${\mathcal{A}}$ on a
$\Sigma$-labeled tree $T$ is the tree ${\mathcal{A}}(T)$ that is of the same
shape as $T$, and such that its every node $u$ originally labeled by $a_{u}$
becomes labeled by the pair $(a_{u},f_{u})$, where $f_{u}\colon
Q\to\\{0,1,2\\}$ is the function that assigns to every index $q\in Q$

  * •

$1$ if $\varphi_{q}$ is true in $T{\restriction}_{u}$;

  * •

$0$ otherwise.111MSO automata never assign the value $2$; nevertheless, for
uniformity between $\mathsf{U}$-prefix automata and MSO automata, we assume
that the set of values is $\\{0,1,2\\}$.

######  Example 6.

Let
${\mathcal{A}}_{2}=(\\{a\\}\times\\{0,1,2\\}^{\\{q_{\exists\mathit{lf}},q_{\mathsf{fin}}\\}},\\{q_{1},q_{2}\\},(\varphi_{q_{1}},\varphi_{q_{2}}))$,
where $\varphi_{q_{1}}$ says that the second child of the root exists and is
labeled by $(a,[q_{\exists\mathit{lf}}\mapsto 1,q_{\mathsf{fin}}\mapsto 1])$,
and $\varphi_{q_{2}}$ says that there exists an infinite branch with all nodes
labeled by $(a,[q_{\exists\mathit{lf}}\mapsto 2,q_{\mathsf{fin}}\mapsto 0])$.
Let us analyze ${\mathcal{A}}_{2}({\mathcal{A}}_{1}(T_{1}))$, for the tree
$T_{1}$ from Example 5. It has the same shape as ${\mathcal{A}}_{1}(T_{1})$,
and as $T_{1}$. All leaves become labeled by
$((a,[q_{\exists\mathit{lf}}\mapsto 1,q_{\mathsf{fin}}\mapsto
1]),[q_{1}\mapsto 0,q_{2}\mapsto 0])$, other nodes of $B_{i}$ become labeled
by $((a,[q_{\exists\mathit{lf}}\mapsto 1,q_{\mathsf{fin}}\mapsto
1]),[q_{1}\mapsto 1,q_{2}\mapsto 0])$, and nodes on the leftmost branch of the
tree become labeled by $((a,[q_{\exists\mathit{lf}}\mapsto
2,q_{\mathsf{fin}}\mapsto 0]),[q_{1}\mapsto 1,q_{2}\mapsto 1])$.

By the _input alphabet_ of ${\mathcal{A}}$, where ${\mathcal{A}}$ is either a
$\mathsf{U}$-prefix automaton $(\Sigma,Q,Q_{\mathsf{imp}},\Delta)$ or an MSO
automaton $(\Sigma,Q,(\varphi_{q})_{q\in Q})$, we mean the set
$\Sigma^{\mathsf{in}}({\mathcal{A}})=\Sigma$. The _output alphabet_ of
${\mathcal{A}}$ is
$\Sigma^{\mathsf{out}}({\mathcal{A}})=\Sigma^{\mathsf{in}}({\mathcal{A}})\times\\{0,1,2\\}^{Q}$.

A _nested $\mathsf{U}$-prefix MSO automaton_ is a sequence
${\mathcal{A}}={\mathcal{A}}_{1}\vartriangleright\dots\vartriangleright{\mathcal{A}}_{k}$
(with $k\geq 1$), where every ${\mathcal{A}}_{i}$ is either a
$\mathsf{U}$-prefix automaton or an MSO automaton, and where
$\Sigma^{\mathsf{in}}({\mathcal{A}}_{i+1})=\Sigma^{\mathsf{out}}({\mathcal{A}}_{i})$
for $i\in\\{1,\dots,k-1\\}$. We define ${\mathcal{A}}(T)$ to be
${\mathcal{A}}_{k}(\dots({\mathcal{A}}_{1}(T))\dots)$. The input and output
alphabets of ${\mathcal{A}}$, denoted $\Sigma^{\mathsf{in}}({\mathcal{A}})$
and $\Sigma^{\mathsf{out}}({\mathcal{A}})$, equal
$\Sigma^{\mathsf{in}}({\mathcal{A}}_{1})$ and
$\Sigma^{\mathsf{out}}({\mathcal{A}}_{k})$, respectively. The key property is
that these automata can check properties expressed in MSO+$\mathsf{U^{fin}}$,
as we state in Lemma 7, and we prove in the remainder of this section.

######  Lemma 7.

Let $\Sigma$ be a finite alphabet, and let $r_{\max}\in\mathbb{N}$. For every
MSO+$\mathsf{U^{fin}}$ sentence $\varphi$ we can construct a nested
$\mathsf{U}$-prefix MSO automaton ${\mathcal{A}}_{\varphi}$ with
$\Sigma^{\mathsf{in}}({\mathcal{A}}_{\varphi})=\Sigma$, and a subset
$\Sigma_{\mathsf{F}}\subseteq\Sigma^{\mathsf{out}}({\mathcal{A}}_{\varphi})$
such that for every $(\Sigma,r_{\max})$-tree $T$, the root of
${\mathcal{A}}_{\varphi}(T)$ is labeled by a letter in $\Sigma_{\mathsf{F}}$
if and only if $\varphi$ holds in $T$.

Recall that our aim is to evaluate $\varphi$ in a tree $T$ generated by a
recursion scheme ${\mathcal{G}}$, so the restriction to
$(\Sigma,r_{\max})$-trees is not harmful: as $(\Sigma,r_{\max})$ we are going
to take $(\Sigma_{\mathcal{G}},r_{\max}({\mathcal{G}}))$.

It is not difficult to see that in MSO+$\mathsf{U^{fin}}$ we can express
properties checked by nested $\mathsf{U}$-prefix MSO automata. This means that
the two formalisms are actually equivalent. Although we do not need this
second direction in order to prove Theorem 1, we state it in Lemma 8 for
cognitive purposes.

######  Lemma 8.

Let $r_{\max}\in\mathbb{N}$. For every nested $\mathsf{U}$-prefix MSO
automaton ${\mathcal{A}}$, and every letter
$\eta\in\Sigma^{\mathsf{out}}({\mathcal{A}})$ we can construct an
MSO+$\mathsf{U^{fin}}$ sentence $\varphi_{{\mathcal{A}},\eta}$ such that for
every $(\Sigma^{\mathsf{in}}({\mathcal{A}}),r_{\max})$-tree $T$, the root of
${\mathcal{A}}(T)$ is labeled by $\eta$ if and only if
$\varphi_{{\mathcal{A}},\eta}$ holds in $T$.

######  Proof 3.1 (Proof sketch).

When ${\mathcal{A}}$ is a single MSO automaton,
${\mathcal{A}}=(\Sigma,Q,(\psi_{q})_{q\in Q})$, it is straightforward to
construct $\varphi_{{\mathcal{A}},\eta}$ in question. Namely, when
$\eta=(a,f)$, as $\varphi_{{\mathcal{A}},\eta}$ we take

$\displaystyle\xi_{a}\land\bigwedge_{q:f(q)=1}\psi_{q}\land\bigwedge_{q:f(q)=0}\neg\psi_{q}\,,$

where $\xi_{a}$ says that the root is labeled by $a$.

It is also not difficult to deal with a single $\mathsf{U}$-prefix automaton.
Indeed, it is standard to express in MSO that a run of an automaton exists.
The fact that there exist runs with arbitrarily many important states is
expressed using the $\mathsf{U}$ quantifier.

It remains to simulate composition of automata. Suppose that
${\mathcal{A}}={\mathcal{A}}_{1}\vartriangleright{\mathcal{A}}_{2}$ (where
${\mathcal{A}}_{1},{\mathcal{A}}_{2}$ may be nested again), and that we
already have sentences $\psi_{{\mathcal{A}}_{1},a}$ corresponding to
${\mathcal{A}}_{1}$ for
$a\in\Sigma^{\mathsf{out}}({\mathcal{A}}_{1})=\Sigma^{\mathsf{in}}({\mathcal{A}}_{2})$,
and $\psi_{{\mathcal{A}}_{2},\eta}$ corresponding to ${\mathcal{A}}_{2}$. Out
of every sentence $\psi_{{\mathcal{A}}_{1},a}$ we construct a formula
$\widehat{\psi}_{{\mathcal{A}}_{1},a}(\mathsf{Z})$ saying that
$\psi_{{\mathcal{A}}_{1},a}$ holds in all subtrees starting in elements of the
set represented by $\mathsf{Z}$ (cf. Fact 4). The formula
$\psi_{{\mathcal{A}}_{2},\eta}$ is evaluated in ${\mathcal{A}}_{1}(T)$, while
the formula $\varphi_{{\mathcal{A}},\eta}$ that we are going to construct is
evaluated in $T$. Thus, whenever $\psi_{{\mathcal{A}}_{2},\eta}$ uses
$a(\mathsf{Z})$ for some letter $a\in\Sigma^{\mathsf{in}}({\mathcal{A}}_{2})$
and some variable $\mathsf{Z}$, in $\varphi_{{\mathcal{A}},\eta}$ we replace
it by $\widehat{\psi}_{{\mathcal{A}}_{1},a}(\mathsf{Z})$.

We now come to the proof of Lemma 7. We notice that due to the nested
structure, our automata are quite close to the logic. It is clear that MSO
automata can simulate all of MSO. On the other hand, $\mathsf{U}$-prefix
automata check whether something is unbounded, which corresponds to
$\mathsf{U}$ quantifiers. As states of the $\mathsf{U}$-prefix automata we
take _phenotypes_ (aka. logical types), which are defined next.

Let $\varphi$ be a formula of MSO+$\mathsf{U^{fin}}$, let $T$ be a tree, and
let $\nu$ be a valuation (defined at least for all free variables of
$\varphi$). We define the _$\varphi$ -phenotype_ of $T$ under valuation $\nu$,
denoted $[T]_{\varphi}^{\nu}$, by induction on the size of $\varphi$ as
follows:

  * •

if $\varphi$ is of the form $a(\mathsf{X})$ (for some letter $a$) or
$\mathsf{X}\subseteq\mathsf{Y}$ then $[T]_{\varphi}^{\nu}$ is the logical
value of $\varphi$ in $T,\nu$, that is, $\mathsf{tt}$ if $T,\nu\models\varphi$
and $\mathsf{ff}$ otherwise,

  * •

if $\varphi$ is of the form $\mathsf{X}\curlywedgedownarrow_{i}\mathsf{Y}$,
then $[T]_{\varphi}^{\nu}$ equals

    * –

$\mathsf{tt}$ if $T,\nu\models\varphi$,

    * –

$\mathsf{empty}$ if $\nu(\mathsf{X})=\nu(\mathsf{Y})=\emptyset$,

    * –

$\mathsf{root}$ if $\nu(\mathsf{X})=\emptyset$ and
$\nu(\mathsf{Y})=\\{\varepsilon\\}$, and

    * –

$\mathsf{ff}$ otherwise,

  * •

if $\varphi\equiv(\psi_{1}\land\psi_{2})$, then
$[T]_{\varphi}^{\nu}=([T]_{\psi_{1}}^{\nu},[T]_{\psi_{2}}^{\nu})$,

  * •

if $\varphi\equiv(\neg\psi)$, then $[T]_{\varphi}^{\nu}=[T]_{\psi}^{\nu}$,

  * •

if $\varphi\equiv\exists\mathsf{X}.\psi$, then

$\displaystyle[T]_{\varphi}^{\nu}=\\{\sigma\mid\exists
X.[T]_{\psi}^{\nu[\mathsf{X}\mapsto X]}=\sigma\\}\,,$

  * •

if $\varphi\equiv{\exists_{\mathsf{fin}}}\mathsf{X}.\psi$, then

$\displaystyle[T]_{\varphi}^{\nu}=\\{\sigma\mid\exists
X.[T]_{\psi}^{\nu[\mathsf{X}\mapsto X]}=\sigma\land|X|<\infty\\}\,,$ and

  * •

if $\varphi\equiv\mathsf{U}\mathsf{X}.\psi$, then

$\displaystyle[T]_{\varphi}^{\nu}=($ $\displaystyle\\{\sigma\mid\exists
X.[T]_{\psi}^{\nu[\mathsf{X}\mapsto X]}=\sigma\land|X|<\infty\\},$
$\displaystyle\\{\sigma\mid\forall n\in\mathbb{N}.\exists
X.[T]_{\psi}^{\nu[\mathsf{X}\mapsto X]}=\sigma\land n\leq|X|<\infty\\})\,,$

where $X$ ranges over sets of nodes of $T$.

For each $\varphi$, let $\mathit{Pht}_{\varphi}$ denote the set of all
potential $\varphi$-phenotypes. Namely,
$\mathit{Pht}_{\varphi}=\\{\mathsf{tt},\mathsf{ff}\\}$ in the first case,
$\mathit{Pht}_{\varphi}=\\{\mathsf{tt},\mathsf{empty},\mathsf{root},\mathsf{ff}\\}$
in the second case,
$\mathit{Pht}_{\varphi}=\mathit{Pht}_{\psi_{1}}\times\mathit{Pht}_{\psi_{2}}$
in the third case, $\mathit{Pht}_{\varphi}=\mathit{Pht}_{\psi}$ in the fourth
case, $\mathit{Pht}_{\varphi}={\mathcal{P}}(\mathit{Pht}_{\psi})$ in the fifth
and sixth case, and
$\mathit{Pht}_{\varphi}=({\mathcal{P}}(\mathit{Pht}_{\psi}))^{2}$ in the last
case.

We immediately see two facts. First, $\mathit{Pht}_{\varphi}$ is finite for
every $\varphi$. Second, the fact whether $\varphi$ holds in $T,\nu$ is
determined by $[T]_{\varphi}^{\nu}$. This means that there is a function
$\mathit{tv}_{\varphi}\colon\mathit{Pht}_{\varphi}\to\\{\mathsf{tt},\mathsf{ff}\\}$
such that $\mathit{tv}_{\varphi}([T]_{\varphi}^{\nu})=\mathsf{tt}$ if and only
if $T,\nu\models\varphi$.

Next, we observe that phenotypes behave in a compositional way, as formalized
below. Here for a valuation $\nu$ and a node $u$, by $\nu{\restriction}_{u}$
we mean the valuation that restricts $\nu$ to the subtree starting at $u$,
that is, maps every variable $\mathsf{X}\in\mathrm{dom}(\nu)$ to $\\{w\mid
uw\in\nu(\mathsf{X})\\}$.

[[GK10, PT16]] For every letter $a$, every $r\in\mathbb{N}$, and every
MSO+$\mathsf{U^{fin}}$ formula $\varphi$, one can compute a function
$\mathit{Comp}_{a,r,\varphi}\colon{\mathcal{P}}^{\mathsf{fin}}({\mathcal{V}})\times(\mathit{Pht}_{\varphi})^{r}\to\mathit{Pht}_{\varphi}$
such that for every tree $T$ whose root has label $a$ and $r$ children, and
for every valuation $\nu$,

$\displaystyle[T]_{\varphi}^{\nu}=\mathit{Comp}_{a,r,\varphi}(\\{\mathsf{X}\in\mathrm{dom}(\nu)\mid\varepsilon\in\nu(\mathsf{X})\\},[T{\restriction}_{1}]_{\varphi}^{\nu{\restriction}_{1}},\dots,[T{\restriction}_{r}]_{\varphi}^{\nu{\restriction}_{r}})\,.$

######  Proof 3.2.

We proceed by induction on the size of $\varphi$.

When $\varphi$ is of the form $b(\mathsf{X})$ or
$\mathsf{X}\subseteq\mathsf{Y}$, then we see that $\varphi$ holds in $T,\nu$
if and only if it holds in every subtree
$T{\restriction}_{i},\nu{\restriction}_{i}$ and in the root of $T$. Thus, for
$\varphi\equiv b(\mathsf{X})$ as
$\mathit{Comp}_{a,r,\varphi}(R,\tau_{1},\dots,\tau_{r})$ we take $\mathsf{tt}$
when $\tau_{i}=\mathsf{tt}$ for all $i\in\\{1,\dots,r\\}$ and either $a=b$ or
$\mathsf{X}\not\in R$. For $\varphi\equiv(\mathsf{X}\subseteq\mathsf{Y})$ the
last part of the condition is replaced by “if $\mathsf{X}\in R$ then
$\mathsf{Y}\in R$”.

Next, suppose that
$\varphi\equiv(\mathsf{X}\curlywedgedownarrow_{k}\mathsf{Y})$. Then as
$\mathit{Comp}_{a,r,\varphi}(R,\tau_{1},\dots,\tau_{r})$ we take

  * •

$\mathsf{tt}$ if $\tau_{j}=\mathsf{tt}$ for some $j\in\\{1,\dots,r\\}$, and
$\tau_{i}=\mathsf{empty}$ for all $i\in\\{1,\dots,r\\}\setminus\\{j\\}$, and
$\mathsf{X}\not\in R$, and $\mathsf{Y}\not\in R$,

  * •

$\mathsf{tt}$ also if $\tau_{k}=\mathsf{root}$, and $\tau_{i}=\mathsf{empty}$
for all $i\in\\{1,\dots,r\\}\setminus\\{k\\}$, and $\mathsf{X}\in R$, and
$\mathsf{Y}\not\in R$,

  * •

$\mathsf{empty}$ if $\tau_{i}=\mathsf{empty}$ for all $i\in\\{1,\dots,r\\}$,
and $\mathsf{X}\not\in R$, and $\mathsf{Y}\not\in R$,

  * •

$\mathsf{root}$ if $\tau_{i}=\mathsf{empty}$ for all $i\in\\{1,\dots,r\\}$,
and $\mathsf{X}\not\in R$, and $\mathsf{Y}\in R$, and

  * •

$\mathsf{ff}$ otherwise.

By comparing this definition with the definition of the phenotype we
immediately see that the thesis is satisfied.

When $\varphi\equiv(\neg\psi)$, we simply take
$\mathit{Comp}_{a,r,\varphi}=\mathit{Comp}_{a,r,\psi}$, and when
$\varphi\equiv(\psi_{1}\land\psi_{2})$, as
$\mathit{Comp}_{a,r,\varphi}(R,(\tau_{1}^{1},\tau_{1}^{2}),\dots,(\tau^{1}_{r},\tau^{2}_{r}))$
we take the pair of
$\mathit{Comp}_{a,r,\psi_{i}}(R,\tau_{1}^{i},\dots,\tau^{i}_{r})$ for
$i\in\\{1,2\\}$.

Suppose now that $\varphi\equiv\exists\mathsf{X}.\psi$ or
$\varphi\equiv{\exists_{\mathsf{fin}}}\mathsf{X}.\psi$. As
$\mathit{Comp}_{a,r,\varphi}(R,\tau_{1},\dots,\tau_{r})$ we take

$\displaystyle\\{\mathit{Comp}_{a,r,\psi}(R\cup\\{\mathsf{X}\\},\sigma_{1},\dots,\sigma_{r}),\mathit{Comp}_{a,r,\psi}(R\setminus\\{\mathsf{X}\\},\sigma_{1},\dots,\sigma_{r})$
$\displaystyle\hskip
200.0003pt\mid(\sigma_{1},\dots,\sigma_{r})\in\tau_{1}\times\dots\times\tau_{r}\\}\,.$

The two possibilities, $R\cup\\{\mathsf{X}\\}$ and
$R\setminus\\{\mathsf{X}\\}$, correspond to the fact that when quantifying
over $\mathsf{X}$, the root of $T$ may be either taken to the set represented
by $\mathsf{X}$ or not. Notice that the cases of $\exists\mathsf{X}$ and
${\exists_{\mathsf{fin}}}\mathsf{X}$ are handled in the same way: for a local
behavior near the root it does not matter whether we quantify over all sets or
only over finite sets.

Finally, suppose that $\varphi\equiv\mathsf{U}\mathsf{X}.\psi$. The arguments
of $\mathit{Comp}_{a,r,\varphi}$ are pairs
$(\tau_{1},\rho_{1}),\dots,\allowbreak(\tau_{r},\rho_{r})$. Let $A$ be the set
of tuples $(\sigma_{1},\dots,\sigma_{r})\in\tau_{1}\times\dots\times\tau_{r}$,
and let $B$ be the set of tuples $(\sigma_{1},\dots,\sigma_{r})$ such that
$\sigma_{j}\in\rho_{j}$ for some $j\in\\{1,\dots,r\\}$ and
$\sigma_{i}\in\tau_{i}$ for all $i\in\\{1,\dots,r\\}\setminus\\{j\\}$. As
$\mathit{Comp}_{a,r,\varphi}(R,(\tau_{1},\rho_{1}),\dots,(\tau_{r},\rho_{r}))$
we take

$\displaystyle($
$\displaystyle\\{\mathit{Comp}_{a,r,\psi}(R\cup\\{\mathsf{X}\\},\sigma_{1},\dots,\sigma_{r}),\mathit{Comp}_{a,r,\psi}(R\setminus\\{\mathsf{X}\\},\sigma_{1},\dots,\sigma_{r})\mid(\sigma_{1},\dots,\sigma_{r})\in
A\\},$
$\displaystyle\\{\mathit{Comp}_{a,r,\psi}(R\cup\\{\mathsf{X}\\},\sigma_{1},\dots,\sigma_{r}),\mathit{Comp}_{a,r,\psi}(R\setminus\\{\mathsf{X}\\},\sigma_{1},\dots,\sigma_{r})\mid(\sigma_{1},\dots,\sigma_{r})\in
B\\})\,.$

The first coordinate is defined as for the existential quantifiers. The second
coordinate is computed correctly due to the pigeonhole principle: if for every
$n$ we have a set $X_{n}$ of cardinality at least $n$ (satisfying some
property), then we can choose an infinite subsequence of these sets such that
either the root belongs to all of them or to none of them, and one can choose
some $j\in\\{1,\dots,r\\}$ such that the sets contain unboundedly many
descendants of $j$.

In order to prove Lemma 7 by induction on the structure of the sentence
$\varphi$, we need to generalize it a bit; this is done in Lemma 9. In
particular, we need to use phenotypes, instead of the truth value of the
sentence (because phenotypes are compositional, unlike truth values). We also
need to allow formulae with free variables, not just sentences, as well as
arbitrary valuations. A special role is played by the valuation
$\nu_{\emptyset}$ that maps every variable to the empty set; for this
valuation we have a stronger version of the lemma.

######  Lemma 9.

Let $\Sigma$ be a finite alphabet, and let $r_{\max}\in\mathbb{N}$. Then for
every MSO+$\mathsf{U^{fin}}$ formula $\varphi$ we can construct

  1. (1)

a nested $\mathsf{U}$-prefix MSO automaton ${\mathcal{A}}_{\varphi}$ with
$\Sigma^{\mathsf{in}}({\mathcal{A}}_{\varphi})=\Sigma$, and MSO formulae
$\xi_{\varphi,\tau}$ for all $\tau\in\mathit{Pht}_{\varphi}$, such that for
every $(\Sigma,r_{\max})$-tree $T$, every valuation $\nu$ in $T$, and every
$\tau\in\mathit{Pht}_{\varphi}$ it holds
${\mathcal{A}}_{\varphi}(T),\nu\models\xi_{\varphi,\tau}$ if and only if
$[T]_{\varphi}^{\nu}=\tau$, and

  2. (2)

a nested $\mathsf{U}$-prefix MSO automaton ${\mathcal{B}}_{\varphi}$ with
$\Sigma^{\mathsf{in}}({\mathcal{B}}_{\varphi})=\Sigma$, and a function
$f_{\varphi}\colon\allowbreak\Sigma^{\mathsf{out}}({\mathcal{B}}_{\varphi})\to\mathit{Pht}_{\varphi}$,
such that for every $(\Sigma,r_{\max})$-tree $T$ the root of
${\mathcal{B}}_{\varphi}(T)$ is labeled by a letter $\eta$ such that
$f_{\varphi}(\eta)=[T]_{\varphi}^{\nu_{\emptyset}}$.

######  Proof 3.3.

Induction on the size of $\varphi$. We start by observing how Item (2) follows
from Item (1). Item (1) gives us an automaton ${\mathcal{A}}_{\varphi}$ and
MSO formulae $\xi_{\varphi,\tau}$ for all $\tau\in\mathit{Pht}_{\varphi}$. We
change these formulae into sequences $\xi_{\varphi,\tau}^{\prime}$, assuming
that all their free variables are valuated to the empty set. More precisely,
for every free variable $\mathsf{X}$ we change subformulae of
$\xi_{\varphi,\tau}$ of the form $a(\mathsf{X})$ and
$\mathsf{X}\subseteq\mathsf{Y}$ into $\mathsf{tt}$, subformulae of the form
$\mathsf{X}\curlywedgedownarrow_{i}\mathsf{Y}$ and
$\mathsf{Y}\curlywedgedownarrow_{i}\mathsf{X}$ into $\mathsf{ff}$, and
subformulae of the form $\mathsf{Y}\subseteq\mathsf{X}$, where $\mathsf{Y}$ is
a bound variable, into formulae checking that the set represented by
$\mathsf{Y}$ is empty. Then, we take
${\mathcal{B}}_{\varphi}={\mathcal{A}}_{\varphi}\vartriangleright{\mathcal{C}}$
for
${\mathcal{C}}=(\Sigma^{\mathsf{out}}({\mathcal{A}}_{\varphi}),\mathit{Pht}_{\varphi},(\xi_{\varphi,\tau}^{\prime})_{\tau\in\mathit{Pht}_{\varphi}})$.
If $\eta=(a,h)$ for a function $h$ mapping exactly one phenotype $\tau$ to
$1$, we define $f_{\varphi}(\eta)$ to be this phenotype $\tau$, and for
$\eta=(a,h)$ with $|h^{-1}(1)|\neq 1$ we define $f_{\varphi}(\eta)$
arbitrarily.

Consider now a $(\Sigma,r_{\max})$-tree $T$. By Item (1), for
$\tau=[T]_{\varphi}^{\nu_{\emptyset}}$ we have
${\mathcal{A}}_{\varphi}(T),\nu_{\emptyset}\models\xi_{\varphi,\tau}$
(equivalently, ${\mathcal{A}}_{\varphi}(T)\models\xi_{\varphi,\tau}^{\prime}$)
and for
$\tau\in\mathit{Pht}_{\varphi}\setminus\\{[T]_{\varphi}^{\nu_{\emptyset}}\\}$
we have
${\mathcal{A}}_{\varphi}(T),\nu_{\emptyset}\not\models\xi_{\varphi,\tau}$
(equivalently,
${\mathcal{A}}_{\varphi}(T)\not\models\xi_{\varphi,\tau}^{\prime}$). It
follows that the root of ${\mathcal{B}}_{\varphi}(T)$ is labeled by
$\eta=(a,h)$ where $a$ is the label of the root in
${\mathcal{A}}_{\varphi}(T)$, and $h([T]_{\varphi}^{\nu_{\emptyset}})=1$, and
$h(\tau)=0$ for
$\tau\in\mathit{Pht}_{\varphi}\setminus\\{[T]_{\varphi}^{\nu_{\emptyset}}\\}$.
Then $f_{\varphi}(\eta)=[T]_{\varphi}^{\nu_{\emptyset}}$, as required.

We now come to the proof of Item (1), where we proceed by case distinction.
When $\varphi$ is an atomic formula, that is, equals $a(\mathsf{X})$,
$\mathsf{X}\subseteq\mathsf{Y}$, or
$\mathsf{X}\curlywedgedownarrow_{i}\mathsf{Y}$, then the automaton
${\mathcal{A}}_{\varphi}$ is not needed: as ${\mathcal{A}}_{\varphi}$ we can
take the MSO automaton with empty set of states (and input alphabet $\Sigma$).
For such an automaton we have that ${\mathcal{A}}_{\varphi}(T)=T$ for every
$(\Sigma,r_{\max})$-tree $T$. As $\xi_{\varphi,\mathsf{tt}}$ we take
$\varphi$. When $\varphi$ equals $a(\mathsf{X})$ or
$\mathsf{X}\subseteq\mathsf{Y}$, the only phenotypes are $\mathsf{tt}$ and
$\mathsf{ff}$, and thus we take $\xi_{\varphi,\mathsf{ff}}\equiv\neg\varphi$.
In the case of $\varphi\equiv\mathsf{X}\curlywedgedownarrow_{i}\mathsf{Y}$,
the situation when the formula is false is divided into three phenotypes:
$\mathsf{empty}$, $\mathsf{root}$, and $\mathsf{ff}$. Nevertheless, it is easy
to express in MSO that we have a particular phenotype, following the
definition of $[T]_{\varphi}^{\nu}$.

Suppose now that $\varphi$ is of the form $\psi_{1}\land\psi_{2}$. From the
induction assumption, Item (1), we have two automata,
${\mathcal{A}}_{\psi_{1}}$ and ${\mathcal{A}}_{\psi_{2}}$, as well as formulae
$\xi_{\psi_{1},\tau_{1}}$ for all $\tau_{1}\in\mathit{Pht}_{\psi_{1}}$ and
$\xi_{\psi_{2},\tau_{2}}$ for all $\tau_{2}\in\mathit{Pht}_{\psi_{2}}$. We
combine the two automata into a single automaton ${\mathcal{A}}_{\varphi}$
with $\Sigma^{\mathsf{in}}({\mathcal{A}}_{\varphi})=\Sigma$. More precisely,
we take
${\mathcal{A}}_{\varphi}={\mathcal{A}}_{\psi_{1}}\vartriangleright{\mathcal{A}}_{\psi_{2}}^{\prime}$,
where ${\mathcal{A}}_{\psi_{2}}^{\prime}$ works exactly like
${\mathcal{A}}_{\psi_{2}}$, but instead of reading a tree $T$ over alphabet
$\Sigma$, it reads the tree ${\mathcal{A}}_{\psi_{1}}(T)$ and ignores the part
of its labels added by ${\mathcal{A}}_{\psi_{1}}$. We also amend
$\xi_{\psi_{1},\tau_{1}}$ and $\xi_{\psi_{2},\tau_{2}}$ so that they can read
the output of ${\mathcal{A}}_{\varphi}$: formulae
$\xi_{\psi_{1},\tau_{1}}^{\prime}$ work like $\xi_{\psi_{1},\tau_{1}}$ but
ignore the parts of labels added by ${\mathcal{A}}_{\psi_{2}}^{\prime}$, and
formulae $\xi_{\psi_{2},\tau_{2}}^{\prime}$ work like
$\xi_{\psi_{2},\tau_{2}}$ but ignore the parts of labels added by
${\mathcal{A}}_{\psi_{1}}$. Having the above, for every
$\tau=(\tau_{1},\tau_{2})\in\mathit{Pht}_{\varphi}$ we take
$\xi_{\varphi,\tau}\equiv\xi_{\psi_{1},\tau_{1}}^{\prime}\land\xi_{\psi_{2},\tau_{2}}^{\prime}$.
Because a tree has $\varphi$-phenotype $\tau$ when it has $\psi_{1}$-phenotype
$\tau_{1}$ and simultaneously $\psi_{2}$-phenotype $\tau_{2}$, it should be
clear that the thesis of Item (1) becomes satisfied.

When $\varphi$ is of the form $\neg\psi$, or $\exists\mathsf{X}.\psi$, or
${\exists_{\mathsf{fin}}}\mathsf{X}.\psi$, as ${\mathcal{A}}_{\varphi}$ we
take ${\mathcal{A}}_{\psi}$ existing by the induction assumption, Item (1).
The induction assumption gives us also formulae $\xi_{\psi,\tau}$ for all
$\tau\in\mathit{Pht}_{\psi}$. If $\varphi\equiv\neg\psi$, we take
$\xi_{\varphi,\tau}\equiv\xi_{\psi,\tau}$. If
$\varphi\equiv\exists\mathsf{X}.\psi$, we take

$\displaystyle\xi_{\varphi,\tau}\equiv\bigwedge_{\sigma\in\tau}(\exists\mathsf{X}.\xi_{\psi,\sigma})\land\bigwedge_{\sigma\in\mathit{Pht}_{\psi}\setminus\tau}(\neg\exists\mathsf{X}.\xi_{\psi,\sigma})\,.$

If $\varphi\equiv{\exists_{\mathsf{fin}}}\mathsf{X}.\psi$, we take the same
formula, but with ${\exists_{\mathsf{fin}}}$ quantifiers instead of $\exists$.

Finally, suppose that $\varphi\equiv\mathsf{U}\mathsf{X}.\psi$. We cannot
proceed like in the previous cases, because the $\mathsf{U}$ quantifier cannot
be expressed in MSO; we rather need to append a new $\mathsf{U}$-prefix
automaton at the end of the constructed automaton. In this case we first prove
Item (2), and then we deduce Item (1) out of Item (2). By Item (2) of the
induction assumption we have an automaton ${\mathcal{B}}_{\psi}$ and a
function
$f_{\psi}\colon\Sigma^{\mathsf{out}}({\mathcal{B}}_{\psi})\to\mathit{Pht}_{\psi}$
such that for every node $u$ of $T$, the root of
${\mathcal{B}}_{\psi}(T{\restriction}_{u})$ is labeled by a letter $\eta_{u}$
such that $f_{\psi}(\eta_{u})=[T{\restriction}_{u}]_{\psi}^{\nu_{\emptyset}}$.
Moreover, there is a function
$g\colon\Sigma^{\mathsf{out}}({\mathcal{B}}_{\psi})\to\Sigma$ such that
$g(\eta_{u})$ is the original label of $u$ in $T$ (such a function exists,
because the labels from $T$ remain as a part of the labels in
${\mathcal{B}}_{\psi}(T)$). Recall that ${\mathcal{B}}_{\psi}(T)$ has the same
shape as $T$, and actually
$({\mathcal{B}}_{\psi}(T)){\restriction}_{u}={\mathcal{B}}_{\psi}(T{\restriction}_{u})$
for every node $u$. We construct a new layer ${\mathcal{C}}$, which calculates
$\varphi$-phenotypes basing on $\psi$-phenotypes, and we take
${\mathcal{B}}_{\varphi}={\mathcal{B}}_{\psi}\vartriangleright{\mathcal{C}}$.
As the state set of ${\mathcal{C}}$ we take
$Q=\\{0,1\\}\times\mathit{Pht}_{\psi}$; states from
$\\{1\\}\times\mathit{Pht}_{\psi}$ are considered as important. Transitions
are determined by the $\mathit{Comp}$ predicate from Lemma 3.1. More
precisely, for every $r\leq r_{\max}$, every
$\eta\in\Sigma^{\mathsf{out}}({\mathcal{B}}_{\psi})$, and all
$((i_{1},\sigma_{1}),\dots,(i_{r},\sigma_{r}))\in Q^{r}$ we have transitions

$\displaystyle((0,\mathit{Comp}_{g(\eta),r,\psi}(\emptyset,\sigma_{1},\dots,\sigma_{r})),\eta,(i_{1},\sigma_{1}),\dots,(i_{r},\sigma_{r}))\,,$
and
$\displaystyle((1,\mathit{Comp}_{g(\eta),r,\psi}(\\{\mathsf{X}\\},\sigma_{1},\dots,\sigma_{r})),\eta,(i_{1},\sigma_{1}),\dots,(i_{r},\sigma_{r}))\,.$

Moreover, we have transitions that read the $\psi$-phenotype from the label:

$\displaystyle((0,f_{\psi}(\eta)),\eta,\underbrace{\top,\dots,\top}_{r})$
$\displaystyle\mbox{for }r\leq r_{\max}.$

We notice that there is a direct correspondence between runs of
${\mathcal{C}}$ and choices of a set of nodes $X$ to which the variable
$\mathsf{X}$ is mapped. The first coordinate of the state is set to $1$ in
nodes chosen to belong to the set $X$. The second coordinate contains the
$\psi$-phenotype under the valuation mapping $\mathsf{X}$ to $X$ and every
other variable to the empty set. In some nodes below the chosen set $X$ we use
transitions of the second kind, reading the $\psi$-phenotype from the label;
it does not matter in which nodes this is done, as everywhere a correct
$\psi$-phenotype is written. The fact that we quantify only over finite sets
$X$ corresponds to the fact that the run of ${\mathcal{C}}$ can assign
non-$\top$ states only to a finite prefix of the tree. Moreover, the
cardinality of $X$ is reflected by the number of important states assigned by
a run. It follows that for every $\sigma\in\mathit{Pht}_{\psi}$,

  * •

there exists a finite set $X$ of nodes of $T$ such that
$[T]_{\psi}^{\nu_{\emptyset}[\mathsf{X}\mapsto X]}=\sigma$ if and only if for
some $i\in\\{0,1\\}$ there is a run of ${\mathcal{C}}$ on
${\mathcal{B}}_{\psi}(T)$ that assigns $(i,\sigma)$ to the root, and

  * •

for every $n\in\mathbb{N}$ there exists a finite set $X_{n}$ of nodes of $T$
such that $[T]_{\psi}^{\nu_{\emptyset}[\mathsf{X}\mapsto X_{n}]}=\sigma$ and
$|X_{n}|\geq n$ if and only if for some $i\in\\{0,1\\}$ and for every
$n\in\mathbb{N}$ there is a run $\rho_{n}$ of ${\mathcal{C}}$ on
${\mathcal{B}}_{\psi}(T)$ that assigns $(i,\sigma)$ to the root, and such that
$\rho_{n}$ assigns an important state to at least $n$ nodes.

Thus, looking at the root’s label in ${\mathcal{B}}_{\varphi}(T)$ we can
determine $[T]_{\varphi}^{\nu_{\emptyset}}$. This finishes the proof of Item
(2) in the case of the $\mathsf{U}$ quantifier.

Next, still supposing that $\varphi\equiv\mathsf{U}\mathsf{X}.\psi$, we prove
Item (1) using Item (2), which is already proved. It is essential that, by the
definition of the MSO+$\mathsf{U^{fin}}$ logic, all free variables of
$\varphi$ come from ${\mathcal{V}}^{\mathsf{fin}}$, that is, represent finite
sets. This means that only nodes from a finite prefix of a considered tree can
belong to $\nu(\mathsf{Y})$ for $\mathsf{Y}$ free in $\varphi$ (since clearly
the number of free variables is finite). Outside of this finite prefix we can
read the $\varphi$-phenotype from the output of ${\mathcal{B}}_{\varphi}$
(because the valuation is empty there), and in the finite prefix we can
compute them using the $\mathit{Comp}$ function.

More precisely, as ${\mathcal{A}}_{\varphi}$ we take
${\mathcal{B}}_{\varphi}$, coming from Item (2). Item (2) gives us a function
$f_{\varphi}\colon\Sigma^{\mathsf{out}}({\mathcal{A}}_{\varphi})\to\mathit{Pht}_{\varphi}$
reading the $\varphi$-phenotype of a $(\Sigma,r_{\max})$-tree $T$ out of the
root label of ${\mathcal{A}}_{\varphi}(T)$; we also have a function
$g\colon\Sigma^{\mathsf{out}}({\mathcal{A}}_{\varphi})\to\Sigma$ that extracts
original labels out of labels in ${\mathcal{A}}_{\varphi}(T)$. For every
$\tau\in\mathit{Pht}_{\varphi}$ we define the formula $\xi_{\psi,\tau}$ as
follows. It starts with a sequence of $|\mathit{Pht}_{\varphi}|$ existential
quantifiers, quantifying over variables $\mathsf{X}_{\rho}$ for all
$\rho\in\mathit{Pht}_{\varphi}$. The intention is that, in a tree $T$, every
$\mathsf{X}_{\rho}$ represents the set of nodes $u$ such that
$[T{\restriction}_{u}]_{\varphi}^{\nu{\restriction}_{u}}=\rho$. Inside the
quantification we say that

  * •

the sets represented by these variables are disjoint, and every node belongs
to some of them,

  * •

the root belongs to $\mathsf{X}_{\tau}$,

  * •

if a node with label $\eta\in\Sigma^{\mathsf{out}}({\mathcal{A}}_{\varphi})$
belongs to $\mathsf{X}_{\rho}$, and its children belong to
$\mathsf{X}_{\rho_{1}},\dots,\mathsf{X}_{\rho_{r}}$, respectively (where
$r\leq r_{\max}$), and $R$ is the set of free variables $\mathsf{Y}$ of
$\varphi$ for which the node belongs to $\nu(\mathsf{Y})$, then
$\rho=\mathit{Comp}_{g(\eta),r,\varphi}(R,\rho_{1},\dots,\rho_{r})$ (there are
only finitely many possibilities for
$\rho,\rho_{1},\dots,\rho_{r}\in\mathit{Pht}_{\varphi}$, for
$r\in\\{0,\dots,r_{\max}\\}$, for
$\eta\in\Sigma^{\mathsf{out}}({\mathcal{A}}_{\varphi})$, and finitely many
free variables of $\varphi$, thus the constructed formula can be just a big
alternative listing all possible cases), and

  * •

if a node with label $\eta\in\Sigma^{\mathsf{out}}({\mathcal{A}}_{\varphi})$
belongs to $\mathsf{X}_{\rho}$ and none of $\nu(\mathsf{Y})$ for $\mathsf{Y}$
free in $\varphi$ contains this node or some its descendant, then
$\rho=f_{\varphi}(\eta)$.

Consider now a $(\Sigma,r_{\max})$-tree $T$, and a valuation $\nu$ in this
tree. If $[T]_{\varphi}^{\nu}=\tau$, then we can show that
$\xi_{\varphi,\tau}$ is true by taking for $\mathsf{X}_{\rho}$ the set of
nodes $u$ for which
$[T{\restriction}_{u}]_{\varphi}^{\nu{\restriction}_{u}}=\rho$ (for every
$\rho\in\mathit{Pht}_{\varphi}$). Conversely, suppose that
$\xi_{\varphi,\tau}$ is true. Then we can prove that a node $u$ can belong to
the set represented by $\mathsf{X}_{\rho}$ (for
$\rho\in\mathit{Pht}_{\varphi}$) only when
$[T{\restriction}_{u}]_{\varphi}^{\nu{\restriction}_{u}}=\rho$. The proof is
by a straightforward induction on the number of descendants of $u$ that belong
to $\nu(\mathsf{Y})$ for some $\mathsf{Y}$ free in $\varphi$; we use Lemma 3.1
for the induction step.

Now the proof of Lemma 7 follows easily. Indeed, when $\varphi$ is a sentence
(has no free variables), $[T]_{\varphi}^{\nu_{\emptyset}}$ determines whether
$\varphi$ holds in $T$. Thus, it is enough to take the automaton
${\mathcal{B}}_{\varphi}$ constructed in Lemma 9, and replace the function
$f_{\varphi}$ by the set
$\Sigma_{\mathsf{F}}=\\{\eta\in\Sigma^{\mathsf{out}}({\mathcal{A}})\mid\mathit{tv}_{\varphi}(f_{\varphi}(\eta))\\}$
(where $\mathit{tv}_{\varphi}$, defined on page 3.1, given a
$\varphi$-phenotype says whether $\varphi$ holds in trees having this
$\varphi$-phenotype).

We remark that the WMSO+$\mathsf{U}$ logic (which is weaker than
MSO+$\mathsf{U^{fin}}$) corresponds to nested $\mathsf{U}$-prefix automata,
composed of $\mathsf{U}$-prefix automata only (i.e., not using MSO automata).
Indeed, MSO automata are needed only to deal with infinite sets; when all
quantified sets are finite, we can simulate all the constructs using
$\mathsf{U}$-prefix automata [Par18a].

We also remark that Bojańczyk and Toruńczyk [BT12] introduce another model of
automata equivalent to WMSO+$\mathsf{U}$: nested limsup automata. A common
property of these two models is that both of them are nested; the components
of nested limsup automata are of a different form, though.

##  4\. Proof of the main theorem

In this section we prove our main theorem—Theorem 1. To this end, we have to
recall three properties of recursion schemes: logical reflection (Fact 10),
SUP reflection (Fact 11), and closure under composition with finite tree
transducers (Fact 12).

The property of logical reflection for schemes comes from Broadbent, Carayol,
Ong, and Serre [BCOS10]. They state it for sentences of $\mu$-calculus, but
$\mu$-calculus and MSO are equivalent over infinite trees [EJ91].

######  Fact 10 (logical reflection [BCOS10, Theorem 2(ii)]).

For every MSO sentence $\varphi$ and every scheme ${\mathcal{G}}$ generating a
tree $T$ one can construct a scheme ${\mathcal{G}}_{\varphi}$ that generates a
tree of the same shape as $T$, and such that its every node $u$ is labeled by
a pair $(a_{u},b_{u})$, where $a_{u}$ is the label of $u$ in $T$, and $b_{u}$
is $\mathsf{tt}$ if $\varphi$ is satisfied in $T{\restriction}_{u}$ and
$\mathsf{ff}$ otherwise. ∎

The SUP reflection is the heart of our proof. In order to talk about this
property, we need a few more definitions. By $\\#_{a}(U)$ we denote the number
of $a$-labeled nodes in a (finite) tree $U$. For a set of (finite) trees
${\mathcal{L}}$ and a set of symbols $A$, we define a predicate
$\mathsf{SUP}_{A}({\mathcal{L}})$, which holds if for every $n\in\mathbb{N}$
there is some $U_{n}\in{\mathcal{L}}$ such that for all $a\in A$ it holds that
$\\#_{a}(U_{n})\geq n$.

Originally, in the simultaneous unboundedness problem we consider
nondeterministic higher-order recursion schemes, which instead of generating a
single infinite tree, recognize a set of finite trees. We use here an
equivalent formulation, in which the set of finite trees is encoded in a
single infinite tree. To this end, we use a special letter $\mathsf{nd}$,
denoting a nondeterministic choice. We write $T\to_{\mathsf{nd}}U$ if $U$ is
obtained from $T$ by choosing some $\mathsf{nd}$-labeled node $u$ and some its
child $v$, and attaching $T{\restriction}_{v}$ in place of
$T{\restriction}_{u}$. In other words, $\to_{\mathsf{nd}}$ is the smallest
relation such that $\mathsf{nd}\langle
T_{1},\dots,T_{r}\rangle\to_{\mathsf{nd}}T_{j}$ for $j\in\\{1,\dots,r\\}$, and
if $T_{j}\to_{\mathsf{nd}}T_{j}^{\prime}$ for some $j\in\\{1,\dots,r\\}$, and
$T_{i}=T_{i}^{\prime}$ for all $i\in\\{1,\dots,r\\}\setminus\\{j\\}$, then
$a\langle T_{1},\dots,T_{r}\rangle\to_{\mathsf{nd}}a\langle
T_{1}^{\prime},\dots,T_{r}^{\prime}\rangle$. For a tree $T$,
${\mathcal{L}}(T)$ is the set of all finite trees $U$ such that
$\\#_{\mathsf{nd}}(U)=\\#_{\omega}(U)=0$ and $T\to_{\mathsf{nd}}^{*}U$.

######  Fact 11 (SUP reflection [Par18b, Theorem 10.1]).

For every scheme ${\mathcal{G}}$ generating a tree $T$ one can construct a
scheme ${\mathcal{G}}_{\mathit{SUP}}$ that generates a tree of the same shape
as $T$, and such that its every node $u$, having in $T$ label $a_{u}$, is
labeled by

  * •

a pair
$(a_{u},\\{A\subseteq\Sigma_{\mathcal{G}}\mid\mathsf{SUP}_{A}({\mathcal{L}}(T{\restriction}_{u}))\\})$,
if $a_{u}\neq\mathsf{nd}$, and

  * •

the letter $\mathsf{nd}$, if $a_{u}=\mathsf{nd}$. ∎

The third recalled fact (Fact 12) talks about finite tree transducers. A
_(deterministic, top-down) finite tree transducer_ is a tuple
${\mathcal{T}}=(\Sigma,r_{\max},Q,q_{\mathsf{0}},\delta)$, where $\Sigma$ is a
finite alphabet, $r_{\max}$ is the maximal arity of considered trees, $Q$ is a
finite set of states, $q_{\mathsf{0}}\in Q$ is an initial state, and $\delta$
is a transition function mapping $Q\times\Sigma\times\\{0,\dots,r_{\max}\\}$
to finite lambda-terms. A triple $(q,a,r)$ should be mapped by $\delta$ to a
term that uses only node constructors and variables of the form
$\mathsf{x}_{i,p}$, where $i\in\\{1,\dots,r\\}$ and $p\in Q$ (applications and
lambda-binders are not allowed); at least one node constructor has to be used
(the whole $\delta(q,a,r)$ cannot be equal to a variable).

For a $(\Sigma,r_{\max})$-tree $T$ and a state $q\in Q$, we define
${\mathcal{T}}_{q}(T)$ by coinduction, as follows: if $T=a\langle
T_{1},\dots,T_{r}\rangle$, then ${\mathcal{T}}_{q}(T)$ is the tree obtained
from $\delta(q,a,r)$ by substituting ${\mathcal{T}}_{p}(T_{i})$ for the
variable $\mathsf{x}_{i,p}$, for all $i\in\\{1,\dots,r\\}$ and $p\in Q$. In
the root we start from the initial state, that is, we define
${\mathcal{T}}(T)={\mathcal{T}}_{q_{\mathsf{0}}}(T)$. We have the following
fact.

######  Fact 12.

For every finite tree transducer
${\mathcal{T}}=(\Sigma,r_{\max},Q,q_{\mathsf{0}},\delta)$ and every scheme
${\mathcal{G}}$ generating a $(\Sigma,r_{\max})$-tree $T$, one can construct a
scheme ${\mathcal{G}}_{\mathcal{T}}$ that generates the tree
${\mathcal{T}}(T)$. ∎

This fact follows from the equivalence between schemes and collapsible
pushdown systems [HMOS08], as it is straightforward to compose a collapsible
pushdown system with ${\mathcal{T}}$ (where due to Fact 2 we can assume that
$\Lambda({\mathcal{G}})$ is fully convergent, i.e., that every node of $T$ is
explicitly generated by the collapsible pushdown system). Since we are not
aware of any proof of this fact in the literature, we give more details in
Appendix A.

Using Fact 10 we can compose schemes with MSO automata, as stated below.

######  Lemma 13.

For every MSO automaton ${\mathcal{A}}$ and every scheme ${\mathcal{G}}$
generating a tree $T$, where
$\Sigma_{\mathcal{G}}\subseteq\Sigma^{\mathsf{in}}({\mathcal{A}})$, one can
construct a scheme ${\mathcal{G}}_{\mathcal{A}}$ that generates the tree
${\mathcal{A}}(T)$.

######  Proof 4.1.

Let ${\mathcal{A}}=(\Sigma,Q,(\varphi_{q})_{q\in Q})$. Assume that
$Q=\\{1,\dots,n\\}$, and take ${\mathcal{G}}_{0}={\mathcal{G}}$ and $T_{0}=T$.
Consecutively for $q=1,\dots,n$ we want to apply Fact 10 to $\varphi_{q}$ and
${\mathcal{G}}_{q-1}$, and obtain a scheme ${\mathcal{G}}_{q}$ that generates
a tree $T_{q}$ of the same shape as $T$, and such that its every node $u$ is
labeled by a tuple $(a,b_{1},\dots,b_{q})$, where $a$ is the label of $u$ in
$T$, and $b_{i}$ says whether $\varphi_{i}$ is satisfied in
$T{\restriction}_{u}$ for $i\in\\{1,\dots,q\\}$. Strictly speaking, we cannot
apply Fact 10 to the original sentences $\varphi_{q}$ (these sentences can be
evaluated in $T$, but not in $T_{q-1}$). We need to slightly modify the
sentences: out of $\varphi_{q}$ we obtain $\varphi_{q}^{\prime}$ by changing
every subformula of the form $a(\mathsf{X})$ to a formula saying that every
node in the set represented by $\mathsf{X}$ is labeled by a letter from
$\\{a\\}\times\\{\mathsf{tt},\mathsf{ff}\\}^{q-1}$. Then $\varphi_{q}$ is
satisfied in $T{\restriction}_{u}$ if and only if $\varphi_{q}^{\prime}$ is
satisfied in $T_{q-1}{\restriction}_{u}$; in consequence, we can apply Fact 10
to $\varphi_{q}^{\prime}$ and ${\mathcal{G}}_{q-1}$.

The last tree, $T_{n}$, contains truth values of all sentences $\varphi_{q}$.
In order to obtain ${\mathcal{G}}_{A}$ as required, it is thus enough to
rename letters appearing in ${\mathcal{G}}_{n}$: we change every letter
$(a,b_{1},\dots,b_{n})$ to $(a,f)$ for $f\colon Q\to\\{0,1,2\\}$ mapping every
$q\in Q$ to $1$ if $b_{q}=\mathsf{tt}$, and to $0$ if $b_{q}=\mathsf{ff}$.

As one can expect, we can also compose schemes with $\mathsf{U}$-prefix
automata, and for that we need Facts 11 and 12.

######  Lemma 14.

For every $\mathsf{U}$-prefix automaton ${\mathcal{A}}$ and every scheme
${\mathcal{G}}$ generating a tree $T$, where
$\Sigma_{\mathcal{G}}\subseteq\Sigma^{\mathsf{in}}({\mathcal{A}})$, one can
construct a scheme ${\mathcal{G}}_{\mathcal{A}}$ that generates the tree
${\mathcal{A}}(T)$.

It is easy to deduce Theorem 1 out of Lemmata 13 and 14. Indeed, consider an
MSO+$\mathsf{U^{fin}}$ sentence $\varphi$ and a scheme ${\mathcal{G}}_{0}$
generating a tree $T_{0}$. By Lemma 7, $\varphi$ is equivalent to a nested
$\mathsf{U}$-prefix MSO automaton
${\mathcal{A}}={\mathcal{A}}_{1}\vartriangleright\dots\vartriangleright{\mathcal{A}}_{k}$,
together with an accepting set $\Sigma_{\mathsf{F}}$. By consecutively
applying Lemmata 13 and 14 for $i=1,\dots,k$, we combine ${\mathcal{G}}_{i-1}$
with ${\mathcal{A}}_{i}$, obtaining a scheme ${\mathcal{G}}_{i}$ that
generates the tree $T_{i}={\mathcal{A}}_{i}(T_{i-1})$. The root of
$T_{k}={\mathcal{A}}(T_{0})$ has label in $\Sigma_{\mathsf{F}}$ if and only if
$\varphi$ is satisfied in $T_{0}$. Surely this label can be read: having
${\mathcal{G}}_{k}$, we simply start generating the tree $T_{k}$, until its
root is generated (by Fact 2, we can assume that $\Lambda({\mathcal{G}}_{k})$
is fully convergent).

We now come to the proof of Lemma 14. We are thus given a $\mathsf{U}$-prefix
automaton ${\mathcal{A}}=(\Sigma,Q,Q_{\mathsf{imp}},\Delta)$, and a scheme
${\mathcal{G}}$ generating a tree $T$, where
$\Sigma_{\mathcal{G}}\subseteq\Sigma$; our goal is to create a scheme
${\mathcal{G}}_{\mathcal{A}}$ that generates the tree ${\mathcal{A}}(T)$. As a
first step, we create a finite tree transducer ${\mathcal{T}}$ that converts
$T$ into a tree containing all runs of ${\mathcal{A}}$ on all subtrees of $T$.
Let us write $Q=\\{p_{1},\dots,p_{|Q|}\\}$. As ${\mathcal{T}}$ we take
$(\Sigma_{\mathcal{G}},r_{\max}({\mathcal{G}}),Q\cup\\{q_{\mathsf{0}},\top\\},q_{\mathsf{0}},\delta)$,
where $q_{\mathsf{0}}\not\in Q$ is a fresh state, and $\delta$ is defined as
follows. For $q\in Q$, $a\in\Sigma_{\mathcal{G}}$, and $r\leq
r_{\max}({\mathcal{G}})$ we take

$\displaystyle\delta(q,a,r)=\mathsf{nd}\langle
q\langle\mathsf{x}_{1,q_{11}},\dots,\mathsf{x}_{r,q_{1r}}\rangle,\dots,q\langle\mathsf{x}_{1,q_{k1}},\dots,\mathsf{x}_{r,q_{kr}}\rangle\rangle\,,$

where $(q,a,q_{11},\dots,q_{1r}),\dots,(q,a,q_{k1},\dots,q_{kr})$ are all
elements of $\Delta$ being of length $r+2$ and having $q$ and $a$ on the first
two coordinates. Moreover, for $a\in\Sigma_{\mathcal{G}}$ and $r\leq
r_{\max}({\mathcal{G}})$ (and for a special letter “?”) we take

$\displaystyle\delta(q_{\mathsf{0}},a,r)$
$\displaystyle=a\langle\mathsf{x}_{1,q_{\mathsf{0}}},\dots,\mathsf{x}_{r,q_{\mathsf{0}}},?\langle\delta(p_{1},a,r)\rangle,\dots,?\langle\delta(p_{|Q|},a,r)\rangle\rangle\,,$
and $\displaystyle\delta(\top,a,r)$ $\displaystyle=\top\langle\rangle\,.$

We see that ${\mathcal{T}}(T)$ contains all nodes of the original tree $T$.
Additionally, below every node $u$ coming from $T$ we have $|Q|$ new children
labeled by $?$, such that subtrees starting below these children describe runs
of ${\mathcal{A}}$ on $T{\restriction}_{u}$, starting in particular states.
More precisely, when $u$ has $r$ children in $T$, for every
$i\in\\{1,\dots,|Q|\\}$ there is a bijection between trees $U$ in
${\mathcal{L}}({\mathcal{T}}(T){\restriction}_{u(r+i)1})$ and runs $\rho$ of
${\mathcal{A}}$ on $T{\restriction}_{u}$ such that $\rho(\varepsilon)=p_{i}$.
The label of every node $v$ in such a tree $U$ contains the state assigned by
$\rho$ to $v$, where $U$ contains exactly all nodes to which $\rho$ assigns a
state from $Q$, and all minimal nodes to which $\rho$ assigns $\top$ (i.e.,
such that $\rho$ does not assign $\top$ to their parents). Recall that by
definition $\rho$ can assign a state from $Q$ only to a finite prefix of the
tree $T{\restriction}_{u}$, which corresponds to the fact that
${\mathcal{L}}({\mathcal{T}}(T){\restriction}_{u(r+i)1})$ contains only finite
trees.

Actually, we need to consider a transducer ${\mathcal{T}}^{\prime}$ obtained
from ${\mathcal{T}}$ by a slight modification: we replace the letter $q$
appearing in $\delta(q,a,r)$ by $1$ if $q\in Q_{\mathsf{imp}}$, and by $0$ if
$q\not\in Q_{\mathsf{imp}}$. Then, for a node $u$ of $T$ having $r$ children,
and for $i\in\\{1,\dots,|Q|\\}$, we have the following equivalence:
$\mathsf{SUP}_{\\{1\\}}({\mathcal{T}}^{\prime}(T){\restriction}_{u(r+i)})$
holds if and only if for every $n\in\mathbb{N}$ there is a run $\rho_{n}$ of
${\mathcal{A}}$ on $T{\restriction}_{u}$ that assigns $p_{i}$ to the root of
$T{\restriction}_{u}$, and such that for at least $n$ nodes $v$ it holds that
$\rho_{n}(v)\in Q_{\mathsf{imp}}$.

We now apply Fact 12 to ${\mathcal{G}}$ and ${\mathcal{T}}^{\prime}$; we
obtain a scheme ${\mathcal{G}}_{{\mathcal{T}}^{\prime}}$ that generates the
tree ${\mathcal{T}}^{\prime}(T)$. Then, we apply Fact 11 (SUP reflection) to
${\mathcal{G}}_{{\mathcal{T}}^{\prime}}$, which gives us a scheme
${\mathcal{G}}^{\prime}$. The tree $T^{\prime}$ generated by
${\mathcal{G}}^{\prime}$ has the same shape as ${\mathcal{T}}^{\prime}(T)$,
but in the label of every node $v$ (originally having label other than
$\mathsf{nd}$) there is additionally written a set ${\mathcal{U}}$ containing
these sets $A\subseteq\Sigma_{{\mathcal{G}}_{{\mathcal{T}}^{\prime}}}$ for
which $\mathsf{SUP}_{A}({\mathcal{L}}(T{\restriction}_{v}))$ holds. Next,
using Fact 10 (logical reflection) $2|Q|$ times, we annotate every node $u$ of
$T^{\prime}$, having $r^{\prime}$ children, by logical values of the following
properties, for $i=1,\dots,|Q|$:

  * •

whether $r^{\prime}\geq|Q|$ and
${\mathcal{L}}(T^{\prime}{\restriction}_{u(r^{\prime}-|Q|+i)1})$ is nonempty,
and

  * •

whether $r^{\prime}\geq|Q|$ and the label $(a,{\mathcal{U}})$ of node
$u(r^{\prime}-|Q|+i)$ in $T^{\prime}$ satisfies $\\{1\\}\in{\mathcal{U}}$.

Clearly both these properties can be expressed in MSO. For nodes $u$ coming
from $T$, the first property holds when there is a run of ${\mathcal{A}}$ on
$T{\restriction}_{u}$ that assigns $p_{i}$ to the root of
$T{\restriction}_{u}$, and the second property holds when for every
$n\in\mathbb{N}$ there is a run $\rho_{n}$ of ${\mathcal{A}}$ on
$T{\restriction}_{u}$ that assigns $p_{i}$ to the root of
$T{\restriction}_{u}$, and such that for at least $n$ nodes $w$ it holds that
$\rho_{n}(w)\in Q_{\mathsf{imp}}$. Let ${\mathcal{G}}^{\prime\prime}$ be the
scheme generating the tree $T^{\prime\prime}$ containing these annotations.

Finally, we create ${\mathcal{G}}_{\mathcal{A}}$ by slightly modifying
${\mathcal{G}}^{\prime\prime}$: we replace every node constructor
$(a,{\mathcal{U}},\sigma_{1},\tau_{1},\dots,\sigma_{|Q|},\tau_{|Q|})\langle
P_{1},\dots,P_{r+|Q|}\rangle$ with $(a,f)\langle P_{1},\dots,P_{r}\rangle$,
where $f\colon Q\to\\{0,1,2\\}$ is such that $f(p_{i})=2$ if
$\tau_{i}=\mathsf{tt}$, and $f(p_{i})=1$ if $\sigma_{i}=\mathsf{tt}$ but
$\tau_{i}=\mathsf{ff}$, and $f(p_{i})=0$ otherwise, for all
$i\in\\{1,\dots,|Q|\\}$ (we do not do anything with node constructors of arity
smaller than $|Q|$). As a result, only the nodes coming from $T$ remain, and
they are appropriately relabeled.

##  5\. Extensions

In this section we give a few possible extensions of our main theorem, saying
that we can evaluate MSO+$\mathsf{U^{fin}}$ sentences on trees generated by
recursion schemes. First, we notice that our solution actually proves a
stronger result: logical reflection for MSO+$\mathsf{U^{fin}}$.

######  Theorem 15.

For every MSO+$\mathsf{U^{fin}}$ sentence $\varphi$ and every scheme
${\mathcal{G}}$ generating a tree $T$ one can construct a scheme
${\mathcal{G}}_{\varphi}$ that generates a tree of the same shape as $T$, and
such that its every node $u$ is labeled by a pair $(a_{u},b_{u})$, where
$a_{u}$ is the label of $u$ in $T$, and $b_{u}$ is $\mathsf{tt}$ if $\varphi$
is satisfied in $T{\restriction}_{u}$ and $\mathsf{ff}$ otherwise.

######  Proof 5.1.

In the proof of Theorem 1 we have constructed a nested $\mathsf{U}$-prefix
automaton ${\mathcal{A}}$ equivalent to $\varphi$, and then a scheme
${\mathcal{G}}_{\mathcal{A}}$ that generates the tree ${\mathcal{A}}(T)$. In
every node $u$ of ${\mathcal{A}}(T)$ it is written whether
$T{\restriction}_{u}$ satisfies $\varphi$. Moreover, labels of
${\mathcal{A}}(T)$ contain also original labels coming from $T$. Thus in order
to obtain ${\mathcal{G}}_{\varphi}$ it is enough to appropriately relabel node
constructors appearing in ${\mathcal{G}}_{\mathcal{A}}$.

In Theorem 15, the sentence $\varphi$ talks only about the subtree starting in
$u$. One can obtain a stronger version of logical reflection (Theorem 16),
where $\varphi$ is a formula allowed to talk about $u$ in the context of the
whole tree. This version can be obtained as a simple corollary of Theorem 15
by using the same methods as in Broadbent et al. [BCOS10, Proof of Corollary
2]. As shown on page 5.4, it is also an immediate consequence of our next
theorem (Theorem 17).

######  Theorem 16.

For every MSO+$\mathsf{U^{fin}}$ formula $\varphi(\mathsf{X})$ with one free
variable $\mathsf{X}$ and every scheme ${\mathcal{G}}$ generating a tree $T$,
one can construct a scheme ${\mathcal{G}}_{\varphi}$ that generates a tree of
the same shape as $T$, and such that its every node $u$ is labeled by a pair
$(a_{u},b_{u})$, where $a_{u}$ is the label of $u$ in $T$, and $b_{u}$ is
$\mathsf{tt}$ if $\varphi$ is satisfied in $T$ with $\mathsf{X}$ valuated to
$\\{u\\}$, and $\mathsf{ff}$ otherwise.

Carayol and Serre [CS12] show one more property of MSO and schemes, called
effective selection. This time we are given an MSO sentence $\psi$ of the form
$\exists\mathsf{X}.\varphi$. Assuming that $\psi$ is satisfied in the tree $T$
generated by a scheme ${\mathcal{G}}$, one wants to compute an example set $X$
of nodes of $T$, such that $\varphi$ is true in $T$ with the variable
$\mathsf{X}$ valuated to this set $X$. The theorem says that it is possible to
create a scheme ${\mathcal{G}}_{\varphi}$ that generates a tree of the same
shape as $T$, in which nodes belonging to some such example set $X$ are
marked. We can show the same for MSO+$\mathsf{U^{fin}}$.

######  Theorem 17.

For every MSO+$\mathsf{U^{fin}}$ formula $\varphi(\mathsf{X})$ with one free
variable $\mathsf{X}\in{\mathcal{V}}^{\mathsf{inf}}$ and every scheme
${\mathcal{G}}$ generating a tree $T$, if
$\exists\mathsf{X}.\varphi(\mathsf{X})$ holds in $T$, then one can construct a
scheme ${\mathcal{G}}_{\varphi}$ that generates a tree $T^{\prime}$ of the
same shape as $T$, and such that its every node $u$ is labeled by a pair
$(a_{u},b_{u})$, where $a_{u}$ is the label of $u$ in $T$, and $b_{u}$ belongs
to $\\{\mathsf{tt},\mathsf{ff}\\}$; when $X$ is the set of nodes of
$T^{\prime}$ having $\mathsf{tt}$ on the second coordinate of the label,
$\varphi$ is holds in $T$ with $\mathsf{X}$ valuated to $X$.

The proof of this theorem bases on the following lemma, which is also
interesting in itself.

######  Lemma 18.

For every MSO+$\mathsf{U^{fin}}$ formula $\varphi$ and every scheme
${\mathcal{G}}$ generating a tree $T$ one can construct a scheme
${\mathcal{G}}_{+}$ that generates a tree $T^{\prime}$ of the same shape as
$T$, and an MSO formula $\varphi_{\mathit{MSO}}$ (whose all free variables are
also free in $\varphi$) such that for every valuation $\nu$ in $T$ (defined at
least for all free variables of $\varphi$) it holds that
$T^{\prime},\nu\models\varphi_{\mathit{MSO}}$ if and only if
$T,\nu\models\varphi$. Moreover, the label of every node of $T^{\prime}$
contains as its part the label of that node in $T$.

######  Proof 5.2.

Recall that Lemma 9 gives us a nested $\mathsf{U}$-prefix MSO automaton
${\mathcal{A}}_{\varphi}$ and MSO formulae $\xi_{\varphi,\tau}$ for all
$\tau\in\mathit{Pht}_{\varphi}$ such that for every valuation $\nu$ in $T$
(where $T$ is now the fixed
$(\Sigma_{\mathcal{G}},r_{\max}({\mathcal{G}}))$-tree generated by
${\mathcal{G}}$) it holds that
${\mathcal{A}}_{\varphi}(T),\nu\models\xi_{\varphi,\tau}$ if and only if
$[T]_{\varphi}^{\nu}=\tau$.

Applying Lemmata 13 and 14 to components of the automaton
${\mathcal{A}}_{\varphi}$, out of the scheme ${\mathcal{G}}$ we can construct
a scheme ${\mathcal{G}}_{+}$ that generates the tree
${\mathcal{A}}_{\varphi}(T)$.

Recall that $\mathit{tv}_{\varphi}(\tau)$ says whether $\varphi$ is true in a
tree having $\varphi$-phenotype $\tau$, and consider the MSO formula

$\displaystyle\varphi_{\mathit{MSO}}\equiv\bigvee_{\begin{subarray}{c}\tau\in\mathit{Pht}_{\varphi}\\\
\mathit{tv}_{\varphi}(\tau)\end{subarray}}\xi_{\varphi,\tau}\,.$

By the above, for every valuation $\nu$, it holds that
${\mathcal{A}}_{\varphi}(T),\nu\models\varphi_{\mathit{MSO}}$ if and only if
$T,\nu\models\varphi$, as required in the thesis.

Using the above lemma, we can easily deduce effective selection for
MSO+$\mathsf{U^{fin}}$ out of effective selection for MSO.

######  Proof 5.3 (Proof of Theorem 17).

Using effective selection for MSO (which is a theorem with the same statement
as Theorem 17, but for the MSO logic [CS12]) for the formula
$\varphi_{\mathit{MSO}}$ and for the scheme ${\mathcal{G}}_{+}$ (created by
Lemma 18) we obtain a scheme ${\mathcal{G}}_{\varphi}^{\prime}$. It is almost
as required: it generates a tree $T^{\prime}$ of the same shape as $T$ (but
with some additional parts of labels, added by ${\mathcal{G}}_{+}$), where
additionally nodes of some set $X$ are marked, so that
$\varphi_{\mathit{MSO}}$ holds in $T^{\prime}$ with $\mathsf{X}$ valuated to
$X$. Lemma 18 implies that then also $\varphi$ holds in $T$ with $\mathsf{X}$
valuated to $X$. Thus, it is enough to modify node constructors of
${\mathcal{G}}_{\varphi}^{\prime}$: out of every letter we leave only the
original letter coming from ${\mathcal{G}}$, and the last component marking
the set $X$, while we remove all the components added by ${\mathcal{G}}_{+}$.

One may want to obtain an analogous theorem for
$\mathsf{X}\in{\mathcal{V}}^{\mathsf{fin}}$, that is, for a sentence of the
form ${\exists_{\mathsf{fin}}}\mathsf{X}.\varphi(X)$. It is, however, a
special case of Theorem 17, which can be used with the sentence
$\exists\mathsf{X}^{\prime}.{\exists_{\mathsf{fin}}}\mathsf{X}.\mathsf{X}\subseteq\mathsf{X}^{\prime}\land\mathsf{X}^{\prime}\subseteq\mathsf{X}\land\varphi(\mathsf{X})$.
We remark, though, that the version of Theorem 17 for
$\mathsf{X}\in{\mathcal{V}}^{\mathsf{fin}}$ is actually also a corollary of
Theorem 1, because there are only countably many finite sets $X$, so we may
try one after another, until we find some set for which $\varphi$ is
satisfied; it is easy to hardcode a given set $X$ in the formula (or in the
scheme).

We now show how Theorem 16 follows from Theorem 17.

######  Proof 5.4 (Proof of Theorem 16).

We use Theorem 17 for

$\displaystyle\varphi^{\prime}(\mathsf{X}^{\prime})\equiv\forall\mathsf{X}.\mathit{sing}(\mathsf{X})\mathbin{\to}(\mathsf{X}\subseteq\mathsf{X}^{\prime}\mathbin{\to}\varphi(\mathsf{X}))\land(\neg(\mathsf{X}\subseteq\mathsf{X}^{\prime})\mathbin{\to}\neg\varphi(\mathsf{X}))\,.$

The only set $X^{\prime}$ for which $\varphi^{\prime}$ is true in a tree $T$
is the set of all nodes $u$ for which $\varphi$ is true in $T$ with
$\mathsf{X}$ valuated to $\\{u\\}$. Thus the scheme
${\mathcal{G}}_{\varphi^{\prime}}$ obtained from Theorem 17 satisfies the
thesis of Theorem 16.

Our algorithm for Theorem 1 has nonelementary complexity. This is unavoidable,
as already model-checking of WMSO sentences on the infinite word over an unary
alphabet is nonelementary. It would be interesting to find some other
formalism for expressing unboundedness properties, maybe using some model of
automata, for which the model-checking problem has better complexity. We leave
this issue for future work.

Finally, we remark that in our solution we do not use the full power of the
simultaneous unboundedness problem, we only use the single-letter case. On the
other hand, it seems that MSO+$\mathsf{U^{fin}}$ is not capable to express
simultaneous unboundedness, only its single-letter case. Thus, another
direction for a future work is to extend MSO+$\mathsf{U^{fin}}$ to a logic
that can actually express simultaneous unboundedness. As a possible candidate
we see the qcMSO logic introduced in Kaiser, Lang, Leßenich, and Löding
[KLLL15], in which simultaneous unboundedness is expressible.

## References

  * [Aho68] Alfred V. Aho.  Indexed grammars - an extension of context-free grammars.  J. ACM, 15(4):647–671, 1968.
  * [BCCC96] Luca Breveglieri, Alessandra Cherubini, Claudio Citrini, and Stefano Crespi-Reghizzi.  Multi-push-down languages and grammars.  Int. J. Found. Comput. Sci., 7(3):253–292, 1996.
  * [BCL08] Achim Blumensath, Thomas Colcombet, and Christof Löding.  Logical theories and compatible operations.  In Jörg Flum, Erich Grädel, and Thomas Wilke, editors, Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 73–106. Amsterdam University Press, 2008.
  * [BCOS10] Christopher H. Broadbent, Arnaud Carayol, C.-H. Luke Ong, and Olivier Serre.  Recursion schemes and logical reflection.  In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 120–129. IEEE Computer Society, 2010.
  * [BK13] Christopher H. Broadbent and Naoki Kobayashi.  Saturation-based model checking of higher-order recursion schemes.  In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 129–148. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013.
  * [BO09] Christopher H. Broadbent and C.-H. Luke Ong.  On global model checking trees generated by higher-order recursion schemes.  In Luca de Alfaro, editor, Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5504 of Lecture Notes in Computer Science, pages 107–121. Springer, 2009.
  * [Boj04] Mikołaj Bojańczyk.  A bounding quantifier.  In Jerzy Marcinkowski and Andrzej Tarlecki, editors, Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 41–55. Springer, 2004.
  * [Boj11] Mikołaj Bojańczyk.  Weak MSO with the unbounding quantifier.  Theory Comput. Syst., 48(3):554–576, 2011.
  * [Boj14] Mikołaj Bojańczyk.  Weak MSO+U with path quantifiers over infinite trees.  In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part II, volume 8573 of Lecture Notes in Computer Science, pages 38–49. Springer, 2014.
  * [BPT16] Mikołaj Bojańczyk, Paweł Parys, and Szymon Toruńczyk.  The MSO+U theory of (N, <) is undecidable.  In Nicolas Ollinger and Heribert Vollmer, editors, 33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France, volume 47 of LIPIcs, pages 21:1–21:8. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
  * [BT12] Mikołaj Bojańczyk and Szymon Toruńczyk.  Weak MSO+U over infinite trees.  In Christoph Dürr and Thomas Wilke, editors, 29th International Symposium on Theoretical Aspects of Computer Science, STACS 2012, February 29th - March 3rd, 2012, Paris, France, volume 14 of LIPIcs, pages 648–660. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012\.
  * [CMvRZ15] Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, and Marc Zeitoun.  A note on decidable separability by piecewise testable languages.  In Adrian Kosowski and Igor Walukiewicz, editors, Fundamentals of Computation Theory - 20th International Symposium, FCT 2015, Gdańsk, Poland, August 17-19, 2015, Proceedings, volume 9210 of Lecture Notes in Computer Science, pages 173–185. Springer, 2015.
  * [CPSW15] Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz.  Ordered tree-pushdown systems.  In Prahladh Harsha and G. Ramalingam, editors, 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2015, December 16-18, 2015, Bangalore, India, volume 45 of LIPIcs, pages 163–177. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [CPSW16] Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz.  The diagonal problem for higher-order recursion schemes is decidable.  In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 96–105. ACM, 2016.
  * [CS12] Arnaud Carayol and Olivier Serre.  Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection.  In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012, pages 165–174. IEEE Computer Society, 2012.
  * [Dam82] Werner Damm.  The IO- and OI-hierarchies.  Theor. Comput. Sci., 20:95–207, 1982.
  * [EJ91] E. Allen Emerson and Charanjit S. Jutla.  Tree automata, mu-calculus and determinacy (extended abstract).  In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368–377. IEEE Computer Society, 1991.
  * [FV59] Solomon Feferman and Robert Lawson Vaught.  The first order properties of products of algebraic systems.  Fundamenta Mathematicae, 47(1):57–103, 1959.
  * [GK10] Tobias Ganzow and Łukasz Kaiser.  New algorithm for weak monadic second-order logic on inductive structures.  In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 366–380. Springer, 2010.
  * [Had12] Axel Haddad.  IO vs OI in higher-order recursion schemes.  In Dale Miller and Zoltán Ésik, editors, Proceedings 8th Workshop on Fixed Points in Computer Science, FICS 2012, Tallinn, Estonia, 24th March 2012., volume 77 of EPTCS, pages 23–30, 2012.
  * [HKO16] Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong.  Unboundedness and downward closures of higher-order pushdown automata.  In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 151–163. ACM, 2016.
  * [HM12] Szczepan Hummel and Michał Skrzypczak.  The topological complexity of MSO+U and related automata models.  Fundam. Inform., 119(1):87–111, 2012.
  * [HMOS08] Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre.  Collapsible pushdown automata and recursion schemes.  In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 452–461. IEEE Computer Society, 2008.
  * [KLLL15] Łukasz Kaiser, Martin Lang, Simon Leßenich, and Christof Löding.  A unified approach to boundedness properties in MSO.  In Kreutzer [Kre15], pages 441–456.
  * [KNU02] Teodor Knapik, Damian Niwiński, and Paweł Urzyczyn.  Higher-order pushdown trees are easy.  In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings, volume 2303 of Lecture Notes in Computer Science, pages 205–222. Springer, 2002.
  * [KO09] Naoki Kobayashi and C.-H. Luke Ong.  A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes.  In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009, 11-14 August 2009, Los Angeles, CA, USA, pages 179–188. IEEE Computer Society, 2009.
  * [Kob11] Naoki Kobayashi.  A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes.  In Martin Hofmann, editor, Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6604 of Lecture Notes in Computer Science, pages 260–274. Springer, 2011.
  * [Kob13] Naoki Kobayashi.  Model checking higher-order programs.  J. ACM, 60(3):20:1–20:62, 2013.
  * [Kre15] Stephan Kreutzer, editor.  24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7-10, 2015, Berlin, Germany, volume 41 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [Lä68] Hans Läuchli.  A decision procedure for the weak second order theory of linear order.  Studies in Logic and the Foundations of Mathematics, 50:189–197, 1968.
  * [NO14] Robin P. Neatherway and C.-H. Luke Ong.  TravMC2: Higher-order model checking for alternating parity tree automata.  In Neha Rungta and Oksana Tkachuk, editors, 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, July 21-23, 2014, pages 129–132. ACM, 2014.
  * [Ong06] C.-H. Luke Ong.  On model-checking trees generated by higher-order recursion schemes.  In 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pages 81–90. IEEE Computer Society, 2006.
  * [Par17] Paweł Parys.  The complexity of the diagonal problem for recursion schemes.  In Satya V. Lokam and R. Ramanujam, editors, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, volume 93 of LIPIcs, pages 45:1–45:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
  * [Par18a] Paweł Parys.  Recursion schemes and the WMSO+U logic.  In Rolf Niedermeier and Brigitte Vallée, editors, 35th Symposium on Theoretical Aspects of Computer Science, STACS 2018, February 28 to March 3, 2018, Caen, France, volume 96 of LIPIcs, pages 53:1–53:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018.
  * [Par18b] Paweł Parys.  A type system describing unboundedness.  Submitted, 2018.
  * [PT16] Paweł Parys and Szymon Toruńczyk.  Models of lambda-calculus and the weak MSO logic.  In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 11:1–11:12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
  * [RNO14] Steven J. Ramsay, Robin P. Neatherway, and C.-H. Luke Ong.  A type-directed abstraction refinement approach to higher-order model checking.  In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 61–72. ACM, 2014\.
  * [She75] Saharon Shelah.  The monadic theory of order.  Annals of Mathematics, 102(3):379–419, 1975.
  * [SW14] Sylvain Salvati and Igor Walukiewicz.  Krivine machines and higher-order schemes.  Inf. Comput., 239:340–355, 2014.
  * [SW15a] Sylvain Salvati and Igor Walukiewicz.  A model for behavioural properties of higher-order programs.  In Kreutzer [Kre15], pages 229–243.
  * [SW15b] Sylvain Salvati and Igor Walukiewicz.  Using models to model-check recursive schemes.  Logical Methods in Computer Science, 11(2), 2015.
  * [SW16] Sylvain Salvati and Igor Walukiewicz.  Simply typed fixpoint calculus and collapsible pushdown automata.  Mathematical Structures in Computer Science, 26(7):1304–1350, 2016\.
  * [Zet15] Georg Zetzsche.  An approach to computing downward closures.  In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 440–451. Springer, 2015.

##  Appendix A Proof of Fact 12

As already said, Fact 12 follows easily from the equivalence between schemes
and collapsible pushdown systems. We do not even need to know a full
definition of these systems. Let us recall those fragments that are relevant
for us.

For every $n\in\mathbb{N}$, and every finite set $\Gamma$ containing a
distinguished initial symbol $\bot\in\Gamma$, there are defined:

  * •

a set $\mathcal{PD}_{n,\Gamma}$ of collapsible pushdowns of order $n$ over
stack alphabet $\Gamma$,

  * •

an initial pushdown $\bot_{n}\in\mathcal{PD}_{n,\Gamma}$,

  * •

a finite set $\mathit{Op}_{n,\Gamma}$ of operations on these pushdowns, where
every $\mathit{op}\in\mathit{Op}_{n,\Gamma}$ is a partial function from
$\mathcal{PD}_{n,\Gamma}$ to $\mathcal{PD}_{n,\Gamma}$, and

  * •

a function $\mathit{top}\colon\mathcal{PD}_{n,\Gamma}\to\Gamma$ (returning the
topmost symbol of a pushdown).

We assume that $\mathit{Op}_{n,\Gamma}$ contains the identity operation
$\mathsf{id}$, mapping every element of $\mathcal{PD}_{n,\Gamma}$ to itself.

Having the above, we define a _collapsible pushdown system_ (a _CPS_ for
short) as a tuple ${\mathcal{C}}=(Q,q_{\mathsf{0}},n,\Gamma,\delta)$, where
$Q$ is a set of states, $q_{\mathsf{0}}\in Q$ is an initial state,
$n\in\mathbb{N}$ is an order, $\Gamma$ is a finite stack alphabet, and
$\delta\colon
Q\times\Gamma\to(Q\times\mathit{Op}_{n,\Gamma})\uplus(\Sigma\times Q^{*})$ is
a transition function (where $\Sigma$ is some alphabet). A _configuration_ of
${\mathcal{C}}$ is a pair $(q,s)\in Q\times\mathcal{PD}_{n,\Gamma}$. A
configuration $(p,t)$ is a _successor_ of $(q,s)$, written
$(q,s)\to_{\mathcal{C}}(p,t)$, if $\delta(q,\mathit{top}(s))=(p,\mathit{op})$
and $\mathit{op}(s)=t$. We define when a tree is generated by ${\mathcal{C}}$
from $(q,s)$, by coinduction:

  * •

if $(q,s)\to_{\mathcal{C}}^{*}(p,t)$, and
$\delta(p,\mathit{top}(t))=(a,q_{1},\dots,q_{r})\in\Sigma\times Q^{*}$, and
trees $T_{1},\dots,T_{r}$ are generated by ${\mathcal{C}}$ from
$(q_{1},t),\dots,(q_{r},t)$, respectively, then $a\langle
T_{1},\dots,T_{r}\rangle$ is generated by ${\mathcal{C}}$ from $(q,s)$,

  * •

if there is no $(p,t)$ such that $(q,s)\to_{\mathcal{C}}^{*}(p,t)$ and
$\delta(p,\mathit{top}(t))\in\Sigma\times Q^{*}$, then $\omega\langle\rangle$
is generated by ${\mathcal{C}}$ from $(q,s)$.

Notice that for every configuration $(q,s)$ there is at most one configuration
$(p,t)$ such that $(q,s)\to_{\mathcal{C}}^{*}(p,t)$ and
$\delta(p,\mathit{top}(t))\in\Sigma\times Q^{*}$; in consequence exactly one
tree is generated by ${\mathcal{C}}$ from every configuration. While talking
about the tree generated by ${\mathcal{C}}$, without referring to a
configuration, we mean generating from the initial configuration
$(q_{\mathsf{0}},\bot_{n})$.

We say that a CPS is _fully convergent_ (from a configuration $(q,s)$) if it
generates (from $(q,s)$) a tree without using the second item of the
definition. More formally: we consider the CPS ${\mathcal{C}}_{-\omega}$
obtained from ${\mathcal{C}}$ by replacing $\omega$ with some other letter
$\omega^{\prime}$ (in all transitions), and we say that ${\mathcal{C}}$ is
fully convergent (from $(q,s)$) if ${\mathcal{C}}_{-\omega}$ generates (from
$(q,s)$) a tree without $\omega$-labeled nodes. We have the following fact.

######  Fact 19 ([HMOS08]).

For every scheme ${\mathcal{G}}$ one can construct a CPS ${\mathcal{C}}$ that
generates the tree generated by ${\mathcal{G}}$ and, conversely, for every CPS
${\mathcal{C}}$ one can construct a scheme ${\mathcal{G}}$ that generates the
tree generated by ${\mathcal{C}}$. Both translations preserve the property of
being fully convergent.222Clearly only a fully-convergent CPS/scheme can
generate a tree without $\omega$-labeled nodes. Thus it is easy to preserve
the property of being fully convergent: we can replace all appearances of
$\omega$ by some fresh letter $\omega^{\prime}$, switch to the other
formalism, and then replace $\omega^{\prime}$ back by $\omega$. ∎

In Fact 12 we are given a finite tree transducer
${\mathcal{T}}=(\Sigma,r_{\max},P,p_{\mathsf{0}},\delta_{\mathcal{T}})$, and a
scheme ${\mathcal{G}}$ generating a $(\Sigma,r_{\max})$-tree $T$, and we want
to construct a scheme ${\mathcal{G}}_{\mathcal{T}}$ that generates the tree
${\mathcal{T}}(T)$. By Fact 2 we can assume that ${\mathcal{G}}$ is fully
convergent. As a first step, we translate ${\mathcal{G}}$ to a fully
convergent CPS
${\mathcal{C}}=(Q,q_{\mathsf{0}},n,\Gamma,\delta_{\mathcal{C}})$ generating
$T$, using Fact 19.

Then, we create a CPS
${\mathcal{C}}_{\mathcal{T}}=(R,(q_{\mathsf{0}},p_{\mathsf{0}}),n,\Gamma,\delta)$
by combining ${\mathcal{C}}$ with ${\mathcal{T}}$. Its set of states $R$
contains states of two kinds: pairs $(q,p)\in Q\times P$, and pairs $(q,U)$
where $q\in Q$ and $U$ is a subterm of $\delta_{\mathcal{T}}(p,a,r)$ for some
$(p,a,r)\in P\times\Sigma\times\\{0,\dots,r_{\max}\\}$. We define the
transitions as follows:

  * •

if $\delta_{\mathcal{C}}(q,\chi)=(q^{\prime},\mathit{op})\in
Q\times\mathit{Op}_{n,\Gamma}$, then
$\delta((q,p),\chi)=((q^{\prime},p),\mathit{op})$,

  * •

if $\delta_{\mathcal{C}}(q,\chi)=(a,q_{1},\dots,q_{r})\in\Sigma\times Q^{*}$,
then $\delta((q,p),\chi)=((q,\delta_{\mathcal{T}}(p,a,r)),\mathsf{id})$,

  * •

if $\delta_{\mathcal{C}}(q,\chi)\in\Sigma\times Q^{*}$, then
$\delta((q,b\langle
U_{1},\dots,U_{k}\rangle),\chi)=(b,(q,U_{1}),\dots,(q,U_{k}))$,

  * •

if $\delta_{\mathcal{C}}(q,\chi)=(a,q_{1},\dots,q_{r})\in\Sigma\times Q^{*}$
and $i\in\\{1,\dots,r\\}$, then
$\delta((q,\mathsf{x}_{i,p}),\chi)=((q_{i},p),\mathsf{id})$, and

  * •

all other transitions are irrelevant, and can be defined arbitrarily.

It is easy to prove by coinduction that if ${\mathcal{C}}$ is fully convergent
from some configuration $(q,s)$, then, for every state $p\in P$,
${\mathcal{C}}_{\mathcal{T}}$ generates ${\mathcal{T}}_{p}(T_{q,s})$ from
$((q,p),s)$, where $T_{q,s}$ is the tree generated by ${\mathcal{C}}$ from
$(q,s)$. Indeed, because ${\mathcal{C}}$ is fully convergent from $(q,s)$, for
some $(q^{\prime},t$) we have $(q,s)\to_{\mathcal{C}}^{*}(q^{\prime},t)$ and
$\delta(q^{\prime},\mathit{top}(t))=(a,q_{1},\dots,q_{r})\in\Sigma\times
Q^{*}$. In such a situation
$((q,p),s)\to_{{\mathcal{C}}_{\mathcal{T}}}^{*}((q^{\prime},p),t)$ (where we
use transitions of the first kind). From $((q^{\prime},p),t)$ the CPS
${\mathcal{C}}_{\mathcal{T}}$ uses a transition of the second kind, and then
starts generating the tree $\delta_{\mathcal{T}}(p,a,r)$ until a variable is
reached (using transitions of the third kind). When a variable
$\mathsf{x}_{i,p^{\prime}}$ is reached, ${\mathcal{C}}_{\mathcal{T}}$ enters
the configuration $((q_{i},p^{\prime}),t)$ (a transition of the fourth kind),
which, by the assumption of coinduction, means that it continues by generating
the tree ${\mathcal{T}}_{p^{\prime}}(T_{q_{i},t})$, where $T_{q_{i},t}$ is the
tree generated by ${\mathcal{C}}$ from $(q_{i},t)$.

In particular we have that ${\mathcal{C}}_{\mathcal{T}}$ generates
${\mathcal{T}}(T)$. At the end we translate ${\mathcal{C}}_{\mathcal{T}}$ to a
scheme ${\mathcal{G}}_{\mathcal{T}}$ generating the same tree, using again
Fact 19.