$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions where the number of
$\mathit{call}$-moves on the path is equal to the number of
$\mathit{ret}$-moves on the path and the path has minimal length. Consider a
subpath of this path from a node $z$ to a node $z^{\prime}$ starting with a
$\mathit{call}$-transition, then following only $\mathit{int}$-transitions and
finally ending with a $\mathit{ret}$-transition. By the construction in (ii),
we only obtain such a path if $z\curvearrowright z^{\prime}$. Now remove the
nodes between $z$ and $z^{\prime}$ from the path and repeat this procedure.
Since the initial path has minimal length, it must end with a
$\mathit{ret}$-transition, it starts with a $\mathit{call}$-transition and we
finally see that $x\curvearrowright y$.

Thus, we have shown that $G$ is indeed an execution graph. It remains to show
that $\mathcal{T}_{A}$ is the tree representation of $G$.

For this, we show by induction over the length of $t$ that for all $t\in T$
with $r_{A}(t)=(p,c)$ we have $\delta_{G}(t)=t$ and either $p\neq\bot$ and $t$
has a $p$-predecessor or $p=\bot$ and $t=\varepsilon$.

In the base case, where $t=\varepsilon$, we have $\delta_{G}(t)=\varepsilon=t$
since $\varepsilon\in V$ has no predecessor. Moreover, we have
$r_{A}(t)=q_{0}=(\bot,0)$, since $r_{A}$ is an $(\varepsilon,q_{0})$-run, i.e.
$p=\bot$.

In the inductive step, let $t$ be of the form $t^{\prime}\cdot i$ for
$i\in\\{0,1\\}$ with $r(t^{\prime})=(l^{\prime},d,p^{\prime})$. Since $T$ is
prefix-closed, we have $t^{\prime}\in T$ and thus, by the induction
hypothesis, $\delta_{G}(t^{\prime})=t^{\prime}$. Here, we make a case
distinction on $d$.

  * •

If $d\in\\{\mathit{int},\mathit{call}\\}$, then
$\mathit{ar}(r(t^{\prime}))=1$, i.e. $i=0$ since $t=t^{\prime}\cdot i\in T$.
Moreover, we have $t^{\prime}\rightarrow^{\mathit{int}}t$ and thus
$\delta_{G}(t)=\delta_{G}(t^{\prime})\cdot 0=t^{\prime}\cdot 0=t$ and
$r_{A}(t)=(d,c)$ for a $c\in\\{0,1\\}$ and $t$ has a $d$-predecessor
$t^{\prime}$.

  * •

If $d=\mathit{callRet}$, then $t^{\prime}$ has a $\mathit{call}$-successor
$t^{\prime}\cdot 0$ and we have $t^{\prime}\curvearrowright t^{\prime}\cdot
1$. If additionally $i=0$, we have $\delta_{G}(t)=\delta_{G}(t^{\prime})\cdot
0=t^{\prime}\cdot 0=t$ and $r_{A}(t)=(\mathit{call},1)$ and $t$ has a
$\mathit{call}$-predecessor $t^{\prime}$. If instead $i=1$, we have
$\delta_{G}(t)=\delta_{G}(t^{\prime})\cdot 1=t^{\prime}\cdot 1=t$ and
$r_{A}(t)=(\mathit{ret},c)$ for a $c\in\\{0,1\\}$ and since
$t^{\prime}\curvearrowright t^{\prime}\cdot 1$ and $G$ is an execution graph,
$t=t^{\prime}\cdot 1$ has a $\mathit{ret}$-predecessor by Lemma 4(i).

  * •

If $d=\mathit{spawn}$, then $t^{\prime}$ has an $\mathit{int}$-successor
$t^{\prime}\cdot 0$ and a $\mathit{spawn}$-successor $t^{\prime}\cdot 1$. If
additionally $i=0$, we have $\delta_{G}(t)=\delta_{G}(t^{\prime})\cdot
0=t^{\prime}\cdot 0=t$ and $r_{A}(t)=(\mathit{int},c)$ for a $c\in\\{0,1\\}$
and $t$ has an $\mathit{int}$-predecessor $t^{\prime}$. If instead $i=1$, we
have $\delta_{G}(t)=\delta_{G}(t^{\prime})\cdot 1=t^{\prime}\cdot 1=t$ and
$r_{A}(t)=(\mathit{spawn},0)$ and $t$ has a $\mathit{spawn}$-predecessor
$t^{\prime}$.

  * •

We cannot have $d\in\\{\mathit{ret},\mathit{end}\\}$, since that would mean
$\mathit{ar}(r(t^{\prime}))=0$, i.e. $t^{\prime}$ has no children.

Moreover, for all nodes $t\in V$ with $r_{A}(t)=(p,c)$ and
$r(t)=(l^{\prime},d,p^{\prime})$, the boolean formula
$\rho((p,c),(l^{\prime},d,p^{\prime}))$ must be satisfied by the children of
$t$, i.e we have $p^{\prime}=p$ since otherwise we had
$\rho((p,c),(l^{\prime},d,p^{\prime}))=\mathit{false}$. Thus, $p^{\prime}$
characterizes the predecessor type of $t$ as required. Finally, it is
straightforward to see that for all $t\in T$ with $r(t)=(l,d,p)$, $d$
specifies the successor types of $t=\delta_{G}^{-1}(t)$ as required for tree
representations.

Overall, we conclude
$\mathcal{T}_{A}=(T,r)=(\mathit{im}(\delta_{G}),r)=\mathcal{T}(G)$. ∎

######  Proof (Proof of Theorem 7.2)

We prove the theorem by induction on the structure of $\varphi$. Therefore, we
also have do deal with non-closed subformulae and consider valuations to
decide whether a subformula is satisfied. In order to do this in a formal way,
we consider automata with special states $X_{1},\dots,X_{n}$, called _holes_ ,
that can be filled with sets of nodes $L_{1},\dots,L_{n}$ of a given tree.
Intuitively, such an automaton can operate on a tree as before, but when a
hole $X_{i}$ is encountered during a run and we are at the tree node $t$, then
we do not continue on the current path and say that it is accepting iff $t\in
L_{i}$.

