Database Reference
In-Depth Information
Lemma 12.23
For every UNFTA
A
and a tree T
∈
L
(
A
)
and m
∈
N
there is an
A
-
kind K with height and branching at most
(2
m
+1)
A
, admitting an accepting run with
margins of size m, such that T
∈
L
(
K
)
.
Proof
Argue just like for
Lemma 12.20
, only keep margins of size
m
around ports: for
SCCs of horizontal automata and nonbranching SCCs of
keep
m
initial and
m
final
steps of the run within the SCC, and for branching SCCs keep the
m
final steps (looking
bottom-up).
A
In the combining procedure, instead of the
T
u
's we use larger forest/contexts, encom-
passing the margins. Fix a run
λ
over
K
with margins of length
m
.Foratree
T
∈
L
(
K
),a
m
,define
T
u
as an extension of
T
u
by
k
nodes along the margins, i.e.,
using the notation in
Definition 12.22
:
port
u
in
K
,and
k
≤
if
u
is a
p
-port, let
T
u
=
T
.
v
k
;
•
if
u
is a
p
,
p
-port, then
T
u
is the context obtained from
T
.
v
−
k
by replacing
T
.
v
k
with a
port;
•
∑
−
1
i
=
if
u
is a
q
,
q
-port, let
T
u
=
i
=1
T
.
v
i
;
•
k
T
.
v
i
+
T
u
+
∑
−
where
v
denotes the node in
T
corresponding to
v
,and
T
.
w
denotes the subtree of
T
rooted
at
w
. In particular,
T
u
=
T
u
.
Note that in
T
L
(
K
), then the
T
u
's need not be disjoint. This means that combining
n
trees one by one would result in an exponential overhead. In consequence, we have to
combine them in one go by concatenating the forests or contexts replacing
u
in all
n
trees.
Fix a run
∈
over
K
with margins of size
m
, together with the witnessing horizontal runs,
and let
T
1
,
T
2
,...,
T
n
∈
L
(
K
).For
i
= 1
,
2
,...,
n
fix a run λ
i
compatible with λ , witnessing
that
T
i
∈
L
(
K
). We build
λ
T
1
⊕
m
T
2
⊕
m
···⊕
m
T
n
∈
L
(
K
)
by substituting at each port
u
in
K
the following forest or context
F
1
+(
T
1
)
u
+
F
2
+(
T
2
)
u
+
•
···
+
F
m
+1
if
u
is a forest port, or
(
T
1
)
u
·
(
T
2
)
u
·
•
C
1
·
C
2
·
...
·
C
m
+1
if
u
is a context port, or
M
1
((
T
1
)
u
,
M
2
((
T
2
)
u
,...
M
n
−
1
((
T
n
−
1
)
u
,
(
T
n
)
u
)
...
)) if
u
is a tree port,
•
where
F
i
are compatible forests,
C
i
are compatible contexts, and
M
i
are compatible
multicontexts with two ports. The existence of small
F
i
's,
C
i
's, and
M
i
's follows from
Lemma 12.18
and the fact that along the margins the runs stay within a single SCC (a
branching one in the case of tree ports). In this way we obtain a tree of size at most
|
+(
n
+1)
c
,where
c
is a constant independent of the
T
i
's, single-
K
|
|
T
1
|
+
|
T
2
|
+
···
+
|
T
n
|
exponential in
A
.
Correctness of the construction is guaranteed by the following lemma.
