Information Technology Reference
In-Depth Information
(i)
s
−ₒ
. Here
V
(
s
)
={
0
}
and since
V
(
ʘ
) is not empty we clearly have that
V
(
s
)
≤
Ho
V
(
ʘ
).
ˉ
−ₒ
ˉ
−ₒ
ʔ
for some
ʔ
. Here
ʘ
(
ʘ
)
(ii)
s
V
(
s
)
={
1
}
and
ʘ
⃒
with
V
={
1
}
.
By Lemma
6.32
specialised to full distributions, we have 1
∈
V
(
ʘ
). Therefore,
V
(
s
)
≤
Ho
V
(
ʘ
).
s
)
†
ʘ
. Use Proposition
6.2
to decompose
Now for the general case we suppose
ʔ
(
ʘ
into
s
∈
ʔ
ʔ
(
s
)
·
ʘ
s
such that
s
s
ʘ
s
for each
s
∈
ʔ
, and recall each
such state
s
is stable. From above, we have that
V
(
s
)
≤
Ho
V
(
ʘ
s
) for those
s
, and so
=
∈
ʔ
≤
Ho
s
∈
ʔ
V
(
ʔ
)
ʔ
(
s
)
·
V
(
s
)
ʔ
(
s
)
·
V
(
ʘ
s
)
=
V
(
ʘ
).
Lemma 6.45
Let ʔ and ʘ be distributions in an ˉ-respecting finitary pLTS given
s
)
†
ʘ, then we have
by
S
,
{
˄
,
ˉ
}
,
ₒ
.Ifʔ
(
V
(
ʔ
)
≤
Ho
V
(
ʘ
)
.
ʔ
;by
distillation of divergence (Theorem
6.11
) we have full distributions
ʔ
,
ʔ
1
and
ʔ
2
and probability
p
such that
s
s
)
†
ʘ
, we consider subdistributions
ʔ
with
ʔ
Proof
Since
ʔ
(
⃒
ʔ
=
(
ʔ
1
p
↕
ʔ
2
) and
ʔ
=
ʔ
1
and
ʔ
2
⃒
⃒
p
·
ʘ
such that
ʔ
(
s
)
†
ʘ
.By
ʵ
. There is, thus, a matching transition
ʘ
⃒
Proposition
6.2
, we can find distributions
ʘ
1
,
ʘ
2
such that
ʘ
=
ʘ
1
p
↕
ʘ
2
,
ʔ
1
(
s
)
†
ʘ
1
and
ʔ
2
(
s
)
†
ʘ
2
.
ʔ
1
=
ʔ
we have that
ʔ
1
is stable. It follows from Lemma
6.44
that
Since
(
ʔ
1
)
(
ʘ
1
). Thus we finish off with
V
≤
Ho
V
(
ʔ
)
V
ʔ
1
)
ʔ
=
ʔ
1
=
V
(
p
·
p
·
(
ʔ
1
)
=
p
·
V
linearity of
V
(
ʘ
1
)
≤
Ho
p
·
V
above argument based on distillation
ʘ
1
)
=
V
(
p
·
linearity of
V
(
ʘ
)
ʘ
=
ʘ
1
p
↕
ʘ
2
≤
Ho
V
≤
Ho
V
(
ʘ
)
.
Lemma
6.32
specialised to full distributions
Since
ʔ
was arbitrary, we have our result.
Lemma 6.46
Let ʔ and ʘ be distributions in an ˉ-respecting finitary pLTS given
by
S
,
{
˄
,
ˉ
}
,
ₒ
.Ifʔ
S
ʘ, then it holds that
V
(
ʔ
)
≤
Ho
V
(
ʘ
)
.
S
ʘ
. By Lemma
6.43
, there exists some distribution
ʘ
match
Proof
Suppose
ʔ
ʘ
match
s
)
†
ʘ
match
. By Lemmas
6.45
and
6.32
we obtain
such that
ʘ
⃒
and
ʔ
(
(
ʘ
)
V
(
ʔ
)
≤
Ho
V
ↆ
V
(
ʘ
).
Theorem 6.18
For any finitary processes P and Q,ifP
S
Q then P
pmay
Q.
Search WWH ::
Custom Search