Database Reference
In-Depth Information
Clearly,
T
1
⊕
m
T
2
⊕
m
···⊕
m
T
n
is a safe extension of
T
i
for each
i
,so
Lemma 12.24
follows from the following fact.
Lemma 12.26
Fix a pattern
π
, a natural number m
≥
π
, a kind K together with an
extended run with margins of size m, and a tree T
L
(
K
)
. For each m-safe extension T
of
∈
T
T
|
=
π
(
a
)
whenever T
|
=
π
(
a
)
.
Proof
Fix
a
such that
T
|
=
π
(
a
) and a witnessing homomorphism
h
:
π
→
T
.Wedefine
's vertices, such that a homomorphism
h
:
T
can be
a partition
V
of
V
π
,thesetof
π
π
→
defined independently on each part as long as some simple rules are satisfied.
The areas potentially affected by the extension are the
T
u
's. We associate with
u
aset
Z
u
such that
T
u
⊆
T
u
, where the homomorphism can be modified independently of the
rest of the tree. If for some
u
the image of
h
is disjoint from
T
u
,take
Z
u
= 0. If
T
u
is not
disjoint from the image of
h
, there are three cases, depending on the type of
u
.
Z
u
⊆
If
u
is a forest port, then
T
u
=
M
+
T
u
+
N
and since the image of
h
has cardinality
at most
Case 1
and is not disjoint from
T
u
, by the pigeon-hole principle there exist
roots
v
in
M
and
v
in
N
outside of the image of
h
. (If there is choice, choose the
ones closest to
T
u
.) Let
Z
u
be the forest of trees rooted at the sequence of siblings
between
v
and
v
(excluding
v
and
v
).
π
Case 2
If
u
is a tree port, then
T
u
=
M
T
u
and there exists a node
v
in
M
on the pathfrom
the root to the port, closest to
T
u
, that is not in the image of
h
.Let
Z
u
=
T
.
v
.
·
If
u
is a context port, then
T
u
=
M
Case 3
N
, and one can find
v
on the path from the
root to the port in
M
and
v
on the path from the root to the port in
N
, closest to
T
u
, that are not in the image of
h
.Let
Z
u
=
T
.
v
·
T
u
·
T
.
v
.
−
The sets
Z
u
need not be disjoint, but we can pick a pairwise disjoint subfamily
covering
all the sets
T
u
that intersect the image of
h
. To prove this, we first show by case analysis
that for each
u
,
u
either
T
u
⊆
Z
Z
u
,or
Z
u
and
Z
u
are disjoint. In fact, in all
cases except the last one,
Z
u
and
Z
u
either are disjoint or one is contained in the other.
Z
u
,or
T
u
⊆
•
For two forest ports, we are dealing with two forests whose roots are children of some
nodes
w
and
w
. If such forests are not disjoint, and neither is contained in a subtree of
the other, then they share one of the roots. But this is impossible: two sibling ports are
always separated by a margin, which must contain a node that is not in the image of
h
;
the associated forests are disjoint because they were chosen minimal.
•
For a tree port and a forest port (or a tree port), the corresponding sets are: a subtree,
and a subforest whose roots are siblings. Such sets are always either disjoint, or one is
contained in the other.
•
For a context port and a tree port, whose corresponding sets are not disjoint and neither is
contained in the other, the root of the tree must be contained in the path between the root
and the port of the context. But this would mean that the margin paths of the two ports