Formally, let $\mathcal{A}=(Q,q_{0},\rho,\Omega)$ be a 2-way alternating tree
automaton over $(\Sigma,\mathit{ar})$-labelled binary trees with states
$q,X_{1},...,X_{n}\in Q$, $\mathcal{T}=(T,l)$ be a
$(\Sigma,\mathit{ar})$-labelled binary tree, $t\in T$ be a tree node and
$L_{1},...,L_{n}\subseteq T$ be sets of tree nodes. A $(t,q)$-run over
$\mathcal{A}[X_{1}:L_{1},\dots,X_{n}:L_{n}]$ is defined as a $(t,q)$-run
$(T_{r},r)$ over $\mathcal{A}$ except that for nodes $x\in T_{r}$ with
$r(x)=(t^{\prime},X_{i})$ for a $t^{\prime}\in T$, the positive boolean
formula $\rho(X_{i},l(t^{\prime}))$ that has to be satisfied by the children
of $x$ is replaced by $\mathit{true}$, if $t^{\prime}\in L_{i}$, and by
$\mathit{false}$, if $t^{\prime}\notin L_{i}$. The acceptance of such a path
is then defined as before. By
$\mathcal{L}_{q}^{\mathcal{T}}(\mathcal{A}[X_{1}:L_{1},...,X_{n}:L_{n}])$ we
denote the set of nodes $t\in T$ such that there is an accepting $(t,q)$-run
over $\mathcal{A}[X_{1}:L_{1},\dots,X_{n}:L_{n}]$.

For the inductive proof, we now assume that the free variables of the current
formula $\psi\in\mathit{Sub}(\varphi)$ are holes in the automaton and show
that the language of this automaton corresponds to the semantics of $\psi$.
Intuitively, we fill the holes in the automaton, i.e. the free variables of
$\psi$, with the same sets of nodes as specified by a given valuation that we
consider for the semantics of $\psi$. More formally, the holes are filled by
sets of tree nodes that correspond to given sets of graph nodes in the
valuation. Therefore, we lift the function $\delta_{G}\colon V\to T$ for the
execution graph
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ with
$\mathcal{T}(G)=\mathcal{T}=(T,r)$ to a function $\tilde{\delta}_{G}\colon
2^{V}\to 2^{T}$ by $\tilde{\delta}_{G}(A):=\\{\delta_{G}(a)\mid a\in A\\}$ and
show the following claim:

Claim: For all fixpoint variable assignments $\mathcal{V}$, subformulae
$\psi\in\mathit{Sub}(\varphi)$ with free variables $X_{1},\dots,X_{n}$ and
$L_{1},\dots,L_{n}\subseteq V$ we have

$\displaystyle\mathcal{L}_{\psi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])=\tilde{\delta}_{G}(\llbracket\psi\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G}).$

Since $\varphi$ is closed, this implies in particular that

$\displaystyle\mathcal{T}\in\mathcal{L}(\mathcal{\tilde{A}}_{\varphi})\Leftrightarrow\varepsilon\in\mathcal{L}_{\varphi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi})\Leftrightarrow\varepsilon\in\tilde{\delta}_{G}(\llbracket\varphi\rrbracket^{G})\Leftrightarrow
v_{0}\in\llbracket\varphi\rrbracket^{G}\Leftrightarrow
G\in\llbracket\varphi\rrbracket.$

We now proceed with the structural induction.

  * •

For $\psi\equiv\mathit{ap}\in\mathit{AP}$ we have

$\displaystyle\
\mathcal{L}_{\psi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi})=\\{\delta_{G}(x)\in
T\mid\mathit{ap}\in l(x)\\}$ $\displaystyle=$ $\displaystyle\
\tilde{\delta}_{G}(\\{x\in V\mid\mathit{ap}\in l(x)\\})$ $\displaystyle=$
$\displaystyle\
\tilde{\delta}_{G}(\llbracket\psi\rrbracket_{\mathcal{V}}^{G}).$

  * •

For $\psi\equiv\lnot\mathit{ap}$ with $\mathit{ap}\in\mathit{AP}$, the claim
follows analogously.

  * •

For $\psi\equiv X$ and $L\subseteq V$ we have

$\displaystyle\
\mathcal{L}_{\psi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X:\tilde{\delta}_{G}(L)])$
$\displaystyle=$ $\displaystyle\ \tilde{\delta}_{G}(L)$ $\displaystyle=$
$\displaystyle\ \tilde{\delta}_{G}(\mathcal{V}[X\mapsto L](X))$
$\displaystyle=$ $\displaystyle\
\tilde{\delta}_{G}(\llbracket\psi\rrbracket_{\mathcal{V}[X\mapsto L]}^{G}).$

  * •

For $\psi\equiv\psi_{1}\lor\psi_{2}$, let
$X_{k^{i}_{1}},\dots,X_{k^{i}_{n_{i}}}$ be the free variables of $\psi_{i}$
for $i\in\\{1,2\\}$. We clearly have
$\mathcal{L}_{\psi_{i}}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])=\mathcal{L}_{\psi_{i}}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{k^{i}_{1}}:\tilde{\delta}_{G}(L_{k^{i}_{1}}),\dots,X_{k^{i}_{n_{i}}}:\tilde{\delta}_{G}(L_{k^{i}_{n_{i}}})])$
since a $(t,\psi_{i})$-run over
$\mathcal{\tilde{A}}_{\varphi}[X_{k^{i}_{1}}:\tilde{\delta}_{G}(L_{k^{i}_{1}}),\dots,X_{k^{i}_{n_{i}}}:\tilde{\delta}_{G}(L_{k^{i}_{n_{i}}})]$
can only reach nodes labelled by a fixpoint variable $X$ if $X$ occurs in
$\psi_{i}$. Moreover,
$\llbracket\psi_{i}\rrbracket_{\mathcal{V}[X_{k^{i}_{1}}\mapsto
L_{k^{i}_{1}},\dots,X_{k^{i}_{n_{i}}}\mapsto
L_{k^{i}_{n_{i}}}]}^{G}=\llbracket\psi\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G}$, since all the free variables
$X_{k^{i}_{1}},\dots,X_{k^{i}_{n_{i}}}$ of $\psi_{i}$ are also among the free
variables $X_{1},\dots,X_{n}$ of $\psi$. Thus, we have

$\displaystyle\
\mathcal{L}_{\psi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[IH]{}}}{=}}$
$\displaystyle\bigcup\limits_{i\in\\{0,1\\}}\mathcal{L}_{\psi_{i}}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[IH]{}}}{=}}$
$\displaystyle\bigcup\limits_{i\in\\{0,1\\}}\mathcal{L}_{\psi_{i}}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{k^{i}_{1}}:\tilde{\delta}_{G}(L_{k^{i}_{1}}),\dots,X_{k^{i}_{n_{i}}}:\tilde{\delta}_{G}(L_{k^{i}_{n_{i}}})])$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[IH]{(IH)}}}{=}}$
$\displaystyle\bigcup\limits_{i\in\\{0,1\\}}\tilde{\delta}_{G}(\llbracket\psi_{i}\rrbracket_{\mathcal{V}[X_{k^{i}_{1}}\mapsto
L_{k^{i}_{1}},\dots,X_{k^{i}_{n_{i}}}\mapsto L_{k^{i}_{n_{i}}}]}^{G})$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[IH]{}}}{=}}$
$\displaystyle\bigcup\limits_{i\in\\{0,1\\}}\tilde{\delta}_{G}(\llbracket\psi_{i}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G})$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[IH]{}}}{=}}$
$\displaystyle\
\tilde{\delta}_{G}(\bigcup\limits_{i\in\\{0,1\\}}\llbracket\psi_{i}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G})$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[IH]{}}}{=}}$
$\displaystyle\
\tilde{\delta}_{G}(\llbracket\psi\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G})$

where equation (IH) uses the induction hypothesis.

  * •

For $\psi\equiv\psi_{1}\land\psi_{2}$, the claim follows analogously since
$\tilde{\delta}_{G}$ is injective.

  * •

For $\psi\equiv\bigcirc^{f}\psi^{\prime}$ with $f\in\\{g,\uparrow,a,-,p,c\\}$,
the free variables $X_{1},\dots,X_{n}$ of $\psi$ are also the free variables
of $\psi^{\prime}$. Following the definition of the tree successor functions,
we easily see that

$\displaystyle\mathcal{L}_{\psi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[*]{}}}{=}}$
$\displaystyle\\{t\in T\mid\mathit{succ}_{f}^{\mathcal{T}}(t)\text{ is defined
and}$
$\displaystyle\mathit{succ}_{f}^{\mathcal{T}}(t)\in\mathcal{L}_{\psi^{\prime}}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])\\}$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[*]{(IH)}}}{=}}$
$\displaystyle\\{t\in T\mid\mathit{succ}_{f}^{\mathcal{T}}(t)\text{ is defined
and
}\mathit{succ}_{f}^{\mathcal{T}}(t)\in\tilde{\delta}_{G}(\llbracket\psi^{\prime}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G})\\}$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[*]{(\textasteriskcentered)}}}{=}}$
$\displaystyle\\{\delta_{G}(x)\in T\mid\mathit{succ}_{f}^{G}(x)\text{ is
defined and}$
$\displaystyle\delta_{G}(\mathit{succ}_{f}^{G}(x))\in\tilde{\delta}_{G}(\llbracket\psi^{\prime}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G})\\}$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[*]{}}}{=}}$
$\displaystyle\tilde{\delta}_{G}(\\{x\in V\mid\mathit{succ}_{f}^{G}(x)\text{
is defined and
}\mathit{succ}_{f}^{G}(x)\in\llbracket\psi^{\prime}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G}\\})$
$\displaystyle\mathrel{\overset{\scriptsize{\eqmakebox[*]{}}}{=}}$
$\displaystyle\tilde{\delta}_{G}(\llbracket\psi\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G}),$

where equation (IH) uses the induction hypothesis and equation (*) uses Lemma
1.

  * •

For $\psi\equiv\bigcirc^{\bar{f}}\psi^{\prime}$ with
$f\in\\{g,\uparrow,a,-,p,c\\}$ we observe that a $(t,\psi)$-run behaves as a
$(t,\bigcirc^{f}\psi^{\prime})$-run except that we move to $\mathit{true}$
instead of $\mathit{false}$, if a desired successor or predecessor does not
exist. Thus, analogously to the previous case, it is easy to see that

$\displaystyle\
\mathcal{L}_{\psi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])$
$\displaystyle=$ $\displaystyle\ \\{t\in
T\mid\mathit{succ}_{f}^{\mathcal{T}}(t)\text{ is undefined or}$
$\displaystyle\mathit{succ}_{f}^{\mathcal{T}}(t)\in\mathcal{L}_{\psi^{\prime}}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])\\}$
$\displaystyle{=}$ $\displaystyle\ \tilde{\delta}_{G}(V\setminus\\{x\in
V\mid\mathit{succ}_{f}^{G}(x)\text{ is defined and}$
$\displaystyle\mathit{succ}_{f}^{G}(x)\notin\llbracket\psi^{\prime}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G}\\})$ $\displaystyle{=}$ $\displaystyle\
\tilde{\delta}_{G}(V\setminus\\{x\in V\mid\mathit{succ}_{f}^{G}(x)\text{ is
defined and}$
$\displaystyle\mathit{succ}_{f}^{G}(x)\in\llbracket\lnot\psi^{\prime}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G}\\})$ $\displaystyle{=}$ $\displaystyle\
\tilde{\delta}_{G}(V\setminus\llbracket\bigcirc^{f}\lnot\psi^{\prime}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G})$ $\displaystyle{=}$ $\displaystyle\
\tilde{\delta}_{G}(\llbracket\lnot\bigcirc^{f}\lnot\psi^{\prime}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G})$ $\displaystyle{=}$ $\displaystyle\
\tilde{\delta}_{G}(\llbracket\psi\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}^{G}).$

  * •

For $\psi\equiv\mu X.\psi^{\prime}$, the free variables of $\psi^{\prime}$ are
given by $X_{1},\dots,X_{n},X$. We observe that a $(t,\psi)$-run over
$\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})]$
can only visit states $\varphi^{\prime}$ of the form $\mu
X.\psi^{\prime\prime}$ or $\nu X.\psi^{\prime\prime}$ if $\varphi^{\prime}$ is
a subformula of $\psi$. Therefore, $\Omega(\psi)$ is the lowest priority
occurring in the run so that the state $\psi$ can only be visited finitely
often if the run is accepting. This means we can characterize
$\mathcal{L}_{\psi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])$
as the least fixpoint of the function $f:2^{T}\to 2^{T}$ with
$f(\tilde{\delta}_{G}(L)):=\mathcal{L}_{\psi^{\prime}}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n}),X:\tilde{\delta}_{G}(L)])$.
By the induction hypothesis, we obtain
$f(\tilde{\delta}_{G}(L))=\tilde{\delta}_{G}(\llbracket\psi^{\prime}\rrbracket_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n},X\mapsto
L]}^{G})=\tilde{\delta}_{G}(\alpha_{S}(L))$ where $S=(G,\\\
\mathcal{V}[X_{1}\mapsto L_{1},\dots,X_{n}\mapsto L_{n}],X,\psi^{\prime})$. By
Corollary 2, the least fixpoint of $\alpha_{S}$ is given by
$\llbracket\psi\rrbracket^{G}_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}$. Since the function $\tilde{\delta}_{G}$ is
trivially monotone and bijective because $\delta_{G}$ is bijective, we
conclude by Lemma 2 that
$\tilde{\delta}_{G}(\llbracket\psi\rrbracket^{G}_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]})$ is the least fixpoint of $f$, i.e.

$\displaystyle\mathcal{L}_{\psi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:\tilde{\delta}_{G}(L_{1}),\dots,X_{n}:\tilde{\delta}_{G}(L_{n})])=\tilde{\delta}_{G}(\llbracket\psi\rrbracket^{G}_{\mathcal{V}[X_{1}\mapsto
L_{1},\dots,X_{n}\mapsto L_{n}]}).$

  * •

For $\psi\equiv\nu X.\psi^{\prime}$, the claim follows analogously. ∎

In order to prove Theorem 7.3, we establish the following lemma:

###### Lemma 5

Let $\mathcal{M}=(S,s_{0},\gamma_{0},\Delta,L)$ be a DPN and
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ be an
execution graph of $\mathcal{M}$ witnessed by the assignment
$\mathit{as}\colon V\to S\times\Gamma^{*}\bot$. Further, let $x,y\in V$ be
nodes with $y=\mathit{succ}_{a}^{G}(x)$. Then there are control locations
$s,s^{\prime}\in S$, stack symbols $\gamma,\gamma^{\prime}\in\Gamma$ and a
stack content $w\in\Gamma^{*}\bot$ such that $\mathit{as}(x)=(s,\gamma w)$ and
$\mathit{as}(y)=(s^{\prime},\gamma^{\prime}w)$.

###### Proof

Since $y=\mathit{succ}_{a}^{G}(x)$, we either have
$x\rightarrow^{\mathit{int}}y$ or $x\curvearrowright y$. In both cases, there
is a path $\pi$ from $x$ to $y$ following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions such that the number
$n$ of $\mathit{call}$-moves on $\pi$ is equal to the number of
$\mathit{ret}$-moves on $\pi$. We show the claim by induction over $n$.

If $n=0$, we have $x\rightarrow^{\mathit{int}}y$. Since $G$ is generated by
$\mathcal{M}$, we thus have
$\mathit{as}(x)\rightarrow_{\mathit{int}}\mathit{as}(y)$, i.e. there are
control locations $s,s^{\prime}\in S$, stack symbols
$\gamma,\gamma^{\prime}\in\Gamma$ and a stack content $w\in\Gamma^{*}\bot$
such that $\mathit{as}(x)=(s,\gamma w)$ and
$\mathit{as}(y)=(s^{\prime},\gamma^{\prime}w)$.

If $n>0$, we have $x\curvearrowright y$. Thus, $x$ has a
$\mathit{call}$-successor $x^{\prime}$ and by Lemma 4(i), $y$ has a
$\mathit{ret}$-predecessor $y^{\prime}$ with
$\mathit{succ}_{-}^{G}(z^{\prime})=x$, i.e. there is a path $\pi^{\prime}$
from $x^{\prime}$ to $z^{\prime}$ following abstract successors. In
particular, in each step in $\pi^{\prime}$ from a node $u$ to its abstract
successor $v$, there is a path $\pi^{\prime\prime}$ from $u$ to $v$ following
only $\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions such that the
number $m_{\pi^{\prime\prime}}$ of $\mathit{call}$-moves on
$\pi^{\prime\prime}$ is equal to the number of $\mathit{ret}$-moves on
$\pi^{\prime\prime}$. Since all of these paths $\pi^{\prime\prime}$ are proper
subpaths of $\pi$, we clearly have $m_{\pi^{\prime\prime}}<n$ in each step.
Thus, by the induction hypothesis, there are control locations $s_{1},s_{2}\in
S$, stack symbols $\gamma_{1},\gamma_{2}\in\Gamma$ and a stack content
$w^{\prime}\in\Gamma^{*}\bot$ such that
$\mathit{as}(x^{\prime})=(s_{1},\gamma_{1}w^{\prime})$ and
$\mathit{as}(y^{\prime})=(s_{2},\gamma_{2}w^{\prime})$. Since further
$x\rightarrow^{\mathit{call}}x^{\prime}$ and hence
$\mathit{as}(x)\rightarrow_{\mathit{call}}\mathit{as}(x^{\prime})$, we also
have $\mathit{as}(x)=(s,\gamma w)$ for some $s\in S$ and $\gamma\in\Gamma$ as
well as $w^{\prime}=\gamma^{\prime}w$ for some $\gamma^{\prime}\in\Gamma$.
Finally, since $y^{\prime}\rightarrow^{\mathit{ret}}y$ and hence
$\mathit{as}(y^{\prime})\rightarrow_{\mathit{ret}}\mathit{as}(y)$, we also
have $\mathit{as}(y)=(s^{\prime},w^{\prime})=(s^{\prime},\gamma^{\prime}w)$
for some $s^{\prime}\in S$. ∎

######  Proof (Proof of Theorem 7.3)

We first show that $\mathcal{{A}}_{\mathcal{M}}$ accepts all tree
representations of executions graphs generated by $\mathcal{M}$.

For this, let
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ be an
execution graph of $\mathcal{M}$ witnessed by the assignment
$\mathit{as}\colon V\to S\times\Gamma^{*}\bot$. Further, let
$\mathcal{T}(G)=(T,r)$ be the tree representation of $G$. We first define maps
$r_{S}\colon V\to S$ and $r_{\Gamma}\colon V\to\Gamma$ as follows. For nodes
$x\in V$ with $\mathit{as}(x)=(s,\gamma w)$ for some stack symbol
$\gamma\in\Gamma$ and stack content $w\in\Gamma^{*}\bot$ we set $r_{S}(x):=s$
and $r_{\Gamma}(x)=\gamma$. Moreover, we inductively define a map $r_{R}\colon
V\to(S\times\Gamma)\cup\\{\bot\\}$ as follows. First, we set
$r_{R}(v_{0}):=\bot$. Then, for all nodes $x\in V$,

  * •

if there is a node $y\in V$ such that $y$ is an $\mathit{int}$-predecessor of
$x$ or $y\curvearrowright x$ (the latter holds by Lemma 4(i) iff $x$ has a
$\mathit{ret}$-predecessor), we set $r_{R}(x):=r_{R}(y)$,

  * •

if $x$ (i) has a $\mathit{spawn}$-predecessor or (ii) it has a
$\mathit{call}$-predecessor $y$ and there is no $z\in V$ with
$y\curvearrowright z$, we set $r_{R}(x):=\bot$ and

  * •

if $x$ has a $\mathit{call}$-predecessor $y$ and there is $z\in V$ with
$y\curvearrowright z$, we set
$r_{R}(x):=(r_{S}(z^{\prime}),r_{\Gamma}(z^{\prime}))$, where $z^{\prime}$ is
the $\mathit{ret}$-predecessor of $z$ (this node exists in this case by Lemma
4(i)).

Finally, we define a map $r_{A}\colon T\to Q$ by
$r_{A}(\delta_{G}(x)):=(r_{S}(x),r_{\Gamma}(x),r_{R}(x))$ and show the
following claim:

Claim: $r_{A}$ is an accepting $(\varepsilon,q_{0})$-run of
$\mathcal{A}_{\mathcal{M}}$ over $\mathcal{T}(G)$.

First, we show that $r_{A}$ is an $(\varepsilon,q_{0})$-run of
$\mathcal{A}_{\mathcal{M}}$ over $\mathcal{T}(G)$.

For the initial node, we have $\mathit{as}(v_{0})=(s_{0},\gamma_{0}\bot)$ as
well as $r_{R}(v_{0})=\bot$ and thus
$r_{A}(\varepsilon)=r_{A}(\delta_{G}(v_{0}))=(s_{0},\gamma_{0},\bot)=q_{0}$.

Now let $t=\delta_{G}(x)\in T$ be a node with $r(t)=(l(x),d(x),p(x))$ and
$r_{A}(t)=(s,\gamma,c)$. Then we have $\mathit{as}(x)=(s,\gamma w)$ for a
stack content $w\in\Gamma^{*}\bot$ and the node is labelled by
$l(x)=L(s,\gamma)$ since $G$ is generated by $\mathcal{M}$. By a case
distinction on $d(x)$, we show that the successors of $t$ satisfy the
transition function of $\mathcal{A}_{\mathcal{M}}$.

  * •

If $d(x)=\mathit{int}$, then $x$ has an $\mathit{int}$-successor $y$ with
$\mathit{as}(x)\rightarrow_{\mathit{int}}\mathit{as}(y)$. Thus, there are
$s^{\prime}\in S$ and $\gamma^{\prime}\in\Gamma$ with
$\mathit{as}(y)=(s^{\prime},\gamma^{\prime}w)$ and $s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\in\Delta_{I}$. Moreover, we have
$r_{R}(y)=r_{R}(x)=c$ and $\delta_{G}(y)=t\cdot 0$. Thus, $\\{(0,r_{A}(t\cdot
0))\\}=\\{(0,(s^{\prime},\gamma^{\prime},c))\\}$ satisfies
$\rho((s,\gamma,c),r(t))$.

  * •

If $d(x)=\mathit{call}$, then $x$ has a $\mathit{call}$-successor $y$ with
$\mathit{as}(x)\rightarrow_{\mathit{call}}\mathit{as}(y)$. Thus, there are
$s^{\prime}\in S$ and $\gamma^{\prime},\gamma^{\prime\prime}\in\Gamma$ with
$\mathit{as}(y)=(s^{\prime},\gamma^{\prime}\gamma^{\prime\prime}w)$ and
$s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}$. Moreover, there
is no node $z\in V$ with $x\curvearrowright z$, i.e. $r_{R}(x)=\bot$, and
$\delta_{G}(y)=t\cdot 0$. Thus $\\{(0,r_{A}(t\cdot
0))\\}=\\{(0,(s^{\prime},\gamma^{\prime},\bot))\\}$ satisfies
$\rho((s,\gamma,c),r(t))$.

  * •

If $d(x)=\mathit{callRet}$, then $x$ has a $\mathit{call}$-successor $y$ with
$\mathit{as}(x)\rightarrow_{\mathit{call}}\mathit{as}(y)$. Thus, there are
$s^{\prime}\in S$ and $\gamma^{\prime},\gamma^{\prime\prime}\in\Gamma$ with
$\mathit{as}(y)=(s^{\prime},\gamma^{\prime}\gamma^{\prime\prime}w)$ and
$s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}$. Moreover, there
is a node $z\in V$ with $x\curvearrowright z$. By Lemma 4(i), $z$ has a
$\mathit{ret}$-predecessor $z^{\prime}$ with
$\mathit{succ}_{-}^{G}(z^{\prime})=x$, i.e. there is a path from the
$\mathit{call}$-successor $y$ of $x$ to $z^{\prime}$ following abstract
successors. Hence, by Lemma 5, there are $s_{r}\in S$ and
$\gamma_{r}\in\Gamma$ with
$\mathit{as}(z^{\prime})=(s_{r},\gamma_{r}\gamma^{\prime\prime}w)$. Moreover,
since $z^{\prime}\rightarrow^{\mathit{ret}}z$, we have
$\mathit{as}(z^{\prime})\rightarrow_{\mathit{ret}}\mathit{as}(z)$, i.e. there
is $s^{\prime\prime}\in S$ with
$\mathit{as}(z)=(s^{\prime\prime},\gamma^{\prime\prime}w)$ and
$s_{r}\gamma_{r}\rightarrow s^{\prime\prime}\in\Delta_{R}$. Thus, we have
$r_{R}(y)=(r_{S}(z^{\prime}),r_{\Gamma}(z^{\prime}))=(s_{r},\gamma_{r})$,
$\delta_{G}(y)=t\cdot 0$, $r_{R}(z)=r_{R}(x)=c$ and $\delta_{G}(z)=t\cdot 1$.
Hence, $\\{(0,r_{A}(t\cdot 0)),(1,r_{A}(t\cdot
1))\\}=\\{(0,(s^{\prime},\gamma^{\prime},(s_{r},\gamma_{r}))),(1,(s^{\prime\prime},\gamma^{\prime\prime},c))\\}$
satisfies $\rho((s,\gamma,c),r(t))$.

  * •

If $d(x)=\mathit{spawn}$, then $x$ has an $\mathit{int}$-successor $y$ and a
$\mathit{spawn}$-successor $z$ with
$\mathit{as}(x)\rightarrow\mathit{as}(y)\vartriangleright\mathit{as}(z)$.
Thus, there are $s^{\prime},s_{n}\in S$ and
$\gamma^{\prime},\gamma_{n}\in\Gamma$ with
$\mathit{as}(y)=(s^{\prime},\gamma^{\prime}w)$,
$\mathit{as}(z)=(s_{n},\gamma_{n}\bot)$ and $s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\vartriangleright s_{n}\gamma_{n}\in\Delta_{S}$.
Moreover, we have $r_{R}(y)=r_{R}(x)=c$, $\delta_{G}(y)=t\cdot 0$,
$r_{R}(z)=\bot$, and $\delta_{G}(z)=t\cdot 1$. Thus, $\\{(0,r_{A}(t\cdot
0)),(1,r_{A}(t\cdot
1))\\}=\\{(0,(s^{\prime},\gamma^{\prime},c)),(1,(s_{n},\gamma_{n},\bot))\\}$
satisfies $\rho((s,\gamma,c),r(t))$.

  * •

If $d(x)=\mathit{ret}$, then $x$ has a $\mathit{ret}$-successor $y$ with
$\mathit{as}(x)\rightarrow_{\mathit{ret}}\mathit{as}(y)$. Thus, there is
$s^{\prime}\in S$ with $\mathit{as}(y)=(s^{\prime},w)$ and $s\gamma\rightarrow
s^{\prime}\in\Delta_{R}$. Moreover, by Lemma 4(i), there is a node $z\in V$
with $z\curvearrowright y$ and $z=\mathit{succ}_{-}^{G}(x)$, i.e. there is a
path from the $\mathit{call}$-successor $z^{\prime}$ of $z$ to $x$ following
abstract successors. Thus, we have
$c=r_{R}(x)=r_{R}(z^{\prime})=(r_{S}(x),r_{\Gamma}(x))=(s,\gamma)$, i.e.
$\emptyset$ satisfies
$\mathit{true}=\rho((s,\gamma,(s,\gamma)),r(t))=\rho((s,\gamma,c),r(t))$.

  * •

If $d(x)=\mathit{end}$, then $x$ has no successors and hence $\mathit{as}(x)$
has no successor, i.e. there is no rule for $s\gamma$ in $\Delta$. Assume
towards contradiction that $c\neq\bot$. By construction, there must be nodes
$y,z\in V$ with $y\curvearrowright z$ and a path from the
$\mathit{call}$-successor $y^{\prime}$ of $y$ to $x$ following abstract
successors. Thus, $\delta_{G}(x)$ is the
$\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of the left child
$\delta_{G}(y^{\prime})=\delta_{G}(y)\cdot 0$ of the parent node
$\delta_{G}(y)$ of $\delta_{G}(z)=\delta_{G}(y)\cdot 1$. Then we have
$\mathit{succ}_{\uparrow}^{\mathcal{T}(G)}(\delta_{G}(z))=\delta_{G}(x)$.
Using Lemma 1, we obtain
$\delta_{G}(\mathit{succ}_{\uparrow}^{G}(z))=\mathit{succ}_{\uparrow}^{\mathcal{T}(G)}(\delta_{G}(z))=\delta_{G}(x)$
and thus $\mathit{succ}_{\uparrow}^{G}(z)=x$ since $\delta_{G}$ is injective.
This means that $z$ is a successor of $x$, which contradicts our assumption
that $x$ has no successor. Thus, we have $c=\bot$ and hence $\emptyset$
satisfies $\mathit{true}=\rho((s,\gamma,\bot),r(t))=\rho((s,\gamma,c),r(t))$.

Thus, we have established that $r_{A}$ is an $(\varepsilon,q_{0})$-run of
$\mathcal{{A}}_{\mathcal{M}}$ over $\mathcal{T}(G)$. Since we have
$\Omega(q)=0$ for all $q\in Q$, the run is clearly accepting, and thus
$\mathcal{T}(G)\in\mathcal{L}(\mathcal{{A}}_{\mathcal{M}})$.

For the other direction of the theorem, we show that all exeution trees
accepted by $\mathcal{A}_{\mathcal{M}}$ are tree representations of execution
graphs of $\mathcal{M}$. For this, let
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ be an
execution graph with
$\mathcal{T}(G)=(T,r)\in\mathcal{L}(\mathcal{A}_{\mathcal{M}})$. Then there is
an accepting $(\varepsilon,q_{0})$-run $r_{A}$ of
$\mathcal{{A}}_{\mathcal{M}}$ over $\mathcal{T}(G)$. We now inductively define
an assignment $\mathit{as}\colon V\to S\times\Gamma^{*}\bot$ such that for all
nodes $v\in V$ with $\mathit{as}(v)=(s,\gamma w)$ for a stack symbol
$\gamma\in\Gamma$ and a stack content $w\in\Gamma^{*}\bot$, we have
$r_{A}(\delta_{G}(v))=(s,\gamma,c)$ for a $c\in(S\times\Gamma)\cup\\{\bot\\}$.

In the base case, we set $\mathit{as}(v_{0}):=(s_{0},\gamma_{0}\bot)$. Since
$r_{A}$ is an $(\varepsilon,q_{0})$-run of $\mathcal{{A}}_{\mathcal{M}}$, we
have
$r_{A}(\delta_{G}(v_{0}))=r_{A}(\varepsilon)=q_{0}=(s_{0},\gamma_{0},\bot)$.

In the inductive step, let $\mathit{as}$ be defined for some node $v\in V$
with $r(\delta_{G}(v))=(l^{\prime},d,p)$ such that there are $\gamma\in\Gamma$
and $w\in\Gamma^{*}\bot$ with $\mathit{as}(v)=(s,\gamma w)$ and
$r_{A}(\delta_{G}(v))=(s,\gamma,c)$ for a $c\in(S\times\Gamma)\cup\\{\bot\\}$.
We define the mapping for the successors of $v$ by a case distinction on $d$.

  * •

If $d=\mathit{int}$, $v$ has exactly one $\mathit{int}$-successor $v^{\prime}$
and we have $r_{A}(\delta_{G}(v^{\prime}))=r_{A}(\delta_{G}(v)\cdot
0)=(s^{\prime},\gamma^{\prime},c)$ for some $s^{\prime}\in S$ and
$\gamma^{\prime}\in\Gamma$ such that $s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\in\Delta_{I}$. Then we set
$\mathit{as}(v^{\prime}):=(s^{\prime},\gamma^{\prime}w)$.

  * •

If $d=\mathit{call}$, $v$ has exactly one $\mathit{call}$-successor
$v^{\prime}$ and we have
$r_{A}(\delta_{G}(v^{\prime}))=r_{A}(\delta_{G}(v)\cdot
0)=(s^{\prime},\gamma^{\prime},\bot)$ for some $s^{\prime}\in S$ and
$\gamma^{\prime}\in\Gamma$ such that $s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}$ for a
$\gamma^{\prime\prime}\in\Gamma$. Then we set
$\mathit{as}(v^{\prime}):=(s^{\prime},\gamma^{\prime}\gamma^{\prime\prime}w)$.

  * •

If $d=\mathit{callRet}$, $v$ has exactly one $\mathit{call}$-successor
$v^{\prime}$ and there is $v^{\prime\prime}\in V$ with $v\curvearrowright
v^{\prime\prime}$. Then we have
$r_{A}(\delta_{G}(v^{\prime}))=r_{A}(\delta_{G}(v)\cdot
0)=(s^{\prime},\gamma^{\prime},(s_{r},\gamma_{r}))$ and
$r_{A}(\delta_{G}(v^{\prime\prime}))=r_{A}(\delta_{G}(v)\cdot
1)=(s^{\prime\prime},\gamma^{\prime\prime},c)$ for some
$s^{\prime},s^{\prime\prime},s_{r}\in S$ and
$\gamma^{\prime},\gamma^{\prime\prime},\gamma_{r}\in\Gamma$ such that
$s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}$ and
$s_{r}\gamma_{r}\rightarrow s^{\prime\prime}\in\Delta_{R}$. Then we set
$\mathit{as}(v^{\prime}):=(s^{\prime},\gamma^{\prime}\gamma^{\prime\prime}w)$
and
$\mathit{as}(v^{\prime\prime}):=(s^{\prime\prime},\gamma^{\prime\prime}w)$.

  * •

If $d=\mathit{spawn}$, $v$ has exactly one $\mathit{int}$-successor
$v^{\prime}$ and one $\mathit{spawn}$-successor $v^{\prime\prime}$. Then we
have $r_{A}(\delta_{G}(v^{\prime}))=r_{A}(\delta_{G}(v)\cdot
0)=(s^{\prime},\gamma^{\prime},c)$ and
$r_{A}(\delta_{G}(v^{\prime\prime}))=r_{A}(\delta_{G}(v)\cdot
1)=(s_{n},\gamma_{n},\bot)$ for some $s^{\prime},s_{n}\in S$ and
$\gamma^{\prime},\gamma_{n}\in\Gamma$ such that $s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\vartriangleright s_{n}\gamma_{n}\in\Delta_{S}$. Then
we set $\mathit{as}(v^{\prime}):=(s^{\prime},\gamma^{\prime}w)$ and
$\mathit{as}(v^{\prime\prime}):=(s_{n},\gamma_{n}\bot)$.

Most conditions for $\mathit{as}$ to witness that $G$ is generated by
$\mathcal{M}$ are directly satisfied by construction. We only show the more
involved conditions regarding nodes with $\mathit{ret}$-successors and nodes
without successors. In order to do this, we inductively show that the
following holds for all nodes $v\in V$ with
$r_{A}(\delta_{G}(v))=(s,\gamma,c)$:

$(*)$ We have $c=(s_{r},\gamma_{r})$ for a $s_{r}\in S$ and
$\gamma_{r}\in\Gamma$ iff there are nodes $v_{1},v_{2},v_{3}\in V$ with
$v_{1}\rightarrow^{\mathit{call}}v_{2}$, $v_{1}\curvearrowright v_{3}$ and
$s^{\prime}\in S$ and $\gamma^{\prime}\in\Gamma$ with
$r_{A}(\delta_{G}(v_{2}))=(s^{\prime},\gamma^{\prime},c)$ and there is a path
from $v_{2}$ to $v$ following abstract successors.

In the base case, where $v=v_{0}$, we have $c=\bot$ and there is no incoming
$\mathit{int}$-transition or nesting edge to $v$.

In the inductive step, let $v\in V$ be a node with
$r_{A}(\delta_{G}(v))=(s,\gamma,c)$ such that
$\delta_{G}(v)=\delta_{G}(v^{\prime})\cdot i$ for an $i\in\\{0,1\\}$ and a
node $v^{\prime}\in V$ with $r(\delta_{G}(v^{\prime}))=(l^{\prime},d,p)$ and
$r_{A}(\delta_{G}(v^{\prime}))=(s^{\prime},\gamma^{\prime},c^{\prime})$. We
show $(*)$ for $v$ by a case distinction on $d$.

  * •

If $d=\mathit{int}$, we have $i=0$ and
$\rho(r_{A}(\delta_{G}(v^{\prime})),r(\delta_{G}(v^{\prime})))$ is a
disjunction of formulae of the form
$(0,(s^{\prime\prime},\gamma^{\prime\prime},c^{\prime}))$ for
$s^{\prime\prime}\in S$ and $\gamma^{\prime\prime}\in\Gamma$, i.e.
$c=c^{\prime}$. Since $v^{\prime}\rightarrow^{\mathit{int}}v$ and abstract
successors are uniquely determined, the right side of the equivalence in $(*)$
is satisfied for $v$ iff it is satisfied for $v^{\prime}$. Thus, by the
induction hypothesis, $(*)$ also holds for $v$.

  * •

If $d=\mathit{call}$, we have $i=0$ and
$\rho(r_{A}(\delta_{G}(v^{\prime})),r(\delta_{G}(v^{\prime})))$ is a
disjunction of formulae of the form
$=(0,(s^{\prime\prime},\gamma^{\prime\prime},\bot))$ for $s^{\prime\prime}\in
S$ and $\gamma^{\prime\prime}\in\Gamma$, i.e. $c=\bot$. Since there is no node
$\tilde{v}\in V$ with $\tilde{v}\rightarrow^{\mathit{int}}v$,
$\tilde{v}\curvearrowright v$ or $v^{\prime}\curvearrowright\tilde{v}$, the
required nodes and the path for any $c\neq\bot$ do not exist for $v$.

  * •

If $d=\mathit{callRet}$, then
$\rho(r_{A}(\delta_{G}(v^{\prime})),r(\delta_{G}(v^{\prime})))$ is a
disjunction of formulae of the form
$(0,(s_{1},\gamma_{1},(s_{r},\gamma_{r})))\land(1,(s_{2},\gamma_{2},c^{\prime}))$
for $s_{1},s_{2},s_{r}\in S$ and $\gamma_{1},\gamma_{2},\gamma_{r}\in\Gamma$.
If additionally $i=0$, then $c=(s_{r},\gamma_{r})$ for some $s_{r}\in S$ and
$\gamma_{r}\in\Gamma$. Since $v^{\prime}\rightarrow^{\mathit{call}}v$ and
$v^{\prime}\curvearrowright v^{\prime\prime}$ for some $v^{\prime\prime}\in
V$, the nodes $v_{1}=v^{\prime}$, $v_{2}=v$ and $v_{3}=v^{\prime\prime}$ and
the empty path from $v_{2}=v$ to $v$ witness that $(*)$ holds. If instead
$i=1$, then $c=c^{\prime}$ and $v^{\prime}\curvearrowright v$. Since abstract
successors are uniquely determined, the right side of the equivalence in $(*)$
is satisfied for $v$ iff it is satisfied for $v^{\prime}$. Thus, by the
induction hypothesis, $(*)$ also holds for $v$.

  * •

If $d=\mathit{spawn}$, then
$\rho(r_{A}(\delta_{G}(v^{\prime})),r(\delta_{G}(v^{\prime})))$ is a
disjunction of formulae of the form
$(0,(s_{1},\gamma_{1},c^{\prime}))\land(1,(s_{2},\gamma_{2},\bot))$ for
$s_{1},s_{2}\in S$ and $\gamma_{1},\gamma_{2}\in\Gamma$. If additionally
$i=0$, then $c=c^{\prime}$. Since $v^{\prime}\rightarrow^{\mathit{int}}v$ and
abstract successors are uniquely determined, the right side of the equivalence
in $(*)$ is satisfied for $v$ iff it is satisfied for $v^{\prime}$. Thus, by
induction hypothesis, $(*)$ also holds for $v$. If instead $i=1$, then
$c=\bot$. Since there is no node $\tilde{v}\in V$ with
$\tilde{v}\rightarrow^{\mathit{int}}v$, $\tilde{v}\curvearrowright v$ or
$v^{\prime}\curvearrowright\tilde{v}$, the required nodes and the path for any
$c\neq\bot$ do not exist for $v$.

Given $(*)$, we now show the more involved conditions regarding nodes with
$\mathit{ret}$-successors. For this, let $x,y\in V$ be nodes with
$x\rightarrow^{\mathit{ret}}y$. By Lemma 4(i), there is a node $z\in V$ with
$z\curvearrowright y$ and $\mathit{succ}_{-}^{G}(x)=z$, i.e. there is a path
from the $\mathit{call}$-successor $z^{\prime}$ of $z$ to $x$ following
abstract successors. Let $r_{A}(\delta_{G}(x))=(s_{x},\gamma_{x},c_{x})$ and
$r_{A}(\delta_{G}(z))=(s,\gamma,c)$. Then we have $\mathit{as}(z)=(s,\gamma
w)$ for a $w\in\Gamma^{*}\bot$. Since
$r(\delta_{G}(z))=(l(z),\mathit{callRet},p(z))$,
$\rho(r_{A}(\delta_{G}(z)),r(\delta_{G}(z)))$ is a disjunction of formulae of
the form
$(0,(s^{\prime},\gamma^{\prime},(s_{r},\gamma_{r})))\land(1,(s^{\prime\prime},\gamma^{\prime\prime},c))$
with $s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}$ and
$s_{r}\gamma_{r}\rightarrow s^{\prime\prime}\in\Delta_{R}$. Thus,
$r_{A}(\delta_{G}(z^{\prime}))=(s^{\prime},\gamma^{\prime},(s_{r},\gamma_{r}))$
as well as $r_{A}(\delta_{G}(y))=(s^{\prime\prime},\gamma^{\prime\prime},c)$
for some $s^{\prime},s^{\prime\prime},s_{r}\in S$ and
$\gamma^{\prime},\gamma^{\prime\prime},\gamma_{r}\in\Gamma$ with
$s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}$ and
$s_{r}\gamma_{r}\rightarrow s^{\prime\prime}\in\Delta_{R}$. By $(*)$ we infer
$c_{x}=(s_{r},\gamma_{r})$. Moreover, since $x$ has a
$\mathit{ret}$-successor, we have $d(x)=\mathit{ret}$ and thus
$\rho(r_{A}(\delta_{G}(x)),r(\delta_{G}(x)))$ is $\mathit{true}$, if
$s_{x}=s_{r}$ and $\gamma_{x}=\gamma_{r}$, and $\mathit{false}$ otherwise.
Since the transition function must be satisfied by the children of
$\delta_{G}(x)$, we thus have $s_{x}=s_{r}$ and $\gamma_{x}=\gamma_{r}$, i.e.
$\mathit{as}(x)=(s_{r},\gamma_{r}w^{\prime})$ for a
$w^{\prime}\in\Gamma^{*}\bot$. By construction of $\mathit{as}$, we clearly
have $w^{\prime}=\gamma^{\prime\prime}w$. Thus, since
$\mathit{as}(x)=(s_{r},\gamma_{r}\gamma^{\prime\prime}w)$,
$\mathit{as}(y)=(s^{\prime\prime},\gamma^{\prime\prime}w)$ and
$s_{r}\gamma_{r}\rightarrow s^{\prime\prime}\in\Delta_{R}$, we have
$\mathit{as}(x)\rightarrow_{\mathit{ret}}\mathit{as}(y)$.

Finally, let $x\in V$ be a node without successors. Then we have
$r(\delta_{G}(x))=(l(x),\mathit{end},p(x))$. Let
$r_{A}(\delta_{G}(x))=(s,\gamma,c)$, i.e. $\mathit{as}(x)=(s,\gamma w)$ for
some $w\in\Gamma^{*}\bot$. Assume towards contradiction that we have
$c=(s_{r},\gamma_{r})$ for some $s_{r}\in S$ and $\gamma_{r}\in\Gamma$. By
$(*)$, there are $v_{1},v_{2},v_{3}\in V$ with
$v_{1}\rightarrow^{\mathit{call}}v_{2}$ and $v_{1}\curvearrowright v_{3}$ and
there is a path from $v_{2}$ to $x$ following abstract successors. Thus,
$\delta_{G}(x)$ is the $\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of
the left child $\delta_{G}(v_{2})=\delta_{G}(v_{1})\cdot 0$ of the parent node
$\delta_{G}(v_{1})$ of $\delta_{G}(v_{3})=\delta_{G}(v_{1})\cdot 1$. Then we
have
$\mathit{succ}_{\uparrow}^{\mathcal{T}(G)}(\delta_{G}(v_{3}))=\delta_{G}(x)$.
Using Lemma 1, we obtain
$\delta_{G}(\mathit{succ}_{\uparrow}^{G}(v_{3}))=\mathit{succ}_{\uparrow}^{\mathcal{T}(G)}(\delta_{G}(v_{3}))=\delta_{G}(x)$
and thus $\mathit{succ}^{G}_{\uparrow}(v_{3})=x$ since $\delta_{G}$ is
injective. This means that $v_{3}$ is a successor of $x$, which contradicts
our assumption that $x$ has no successor. Thus, we must have $c=\bot$, i.e.
$\rho(r_{A}(\delta_{G}(x)),r(\delta_{G}(x)))$ is $\mathit{true}$, if there is
no rule for $s\gamma$ in $\Delta$, and $\mathit{false}$ otherwise. Since the
transition function must be satisfied by the children of $\delta_{G}(x)$,
there is thus no successor of $\mathit{as}(x)$. ∎