to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{49.53105pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{N}}}\shuffle\makebox[11.86668pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}}}$}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{49.53105pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{N}}}\shuffle\makebox[11.86668pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}}}$}})}}$}}\cup\\{\epsilon\\}$.

###  B.3 Proof of Proposition 18: Regularity and Connectives

######  Proposition 84.

  1. 1.

If ${\mathbf{N}}$ is regular then $\shpos{\mathbf{N}}$ is regular.

  2. 2.

If ${\mathbf{P}}$ is regular then $\shneg{\mathbf{P}}$ is regular.

###### Proof.

  1. 1.

Following Proposition 75:

     * •

By internal completeness, the trivial views of $\shpos{\mathbf{N}}$ are of the
form $\kappa_{\blacktriangledown}{\mathbb{t}}$ where ${\mathbb{t}}$ is a
trivial view of ${\mathbf{N}}$. Since ${\mathbf{N}}$ is regular
${\mathbb{t}}\in V_{{\mathbf{N}}}$. Hence by Proposition 78,
$\kappa_{\blacktriangledown}{\mathbb{t}}\in V_{{\mathbf{\shpos N}}}$.

     * •

Since $V_{{\mathbf{N}}}$ is stable by shuffle, so is $V_{{\mathbf{\shpos
N}}}=\kappa_{\blacktriangledown}V_{{\mathbf{N}}}^{x}$ where
$\kappa_{\blacktriangledown}$ is a positive action.

     * •

For all paths $\kappa_{\blacktriangle}\mathpzc{s}$,
$\kappa_{\blacktriangle}\mathpzc{t}\in V_{{\mathbf{(\shpos
N)^{\perp}}}}=\kappa_{\blacktriangle}V_{{\mathbf{N^{\perp}}}}^{x}$ such that
$\kappa_{\blacktriangle}\mathpzc{s}\shuffle\kappa_{\blacktriangle}\mathpzc{t}$
is defined, $\mathpzc{s}$ and $\mathpzc{t}$ start necessarily by the same
positive action and $\mathpzc{s}\shuffle\mathpzc{t}\subseteq
V_{{\mathbf{N^{\perp}}}}^{x}$ because $V_{{\mathbf{N^{\perp}}}}$ (thus also
$V_{{\mathbf{N^{\perp}}}}^{x}$) is stable by $\shuffle$, hence
$\kappa_{\blacktriangle}\mathpzc{s}\shuffle\kappa_{\blacktriangle}\mathpzc{t}=\kappa_{\blacktriangle}(\mathpzc{s}\shuffle\mathpzc{t})\subseteq
V_{{\mathbf{(\shpos N)^{\perp}}}}$.

  2. 2.

If ${\mathbf{P}}$ is regular then ${\mathbf{P}}^{\perp}$ is too. Then by
previous point $\shpos{\mathbf{P}}^{\perp}$ is regular, therefore so is
$(\shpos{\mathbf{P}}^{\perp})^{\perp}$. By Lemma 77, this means that
$\shneg{\mathbf{P}}$ is regular.

∎

######  Proposition 85.

If ${\mathbf{M}}$ and ${\mathbf{N}}$ are regular then
${\mathbf{M}}\oplus{\mathbf{N}}$ is regular.

###### Proof.

Similar to Proposition 84 (1), by the same remark as in proof of Proposition
79. ∎

In order to show that $\otimes$ preserves regularity, consider first the
following definitions and lemma. We call quasi-path a positive-ended P-visible
aj-sequence. The shuffle $\mathpzc{s}\shuffle\mathpzc{t}$ of two negative
quasi-paths $\mathpzc{s}$ and $\mathpzc{t}$ is the set of paths $\mathpzc{u}$
formed with actions from $\mathpzc{s}$ and $\mathpzc{t}$ such that
$\mathinner{\mathchoice{\mathpzc{u}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\mathpzc{u}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\mathpzc{u}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{s}}{\mathpzc{u}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}}=\mathpzc{s}$
and
$\mathinner{\mathchoice{\mathpzc{u}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{t}}{\mathpzc{u}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}}=\mathpzc{t}$.

######  Lemma 86.

Let $\mathpzc{s}$ and $\mathpzc{t}$ be negative quasi-paths. If
$\mathpzc{s}\shuffle\mathpzc{t}\neq\emptyset$ then $\mathpzc{s}$ and
$\mathpzc{t}$ are paths.

###### Proof.

We prove the result by contradiction. Let us suppose that there exists a
triple $(\mathpzc{s},\mathpzc{t},\mathpzc{u})$ such that $\mathpzc{s}$ and
$\mathpzc{t}$ are two negative quasi-paths,
$\mathpzc{u}\in\mathpzc{s}\shuffle\mathpzc{t}$ is a path, and at least one of
$\mathpzc{s}$ or $\mathpzc{t}$ does not satisfy O-visibility, say
$\mathpzc{s}$: there exists a negative action $\kappa^{-}$ and a prefix
$\mathpzc{s}_{0}\kappa^{-}$ of $\mathpzc{s}$ such that the action $\kappa^{-}$
is justified in $\mathpzc{s}_{0}$ but $\mathrm{just}(\kappa^{-})$ does not
appear in ${\llcorner\mathpzc{s}_{0}\lrcorner}$.

We choose the triple $(\mathpzc{s},\mathpzc{t},\mathpzc{u})$ such that the
length of $\mathpzc{u}$ is minimal with respect to all such triples. Without
loss of generality, we can assume that $\mathpzc{u}$ and $\mathpzc{s}$ are of
the form $\mathpzc{u}=\mathpzc{u}_{0}\kappa^{-}\maltese$ and
$\mathpzc{s}=\mathpzc{s}_{0}\kappa^{-}\maltese$ respectively. Indeed, if this
is not true, $\mathpzc{u}$ has a strict prefix of the form
$\mathpzc{u}_{0}\kappa^{-}$; in this case we can replace
$(\mathpzc{s},\mathpzc{t},\mathpzc{u})$ by the triple
$(\mathpzc{s}_{0}\kappa^{-}\maltese,\mathinner{\mathchoice{\mathpzc{u}_{0}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}_{0}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}_{0}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{t}}{\mathpzc{u}_{0}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}},\mathpzc{u}_{0}\kappa^{-}\maltese)$
which satisfies all the constraints, and where the length of
$\mathpzc{u}_{0}\kappa^{-}\maltese$ is less or equal to the length of
$\mathpzc{u}$.

Let $\kappa^{+}=\mathrm{just}(\kappa^{-})$. $\mathpzc{u}$ is necessarily of
the form
$\mathpzc{u}=\mathpzc{u}_{1}\alpha^{-}\mathpzc{u}_{2}\alpha^{+}\kappa^{-}\maltese$
where $\alpha^{-}$ justifies $\alpha^{+}$ and $\kappa^{+}$ appears in
$\mathpzc{u}_{1}$, indeed:

  * •

$\kappa^{+}$ does not appear immediately before $\kappa^{-}$ in $\mathpzc{u}$,
otherwise it would also be the case in $\mathpzc{s}$, contradicting the fact
that $\kappa^{-}$ is not O-visible in $\mathpzc{s}$.

  * •

The action $\alpha^{+}$ which is immediately before $\kappa^{-}$ in
$\mathpzc{u}$ is justified by an action $\alpha^{-}$, and $\kappa^{+}$ appears
before $\alpha^{-}$ in $\mathpzc{u}$, otherwise $\kappa^{+}$ would not appear
in ${\llcorner\mathpzc{u}_{0}\lrcorner}$ and that would contradict
O-visibility of $\mathpzc{u}$.

Let us show by contradiction something that will be useful for the rest of
this proof: in the path $\mathpzc{u}$, all the actions of $\mathpzc{u}_{2}$
(which cannot be initial) are justified in $\alpha^{-}\mathpzc{u}_{2}$. If it
is not the case, let $\mathpzc{u}_{1}\alpha^{-}\mathpzc{u}^{\prime}_{2}\beta$
be longest prefix of $\mathpzc{u}$ such that $\beta$ is an action of
$\mathpzc{u}_{2}$ justified in $\mathpzc{u}_{1}$, and let $\beta^{\prime}$ be
the following action (necessarily in $\mathpzc{u}_{2}\alpha^{+}$), thus
$\beta^{\prime}$ is justified in $\alpha^{-}\mathpzc{u}_{2}$. If
$\beta^{\prime}$ is positive (resp. negative) then $\beta$ is negative (resp.
positive), thus
$\raisebox{2.02205pt}{$\ulcorner$}{\mathpzc{u}_{1}\alpha^{-}\mathpzc{u}^{\prime}_{2}\beta}\raisebox{2.02205pt}{$\urcorner$}=\raisebox{0.9387pt}{$\ulcorner$}{\mathpzc{u}^{\prime}_{1}}\raisebox{0.9387pt}{$\urcorner$}$
(resp.
${\llcorner\mathpzc{u}_{1}\alpha^{-}\mathpzc{u}^{\prime}_{2}\beta\lrcorner}={\llcorner\mathpzc{u}^{\prime}_{1}\lrcorner}$)
where $\mathpzc{u}^{\prime}_{1}$ is the prefix of $\mathpzc{u}_{1}$ ending on
$\mathrm{just}(\beta)$. But then
$\raisebox{2.02205pt}{$\ulcorner$}{\mathpzc{u}_{1}\alpha^{-}\mathpzc{u}^{\prime}_{2}\beta}\raisebox{2.02205pt}{$\urcorner$}$
(resp.
${\llcorner\mathpzc{u}_{1}\alpha^{-}\mathpzc{u}^{\prime}_{2}\beta\lrcorner}$)
does not contain $\mathrm{just}(\beta^{\prime})$: this contradicts the fact
that $\mathpzc{u}$ is a path, since P-visibility (resp. O-visibility) is not
satisfied.

Now define $\mathpzc{u}^{\prime}=\mathpzc{u}_{1}\kappa^{-}\maltese$,
$\mathpzc{s}^{\prime}=\mathinner{\mathchoice{\mathpzc{u}^{\prime}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\mathpzc{u}^{\prime}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\mathpzc{u}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{s}}{\mathpzc{u}^{\prime}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}}$
and
$\mathpzc{t}^{\prime}=\mathinner{\mathchoice{\mathpzc{u}^{\prime}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}^{\prime}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{t}}{\mathpzc{u}^{\prime}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}}$,
and remark that:

  * •

$\mathpzc{u}^{\prime}$ is a path, indeed, O-visibility for $\kappa^{-}$ is
still satisfied since
${\llcorner\mathpzc{u}_{1}\alpha^{-}\mathpzc{u}_{2}\alpha^{+}\kappa^{-}\lrcorner}={\llcorner\mathpzc{u}_{1}\lrcorner}\alpha^{-}\alpha^{+}\kappa^{-}$
and
${\llcorner\mathpzc{u}_{1}\kappa^{-}\lrcorner}={\llcorner\mathpzc{u}_{1}\lrcorner}\kappa^{-}$
both contain $\kappa^{+}$ in ${\llcorner\mathpzc{u}_{1}\lrcorner}$.

  * •

$\mathpzc{s}^{\prime}$ and $\mathpzc{t}^{\prime}$ are quasi-paths, since
$\mathpzc{s}^{\prime}$ is of the form
$\mathpzc{s}^{\prime}=\mathpzc{s}_{1}\kappa^{-}\maltese$ where
$\mathpzc{s}_{1}=\mathinner{\mathchoice{\mathpzc{u}_{1}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\mathpzc{u}_{1}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\mathpzc{u}_{1}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{s}}{\mathpzc{u}_{1}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}}$ is
a prefix of $\mathpzc{s}$ containing $\kappa^{+}=\mathrm{just}(\kappa^{-})$,
and
$\mathpzc{t}^{\prime}=\mathinner{\mathchoice{\mathpzc{u}^{\prime}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}^{\prime}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{t}}{\mathpzc{u}^{\prime}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}}=\mathinner{\mathchoice{\mathpzc{u}_{1}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}_{1}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}{\mathpzc{u}_{1}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{t}}{\mathpzc{u}_{1}\\!\\!\upharpoonright\\!\\!\mathpzc{t}}}$ is
a prefix of $\mathpzc{t}$.

  * •

$\mathpzc{u}^{\prime}\in\mathpzc{s}^{\prime}\shuffle\mathpzc{t}^{\prime}$.

  * •

$\mathpzc{s}^{\prime}$ is not a path: Note that $\mathpzc{s}$ is of the form
$\mathpzc{s}_{1}\mathpzc{s}_{2}\kappa^{-}\maltese$ where
$\mathpzc{s}_{1}=\mathinner{\mathchoice{\mathpzc{u}_{1}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\mathpzc{u}_{1}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\mathpzc{u}_{1}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{s}}{\mathpzc{u}_{1}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}}$ and
$\mathpzc{s}_{2}=\mathinner{\mathchoice{\alpha^{-}\mathpzc{u}_{2}\alpha^{+}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\alpha^{-}\mathpzc{u}_{2}\alpha^{+}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}{\alpha^{-}\mathpzc{u}_{2}\alpha^{+}\mkern
1.0mu\upharpoonright\mkern
1.0mu\mathpzc{s}}{\alpha^{-}\mathpzc{u}_{2}\alpha^{+}\\!\\!\upharpoonright\\!\\!\mathpzc{s}}}$.
By hypothesis, $\mathpzc{s}$ is not a path because $\kappa^{+}$ does not
appear in ${\llcorner\mathpzc{s}_{1}\mathpzc{s}_{2}\lrcorner}$. But
${\llcorner\mathpzc{s}_{1}\mathpzc{s}_{2}\lrcorner}$ is of the form
${\llcorner\mathpzc{s}_{1}\lrcorner}\mathpzc{s}_{2}^{\prime}$, since all the
actions of $\mathpzc{s}_{2}$ are hereditarily justified by the first
(necessarily negative) action of $\mathpzc{s}_{2}$, indeed: we have proved
that, in $\mathpzc{u}$, all the actions of $\mathpzc{u}_{2}$ (in particular
those of $\mathpzc{s}_{2}$) were justified in $\alpha^{-}\mathpzc{u}_{2}$.
Thus $\kappa^{+}$ does not appear in ${\llcorner\mathpzc{s}_{1}\lrcorner}$,
which means that O-visibility is not satisfied for $\kappa^{-}$ in
$\mathpzc{s}^{\prime}=\mathpzc{s}_{1}\kappa^{-}\maltese$.

Hence the triple
$(\mathpzc{s}^{\prime},\mathpzc{t}^{\prime},\mathpzc{u}^{\prime})$ satisfies
all the conditions. This contradicts the minimality of $\mathpzc{u}$. ∎

######  Proposition 87.

If ${\mathbf{M}}$ and ${\mathbf{N}}$ are regular, then
${\mathbf{M}}\otimes{\mathbf{N}}$ is regular.

###### Proof.

Following Proposition 75, we will prove that the positive-ended trivial views
of ${\mathbf{M}}\otimes{\mathbf{N}}$ are visitable in
${\mathbf{M}}\otimes{\mathbf{N}}$, and that $V_{{\mathbf{M\otimes N}}}$ and
$V_{{\mathbf{(M\otimes N)^{\perp}}}}$ are stable by shuffle.

