1: \begin{definition}[tree automaton for $\AE$-LTL]

2:   \label{d:algo}

3:   Let $\Dcal \subseteq \Nat^*$ be a finite set of arities, and let

4:   $\alpha .  \varphi$ be an $\AE$-LTL formula.

5: %

6:   The parity tree automaton $A^\Dcal_{\alpha . \varphi}$ is obtained

7:   by applying the transformation described in

8:   Definition~\ref{d:abstract-mark} to the parity automaton

9:   $A^\Dcal_{\pf{\alpha . \varphi}}$ built according to

10:   Theorem~\ref{t:ctlstar-tree-aut}.

11: \end{definition}

12: