Information Technology Reference
In-Depth Information
cl
(
F
{
μX.E/X
}
)
=
cl
(
μY.F
1
{
μX.E/X
}
)
F
{
F
∈
=
{
μY.F
1
{
μX.E/X
}
/Y
}|
cl
(
F
1
{
μX.E/X
}
)
}
def. of
cl
F
{
⊆{
μY.F
1
{
μX.E/X
}
/Y
}|
F
∈{
F
1
{
F
1
∈
μX.E/X
}|
cl
(
F
1
)
}∪
cl
(
μX.E
)
}
ind. hyp.
=
{F
1
{μX.E/X}{μY.F
1
{μX.E/X}/Y }|F
1
∈
cl
(
F
1
)
}
∪{
F
{
F
∈
μY.F
1
{
μX.E/X
}
/Y
}|
cl
(
μX.E
)
}
=
{
F
1
{
μY.F
1
/Y
}{
μX.E/X
}|
F
1
∈
cl
(
F
1
)
}
F
|
F
∈
∪{
cl
(
μX.E
)
}
∗∗
{
F
{
μX.E/X
}|
F
∈{
F
1
{
μY.F
1
/Y
}|
F
1
∈
cl
(
F
1
)
}}
=
∪
cl
(
μX.E
)
F
{
F
∈
=
{
μX.E/X
}|
cl
(
μY.F
1
)
}∪
cl
(
μX.E
)
def. of
cl
Here we explain the step marked
above, keep in mind that
Y
does not occur
free in
μX.E
. With such condition on variable, first by the well known substitu-
tion lemma in this case we have
∗∗
F
1
{
=
F
1
{
μY.F
1
/Y
}{
μX.E/X
}
μX.E/X
}{
μY.F
1
{
μX.E/X
}
/Y
}
.
Second, for
F
cl
(
μX.E
) by Lemma 2
fv
(
F
)
∈
⊆
fv
(
μX.E
), thus
Y
does not
occur free in
F
,so
F
{
=
F
.
μY.F
1
{
μX.E/X
}
/Y
}
Other cases are trivial.
When confusion is unlikely, for
α
∈S
we will also write
α
to mean the set of
expressions which occur in
α
.
a
−→
Lemma 4.
If
α
β
then
β
∪
cl
(
β
)
⊆
α
∪
cl
(
α
)
.
a
−→
Proof:
First, we have the fact: if
E
cl
(
E
). This can be
proved by induction on the rules of Table 2, where for rule
rec
we need to use
Lemma 3.
Suppose
α
β
then
β
∪
cl
(
β
)
⊆
a
−→
β
, then by the rules of Table 2 it must be that
α
=
Eα
,
a
−→
β
=
β
α
,and
E
β
for some
E, α
,β
.Bythefactabove
β
∪
cl
(
β
)
⊆
cl
(
E
),
cl
(
β
)=
β
∪
α
∪
cl
(
β
)
cl
(
α
)
α
∪
cl
(
α
)
thus
β
∪
∪
⊆
cl
(
E
)
∪
⊆
α
∪
cl
(
α
).
With this lemma, by transitivity it is easy to see that if
β
is reachable from
α
then
β
cl
(
α
), and in particular we have the following theorem which
we aimed at from the beginning.
∪
cl
(
β
)
⊆
α
∪
Theorem 1.
If
β
is reachable from
α
then
β
⊆
α
∪
cl
(
α
)
.
With this theorem, when we discuss bisimulation equivalence of two states
α, β
∈
S
we know that the reachable state space is the part consisting of states in which
only processes from a finite set
α
cl
(
β
) can occur. Thus, in the
discussion of the next section we can assume that the relevant state space
∪
β
∪
cl
(
α
)
∪
S
is
S⊆P
∗
.
of this kind. That is there is a finite process set
P
such that
Search WWH ::
Custom Search