\documentstyle[12pt]{article}
\hfuzz=1pt
\tolerance=1000
\emergencystretch=10pt

\def\BbbR{{\rm I\!R}} %reelle Zahlen
\def\BbbN{{\rm I\!N}} %natuerliche Zahlen
\def\BbbQ{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
\def\BbbZ{{\mathchoice {\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
{\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
{\hbox{$\sf\scriptstyle Z\kern-0.3em Z$}}
{\hbox{$\sf\scriptscriptstyle Z\kern-0.2em Z$}}}}

\begin{document}

\input amssym.def

\centerline{\S4. {\bf The generalization of Shelah -- Stup theorem.}}

A {\it signature\/} is a finite  set  of  predicate  symbols;  each
symbol has its own dimension ($=$ number of arguments).

A  {\it structure\/}  of  signature $\sigma =({\bf P}_{1},\ldots,{\bf P}_{n})$   is   a   tuple
$\langle {\bf D},{\bf {\bar P}}_{1},\ldots{\bf {\bar P}}_{n}\rangle$, where ${\bf D}$ is a non-empty set (the universum  of  the
structure) and ${\bf {\bar P}}_{1},\ldots,{\bf {\bar P}}_{n}$  are  relations  on ${\bf D}$  such  that  the
dimension of ${\bf {\bar P}}_{i}$ equals to the dimension of ${\bf P}_{i}$ for each ${\bf i\le n}$.

Let us define the notion of {\it tree counterpart\/} of a structure
$\langle {\bf D};{\bf {\bar P}}_{1},\ldots,{\bf {\bar P}}_{n}\rangle$. This is a structure of signature ${\bar \sigma }=({\bf P}_{1},\ldots,
{\bf P}_{n},{\bf Q})$
where ${\bf Q}$ is a new binary predicate symbol. Its universum  is  the
set ${\bf D}^{*}$ of all the words over the alphabet ${\bf D}$. Similar to the case
of binary tree, we call ${\bf D}^{*}$ the {\it tree of ${\bf D}$-branching, or the  tree
of branching\/} ${\bf D}$ (e.g., binary  tree  is  the  tree  of  branching
$\{{\bf L},{\bf R}\})$. The elements of ${\bf D}$ are called {\it directions.} Let  us  define
the interpretations ${\bf {\bar {\bar P}}}_{1},\ldots,{\bf {\bar {\bar P}}}_{n},{\bf {\bar {\bar Q}}}$  of predicate symbols ${\bf P}_{1},\ldots,
{\bf P}_{n},{\bf Q}$
in the tree counterpart. The predicate symbol ${\bf Q}$  is  interpreted
as the relation ``to be a son'', i.e., ${\bf {\bar {\bar Q}}}({\bf u},{\bf v})$ is true if ${\bf u}={\bf vd}$  for
some ${\bf d\in D}$. The predicate symbol ${\bf P}_{i}$ is interpreted as the relation
${\bf {\bar {\bar P}}}_{i}$ which is  true  on  a  tuple $\langle {\bf v}_{1},\ldots,
{\bf v}_{k}\rangle$ (where ${\bf k}$  is  the
dimension of ${\bf P}_{i}$) if there exist ${\bf v\in D}^{*}$ and ${\bf d}_{1},\ldots,
{\bf d}_{k}\in {\bf D}$  such  that
${\bf v}_{1}={\bf vd}_{1}$, ${\bf v}_{2}={\bf vd}_{2},\ldots,
{\bf v}_{k}={\bf vd}_{k}$ and ${\bf {\bar P}}_{i}({\bf d}_{1},\ldots,
{\bf d}_{k})$ is  true.  In  other words, ${\bf {\bar {\bar P}}}_{i}({\bf v}_{1},\ldots,
{\bf v}_{k})$ is true if ${\bf v}_{1},\ldots,{\bf v}_{k}$ ``are in the same  fan''
and their last letters satisfy ${\bf {\bar P}}_{i}$.

Let us give the definition  of  the  monadic  theory  of  a
structure. In \S{\bf 1}, this definition was given  for  the  structure
$\langle {\rm binary\ tree;}\ {\bf L},\ {\bf R}\rangle$. Let ${\bf S}=\langle {\bf M};{\bf {\bar P}}_{1},\ldots,
{\bf {\bar P}}_{n}\rangle$  be  a  structure  of
signature $\sigma =({\bf P}_{1},\ldots,{\bf P}_{n})$.  The  monadic  language  contains  both
individual and set variables, its atomic  formulae  are  of  the
form ${\bf x\in Q}$ and ${\bf P}_{i}({\bf x}_{1},\ldots,{\bf x}_{k})$,  where ${\bf x},{\bf x}_{1},\ldots,
{\bf x}_{k}$  are  individual
variables, ${\bf Q}$ is a set variable  and ${\bf P}_{i}$  is a ${\bf k}$-ary  predicate
symbol in $\sigma $. Both individual and set variables can be bounded by
quantifiers in formulae of the language. The monadic theory of ${\bf S}$
consists of all closed formulae of  the  language  true  in  the
structure ${\bf S}$.

Shelah and Stup [?] proved the following generalization
of Rabin's theorem.

\underline{{\bf Theorem of Shelah and Stup.}} {\it If  the  monadic  theory  of  a
structure is decidable, then the  monadic  theory  of  its  tree
counterpart is decidable also.}

Theorem of Rabin is a consequence of Theorem of Shelah  and
Stup, as theory ${\bf S2S}$ is equivalent to the monadic theory  of  the
tree counterpart of the structure $\langle \{{\bf L},{\bf R}\}$; unary relation ``to  be
equal to ${\bf L}$''$\rangle$.

Our goal is to strengthen Theorem of  Shelah  and  Stup  by
enriching the signature of tree counterpart. Let us  include  in
the signature of tree counterpart the unary relation ${\bf {\bar {\bar R}}}({\bf u})$  which
means that ${\bf u}={\bf wdd}$ for some ${\bf w\in D}^{*}$ and ${\bf d\in D}$, i.e., the last letter of
${\bf u}$ and the last but one letter of ${\bf u}$ are  equal.  Thus,  the  tree
counterpart of a structure $\langle {\bf D};{\bf {\bar P}}_{1},\ldots,
{\bf {\bar P}}_{n}\rangle$ in the  new  sense  is
the structure $\langle {\bf D}^{*};{\bf {\bar {\bar P}}}_{1},\ldots,
{\bf {\bar {\bar P}}}_{n},{\bf {\bar {\bar Q}}},{\bf {\bar {\bar R}}}\rangle$ of signature $({\bf P}_{1},\ldots,
{\bf P}_{n},{\bf Q},{\bf R})$.

Note that if ${\bf k}$ is the dimension of ${\bf P}_{i}$,  then,  in  enriched
language, we can express that vertices ${\bf v}_{1},\ldots,
{\bf v}_{k-1}$  are  in  the
same fan and their last letters and their common  last  but  one
letter satisfy ${\bf {\bar P}}_{i}$, as well as other relations of this type.

\underline{{\bf Theorem 6.}} {\it If  the  monadic  theory  of  a   structure   is
decidable, then the monadic theory of its  tree  counterpart  in
the new sense is decidable also.}

Let us mention that this theorem cannot be strengthened  by
means of including in the signature the unary relation ``the last
letter of ${\bf u}$ and the  last  but  two  letter  of ${\bf u}$  are  equal''.
Moreover, we even cannot replace ${\bf {\bar {\bar R}}}$ with this  relation.  Namely,
if the initial structure is ${\bf S}=({\BbbN};<)$, the monadic theory of which
is known to be decidable, and we enrich the tree counterpart  of
${\bf S}$ (in the first sense) by the unary relation  ``the  last  letter
and the last but two letter are equal'', then we get a  structure
with undecidable monadic theory. Indeed, in the  monadic  theory
of the resulting structure we can simulate any  machine,  having
two counters, i.e., for a given machine with  two  counters  and
its input we can construct a monadic formula which  is  true  in
the resulting structure iff the given machine halts on the given
input. It is well known that  machines  with  two  counters  can
simulate Turing machines.

{\it Proof of Theorem} 6. The proof is similar to  our  proof  of
Rabin's theorem.

For every notion used in that proof we give its analog.

A $\Sigma$-tree  of ${\bf D}$-branching (where $\Sigma $ is an  alphabet)  is  any
mapping from ${\bf D}^{*}$ into $\Sigma $. Analogous to the notion of an  automaton
on binary $\Sigma $-trees, we could give the notion of an  automaton  on
$\Sigma $-trees of ${\bf D}$-branching. However, we need a notion  of  automaton
different from  that  natural  generalization.  Namely,  in  the
automaton of the new type, the state  labeling  a  son ${\bf u}$  of  a
vertex ${\bf v}$ can depend not only on automaton state in vertex ${\bf v}$,  on
the label of ${\bf v}$ in the tree and on the last letter of ${\bf u}$ but  also
on the last letter of ${\bf v}$ (if ${\bf v}$ is not empty).  Let  us  give  the
formal definition. Compared with  automata  on  binary $\Sigma $-trees,
only  the notion of a transition and the notion of  a  table  of
transitions are  changed.  Now,  a  {\it transition\/}  is  a  quadruple
$\langle {\bf s},{\bf a},{\bf d},{\bf f}\rangle$, where ${\bf s}$ is a state, ${\bf a\in \Sigma }$, ${\bf d\in D}$ and ${\bf f}$ is a function from
${\bf D}$ into  the set of automaton states. A set ${\bf T}$ of  transitions  is
called  monadic  definable  if  there  is  a   monadic   formula
$\varphi({\bf s},{\bf a},{\bf d},{\bf f})$ such that a transition $\langle {\bf s},{\bf a},{\bf d},{\bf f}\rangle$  belongs  to ${\bf T}$  iff
$\varphi({\bf s},{\bf a},{\bf d},{\bf f})$ is true in ${\bf D}$.

To make this definition meaningful we  enrich  the  monadic
language as follows:

(1) we include variables ranging $\Sigma $ and all elements from $\Sigma $
as constants;

(2) we include variables ranging ${\bf S}$ (the set of states)  and
all elements from ${\bf S}$ as constants;

(3) we include variables ranging the set of functions  from
${\bf D}$ into ${\bf S}$; for any such variable ${\bf f}$, for any individual variable ${\bf x}$
(i.e.\ ranging ${\bf D}$) and for any ${\bf s\in S}$ we allow the expression ${\bf f}({\bf x})={\bf s}$;

(4) we include equality relation;

(5) we allow to bound new variables by quantifiers.

Let us note that if the monadic theory of  a  structure  is
decidable, then the theory of that structure in enriched monadic
language is also decidable, since  given  a  closed  formula  in
enriched monadic language we can construct an equivalent formula
in monadic language.

So, we require the  table  of  transitions  to  be  monadic
definable.

As earlier, let us call a {\it transition  of  automaton  ${\frak A}$}  any
transition in the table of transitions of  ${\frak A}$.  Let  us  call  an
automaton ${\frak A}$  {\it correct\/} if its transitions having the initial  state
${\bf s}_{0}$ at the bottom don't depend on  the  last  letter  of  vertex,
i.e., if for all ${\bf a\in \Sigma},\ {\bf d},{\bf d'\in D}$ and ${\bf f}\colon\,{\bf D}\longrightarrow {\bf S}$,\\
$\langle {\bf s}_{0},{\bf a},{\bf d},{\bf f}\rangle$ is a transition of ${\frak A}$ $\Longleftrightarrow$ $\langle {\bf s}_{0},{\bf a},{\bf d'},{\bf f}\rangle$ is a  transition
of ${\frak A}$.

For a labelled tree ${\bf G}$ and for a vertex ${\bf x}$, we denote by ${\bf G}({\bf x})$
the label of ${\bf x}$ in ${\bf G}$. Let us define the notion  of  a  run  of  a
correct automaton ${\frak A}$  on a $\Sigma$-tree ${\bf T}$  of ${\bf D}$-branching.  This  is a
${\bf S}$-tree ${\bf H}$ of ${\bf D}$-branching such that

1) ${\bf H}(\lambda)={\bf s}_{0}$;

2) for any ${\bf x\in D}^{*}$, the transition $\langle {\bf H}({\bf x}),{\bf T}({\bf x}),{\bf d},{\bf f}\rangle$ belongs  to
the table of transitions of ${\frak A}$, where ${\bf d}$  and ${\bf f}$  are  defined  as
follows: ${\bf d}$ is the last letter of ${\bf x}$ (and any element of ${\bf D}$ if ${\bf x}=\lambda$)
and ${\bf f}$ is the function from ${\bf D}$ into ${\bf S}$ such that ${\bf f}({\bf d'})={\bf H}({\bf xd'})$;  the
transition $\langle {\bf H}({\bf x}),{\bf T}({\bf x}),{\bf d},{\bf f}\rangle$ is called the {\it transition of\/} ${\bf H}$ {\it in\/} ${\bf x}$
(when ${\bf T}$ is clear from the context).

Now, similar to the case of binary tree, we have  to  prove
that any monadic definable set of $\Sigma$-trees of ${\bf D}$-branching can  be
recognized by a correct automaton on $\Sigma $-trees of ${\bf D}$-branching. The
proof runs as the proof of Theorem~1. As it  was  earlier,  only
one point is nontrivial: to prove that  the  complement  of  any
recognizable set of $\Sigma $-trees of ${\bf D}$-branching is recognizable.

A correct semiautomaton on $\Sigma $-trees of ${\bf D}$-branching is a pair
$\langle$a  correct  automation  ${\frak L}$   on $\Sigma $-trees   of ${\bf D}$-branching;   a
(nondeterministic) automaton ${\frak B}$  on $\omega $-words over the  set  of  ${\frak L}$'s
states$\rangle$. The semiautomation accepts a $\Sigma$-tree ${\bf T}$ of ${\bf D}$-branching if
there is a run of ${\frak L}$  on ${\bf T}$ such that  all  the  sequences  of  ${\frak L}$'s
states lying along infinite paths in that run are rejected by ${\frak B}$.

Let us prove first that the complement of any  recognizable
(by a correct  automaton)  set  of $\Sigma $-trees  of ${\bf D}$-branching  is
recognizable by a correct semiautomaton.  Again  we  define  the
notion of a strategy with memory. The only difference  with  old
definition is that now the strategy distributes all possible (in
a vertex) copy-transitions among elements  of ${\bf D}$  and  does  not
divide them into left and right. The  analog  of  Theorem~4  is
proved in the similar way. The only  difficulty  arises  in  the
proof of the analog of Theorem~5, i.e., in the  proof  that  for
any correct automaton ${\frak A}$  and for any strategy set ${\bf M}$, the  set  of
$\Sigma $-trees of ${\bf D}$-branching on which there is  a  rejecting  strategy
for ${\frak A}$  based on ${\bf M}$, is semirecognizable. Let us present the  proof
of this statement in detail. To understand the following better,
we advise the reader to recall the notions of  a  strategy  with
memory, of a strategy set and of a probable path.

Let us remind  that  in  binary  case  the  states  of  the
semiautomaton recognizing the set of $\Sigma $-trees on which there is a
rejecting   strategy,   were   pairs   of   disjoint   sets   of
copy-transitions of the initial automaton. In our case, if ${\bf D}$  is
infinite, then the number of such pairs is infinite.  Therefore,
we have to take another semiautomaton. Let us define  its  first
component ${\frak L}$  (a correct automaton on $\Sigma $-trees of ${\bf D}$-branching). The
states of ${\frak L}$  are subsets of ${\bf M\times M}$ (recall that ${\bf M}$  is  the  strategy
set). The initial state is the set $\left\{{\langle {\bf m}_{0},{\bf m}_{0}}\rangle\right\}$, where ${\bf m}_{0}$  is  the
initial copy of initial state of automaton ${\frak A}$. Let us define  the
table of transitions of ${\frak L}$. Let $\langle {\bf A},{\bf a},{\bf d},{\bf F}\rangle$ be a transition,  where
${\bf A\subset M\times M}$, ${\bf a\in \Sigma}$, ${\bf d\in D}$, and ${\bf F}\colon\,{\bf D}\longrightarrow {\bf P}({\bf M\times M})$. Let us define in  what  case
it belongs to the table of transitions. Let ${\bf G}$ be a function from
${\bf M\times \Sigma \times D\times S}^{{\bf D}}$ into ${\bf D}$ (the meaning is that ${\bf G}$ attaches a  direction  to
every copy-transition). Denote by ${\bf G}_{{\bf A},{\bf a},{\bf d}}$ the following  function
from ${\bf D}$ into ${\bf P}({\bf M\times M})$. Its value on ${\bf d'\in D}$  consists  of  all  pairs
$\langle {\bf m},{\bf f}({\bf d'})\rangle$ such that $\langle {\bf m},{\bf a},{\bf d},{\bf f}\rangle$ is a transition  of  ${\frak A}$   for  which
${\bf G}(\langle {\bf m},{\bf a},{\bf d},{\bf f}\rangle)={\bf d'}$ and ${\bf m}$ belongs to the second projection of ${\bf A}$.

Formally, ${\bf G}_{{\bf A},{\bf a},{\bf d}}({\bf d'})=\Bigl\{\langle {\bf m},{\bf f}({\bf d'})\rangle\mid \langle {\bf m},{\bf a},{\bf d},{\bf f}\rangle$    is     a
transition of ${\frak A}$, ${\bf G}(\langle {\bf m},{\bf a},{\bf d},{\bf f}\rangle)={\bf d'}$ and there  is ${\bf m'\in M}$  such  that
$\langle {\bf m'},{\bf m\rangle\in A}\Bigr\}$.

So, a quadruple $\langle {\bf A},{\bf a},{\bf d},{\bf F}\rangle$ is a transition of ${\frak L}$  if there  is
a function ${\bf G}$ such that ${\bf G}_{{\bf A},{\bf a},{\bf d}}({\bf d'})\subseteq {\bf F}({\bf d'})$ for all ${\bf d'\in D}$.
Clearly, ${\frak L}$ is correct.

Let us prove that the property of a quadruple $\langle {\bf A},{\bf a},{\bf d},{\bf F}\rangle$ ``to
be a transition of ${\frak L}$'' is monadic definable. Indeed,
this property can be expressed by  the  formula $\varphi({\bf A},{\bf a},{\bf d},{\bf F})$
which states that for every copy-transition of  ${\frak A}$   of  the  form
$\langle {\bf m},{\bf a},{\bf d},{\bf f}\rangle$, where ${\bf m}$ belongs to the second projection of ${\bf A}$,  there
is a ${\bf d'\in D}$ such that the pair $\langle {\bf m},{\bf f}({\bf d'})\rangle$ belongs to ${\bf F}({\bf d'})$.

Let us construct the second component of the semiautomaton,
i.e., the automaton ${\frak B}$  on $\omega$-words over the set of  states  of  ${\frak L}$.
Let us define when ${\frak B}$  accepts a sequence $\alpha=({\bf A}_{0},{\bf A}_{1},\ldots,
{\bf A}_{k},\ldots)$  of
states of ${\frak L}$. Let us call a sequence ${\bf s}_{0},{\bf s}_{1},\ldots,
{\bf s}_{k},\ldots$  of  states
of ${\frak A}$ {\it possible for\/} $\alpha$ if there exist  copies ${\bf m}_{0},{\bf m}_{1},\ldots,
{\bf m}_{k},\ldots$  of
the states ${\bf s}_{0},{\bf s}_{1},\ldots,{\bf s}_{k},\ldots$,
respectively, such that $\langle {\bf m}_{0},{\bf m}_{1}\rangle\in {\bf A}_{1}$,
$\langle {\bf m}_{1},{\bf m}_{2}\rangle\in {\bf A}_{2},\ldots,
\langle {\bf m}_{k-1},{\bf m}_{k}\rangle\in {\bf A}_{k},\ldots$.
So, ${\frak B}$  accepts $\alpha $ if there  is  a
sequence ${\bf s}_{0},{\bf s}_{1},\ldots,{\bf s}_{k},\ldots$
having final limit macrostate which is
possible for $\alpha$. It is easy to construct an automaton on $\omega $-words
satisfying this requirement.

Let us prove  that  the  defined  semiautomaton  accepts a
$\Sigma $-tree ${\bf T}$ of ${\bf D}$-branching iff there is a rejecting strategy  based
on ${\bf M}$ for ${\frak A}$  on ${\bf T}$. Assume that there is a rejecting strategy based
on ${\bf M}$ for ${\frak A}$  on a $\Sigma $-tree ${\bf T}$  of ${\bf D}$-branching.  Let  us  define  the
following run of the semiautomaton on ${\bf T}$: in every vertex ${\bf x}$, take
the transition $\langle {\bf A},{\bf a},{\bf d},{\bf G}_{{\bf A},{\bf a},{\bf d}}\rangle$ where ${\bf d}$ is the last letter of ${\bf x}$, ${\bf a}$
is the label of ${\bf x}$ and ${\bf G}$ is the function  from ${\bf M\times \Sigma \times D\times S}^{{\bf D}}$  into ${\bf D}$
indicating    how    the    rejecting    strategy    distributes
copy-transitions possible in ${\bf x}$ among directions  (on  impossible
in ${\bf x}$ copy-transitions ${\bf G}$ is defined in any way).  Obviously,  any
sequence ${\bf s}_{0},{\bf s}_{1},\ldots,{\bf s}_{k},\ldots$
that  is  possible  for  a  sequence
${\bf A}_{0},{\bf A}_{1},\ldots,{\bf A}_{k},\ldots$ of states of the semiautomaton lying  along  an
infinite path in this run, is a probable path of  the  rejecting
strategy and therefore has non-final  limit  macrostate.  Hence,
the defined run is an accepting run.

Conversely,  if  there  is  an  accepting  run ${\bf H}$  of   the
semiautomaton on a $\Sigma $-tree  of ${\bf D}$-branching,  then  there  is  a
rejecting strategy on that tree (in a vertex ${\bf x}$,  the  rejecting
strategy distributes transitions among directions  according  to
the function ${\bf G}$ for which $\forall {\bf d'\ G}_{{\bf A},{\bf a},{\bf d}}({\bf d'})\subseteq {\bf F}({\bf d'})$,  where $\langle {\bf A},{\bf a},{\bf d},{\bf F}\rangle$
is the transition of ${\bf H}$ in ${\bf x}$).

Just as it was done in Theorem 1, we can prove that any set
recognizable  by  a  correct   semiautomaton   on $\Sigma $-trees   of
${\bf D}$-branching is recognizable by a correct automaton on $\Sigma $-trees of
${\bf D}$-branching.

Thus, we have completed the proof of the analog of  Theorem~1.
To complete the proof of Theorem~6 we have  to  construct  an
algorithm deciding whether a correct automaton ${\frak A}$  on $\Sigma $-trees  of
${\bf D}$-branching recognizes the empty set,  where $\Sigma $  consists  of  a
single letter.  There  is  unique $\Sigma $-tree  of ${\bf D}$-branching  (for
one-element $\Sigma$), call it simply the  {\it tree of\/} ${\bf D}$-{\it branching}; we  may
think, that its vertices have no labels. Therefore we may delete
the second  component  from  transitions  of  ${\frak A}$.  The  algorithm
recognizing emptiness is more complicated compared  with  binary
case. We are going to construct it.

Let  us  consider  arbitrary  automata  on  the   tree   of
${\bf D}$-branching (not only correct ones). Moreover, let  us  consider
automata with dead ends from a set $\Delta $, which are defined in usual
way. Let ${\bf d}_{0}$ be a direction. Let us define the notion of a ${\bf d}_{0}$-run
of an automaton  with  dead  ends  from $\Delta $  on a ${\bf P}(\Delta)$-tree  of
${\bf D}$-branching. Informally speaking, a ${\bf d}_{0}$-run is  an  ordinary  run
of the automaton with dead  ends  on ${\bf P}(\Delta )$-tree  of ${\bf D}$-branching
provided the last letter of the empty word is defined to be ${\bf d}_{0}$.
Formally, a ${\bf d}_{0}$-run of an automaton ${\frak A}$  with dead ends from $\Delta $ on a
${\bf P}(\Delta)$-tree of ${\bf D}$-branching  is  any  subtree ${\bf H}$  of  the  tree ${\bf D}^{*}$
labelled by letters from ${\bf S\bigcup \Delta}$ (where ${\bf S}$ is the set of states  of
${\frak A}$) such that

(1) ${\bf H}(\lambda)$ is the initial state (recall that ${\bf H}({\bf x})$ denotes the
label of vertex ${\bf x}$ in ${\bf H}$);

(2) if ${\bf x}$ is a vertex such that ${\bf H}({\bf x})\in {\bf S}$, then the  vertex ${\bf xd}$
is in ${\bf H}$ for any ${\bf d\in D}$ and the triple $\langle {\bf H}({\bf x}),{\bf d'},{\bf f}\rangle$ is  a  transition
of ${\bf H}$, where ${\bf d'}={\bf d}_{0}$ if ${\bf x}=\lambda $  and ${\bf d'}$  is  the  last  letter  of ${\bf x}$
otherwise and ${\bf f}({\bf d})={\bf H}({\bf xd})$ for all ${\bf d\in D}$;

(3) if ${\bf x}$ is a vertex  such  that ${\bf H}({\bf x})\in \Delta $,  then ${\bf x}$  has  no
descendants in ${\bf H}$.

The notion of an accepting ${\bf d}_{0}$-path is  defined  similar  to
the binary case. Let us say that an  automaton  ${\frak A}$  ${\bf d}_{0}$-{\it accepts\/}  a
tree if there is an accepting ${\bf d}_{0}$-run of ${\frak A}$  on that tree.

A {\it simple\/} ${\bf P}(\Delta )$-tree is any ${\bf P}(\Delta )$-tree  of ${\bf D}$-branching  such
that for any vertex ${\bf x}$, the label of ${\bf x}$ depends only on  the  last
letter of ${\bf x}$ (if ${\bf x}$ is not the root) and the root of the  tree  is
labelled by the empty set. Obviously, every function from ${\bf D}$ into
${\bf P}(\Delta)$ uniquely defines a simple ${\bf P}(\Delta )$-tree.

For any given automaton ${\frak A}$  with dead ends,  we  construct  a
monadic formula $\varphi({\bf g},{\bf d})$ in the  language  of ${\bf D}$,  where ${\bf d\in D}$  and
${\bf g}\colon\,{\bf D}\longrightarrow {\bf P}(\Delta )$, which is true in ${\bf D}$  iff  ${\frak A}$  ${\bf d}$-accepts  the  simple
${\bf P}(\Delta )$-tree defined by ${\bf g}$. Assume that this is already  done.  Then
to decide whether the  given  correct  automaton  (without  dead
ends) accepts the tree  of ${\bf D}$-branching  we  can  construct  the
formula $\varphi({\bf g},{\bf d})$  for  that  automaton,  substitute  the  function
${\bf f}({\bf d})\equiv \emptyset$ for ${\bf g}$ and any direction for ${\bf d}$ and then decide whether the
resulting formula is true (making use of decidability of monadic
theory of ${\bf D}$).

So let us  start  with  the  construction  of  the  formula
$\varphi({\bf g},{\bf d})$. Let ${\bf h}$ be a function from ${\bf D}$ into ${\bf P}(\Delta \bigcup {\bf S})$ and let ${\bf g}$ be  a
function  from ${\bf D}$  into ${\bf P}(\Delta)$.  Say  that ${\bf h}$   {\it extends\/} ${\bf g}$   if
${\bf h}({\bf d})\bigcap \Delta ={\bf g}({\bf d})$ for all ${\bf d\in D}$.

We use the induction on the number of states.

Consider the case of an automaton ${\frak A}$   having  single  state.
Denote that state by ${\bf s}$. Consider two subcases.

\underline{{\bf First subcase:}} the macrostate $\{{\bf s}\}$ is not final.

Say that a function ${\bf h}$ from ${\bf D}$ into ${\bf P}(\Delta \bigcup \{{\bf s}\})$  is  {\it downward
closed\/} if ${\bf s\in h}({\bf d})$ for each ${\bf d\in D}$ such that there  is  a  transition
$\langle {\bf s},{\bf d},{\bf f}\rangle$ of ${\frak A}$  for which $\forall {\bf d'\in D\  f}({\bf d'})\in {\bf h}({\bf d'})$.

\underline{{\bf Lemma 6.}} {\it The  following  conditions  are equivalent.}

(1) {\it The automaton ${\frak A}$  ${\bf d}_{0}$-accepts the simple ${\bf P}(\Delta )$-tree defined
by the function ${\bf g}$.}

(2) {\it ${\bf s\in h}({\bf d}_{0})$ for any function ${\bf h}$ which is downward closed and
extends ${\bf g}$.}

{\it Proof.} Let us prove first that (2) involves (1). Let (2) be
fulfilled.
$$
{\rm Set}\ {\bf h}({\bf d})=\cases{{\bf g}({\bf d})\bigcup \{{\bf s}\}\quad {\rm if}\ {\frak A}\ {\bf d}-{\rm accepts\ the\ simple\ tree}\cr
\phantom{aaaaaaaaaa}{\rm defined\ by}\ {\bf g};\cr {\bf g}({\bf d})\qquad {\rm else.}}
$$

Obviously, ${\bf h}$ extends ${\bf g}$ and ${\bf h}$ is downward closed,  therefore
${\bf s\in h}({\bf d}_{0})$, i.e., ${\frak A}$  ${\bf d}_{0}$-accepts the simple tree defined by ${\bf g}$.

Conversely, let (2) be false, that is, there is a  downward
closed function ${\bf h}$ extending ${\bf g}$ for which ${\bf s\notin h}({\bf d}_{0})$.  Let  us  prove
that any ${\bf d}_{0}$-run of ${\frak A}$  on the simple tree  defined  by ${\bf g}$  has  an
infinite path or a finite path ending in a non-allowed dead end.

For any ${\bf x\in D}^{*}$, let us define
$$
{\bf l}({\bf x})=\cases{{\rm the\ last\ letter\ of}\ {\bf x}\quad {\rm if}\ {\bf x\neq \lambda},\cr
{\bf d}_{0}\quad {\rm if}\ {\bf x}=\lambda.}
$$
Let ${\bf H}$ be a ${\bf d}_{0}$-run of ${\frak A}$  on the simple tree defined  by ${\bf g}$.  Using
the induction on {\bf i}, we define the path ${\bf x}_{0}=\lambda,\,{\bf x}_{1},\ldots,
{\bf x}_{i},\ldots$  such
that ${\bf H}({\bf x}_{i})\notin {\bf h}({\bf l}({\bf x}_{i}))$   for   all ${\bf i}$.   For   ${\bf i}=0$    we    have
${\bf H}({\bf x}_{0})={\bf H}(\lambda)={\bf s\notin h}({\bf l}(\lambda))={\bf h}({\bf d}_{0})$. Let ${\bf x}_{0},{\bf x}_{1},\ldots,
{\bf x}_{i}$ have already been
defined and ${\bf H}({\bf x}_{i})\notin {\bf h}({\bf l}({\bf x}_{i}))$. If ${\bf H}({\bf x}_{i})$ is a dead  end,  then  that
dead end is not allowed as ${\bf h}$ extends ${\bf g}$. In this case the desired
path is already constructed. Otherwise (when ${\bf H}({\bf x}_{i})={\bf s}$)  we  have
${\bf s\notin h}({\bf l}({\bf x}_{i}))$. As ${\bf h}$ is downward closed, there is a ${\bf d'\in D}$  such  that
${\bf H}({\bf x}_{i}{\bf d'})\notin {\bf h}({\bf d'})$. Set ${\bf x}_{i+1}={\bf x}_{i}{\bf d'}$. Lemma 6 is proved.

Obviously, the property of a function ${\bf g}$ and of an element ${\bf d}$
stated in item~(2) of Lemma~6 is  monadic  definable,  thus  the
first subcase is completed.

\underline{{\bf Second subcase:}} the macrostate $\{{\bf s}\}$ is final.

Let us call a function ${\bf h}\colon\,{\bf D}\longrightarrow {\bf P}(\Delta \bigcup \{{\bf s}\})$ {\it upward  closed\/}  if
${{\bf s\in h}({\bf d})}$ implies that there is a transition ${\langle {\bf s},{\bf d},{\bf f}\rangle}$ of ${\frak A}$  such that
${\forall {\bf d'\in D},\ {\bf f}({\bf d'})\in {\bf h}({\bf d'})}$.
{\hfuzz=2pt \tolerance=9999 \emergencystretch=20pt

}
Now we need the following

\underline{{\bf Lemma 7.}} {\it The following assertions are equivalent.}

(1) {\it The automaton ${\frak A}$  ${\bf d}_{0}$-accepts the simple ${\bf P}(\Delta )$-tree defined
by the function ${\bf g}$.}

(2) {\it ${\bf s\in h}({\bf d}_{0})$ for some function ${\bf h}$ which is upward closed  and
extends ${\bf g}$.}

{\it Proof.} Assume that (1) is true. Let us prove  that~(2)  is
true. Let us fix an accepting ${\bf d}_{0}$-run ${\bf H}$  of  ${\frak A}$   on  the  simple
${\bf P}(\Delta )$-tree defined by ${\bf g}$. Define the function ${\bf l}({\bf x})$ just as it  was
done in Lemma~6.\\
Set
$$
{\bf h}({\bf d})=\cases{\{{\bf s}\}\bigcup {\bf g}({\bf d})\quad {\rm if\  there\ is}\ {\bf x\in D}^{*}\ {\rm such\ that}\ {\bf d}={\bf l}({\bf x})\ {\rm and}\ {\bf H}({\bf x})={\bf s},\cr
{\bf g}({\bf d})\qquad {\rm else.}}
$$
Obviously, ${\bf h}$ extends ${\bf g}$, ${\bf h}$ is upward closed and ${\bf s\in h}({\bf d}_{0})$.

Conversely, let ${\bf s}$  be  in ${\bf h}({\bf d}_{0})$  for  some  upward  closed
function ${\bf h}$ extending ${\bf g}$. Let us construct an accepting ${\bf d}_{0}$-run ${\bf H}$
of ${\frak A}$  on the simple tree defined by ${\bf g}$. For every vertex ${\bf x\in D}^{*}$, let
us define whether ${\bf x}$ belongs to ${\bf H}$ and if this is  the  case  then
let us define the label of ${\bf x}$. This will be done by induction  on
the length of ${\bf x}$ in such a way that the label  of ${\bf x}$  belongs  to
${\bf h}({\bf l}({\bf x}))$.

Base of induction:  the  root ${\bf x}=\lambda $  belongs  to ${\bf H}$  and  is
labelled by ${\bf s}$.

Induction step. Assume that for any vertex ${\bf x}$ of length  not
exceeding ${\bf n}$, we have made our decision in such a  way  that  the
label of ${\bf x}$ belongs to ${\bf h}({\bf l}({\bf x}))$. Let ${\bf x}$ be a vertex of length ${\bf n}$. If
${\bf x}$ doesn't belong to ${\bf H}$ or ${\bf x}$ is labelled by a dead end,  then  all
the sons of ${\bf x}$ don't belong to ${\bf H}$. Assume that ${\bf x}$ is labelled by ${\bf s}$.
Since ${\bf s\in h}({\bf l}({\bf x}))$ and ${\bf h}$ is upward closed, there  is  a  transition
$\langle {\bf s},{\bf l}({\bf x}),{\bf f}\rangle$ of ${\frak A}$  such that $\forall {\bf d'\in D}\ {\bf f}({\bf d'})\in {\bf h}({\bf d'})$.  Include  all  the
sons of ${\bf x}$ in ${\bf H}$ and label the son ${\bf xd'}$ by ${\bf f}({\bf d'})$.

Thus, the run ${\bf H}$ is  defined.  All  its  finite  paths  have
allowed dead ends because if ${\bf x}$ is a leaf of ${\bf H}$, then the label of
${\bf x}$ is a dead end from ${\bf g}({\bf l}({\bf x}))$ (as ${\bf h}$ extends ${\bf g}$). As the macrostate
$\{{\bf s}\}$  is  final,  all  infinite  paths  in ${\bf H}$  have  final  limit
macrostate, therefore, the run ${\bf H}$ is an accepting run. Lemma 7 is proved.

Obviously, the property of a function ${\bf g}$ and of an element ${\bf d}$
stated in item~(2) of Lemma~7 is  monadic  definable,  therefore
the case of an automaton with unique state is completed.

Let us turn to automata having more than one state. Let  an
automaton ${\frak A}$  have ${\bf n}$ states $0,1,\ldots,{\bf n}-1$ and let 0 be  the  initial
state. Let $\Delta $ be  the  set  of  dead  ends  of  ${\frak A}$.  Consider  two
subcases.

\underline{{\bf First subcase:}} the macrostate ${\bf S}=\{0,1,\ldots,{\bf n}-1\}$ is not final.
We use the automaton ${\frak B}_{i}$, where ${\bf i\in S}$,  introduced  in  \S2.  Recall
that the set of states of ${\frak B}_{i}$ is ${\bf S}\setminus \{{\bf i}+1\}$, where the  addition  is
modulo ${\bf n}$, the  initial  state  of  ${\frak B}_{i}$  is  ${\bf i}$;  ${\frak B}_{i}$  has  all  the
transitions of ${\frak A}$  except for those having $({\bf i}+1)$  on  the  bottom,
the  set  of  dead  ends  of  ${\frak B}_{i}$  is $\Delta \bigcup ({\bf i}+1)$;  finally,   the
macrostates of ${\frak B}_{i}$ are obtained from macrostates of ${\frak A}$  by deleting
$({\bf i}+1)$.

Let us say that a function ${\bf h}$  from ${\bf D}$   into ${\bf P}({\bf S\bigcup \Delta })$  is
{\it downward closed\/} if ${\bf i\in h}({\bf d})$ for any ${\bf i\in S}$ and for any ${\bf d\in D}$ such  that
${\frak B}_{i}$ ${\bf d}$-accepts  the  simple ${\bf P}(\Delta \bigcup \{{\bf i}+1\})$-tree  defined  by   the
function ${\bf h}_{i}({\bf d'})={\bf h}({\bf d'})\bigcap (\Delta \bigcup \{{\bf i}+1\})$.

\underline{{\bf Lemma 8.}} {\it The following assertions are equivalent.}

(1) {\it The automaton ${\frak A}$  ${\bf d}_{0}$-accepts the simple ${\bf P}(\Delta )$-tree defined
by ${\bf g}$.}

(2) {\it $0\in {\bf h}({\bf d}_{0})$ for any downward closed function ${\bf h}$ extending ${\bf g}$.}

{\it Proof.} Assume that (2) is true. Let us prove  that~(1)  is
true. Define ${\frak A}_{i}$ to be the automaton obtained from ${\frak A}$  by declaring
${\bf i}$ to be the (single) initial state. Set\\
${\bf h}({\bf d})={\bf g}({\bf d})\bigcup \bigl\{{\bf i\in S}\mid {\frak A}_{i}$ ${\bf d}$-accepts the simple tree defined by ${\bf g}\bigr\}$.

Obviously ${\bf h}$  extends ${\bf g}$  and  is  downward  closed.  Hence
$0\in {\bf h}({\bf d}_{0})$, that is, the automaton  ${\frak A}_{0}={\frak A}$ ${\bf d}_{0}$-accepts  the  simple
tree defined by ${\bf g}$.

Conversely, assume that there is a downward closed function
${\bf h}$ extending ${\bf g}$ such that $0\notin {\bf h}({\bf d}_{0})$. Let us prove that~(1) is false.
Let us define the function ${\bf l}({\bf x})$ just as it was done in the proof
of Lemma~6. Let ${\bf H}$ be an arbitrary ${\bf d}_{0}$-run of ${\frak A}$  on the simple tree
defined by ${\bf g}$. Let us prove that ${\bf H}$ has an  infinite  path  having
non-final limit macrostate or a finite path with  a  non-allowed
dead end. We construct that path step by step; on each  step  we
add a finite or an infinite continuation to existing path.

Denote by ${\bf P}_{j}$ (finite or infinite)  path  obtained  on ${\bf j}$-th
step. On ${\bf j}$-th step we want to satisfy  one  of  three  following
conditions:

(1) ${\bf P}_{j}$ is infinite and has non-final limit  macrostate;  in
this case the construction in completed;

(2) ${\bf P}_{j}$ is finite and its last vertex ${\bf x}_{j}$ is labelled in ${\bf H}$ by
a non-allowed  dead  end;  in  this  case  the  construction  is
completed also;

(3) ${\bf P}_{j}$ is finite and its last vertex ${\bf x}_{j}$ is labelled by  the
state ${\bf i}$, where ${\bf i}=({\bf j}\bmod {\bf n})$, and ${\bf i\notin h}({\bf l}({\bf x}_{j}))$.

At the start ${\bf x}_{0}=\lambda $ and ${\bf H}({\bf x}_{0})={\bf H}(\lambda )=0\notin {\bf h}({\bf d}_{0})$,  thus  for ${\bf j}=0$
third alternative holds.

Assume now that the step ${\bf j}$ is made and that  assertion~(3)
is true. Denote by ${\bf x}_{j}$ the last vertex of ${\bf P}_{j}$ and  by ${\bf i}=({\bf j}\bmod {\bf n})$
its label in ${\bf H}$. As ${\bf i\notin h}({\bf l}({\bf x}_{j}))$ and ${\bf h}$  is  downward  closed,  the
automaton ${\frak B}_{i}$ doesn't ${\bf l}({\bf x}_{j})$-accept the  simple ${\bf P}(\Delta \bigcup \{{\bf i}+1\})$-tree
defined  by  the  function ${\bf h}_{i}({\bf d'})={\bf h}({\bf d'})\bigcap (\Delta \bigcup \{{\bf i}+1\})$.  Let  us
define a subtree ${\bf H'}$ of  the  tree  of ${\bf D}$-branching  labelled  by
elements of ${\bf S}$. The tree ${\bf H'}$ consists of all the vertices ${\bf y}$  such
that no proper prefix of the word ${\bf x}_{j}{\bf y}$ is labelled by ${\bf i}+1$ in ${\bf H}$. A
vertex ${\bf y}$ has in ${\bf H'}$ the label equal to the label of ${\bf x}_{j}{\bf y}$ in ${\bf H}$.  It
is easy to verify that ${\bf H'}$ is a ${\bf l}({\bf x}_{j})$-run of  ${\frak B}_{i}$  on  the  simple
${\bf P}(\Delta \bigcup \{{\bf i}+1\})$-tree defined by ${\bf h}_{i}$. We  know  that ${\bf H'}$  is  not  an
accepting run. Hence, there is a finite path ${\bf S'}$ in ${\bf H'}$ ending  in
a vertex ${\bf y}$ such that ${\bf H'}({\bf y})\in \Delta \bigcup \{{\bf i}+1\}\setminus {\bf h}_{i}({\bf l}({\bf y}))$ or  an  infinite
path ${\bf S'}$ in ${\bf H'}$ having non-final limit macrostate. In the first  case
either ${\bf H'}({\bf y})\in \Delta \setminus {\bf g}({\bf l}({\bf y}))$, or ${\bf H'}({\bf y})={\bf i}+1\notin {\bf h}({\bf l}({\bf y}))$. Thus, in this
case we can define the last vertex of the new path ${\bf P}_{j+1}$ to
be ${\bf x}_{j}{\bf y}$. In the second case the path ${\bf x}_{j}{\bf S'}$ is infinite path in ${\bf H}$
having non-final limit macrostate.

The construction of the path is completed.  It  remains  to
note that if we have made infinitely many steps then  the  limit
macrostate of the defined path is equal to ${\bf S}$ and ${\bf S}$ is  non-final
macrostate. Lemma 8 is proved.

By induction hypothesis, for each ${\bf i\in S}$ there  is  a  formula
$\varphi_{i}({\bf h}_{i},{\bf d})$  which  is   true   iff   ${\frak B}_{i}$ ${\bf d}$-accepts   the   simple
${\bf P}(\Delta \bigcup \{{\bf i}+1\})$-tree defined by ${\bf h}_{i}$. Thus, the property of ${\bf h}$  to  be
downward closed is monadic definable, therefore, the property of
${\bf g}$ and ${\bf d}_{0}$ stated in item~(2) of Lemma~8 is monadic definable.

\underline{{\bf Second subcase:}} The macrostate ${\bf S}$ is final.

Let us call a function ${\bf h}\colon\,{\bf D}\longrightarrow {\bf P}(\Delta \bigcup {\bf S})$ {\it upward closed\/} if  ${\frak B}_{i}$
${\bf d}_{0}$-accepts the simple ${\bf P}(\Delta \bigcup \{{\bf i}+1\})$-tree defined by the  function
${{\bf h}_{i}({\bf d'})={\bf h}({\bf d'})\bigcap (\Delta \bigcup \{{\bf i}+1\})}$ for any ${\bf i\in S}$ and  for  any ${{\bf d}_{0}\in {\bf D}}$  such
that ${{\bf i\in h}({\bf d}_{0})}$.
{\hfuzz=2pt \tolerance=9999 \emergencystretch=20pt

}
\underline{{\bf Lemma 9.}} {\it The following assertions are equivalent.}

(1) {\it The automaton ${\frak A}$  ${\bf d}_{0}$-accepts the simple ${\bf P}(\Delta )$-tree defined
by ${\bf g}$.}

(2) {\it There is an upward closed function ${\bf h}$ extending ${\bf g}$  such
that $0\in {\bf h}({\bf d}_{0})$.}

{\it Proof.} Assume that (1) is true. Let us prove  that~(2)  is
true. Let us fix an accepting ${\bf d}_{0}$-run  of ${\frak A}$  on  the  simple  tree
defined by ${\bf g}$. Set ${{\bf h}({\bf d})=\Bigl\{{\bf H}({\bf x})\mid {\bf l}({\bf x})={\bf d}\Bigr\}\bigcup {\bf g}({\bf d})}$,  where ${\bf l}({\bf x})$  is
defined just as it was done in Lemma~6. It  is  easy  to  verify
that ${\bf h}$ is upward closed, extends ${\bf g}$ and ${0\in {\bf h}({\bf d}_{0})}$.
{\hfuzz=2pt \tolerance=9999 \emergencystretch=20pt

}
Conversely, assume that there is an upward closed  function
${\bf h}$ extending ${\bf g}$ such that $0\in {\bf h}({\bf d}_{0})$.  Let  us  define  an  accepting
${\bf d}_{0}$-run of ${\frak A}$  on the simple tree defined by ${\bf g}$. As $0\in {\bf h}({\bf d}_{0})$ and ${\bf h}$ is
upward closed, there is an accepting ${\bf d}_{0}$-run ${\bf H}_{0}$  of  ${\frak B}_{0}$  on  the
simple tree defined by ${\bf h}_{0}$.

Obviously ${\bf H}_{0}$ is also a ${\bf d}_{0}$-run of ${\frak A}$  on the simple ${\bf P}(\Delta )$-tree
defined by ${\bf g}$. The ${\bf d}_{0}$-run ${\bf H}_{0}$ is not an accepting ${\bf d}_{0}$-run of ${\frak A}$  only
if some its leaves are labelled by~1.

For every vertex ${\bf x}$  in ${\bf H}_{0}$  labelled  by  1  we  make  the
following.  We  know  that $1\in {\bf h}({\bf l}({\bf x}))$.  Therefore  there  is  an
accepting ${\bf l}({\bf x})$-run ${\bf H}_{1}$ of ${\frak B}_{1}$ on the simple tree  defined  by ${\bf h}_{1}$.
Let us glue to ${\bf x}$ the labelled tree ${\bf H}_{1}$.

The resulting labelled tree may be regarded as a ${\bf d}_{0}$-run  of
${\frak A}$  on the simple tree defined by ${\bf g}$. This tree is not an accepting
${\bf d}_{0}$-run only if some its leaves are labelled by 2. We repeat  the
above actions and so on. After $\omega $ steps we obtain a ${\bf d}_{0}$-run  of  ${\frak A}$
on the simple tree defined by ${\bf g}$. Any dead end  in  that  run  is
allowed. Every infinite path in that run either from some  place
comes into an accepting run of ${\frak B}_{i}$ (for some ${\bf i\in S}$),  or  for  each
${\bf i\in S}$ has infinitely many occurrences of ${\bf i}$ and therefore has final
limit macrostate. Lemma 9 is proved.

It remains to note that the property of ${\bf d}_{0}$ and ${\bf g}$ stated  in
item~(2) of Lemma~9 is monadic definable.

\end{document}
