Existence of pids

To prove $\mbox{$[\![\:$}S\mbox{$\:]\!]$} = \mbox{\tt RmPids}( \mbox{\tt {SemG}$($}S\mbox{$)$} )$, first observe that one direction is quite obvious. Recall that $\mbox{\tt RmPids}$ removes the pid field of a local semantic primitive $\mbox{\it lsp}$. Hence, $\mbox{\it lsp}\in \mbox{\tt {SemG}$($}S\mbox{$)$} (s)$ implies $\mbox{\tt RmPids}(\mbox{\it lsp}) \in \mbox{$[\![\:$}S\mbox{$\:]\!]$} (s)$. This has been proved in PVS by induction on $S$; all cases for the language constructs could be proved automatically.

Next consider the other direction, i.e., $sp \in \mbox{$[\![\:$}S\mbox{$\:]\!]$} (s)$ implies that there exists a local semantic primitive $\mbox{\it lsp}$ such that $\mbox{\tt RmPids}(\mbox{\it lsp}) = sp$ and $\mbox{\it lsp}\in \mbox{\tt {SemG}$($}S\mbox{$)$} (s)$. The problem here is to construct a $\mbox{\it pid}$-field that can be added to $sp$, 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 $S$ does not contain any parallel composition, all events should have the same pid. Otherwise, since $S$ 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 $sp \in \mbox{$[\![\:$}S\mbox{$\:]\!]$} (s)$ then

a)

if $S$ does not contain parallel composition then for each pid $p$ there exists an $\mbox{\it lsp}$ such that $\mbox{\tt RmPids}(\mbox{\it lsp}) = sp$, $\mbox{\it lsp}\in \mbox{\tt {SemG}$($}S\mbox{$)$} (s)$ and $\forall E \in \mbox{\it evs}(\mbox{\it lsp}) [ \mbox{\it pid}(\mbox{\it lsp})(E) = p]$;

b)

otherwise, for each set of pids $\mbox{\it pset}$ there exists a local semantic primitive $\mbox{\it lsp}$ such that $\mbox{\tt RmPids}(\mbox{\it lsp}) = sp$, $\mbox{\it lsp}\in \mbox{\tt {SemG}$($}S\mbox{$)$} (s)$ and $\forall E \in \mbox{\it evs}(\mbox{\it lsp}) [ \mbox{\it pid}(\mbox{\it lsp})(E) \notin \mbox{\it pset}]$.

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 $S$.