Information Technology Reference
In-Depth Information
Appendix: Proof of Theorem 1
The proof proceeds by induction on the construction of
P
. Two cases are of special
interest: Parallel composition because it is the only case that uses lemma 2 and external
choice because, as explained in Section 3, hiding of initial events of the external choice's
operands disallows distributivity of hiding over external choice in general. See the [6]
for the whole proof.
Parallel Composition
:
Ext
(
P |
A
|
Q
)
=
Lemma 1 and
T
(
P |
A
| Q
)
Hr
(
T
(
P
)
|
{s.x,e.x|x∈A}
| T
(
Q
))
=
Lemma 2
Hr
(
T
(
P
)
|
{s.x|x∈A}
| T
(
Q
))
=
distributivity of hiding and renaming over
|
{s.x|x∈A}
|
Hr
(
T
(
P
))
|
A
| Hr
(
T
(
Q
))
=
Lemma 1
Ext
(
P
)
|
A
| Ext
(
Q
)
=
induction hypothesis
P |
A
| Q .
External Choice
:
Ext
(
P Q
)
=
Lemma 1 and
T
(
P
Q
)
Hr
(
T
(
P
)
T
(
Q
))
=
definition of
Hr
(
T
(
P
)
T
(
Q
))
\ H
Hr
[
s.x ← x | x ∈ Σ
P
∪ Σ
Q
]
=
T
distributivity of hiding over
in
T
(
T
(
P
)
\ H
Hr
T
(
Q
)
\ H
Hr
)[
s.x ← x | x ∈ Σ
P
∪ Σ
Q
]
= distributivity of renaming over
T
(
P
)
\ H
Hr
[
s.x ← x | x ∈ Σ
P
]
T
(
Q
)
\ H
Hr
[
s.x ← x | x ∈ Σ
Q
]
=
definition of
Hr
and Lemma 1
Ext
(
P
)
Ext
(
Q
)
=
induction hypothesis
P Q .
Search WWH ::
Custom Search