Every trivial view of ${\mathbf{M}}\otimes{\mathbf{N}}$ is of the form
$\kappa_{\bullet}{\mathbb{t}}$. It follows from internal completeness
(incarnated form) that $\kappa_{\bullet}{\mathbb{t}}$ is a trivial view of
${\mathbf{M}}\otimes{\mathbf{N}}$ iff ${\mathbb{t}}$ is a trivial view either
of ${\mathbf{M}}^{x}$ or of ${\mathbf{N}}^{y}$. As ${\mathbf{M}}$ (resp.
${\mathbf{N}}$) is regular, positive-ended trivial views of ${\mathbf{M}}^{x}$
(resp. ${\mathbf{N}}^{y}$) are in $V_{{\mathbf{M}}}^{x}$ (resp.
$V_{{\mathbf{N}}}^{y}$). Thus by Proposition 82, positive-ended trivial views
of ${\mathbf{M}}\otimes{\mathbf{N}}$ are in $V_{{\mathbf{M\otimes N}}}$.

From Proposition 82, and from the fact that $\shuffle$ is associative and
commutative, we also have that $V_{{\mathbf{M\otimes N}}}$ is stable by
shuffle.

Let us prove that $V_{{\mathbf{M\otimes N}}}$ is stable by anti-shuffle. Let
$\mathpzc{t},\mathpzc{u}\in V_{{\mathbf{M\otimes N}}}$ and let
$\mathpzc{s}\in\mathpzc{t}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\mathpzc{u}$,
we show that $\mathpzc{s}\in V_{{\mathbf{M\otimes N}}}$ by induction on the
length of $\mathpzc{s}$. Notice first that, from Proposition 82, there exist
paths $\mathpzc{t}_{1},\mathpzc{u}_{1}\in V_{{\mathbf{M}}}^{x}$ and
$\mathpzc{t}_{2},\mathpzc{u}_{2}\in V_{{\mathbf{N}}}^{y}$ such that
$\mathpzc{t}\in\kappa_{\bullet}(\mathpzc{t}_{1}\shuffle\mathpzc{t}_{2})$ and
$\mathpzc{u}\in\kappa_{\bullet}(\mathpzc{u}_{1}\shuffle\mathpzc{u}_{2})$. In
the case $\mathpzc{s}$ of length $1$, either $\mathpzc{s}=\maltese$ or
$\mathpzc{s}=\kappa_{\bullet}$, thus the result is immediate. So suppose
$\mathpzc{s}=\mathpzc{s}^{\prime}\kappa^{-}\kappa^{+}$ and by induction
hypothesis $\mathpzc{s}^{\prime}\in V_{{\mathbf{M\otimes N}}}$. Hence, it
follows from Proposition 82 that there exist paths $\mathpzc{s}_{1}\in
V_{{\mathbf{M}}}^{x}$ and $\mathpzc{s}_{2}\in V_{{\mathbf{N}}}^{y}$ such that
$\mathpzc{s}^{\prime}\in\kappa_{\bullet}(\mathpzc{s}_{1}\shuffle\mathpzc{s}_{2})$.
Without loss of generality, we can suppose that $\kappa^{-}$ is an action of
$\mathpzc{t}_{1}$, hence of $\mathpzc{t}$. We study the different cases,
proving each time either that $\mathpzc{s}\in V_{{\mathbf{M\otimes N}}}$ or
that the case is impossible.

  * •

Either $\kappa^{+}=\maltese$. In that case,
$\mathpzc{s}_{1}\kappa^{-}\maltese$ is a negative quasi-path. As $\mathpzc{s}$
is a path and
$\mathpzc{s}\in\kappa_{\bullet}(\mathpzc{s}_{1}\kappa^{-}\maltese\shuffle\mathpzc{s}_{2})$,
by Lemma 86, we have moreover that $\mathpzc{s}_{1}\kappa^{-}\maltese$ is a
path. Notice that
$\kappa_{\bullet}\langle\mathpzc{s}_{1}\kappa^{-}\rangle=\langle\kappa^{-}\rangle_{\mathpzc{s}}=\langle\kappa^{-}\rangle_{\mathpzc{t}}=\kappa_{\bullet}\langle\kappa^{-}\rangle_{\mathpzc{t}_{1}}$.
Hence
$\langle\mathpzc{s}_{1}\kappa^{-}\rangle=\langle\kappa^{-}\rangle_{\mathpzc{t}_{1}}$
is a trivial view of ${\mathbf{M}}^{x}$. Let
${\mathbb{t}}\kappa^{-}=\langle\mathpzc{s}_{1}\kappa^{-}\rangle$. By Lemma 74,
$\mathpzc{s}_{1}$ is a shuffle of anti-shuffles of trivial views of
${\mathbf{M}}^{x}$, one of which is the trivial view ${\mathbb{t}}$. Then
remark that $\mathpzc{s}_{1}\kappa^{-}\maltese$ is also a shuffle of anti-
shuffles of trivial views of ${\mathbf{M}}^{x}$, replacing ${\mathbb{t}}$ by
${\mathbb{t}}\kappa^{-}\maltese$ (note that ${\mathbb{t}}\kappa^{-}\maltese$
is indeed a trivial view of ${\mathbf{M}}^{x}$ since
${\mathbb{t}}\kappa^{-}\maltese=\langle\mathpzc{t}_{0}\kappa^{-}\maltese\rangle$
where $\mathpzc{t}_{0}\kappa^{-}$ is the prefix of $\mathpzc{t}_{1}$ ending
with $\kappa^{-}$, and $\mathpzc{t}_{0}\kappa^{-}\maltese\in
V_{{\mathbf{M}}}^{x}$ by Lemma 71). It follows from Proposition 75 that
$\mathpzc{s}_{1}\kappa^{-}\maltese\in V_{{\mathbf{M}}}^{x}$. Finally, as
$\mathpzc{s}\in\kappa_{\bullet}(\mathpzc{s}_{1}\kappa^{-}\maltese\shuffle\mathpzc{s}_{2})$
and by Proposition 82, we have $\mathpzc{s}\in V_{{\mathbf{M\otimes N}}}$.

  * •

Or $\kappa^{+}$ is a proper action of $\mathpzc{t}_{1}$, hence of
$\mathpzc{t}$. Remark that
$\raisebox{0.9387pt}{$\ulcorner$}{\mathpzc{s}^{\prime}\kappa^{-}}\raisebox{0.9387pt}{$\urcorner$}=\raisebox{0.5887pt}{$\ulcorner$}{\kappa_{\bullet}\mathpzc{s}_{1}\kappa^{-}}\raisebox{0.5887pt}{$\urcorner$}=\kappa_{\bullet}\raisebox{0.5887pt}{$\ulcorner$}{\mathpzc{s}_{1}\kappa^{-}}\raisebox{0.5887pt}{$\urcorner$}$,
thus $\mathrm{just}(\kappa^{+})$ appears in
$\raisebox{0.5887pt}{$\ulcorner$}{\mathpzc{s}_{1}\kappa^{-}}\raisebox{0.5887pt}{$\urcorner$}$
hence $\mathpzc{s}_{1}\kappa^{-}\kappa^{+}$ is a (negative) quasi-path. As
$\mathpzc{s}$ is a path and as
$\mathpzc{s}\in\kappa_{\bullet}(\mathpzc{s}_{1}\kappa^{-}\kappa^{+}\shuffle\mathpzc{s}_{2})$,
by Lemma 86 $\mathpzc{s}_{1}\kappa^{-}\kappa^{+}$ is a path. We already know
from previous item that $\mathpzc{s}_{1}\kappa^{-}\maltese\in
V_{{\mathbf{M}}}^{x}$. Notice that
$\kappa_{\bullet}\langle\mathpzc{s}_{1}\kappa^{-}\kappa^{+}\rangle=\langle\kappa^{+}\rangle_{\mathpzc{s}}=\langle\kappa^{+}\rangle_{\mathpzc{t}}=\kappa_{\bullet}\langle\kappa^{+}\rangle_{\mathpzc{t}_{1}}$.
Hence
$\langle\mathpzc{s}_{1}\kappa^{-}\kappa^{+}\rangle=\langle\kappa^{+}\rangle_{\mathpzc{t}_{1}}$
is a trivial view of ${\mathbf{M}}^{x}$. Let
${\mathbb{u}}\kappa^{+}=\langle\mathpzc{s}_{1}\kappa^{-}\kappa^{+}\rangle$. By
Lemma 74, $\mathpzc{s}_{1}\kappa^{-}\maltese$ is a shuffle of anti-shuffles of
trivial views of ${\mathbf{M}}^{x}$, one of which is the trivial view
${\mathbb{u}}\maltese$. Remark that $\mathpzc{s}_{1}\kappa^{-}\kappa^{+}$ is
also a shuffle of anti-shuffles of trivial views of ${\mathbf{M}}^{x}$,
replacing ${\mathbb{u}}\maltese$ by ${\mathbb{u}}\kappa^{+}$. By Proposition
75, $\mathpzc{s}_{1}\kappa^{-}\kappa^{+}\in V_{{\mathbf{M}}}^{x}$. Finally, as
$\mathpzc{s}\in\kappa_{\bullet}(\mathpzc{s}_{1}\kappa^{-}\kappa^{+}\shuffle\mathpzc{s}_{2})$
and by Proposition 82, we have $\mathpzc{s}\in V_{{\mathbf{M\otimes N}}}$.

  * •

Or $\kappa^{+}$ is a proper action of $\mathpzc{u}_{1}$, hence of
$\mathpzc{u}$. The reasoning is similar to previous item, using $\mathpzc{u}$
and $\mathpzc{u}_{1}$ instead of $\mathpzc{t}$ and $\mathpzc{t}_{1}$
respectively.

  * •

Or $\kappa^{+}$ is a proper action of $\mathpzc{t}_{2}$, hence of
$\mathpzc{t}$. This is impossible, being given the structure of $\mathpzc{s}$:
the action $\kappa_{0}^{+}$ following the negative action $\kappa^{-}$ in
$\mathpzc{t}$ is necessarily in $\mathpzc{t}_{1}$ (due to the structure of a
shuffle), hence the action following $\kappa^{-}$ in $\mathpzc{s}$ is
necessarily either $\kappa_{0}^{+}$ (hence in $\mathpzc{t}_{1}$) or in
$\mathpzc{u}$.

  * •

Or $\kappa^{+}$ is a proper action of $\mathpzc{u}_{2}$, hence of
$\mathpzc{u}$: this case also leads to a contradiction. We know from previous
item that a positive action of $\mathpzc{t}_{2}$ cannot immediately follow a
negative action of $\mathpzc{t}_{1}$ in $\mathpzc{s}$. Similarly, a positive
action of $\mathpzc{u}_{2}$ (resp. $\mathpzc{t}_{1}$, $\mathpzc{u}_{1}$)
cannot immediately follow a negative action of $\mathpzc{u}_{1}$ (resp.
$\mathpzc{t}_{2}$, $\mathpzc{u}_{2}$) in $\mathpzc{s}$. Suppose that there
exists a positive action $\kappa_{0}^{+}$ of $\mathpzc{u}_{2}$ (or resp.
$\mathpzc{t}_{2}$, $\mathpzc{u}_{1}$, $\mathpzc{t}_{1}$) which follows
immediately a negative action $\kappa_{0}^{-}$ of $\mathpzc{t}_{1}$ (or resp.
$\mathpzc{u}_{1}$, $\mathpzc{t}_{2}$, $\mathpzc{u}_{2}$). Let
$\mathpzc{s}_{0}\kappa_{0}^{-}\kappa_{0}^{+}$ be the shortest prefix of
$\mathpzc{s}$ satisfying such a property, say $\kappa_{0}^{+}$ is an action of
$\mathpzc{u}_{2}$ and $\kappa_{0}^{-}$ is an action of $\mathpzc{t}_{1}$. Then
the view
$\raisebox{0.5887pt}{$\ulcorner$}{\mathpzc{s}_{0}\kappa_{0}^{-}}\raisebox{0.5887pt}{$\urcorner$}$
is necessarily only made of $\kappa_{\bullet}$ and of actions from
$\mathpzc{t}_{1}$ or $\mathpzc{u}_{1}$, thus it does not contain
$\mathrm{just}(\kappa_{0}^{+})$ (where $\kappa_{0}^{+}$ cannot be initial
because ${\mathbf{N}}$ is negative), i.e., $\mathpzc{s}$ does not satisfy
P-visibility: contradiction.

∎

######  Corollary 88.

If ${\mathbf{N}}$ and ${\mathbf{P}}$ are regular, then
${\mathbf{N}}\multimap{\mathbf{P}}$ is regular.

###  B.4 Proofs of Propositions 19 and 21: Purity and Connectives

###### Proof (Proposition 19).

We must prove:

  * •

If ${\mathbf{N}}$ is pure then $\shpos{\mathbf{N}}$ is pure.

  * •

If ${\mathbf{P}}$ is pure then $\shneg{\mathbf{P}}$ is pure.

  * •

If ${\mathbf{M}}$ and ${\mathbf{N}}$ are pure then
${\mathbf{M}}\oplus{\mathbf{N}}$ is pure.

  * •

If ${\mathbf{M}}$ and ${\mathbf{N}}$ are pure then
${\mathbf{M}}\otimes{\mathbf{N}}$ is pure.

For the shifts and plus, the result is immediate given the form of visitable
paths of $\shpos{\mathbf{N}}$, $\shneg{\mathbf{P}}$ and
${\mathbf{M}}\oplus{\mathbf{N}}$ (Propositions 78 and 79). Let us prove the
result for the tensor.

Let $\mathpzc{s}=\mathpzc{s}^{\prime}\maltese\in
V_{{\mathbf{M}}\otimes{\mathbf{N}}}$. According to Proposition 80, either
$\mathpzc{s}=\maltese$ or there exist $\mathpzc{s}_{1}\in
V_{{\mathbf{M}}}^{x}$ and $\mathpzc{s}_{2}\in V_{{\mathbf{N}}}^{y}$ such that
$\mathpzc{s}\in\kappa_{\bullet}(\mathpzc{s}_{1}\shuffle\mathpzc{s}_{2})$. If
$\mathpzc{s}=\maltese$ then it is extensible with $\kappa_{\bullet}$, so
suppose
$\mathpzc{s}\in\kappa_{\bullet}(\mathpzc{s}_{1}\shuffle\mathpzc{s}_{2})$.
Without loss of generality, suppose
$\mathpzc{s}_{1}=\mathpzc{s}_{1}^{\prime}\maltese$. Since ${\mathbf{M}}$ is
pure, $\mathpzc{s}_{1}$ is extensible: there exists a proper positive action
$\kappa^{+}$ such that $\mathpzc{s}_{1}^{\prime}\kappa^{+}\in
V_{{\mathbf{M}}}^{x}$. Then, note that $\mathpzc{s}^{\prime}\kappa^{+}$ is a
path: indeed, since $\mathpzc{s}_{1}^{\prime}\kappa^{+}$ is a path, the
justification of $\kappa^{+}$ appears in
$\raisebox{0.9387pt}{$\ulcorner$}{\mathpzc{s}_{1}^{\prime}}\raisebox{0.9387pt}{$\urcorner$}=\raisebox{0.9387pt}{$\ulcorner$}{\mathpzc{s}^{\prime}}\raisebox{0.9387pt}{$\urcorner$}$.
Moreover
$\mathpzc{s}^{\prime}\kappa^{+}\in\kappa_{\bullet}(V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y})$, let us show that $\mathpzc{s}^{\prime}\kappa^{+}\in
V_{{\mathbf{M}}\otimes{\mathbf{N}}}$. Let $\mathpzc{t}\in
V_{{\mathbf{M}}}^{x}\shuffle V_{{\mathbf{N}}}^{y}$ and $\kappa^{-}$ a negative
action such that $\overline{\kappa_{\bullet}\mathpzc{t}\kappa^{-}}$ is a path
of
$\raisebox{1.01648pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[15.60158pt][c]{\mbox{\rule{0.0pt}{5.93887pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}\kappa^{+}}}$}}}\raisebox{1.01648pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$,
and by Proposition 80 it suffices to show that
$\mathpzc{t}\kappa^{-}\maltese\in V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y}$. But
$\raisebox{1.01648pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[15.60158pt][c]{\mbox{\rule{0.0pt}{5.93887pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}\kappa^{+}}}$}}}\raisebox{1.01648pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}=\raisebox{2.0pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\overline{\mathpzc{s}^{\prime}\kappa^{+}}\maltese}\raisebox{2.0pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}=\raisebox{0.75537pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\overline{\mathpzc{s}^{\prime}}}\raisebox{0.75537pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}=\raisebox{-0.61685pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}}\raisebox{-0.61685pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$,
therefore $\overline{\kappa_{\bullet}\mathpzc{t}\kappa^{-}}$ is a path of
$\raisebox{-0.61685pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}}\raisebox{-0.61685pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$.
Since $\mathpzc{s}\in V_{{\mathbf{M}}\otimes{\mathbf{N}}}$, by Proposition 80
we get $\mathpzc{t}\kappa^{-}\maltese\in V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y}$. Finally $\mathpzc{s}^{\prime}\kappa^{+}\in
V_{{\mathbf{M}}\otimes{\mathbf{N}}}$, hence $\mathpzc{s}$ is extensible. ∎

###### Proof (Proposition 21).

Since ${\mathbf{N}}$ and ${\mathbf{P}}$ are regular, $V_{{\mathbf{(N\multimap
P)^{\perp}}}}=\kappa_{\bullet}(V_{{\mathbf{N}}}^{x}\shuffle\makebox[11.86668pt][c]{\mbox{\rule{0.0pt}{8.03886pt}$\mathchoice{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}$}})\cup\\{\maltese\\}$
by Corollary 83. Let $\mathpzc{s}\in
V_{({{\mathbf{N}}\multimap{\mathbf{P}}})^{\perp}}$ and suppose
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
is $\maltese$-ended, i.e., $\mathpzc{s}$ is $\maltese$-free. We must show that
either $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
is extensible or $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
is not well-bracketed. The path $\mathpzc{s}$ is of the form
$\mathpzc{s}=\kappa_{\bullet}\mathpzc{s}^{\prime}$ and there exist
$\maltese$-free paths $\mathpzc{t}\in V_{{\mathbf{N}}}^{x}$ and
$\mathpzc{u}\in\makebox[11.86668pt][c]{\mbox{\rule{0.0pt}{8.03886pt}$\mathchoice{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}$}}$
such that $\mathpzc{s}^{\prime}\in\mathpzc{t}\shuffle\mathpzc{u}$. We are in
one of the following situations:

  * •

Either $\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}$}}\in
V_{{\mathbf{P}}}^{y}$ is not well-bracketed, hence neither is
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$.

  * •

Otherwise, since ${\mathbf{P}}$ is quasi-pure,
$\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}$}}=\overline{\mathpzc{u}}\maltese$
is extensible, i.e., there exists a proper positive action
$\kappa_{\mathpzc{u}}^{+}$ such that
$\overline{\mathpzc{u}}\kappa_{\mathpzc{u}}^{+}\in V_{{\mathbf{P}}}^{y}$. If
$\overline{\mathpzc{s}}\kappa_{\mathpzc{u}}^{+}$ is a path, then
$\overline{\mathpzc{s}}\kappa_{\mathpzc{u}}^{+}\in V_{{\mathbf{N\multimap
P}}}$, hence $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
is extensible: indeed,
$\makebox[13.87271pt][c]{\mbox{\rule{0.0pt}{5.93887pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{13.87271pt}{0.0pt}{$\sim$}$}\hss}{\overline{\mathpzc{s}}\kappa_{\mathpzc{u}}^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{13.87271pt}{0.0pt}{$\sim$}$}\hss}{\overline{\mathpzc{s}}\kappa_{\mathpzc{u}}^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{13.87271pt}{0.0pt}{$\sim$}$}\hss}{\overline{\mathpzc{s}}\kappa_{\mathpzc{u}}^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{13.87271pt}{0.0pt}{$\sim$}$}\hss}{\overline{\mathpzc{s}}\kappa_{\mathpzc{u}}^{+}}}$}}=\mathpzc{s}\overline{\kappa_{\mathpzc{u}}^{+}}\maltese\in\kappa_{\bullet}(\mathpzc{t}\shuffle\mathpzc{u}\overline{\kappa_{\mathpzc{u}}^{+}}\maltese)$,
thus
$\mathpzc{s}\overline{\kappa_{\mathpzc{u}}^{+}}\maltese\in\kappa_{\bullet}(V_{{\mathbf{N}}}^{x}\shuffle\makebox[11.86668pt][c]{\mbox{\rule{0.0pt}{8.03886pt}$\mathchoice{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{11.86668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P}}}^{y}}}$}})$.
In the case $\overline{\mathpzc{s}}\kappa_{\mathpzc{u}}^{+}$ is not a path,
this means that $\kappa_{\mathpzc{u}}^{+}$ is justified by an action
$\kappa_{\mathpzc{u}}^{-}$ that does not appear in
$\raisebox{0.75537pt}{$\ulcorner$}{\overline{\mathpzc{s}}}\raisebox{0.75537pt}{$\urcorner$}$,
thus we have something of the form:

$\overline{\mathpzc{s}}\kappa_{\mathpzc{u}}^{+}=\hskip 14.22636pt\dots\hskip
14.22636pt\kappa^{+}\hskip 14.22636pt\dots\hskip
14.22636pt\kappa_{\mathpzc{u}}^{-}\hskip 14.22636pt\dots\hskip
14.22636pt\kappa^{-}\hskip 14.22636pt\dots\hskip
14.22636pt\kappa_{\mathpzc{u}}^{+}$just.just.view
$\raisebox{1.01648pt}{$\ulcorner$}{\overline{\mathpzc{s}}\kappa_{\mathpzc{u}}^{+}}\raisebox{1.01648pt}{$\urcorner$}$

If $\kappa^{-}$ comes from $\overline{\mathpzc{t}}$, and thus also
$\kappa^{+}$, then $\overline{s}$ is not well-bracketed, indeed: since
$\kappa_{\mathpzc{u}}^{-}$ is hereditarily justified by
$\overline{\kappa_{\bullet}}$ and by no action from $\overline{\mathpzc{t}}$,
we have:

$\overline{\mathpzc{s}}=\hskip 14.22636pt\overline{\kappa_{\bullet}}\hskip
14.22636pt\dots\hskip 14.22636pt\kappa^{+}\hskip 14.22636pt\dots\hskip
14.22636pt\kappa_{\mathpzc{u}}^{-}\hskip 14.22636pt\dots\hskip
14.22636pt\kappa^{-}\hskip 14.22636pt\dots$just.just.

So suppose now that $\kappa^{-}$ comes from $\overline{\mathpzc{u}}$, thus
also $\kappa^{+}$. We know that
$\raisebox{0.75537pt}{$\ulcorner$}{\overline{\mathpzc{u}}}\raisebox{0.75537pt}{$\urcorner$}$
contains $\kappa_{\mathpzc{u}}^{-}=\mathrm{just}(\kappa_{\mathpzc{u}}^{+})$,
thus in particular
$\raisebox{0.75537pt}{$\ulcorner$}{\overline{\mathpzc{u}}}\raisebox{0.75537pt}{$\urcorner$}$
does not contain $\kappa^{-}$; on the contrary, we have seen that
$\raisebox{0.75537pt}{$\ulcorner$}{\overline{\mathpzc{s}}}\raisebox{0.75537pt}{$\urcorner$}$
contains $\kappa^{-}$. By definition of the view of a sequence, this
necessarily means that, in $\overline{\mathpzc{s}}$, between the action
$\kappa^{-}$ and the end of the sequence, the following happens:
$\raisebox{0.75537pt}{$\ulcorner$}{\overline{\mathpzc{s}}}\raisebox{0.75537pt}{$\urcorner$}$
comes across an action $\alpha_{\mathpzc{t}}^{-}$ from
$\overline{\mathpzc{t}}$, justified by an action $\alpha_{\mathpzc{t}}^{+}$
also from $\overline{\mathpzc{t}}$, making the view miss at least one action
$\alpha_{\mathpzc{u}}$ from $\overline{\mathpzc{u}}$ appearing in
$\raisebox{0.75537pt}{$\ulcorner$}{\overline{\mathpzc{u}}}\raisebox{0.75537pt}{$\urcorner$}$,
as depicted below.

$\overline{\mathpzc{s}}=\hskip 14.22636pt\overline{\kappa_{\bullet}}\hskip
14.22636pt\dots\hskip 14.22636pt\kappa^{-}\hskip 14.22636pt\dots\hskip
14.22636pt\alpha_{\mathpzc{t}}^{+}\hskip 14.22636pt\dots\hskip
14.22636pt\alpha_{\mathpzc{u}}\hskip 14.22636pt\dots\hskip
14.22636pt\alpha_{\mathpzc{t}}^{-}\hskip 14.22636pt\dots$just.view
$\raisebox{0.75537pt}{$\ulcorner$}{\overline{\mathpzc{s}}}\raisebox{0.75537pt}{$\urcorner$}$

Since $\alpha_{\mathpzc{u}}$ is hereditarily justified by
$\overline{\kappa_{\bullet}}$ and by no action from $\overline{\mathpzc{t}}$,
the path $\overline{\mathpzc{s}}$ is not well-bracketed: the justifications of
$\alpha_{\mathpzc{u}}$ and of $\alpha_{\mathpzc{t}}^{-}$ intersect.

To sum up, we have proved that in the case when
$\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}$}}=\overline{\mathpzc{u}}\maltese$
is extensible, either $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
is extensible too or it is not well-bracketed.

Hence ${\mathbf{N}}\multimap{\mathbf{P}}$ is quasi-pure. ∎

##  Appendix C Proofs of Section 4

In this section we prove:

  * •

that the functions $\phi^{A}_{\sigma}$ are Scott-continuous (Proposition 25),

  * •

internal completeness for particular infinite unions of behaviours (Theorem
30),

  * •

two lemmas of Subsection 4.3 (Lemmas 32 and 37).

###  C.1 Proof of Proposition 25

######  Lemma 89.

Let $E,F$ be sets of atomic negative designs and $G$ be a set of atomic
positive designs.

  1. 1.

$\shpos(E^{\perp\perp})=\blacktriangledown\langle E\rangle^{\perp\perp}$

  2. 2.

$\shneg(G^{\perp\perp})=\\{{\mathfrak{n}}\leavevmode\nobreak\
\boldsymbol{|}\leavevmode\nobreak\
\mathinner{\mathchoice{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\blacktriangle}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\blacktriangle}{{\mathfrak{n}}\mkern
1.0mu\upharpoonright\mkern
1.0mu\blacktriangle}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\blacktriangle}}\in\blacktriangle(x).G^{x}\\}^{\perp\perp}$

  3. 3.

$(E^{\perp\perp})\oplus(F^{\perp\perp})=(\iota_{1}\langle
E\rangle\cup\iota_{2}\langle F\rangle)^{\perp\perp}$

  4. 4.

$(E^{\perp\perp})\otimes(F^{\perp\perp})=\bullet\langle
E,F\rangle^{\perp\perp}$

###### Proof.

We prove (1) and (2), the other cases are very similar to (1).

  1. 1.

$\blacktriangledown\langle
E\rangle^{\perp\perp}=\\{{\mathfrak{n}}\leavevmode\nobreak\
\boldsymbol{|}\leavevmode\nobreak\
\mathinner{\mathchoice{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\blacktriangle}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\blacktriangle}{{\mathfrak{n}}\mkern
1.0mu\upharpoonright\mkern
1.0mu\blacktriangle}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\blacktriangle}}\in\blacktriangle(x).(E^{\perp})^{x}\\}^{\perp}=(\shneg(E^{\perp}))^{\perp}=(\shpos(E^{\perp\perp}))^{\perp\perp}=\shpos(E^{\perp\perp})$,

  2. 2.

$\\{{\mathfrak{n}}\leavevmode\nobreak\ \boldsymbol{|}\leavevmode\nobreak\
\mathinner{\mathchoice{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\blacktriangle}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\blacktriangle}{{\mathfrak{n}}\mkern
1.0mu\upharpoonright\mkern
1.0mu\blacktriangle}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\blacktriangle}}\in\blacktriangle(x).G^{x}\\}^{\perp\perp}=\\{\blacktriangledown\langle{\mathfrak{m}}\rangle\leavevmode\nobreak\
\boldsymbol{|}\leavevmode\nobreak\ {\mathfrak{m}}\in
G^{\perp}\\}^{\perp}=(\shpos(G^{\perp}))^{\perp}=\shneg(G^{\perp\perp})$,

using the definition of the orthogonal, internal completeness, and Lemma 77. ∎

###### Proof (Proposition 25).

By induction on $A$, we prove that for every $X$ and every $\sigma$ the
function $\phi^{A}_{\sigma}$ is continuous. Note that $\phi^{A}_{\sigma}$ is
continuous if and only if for every directed subset
$\mathbb{P}\subseteq\mathcal{B}^{+}$ we have
$\bigvee_{{\mathbf{P}}\in\mathbb{P}}(\llbracket
A\rrbracket^{\sigma,X\mapsto{\mathbf{P}}})=\llbracket
A\rrbracket^{\sigma,X\mapsto\bigvee\mathbb{P}}$. The cases $A=Y\in\mathcal{V}$
and $A=a\in\mathcal{S}$ are trivial, and the case $A=A_{1}\oplus^{+}A_{2}$ is
very similar to the tensor, hence we only treat the two remaining cases. Let
$\mathbb{P}\subseteq\mathcal{B}^{+}$ be directed.

  * •

Suppose $A=A_{1}\otimes^{+}A_{2}$, thus $\llbracket
A\rrbracket^{\sigma,X\mapsto{\mathbf{P}}}=\llbracket
A_{1}\rrbracket^{\sigma,X\mapsto{\mathbf{P}}}\otimes^{+}\llbracket
A_{2}\rrbracket^{\sigma,X\mapsto{\mathbf{P}}}$, with both functions
$\phi^{A_{i}}_{\sigma}:{\mathbf{P}}\mapsto\llbracket
A_{i}\rrbracket^{\sigma,X\mapsto{\mathbf{P}}}$ continuous by induction
hypothesis. For any positive behaviour ${\mathbf{P}}$, let us write
$\sigma_{{\mathbf{P}}}$ instead of $\sigma,X\mapsto{\mathbf{P}}$. We have

$\bigvee_{{\mathbf{P}}\in\mathbb{P}}\llbracket
A\rrbracket^{\sigma_{{\mathbf{P}}}}=(\bigcup_{{\mathbf{P}}\in\mathbb{P}}\llbracket
A\rrbracket^{\sigma_{{\mathbf{P}}}})^{\perp\perp}=(\bigcup_{{\mathbf{P}}\in\mathbb{P}}(\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}}}\otimes^{+}\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}}}))^{\perp\perp}$

Let us show that

