Equivalence of the two models

To express the equivalence of the two semantics defined above, we remove the pids from the local semantics. This is done by a function $\mbox{\tt RmPids}$ which removes the pids from the local semantic primitives to obtain the semantic primitives of the global semantics. Then we prove, for a non-nested Splice program $S$, that

$$\mbox{$[\![\:$}S\mbox{$\:]\!]$} = \mbox{\tt RmPids}( \mbox{\tt {SemL}$($}S\mbox{$)$} ).$$

The main issues in the proof concern:

1. The equivalence for the ${\tt Close}$-operator, especially showing that we can construct a global order for the global semantics, given the local orders for the processes in the local semantics.
2. The existence of a $\mbox{\it pid}$ assignment, satisfying the constraints, for the local semantics, given a semantic primitive in the global semantics of a non-nested Splice program.

Since both issues involve quite some technical detail and proof effort, they are separated by introducing an intermediate semantics for non-nested Splice programs $S$ with initial state $s$, denoted $\mbox{\tt {SemG}$($}S\mbox{$)$}(s)$, where we have added a $\mbox{\it pid}$-field to the global semantics. For $\mbox{\tt {SemG}$($}S\mbox{$)$}(s)$, the semantics of the ${\tt Close}$-operator equals the one for the global semantics plus the constraint on pids of the local semantics. All other statements have the local semantics, which equals the global one plus constraints on pids. Then the proof is split into the following two lemmas, corresponding to the two issues above:

1. $\mbox{\tt {SemL}} = \mbox{\tt {SemG}}$. An outline of the proof can be found in section 5.1.
2. $\mbox{$[\![\:$}S\mbox{$\:]\!]$} = \mbox{\tt RmPids}( \mbox{\tt {SemG}$($}S\mbox{$)$} )$. The proof of this property is sketched in section 5.2.

For more details we refer to the technical report [1].