** Next:** Related work
** Up:** Equivalence of the two
** Previous:** Equivalence of the two

##

Existence of pids

To prove
,
first observe that one direction is quite obvious.
Recall that
removes the pid field of a local semantic primitive
.
Hence,
implies
.
This has been proved in PVS by induction on ;
all cases for the language constructs could be
proved automatically.
Next consider the other direction, i.e.,
implies that there exists a local semantic
primitive
such that
and
.
The problem here is to construct
a
-field that can be added to ,
i.e., a function from the events to process identifiers,
which satisfies the constraints of the semantics.
Recall that for sequential composition, the pids of events of the components
should be equal, whereas for parallel composition they have to be
different.
Hence, as long as does not contain any parallel composition,
all events should have the same pid.
Otherwise, since is non-nested, we only have to deal with
parallel composition and closure operations and then
it is important to be able to choose different pids.

To formalize this, we have proved a stronger lemma expressing that
if
then

- a)
- if does not contain parallel composition
then for each pid
there exists an
such that
,
and
;
- b)
- otherwise, for each set of pids
there exists a local semantic primitive
such that
,
and
.

Additionally, we have to assume that there are sufficiently many
process identifiers.
Then the lemma is strong enough to be proved by
induction on the structure of program .

** Next:** Related work
** Up:** Equivalence of the two
** Previous:** Equivalence of the two
Roel Bloo
1999-11-26