$\bigcup_{{\mathbf{P}}\in\mathbb{P}}(\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}}}\otimes^{+}\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}}})=\bullet\langle\bigcup_{{\mathbf{P}}^{\prime}\in\mathbb{P}}\shneg\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime}}},\bigcup_{{\mathbf{P}}^{\prime\prime}\in\mathbb{P}}\shneg\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime\prime}}}\rangle\cup\\{\maltese\\}$

By internal completeness we have $\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}}}\otimes^{+}\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}}}=\bullet\langle\shneg\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}}},\shneg\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}}}\rangle\cup\\{\maltese\\}$ for every
${\mathbf{P}}\in\mathbb{P}$. The inclusion $(\subseteq)$ of (• ‣ C.1) is then
immediate, so let us prove $(\supseteq)$. First, indeed, $\maltese$ belongs to
the left side. Let
${\mathbf{P}}^{\prime},{\mathbf{P}}^{\prime\prime}\in\mathbb{P}$, let
${\mathfrak{m}}\in\shneg\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime}}}$,
${\mathfrak{n}}\in\shneg\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime\prime}}}$, and let us show that
$\bullet\langle{\mathfrak{m}},{\mathfrak{n}}\rangle\in\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}}}\otimes^{+}\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}}}$ where
${\mathbf{P}}={\mathbf{P}}^{\prime}\vee{\mathbf{P}}^{\prime\prime}$ (note that
${\mathbf{P}}\in\mathbb{P}$ since $\mathbb{P}$ is directed). By induction
hypothesis, $\phi^{A_{1}}_{\sigma}$ is continuous, thus in particular
increasing; since ${\mathbf{P}}^{\prime}\subseteq{\mathbf{P}}$, it follows
that $\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime}}}=\phi^{A_{1}}_{\sigma}({\mathbf{P}}^{\prime})\subseteq\phi^{A_{1}}_{\sigma}({\mathbf{P}})=\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}}}$. Similarly, $\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime\prime}}}\subseteq\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}}}$. We get
$\bullet\langle{\mathfrak{m}},{\mathfrak{n}}\rangle\in\bullet\langle\shneg\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}}},\shneg\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}}}\rangle\subseteq\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}}}\otimes^{+}\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}}}$, using internal completeness for
$\shneg$, which proves (• ‣ C.1). Using internal completeness, Lemma 89 and
induction hypothesis, we deduce

$\displaystyle(\bigcup_{{\mathbf{P}}\in\mathbb{P}}(\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}}}\otimes^{+}\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}}}))^{\perp\perp}$
$\displaystyle=\bullet\langle\bigcup_{{\mathbf{P}}^{\prime}\in\mathbb{P}}\shneg\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime}}},\bigcup_{{\mathbf{P}}^{\prime\prime}\in\mathbb{P}}\shneg\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime\prime}}}\rangle^{\perp\perp}$
$\displaystyle=(\bigcup_{{\mathbf{P}}^{\prime}\in\mathbb{P}}\shneg\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime}}})^{\perp\perp}\otimes(\bigcup_{{\mathbf{P}}^{\prime\prime}\in\mathbb{P}}\shneg\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime\prime}}})^{\perp\perp}$
$\displaystyle=(\bigcup_{{\mathbf{P}}^{\prime}\in\mathbb{P}}\llbracket
A_{1}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime}}})^{\perp\perp}\otimes^{+}(\bigcup_{{\mathbf{P}}^{\prime\prime}\in\mathbb{P}}\llbracket
A_{2}\rrbracket^{\sigma_{{\mathbf{P}}^{\prime\prime}}})^{\perp\perp}$
$\displaystyle=\llbracket{A_{1}}\rrbracket^{\sigma,X\mapsto\bigvee\mathbb{P}}\otimes^{+}\llbracket{A_{2}}\rrbracket^{\sigma,X\mapsto\bigvee\mathbb{P}}$
$\displaystyle=\llbracket A\rrbracket^{\sigma,X\mapsto\bigvee\mathbb{P}}$

Consequently $\phi^{A}_{\sigma}$ is continuous.

  * •

If $A=\mu Y.A_{0}$, define $f_{0}:{\mathbf{Q}}\mapsto\llbracket
A_{0}\rrbracket^{\sigma,X\mapsto\bigvee\mathbb{P},Y\mapsto{\mathbf{Q}}}$ and,
for every ${\mathbf{P}}\in\mathcal{B}^{+}$,
$f_{{\mathbf{P}}}:{\mathbf{Q}}\mapsto\llbracket
A_{0}\rrbracket^{\sigma,X\mapsto{\mathbf{P}},Y\mapsto{\mathbf{Q}}}$. Those
functions are continuous by induction hypothesis, thus using Kleene fixed
point theorem we have
$\mathrm{lfp}(f_{0})=\bigvee_{n\in\mathbb{N}}{f_{0}}^{n}(\maltese)\mbox{ and
}\mathrm{lfp}(f_{{\mathbf{P}}})=\bigvee_{n\in\mathbb{N}}{f_{{\mathbf{P}}}}^{n}(\maltese)$.
Therefore $\bigvee_{{\mathbf{P}}\in\mathbb{P}}(\llbracket
A\rrbracket^{\sigma,X\mapsto{\mathbf{P}}})=\bigvee_{{\mathbf{P}}\in\mathbb{P}}(\mathrm{lfp}(f_{{\mathbf{P}}}))=\bigvee_{{\mathbf{P}}\in\mathbb{P}}(\bigvee_{n\in\mathbb{N}}{f_{{\mathbf{P}}}}^{n}(\maltese))=\bigvee_{n\in\mathbb{N}}(\bigvee_{{\mathbf{P}}\in\mathbb{P}}{f_{{\mathbf{P}}}}^{n}(\maltese))$.

For every ${\mathbf{Q}}\in\mathcal{B}^{+}$ the function
$g_{{\mathbf{Q}}}:{\mathbf{P}}\mapsto f_{{\mathbf{P}}}({\mathbf{Q}})$ is
continuous by induction hypothesis, hence
$f_{0}({\mathbf{Q}})=\bigvee_{{\mathbf{P}}\in\mathbb{P}}f_{{\mathbf{P}}}({\mathbf{Q}})$.
From this, we prove easily by induction on $m$ that for every
${\mathbf{Q}}\in\mathcal{B}^{+}$ we have
${f_{0}}^{m}({\mathbf{Q}})=\bigvee_{{\mathbf{P}}\in\mathbb{P}}{f_{{\mathbf{P}}}}^{m}({\mathbf{Q}})$.
Thus $\bigvee_{{\mathbf{P}}\in\mathbb{P}}(\llbracket
A\rrbracket^{\sigma,X\mapsto{\mathbf{P}}})=\bigvee_{n\in\mathbb{N}}{f_{0}}^{n}(\maltese)=\mathrm{lfp}(f_{0})=\llbracket
A\rrbracket^{\sigma,X\mapsto\bigvee\mathbb{P}}$. We conclude that the function
$\phi^{A}_{\sigma}$ is continuous.

∎

###  C.2 Proof of Theorem 30

Before proving Theorem 30 we need some lemmas. Suppose
$({\mathbf{A}}_{n})_{n\in\mathbb{N}}$ is an infinite sequence of regular
behaviours such that for all $n\in\mathbb{N}$,
$|{\mathbf{A}}_{n}|\subseteq|{\mathbf{A}}_{n+1}|$; the simplicity hypothesis
is not needed for now. Let us note
${\mathbf{A}}=\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n}$. Notice that the
definition of visitable paths can harmlessly be extended to any set $E$ of
designs of same polarity, even if it is not a behaviour; the same applies to
the definition of incarnation, provided that $E$ satisfies the following: if
${\mathfrak{d}},{\mathfrak{e}}_{1},{\mathfrak{e}}_{2}\in E$ are cut-free
designs such that ${\mathfrak{e}}_{1}\sqsubseteq{\mathfrak{d}}$ and
${\mathfrak{e}}_{2}\sqsubseteq{\mathfrak{d}}$ then there exists
${\mathfrak{e}}\in E$ cut-free such that
${\mathfrak{e}}\sqsubseteq{\mathfrak{e}}_{1}$ and
${\mathfrak{e}}\sqsubseteq{\mathfrak{e}}_{2}$. In particular, as a union of
behaviours, ${\mathbf{A}}$ satisfies this condition.

######  Lemma 90.

  1. 1.

$\forall n\in\mathbb{N}$, $V_{{\mathbf{A}}_{n}}\subseteq
V_{{\mathbf{A}}_{n+1}}$.

  2. 2.

$V_{\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n}}=\bigcup_{n\in\mathbb{N}}V_{{\mathbf{A}}_{n}}$.

  3. 3.

$|\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n}|=\bigcup_{n\in\mathbb{N}}|{\mathbf{A}}_{n}|$.

###### Proof.

  1. 1.

Fix $n$ and let $\mathpzc{s}\in V_{A_{n}}$. There exist
${\mathfrak{d}}\in|{\mathbf{A}}_{n}|$ such that $\mathpzc{s}$ is a path of
${\mathfrak{d}}$. Since $|{\mathbf{A}}_{n}|\subseteq|{\mathbf{A}}_{n+1}|$ we
have ${\mathfrak{d}}\in|{\mathbf{A}}_{n+1}|$, thus by regularity of
${\mathbf{A}}_{n+1}$, $\mathpzc{s}\in V_{A_{n+1}}$.

  2. 2.

$(\subseteq)$ Let $\mathpzc{s}\in V_{{\mathbf{A}}}$. There exist
$n\in\mathbb{N}$ and ${\mathfrak{d}}\in|{\mathbf{A}}_{n}|$ such that
$\mathpzc{s}$ is a path of ${\mathfrak{d}}$. By regularity of
${\mathbf{A}}_{n}$ we have $\mathpzc{s}\in V_{{\mathbf{A}}_{n}}$.
$(\supseteq)$ Let $m\in\mathbb{N}$ and $\mathpzc{s}\in V_{{\mathbf{A}}_{m}}$.
For all $n\geq m$, $V_{{\mathbf{A}}_{m}}\subseteq V_{{\mathbf{A}}_{n}}$ by
previous item, thus $\mathpzc{s}\in V_{{\mathbf{A}}_{n}}$. Hence if we take
${\mathfrak{e}}=\raisebox{-0.61685pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}}\raisebox{-0.61685pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$,
we have ${\mathfrak{e}}\in{{\mathbf{A}}_{n}}^{\perp}$ for all $n\geq m$ by
monotonicity. We deduce ${\mathfrak{e}}\in\bigcap_{n\geq
m}{{\mathbf{A}}_{n}}^{\perp}=(\bigcup_{n\geq
m}{\mathbf{A}}_{n})^{\perp}=(\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n})^{\perp}={\mathbf{A}}^{\perp}$.
Let ${\mathfrak{d}}\in{\mathbf{A}}_{m}$ such that $\mathpzc{s}$ is a path of
${\mathfrak{d}}$; we have ${\mathfrak{d}}\in{\mathbf{A}}$ and
${\mathfrak{e}}\in{\mathbf{A}}^{\perp}$, thus
$\langle{\mathfrak{d}}\leftarrow{\mathfrak{e}}\rangle=\mathpzc{s}\in
V_{{\mathbf{A}}}$.

  3. 3.

$(\subseteq)$ Let ${\mathfrak{d}}$ be cut-free and minimal for $\sqsubseteq$
in ${\mathbf{A}}$. There exists $m\in\mathbb{N}$ such that
${\mathfrak{d}}\in{\mathbf{A}}_{m}$. Thus ${\mathfrak{d}}$ is minimal for
$\sqsubseteq$ in ${\mathbf{A}}_{m}$ otherwise it would not be minimal in
${\mathbf{A}}$, hence the result.
$(\supseteq)$ Let $m\in\mathbb{N}$, and let
${\mathfrak{d}}\in|{\mathbf{A}}_{m}|$. By hypothesis,
${\mathfrak{d}}\in|{\mathbf{A}}_{n}|$ for all $n\geq m$. Suppose
${\mathfrak{d}}$ is not in $|{\mathbf{A}}|$, so there exists
${\mathfrak{d}}^{\prime}\in{\mathbf{A}}$ such that
${\mathfrak{d}}^{\prime}\sqsubseteq{\mathfrak{d}}$ and
${\mathfrak{d}}^{\prime}\neq{\mathfrak{d}}$. In this case, there exists $n\geq
m$ such that ${\mathfrak{d}}^{\prime}\in{\mathbf{A}}_{n}$, but this
contradicts the fact that ${\mathfrak{d}}\in|{\mathbf{A}}_{n}|$.

∎

######  Lemma 91.

$V_{\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n}}=\makebox[31.96376pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{31.96376pt}{0.0pt}{$\sim$}$}\hss}{V_{(\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n})^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{31.96376pt}{0.0pt}{$\sim$}$}\hss}{V_{(\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n})^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{31.96376pt}{0.0pt}{$\sim$}$}\hss}{V_{(\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n})^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{31.96376pt}{0.0pt}{$\sim$}$}\hss}{V_{(\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n})^{\perp}}}}$}}=V_{(\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n})^{\perp\perp}}$.

###### Proof.

In this proof we use the alternative definition of regularity (Proposition
75). We prove
$V_{{\mathbf{A}}}=\makebox[14.65556pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A^{\perp}}}}}}$}}$,
and the result will follow from the fact that for any behaviour ${\mathbf{B}}$
(in particular if ${\mathbf{B}}={\mathbf{A}}^{\perp\perp}$) we have
$\makebox[14.42223pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.42223pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{B^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.42223pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{B^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.42223pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{B^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.42223pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{B^{\perp}}}}}}$}}=V_{{\mathbf{B}}}$.
First note that the inclusion
$V_{{\mathbf{A}}}\subseteq\makebox[14.65556pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A^{\perp}}}}}}$}}$
is immediate.

Let $\mathpzc{s}\in V_{{\mathbf{A^{\perp}}}}$ and let us show that
$\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}\in
V_{{\mathbf{A}}}$. Let ${\mathfrak{e}}\in|{\mathbf{A}}^{\perp}|$ such that
$\mathpzc{s}$ is a path of ${\mathfrak{e}}$. By Lemma 74 and the remark
following it, $\mathpzc{s}$ is in the shuffle of anti-shuffles of trivial
views ${\mathbb{t}}_{1},\dots,{\mathbb{t}}_{k}$ of ${\mathbf{A}}^{\perp}$. For
every $i\leq k$, suppose ${\mathbb{t}}_{i}=\langle\kappa_{i}\rangle$;
necessarily, there exists a design ${\mathfrak{d}}_{i}\in{\mathbf{A}}$ such
that $\kappa_{i}$ occurs in
$\langle{\mathfrak{e}}\leftarrow{\mathfrak{d}}_{i}\rangle$, i.e., such that
${\mathbb{t}}_{i}$ is a subsequence of
$\langle{\mathfrak{e}}\leftarrow{\mathfrak{d}}_{i}\rangle$, otherwise
${\mathfrak{e}}$ would not be in the incarnation of ${\mathbf{A}}^{\perp}$ (it
would not be minimal). Let $n$ be big enough such that
${\mathfrak{d}}_{1},\dots,{\mathfrak{d}}_{k}\in{\mathbf{A}}_{n}$, and note
that in particular ${\mathfrak{e}}\in{{\mathbf{A}}_{n}}^{\perp}$. For all $i$,
$\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{i}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{i}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{i}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{i}}}$
is a trivial view of $|{\mathfrak{d}}_{i}|_{{\mathbf{A}}_{n}}$, thus it is a
trivial view of ${\mathbf{A}}_{n}$. By regularity of ${\mathbf{A}}_{n}$ we
have $\makebox[9.42928pt][c]{\mbox{\rule{0.0pt}{7.0pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{i}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{i}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{i}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{i}}}$}}\in
V_{{\mathbf{A}}_{n}}$. Since $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
is in the anti-shuffle of shuffles of
$\makebox[10.3pt][c]{\mbox{\rule{0.0pt}{7.0pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{10.3pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{1}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{10.3pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{1}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{10.3pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{1}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{10.3pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{1}}}$}},\dots,\makebox[10.59166pt][c]{\mbox{\rule{0.0pt}{7.0pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{10.59166pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{k}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{10.59166pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{k}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{10.59166pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{k}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{10.59166pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}_{k}}}$}}$,
we have
$\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}\in
V_{{\mathbf{A}}_{n}}$ using regularity again. Therefore
$\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}\in
V_{{\mathbf{A}}}$ by Lemma 90. ∎

######  Lemma 92.

$(\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n})^{\perp}$ and
$(\bigcup_{n\in\mathbb{N}}{\mathbf{A}}_{n})^{\perp\perp}$ are regular.

###### Proof.

Let us show ${\mathbf{A}}^{\perp}$ is regular using the equivalent definition
(Proposition 75).

  * •

Let ${\mathbb{t}}$ be a trivial view of ${\mathbf{A}}^{\perp}$. By a similar
argument as in the proof above, there exists $n\in\mathbb{N}$ such that
$\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}}}$
is a trivial view of ${\mathbf{A}}_{n}$, thus
$\makebox[7.5pt][c]{\mbox{\rule{0.0pt}{7.0pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{t}}}}$}}\in
V_{{\mathbf{A}}_{n}}\subseteq V_{{\mathbf{A}}}$. By Lemma 91 ${\mathbb{t}}\in
V_{{\mathbf{A^{\perp}}}}$.

  * •

Let $\mathpzc{s},\mathpzc{t}\in V_{{\mathbf{A^{\perp}}}}$. By Lemma 91,
$\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}},\makebox[3.8889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}$}}\in
V_{{\mathbf{A}}}$. By Lemma 90(2), there exists $n\in\mathbb{N}$ such that
$\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}},\makebox[3.8889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}$}}\in
V_{{\mathbf{A}}_{n}}$, thus by regularity of ${\mathbf{A}}_{n}$ we have
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
$\shuffle$ $\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}$,
$\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}\shuffle\makebox[3.8889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}$}}\subseteq
V_{{\mathbf{A}}_{n}}\subseteq V_{{\mathbf{A}}}$, in other words
$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{15.33336pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\shuffle\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{15.33336pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\shuffle\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{15.33336pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\shuffle\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{15.33336pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\shuffle\mathpzc{t}}}$,
$\makebox[16.90277pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{16.90277pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{16.90277pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{16.90277pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{16.90277pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\mathpzc{t}}}$}}\subseteq
V_{{\mathbf{A}}}$. By Lemma 91 we deduce $\mathpzc{s}\shuffle\mathpzc{t}$,
$\mathpzc{s}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\mathpzc{t}\subseteq
V_{{\mathbf{A^{\perp}}}}$, hence $V_{{\mathbf{A^{\perp}}}}$ is stable under
shuffle and anti-shuffle.

Finally ${\mathbf{A}}^{\perp}$ is regular. We deduce that
${\mathbf{A}}^{\perp\perp}$ is regular since regularity is stable under
orthogonality. ∎

Let us introduce some more notions for next proof. An $\infty$-path (resp.
$\infty$-view) is a finite or infinite sequence of actions satisfying all the
conditions of the definition of path (resp. view) but the requirement of
finiteness. In particular, a finite $\infty$-path (resp. $\infty$-view) is a
path (resp. a view). An $\infty$-path (resp. $\infty$-view) of a design
${\mathfrak{d}}$ is such that any of its positive-ended prefix is a path
(resp. a view) of ${\mathfrak{d}}$. We call infinite chattering a closed
interaction which diverges because the computation never ends; note that
infinite chattering occurs in the interaction between two atomic designs
${\mathfrak{p}}$ and ${\mathfrak{n}}$ if and only if there exists an infinite
$\infty$-path $\mathpzc{s}$ of ${\mathfrak{p}}$ such that $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
is an $\infty$-path of ${\mathfrak{n}}$ (where, when $\mathpzc{s}$ is
infinite, $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
is obtained from $\mathpzc{s}$ by simply reversing the polarities of all the
actions). Given an infinite $\infty$-path $\mathpzc{s}$, the design
$\raisebox{-0.61685pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$
is constructed similarly to the case when $\mathpzc{s}$ is finite (see §
B.1.1).

For the proof of the theorem, suppose now that the behaviours
$({\mathbf{A}}_{n},)_{n\in\mathbb{N}}$ are simple. Remark that the second
condition of simplicity implies in particular that the dual of a path in a
design of a simple behaviour is a view.

###### Proof (Theorem 30).

We must show that ${\mathbf{A}}^{\perp\perp}\subseteq{\mathbf{A}}$ since the
other inclusion is trivial. Remark the following: given designs
${\mathfrak{d}}$ and ${\mathfrak{d}}^{\prime}$, if
${\mathfrak{d}}\in{\mathbf{A}}$ and
${\mathfrak{d}}\sqsubseteq{\mathfrak{d}}^{\prime}$ then
${\mathfrak{d}}^{\prime}\in{\mathbf{A}}$. Indeed, if
${\mathfrak{d}}\in{\mathbf{A}}$ then there exists $n\in\mathbb{N}$ such that
${\mathfrak{d}}\in{\mathbf{A}}_{n}$; if moreover
${\mathfrak{d}}\sqsubseteq{\mathfrak{d}}^{\prime}$ then in particular
${\mathfrak{d}}\preceq{\mathfrak{d}}^{\prime}$, and by monotonicity
${\mathfrak{d}}^{\prime}\in{\mathbf{A}}_{n}$, hence
${\mathfrak{d}}^{\prime}\in{\mathbf{A}}$. Thus it is sufficient to show
$|{\mathbf{A}}^{\perp\perp}|\subseteq{\mathbf{A}}$ since for every
${\mathfrak{d}}^{\prime}\in{\mathbf{A}}^{\perp\perp}$ we have
$|{\mathfrak{d}}^{\prime}|\in|{\mathbf{A}}^{\perp\perp}|$ and
$|{\mathfrak{d}}^{\prime}|\sqsubseteq{\mathfrak{d}}^{\prime}$.

So let ${\mathfrak{d}}\in|{\mathbf{A}}^{\perp\perp}|$ and suppose
${\mathfrak{d}}\notin{\mathbf{A}}$. First note the following: by Lemmas 91 and
92, every path $\mathpzc{s}$ of ${\mathfrak{d}}$ is in
$V_{{\mathbf{A^{\perp\perp}}}}=V_{{\mathbf{A}}}$, thus there exists
${\mathfrak{d}}^{\prime}\in|{\mathbf{A}}|$ containing $\mathpzc{s}$. We
explore separately the possible cases, and show how they all lead to a
contradiction.
If ${\mathfrak{d}}$ has an infinite number of maximal slices then:

  * •

Either there exists a negative subdesign
${\mathfrak{n}}=\sum_{a\in\mathcal{S}}a(\overrightarrow{x^{a}}).{\mathfrak{p}}_{a}$
of ${\mathfrak{d}}$ for which there is an infinity of names $a\in\mathcal{A}$
such that ${\mathfrak{p}}_{a}\neq\Omega$. In this case, let ${\mathbb{v}}$ be
the view of ${\mathfrak{d}}$ such that for every action $\kappa^{-}$ among the
first ones of ${\mathfrak{n}}$, ${\mathbb{v}}\kappa^{-}$ is the prefix of a
view of ${\mathfrak{d}}$. All such sequences ${\mathbb{v}}\kappa^{-}$ being
prefixes of paths of ${\mathfrak{d}}$, we deduce by regularity of
${\mathbf{A}}^{\perp\perp}$ and using Lemma 71 that
${\mathbb{v}}\kappa^{-}\maltese\in V_{{\mathbf{A^{\perp\perp}}}}$. Let
${\mathfrak{d}}^{\prime}\in|{\mathbf{A}}|$ be such that ${\mathbb{v}}$ is a
view of ${\mathfrak{d}}^{\prime}$. Since ${\mathfrak{d}}^{\prime}$ is also in
${\mathbf{A}}^{\perp\perp}$, we deduce by Lemma 72 that for every action
$\kappa^{-}$ among the first ones of ${\mathfrak{n}}$,
${\mathbb{v}}\kappa^{-}$ is the prefix of a view of ${\mathfrak{d}}^{\prime}$.
Thus ${\mathfrak{d}}^{\prime}$ has an infinite number of slices:
contradiction.

  * •

Or we can find an infinite $\infty$-view
${\mathbb{v}}=(\kappa^{-}_{0})\kappa^{+}_{1}\kappa^{-}_{1}\kappa^{+}_{2}\kappa^{-}_{1}\kappa^{+}_{3}\kappa^{-}_{3}\dots$
of ${\mathfrak{d}}$ (the first action $\kappa^{-}_{0}$ being optional
depending on the polarity of ${\mathfrak{d}}$) satisfying the following: there
is an infinity of $i\in\mathbb{N}$ such than $\kappa^{-}_{i}$ is one of the
first actions of a negative subdesign
$\sum_{a\in\mathcal{S}}a(\overrightarrow{x^{a}}).{\mathfrak{p}}_{a}$ of
${\mathfrak{d}}$ with at least two names $a\in\mathcal{A}$ such that
${\mathfrak{p}}_{a}\neq\Omega$. Let ${\mathbb{v}}_{i}$ be the prefix of
${\mathbb{v}}$ ending on $\kappa^{+}_{i}$. There is no design
${\mathfrak{d}}^{\prime}\in|{\mathbf{A}}|$ containing ${\mathbb{v}}$, indeed:
in this case, for all $i$ and all negative action $\kappa^{-}$ such that
${\mathbb{v}}_{i}\kappa^{-}$ is a prefix of a view of ${\mathfrak{d}}$,
${\mathbb{v}}_{i}\kappa^{-}$ would be a prefix of a view of
${\mathfrak{d}}^{\prime}$ by Lemma 72, thus ${\mathfrak{d}}^{\prime}$ would
have an infinite number of slices, which is impossible since the
${\mathbf{A}}_{n}$ are simple. Thus consider
${\mathfrak{e}}=\raisebox{2.0776pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[7.5pt][c]{\mbox{\rule{0.0pt}{7.0pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}}}$}}}\raisebox{2.0776pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$:
since all the ${\mathbb{v}}_{i}$ are views of designs in
$|{\mathbf{A}}|=\bigcup_{n\in\mathbb{N}}|{\mathbf{A}}_{n}|$ and since the
${\mathbf{A}}_{n}$ are simple, the sequences $\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}_{i}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}_{i}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}_{i}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{9.42928pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}_{i}}}$
are views, thus $\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{7.5pt}{0.0pt}{$\sim$}$}\hss}{{\mathbb{v}}}}$
is an $\infty$-view. Therefore an interaction between a design
${\mathfrak{d}}^{\prime}\in{\mathbf{A}}$ and ${\mathfrak{e}}$ necessarily
eventually converges by reaching a daimon of ${\mathfrak{e}}$, indeed:
infinite chattering is impossible since we cannot follow ${\mathbb{v}}$
forever, and interaction cannot fail after following a finite portion of
${\mathbb{v}}$ since those finite portions ${\mathbb{v}}_{i}$ are in
$V_{{\mathbf{A}}}$. Hence ${\mathfrak{e}}\in{\mathbf{A}}^{\perp}$. But
${\mathfrak{d}}\not\perp{\mathfrak{e}}$, because of infinite chattering
following ${\mathbb{v}}$. Contradiction.

If ${\mathfrak{d}}$ has a finite number of maximal slices
${\mathfrak{c}}_{1},\dots,{\mathfrak{c}}_{k}$ then for every $i\leq k$ there
exist an $\infty$-path $\mathpzc{s}_{i}$ that visits all the positive proper
actions of ${\mathfrak{c}}_{i}$. Indeed, any (either infinite or positive-
ended) sequence $\mathpzc{s}$ of proper actions in a slice
${\mathfrak{c}}\sqsubseteq{\mathfrak{d}}$, without repetition, such that
polarities alternate and the views of prefixes of $\mathpzc{s}$ are views of
${\mathfrak{c}}$, is an $\infty$-path:

  * •

(Linearity) is ensured by the fact that we are in only one slice,

  * •

(O-visibility) is satisfied since positive actions of ${\mathfrak{d}}$, thus
also of ${\mathfrak{c}}$, are justified by the immediate previous negative
action (a condition true in $|{\mathbf{A}}|$, thus also satisfied in
${\mathfrak{d}}$ because all its views are views of designs in
$|{\mathbf{A}}|$)

  * •

(P-visibility) is natively satisfied by the fact that $\mathpzc{s}$ is a
promenade in the tree representing a design.

For example, $\mathpzc{s}$ can travel in the slice ${\mathfrak{c}}$ as a
breadth-first search on couples of nodes $(\kappa^{-},\kappa^{+})$ such that
$\kappa^{+}$ is just above $\kappa^{-}$ in the tree, and $\kappa^{+}$ is
proper. Then 2 cases:

  * •

Either for all $i$, there exists $n_{i}\in\mathbb{N}$ and
${\mathfrak{d}}_{i}\in{\mathbf{A}}_{n_{i}}$ such that $\mathpzc{s}_{i}$ is an
$\infty$-path of ${\mathfrak{d}}_{i}$. Without loss of generality we can even
suppose that ${\mathfrak{c}}_{i}\sqsubseteq{\mathfrak{d}}_{i}$: if it is not
the case, replace some positive subdesigns (possibly $\Omega$) of
${\mathfrak{d}}_{i}$ by $\maltese$ until you obtain
${\mathfrak{d}}^{\prime}_{i}$ such that
${\mathfrak{c}}_{i}\sqsubseteq{\mathfrak{d}}^{\prime}_{i}$, and note that
indeed ${\mathfrak{d}}^{\prime}_{i}\in{\mathbf{A}}_{n_{i}}$ since
${\mathfrak{d}}_{i}\preceq{\mathfrak{d}}^{\prime}_{i}$. Let
$N=\mathrm{max}_{1\leq i\leq k}(n_{i})$. Since
${\mathfrak{d}}\not\in{\mathbf{A}}$, thus in particular
${\mathfrak{d}}\not\in{\mathbf{A}}_{N}$, there exists
${\mathfrak{e}}\in{\mathbf{A}}_{N}^{\perp}$ such that
${\mathfrak{d}}\not\perp{\mathfrak{e}}$. The reason of divergence cannot be
infinite chattering, otherwise there would exist an infinite $\infty$-path
$\mathpzc{t}$ in ${\mathfrak{d}}$ such that $\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{3.8889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}}}$
is in ${\mathfrak{e}}$, and $\mathpzc{t}$ is necessarily in a single slice of
${\mathfrak{d}}$ (say ${\mathfrak{c}}_{i}$) to ensure its linearity; but in
this case we would also have ${\mathfrak{d}}_{i}\not\perp{\mathfrak{e}}$ where
${\mathfrak{d}}_{i}\in{\mathbf{A}}_{N}$, impossible. Similarly, for all
(finite) path $\mathpzc{s}$ of ${\mathfrak{d}}$, there exists $i$ such that
$\mathpzc{s}$ is a path of ${\mathfrak{c}}_{i}$ thus of
${\mathfrak{d}}_{i}\in{\mathbf{A}}_{N}$; this ensures that interaction between
${\mathfrak{d}}$ and ${\mathfrak{e}}$ cannot diverge after a finite number of
steps either, leading to a contradiction.

  * •

Or there is an $i$ such that the (necessarily infinite) $\infty$-path
$\mathpzc{s}_{i}$ is in no design of ${\mathbf{A}}$. In this case, let
${\mathfrak{e}}=\raisebox{-0.61685pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.5pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.5pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}_{i}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.5pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}_{i}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.5pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}_{i}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.5pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}_{i}}}$}}}\raisebox{-0.61685pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$
(where $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.5pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}_{i}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.5pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}_{i}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.5pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}_{i}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.5pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}_{i}}}$
is a view since the ${\mathbf{A}}_{n}$ are simple), and with a similar
argument as previously we have ${\mathfrak{e}}\in{\mathbf{A}}^{\perp}$ but
${\mathfrak{d}}\not\perp{\mathfrak{e}}$ by infinite chattering, contradiction.

∎

###  C.3 Proofs of Subsection 4.3

###### Proof (Lemma 32).

By induction on $A$, we prove that for all $X\in\mathcal{V}$ and
$\sigma:\mathrm{FV}(A)\setminus\\{X\\}\to\mathcal{B}^{+}$ simple and regular,
the induction hypothesis consisting in all the following statements holds:

  1. 1.

for all simple regular behaviours
${\mathbf{P}},{\mathbf{P}}^{\prime}\in\mathcal{B}^{+}$, if
$|{\mathbf{P}}|\subseteq|{\mathbf{P}}^{\prime}|$ then
$|{\phi^{A}_{\sigma}}({\mathbf{P}})|\subseteq|{\phi^{A}_{\sigma}}({\mathbf{P}}^{\prime})|$;

  2. 2.

for all $n\in\mathbb{N}$,
$|(\phi^{A}_{\sigma})^{n}(\maltese)|\subseteq|(\phi^{A}_{\sigma})^{n+1}(\maltese)|$;

  3. 3.

for all simple regular behaviour ${\mathbf{P}}\in\mathcal{B}^{+}$,
${\phi^{A}_{\sigma}}({\mathbf{P}})$ is simple and regular;

  4. 4.

$\llbracket\mu
X.A\rrbracket^{\sigma}=\bigcup_{n\in\mathbb{N}}(\phi^{A}_{\sigma})^{n}(\maltese)$.

  5. 5.

$|\llbracket\mu
X.A\rrbracket^{\sigma}|=\bigcup_{n\in\mathbb{N}}|(\phi^{A}_{\sigma})^{n}(\maltese)|$.

Let us write $\sigma_{{\mathbf{P}}}$ for $\sigma,X\mapsto{\mathbf{P}}$. Note
that the base cases are immediate. If $A=A_{1}\oplus^{+}A_{2}$ or
$A=A_{1}\otimes^{+}A_{2}$ then:

  1. 1.

Follows from the incarnated form of internal completeness (in Theorem 8).

  2. 2.

Easy by induction on $n$, using previous item.

  3. 3.

Regularity of ${\phi^{A}_{\sigma}}({\mathbf{P}})$ comes from Proposition 18,
and simplicity is easy since the structure of the designs in $\llbracket
A\rrbracket^{\sigma_{{\mathbf{P}}}}$ is given by internal completeness.

  4. 4.

By Corollary 26 we have $\llbracket\mu
X.A\rrbracket^{\sigma}=(\bigcup_{n\in\mathbb{N}}(\phi^{A}_{\sigma})^{n}(\maltese))^{\perp\perp}$,
and by Theorem 30 we have
$(\bigcup_{n\in\mathbb{N}}(\phi^{A}_{\sigma})^{n}(\maltese))^{\perp\perp}=\bigcup_{n\in\mathbb{N}}(\phi^{A}_{\sigma})^{n}(\maltese)$
since items (2) and (3) guarantee that the hypotheses of the theorem are
satisfied.

  5. 5.

By previous item and Lemma 90(3).

If $A=\mu Y.A_{0}$ then:

  1. 1.

Suppose $|{\mathbf{P}}|\subseteq|{\mathbf{P}}^{\prime}|$, where ${\mathbf{P}}$
and ${\mathbf{P}}^{\prime}$ are simple regular. We have
$|{\phi^{A}_{\sigma}}({\mathbf{P}})|=|\llbracket\mu
Y.A_{0}\rrbracket^{\sigma_{{\mathbf{P}}}}|=\bigcup_{n\in\mathbb{N}}|(\phi^{A_{0}}_{\sigma_{{\mathbf{P}}}})^{n}(\maltese)|$
by induction hypothesis (5), and similarly for ${\mathbf{P}}^{\prime}$. By
induction on $n$, we prove that

$|(\phi^{A_{0}}_{\sigma_{{\mathbf{P}}}})^{n}(\maltese)|\subseteq|(\phi^{A_{0}}_{\sigma_{{\mathbf{P}}^{\prime}}})^{n}(\maltese)|$

It is immediate for $n=0$, and the inductive case is:

$\displaystyle|(\phi^{A_{0}}_{\sigma_{{\mathbf{P}}}})^{n+1}(\maltese)|$
$\displaystyle=|\phi^{A_{0}}_{\sigma_{{\mathbf{P}}}}((\phi^{A_{0}}_{\sigma_{{\mathbf{P}}}})^{n}(\maltese))|$
$\displaystyle\subseteq|\phi^{A_{0}}_{\sigma_{{\mathbf{P}}}}((\phi^{A_{0}}_{\sigma_{{\mathbf{P}}^{\prime}}})^{n}(\maltese))|$
by induction hypotheses (1), (3) and ($\delta$)
$\displaystyle=|\phi^{A_{0}}_{\sigma,Y\mapsto(\phi^{A_{0}}_{\sigma_{{\mathbf{P}}^{\prime}}})^{n}(\maltese)}({\mathbf{P}})|$
$\displaystyle\subseteq|\phi^{A_{0}}_{\sigma,Y\mapsto(\phi^{A_{0}}_{\sigma_{{\mathbf{P}}^{\prime}}})^{n}(\maltese)}({\mathbf{P}}^{\prime})|$
by induction hypotheses (1) and (3)
$\displaystyle=|(\phi^{A_{0}}_{\sigma_{{\mathbf{P}}^{\prime}}})^{n+1}(\maltese)|$

  2. 3.

By induction hypotheses (2), (3) and (4) respectively, we have

     * •

for all $n\in\mathbb{N}$,
$|(\phi^{A_{0}}_{\sigma})^{n}(\maltese)|\subseteq|(\phi^{A_{0}}_{\sigma})^{n+1}(\maltese)|$,

     * •

for all $n\in\mathbb{N}$, $(\phi^{A_{0}}_{\sigma})^{n}(\maltese)$ is simple
regular,

     * •

$\llbracket\mu
Y.A_{0}\rrbracket^{\sigma}=\bigcup_{n\in\mathbb{N}}(\phi^{A_{0}}_{\sigma})^{n}(\maltese)$.

Consequently, by Corollary 31, $\llbracket\mu Y.A_{0}\rrbracket^{\sigma}$ is
simple regular.

  3. 2.

4\. 5. Similar to the cases $A=A_{1}\oplus^{+}A_{2}$ and
$A=A_{1}\otimes^{+}A_{2}$.

∎

###### Proof (Lemma 37).

By induction on $A$:

  * •

If $A=a$ then it has basis $\llbracket a\rrbracket={\mathbf{C}}_{a}$.

  * •

If $A=A_{1}\oplus^{+}A_{2}$, without loss of generality suppose $A_{1}$ is
steady, with basis ${\mathbf{B}}_{1}$. Take
$\otimes_{1}\shneg{\mathbf{B}}_{1}$, as a basis for $A$, where the connective
$\otimes_{1}$ is defined like $\shpos$ with a different name of action:
$\otimes_{1}{\mathbf{N}}:=\iota_{1}\langle{\mathbf{N}}\rangle^{\perp\perp}$
and by internal completeness
$\otimes_{1}{\mathbf{N}}:=\iota_{1}\langle{\mathbf{N}}\rangle$.

  * •

If $A=A_{1}\otimes^{+}A_{2}$ then both $A_{1}$ and $A_{2}$ are steady, of
respective base ${\mathbf{B}}_{1}$ and ${\mathbf{B}}_{2}$. The behaviour
${\mathbf{B}}={\mathbf{B}}_{1}\otimes^{+}{\mathbf{B}}_{2}$ is a basis for $A$,
indeed: since ${\mathbf{B}}_{1}$ and ${\mathbf{B}}_{2}$ are regular,
Proposition 82 gives
$V_{{\mathbf{B}}_{1}\otimes^{+}{\mathbf{B}}_{2}}=\kappa_{\bullet}(V_{\shneg{\mathbf{B}}_{1}}^{x}\shuffle
V_{\shneg{\mathbf{B}}_{2}}^{y})\cup\\{\maltese\\}$ where, by Proposition 78,
$V_{\shneg{\mathbf{B}}_{i}}=\kappa_{\blacktriangle}V_{{\mathbf{B}}_{i}}^{x}\cup\\{\epsilon\\}$
for $i\in\\{1,2\\}$; from this, and using internal completeness, we deduce
that ${\mathbf{B}}$ satisfies all the conditions.

  * •

Suppose $A=\mu X.A_{0}$, where $A_{0}$ is steady and has a basis
${\mathbf{B}}_{0}$, let us show that ${\mathbf{B}}_{0}$ is also a basis for
$A$.

    * –

By Proposition 34, $\llbracket
A\rrbracket^{\sigma}=\bigcup_{n\in\mathbb{N}}(\phi^{A_{0}}_{\sigma})^{n}(\maltese)$,
and since ${\mathbf{B}}_{0}$ is a basis for $A_{0}$ we have
${\mathbf{B}}_{0}\subseteq\llbracket
A_{0}\rrbracket^{\sigma,X\to\maltese}=(\phi^{A_{0}}_{\sigma})(\maltese)$, so
indeed ${\mathbf{B}}_{0}\subseteq\llbracket A\rrbracket^{\sigma}$.

    * –

By induction hypothesis, we immediately have that for every path
$\mathpzc{s}\in V_{{\mathbf{B}}_{0}}$, there exists $\mathpzc{t}\in
V_{{\mathbf{B}}_{0}}^{max}$ $\maltese$-free extending $\mathpzc{s}$.

    * –

By Lemma 90(2) $V_{\llbracket
A\rrbracket^{\sigma}}=\\{\maltese\\}\cup\bigcup_{n\in\mathbb{N}}V_{(\phi^{A_{0}}_{\sigma})^{n+1}(\maltese)}=\\{\maltese\\}\cup\bigcup_{n\in\mathbb{N}}V_{\llbracket
A_{0}\rrbracket^{\sigma_{n}}}$ where
$\sigma_{n}=\sigma,X\mapsto(\phi^{A_{0}}_{\sigma})^{n}(\maltese)$ has a simple
regular image. By induction hypothesis, for all $n\in\mathbb{N}$,
$V_{{\mathbf{B}}}^{max}\subseteq V_{\llbracket
A_{0}\rrbracket^{\sigma_{n}}}^{max}$, therefore
$V_{{\mathbf{B}}}^{max}\subseteq V_{\llbracket A\rrbracket^{\sigma}}^{max}$.

∎

##  Appendix D Proof of Proposition 43

In this section, we prove Proposition 43, which requires first several lemmas.
Let us denote the set of functional behaviours by $\mathcal{F}$, and recall
that $\mathcal{D}$ stands for the set of data behaviours.

######  Lemma 93.

Let ${\mathbf{P}}\in\mathcal{D}$, and let ${\mathbf{Q}}$ be a pure regular
behaviour. The behaviour ${\mathbf{P}}\multimap^{+}{\mathbf{Q}}$ is pure.

###### Proof.

By Proposition 19 it suffices to show that
$(\shneg{\mathbf{P}})\multimap{\mathbf{Q}}$ is pure. Remark first that, by
construction of data behaviours, the following assertion is satisfied in views
(thus also in paths) of $\shneg{\mathbf{P}}$: every proper positive action is
justified by the negative action preceding it.

By regularity and Corollary 83, we have $V_{{\mathbf{(\shneg P)\multimap
Q}}}=\makebox[53.88661pt][c]{\mbox{\rule{0.0pt}{7.5pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{53.88661pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle\makebox[12.41112pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}$}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{53.88661pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle\makebox[12.41112pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}$}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{53.88661pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle\makebox[12.41112pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}$}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{53.88661pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle\makebox[12.41112pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}$}})}}$}}\cup\\{\epsilon\\}$.
Let $\mathpzc{s}\maltese\in V_{{\mathbf{(\shneg P)\multimap Q}}}$, and we will
prove that it is extensible. There exist $\mathpzc{t}_{1}\in
V_{{\mathbf{\shneg P}}}$ and $\mathpzc{t}_{2}\in V_{{\mathbf{Q}}}$ such that
$\makebox[12.2778pt][c]{\mbox{\rule{0.0pt}{6.9224pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}$}}=\overline{\mathpzc{s}}\in\kappa_{\bullet}(\mathpzc{t}_{1}\shuffle\makebox[6.6889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}$}})$.
In particular $\mathpzc{t}_{1}$ is $\maltese$-free and $\mathpzc{t}_{2}$ is
$\maltese$-ended, say $\mathpzc{t}_{2}=\mathpzc{t}_{2}^{\prime}\maltese$.
Since ${\mathbf{Q}}$ is pure, there exists $\kappa^{+}$ such that
$\mathpzc{t}_{2}^{\prime}\kappa^{+}\in V_{{\mathbf{Q}}}$. Let us show that
$\mathpzc{s}\kappa^{+}$ is a path, i.e., that if $\kappa^{+}$ is justified
then $\mathrm{just}(\kappa^{+})$ appears in
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\urcorner$}$,
by induction on the length of $\mathpzc{t}_{1}$:

  * •

If $\mathpzc{t}_{1}=\epsilon$ then
$\mathpzc{s}\kappa^{+}=\mathpzc{t}_{2}^{\prime}\kappa^{+}$ hence it is a path.

  * •

Suppose
$\mathpzc{t}_{1}=\mathpzc{t}_{1}^{\prime}\kappa_{p}^{-}\kappa_{p}^{+}$. Since
$\mathpzc{t}_{1}$ is $\maltese$-free, $\kappa_{p}^{+}$ is proper. Thus
$\mathpzc{s}$ is of the form
$\mathpzc{s}=\mathpzc{s}_{1}\overline{\kappa_{p}^{-}\kappa_{p}^{+}}\mathpzc{s}_{2}$,
and by induction hypothesis $\mathpzc{s}_{1}\mathpzc{s}_{2}\kappa^{+}$ is a
path, i.e., $\mathrm{just}(\kappa^{+})$ appears in
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}_{1}\mathpzc{s}_{2}}\raisebox{-0.61685pt}{$\urcorner$}$.

    * –

Either
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\urcorner$}=\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}_{1}\mathpzc{s}_{2}}\raisebox{-0.61685pt}{$\urcorner$}$
and indeed $\mathrm{just}(\kappa^{+})$ also appears in
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\urcorner$}$.

    * –

Or
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\urcorner$}$
is of the form
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\urcorner$}=\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}_{1}}\raisebox{-0.61685pt}{$\urcorner$}\overline{\kappa_{p}^{-}}\overline{\kappa_{p}^{+}}\mathpzc{s}^{\prime}_{2}$
since, by the remark at the beginning of this proof, $\kappa_{p}^{+}$ is
justified by $\kappa_{p}^{-}$. This means in particular that
$\mathpzc{s}^{\prime}_{2}$ start with the same positive action as
$\mathpzc{s}_{2}$, thus we have
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}_{1}\mathpzc{s}_{2}}\raisebox{-0.61685pt}{$\urcorner$}=\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}_{1}}\raisebox{-0.61685pt}{$\urcorner$}\mathpzc{s}^{\prime}_{2}$.
Since $\mathrm{just}(\kappa^{+})$ appears in
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}_{1}\mathpzc{s}_{2}}\raisebox{-0.61685pt}{$\urcorner$}$
and it is an action of $\mathpzc{s}_{1}$, it appears in
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}_{1}}\raisebox{-0.61685pt}{$\urcorner$}$
thus also in
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\urcorner$}$.

Therefore $\mathpzc{s}\kappa^{+}$ is a path. Since
$\mathpzc{s}\kappa^{+}\in\makebox[53.88661pt][c]{\mbox{\rule{0.0pt}{7.5pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{53.88661pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle\makebox[12.41112pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}$}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{53.88661pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle\makebox[12.41112pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}$}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{53.88661pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle\makebox[12.41112pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}$}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{53.88661pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle\makebox[12.41112pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.41112pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{Q}}}}}$}})}}$}}$
and the behaviours are regular, $\mathpzc{s}\kappa^{+}\in
V_{{\mathbf{P\multimap^{+}Q}}}$, thus $\mathpzc{s}\maltese$ is extensible. As
this is true for every $\maltese$-ended path in $V_{{\mathbf{(\shneg
P)\multimap Q}}}$, the behaviour $(\shneg{\mathbf{P}})\multimap{\mathbf{Q}}$
is pure, and so is ${\mathbf{P}}\multimap^{+}{\mathbf{Q}}$. ∎

######  Lemma 94.

If ${\mathbf{P}}\in\mathcal{F}$ and ${\mathbf{Q}}\in\mathrm{Const}$ then
${\mathbf{P}}\multimap^{+}{\mathbf{Q}}$ is pure.

###### Proof.

We prove that $(\shneg{\mathbf{P}})\multimap{\mathbf{Q}}$ is pure, and the
conclusion will follow from Proposition 19. Let
$\kappa^{+}=x_{0}|\overline{a}\langle\overrightarrow{y}\rangle$ where
${\mathbf{Q}}={\mathbf{C}}_{a}$, and let $\mathpzc{s}\maltese\in
V_{{\mathbf{(\shneg P)\multimap Q}}}$. As in the proof of Lemma 93, there
exist $\mathpzc{t}_{1}\in V_{{\mathbf{\shneg P}}}$ and $\mathpzc{t}_{2}\in
V_{{\mathbf{Q}}}$ such that
$\makebox[12.2778pt][c]{\mbox{\rule{0.0pt}{6.9224pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}$}}=\overline{\mathpzc{s}}\in\kappa_{\bullet}(\mathpzc{t}_{1}\shuffle\makebox[6.6889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}$}})$
with $\mathpzc{t}_{2}$ $\maltese$-ended. But
$V_{{\mathbf{Q}}}=\\{\maltese,\kappa^{+}\\}$, thus $\mathpzc{t}_{2}=\maltese$
and $\makebox[6.6889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}$}}=\epsilon$.
Hence
$\mathpzc{s}\maltese=\makebox[15.25049pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{15.25049pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}_{1}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{15.25049pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}_{1}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{15.25049pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}_{1}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{15.25049pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}_{1}}}$}}$,
and this path is extensible with action $\kappa^{+}$, indeed:
$\mathpzc{s}\kappa^{+}$ is a path because $\kappa^{+}$ is justified by
$\kappa_{\bullet}$, which is the only initial action of
$\mathpzc{s}\kappa^{+}$ thus appearing in
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\urcorner$}$;
moreover
$\makebox[14.06158pt][c]{\mbox{\rule{0.0pt}{5.93887pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{14.06158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{14.06158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{14.06158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{14.06158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\kappa^{+}}}$}}\in\kappa_{\bullet}(\mathpzc{t}_{1}\shuffle\makebox[10.11714pt][c]{\mbox{\rule{0.0pt}{5.93887pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{10.11714pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{10.11714pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{10.11714pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{10.11714pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}}}$}})$
where $\kappa^{+}\in V_{{\mathbf{Q}}}$, therefore $\mathpzc{s}\kappa^{+}\in
V_{{\mathbf{(\shneg P)\multimap Q}}}$. ∎

######  Lemma 95.

Let ${\mathbf{P}},{\mathbf{Q}}\in\mathcal{F}$. If there is $\mathpzc{s}\in
V_{{\mathbf{Q}}}$ $\maltese$-free (resp. $\maltese$-ended) and maximal, then
there is $\mathpzc{t}\in V_{{\mathbf{P\multimap^{+}Q}}}$ $\maltese$-free
(resp. $\maltese$-ended) and maximal.

###### Proof.

Suppose there exists $\mathpzc{s}\in V_{{\mathbf{Q}}}$ $\maltese$-free (resp.
$\maltese$-ended) and maximal. Since ${\mathbf{P}}$ is positive and different
from $\maltese$, there exists $\mathpzc{s}^{\prime}\in V_{{\mathbf{\shneg
P}}}$ $\maltese$-free and non-empty. Let
$\mathpzc{t}^{\prime}=\makebox[17.99046pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{17.99046pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{s}^{\prime}\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{17.99046pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{s}^{\prime}\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{17.99046pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{s}^{\prime}\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{17.99046pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{s}^{\prime}\makebox[3.94444pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$}}}}$}}$,
and remark that
$\mathpzc{t}^{\prime}=\overline{\kappa_{\bullet}\mathpzc{s}^{\prime}}\mathpzc{s}$.
This is a path (O- and P-visibility are satisfied), it belongs to
$V_{{\mathbf{(\shneg P)\multimap Q}}}$, it is $\maltese$-free (resp.
$\maltese$-ended). Suppose it is extensible, and consider both the
“$\maltese$-free” and the “$\maltese$-ended” cases:

  * •

if $\mathpzc{s}$ and $\mathpzc{t}^{\prime}$ are $\maltese$-free, then there
exists a negative action $\kappa^{-}$ such that
$\mathpzc{t}^{\prime}\kappa^{-}\maltese\in V_{{\mathbf{(\shneg P)\multimap
Q}}}$. But
$\mathpzc{t}^{\prime}\kappa^{-}\maltese=\overline{\kappa_{\bullet}\mathpzc{s}^{\prime}}\mathpzc{s}\kappa^{-}\maltese$,
and since it belongs to $V_{{\mathbf{(\shneg P)\multimap
Q}}}=\makebox[56.28662pt][c]{\mbox{\rule{0.0pt}{7.5pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{56.28662pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle V_{{\mathbf{Q^{\perp}}}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{56.28662pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle V_{{\mathbf{Q^{\perp}}}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{56.28662pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle V_{{\mathbf{Q^{\perp}}}})}}{\hbox
to0.0pt{\raisebox{7.5pt}{$\leavevmode\resizebox{56.28662pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}(V_{{\mathbf{\shneg
P}}}\shuffle V_{{\mathbf{Q^{\perp}}}})}}$}}\cup\\{\epsilon\\}$, we necessarily
have $\mathpzc{s}\kappa^{-}\maltese\in V_{{\mathbf{Q}}}$ – indeed, the
sequence $\overline{\mathpzc{s}^{\prime}}\kappa^{-}$ has two adjacent negative
actions. This contradicts the maximality of $\mathpzc{s}$ in
$V_{{\mathbf{Q}}}$.

  * •

if $\mathpzc{s}$ and $\mathpzc{t}^{\prime}$ are $\maltese$-ended, there exists
a positive action $\kappa^{+}$ that extends $\mathpzc{t}^{\prime}$ and a
contradiction arises with a similar reasoning.

Hence $\mathpzc{t}^{\prime}$ is maximal in $V_{{\mathbf{(\shneg P)\multimap
Q}}}$. Finally, $\mathpzc{t}=\kappa_{\blacktriangledown}\mathpzc{t}^{\prime}$
fulfills the requirements.∎

######  Lemma 96.

For every behaviour ${\mathbf{P}}\in\mathcal{F}$, there exists $\mathpzc{s}\in
V_{{\mathbf{P}}}$ maximal and $\maltese$-free.

###### Proof.

By induction on ${\mathbf{P}}$. If ${\mathbf{P}}\in\mathcal{D}$ then take
$\mathpzc{s}\in V_{{\mathbf{B}}}$ maximal, where ${\mathbf{B}}$ is a base of
${\mathbf{P}}$. Use Lemma 95 in the case of $\multimap^{+}$, and the result is
easy for $\otimes^{+}$ and $\oplus^{+}$. ∎

######  Lemma 97.

Let ${\mathbf{P}}\in\mathcal{F}$ and let $\mathcal{C}$ be a context. If
$\mathcal{C}[{\mathbf{P}}]$ pure then ${\mathbf{P}}$ pure.

###### Proof.

We prove the contrapositive by induction on $\mathcal{C}$. Suppose
${\mathbf{P}}$ is impure.

  * •

If $\mathcal{C}=[\leavevmode\nobreak\ ]$ then
$\mathcal{C}[{\mathbf{P}}]={\mathbf{P}}$, thus $\mathcal{C}[{\mathbf{P}}]$ is
impure.

  * •

If $\mathcal{C}=\mathcal{C}^{\prime}\oplus^{+}{\mathbf{Q}}$ or
${\mathbf{Q}}\oplus^{+}\mathcal{C}^{\prime}$ and by induction hypothesis
$\mathcal{C}^{\prime}[{\mathbf{P}}]$ is impure, i.e., there exists a maximal
path $\mathpzc{s}\maltese\in V_{{\mathbf{\mathcal{C}^{\prime}[P]}}}$, then one
of $\kappa_{\iota_{1}}\kappa_{\blacktriangle}\mathpzc{s}\maltese$ or
$\kappa_{\iota_{2}}\kappa_{\blacktriangle}\mathpzc{s}\maltese$ is maximal in
$V_{{\mathbf{\mathcal{C}[P]}}}$, hence the result.

  * •

If $\mathcal{C}=\mathcal{C}^{\prime}\otimes^{+}{\mathbf{Q}}$ or
${\mathbf{Q}}\otimes^{+}\mathcal{C}^{\prime}$ and by induction hypothesis
there exists a maximal path $\mathpzc{s}\maltese\in
V_{{\mathbf{\mathcal{C}^{\prime}[P]}}}$, then by Lemma 96, there exists a
$\maltese$-free maximal path $\mathpzc{t}\in V_{{\mathbf{Q}}}$. Consider the
path
$\mathpzc{u}=\kappa_{\bullet}\kappa_{\blacktriangle}^{\mathpzc{t}}\mathpzc{t}\kappa_{\blacktriangle}^{\mathpzc{s}}\mathpzc{s}\maltese$,
where:

    * –

$\kappa_{\blacktriangle}^{\mathpzc{t}}$ justifies the first action of
$\mathpzc{t}$,

    * –

$\kappa_{\blacktriangle}^{\mathpzc{s}}$ justifies the first one of
$\mathpzc{s}$, and

    * –

$\kappa_{\bullet}$ justifies $\kappa_{\blacktriangle}^{\mathpzc{t}}$ and
$\kappa_{\blacktriangle}^{\mathpzc{s}}$, one on each (1st or 2nd) position,
depending on the form of $\mathcal{C}$.

We have $\mathpzc{u}\in V_{{\mathbf{\mathcal{C}[{\mathbf{P}}]}}}$, and
$\mathpzc{u}$ is $\maltese$-ended and maximal, hence the result.

  * •

If $\mathcal{C}={\mathbf{Q}}\multimap^{+}\mathcal{C}^{\prime}$ and by
induction hypothesis $\mathcal{C}^{\prime}[{\mathbf{P}}]$ is impure, then
Lemma 95 (in its “$\maltese$-ended” version) concludes the proof.

∎

###### Proof (Proposition 43).

$(\Rightarrow)$ Suppose ${\mathbf{P}}$ impure. By induction on behaviour
${\mathbf{P}}$:

  * •

${\mathbf{P}}\in\mathcal{D}$ impossible by Corollary 40.

  * •

If ${\mathbf{P}}={\mathbf{P}}_{1}\oplus^{+}{\mathbf{P}}_{2}$ (resp.
${\mathbf{P}}={\mathbf{P}}_{1}\otimes^{+}{\mathbf{P}}_{2}$) then one of
${\mathbf{P}}_{1}$ or ${\mathbf{P}}_{2}$ is impure by Proposition 19, say
${\mathbf{P}}_{1}$. By induction hypothesis, ${\mathbf{P}}_{1}$ is of the form
${\mathbf{P}}_{1}=\mathcal{C}^{\prime}_{1}[\leavevmode\nobreak\
\mathcal{C}^{\prime}_{2}[{\mathbf{Q}}_{1}\multimap^{+}{\mathbf{Q}}_{2}]\multimap^{+}{\mathbf{R}}\leavevmode\nobreak\
]$. Let $\mathcal{C}_{1}=\mathcal{C}^{\prime}_{1}\oplus^{+}{\mathbf{P}}_{2}$
(resp. $\mathcal{C}_{1}=\mathcal{C}^{\prime}_{1}\otimes^{+}{\mathbf{P}}_{2}$)
and $\mathcal{C}_{2}=\mathcal{C}^{\prime}_{2}$, in order to get the result for
${\mathbf{P}}$.

  * •

If ${\mathbf{P}}={\mathbf{P}}_{1}\multimap^{+}{\mathbf{P}}_{2}$, then
${\mathbf{P}}_{2}\not\in\mathrm{Const}$ by Lemma 94, and:

    * –

If ${\mathbf{P}}_{2}$ impure, then by induction hypothesis ${\mathbf{P}}_{2}$
is of the form ${\mathbf{P}}_{2}=\mathcal{C}^{\prime}_{1}[\leavevmode\nobreak\
\mathcal{C}^{\prime}_{2}[{\mathbf{Q}}_{1}\multimap^{+}{\mathbf{Q}}_{2}]\multimap^{+}{\mathbf{R}}\leavevmode\nobreak\
]$, and it suffices to take
$\mathcal{C}_{1}={\mathbf{P}}_{1}\to\mathcal{C}^{\prime}_{1}$ and
$\mathcal{C}_{2}=\mathcal{C}^{\prime}_{2}$ to get the result for
${\mathbf{P}}$.

    * –

If ${\mathbf{P}}_{2}$ is pure, since it is also regular the conclusion follows
from Lemma 93.

$(\Leftarrow)$ Let $\mathcal{C}_{1},\mathcal{C}_{2}$ be contexts,
${\mathbf{Q}}_{1},{\mathbf{Q}}_{2},{\mathbf{R}}\in\mathcal{P}$ with
${\mathbf{R}}\not\in\mathrm{Const}$. Let
${\mathbf{P}}=\mathcal{C}_{1}[\leavevmode\nobreak\
\mathcal{C}_{2}[{\mathbf{Q}}_{1}\multimap^{+}{\mathbf{Q}}_{2}]\multimap^{+}{\mathbf{R}}\leavevmode\nobreak\
]$ and
${\mathbf{Q}}=\mathcal{C}_{2}[{\mathbf{Q}}_{1}\multimap^{+}{\mathbf{Q}}_{2}]$.
We prove that ${\mathbf{P}}$ is impure.

First suppose that
${\mathbf{P}}=\mathcal{C}_{2}[{\mathbf{Q}}_{1}\multimap^{+}{\mathbf{Q}}_{2}]\multimap^{+}{\mathbf{R}}$,
and in this case we show the result by induction on the depth of context
$\mathcal{C}_{2}$. The exact induction hypothesis will be: there exists a
maximal $\maltese$-ended path in $V_{{\mathbf{P}}}$ of the form
$\kappa_{\blacktriangledown}\mathpzc{s}\maltese$ where
$\overline{\mathpzc{s}}\in\kappa_{\bullet}((\kappa_{\blacktriangle}V_{{\mathbf{Q}}})\shuffle\makebox[12.17778pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.17778pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{R}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.17778pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{R}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.17778pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{R}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.17778pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{R}}}}}$}})$.

  * •

If $\mathcal{C}_{2}=[\leavevmode\nobreak\ ]$, then
${\mathbf{Q}}={\mathbf{Q}}_{1}\multimap^{+}{\mathbf{Q}}_{2}=\shpos(\shneg{\mathbf{Q}}_{1}\multimap{\mathbf{Q}}_{2})$
and
${\mathbf{P}}={\mathbf{Q}}\multimap^{+}{\mathbf{R}}=\shpos(\shneg{\mathbf{Q}}\multimap{\mathbf{R}})$.
In order to differentiate actions
$\kappa_{\blacktriangledown},\kappa_{\blacktriangle},\kappa_{\bullet}$ used to
construct ${\mathbf{Q}}$ from those to construct ${\mathbf{P}}$, we will use
corresponding superscripts. Let $\kappa^{Q}_{\blacktriangle}\mathpzc{t}_{1}\in
V_{{\mathbf{\shneg Q_{1}}}}$ be $\maltese$-free (and non-empty). Let
$\mathpzc{t}_{2}\in V_{{\mathbf{Q}}_{2}}$ be a maximal $\maltese$-free path:
its existence is ensured by Lemma 96, and it has one proper positive initial
action $\kappa_{2}^{+}$. Now let
$\mathpzc{t}=\makebox[33.75516pt][c]{\mbox{\rule{0.0pt}{6.21887pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.21887pt}{$\leavevmode\resizebox{33.75516pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{Q}_{\bullet}\kappa^{Q}_{\blacktriangle}\mathpzc{t}_{1}\makebox[6.6889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}$}}}}{\hbox
to0.0pt{\raisebox{6.21887pt}{$\leavevmode\resizebox{33.75516pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{Q}_{\bullet}\kappa^{Q}_{\blacktriangle}\mathpzc{t}_{1}\makebox[6.6889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}$}}}}{\hbox
to0.0pt{\raisebox{6.21887pt}{$\leavevmode\resizebox{33.75516pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{Q}_{\bullet}\kappa^{Q}_{\blacktriangle}\mathpzc{t}_{1}\makebox[6.6889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}$}}}}{\hbox
to0.0pt{\raisebox{6.21887pt}{$\leavevmode\resizebox{33.75516pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{Q}_{\bullet}\kappa^{Q}_{\blacktriangle}\mathpzc{t}_{1}\makebox[6.6889pt][c]{\mbox{\rule{0.0pt}{6.15079pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}{\hbox
to0.0pt{\raisebox{6.15079pt}{$\leavevmode\resizebox{6.6889pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}_{2}}}$}}}}$}}=\overline{\kappa^{Q}_{\bullet}\kappa^{Q}_{\blacktriangle}\mathpzc{t}_{1}}\mathpzc{t}_{2}$.
Similarly to the path constructed in proof of Lemma 95, we have that
$\mathpzc{t}$ is $\maltese$-free, it is in $V_{{\mathbf{(\shneg
Q_{1})\multimap Q_{2}}}}$, and it is maximal. Thus
$\kappa^{Q}_{\blacktriangledown}\mathpzc{t}\in V_{{\mathbf{Q}}}$. Since
${\mathbf{R}}\notin\mathrm{Const}$, there exists a path of the form
$\kappa^{+}\kappa^{-}\maltese\in V_{{\mathbf{R}}}$, and thus necessarily
$\kappa^{+}$ justifies $\kappa^{-}$. Define the sequence:

$\mathpzc{s}\maltese=\overline{\kappa^{P}_{\bullet}\kappa^{P}_{\blacktriangle}\kappa^{Q}_{\blacktriangledown}}\kappa^{Q}_{\bullet}\kappa^{Q}_{\blacktriangle}\kappa^{+}\kappa^{-}\mathpzc{t}_{1}\overline{\mathpzc{t}_{2}}\maltese$

and notice the following facts:

    1. 1.

$\mathpzc{s}\maltese$ is a path: it is a linear aj-sequence. Since
$\kappa^{-}$ is justified by $\kappa^{+}$, O- and P-visibility are easy to
check.

    2. 2.

$\mathpzc{s}\maltese\in V_{\shneg{\mathbf{Q}}\multimap{\mathbf{R}}}$: indeed,
we have $\makebox[12.2778pt][c]{\mbox{\rule{0.0pt}{6.9224pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}$}}\in\kappa^{P}_{\bullet}(\kappa^{P}_{\blacktriangle}\kappa^{Q}_{\blacktriangledown}\mathpzc{t}\shuffle\makebox[26.07875pt][c]{\mbox{\rule{0.0pt}{6.9224pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{26.07875pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}\kappa^{-}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{26.07875pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}\kappa^{-}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{26.07875pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}\kappa^{-}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{26.07875pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}\kappa^{-}\maltese}}$}})$
where
$\kappa^{P}_{\blacktriangle}\kappa^{Q}_{\blacktriangledown}\mathpzc{t}\in
V_{{\mathbf{\shneg Q}}}$ and $\kappa^{+}\kappa^{-}\maltese\in
V_{{\mathbf{R}}}$.

    3. 3.

$\mathpzc{s}\maltese$ is maximal: Let us show that $\mathpzc{s}\maltese$ is
not extensible. First, it is not possible to extend it with an action from
${\mathbf{Q}}^{\perp}$, because this would contradict the maximality of
$\mathpzc{t}$ in $V_{{\mathbf{Q}}}$. Suppose it is extensible with an action
$\kappa^{+\prime}$ from ${\mathbf{R}}$, that is
$\mathpzc{s}\kappa^{+\prime}\in V_{{\mathbf{\shneg Q\multimap R}}}$ and
$\makebox[15.60158pt][c]{\mbox{\rule{0.0pt}{5.93887pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\kappa^{+\prime}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\kappa^{+\prime}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\kappa^{+\prime}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{15.60158pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\kappa^{+\prime}}}$}}\in\kappa^{P}_{\bullet}(\kappa^{P}_{\blacktriangle}\kappa^{Q}_{\blacktriangledown}\mathpzc{t}\shuffle\makebox[29.40253pt][c]{\mbox{\rule{0.0pt}{5.93887pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{29.40253pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}\kappa^{-}\kappa^{+\prime}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{29.40253pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}\kappa^{-}\kappa^{+\prime}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{29.40253pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}\kappa^{-}\kappa^{+\prime}}}{\hbox
to0.0pt{\raisebox{5.93887pt}{$\leavevmode\resizebox{29.40253pt}{0.0pt}{$\sim$}$}\hss}{\kappa^{+}\kappa^{-}\kappa^{+\prime}}}$}})$
where $\kappa^{+}\kappa^{-}\kappa^{+\prime}\in V_{{\mathbf{R}}}$. The action
$\kappa^{+\prime}$ (that cannot be initial) is necessarily justified by
$\kappa^{-}$. But
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\urcorner$}$
contains necessarily the first negative action of
$\overline{\mathpzc{t}_{2}}$, which is the only initial action in
$\overline{\mathpzc{t}_{2}}$, and this action is justified by
$\kappa^{Q}_{\bullet}$ in $\mathpzc{s}$. Therefore
$\raisebox{-0.61685pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{-0.61685pt}{$\urcorner$}$
does not contain any action from $\mathpzc{s}$ between $\kappa^{Q}_{\bullet}$
and $\overline{\mathpzc{t}_{2}}$, in particular it does not contain
$\kappa^{-}=\mathrm{just}(\kappa^{+\prime})$. Thus
$\mathpzc{s}\kappa^{+\prime}$ is not P-visible: contradiction. Hence
$\mathpzc{s}\maltese$ maximal.

Finally $\kappa^{P}_{\blacktriangledown}\mathpzc{s}\maltese\in
V_{{\mathbf{P}}}$ is not extensible, and of the required form.

  * •

If $\mathcal{C}_{2}={\mathbf{Q}}_{0}\multimap^{+}\mathcal{C}$, then
${\mathbf{Q}}$ is of the form
${\mathbf{Q}}={\mathbf{Q}}_{0}\multimap^{+}{\mathbf{Q}}^{\prime}$, thus
previous reasoning applies.

  * •

If $\mathcal{C}_{2}=\mathcal{C}\otimes^{+}{\mathbf{Q}}_{0}$ or
${\mathbf{Q}}_{0}\otimes^{+}\mathcal{C}$, the induction hypothesis gives us
the existence of a maximal path in
$V_{{\mathbf{\mathcal{C}[Q_{1}\multimap^{+}Q_{2}]\multimap^{+}R}}}$ of the
form
$\kappa^{P}_{\blacktriangledown}\overline{\kappa^{P}_{\bullet}\kappa^{P}_{\blacktriangle}}\mathpzc{s}^{\prime}\maltese$
where
$\kappa^{P}_{\blacktriangle}\overline{\mathpzc{s}^{\prime}}\in(\kappa^{P}_{\blacktriangle}\mathpzc{t}^{\prime})\shuffle\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}$}}$
with $\mathpzc{t}^{\prime}\in
V_{{\mathbf{\mathcal{C}[Q_{1}\multimap^{+}Q_{2}]}}}$ and $\mathpzc{u}\in
V_{{\mathbf{R}}}$. Let $\mathpzc{t}_{0}\in V_{{\mathbf{Q_{0}}}}$ be
$\maltese$-free and maximal, using Lemma 96. Consider the following sequence:

$\mathpzc{s}\maltese=\overline{\kappa^{P}_{\bullet}\kappa^{P}_{\blacktriangle}\kappa^{Q}_{\bullet}\kappa^{0}_{\blacktriangle}\mathpzc{t}_{0}\kappa^{1}_{\blacktriangle}}\mathpzc{s}^{\prime}\maltese$

where:

    * –

$\kappa_{\blacktriangle}^{0}$ justifies the first action of $\mathpzc{t}_{0}$,

    * –

$\kappa_{\blacktriangle}^{1}$ justifies the first action of
$\overline{\mathpzc{s}^{\prime}}$ thus the first action of
$\mathpzc{t}^{\prime}$,

    * –

$\kappa^{Q}_{\bullet}$ justifies $\kappa_{\blacktriangle}^{0}$ and
$\kappa_{\blacktriangle}^{1}$,

    * –

$\kappa_{\blacktriangle}^{P}$ now justifies $\kappa^{Q}_{\bullet}$,

    * –

$\kappa_{\bullet}^{P}$ justifies the same actions as before.

Notice that:

    1. 1.

$\mathpzc{s}\maltese$ is a path: O- and P-visibility are satisfied.

    2. 2.

$\mathpzc{s}\maltese\in V_{\shneg{\mathbf{Q}}\multimap{\mathbf{R}}}$: We have
$\kappa^{Q}_{\bullet}\kappa^{0}_{\blacktriangle}\mathpzc{t}_{0}\kappa^{1}_{\blacktriangle}\overline{\mathpzc{t}^{\prime}}\in\kappa^{Q}_{\bullet}(\kappa^{0}_{\blacktriangle}V_{{\mathbf{{\mathbf{Q}}_{0}}}}\shuffle\kappa^{1}_{\blacktriangle}V_{{\mathbf{\mathcal{C}[Q_{1}\multimap^{+}Q_{2}]}}})=V_{{\mathbf{Q}}}$,
hence $\makebox[12.2778pt][c]{\mbox{\rule{0.0pt}{6.9224pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}{\hbox
to0.0pt{\raisebox{6.9224pt}{$\leavevmode\resizebox{12.2778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}\maltese}}$}}\in\kappa^{P}_{\bullet}(V_{{\mathbf{\shneg
Q}}}\shuffle\makebox[12.17778pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.17778pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{R}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.17778pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{R}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.17778pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{R}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.17778pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{R}}}}}$}})$.

    3. 3.

$\mathpzc{s}\maltese$ is maximal: Indeed, it cannot be extended neither by an
action of ${\mathbf{Q}}_{0}^{\perp}$ (contradicts the maximality of
$\mathpzc{t}_{0}$) nor by an action of
$\mathcal{C}[{\mathbf{Q}}_{1}\multimap^{+}{\mathbf{Q}}_{2}]^{\perp}$ or
${\mathbf{R}}$ (contradicts the maximality of $\mathpzc{s}^{\prime}$).

Finally $\kappa^{P}_{\blacktriangledown}\mathpzc{s}\maltese\in
V_{{\mathbf{P}}}$ is a path satisfying the constraints.

  * •

If $\mathcal{C}_{2}=\mathcal{C}\oplus^{+}{\mathbf{Q}}_{0}$ or
${\mathbf{Q}}_{0}\oplus^{+}\mathcal{C}$, by induction hypothesis, there exists
a path of the form
$\kappa^{P}_{\blacktriangledown}\overline{\kappa^{P}_{\bullet}\kappa^{P}_{\blacktriangle}}\mathpzc{s}^{\prime}\maltese$
maximal in
$V_{{\mathbf{\mathcal{C}[Q_{1}\multimap^{+}Q_{2}]\multimap^{+}R}}}$, where
$\kappa^{P}_{\blacktriangle}\overline{\mathpzc{s}^{\prime}}\in(\kappa^{P}_{\blacktriangle}\mathpzc{t}^{\prime})\shuffle\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{u}}}$}}$
with $\mathpzc{t}^{\prime}\in
V_{{\mathbf{\mathcal{C}[Q_{1}\multimap^{+}Q_{2}]}}}$ and $\mathpzc{u}\in
V_{{\mathbf{R}}}$. Reasoning as previous item, we see that for one of
$i\in\\{1,2\\}$ (depending on the form of context $\mathcal{C}_{2}$) the path
$\kappa^{P}_{\blacktriangledown}\overline{\kappa^{P}_{\bullet}\kappa^{P}_{\blacktriangle}\kappa^{Q}_{\iota_{i}}\kappa_{\blacktriangle}}\mathpzc{s}^{\prime}\maltese$
(where $\kappa_{\blacktriangle}^{P}$ now justifies $\kappa^{Q}_{\iota_{i}}$)
is in $V_{{\mathbf{P}}}$, maximal, and of the required form.

The result for the general case, where
${\mathbf{P}}=\mathcal{C}_{1}[\leavevmode\nobreak\
\mathcal{C}_{2}[{\mathbf{Q}}_{1}\multimap^{+}{\mathbf{Q}}_{2}]\multimap^{+}{\mathbf{R}}\leavevmode\nobreak\
]$, finally comes from Lemma 97. ∎