<figure><img src="image_52.png" /><figcaption>Fig. 46. Description of instantiated transitions of $\sigma \otimes \tau$</figcaption></figure>

<figure><img src="image_53.png" /><figcaption>Fig. 47. Projections of instantiated transitions</figcaption></figure>

## D.2 PStrat as an IPA-Structure: Operations

We examine the operations involved in the IPA-structure, and show preservation of Petri strategies.

### D.2.1 Tensor.
The preservation of Petri strategies by the tensor operation is a simplification of composition, without the synchronized events.

**LEMMA D.11.** Consider $\sigma$ and $\tau$ Petri structures.

Then, instantiated transitions of $\sigma \otimes \tau$ are exactly as in Figure 46 – in the sense that there is a one-to-one correspondence between instantiated transitions in the premises and in the conclusion.

Using this description, we define in Figure 47 partial functions $\pi_{\sigma}^{\otimes}: \mathscr{E}_{\sigma \otimes \tau} \to \mathscr{E}_{\sigma}$ and $\pi_{\tau}^{\otimes}: \mathscr{E}_{\sigma \otimes \tau} \to \mathscr{E}_{\tau}$ extracting various data from instantiated transitions, following the characterization of instantiated transitions of $\sigma \otimes \tau$ given in Figure 46.

Finally, those projection functions are extended to instantiated transitions in context via:

$$ 
\begin{aligned}
\pi_{\sigma}^{\otimes} &: \mathcal{F}_{\sigma \otimes \tau} \quad \to \quad \mathcal{F}_{\sigma} \\
\mathbf{e} \uplus (\gamma + \otimes \gamma') &\mapsto \pi_{\sigma}^{\otimes}(\mathbf{e}) \uplus \gamma \\
\pi_{\tau}^{\otimes} &: \mathcal{F}_{\sigma \otimes \tau} \quad \to \quad \mathcal{F}_{\tau} \\
\mathbf{e} \uplus (\gamma + \otimes \gamma') &\mapsto \pi_{\tau}^{\otimes}(\mathbf{e}) \uplus \gamma'.
\end{aligned}
$$

Using these, from a run $\rho: \emptyset \to \sigma \otimes \tau$ we extract:

$$ \rho_{\sigma} = \rho \upharpoonright \pi_{\sigma}^{\otimes}, \qquad \rho_{\tau} = \rho \upharpoonright \pi_{\tau}^{\otimes}, $$
we will also use for restriction the partial functions

<figure><img src="image_54.png" /></figure>

which allow us to prove the following property:

**LEMMA D.12.** Consider $\rho : \emptyset \longrightarrow_{\sigma \otimes \tau} \alpha$. Then, $\alpha = \alpha_{\sigma} + \otimes \alpha_{\tau}$ and
$$ \rho_{\sigma} : \emptyset \longrightarrow \alpha_{\sigma}, \qquad \rho_{\tau} : \emptyset \longrightarrow \alpha_{\tau}. $$

where $\text{play}(\rho_{\sigma}) = \text{play}(\rho) \upharpoonright u$ and $\text{play}(\rho_{\tau}) = \text{play}(\rho) \upharpoonright d$.
Moreover, $\text{Coll}(\rho) = \text{Coll}(\rho_{\sigma}) + \otimes \text{Coll}(\rho_{\tau})$.

**PROOF.** Exactly as for Lemma D.4, without synchronized transitions. $\square$

<figure><img src="image_55.png" /></figure>

Next, as for composition, we observe that these projections preserve valid plays. For that we shall first need the following easy lemma:

**LEMMA D.13.** Consider A, B arenas, and $s \in |A \otimes B|^*$.
Then, $s \in \text{Plays}(A \otimes B)$ iff $s \upharpoonright \ell_{\circ}^* \in \text{Plays}(A)$ and $s \upharpoonright r_{\circ}^* \in \text{Plays}(B)$.

**PROOF.** Straightforward.

<figure><img src="image_56.png" /></figure>

Using this and Lemma D.12, we show that projections preserve valid runs. Consider $\sigma : A_1 \vdash B_1$ and $\tau : A_2 \vdash B_2$ Petri strategies.

**LEMMA D.14.** Consider $\rho : \emptyset \longrightarrow_{\sigma \otimes \tau} \alpha$ such that play($\rho$) $\in$ $\text{Plays}(A_1 \otimes A_2 \vdash B_1 \otimes B_2)$.
Then, $\text{play}(\rho_{\sigma}) \in \text{Plays}(A_1 \vdash B_1)$ and $\text{play}(\rho_{\tau}) \in \text{Plays}(A_2 \vdash B_2)$.

**PROOF.** As for the proof of Lemma D.6 (without synchronization), using condition valid of Petri strategies along with Lemma D.13. $\square$

<figure><img src="image_57.png" /></figure>

Using Lemmas D.12, D.13, and D.14, we prove as for Proposition D.7:

**PROPOSITION D.15.** If $\sigma : A_1 \vdash B_1$ and $\tau : A_2 \vdash B_2$ are Petri strategies, so is $\sigma \otimes \tau : A_1 \otimes B_1 \vdash A_2 \otimes B_2$.
Moreover, if $\sigma$ and $\tau$ are negative, so is $\sigma \otimes \tau$.

### D.2.2 Renamings.
Before we go on to currying and promotion, we introduce a technical tool useful in ensuring that they preserve Petri strategies.

First, for any game A we write $\text{Plays}_{\_}(A)$ for the set of **negative plays** on A, i.e. those $s_1...s_n \in \text{Plays}(A)$ such that $\text{pol}(s_1) = -$. If $f : \text{ Moves} \to \text{ Moves}$ and $s = s_1...s_n \in \text{Plays}(A)$ such that $f$ is defined on $|A|$, then we write $f(s) = f(s_1)...f(s_n)$. In the sequel, we should be particularly interested in such functions on moves that can be decomposed in $f$ and $(g_m)_{m \in \text{dom}(f)}$ where

$f : \mathcal{M} \to \mathcal{M}, \qquad g_m : \text{Tok} \to \text{Tok},$

in which case we obtain a partial function between moves set as

$[f, (g_m)] : \begin{array}{c} \text{ Moves} \\ (m, s, d) \end{array} \to \begin{array}{c} \text{ Moves} \\ (f(m), s', d') \end{array}$
where $(s', d') = g_m(s, d)$.

**Definition D.16.** Consider A, B games, $f, (g_m)$ s.t. $[f, (g_m)] : \text{ Moves} \to \text{ Moves}$ partial injection.
We say $h = [f, (g_m)]$ is a **global renaming** from A to B, written $[f, (g_m)] : A \rightsquigarrow B$, if:
defined: for all $a \in |A|$, $h(a)$ defined.

polarity-preserving: $\forall a \in |A|$, $\text{pol}(ha) = \text{pol}(a)$

validity: $\forall s \in \text{Plays}_-(A)$, $h(s) \in \text{Plays}_-(B)$

receptivity: for all $s \in \text{Plays}_-(A)$, for all $h(s)b^- \in \text{Plays}_-(B)$, there exists $sa^- \in \text{Plays}_-(A)$ such that $h(a) = b$.

courtesy: for all $a \dashrightarrow_A b$, either $h(a) \dashrightarrow_B h(b)$ or $(\text{pol}(a), \text{pol}(b)) = (-, +)$.

Global renamings are used to transport Petri strategies across games. The following definition, first applied simply on Petri structures, extends Definition B.1 in that it also renames tokens rather than merely rerouting visible transitions.

**Definition D.17.** Consider A, B games, $\sigma$ a Petri structure on mult(A), and $h = [f, (g_m)] : A \rightsquigarrow B$. We define the renaming $\sigma[h]$ on mult(B), with the same components as $\sigma$, except:

$$ 
\begin{align*}
\partial_{\sigma[h]}(t) &= f(\partial_{\sigma}(t)) \\
\delta_{\sigma[h]}\langle t^+ \rangle(\alpha) &= g_m(\delta_{\sigma}\langle t^+ \rangle(\alpha)) && \text{for } m = \partial_{\sigma}(t^+) \\
\delta_{\sigma[h]}\langle t^- \rangle(g_m(s, d)) &= \delta_{\sigma}\langle t^- \rangle(s, d) && \text{for } m = \partial_{\sigma}(t^-).
\end{align*}
$$

observing that by hypothesis, $g_m$ is injective for all $m \in \text{dom}(f)$.

In order to use global renaming to transport Petri strategies, we must transport valid runs. Consider A, B games, $h = [f, (g_m)] : A \rightsquigarrow B$, and $\sigma : A$ a Petri strategy. Then we set

$$ 
\begin{array}{rcl}
-[h] : & \mathscr{E}_{\sigma} & \rightarrow \mathscr{E}_{\sigma[h]} \\
& t^0\langle\alpha\rangle & \mapsto t^0\langle\alpha\rangle \\
& t^{-}\langle(s, d)\rangle & \mapsto t^{-}\langle g_m(s, d)\rangle \quad \text{where } m = \partial_{\sigma}(t^{-}) \\
& t^{+}\langle\alpha\rangle & \mapsto t^{+}\langle\alpha\rangle
\end{array}
$$

extended to instantiated transitions in context with $(e \stackrel{\psi}{\rightarrow} \gamma)[h] = e[h] \stackrel{\psi}{\rightarrow} \gamma$. It is immediate from the definition that this substitution leaves pre- and post-conditions of instantiated transitions unchanged, so that it lifts to runs: for any $\rho : \emptyset \dashrightarrow_{\sigma} \alpha$, $\rho[h] : \emptyset \dashrightarrow_{\sigma[h]} \alpha$ is defined pointwise.

We shall now prove that this preserves valid runs. First, an easy observation:

**LEMMA D.18.** Consider A a game, and $\sigma : A$ a negative Petri strategy.
Then, for all $\rho : \emptyset \dashrightarrow_{\sigma} \alpha$ s.t. $\text{play}(\rho) \in \text{Plays}(A)$, we have $\text{play}(\rho) \in \text{Plays}_-(A)$.

**PROOF.** By negative, the first transition of $\rho$ cannot be positive or neutral (as those require at least one tokil). Thus, it is negative. $\square$

**LEMMA D.19.** Consider A a game, $\sigma : A$ negative, $h = [f, (g_m)] : A \rightsquigarrow B$, and $\rho : \emptyset \dashrightarrow_{\sigma} \alpha$.
If $\text{play}(\rho) \in \text{Plays}_-(A)$, then $\text{play}(\rho[h]) = h(\text{play}(\rho)) \in \text{Plays}_-(B)$.

**PROOF.** Straightforward by induction on $\rho$. $\square$

We shall also use a sort of reciprocal statement:

**LEMMA D.20.** Consider A a game, $\sigma : A$ negative, $h = [f, (g_m)] : A \rightsquigarrow B$, and $\rho' : \emptyset \dashrightarrow_{\sigma[h]} \alpha$.
If $\text{play}(\rho') \in \text{Plays}(B)$, there is a unique $\rho : \emptyset \dashrightarrow_{\sigma} \alpha$ s.t. $\text{play}(\rho) \in \text{Plays}(A)$ and $\rho' = \rho[h]$.

**PROOF.** Straightforward by induction on $\rho'$. $\square$

**PROPOSITION D.21.** Consider A a game, $\sigma : A$ negative, $h = [f, (g_m)] : A \rightsquigarrow B$.
Then, $\sigma[h] : B$ is a negative Petri strategy.
**PROOF.** Valid. Consider $\rho' : \emptyset \to \sigma[h]$ $\alpha$ such that play($\rho'$) $\in$ Plays($B$). Consider $f^+ : \alpha \xrightarrow{b} \sigma[h]$ $\beta$, write $f = t^+(|\mu|) \circ \gamma$. By Lemma D.20, there is a unique $\rho : \emptyset \to \sigma$ $\alpha$ such that play($\rho$) $\in$ Plays($A$) and $\rho' = \rho[h]$. By definition of transitions of $\sigma[h]$, we have $b = h(a)$ with

$$t^+(|\mu|) \circ \gamma : \alpha \xrightarrow{a} \beta$$

and play($\rho$) $a \in$ Plays($A$) as $\sigma$ is valid. Note actually play($\rho$) $a \in$ Plays_($A$) by Lemma D.18. Hence, $h(\text{play}(\rho)a) = \text{play}(\rho[h])b \in$ Plays_($B$) by condition validity of global renamings, as required.

**Receptive.** Consider $\rho' : \emptyset \to \sigma[h]$ $\alpha$ such that $s' = \text{play}(\rho') \in$ Plays($B$). Consider $sb^- \in$ Plays($B$). By Lemma D.20, there is a unique $\rho : \emptyset \to \sigma$ $\alpha$ such that $s = \text{play}(\rho) \in$ Plays($A$) and $h(s) = s'$. By condition receptivity of global renamings, there is $sa^- \in$ Plays($A$) such that $h(a) = b$. As $\sigma$ is receptive, there is a unique $e^- \in \mathscr{E}_\sigma$ such that $e^- : \emptyset \xrightarrow{a} \sigma$ $\beta$ for some $\beta$. By definition of $\sigma[h]$, $e^- : \emptyset \xrightarrow{b} \sigma[h]$ $\beta$ as required. Uniqueness follows immediately from uniqueness for $\sigma$.

**Strongly safe.** Consider $\rho' : \emptyset \to \sigma[h]$ $\alpha$ such that $s' = \text{play}(\rho') \in$ Plays($B$). By Lemma D.20, there is a unique $\rho : \emptyset \to \sigma$ $\alpha$ such that $s = \text{play}(\rho) \in$ Plays($A$) and $h(s) = s'$. If $f' : \alpha \to \sigma[h]$ $\beta$ then also $f' : \alpha \to \sigma$ $\beta$, and new($f'$) is fresh in $\rho$, so fresh in $\rho'$. If $f' : \alpha \xrightarrow{b} \sigma[h]$ $\beta$ with $s'b \in$ Plays($B$), then again by Lemma D.20, $f' = f[h]$ and $b = h(a)$ for $f : \alpha \xrightarrow{a} \sigma$ $\beta$ with $sa \in$ Plays($A$). As $\sigma$ is strongly safe, it follows that new($f$) is fresh in $\rho$, but new($f$) = new($f'$) so new($f'$) is fresh in $\rho'$ as required.

**Negative.** Straightforward from the fact that $\sigma$ is negative. $\square$

### D.2.3 *Currying*. This is a simple application of global renaming.

**LEMMA D.22.** Consider $\Gamma, x : A, \Delta$ a list of variable/arena declarations, and $O$ well-opened. Then,

$$ (\Lambda_x, (\text{id})) : (!(\&[\Gamma, x : A, \Delta]) \vdash O) \rightleftharpoons (!(\&[\Gamma, \Delta]) \vdash !A \dashv O) $$

where $\Lambda_x$ is defined in Definition B.2.

**PROOF.** Immediate verification. $\square$

**COROLLARY D.23.** Consider $\sigma : !([\Gamma, x : A, \Delta]) \vdash O$ a negative Petri strategy.

Then, $\Lambda_{x:A,O}^{\Gamma,\Delta}(\sigma) : !([\Gamma, \Delta]) \vdash !A \dashv O$ is a negative Petri strategy.

### D.2.4 *Functorial promotion.* Rather than directly dealing with Definition 2.11, we decompose it: first, a functorial promotion, and secondly, a renaming corresponding to *digging*.

We first define functorial promotion on Petri structures:

**Definition D.24.** Consider $\sigma \in$ PStruct($M, N$). We set $\mathcal{L}_{\sigma} = \mathcal{L}_{\sigma}$, $\mathcal{T}_{\sigma} = \mathcal{T}_{\sigma}$ with the same polarities, $\partial_{\sigma} = \partial_{\sigma}$, and pre- and post-conditions are also unchanged. Finally, the transition table is:

$$ \delta_{\sigma}(t^0) (e :: \alpha) = e :: \beta \quad \text{if } \delta_{\sigma}(t) (\alpha) = \beta $$

$$ \delta_{\sigma}(t^+) (e :: \alpha) = (e :: s, d) \quad \text{if } \delta_{\sigma}(t) (\alpha) = (s, d) $$

$$ \delta_{\sigma}(t^-) (e :: s, d) = e :: \alpha \quad \text{if } \delta_{\sigma}(t) (s, d) = \alpha $$

where $e :: \alpha$ is $\{(e :: s_i, d_i)@l_i \mid (s_i, d_i)@l_i \in \alpha\}$.

With this definition, we obtain $!\sigma \in$ PStruct(!M, !N).

We prove that this operation preserves Petri strategies – the proof follows closely that of tensor, of which the ! can be regarded as an infinitary version.

**LEMMA D.25.** Consider $\sigma$ a Petri structure.

Then, instantiated transitions of $!\sigma$ are exactly as in Figure 48 – in the sense that there is a one-to-one correspondence between instantiated transitions in the premises and in the conclusion.
$$ \frac{t^0(|\alpha|) : \alpha \mapsto_{\sigma} \beta}{t^0(|e :: \alpha|) : e :: \alpha \mapsto_{!\sigma} e :: \beta} $$

$$ \frac{t^{-}(|(s, d)|) : \emptyset \stackrel{m}{\mapsto}_{\sigma} \beta}{t^{-}(|(e :: s, d)|) : \emptyset \stackrel{e:m}{\mapsto}_{!\sigma} e :: \beta} $$

$$ \frac{t^{+}(|\alpha|) : \alpha \stackrel{m}{\mapsto}_{\sigma} \emptyset}{t^{+}(|e :: \alpha|) : e :: \alpha \stackrel{e:m}{\mapsto}_{\sigma} \emptyset} $$

<caption>Fig. 48. Description of instantiated transitions of $!\sigma$</caption>

Using this description, we define for each $e \in \mathcal{E}$ a partial function

$$ \pi_e^! : \begin{array}{ccc} \mathcal{E}_{!\sigma} & \to & \mathcal{E}_{\sigma} \\ t^0(|e :: \alpha|) & \mapsto & t^0(|\alpha|) \\ t^{-}(|(e :: s, d)|) & \mapsto & t^{-}(|(s, d)|) \\ t^{+}(|e :: \alpha|) & \mapsto & t^{+}(|\alpha|) \end{array} $$

and undefined otherwise. In order to extend those to instantiated transitions in context, first define

$$ \big|\big| \alpha_e = \big(\big|\big| e :: \alpha_e $$

for $(\alpha_e)_{e \in \mathcal{E}}$ a family of conditions empty almost everywhere. We may then set:

$$ \pi_e^! : \begin{array}{ccc} \mathcal{F}_{!\sigma} & \to & \mathcal{F}_{\sigma} \\ e \upharpoonright (\|\|_{e \in \mathcal{E}} \gamma_e) & \mapsto & \pi_e^!(e) \upharpoonright \gamma_e. \end{array} $$

Using these, from a run $\rho : \emptyset \to!_{\sigma} \alpha$ we extract, for all $e \in \mathcal{E}$:

$$ \rho_e = \rho \upharpoonright \pi_e^! $$

we will also use for restrictions the partial functions

$$ e : \begin{array}{ccc} \text{Moves} & \to & \text{Moves} \\ (m, e :: s, d) & \mapsto & (m, s, d) \end{array} $$

and undefined otherwise – the abuse of notations should not create confusion.

Now, as for the tensor we can prove:

**LEMMA D.26.** Consider $\rho : \emptyset \to!_{\sigma} \alpha$. Then, $\alpha = \|\|_{e \in \mathcal{E}} \alpha_e$ and
$$ \rho_e : \emptyset \to\sigma \alpha_e $$

for all $e \in \mathcal{E}$, where play($\rho_e$) = play($\rho$) $\upharpoonright$ e.

$$ \text{Moreover, } \text{Coll}(\rho) = \|\|_{e \in \mathcal{E}} \text{Coll}(\rho_e). $$

**PROOF.** The proof is the same as for Lemma D.4, without synchronized transitions. $\square$

<figure><img src="image_58.png" /></figure>

The construction goes on as for the tensor, with preservation of plays via projections:

**LEMMA D.27.** Consider A an arena and $s \in |!A|^*$.

$$ \text{Then, } s \in \text{Plays}(!A) \text{ iff } s \upharpoonright e \in \text{Plays}(A) \text{ for all } e \in \mathcal{E}. $$

**PROOF.** Straightforward. $\square$

<figure><img src="image_59.png" /></figure>

Consider now $\sigma : A \vdash B$ a Petri strategy.

Using Lemmas D.27 and D.26, we show that projections preserve valid runs.

**LEMMA D.28.** Consider $\rho : \emptyset \to!_{\sigma} \alpha$ such that play($\rho) \in \text{Plays}(!A \vdash !B)$.

$$ \text{Then, for all } e \in \mathcal{E}, \text{ play}(\rho_e) \in \text{Plays}(A \vdash B). $$

**PROOF.** As for the proof of Lemma D.6 (without synchronization), using condition valid of Petri strategies along with Lemma D.27. $\square$

<figure><img src="image_60.png" /></figure>
Using Lemmas D.26, D.27 and D.28, we prove as for Proposition D.7:

**PROPOSITION D.29.** If $\sigma : A \vdash B$ is a Petri strategy, then so is $!\sigma : !A \vdash !B$. Moreover, if $\sigma$ is negative then so is $!\sigma$.

**D.2.5** Local renamings. To match Definition 2.11, we must also rename following *digging*.
Recall that *digging* is the following map:

$$ \begin{array}{ccc} \text{dig :} & \text{ Moves } \rightarrow & \text{ Moves} \\ (m, e :: e' :: s, d) & \mapsto & (m, \langle e, e' \rangle :: l, d) \end{array} $$

and undefined otherwise. To rename a strategy following this, it is convenient to introduce:

**Definition D.30.** Consider A, B arenas.

A **(local) renaming** from A to B is a partial injection $f : \text{ Moves} \to \text{ Moves}$ defined on $|A|$, s.t.:

*validity*: for all $x \in \mathscr{C}(A)$, $fx \in \mathscr{C}(B)$,

*polarity-preserving*: for all $a \in |A|$, $\text{pol}(f(a)) = \text{pol}(a)$,

*receptivity*: for all $x \in \mathscr{C}(A)$, if $f(x) \vdash_B b^-$, then there is $x \vdash_A a$ such that $f(a) = b$,

*courtesy*: for all $a \to_A a'$, either $f(a) \to_B f(a')$ or $(\text{pol}(a), \text{pol}(a')) = (-, +)$.

We write $f : A \rightsquigarrow B$ to mean that $f$ is a renaming from $A$ to $B$.

It is clear in particular that $\text{dig} : !A^\perp \to !A$ is a renaming, for any arena A. This is a variant of Definition D.16, closer to the usual lifting operation used for this purpose in concurrent games.

Clearly, a local renaming is a global renaming. But local renamings are sometimes more convenient, because if $f : A^\perp \rightsquigarrow B^\perp$ and $g : A' \rightsquigarrow B'$ are local renaming, then it is obvious that $f \vdash g : A \vdash B \rightsquigarrow A' \vdash B'$ (defined in the obvious way) is still a local renaming – this is not always the case for global renamings for non-negative games.

**Definition D.31.** Consider $\sigma : A \vdash B$ a negative Petri strategy and $f : A^\perp \rightsquigarrow A'^{\perp}, g : B \rightsquigarrow B'$. Then, we define $g \cdot \sigma \cdot f = \sigma[f \vdash g] : A' \vdash B'$.

This yields a negative Petri strategy by Proposition D.21.

**D.2.6** *Digging*. We may finally perform *digging* and deduce the correctness of promotion:

**PROPOSITION D.32.** Consider $\sigma : !A \vdash B$ a negative Petri strategy.
Then, $\sigma^\dagger : !A \vdash !B$ is a negative Petri strategy.

**PROOF.** It is a direct verification that $\sigma^\dagger = (!\sigma)[\text{dig} \vdash \text{id}]$, which is a negative Petri strategy by Propositions D.29 and Definition D.31. $\square$

**D.3** PStrat as an IPA-Structure: Primitives

We now show that the Petri structures representing the primitives of IPA are indeed Petri strategies.

Given a Petri structure $\sigma$ and a play $s$ of a game $A$, we say that $s$ is reachable by $\sigma$ when there exists a run $\rho$ of $\sigma$ with play($\rho$) = $s$. Given a game $A$, we define the Scott order on $\mathscr{C}(A)$ as follows: $x \sqsubseteq_A y := (x \supseteq^- \sqsubseteq^+ y)$ which was already encountered in Lemma D.8 for copycat.

**D.3.1** *Variable and Evaluation.* For variable, we notice that $\text{var}_{x:M} = \mathfrak{c}_M[i_x^x \vdash \text{id}]$ and we conclude easily by D.21 since $i_x^x : M^\perp \rightsquigarrow [\Gamma, x : M, \Delta]^\perp$ is a local renaming. For the evaluation, the map $\Omega$ defined in Section B.2 is a global renaming $((M \to N) \vdash (M \to N)) \rightleftharpoons ((M \to N) \otimes M \vdash N)$.
### D.3.2 Contraction.
We now show that the Petri structure $c_A$ is a Petri strategy on $!A \vdash !A \otimes !A$.

Given a move $a$, we write $\ell_i(a)$ for $(m, \ell_i(e) :: s, d)$ for $a = (m, e :: s, d)$, and similarly for $\kappa_i(a)$. It is not defined on moves with an empty stack.

**LEMMA D.33.** Consider $s \in \text{play}(!A \vdash !A \otimes !A)$ reachable by $c_A$.
Then, $|s| = (\ell_1(x_1) \uplus \kappa_1(x_2) \vdash y_1 \otimes y_2)$ and $y_i \sqsubseteq x_i$.

**PROOF.** We prove the implication by induction on the length of $s$. It holds for all plays of length zero. We assume the implication holds for all plays of length $n$.

Consider $s' = s \cdot a$ reachable by $\sigma$ and $s$ has length $n$. We apply the induction hypothesis to $s$ (which is reachable by $\sigma$) and obtain that, writing $|s| = (\ell_1(x_1) \uplus \ell_1(x_2) \vdash y_1 \otimes y_2)$, we have $y_i \sqsubseteq x_i$.

* If $a$ is negative, and on $\ell_i$, then the inequality for $s'$ holds by definition of $\sqsubseteq$.

* If $a$ is negative, and on $\kappa_i$, then because $s'$ is a play, the parent of $a$ must exist and belong to $s$. By induction, that parent must have an exponential stack of the form $\ell_i e :: s$ or $\kappa_i e :: s$ and we can conclude.

* If $a$ is positive, and on the left, ie. $m = \ell_i m_0$: in the run producing $a$, there must be a token in $m_0^-$ that triggered $t$. That token must be $(s, d)$ since $t$ has a trivial transition function. That token can only be produced by one of the negative transitions $\kappa_i \ell_i m_0$ or $\kappa_i \kappa_i m_0$ – assume the former. This directly shows that $s = \ell_i e :: s'$ for some $s'$, and that $(\kappa_i \ell_i m_0, e :: s, d) \in |s|$, which implies that $(m_0, e :: s, d) \in y$. As a result $|s| = (x \cup \{(m_0, \ell_i e :: s', d)\}) \vdash y \otimes z$ satisfies the desired property.

* If $a$ is positive and on the right for instance $m = \kappa_i \ell_i m_0$. Then a similar line of reasoning shows that $s = e :: s'$ and we must have $(\ell_i m_0, \ell_i e :: s', d) \in |s|$ which entails the desired property. $\square$

**LEMMA D.34.** $c_A$ is a negative Petri strategy on $!A \vdash !A \otimes !A$.

**PROOF.** Negative. Simple inspection of the net.

*Strong safety.* Consider $\rho : \emptyset \stackrel{s}{\Longrightarrow} \alpha$ with $s$ a play, and $f : \alpha \stackrel{a}{\Longrightarrow} \beta$ with $sa$ also a play (note that there is no neutral transition). Note that positive transitions do not create tokens, so there is nothing to check. For negative transitions, it follows from the injectivity of transition functions and the fact that plays are non-repetitive.

*Validity.* Consider $\rho : \emptyset \stackrel{s}{\Longrightarrow} \alpha$ a run of $c_A$ and $s$ a play of the game. Assume that $\rho$ can extend by $f^+ : \alpha \stackrel{a}{\Longrightarrow} \beta$. By Lemma D.33, we know that $|s| = (\ell_i(x_1) \uplus \kappa_i(x_2) \vdash y_1 \otimes y_2)$ with $y_i \sqsubseteq x_i$. There are three transitions, hence three cases. We detail the case for $a = \ell_i a_0$; then by inspecting the net we have that $a_0$ must be of the form $\ell_i(a_1)$ with $a_1 \in y$ or $\kappa_i(a_1)$ with $a_1 \in z$ – assume the former. From $a_1 \in z$, we deduce that the justifier of $a$ is already present in $s$; and moreover $a$ cannot conflict with anything in $s$. That $sa$ is non-repetitive follows from strong safety and that transition functions are injective.

*Receptivity.* Consider $sa^-$ a play of $!A \vdash !A \otimes !A$ and $\rho : \emptyset \stackrel{s}{\Longrightarrow} \alpha$. If $a$ is on the right of $\vdash$, then we can use the corresponding transition whose function domain is total on stacks of $!A$. For $a$ on the left, $a$ cannot be minimal so its justifier $a_0$ must occur in $s$. By Lemma D.33, its exponential stack must start with $\ell_i(e)$ or $\kappa_i(e)$, and thus so must that of $a$. As a result, $a$ will be accepted by the transition corresponding to its address. $\square$

### D.3.3 Fixpoint.
We start by characterising the plays of $Y_O$, where $O$ is a well-opened arena. We reuse the same encodings as in Section C.3.3.

**LEMMA D.35.** Let $\rho : \emptyset \stackrel{s}{\Longrightarrow} \alpha$ be a run of $Y_O$ such that $s$ is a play.
Then there exists suffix-closed $J \subseteq \mathcal{E}^+$, configurations $z, y_e \in \mathcal{C}(O)$, $(y_s)_{s \in J}$ and $(z_s \in \mathcal{C}^{\neq 0}(O))_{s \in J}$ with $J$ empty if $y_e$ is, $z \sqsubseteq y_e$ and $z_s \sqsubseteq y_s$ for all $s$ and

$$|s| = (\emptyset \to () :: y_e) \circled (e :: (s) :: z_{e \cdot s} \to (e \cdot s) :: y_s) \vdash z, \\ \text{plus if } y_e = \emptyset \text{ then } J = \emptyset, \text{ and if } e \cdot s \in J, \text{ then } y_s \neq \emptyset.$$

**PROOF.** A direct induction over the run, using the transition table.

**LEMMA D.36.** $Y_O$ is a negative Petri strategy $ (!O \to O) \vdash O $.

**PROOF.** Negativity and receptivity are easily verified.

*Validity.* Consider $\rho : \emptyset \stackrel{s}{\rightarrow} \alpha$ be a run of $Y_O$ such that $s$ is a play of the game. Consider now an extension of $\rho$ by the positive transition $f : \alpha \stackrel{a}{\rightarrow} \beta$. We show that $sa$ is a valid play. First, if $a$ or a conflicting move occurs already in $s$, given the shape of the net, this means that Opponent played twice the same move or two conflicting moves earlier in $s$ which is absurd. It remains to show that the predecessor of $a$ occurs in $s$, which is a consequence of Lemma D.35

*Strong-safety.* All negative transitions have injective transition functions, and the two negative transitions $x_e^-$ and $\ell, \ell_-$ have a common postcondition ($m^-$), have disjoint codomains, hence $Y_O$ is strongly safe.

**D.3.4** *Queries, Conditional, Constants.* For these IPA structures defined on linear games, a simple inspection shows that they define they are IPA strategies.

**D.3.5** *Let bindings.* We now move on to showing that *let* is a Petri strategy on$ (!X \to Y) \otimes X \vdash Y $.

**LEMMA D.37.** Let $\rho : \emptyset \stackrel{s}{\rightarrow} \alpha$ be a valid run for *let*. Then $|s| = ((\circled_{e \in J} e :: x_e) \to y) \otimes z \vdash w$ with: (1) if $y \neq \emptyset$ then $z$ is maximal in $\mathcal{C}(X)$; (2) $w \sqsubseteq y$ and $x_e \subseteq z$ for all $e \in I$.

**PROOF.** By induction on $\rho$.

**LEMMA D.38.** *let is a Petri strategy on* $ (!X \to Y) \otimes X \vdash Y $.

**PROOF.** As usual, receptivity and negativity are clear. Strong safety is clear on the forwarding transitions. For the transition $s$, we note that the token in location 3 is never in eat($s$), and the other token at location 5 has a stack given by Opponent, so there cannot be any risk of confusion. Validity follows from Lemma D.37.

**D.3.6** *Newref and newsem.* We now show that **newref** and **newsem** are valid Petri strategies. We focus our attention on **newref**, the proof for **newsem** being similar.

We start by recovering, out of a run of **newref**, a memory trace. A memory trace is a word on the alphabet $\Sigma := \mathcal{E} \times \{r, w\} \times \mathcal{D}$. There is a partial function $\pi : \mathcal{E}_{newref} \to \Sigma$ as follows:

$$\begin{align*}
\pi(w\{([e], d)^{@3}, \dots, \_\}) &= (e, w, d) \\
\pi(r\{([e], \_)^{@5}, \dots, \_, d)^{@2}\}) &= (e, r, d)
\end{align*}$$

and undefined everywhere else. We write $\text{Tr}(\rho) = \rho \upharpoonright \pi$.

A memory trace is **consistent** when (1) exponential signatures occurring in it are all distinct, and (2) each read reads the last value written before, or zero if there are no writes.

**LEMMA D.39.** *Consider a run* $\rho : \emptyset \stackrel{s}{\rightarrow} \alpha$ *of newref such that* $s$ *is a play*. *Then:*

* Tr($\rho$) is a consistent memory trace.

* If $\rho$ is not empty, then there is a unique tokil ($s, d)^{@2}$ in $\alpha$ such that: if Tr($\rho$) is empty then $s = []$ and $d = 0$, otherwise $s = [e]$ with e and d the components of the last operation in Tr($\rho$).

* $|s|$ has the shape $((\circled_{e \in J} e :: x_e) \to y) \vdash z$ with $z \sqsubseteq y$ and $x_e \in \mathcal{C}(V)$ such that: - if $x_e$ is non-empty then e occurs in Tr($\rho$) and the value coincide in the case of a read.
- For every signature e occurring in Tr(ρ), x_e is non-empty.

PROOF. We proceed by induction on ρ, the base case being trivial. We assume ρ = ρ' · f with f : α → β. For the visible transitions τ_c(-) and ℓ_cτ_c(-), this is a proof similar to copycat.

* If f is on ℓ_cℓ_ωw_¥Q⁻ or ℓ_cℓ_ωτ_¥Q⁻, there is nothing to add to the induction hypothesis.

* If f = γ ⊎ w{([e], d)@², ([e'], d')@³): then Tr(ρ) = Tr(ρ')([e'], w, d') is still a consistent trace. Moreover, from the tokil ([e'], d')@³, we deduce that in ρ' there must be a visible transition with move (ℓ_cℓ_ωw_¥Q⁻, [e], d').

* If f = γ ⊎ w{([e], d)@², ([e'], •)@⁵): the same line of reasoning works, except that Tr(ρ) = Tr(ρ')([e', r, d]) is no longer automatically consistent. However, by induction we know that in α there is a unique token at location 2, and that its value is the last value written or zero if there is not any - which shows that Tr(ρ) is indeed consistent.

* If f = γ ⊎ ℓ_cℓ_ωw_¥A([e, d]@⁴): the first two conditions are trivially true. Moreover, since ([e], d)@⁴ belongs to α, there must have been a transition w in α before that put it there. That shows that there must be an element in Tr(ρ) with exponential token e as desired. □

LEMMA D.40. *newref* is a Petri strategy on !V →⁻ X ⊢ X.

PROOF. Negativity and receptivity follow by inspection of the net and transition tables.

*Strong-safety.* Consider a run ρ : Θ ↪→ s α such that s is a play, that can be extended by a transition f : α → β that is negative or neutral, with play(ρf) being a play.

*Initial question.* If f is a negative transition α ↪→ s β on the address τ_cQ⁻. Then necessarily ρ = ε and so Coll(ρ) = Θ.

*Final return.* If f is a negative transition α ↪→ s β on the address ℓ_cτ_cA⁻: trivial since the function of this transition is simply the identity, it follows from sa being a play hence non-repetitive.

*Request.* If f is a negative transition α ↪→ s β on the address ℓ_cℓ_ωw_¥Q⁻ or ℓ_cℓ_ωτ_¥Q⁻. In both cases, the transition function is again the identity, so we can conclude by the same argument.

*Atomic operation.* If f arises from w or r. The two cases being symmetric, we only show for w. From the Petri structure, we get that α = γ ⊎ {([e], d)@³, (s, d')@²} and β = γ ⊎ {([e], d)@², ([e], √)@⁶}.

We show that new(f) is fresh in ρ. For the token in location 6, which is always in new(f), only the transition w writes to 6, so if the tokil ([e], √)@⁶ appeared before in ρ, it means that there would be already a tokil ([e], d'')@³ in Coll(ρ). This is not possible because 3 is only fed via the negative transition on ℓ_cℓ_ωw_¥Q⁻. This means that Opponent would have played (ℓ_cℓ_ωw_¥Q⁻, [e], d'') which violates the fact that s is non-repetitive (if d = d'') or that s is a play (if d ≠ d'' as those moves are in conflict).

Finally, if ([e], d)@² is in Coll(ρ), then it means that a previous instance of w or r produced it, which means that there must have been a tokil ([e], d)@³ (for w) or ([e], •)@⁵ (for r). That implies there has been two Opponent moves on addresses of the form ℓ_cℓ_ω(-) with the same exponential address, which is not allowed by the game as they are all in conflict.

*Valid.* Consider a run ρ : Θ ↪→ s α with s a play, and a positive extension f : α ↪→ s β. There are several cases depending on the address of a:

* If a is on τ_cA: easy since ρ is non empty it must contain its justifying move. Moreover a or a conflicting move with a cannot occur in s, since we simply forward moves received from address ℓ_cτ_cA.

* If a is on ℓ_cτ_cQ: same reasoning.

* If a is for instance on ℓ_cℓ_ωw_¥A (the case for τ_c is similar). This means that in location 4, there must be a tokil ([e], √)@⁴. That tokil proves that, there must be an entry (e, w, d) (for some d) in Tr(ρ). By Lemma D.39, we know that in s there must be justifying move (ℓ_cℓ_ωw_¥Q, [e], d).
Moreover, if a or a conflicting move would be already present in a, then we could apply the same reasoning and find a contradiction with the fact that Tr(ρ) cannot repeat twice the same exponential token. □

# E THE UNFOLDING

We provide some detailed proofs of the unfolding to strategies.

## E.1 Construction of the Unfolding

Fix a game A, and a Petri strategy $\sigma$: A. First, for a valid run $\rho: \emptyset \to \sigma \alpha$, we write $\text{post}(\rho) = \alpha$. If $x \in \text{Hist}(\sigma)$, we write $\text{post}(x) = \text{post}(\rho)$ for any $\rho$ such that $x = \mathscr{E}(\rho)$. This is justified by:

**LEMMA E.1.** Consider $\rho: \emptyset \to \sigma \alpha$ and $\rho': \emptyset \to \sigma \alpha'$ valid runs such that $\mathscr{E}(\rho) = \mathscr{E}(\rho')$.
Then, $\alpha = \alpha'$.

**PROOF.** Exploiting strong safety, it is immediate by induction on $\rho$ that:

$$ \alpha = (\wp\{\text{post}(e) \mid e \in \mathscr{E}(\rho)\} \setminus (\wp\{\text{pre}(e) \mid e \in \mathscr{E}(\rho)\}) $$

from which the result immediately follows. □

We aim to prove that valid runs exactly correspond to linearizations of histories. In this section, we write $\leq_{\rho}$ for $(<_{A+B} \cup <_{\sigma})^*$.

**LEMMA E.2.** Consider $\rho$ a valid run of $\sigma$ of the form $\rho = \rho_0 \cdot (e \uplus \alpha) \cdot (e' \uplus \alpha')$.
If $e$ is maximal in $\mathscr{E}(\rho)$ for $\leq_{\rho}$, then $\rho_0 \cdot (e' \uplus \beta') \cdot (e \uplus \beta)$ is a valid run for some $\beta, \beta'$.

**PROOF.** First, we show that for $\beta' = \text{post}(\rho_0) \setminus \text{pre}(e')$, $\rho_0$ extends by $e' \uplus \beta'$ which means showing:

$$ (1) \quad \beta' \cap \text{pre}(e') = \emptyset $$

$$ (2) \quad \text{pre}(e') \subseteq \text{post}(\rho_0) $$

$$ (3) \quad \beta' \cap \text{post}(e') = \emptyset $$

First, (1) is by construction of $\beta'$. For (2), consider $e \in \text{pre}(e')$. Then $e$ must either be in $\alpha \subseteq \text{post}(\rho_0)$, or in $\text{post}(e)$. If it is in $\text{post}(e)$, then it cannot be a token produced by $e$ (i.e. in $\text{new}(e)$) as $e$ and $e'$ are incomparable. So it must be in $\text{pre}(e) \subseteq \text{post}(\rho_0)$ as desired. For (3), consider $e \in \beta' \cap \text{post}(e')$. The token $e$ must be in $\text{new}(e')$, which implies since $e$ and $e'$ are incomparable that $e$ does not appear in $\text{pre}(e)$. Since $e \in \text{post}(\rho_0)$, it must be that $e \in \alpha$. Since $\alpha'$ must be disjoint from $\text{post}(e')$, we have $e \in \text{pre}(e')$ which is absurd. Hence, $\rho_1 = \rho_0 \cdot (e' \uplus \beta')$ is indeed a valid run.

We now let $\beta = \text{post}(\rho_1) \setminus \text{pre}(e)$ and must prove (1) $\text{pre}(e) \subseteq \text{post}(\rho_1)$; and (2) $\beta \cap \text{post}(e) = \emptyset$. For (1), if $e \in \text{pre}(e)$, then $e$ is in $\text{post}(\rho_0)$. As a result, either $e$ is not in $\text{pre}(e')$, which implies that $e \in \beta'$ hence $e \in \text{post}(\rho_1)$ (as desired), or $e \in \text{pre}(e')$ as well. In the second case, we have then $e \in \text{pre}(e) \cap \text{pre}(e')$. Because, in $\rho$, $e$ comes before $e'$, this implies that $e$ cannot be eaten by $e$, in other words $e \in \text{post}(e)$. This implies $e \notin \text{eat}(e')$ as the two transitions are incomparable, i.e. $e \in \text{post}(e') \subseteq \text{post}(\rho_1)$. For (2), consider $e \in \beta \cap \text{post}(e)$, ie. in particular $e \in \text{new}(e)$. As $e \in \text{post}(\rho_1)$, $e$ either belongs to $\beta'$ or $\text{post}(e')$. In the first case, this means that $e \in \text{post}(\rho_0) \cap \text{post}(e)$, which can only be if $e \in \text{pre}(e)$ which is absurd. In the second case, it means that $e \in \text{post}(e')$, which in turn means that $e \in \text{pre}(e')$ as $e$ is produced by $e$ so it cannot be produced by $e'$ as well by strong safety. But that is not possible either as it would imply a dependency from $e$ to $e'$. □

**LEMMA E.3.** Consider $x \in \text{Hist}(\sigma)$ and $e$ a maximal element of $x$.
Then, there exists a valid run $\rho$ ending in $e \uplus \alpha$ (for some context $\alpha$) such that $\mathscr{E}_{\rho} = x$.
PROOF. Consider a run $\rho_0$ spanning $x$, which must have the shape:

$$ \rho_0 = \rho_1 \cdot (\mathbf{e} \uplus \alpha) \cdot (\mathbf{e}_1 \uplus \alpha_1) \dots \cdot (\mathbf{e}_n \uplus \alpha_n). $$

We proceed by induction on $n$. If $n = 0$, then $\mathbf{e}$ already occurs at the end of $\rho$. For $n + 1$, we consider $\rho'$ the prefix of $\rho$ where the last transition has been removed. By IH, we get a run $\chi$ with $\mathscr{E}(\chi) = x \setminus \{\mathbf{e}_{n+1}\}$ and $\chi$ ends with $\mathbf{e}$. By Lemma E.1, we have $\text{post}(\chi) = \text{post}(\rho')$; from that it is immediate that $\chi \cdot (\mathbf{e}_{n+1} \uplus \alpha_{n+1})$ is a valid run, and we conclude by Lemma E.2. $\square$

LEMMA E.4. Consider $x \in \text{Hist}(\sigma)$.

Then, valid runs $\rho$ such that $x = \mathscr{E}(\rho)$ exactly correspond to linearizations of $x$.

PROOF. Clearly, all runs preserve $\leq_{\rho}$. For the converse, for any transition $\mathbf{e}$ maximal in $\mathscr{E}(x)$, we obtain a run where it is played last by taking any valid run $\rho$ such that $x = \mathscr{E}_{\rho}$, and pushing $\mathbf{e}$ to the end via local permutations – maximality of $\mathbf{e}$ ensures that there is no obstruction – see Lemma E.3. Iterating this process, we can indeed obtain any linearization. $\square$

We can now show the correctness of $\leq_{\rho}$:

PROPOSITION 4.11. For $\rho$ a valid run of $\sigma$, $\leq_{\rho} = (\triangleleft_{A \uplus B} \cup \triangleleft_{\sigma})^*$.

PROOF. It is a simple corollary of Lemma E.4. Indeed suppose that $\mathbf{e} \leq_{\rho} \mathbf{e}'$. Then, all equivalent $\rho'$ are linearisations of $\leq_{\rho}$, i.e. in which $\mathbf{e}$ must occur before $\mathbf{e}'$. Conversely, if $\mathbf{e} \leq_{\rho} \mathbf{e}'$, then there cannot be any linearisation of $\leq_{\rho}$ where $\mathbf{e}'$ occurs before $\mathbf{e}$, which implies the desired result. $\square$

## E.2 Hiding

Rigid families seem to have remained in the concurrency theory folklore for a while and to have first appeared in published form in [Castellan et al. 2014a,b; Hayman 2014].

Consider $q = (|q|, \leq_q)$ and $\rho = (|\rho|, \leq_\rho)$ finite partial orders. We say that $q$ is **rigidly included** in $\rho$, written $q \hookrightarrow \rho$, if $|q| \subseteq |\rho|$, and if that inclusion: (1) preserves down-closed sets, i.e. $\mathscr{C}(q) \subseteq \mathscr{C}(\rho)$; and (2) preserves causality, i.e. for all $e, e' \in |q|$, if $e \leq_q e'$ then $e \leq_\rho e'$ as well.

Definition E.5. A **rigid family** $\mathcal{F}$ is a non-empty set of finite partial orders which is:

rigid-closed: if $\rho \in \mathcal{F}$ and $q \hookrightarrow \rho$, then $q \in \mathcal{F}$,

binary-compatible: if $X \subseteq_f \mathcal{F}$, then $X \uparrow$ iff for all $q, \rho \in X$, $\{q, \rho\} \uparrow$.

where $X \uparrow$ means that there is $r \in \mathcal{F}$ such that for all $q \in X$, $q \hookrightarrow r$.

We added binary-compatible to the definition, to match our event structures with binary conflict.

A rigid family $\mathcal{F}$ collects causal executions. Particularly interesting are the **primes** of $\mathcal{F}$, i.e. those $q \in \mathcal{F}$ with a top element $\text{top}(q) = e$: those can be thought of as a single event $e$, with a causal history leading to $e$. Indeed, the reconstructed event structure will have the primes as events:

PROPOSITION E.6. For $\mathcal{F}$ a rigid family, the data $\text{Pr}(\mathcal{F}) = (|\text{Pr}(\mathcal{F})|, \leq_{\text{Pr}(\mathcal{F})}, \#_{\text{Pr}(\mathcal{F})})$ defined by:

$$ \begin{align*} |\text{Pr}(\mathcal{F})| &= \{q \in \mathcal{F} \mid q \text{ prime}\} \\ q \leq_{\text{Pr}(\mathcal{F})} \rho &\Leftrightarrow q \subseteq \rho \\ \neg(q \ #_{\text{Pr}(\mathcal{F})} \rho) &\Leftrightarrow \{q, \rho\} \uparrow, \end{align*} $$

is an event structure with $\chi_F : \mathscr{C}(\text{Pr}(\mathcal{F})) \cong \mathcal{F}$ an order-isomorphism.

The proof is routine – $\chi_F$ takes $x \in \mathscr{C}(\text{Pr}(\mathcal{F}))$ to its sup $\bigvee x \in \mathcal{F}$ obtained as the (necessarily) compatible union of all partial orders in $x$, while $\chi_F^{-1}$ takes $q \in \mathcal{F}$ to the set of primes below $q$.

PROPOSITION E.7. The set comprising all $\mathscr{C}(x)$ for $x \in \text{Hist}(\sigma)$, is a rigid family written $\mathscr{C}(\sigma)$.

Moreover, $\mathscr{C}(\sigma)$ (ordered by rigid inclusion) is order-isomorphic to $\text{Hist}(\sigma)$ (ordered by inclusion).
**PROOF.** First, the claimed order-isomorphism is clear by construction.

**Rigid-closed.** Now if $\mathcal{P} \in \mathcal{C}(\sigma)$ and $\mathcal{q} \hookrightarrow \mathcal{P}$, by Lemma E.4 there is a valid run $\rho$ playing $\mathcal{q}$ first. Truncating $\rho$ after $\mathcal{q}$, we get $\rho'$ such that $\mathcal{C}(\rho') = \mathcal{q}$ by construction.

**Binary-compatible.** Take $X \subseteq_f \text{Hist}(\sigma)$. Clearly, if (1) there are $x, y \in X$, visible instantiated transitions $e$ in $x$ and $e'$ in $y$ labelled by conflicting events of $A \vdash B$; or (2) there are $x, y \in X$, $e : \alpha \to_{\sigma} \beta$ in $x$ and $e' : \alpha' \to_{\sigma} \beta'$ in $y$ such that $\alpha \cap \alpha' \neq \emptyset$; then there cannot be a valid run witnessing $\cup X$: (1) would contradict validity of the run, while (2) would contradict strong safety as the same tokil would have to be consumed twice. Reciprocally, if we have neither (1) nor (2), then any valid runs $(\rho_x)_{x \in X}$ may be directly "zipped" into a valid run witnessing $\cup X \in \text{Hist}(\sigma)$.

This concludes the proof, as it brings compatibility of $X \subseteq_f \mathcal{C}(\sigma)$ to pairwise compatibility. $\square$

**PROPOSITION E.8.** *The event structure $\mathcal{U}(\sigma) = \text{Pr}(\mathcal{C}(\sigma)) \downarrow \mathcal{V}_{\sigma}$, equipped with the display map*

$$ \partial_{\mathcal{U}(\sigma)} : |\mathcal{U}(\sigma)| \to |A \vdash B| \\ \mathcal{q} \mapsto \partial_{\sigma}(\text{top}(\mathcal{q})) $$

*is a strategy in the sense of Definition 4.4. Moreover, $\mathcal{U}(\sigma)$ is negative if $\sigma$ is.*

**PROOF.** It remains to prove *courteous, receptive and negative*. From the order-isos $\mathcal{C}(\mathcal{U}(\sigma)) \cong \mathcal{C}^{\mathcal{V}_{\sigma}}(\text{Pr}(\mathcal{C}(\sigma)))$ and $\mathcal{C}(\text{Pr}(\mathcal{C}(\sigma))) \cong \mathcal{C}(\sigma)$, we get an order-iso:

$$ K_{\sigma} : \mathcal{C}(\mathcal{U}(\sigma)) \cong \mathcal{C}^{V}(\sigma) \qquad (5) $$

We now prove the remaining conditions.

**Courteous.** Consider $x_1 \to_{\mathcal{U}(\sigma)} x_2$ such that $\text{pol}(x_1) = +$ or $\text{pol}(x_2) = -$. So $x_1, x_2 \in \mathcal{C}(\sigma)$ with respective top elements $\text{top}(x_1) = e_1$ and $\text{top}(x_2) = e_2$, such that $\text{pol}(e_1) = +$ or $\text{pol}(e_2) = -$. By definition, $x_1 \hookrightarrow x_2$, so that $e_1, e_2 \in x_2$ with $e_1 <_{x_2} e_2$. By definition, this means there is a sequence

$$ e_1 <_{x_2} e'_1 <_{x_2} \dots e'_n <_{x_2} e_2 $$

where, each $<_{x_2}$ is either $<_{\sigma}$ or $<_{A}$. Now, seeking a contradiction, assume $n \geq 1$. Assume first that $e_1$ is positive. Then, we cannot have $e_1 <_{x_2} e'_1$ as post($e_1$) = new($e_1$) = $\emptyset$. But we also cannot have $e_1 <_{A} e'_1$, as $e_1$ is visible but not $e'_1$. Assuming that $e_2$ is negative is symmetric: we cannot have $e'_n <_{x_2} e_2$ as pre($e_2$) = eat($e_2$) = $\emptyset$, and we cannot have $e'_n <_{A} e_2$ because $e_2$ is visible but not $e'_n$. So, $n = 0$ and we have $e_1 <_{x_2} e_2$. But again, for the same reason this cannot be because $e_1 <_{\sigma} e_2$, so $e_1 <_{A} e_2$, which means $\partial_{\sigma}(e_1) \to_{A} \partial_{\sigma}(e_2)$. Hence, $\partial_{\mathcal{U}(\sigma)} \to_{A} \partial_{\mathcal{U}(\sigma)}$.

**Receptive.** Consider $x \in \mathcal{C}(\mathcal{U}(\sigma))$ and $\partial_{\mathcal{U}(\sigma)}(x) \vdash_A a^-$. So we have $K_{\sigma}(x) \in \mathcal{C}^V(\sigma)$ with $\partial_{\sigma}(K_{\sigma}(x)) \vdash_A a^-$. We show that there is a unique matching extension $e^-$ of $K_{\sigma}(x)$, and conclude by the fact that $K_{\sigma}$ is an order-isomorphism. For *existence*, consider $\rho : \emptyset \to_{\sigma} \alpha$ a valid run such that $K_{\sigma}(x) = \mathcal{C}(\rho)$. Consider $s \in \text{play}(\rho)$, so in particular $s \in \text{Plays}(A)$. By hypothesis, $s \in \text{Plays}(A)$ as well. So by condition *receptive* of Petri strategies, there is a unique $e^-$ : $\emptyset \to^{A^-} \sigma \beta$ for some $\beta \cap \alpha = \emptyset$, so that $\rho' = \rho(e^- \uplus \gamma)$ is a valid run for some $\gamma$; providing the expected extension of $K_{\sigma}(x)$. *Uniqueness* follows immediately from uniqueness of $e^-$.

**Negative.** Consider $x \in |\mathcal{U}(\sigma)|$ minimal. This means that $x$ is a prime history with exactly one visible event $e$, with $e = \text{top}(x)$. So there is a run

$$ f_1 \dots f_n (e \uplus \gamma) : \emptyset \to_{\sigma} \alpha, $$

but by condition *negative* of Petri strategies, $f_1$ cannot be neutral and have no preconditions. So $n = 0$, and we have a one-event run $e : \emptyset \to_{\sigma} \alpha$. But likewise, by condition *negative* of Petri strategies this entails that $e$ is negative, so $x$ is negative as required. $\square$

**LEMMA E.9.** *The order-isomorphism (5) of Lemma E.8 specializes to $K_{\sigma}^{+} : \mathcal{C}^{+}(\mathcal{U}(\sigma)) \cong \mathcal{C}^{+}(\sigma)$ s.t. for all $x \in \mathcal{C}^{+}(\mathcal{U}(\sigma))$, we have $\partial_{\mathcal{U}(\sigma)}(x) = \partial_{\sigma}(K_{\sigma}^{+}(x))$ the labels of visible transitions in $K_{\sigma}^{+}(x)$.*
## E.3 The Unfolding as a Functor

**PROPOSITION E.10.** Consider $\sigma: A \to B$ and $\tau: B \to C$ Petri strategies. Then, there is an order-iso:

$$ \begin{array}{rcl} (- \odot -) & : & \{(x^\tau, x^\sigma) \in \mathscr{E}^+(\tau) \times \mathscr{E}^+(\sigma) \\ & & \qquad | \text{causally compatible}\} \\ & \cong & \mathscr{E}^+(\tau \odot \sigma) \end{array} $$

such that for $x^\sigma \in \mathscr{E}^+(\sigma)$, $x^\tau \in \mathscr{E}^+(\tau)$ causally compatible, $\partial_{\tau \odot \sigma}(x^\tau \odot x^\sigma) = x_A^\sigma \vdash x_C^\tau$.

**PROOF.** For $x^\sigma \in \mathscr{E}(\sigma)$ and $x^\tau \in \mathscr{E}(\tau)$, we set $x^\tau \odot x^\sigma$ as the set of instantiated transitions obtained from $x^\sigma$ and $x^\tau$ by the rules of Figure 44 (following Lemma D.3). We prove by induction that for all $x^\sigma \in \mathscr{E}(\sigma)$ and $x^\tau \in \mathscr{E}(\tau)$ causally compatible, then $x^\tau \odot x^\sigma \in \mathscr{E}(\tau \odot \sigma)$, and

$$ \mathrm{post}(x^\tau \odot x^\sigma) = \mathrm{post}(x^\sigma) + \circ \mathrm{post}(x^\tau). $$

If $x^\tau \odot x^\sigma$ is empty, there is nothing to prove. If $x^\sigma$ or $x^\tau$ have a maximal neutral instantiated transition, say w.l.o.g. that it is $x^\sigma$ with maximal $e = t^0(\mu) \in x^\sigma$. Then, setting $y^\sigma = x^\sigma \setminus \{e\}$ yields $y^\sigma \in \mathscr{E}(\sigma)$ by Proposition E.7; and with also $y^\tau = x^\tau$, it is direct that $y^\sigma$ and $y^\tau$ are still causally compatible. By IH, we have $y^\tau \odot y^\sigma \in \mathscr{E}(\tau \odot \sigma)$ and post($y^\tau \odot y^\sigma$) = post($y^\sigma$) + $\circ$ post($y^\tau$). This means that there is a run $\rho: \emptyset \to \tau \odot \sigma$ $\alpha$ projecting to $\rho_\sigma: \emptyset \to \sigma$ $\alpha_\sigma$ with $\alpha_\sigma = \mathrm{post}(y^\sigma)$. Since $e$ is enabled in post($y^\sigma$) it follows that $\ell^\circ(t^0)(\ell^\circ(\mu))$ is enabled in $y^\tau \odot y^\sigma$, and

$$ \rho(\ell^\circ(t^0)(\ell^\circ(\mu))) : \emptyset \to \tau \odot \sigma \beta $$

where by construction $\beta = \mathrm{post}(x^\sigma) + \circ \mathrm{post}(x^\tau)$ as needed. The symmetric reasoning applies if $x^\tau$ has a maximal neutral instantiated transition – so assume all maximal transitions in $x^\sigma$, $x^\tau$ visible.

Now, by causal compatibility of $x^\sigma$ and $x^\tau$, there is an element of $x_A \parallel x_B \parallel x_C$ (following the notations of Section C.2.2) which is maximal for $\triangleleft$. If it is in $x_A$, it has the form $\partial_\sigma^\ell(e)$ for $e \in x^\sigma$ positive or negative. In both cases, the same argument as in the neutral case applies (with the additional observation that the obtained run yields a valid play from the hypothesis). The reasoning is the same if it is in $x_C$. The last (key) case is if it is in $x_B$. Then there are instantiated transitions

$$ t^+(\mu) : \mu \stackrel{\kappa m}{\leftrightarrow} \emptyset, \qquad t^-(\langle s, d \rangle) : \emptyset \stackrel{\ell m}{\longmapsto} \tau v, $$

or the dual – symmetric – situation, respectively maximal in $x^\sigma$ and $x^\tau$; and by necessity $m = (m, s, d)$ where $\partial_\sigma(t^+) = \kappa m$, $\partial_\tau(t^-) = \ell m$, $\delta(t^+) \mu = (s, d)$ and $\delta(t^-) \mu = v$. Setting $y^\sigma \setminus \{t^+(\mu)\}$ and $y^\tau \setminus \{t^-(\mu)\}$, it is straightforward that they are still causally compatible histories. By IH, $y^\tau \odot y^\sigma \in \mathscr{E}(\tau \odot \sigma)$ with post($y^\tau \odot y^\sigma$) = post($y^\sigma$) + $\circ$ post($y^\tau$). It follows that there is a run

$$ \rho: \emptyset \to \tau \odot \sigma \mathrm{post}(y^\tau \odot y^\sigma). $$

Since $x^\sigma \in \mathscr{E}(\sigma)$ with $t^+(\mu)$ maximal and $x^\tau \in \mathscr{E}(\sigma)$ with $t^-(\langle s, d \rangle)$ maximal, there are

$$ \begin{array}{rcl} \xi_\sigma(t^+(\mu) \upharpoonright \gamma_\sigma) & : & \emptyset \to \sigma \mathrm{post}(x^\sigma), \\ \xi_\tau(t^-(\langle s, d \rangle) \upharpoonright \gamma_\tau) & : & \emptyset \to \tau \mathrm{post}(x^\tau), \end{array} $$

valid runs by Lemma E.3, with $x^\sigma = \mathscr{E}_{\xi_\sigma}$ and $x^\tau = \mathscr{E}_{\xi_\tau}$. By Lemma E.1, post($\xi_\sigma$) = post($\rho_\sigma$) = post($y^\sigma$) and post($\xi_\tau$) = post($\rho_\tau$) = post($y^\tau$). It follows that the transition

$$ (t^+ \oplus t^-)(\ell^\circ(\mu)) : \ell^\circ(\mu) \mapsto \tau \odot \sigma \tau^\circ(v) $$

is enabled in post($y^\tau \odot y^\sigma$), hence it can be appended to $\rho$, witnessing $x^\tau \odot x^\sigma \in \mathscr{E}(\tau \odot \sigma)$.

In the other direction, given $y \in \mathscr{E}(\tau \odot \sigma)$, consider a valid run $\rho: \emptyset \to \tau \odot \sigma$ $\alpha$ such that $y = \mathscr{E}_\rho$. By Lemmas D.4 and D.6, we then have $\alpha = \alpha_\sigma + \circ \alpha_\tau$ with

$$ \rho_\sigma: \emptyset \to \sigma \alpha_\sigma, \qquad \rho_\tau: \emptyset \to \tau \alpha_\tau $$
valid runs. Recall that $\rho_{\sigma} = \rho \upharpoonright \pi_{\sigma}$ and $\rho_{\tau} = \rho \upharpoonright \pi_{\tau}$ – hence, setting $x^{\sigma} = \pi_{\sigma}(y)$ and $x^{\tau} = \pi_{\tau}(y)$, we have $x^{\sigma} \in \mathscr{E}_{\rho_{\sigma}}$ and $x^{\tau} \in \mathscr{E}_{\rho_{\tau}}$ so that $x^{\sigma} \in \mathscr{E}(\sigma)$ and $x^{\tau} \in \mathscr{E}(\tau)$. Causal compatibility is direct as $\rho$ provides a linearization of $\langle\cdot\rangle$.

It is direct that these constructions are inverse; it remains to show that they preserve $+-$covered histories. If $x^{\sigma}$ and $x^{\tau}$ causally compatible are $+-$covered, then consider $e$ maximal in $x^{\tau} \odot x^{\sigma}$. If $e = \ell^{\circ}(t^0)(\ell^{\circ}(\mu))$, this directly contradicts $+-$coveredness of $x^{\sigma}$, and likewise for $\tau^{\circ}(t^0)(\tau^{\circ}(\mu))$. If $e = \ell^{\circ}(t^{-})(\langle\cdot\rangle(s, d))$, then $t^{-}(\langle\cdot\rangle(s, d))$ is maximal in $x^{\sigma}$, contradiction – likewise for $\tau^{\circ}(t^{-})(\langle\cdot\rangle(s, d))$. If $e = (t^{+} \otimes t^{-})(\ell^{\circ}(\mu))$ with $t^{+}(\mu) \in x^{\sigma}$ and $t^{-}(\langle\cdot\rangle(s, d)) \in x^{\tau}$, then $t^{-}(\langle\cdot\rangle(s, d))$ is maximal in $x^{\tau}$, contradiction – likewise, $e = (t^{-} \otimes t^{+})(\ell^{\circ}(\mu))$ leads to a contradiction. So, $x^{\tau} \odot x^{\sigma}$ is $+-$covered.

Reciprocally, assume $x^{\tau} \odot x^{\sigma}$ $+-$covered. Consider $e \in x^{\sigma}$ maximal. If $e = t^0(\mu)$, $\ell^{\circ}(t^0)(\ell^{\circ}(\mu))$ is maximal in $x^{\tau} \odot x^{\sigma}$, contradiction. If $e = t^{-}(\langle\cdot\rangle(s, d))$, then since $x^{\tau} \odot x^{\sigma}$ is $+-$covered, there is

$$ \ell^{\circ}(t^{-})(\langle\cdot\rangle(s, d)) \to_{x^{\tau} \odot x^{\sigma}} e' $$

and a direct case analysis shows that $\pi_{\sigma}e'$ is defined with $t^{-}(\langle\cdot\rangle(s, d)) \to_{x^{\tau}} \pi_{\sigma}e'$, contradicting the maximality of $e$. The last case has $e$ positive; and symmetrically, $x^{\tau}$ is $+-$covered. $\square$

**PROPOSITION E.11.** For $\sigma : A \vdash B$ and $\tau : B \vdash C$ Petri strategies, $\mathcal{U}(\tau \odot \sigma) \cong \mathcal{U}(\tau) \odot \mathcal{U}(\sigma)$.

**PROOF.** We may deduce preservation of composition simply by manipulating isos:

$$ \begin{align*} \mathcal{E}^{+}(\mathcal{U}(\tau \odot \sigma)) & \\ &\cong \mathcal{E}^{+}(\tau \odot \sigma) \\ &\cong \{(x^{\sigma}, x^{\tau}) \in \mathcal{E}^{+}(\sigma) \times \mathcal{E}^{+}(\tau) \mid \text{causally compatible}\} \\ &\cong \{(x^{\mathcal{U}(\sigma)}, x^{\mathcal{U}(\tau)}) \in \mathcal{E}^{+}(\mathcal{U}(\sigma)) \times \mathcal{E}^{+}(\mathcal{U}(\tau)) \mid \text{causally compatible}\} \\ &\cong \mathcal{E}^{+}(\mathcal{U}(\tau) \odot \mathcal{U}(\sigma)) \end{align*} $$

via Lemma E.9, Proposition E.10, and Lemma E.9 – preservation of causal compatibility follows directly from the order-isomorphism. All these steps preserve displays to the game. By Proposition C.7, it follows that $\mathcal{U}(\tau \odot \sigma) \cong \mathcal{U}(\tau) \odot \mathcal{U}(\sigma)$ as required. $\square$

As detailed in Proposition E.11, it follows that unfolding preserves composition up to iso. Next, we show the same for copycat. If $A$ is an arena, then we have obvious bijections

$$ \mathcal{E}_{\omega_A}^{+} \cong |A \vdash A|^{+}, \qquad \mathcal{E}_{\omega_A}^{-} \cong |A \vdash A|^{-}, $$

and coercing silently through these, we have:

**LEMMA E.12.** Consider A an arena, and $\rho : \emptyset \to \omega_A$ $\alpha$ a valid run. Then, $\mathcal{E}_\rho = \text{play}(\rho)$, with negative maximal transitions in bijection with $\alpha$.

**PROOF.** Straightforward by induction on $\rho$. $\square$

**LEMMA E.13.** Consider A an arena. Then, we have the order-isomorphism

$$ \mathcal{E}^{+}(\omega_A) \cong \{x \vdash x \mid x \in \mathcal{C}(A)\} $$

with $\partial_{\omega_A}(x \vdash x) = x \vdash x$.

**PROOF.** The isomorphism simply applies the bijection $\mathcal{E}_{\omega_A} \cong |A|$. From left to right, recall first that by Lemma D.8, for $\rho : \emptyset \to \omega_A$ $\alpha$ a valid run, we have

$$ |\text{play}(\rho)| = x \vdash y, \quad y \supseteq^{-} x \cap y \subseteq^{+} x, \quad \alpha = (y^{-} \setminus x) \uplus (x^{+} \setminus y). $$
By Lemma E.12, the history $\mathscr{E}_{\rho}$ is +-covered iff $\alpha = \emptyset$, i.e. $y^{-} \subseteq x$ and $x^{+} \subseteq y$. But as $y \supseteq x \cap y \subseteq x$ this entails $x = y$. In that case, $\partial_{\mathscr{C}_A}(\mathscr{E}_{\rho}) = |\text{play}(\rho)| = x \vdash x$ as needed. Reciprocally, for any $x \in \mathscr{C}(A)$, it is straightforward to build a valid run $\rho : \emptyset \longrightarrow \mathscr{C}_A \emptyset$ s.t. $\mathscr{E}_{\rho} = x \vdash x$ as required. $\square$

From that, preservation of copycat follows:

**PROPOSITION E.14.** *Consider A an arena. Then, $\mathcal{U}(\mathscr{C}_A) \cong \mathscr{C}_A$.*

**PROOF.** We compose label-preserving order-isomorphisms:

$$ \begin{align*} \mathscr{C}^{+}(\mathcal{U}(\mathscr{C}_A)) &\cong \mathscr{C}^{+}(\mathscr{C}_A) \\ &\cong \{x \vdash x \mid x \in \mathscr{C}(A)\} \\ &\cong \mathscr{C}^{+}(\mathscr{C}_A) \end{align*} $$

by Lemmas E.9 and E.13. From this it follows that $\mathcal{U}(\mathscr{C}_A) \cong \mathscr{C}_A$ by Lemma C.5. $\square$

**COROLLARY E.15.** *We have a functor of precategories $\mathcal{U}: \text{PStrat} \to \text{Strat}$.*

## E.4 The Unfolding Preserves Operations

Next, we prove that the unfolding preserves all operations of the IPA-structure.

### E.4.1 Tensor. Preservation of the tensor operation is easy via the following observation:

**LEMMA E.16.** *Consider $\sigma : A_1 \cup B_1$, $\tau : A_2 \cup B_2$ Petri strategies. Then, we have an order-isomorphism*

$$ (- \otimes -) : \mathscr{C}^{+}(\sigma) \times \mathscr{C}^{+}(\tau) \cong \mathscr{C}^{+}(\sigma \otimes \tau) $$

s.t. $\partial_{\sigma \otimes \tau}(x^{\sigma} \otimes x^{\tau}) = (x_{A_1} \otimes x_{A_2}) \vdash (x_{B_1} \otimes x_{B_2})$ where $\partial_{\sigma}(x^{\sigma}) = x_{A_1} \vdash x_{B_1}$ and $\partial_{\tau}(x^{\tau}) = x_{A_2} \vdash x_{B_2}$.

**PROOF.** Consider $x^{\sigma} \in \mathscr{C}^{+}(\sigma)$ and $x^{\tau} \in \mathscr{C}^{+}(\tau)$. By definition, there are valid runs

$$ \rho^{\sigma} : \emptyset \longrightarrow_{\sigma} \alpha_{\sigma}, \qquad \rho^{\tau} : \emptyset \longrightarrow_{\tau} \alpha_{\tau} $$

such that $x^{\sigma} = \mathscr{C}_{\rho}^{\sigma}$ and $x^{\tau} = \mathscr{C}_{\tau}^{\tau}$. We define the history $x^{\sigma} \otimes x^{\tau}$ as

$$ \begin{align*} x^{\sigma} \otimes x^{\tau} &= \{ \ell^{\otimes}(t^{0,+}) \mid (\ell^{\otimes}(\mu)) \mid t^{0,+}(\mu) \in x^{\sigma} \} \\ &\uplus \{ \ell^{\otimes}(t^{-}) \mid (\ell^{\otimes}(\mu)) \mid t^{-}(\ell^{\otimes}(\mu)) \in x^{\sigma} \} \\ &\uplus \{ \ell^{\otimes}(t^{0,+}) \mid (\ell^{\otimes}(\mu)) \mid t^{0,+}(\mu) \in x^{\tau} \} \\ &\uplus \{ \ell^{\otimes}(t^{-}) \mid (\ell^{\otimes}(\mu)) \mid t^{-}(\ell^{\otimes}(\mu)) \in x^{\tau} \}. \end{align*} $$

This must be the history of a valid run – to show that, we build

$$ \begin{align*} \ell^{\otimes}(\rho^{\sigma}) & : \emptyset \longrightarrow_{\sigma \otimes \tau} \ell^{\otimes}(\alpha_{\sigma}), \\ \tau^{\otimes}(\rho^{\tau}) \uplus \ell^{\otimes}(\alpha_{\sigma}) & : \ell^{\otimes}(\alpha_{\sigma}) \longrightarrow_{\sigma \otimes \tau} \ell^{\otimes}(\alpha_{\sigma}) \uplus \tau^{\otimes}(\alpha_{\tau}) \end{align*} $$

which by concatenation (and Lemma D.13) yields a valid run $\rho^{\sigma} \otimes \rho^{\tau} : \emptyset \longrightarrow_{\sigma \otimes \tau} \alpha_{\sigma} + \otimes \alpha_{\tau}$; and it is immediate that $x^{\tau} \otimes x^{\sigma} = \mathscr{C}_{\rho^{\tau} \otimes \rho^{\sigma}}$. By definition of the causal ordering of instantiated transitions, it is also immediate that $x^{\tau} \otimes x^{\sigma}$ is +-covered; and that this preserves the labelling.

Reciprocally, for any $x \in \mathscr{C}^{+}(\sigma \otimes \tau)$ we consider the projections

$$ x^{\sigma} = \pi_{\sigma}(x), \qquad x^{\tau} = \pi_{\tau}(x), $$

and it follows from Lemma D.14 that $x^{\sigma} \in \mathscr{C}(\sigma)$ and $x^{\tau} \in \mathscr{C}(\tau)$. From the definition of the causal ordering of instantiated transitions, $x^{\sigma}$ and $x^{\tau}$ are still +-covered.

Finally, these two transformations are inverses as required. $\square$

Again, from this we can conclude that the unfolding preserves the tensor.
**COROLLARY E.17.** Consider $\sigma: A_1 \vdash B_1$, $\tau: A_2 \vdash B_2$ Petri strategies.
Then, we have $\mathcal{U}(\sigma \otimes \tau) \cong \mathcal{U}(\sigma) \otimes \mathcal{U}(\tau)$.

**PROOF.** We compose label-preserving isomorphisms:

$$ \begin{align*} \mathcal{C}^+(\mathcal{U}(\sigma \otimes \tau)) &\cong \mathcal{C}^+(\sigma \otimes \tau) \\ &\cong \mathcal{C}^+(\sigma) \times \mathcal{C}^+(\tau) \\ &\cong \mathcal{C}^+(\mathcal{U}(\sigma)) \times \mathcal{C}^+(\mathcal{U}(\tau)) \\ &\cong \mathcal{C}^+(\mathcal{U}(\sigma) \otimes \mathcal{U}(\tau)) \end{align*} $$

by Lemmas E.9, E.16, Lemma E.9 again, and Proposition C.12. □

**E.4.2 Renaming.** Before detailing the unfolding of currying and promotion, we show that it preserves renaming. We have already established in Lemma D.19 that (global) renamings preserve valid runs. In order for renamings to preserve the unfolding, we must ensure that the dependency between instantiated transitions is preserved as well.

**LEMMA E.18.** Consider A, B games, $h = [f, (g_m)]$: $A \rightsquigarrow B$, $\sigma: A$, and $\rho: \emptyset \longrightarrow \sigma$ valid.
For all $e, e' \in \mathcal{E}_\rho$, we have $e \leq_{\rho} e'$ iff $e[h] \leq_{\rho[h]} e'[h]$.

**PROOF.** Consider $e \to_{\rho} e'$. W.l.o.g. we assume that this dependency cannot be deduced otherwise by transitivity. By Lemma E.4, we can assume that $e$ and $e'$ appear subsequently in $\rho$. Assume first $e \to_{A} e'$. By definition,

$$ e: \alpha \stackrel{a}{\mapsto}_{\sigma} \beta, \qquad e': \alpha' \stackrel{a'}{\mapsto}_{\sigma} \beta' $$

with $a \to_A a'$, while by construction, $e[h] : \alpha \stackrel{ha}{\mapsto}_{\sigma[h]} \beta$ and $e'[h] : \alpha' \stackrel{ha'}{\mapsto}_{\sigma[h]} \beta'$. Now, we distinguish cases depending on the polarity of $a, a'$. If $\text{pol}_A(a) = +$ or $\text{pol}_A(a') = -$, then by courtesy we have $ha \to_B ha'$, so that $e[h] \to_B e'[h]$. If $\text{pol}_A(a) = -$ and $\text{pol}_A(a') = +$, then

$$ e = t^{-} \langle (s, d) \rangle : \emptyset \stackrel{a}{\mapsto}_{\sigma} \beta, \qquad e' = t^{+} \langle (\alpha') \rangle : \alpha' \stackrel{a'}{\mapsto}_{\sigma} \emptyset. $$

Assume, seeking a contradiction, that $\beta \cap \alpha' = \emptyset$, and consider the prefix of $\rho$:

$$ \rho'(t^{-} \langle (s, d) \rangle \uplus \gamma)(t^{+} \langle (\alpha') \rangle \uplus \gamma') : \emptyset \longrightarrow \sigma v, $$

but if indeed $\beta \cap \alpha' = \emptyset$, then $e$ and $e'$ permute as in

$$ \rho'(t^{+} \langle (\alpha') \rangle \uplus \mu)(t^{-} \langle (s, d) \rangle \uplus \mu') : \emptyset \longrightarrow \sigma v $$

and by valid, this entails $\text{play}(\rho')a' \in \text{Plays}(A)$, contradicting $a \to_A a'$. Assume now $e \to_{\sigma} e'$. This comes either from $\text{new}(e) \cap \text{pre}(e') \neq \emptyset$, or $\text{post}(e) \cap \text{eat}(e') \neq \emptyset$. But the renaming of instantiated transitions does not change pre- and post-conditions, so $e[h] \to_{\rho[h]} e'[h]$ still.

Reciprocally, assume $e[h] \leq_{\rho[h]} e'[h]$. Seeking a contradiction, assume $\neg (e \leq_{\rho} e')$. By Lemma E.4, we can assume that $e'$ appears before $e$ in $\rho$. Hence, $e'[h]$ appears before $e[h]$ in $\rho[h]$. But by Lemma D.19 $\rho[h]$ is valid, so by Lemma E.4 $e[h]$ must appear before $e'[h]$, contradiction. □

Next, we need to show that valid runs are also reflected by renamings:

**LEMMA E.19.** Consider A, B games, $\sigma: A, h = [f, (g_m)]$: $A \rightsquigarrow B$, and $\rho' : \emptyset \longrightarrow \sigma[h] \alpha$ valid.
Then, there is a unique $\rho : \emptyset \longrightarrow \sigma \alpha$ valid such that $\rho' = \rho[h]$.

**PROOF.** By induction on $\rho'$. If it is empty, this is clear. Consider $\rho'f^0$ with $\rho' : \emptyset \longrightarrow \sigma[h] \alpha$ and $f^0 = t^0 \langle \mu \rangle \uplus \gamma : \alpha \longrightarrow \sigma[h] \beta$, with $t^0 \langle \mu \rangle : \mu \longmapsto \sigma[h] v$. By IH, there is $\rho : \emptyset \longrightarrow \sigma \alpha$. By definition, we still have $t^0 \langle \mu \rangle \uplus \gamma : \alpha \longrightarrow \sigma \beta$, so $\rho f^0 : \emptyset \longrightarrow \sigma \beta$ and as required, $(\rho f^0)[h] = \rho' f^0$.
Next, consider $\rho'f^+$ with $\rho' : \emptyset \to_{\sigma[h]} \alpha$ and $f^+ = t^+(\mu) \upharpoonright \gamma : \alpha \to_{\sigma[h]} \beta$, with $t^+(\mu) : \mu \mapsto_{\sigma[h]} \emptyset$. Necessarily, $b' = (f(m), d', s')$ for $m = \partial_\sigma(t^+)$, and $(d', s') = g_m(d, s)$ for $(d, s) = \delta(t^+)(\mu)$ - so $b = h(b)$ for $b = (m, d, s)$. But then, by definition, $t^+(\mu) : \mu \mapsto_{\sigma} \emptyset$ as well, so $f^+ : \alpha \to \sigma \beta$. By IH, there is $\rho : \emptyset \to \sigma \alpha$ such that $\rho[h] = \rho'$. By valid, $\rho f^+$ is still valid, and $(\rho f^+)[h] = \rho' f^+$.

Finally, consider $\rho'f^-$ with $\rho' : \emptyset \to_{\sigma[h]} \alpha$ and $f^- = t^-(\|s', d'\|) \upharpoonright \gamma : \alpha \to_{\sigma[h]} \beta$, with $t^-(\|s', d'\|) : \emptyset \mapsto_{\sigma[h]} \nu$. Here, necessarily, $b' = (m', s', d')$ where $m' = f(m)$, $m = \partial_\sigma(t^-)$, $(s', d') = g_m(s, d)$. In other words, $b' = h(b)$ with $b = (m, s, d)$. Now, by IH we have $\rho : \emptyset \to \sigma \alpha$ with $\rho[h] = \rho'$. Besides, we have the transition $t^-(\|s, d\|) : \emptyset \mapsto_{\sigma} \nu$, so that $(t^-(\|s, d\|) \upharpoonright \gamma) : \alpha \to \sigma \beta$. Its validity follows immediately from receptivity of global renamings (and the fact that they are injective). It is clear that $(\rho(t^-(\|s, d\|) \upharpoonright \gamma))[h] = \rho'f^-$ as required.

Finally, uniqueness is immediate by induction and injectivity of $h$. □

**LEMMA E.20.** Consider A, B games, $\sigma: A$ a Petri strategy, and $h = [f, (g_m)] : A \rightsquigarrow B$. Then, $\mathcal{U}(\sigma[h]) \cong \mathcal{U}(\sigma)[h]$.

**PROOF.** We construct an order-isomorphism

$$-[h] : \mathcal{E}^+(\sigma) \cong \mathcal{E}^+(\sigma[h]) \qquad (6)$$

such that $\partial_{\sigma[h]}(x) = h(\partial_{\sigma}(x))$ for all $x \in \mathcal{E}^+(\sigma)$. Given $x \in \mathcal{E}^+(\sigma)$, there is some $\rho$ a valid run in $\sigma$ such that $x = \mathcal{E}(\rho)$. By Lemma D.19, $\rho[h]$ is a valid run of $\sigma[h]$, so we may consider $x[h] = \mathcal{E}(\rho[h])$. By Lemma E.18, $-[h]$ on instantiated transitions is an order-isomorphism $-[h] : x \cong x[h]$, so $x[h] \in \mathcal{E}^+(\sigma[h])$. Together with Lemma E.19, this easily entails that we get $-[h] : \mathcal{E}(\sigma) \cong \mathcal{E}(\sigma[h])$ an order-isomorphism. By definition, for each $x \in \mathcal{E}(\sigma)$ we have an order-iso $x \cong x[h]$ defined by applying $-[h]$ on each transition - thus, $-[h]$ preserves and reflects +-covered histories. The requirement w.r.t. labels is obvious by construction.

By Lemma E.9, we also obtain an order-isomorphism

$$-[h] : \mathcal{E}^+(\mathcal{U}(\sigma)) \cong \mathcal{E}^+(\mathcal{U}(\sigma[h]))$$

such that $\partial_{\mathcal{U}(\sigma[h])}(x[h]) = h(\partial_{\mathcal{U}(\sigma)}(x))$ for any $x \in \mathcal{E}^+(\mathcal{U}(\sigma))$, so, from Definition B.1, an order-isomorphism $-[h] : \mathcal{E}^+(\mathcal{U}(\sigma)[h]) \cong \mathcal{E}^+(\mathcal{U}(\sigma[h]))$ such that $\partial_{\mathcal{U}(\sigma[h])}(x[h]) = \partial_{\mathcal{U}(\sigma)[h]}(x)$ for all $x \in \mathcal{E}^+(\mathcal{U}(\sigma)[h])$. By Lemma E.9, it follows that $\mathcal{U}(\sigma)[h]$ and $\mathcal{U}(\sigma[h])$ are isomorphic. □

**E.4.3** *Currying.* Follows from Lemma E.20, as currying is obtained with the same global renaming both in PStrat and in Strat.

**E.4.4** *Promotion.* Let us start with characterizing +-covered traces of the functorial promotion.

**LEMMA E.21.** Consider $\sigma: A \vdash B$ a Petri strategy. Then, we have an order-iso

$$[-] : \mathrm{Fam}(\mathcal{E}^{+, \neq 0}(\sigma)) \cong \mathcal{E}^+(\mathcal{F}(\sigma))$$

satisfying that for all $(x^e)_{e \in E} \in \mathrm{Fam}(\mathcal{E}^{+, \neq 0}(\sigma))$, we have

$$\partial_{\sigma}([ (x^e)_{e \in E} ]) = \left( \bigcup_{e \in E} e \::\:: x_A^e \right) \vdash \left( \bigcup_{e \in E} e \::\:: x_B^e \right)$$

writing $\partial_{\sigma}(x^e) = x_A^e \vdash x_B^e$ for all $e \in E$.

**PROOF.** This is a $n$-ary adaptation of the proof of Lemma E.16. Consider $(x^e)_{e \in E} \in \mathrm{Fam}(\mathcal{E}^{+, \neq 0}(\sigma))$. By definition, there is a valid run

$$\rho^e : \emptyset \to \sigma \alpha^e$$
for all $e \in E$ such that $x^e = \mathscr{E}_{\rho^e}$. We define the history $[(x^e)_{e \in E}]$ as

$$ 
\begin{align*}
[x^e \mid e \in E] &= \{t^0(e \:: \alpha) \mid e \in E, t^0(\alpha) \in x^e\} \\
\cup &\{t^+(e \:: \alpha) \mid e \in E, t^+(\alpha) \in x^e\} \\
\cup &\{t^-(e \:: s, d) \mid e \in E, t^-(s, d) \in x^e\}.
\end{align*}
$$

We construct a run $\rho$ obtained by concatenating all $\rho^e$s in the obvious way as in Lemma E.16. Exploiting Lemma D.27, it is a valid run and $[x^e \mid e \in E] = \mathscr{E}(\rho)$ by construction. By definition of the causal ordering of instantiated transitions, it is also immediate that $[x^e \mid e \in E]$ is +-covered; and that this preserves the labelling. Reciprocally, for any $x \in \mathscr{E}(\neg \sigma)$, we consider the projections

$$x^e = \pi_e^t(x)$$

and it follows from Lemma D.28 that $x^e \in \mathscr{E}(\sigma)$ for all $e \in E$. From the definition of the causal ordering of instantiated transitions, each $x^e$ is still +-covered.

Finally, these two transformations are inverses as required. □

COROLLARY E.22. Consider $\sigma$ : $!A \vdash B$ a Petri strategy. Then, we have $\mathcal{U}(\sigma^\dagger) \cong \mathcal{U}(\sigma)^\dagger$.

PROOF. We exploit the following sequence of label-preserving order-isomorphisms:

$$ 
\begin{align*}
\mathscr{C}^+(\mathcal{U}(\sigma^\dagger)) &\cong \mathscr{C}^+(\sigma^\dagger) \\
&= \mathscr{C}^+((\neg\sigma)[\mathrm{dig} \vdash \mathrm{id}]) \\
&\cong \mathscr{C}^+(\neg\sigma) \\
&\cong \mathrm{Fam}(\mathscr{C}^{+,\neq\emptyset}(\sigma)) \\
&\cong \mathrm{Fam}(\mathscr{C}^{+,\neq\emptyset}(\mathcal{U}(\sigma)))
\end{align*}
$$

using first Lemma E.9, then via a direct verification as in Proposition D.32, then applying (6), followed by Lemma E.21, and then Lemma E.9 – with the obvious verification that it specializes to an iso between non-empty configurations and histories. It is a direct verification that this sequence of isomorphisms preserves display maps.

Consequently, it follows that $\mathcal{U}(\sigma^\dagger) \cong \mathcal{U}(\sigma)^\dagger$ from Proposition C.16. □

## E.5 The Unfolding Preserves Primitives

### E.5.1 Variable and Evaluation. Follows from Lemma E.20.

### E.5.2 Queries, Conditional, Constants. It is a simple calculation to compute the unfolding for these linear Petri strategies and check we obtain the desired finite strategy.

### E.5.3 Fixpoint. We prove the following proposition:

PROPOSITION E.23. For any well-opened arena $O$, $\mathcal{U}(Y_O) \cong Y_O$.

PROOF. Using Lemmas C.5 and E.9, the required isomorphism boils down to an order-iso

$$\mathscr{C}^+(Y_O) \cong \mathscr{C}^+(Y_O)$$

preserving display maps. We build it using Lemmas D.35 and C.22. It is clearly injective so we simply have to show it is surjective. Consider a +-covered configuration $x$ of $Y_O$ represented as a tuple $(J, z, (y_S)_{s \in J})$. We can construct a set of events realising $x$ as follows:

* For each $(m, s, d)^- \in z$ we include the event $\mathfrak{r}_m m((s, d))$, and $\ell, \mathfrak{r}_\infty((\ell, \diamond \:: s, d)^{\mathrm{@m}^-})$

* For each $(m, s, d)^+ \in z$, we include the events $\ell, \mathfrak{r}_\infty((\ell, \diamond \:: s, d))$ and $\mathfrak{r}_m m((\ell, \diamond \:: s, d)^{\mathrm{@m}^+})$

* For each $(m, s_0, d)^- \in y_{e \cdot s}$, we include the events $\mathfrak{r}_m \mathfrak{r}_\infty m((e \:: (s) \:: s_0, d))$ and $\mathfrak{r}_m \mathfrak{r}_\infty m(((e \cdot s) \:: s_0, d)^{\mathrm{@m}^-})$.
* For each $(m, s_0, d)^+ \in y_{e \cdot s}$, we include the events $\tau_e l_\alpha m |((e \cdot s) :: s_0, d))|$ and $\tau_e l_\alpha m |((e \cdot s) :: s_0, d)@m^+)}$,

and it is easy to see that this set of transitions is reachable by a valid run of $Y_O$.

□

**E.5.4 Contraction.** The reasoning follows a similar and simpler route as for the fixpoint operator.

**E.5.5 Let bindings.** We first characterise the configurations of the strategy interpreting lets.

**LEMMA E.24.** *The +-covered configurations of let are order-isomorphic to tuples $\langle I \subseteq \mathcal{E}, x \in \mathcal{C}(X), y, y' \in \mathcal{C}(Y)\rangle$ such that:*

(1) $y \neq \emptyset$ iff $x \neq \emptyset$

(2) $x$ is maximal iff $y' \neq \emptyset$

(3) if $y' \neq \emptyset$, then $y = y'$.

(4) if $y' = \emptyset$, then $I = \emptyset$.

The isomorphism sends such tuples to $((\cup_{e \in I}(e :: x)) \to y') \otimes x \vdash y$.

**LEMMA E.25.** *We have $\mathcal{U}(\mathcal{L}) \cong \mathcal{L}$.*

**PROOF.** As before we rely on Lemmas C.5 and E.9 to build the isomorphism. Lemma D.37 together with Lemma E.24 induce an injective map from $\mathcal{C}^+(\mathcal{L})$ into $\mathcal{C}^+(\mathcal{L})$. We show it is surjective by constructing a set of eventse of $\mathcal{L}$ from $x \in \mathcal{C}^+(\mathcal{L})$ corresponding to a $\langle I, x, y, y' \rangle$.

* If $y \neq \emptyset$, then we have events $\tau_e Q^- |([], \bullet)]$ and $\tau_e Q^+ |([], \bullet)^{@1}]$

* If $x$ has an event $([], d)$ maximal in $X$, then we have the two events $\ell_e \tau_e A^- |([], d)]$, and $\ell_e \ell_\alpha \tau_e Q^+ |([], \bullet)^{@2}]$

* For every $e \in I$, we have three events written $\ell_e \ell_\alpha \ell_\beta Q^- |([e], \bullet)]$, $s|([], \bullet)^{@4}$, $([], d)^{@3}]$, and $\ell_e \ell_\alpha \ell_\beta A^+ |([e], d)^{@5}]$ where $d$ is the value of the maximal event in $x$.

* If $y'$ has a maximal $([], d)$, we have events $\ell_e \ell_\alpha \tau_e A^- |([], d)]$ and $\tau_e A^+ |([], d)^{@6}]$.

□

**E.5.6 Newref and newsem.** We now show that the unfolding of the net for newref is indeed the strategy newref. Our first step is to show that the consistent memory traces described in Section D.3.6 correspond to +-covered configurations of newref:

**LEMMA E.26.** *There is an order-isomorphism between $\mathcal{C}^+(\text{precell})$ and the set of consistent memory traces ordered by prefix.*

**PROOF.** Direct from the definition of precell.

□

We now show the main result:

**PROPOSITION E.27.** $\mathcal{U}(\mathcal{N}ewref) \cong \mathcal{N}ewref$.

**PROOF.** By Lemmas C.5 and E.9, this amounts to building an order-iso:

$$ \mathcal{C}^+(\mathcal{N}ewref) \cong \mathcal{C}^+(\mathcal{N}ewref). $$

*From left-to-right.* We focus on non-empty histories and configurations and use characterisation of $\mathcal{C}^+(\mathcal{N}ewref)$ from Proposition C.26.

Consider a non-empty history $y \in \mathcal{C}^+(\mathcal{N}ewref)$. It is reached by a run $\rho: \emptyset \xrightarrow{s} \alpha$. By Lemma D.39, we know that there $\text{Tr}(\rho)$ is a consistent memory trace, and that $|s|$ must have the shape $((\cup_{e \in I}(e :: x_e)) \to w) \vdash z$. Since $y$ is +-covered, we observe that $w = z$. We can thus map $y$ to $\langle \text{Tr}(\rho), w \rangle \in \mathcal{C}^+(\mathcal{N}ewref)$ using the isomorphism of Proposition C.26. Note that by the side conditions of Lemma D.39, the family $(x_e)_{e \in I}$ is entirely determined by $\text{Tr}(\rho)$: $I$ matches the length of $\text{Tr}(\rho)$ and each $x_e$ is a two-event configuration corresponding to the memory operation $\text{Tr}(\rho)_e$.
The last check it to show that this does not depend on the particular run $\rho$ chosen. Clearly $x$ only depends on $|s|$. For $\text{Tr}(\rho)$, we observe that it is actually directly recoverable from the set of transitions $y$. First, we define the set of memory operations $O_y$ to contain $(w, e, d)$ if $w({[e], d}@^3, \_} \in y$ and $(r, e, d)$ if $r({[e], \_}@^5, \_(d}@^2} \in y$. Then, the causal order on $y$ induces a linear order on $O_y$ due to the threading of exponential signatures. The resulting trace is exactly $\text{Tr}(\rho)$.

*From right-to-left.* Consider now a $\langle\rho, x\rangle \in \mathscr{C}^{+,-\emptyset}(\text{newref})$ where $\rho$ is a consistent memory trace. We can build a history $y$ containing the following instantiated transitions:

* The initial negative event on $\mathscr{r}_c Q(\llbracket \emptyset, \bullet \rrbracket)$.

* The positive event $\ell_c \ell_{-c} Q(\llbracket \emptyset, \bullet \rrbracket)^{@1})$.

* If $x$ contains a move $(A, \emptyset, d)$, then the events $\ell_c \mathscr{r}_c A^- (\llbracket \emptyset, d \rrbracket)$ and $\mathscr{r}_c A^+ (\llbracket \emptyset, d \rrbracket)^{@7})$.

* If $\rho_i = (w, e, d)$ then the events $\ell_c \ell_{-c} w_{\phi} Q^{-} (\llbracket e, d \rrbracket)$, $w(\llbracket e, d \rrbracket^3, \{[e'], d'\}^2\})$ where: $e'$ is the exponential token of $\rho_{i-1}$ (or $\emptyset$ if $i=0$), and $d'$ the value observed by $\rho_{i-1}$ (or zero if $i=0$); and $\ell_c \ell_{-c} w_{\phi} A^+ (\llbracket e, \check{\phantom{0}} \rrbracket)^@4\})$.

* And similarly if $\rho_i = (r, e, d)$.

From this description, it is easy to build a valid run reaching $y$ establishing that $y \in \mathscr{C}(\text{newref})$. An easy verification shows that all maximal events in $y$ are positive. $\square$

Received 2022-07-07; accepted 2022-11-07