Database Reference
In-Depth Information
are not disjoint, which implies that the SCCs associated with the ports are the same. This
leads to a contradiction, as one was assumed branching and the other nonbranching.
•
For two context ports, if the contexts are not disjoint and neither is contained in the
other, the root of one of them lies on the path between the root and the port of the other.
Like above, in this case both ports are associated with the same SCC. Moreover, since
the SCC is nonbranching, the two ports are on the same branch of
K
(otherwise, the two
margin paths would branch). It follows that the ports are separated by a node that is not
in the image of
h
, which guarantees disjointness of the associated contexts.
Finally, for a context port
u
and a forest port
u
, we are dealing with a context
T
.
v
T
.
v
,
and a forest whose roots are children of a single node
w
. If such sets are not disjoint
and neither is contained in the other, the node
w
must lie on the path between
v
and
v
(excluding
v
). The margin path around
u
in
K
cannot contain other ports, which means
that the set
T
u
is disjoint from this path. As
v
liesonthispath,
T
u
does not contain
v
.
It follows that
T
u
⊆
Z
u
.
•
−
To construct
Z
start with
Z
= 0 and for each port
u
make sure that
T
u
is covered: let
(
u
)=
Z
Z
(
u
),then
T
u
is already covered
and we can proceed to the next port; otherwise, by the observation above,
T
u
⊆
Z
u
for all
u
such that
Z
u
∈Z
∈Z |
Z
∩
Z
u
= 0
}
;if
T
u
⊆
Z
for some
Z
∈Z
{
h
−
1
(
Z
)
(
u
), and we replace
Z
with
Z −Z
(
u
)
∪{
Z
u
}
.Let
V
=
|
Z
∈
Z }∪{
V
π
−
h
−
1
(
Z
and denote
V
u
=
h
−
1
(
Z
u
).
Since
h
−
1
(
Z
) covers all vertices of π mapped to
u
T
u
,for
x
∈
V
π
−
h
−
1
(
Z
),
h
(
x
)=
w
is a vertex from the fixed area of
T
, and hence has its counterpart
w
in
T
.Let
h
(
x
)=
w
. Now let us see how to define
h
on
V
u
∈ V
)
}
.Since
T
is a safe extension of
T
,the
forest/context substituted at
u
in
T
contains a copy of
Z
u
, which in turn contains
h
(
V
u
).
We define
h
on
V
u
by transferring
h
from
Z
u
to its copy in
T
. To prove that this gives a
homomorphismwe need to check that no relation between vertices of
π
is violated. We are
going to show that each relation between
x
V
u
must be witnessed by a path
visiting a
critical node
in the fixed part of
T
induced by
K
, and that in
T
the witnessing
paths to the critical nodes exist as well. Since the critical nodes are in the fixed part, the
relations between them are the same in
T
and in
T
and the correctness of
h
follows.
Suppose first that
u
is a forest port. Let us analyze the possible relations in
∈
V
u
and
y
/
∈
π
between
x
and
y
. First, we exclude some possibilities. The case (
x
↓
y
) is impossible, because it
would mean that
h
(
y
) is a child of
h
(
x
), and since
h
(
x
)
∈
Z
u
, it would follow that
h
(
y
)
∈
Z
u
,
V
u
=
h
−
1
(
Z
u
). Similarly, the cases (
x
+
y
)
contradicting the fact that
y
/
∈
→
y
)
,
(
y
→
x
)
,
(
x
↓
x
),then
h
(
y
)=
w
, the parent of
v
and
v
. In the remaining cases,
are impossible. If (
y
↓
+
x
), one checks easily that the witnessing paths must visit
w
,
v
,
and
v
, respectively. Note that
w
,
v
,
v
are vertices of
K
and have their counterparts in
T
.
After transferring the image of
V
u
to the copy of
Z
u
contained in
T
u
as a subforest, the child
and descendant relation with
w
and the following-sibling relation with
v
,
v
are preserved.
If
u
is a tree port, the only possible edge between
x
+
x
)
,
(
x
+
y
)
,
(
y
(
y
↓
→
→
+
x
),andthe
witnessing path must visit
v
. Hence, the image of
V
u
can be transferred to the copy of
Z
u
contained in
T
u
, without violating the existence of witnessing paths.
∈
V
u
and
y
/
∈
V
u
is (
y
↓
