${\mathfrak{N}}$), unless such a path $\mathpzc{t}$ contains a negative
initial action whose address is not the address of a positive action on the
other side, but this restriction is harmless with respect to our condition.

We apply the induction hypothesis to get
${\mathfrak{P}}^{\prime\prime}\perp{\mathfrak{N}}^{\prime\prime}$. Finally
${\mathfrak{P}}\perp{\mathfrak{N}}$.

∎

######  Proposition 65.

Let ${\mathfrak{D}}$ and ${\mathfrak{E}}$ be closed-compatible multi-designs.
${\mathfrak{D}}\perp{\mathfrak{E}}$ if and only if there exists a path
$\mathpzc{s}$ of ${\mathfrak{D}}$ 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 a path of ${\mathfrak{E}}$.

###### Proof.

$(\Rightarrow)$ If ${\mathfrak{D}}\perp{\mathfrak{E}}$ then result follows
from Proposition 63.

$(\Leftarrow)$ We will prove that the hypothesis of Proposition 64 is
satisfied. Let us show that every path of ${\mathfrak{D}}$ (resp. of
${\mathfrak{E}}$) of the form $\mathpzc{t}\kappa^{+}$ where $\kappa^{+}$ is
proper and $\overline{\mathpzc{t}}$ is a path of ${\mathfrak{E}}$ (resp. of
${\mathfrak{D}}$) is a prefix of $\mathpzc{s}$ (resp. of
$\overline{\mathpzc{s}}$). By induction on the length of $\mathpzc{t}$,
knowing that it is either empty or negative-ended:

  * •

If $\mathpzc{t}$ is empty, $\kappa^{+}$ is necessarily the first action of the
positive design in ${\mathfrak{D}}$ (resp. in ${\mathfrak{E}}$), hence the
first action of $\mathpzc{s}$ (resp. of $\overline{\mathpzc{s}}$).

  * •

If $\mathpzc{t}=\mathpzc{t}_{0}\kappa^{-}$, then
$\overline{\mathpzc{t}_{0}\kappa^{-}}$ is a path of ${\mathfrak{E}}$ (resp. of
${\mathfrak{D}}$) and $\mathpzc{t}_{0}$ is a path of ${\mathfrak{D}}$ (resp.
of ${\mathfrak{E}}$). By induction hypothesis,
$\overline{\mathpzc{t}}=\overline{\mathpzc{t}_{0}\kappa^{-}}$ is a prefix of
$\overline{\mathpzc{s}}$ (resp. of $\mathpzc{s}$), thus $\mathpzc{t}$ is a
prefix of $\mathpzc{s}$ (resp. of $\overline{\mathpzc{s}}$). The path
$\mathpzc{s}$ is of the form
$\mathpzc{s}=\mathpzc{t}\kappa^{\prime+}\mathpzc{s}^{\prime}$. But since
$\mathpzc{s}$ and $\mathpzc{t}\kappa^{+}$ are both paths of ${\mathfrak{D}}$
(resp. ${\mathfrak{E}}$), they cannot differ on a positive action, hence
$\kappa^{+}=\kappa^{\prime+}$. Thus $\mathpzc{t}\kappa^{+}$ is a prefix of
$\mathpzc{s}$.

∎

###  A.3 Associativity for Interaction Paths

If $\mathpzc{s}$ is a path of a multi-design ${\mathfrak{D}}$, and
${\mathfrak{E}}\subseteq{\mathfrak{D}}$, then we write
$\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}$
for the longest subsequence of $\mathpzc{s}$ that is a path of
${\mathfrak{E}}$. Note that this is well defined.

######  Proposition 66 (Associativity for paths).

Let ${\mathfrak{D}}$, ${\mathfrak{E}}$ and ${\mathfrak{F}}$ be cut-free multi-
designs such that ${\mathfrak{E}}\cup{\mathfrak{F}}$ is a multi-design, and
suppose ${\mathfrak{D}}\perp({\mathfrak{E}}\cup{\mathfrak{F}})$. We have:

$\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle=\mathinner{\mathchoice{\langle{\mathfrak{E}}\cup{\mathfrak{F}}\leftarrow{\mathfrak{D}}\rangle\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\langle{\mathfrak{E}}\cup{\mathfrak{F}}\leftarrow{\mathfrak{D}}\rangle\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\langle{\mathfrak{E}}\cup{\mathfrak{F}}\leftarrow{\mathfrak{D}}\rangle\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\langle{\mathfrak{E}}\cup{\mathfrak{F}}\leftarrow{\mathfrak{D}}\rangle\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}$

###### Proof.

We will prove the result for a larger class of multi-designs. Instead of the
assumption ${\mathfrak{D}}\perp({\mathfrak{E}}\cup{\mathfrak{F}})$, suppose
that ${\mathfrak{D}}$ and ${\mathfrak{E}}\cup{\mathfrak{F}}$ are:

  * •

of opposite polarities

  * •

compatible

  * •

satisfying
$\mathrm{fv}({\mathfrak{D}})\subseteq\mathrm{np}({\mathfrak{E}}\cup{\mathfrak{F}})$
and
$\mathrm{fv}({\mathfrak{E}}\cup{\mathfrak{F}})\subseteq\mathrm{np}({\mathfrak{D}})$

  * •

and such that
$\maltese\in(\\![\mathfrak{Cut}_{{\mathfrak{E}}\cup{\mathfrak{F}}|{\mathfrak{D}}}]\\!)$
(in particular their interaction is finite).

First remark that ${\mathfrak{F}}$ and ${\mathfrak{D}}$ are compatible, hence
it is possible to define $\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}$.
Then since
$\maltese\in(\\![\mathfrak{Cut}_{{\mathfrak{E}}\cup{\mathfrak{F}}|{\mathfrak{D}}}]\\!)$,
we have
$\maltese\in(\\![\mathfrak{Cut}_{{\mathfrak{E}}|(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)}]\\!)$,
indeed:

$\displaystyle(\\![\mathfrak{Cut}_{{\mathfrak{E}}\cup{\mathfrak{F}}|{\mathfrak{D}}}]\\!)$
$\displaystyle=(\\![\mathfrak{Cut}_{{\mathfrak{E}}|\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}}]\\!)$
by Lemmas 54 and 53
$\displaystyle=(\\![\mathfrak{Cut}_{{\mathfrak{E}}|(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)}]\\!)$
by Corollary 52

This also shows that ${\mathfrak{E}}$ and
$(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)$ are compatible. As
they are of opposite polarities and they satisfy the condition on variables,
$\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle$
is defined.

Let
$\mathpzc{s}=\langle{\mathfrak{E}}\cup{\mathfrak{F}}\leftarrow{\mathfrak{D}}\rangle$,
and let us show the result (i.e.,
$\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle$)
by induction on the length of $\mathpzc{s}$, which is finite because the
interaction between ${\mathfrak{D}}$ and ${\mathfrak{E}}\cup{\mathfrak{F}}$ is
finite.

  * •

If $\mathpzc{s}=\epsilon$ then necessarily $\maltese\in{\mathfrak{D}}$ thus
also $\maltese\in(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)$.
Hence
$\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\epsilon=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle$.

  * •

If $\mathpzc{s}=\maltese$ then $\maltese\in{\mathfrak{E}}\cup{\mathfrak{F}}$.
If $\maltese\in{\mathfrak{E}}$ then
$\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle=\maltese=\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}$.
Otherwise $\maltese\in{\mathfrak{F}}$, thus
$\maltese\in(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)$ and
$\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle=\epsilon=\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}$.

  * •

If $\mathpzc{s}=\kappa^{+}\mathpzc{s}^{\prime}$ where
$\kappa^{+}=x|\overline{a}\langle\overrightarrow{x^{a}}\rangle$ is a proper
positive action, then ${\mathfrak{E}}\cup{\mathfrak{F}}$ is a positive multi-
design such that its only positive design is of the form
${\mathfrak{p}}=x|\overline{a}\langle\overrightarrow{{\mathfrak{m}}}\rangle$.
Thus ${\mathfrak{D}}$ is negative, and there exists ${\mathfrak{n}}$ such that
$({\mathfrak{n}}/x)\in{\mathfrak{D}}$ of the form
${\mathfrak{n}}=\sum_{b\in\mathcal{S}}b(\overrightarrow{x^{b}}).{\mathfrak{p}}_{b}$,
where ${\mathfrak{p}}_{a}\neq\Omega$ because the interaction converges. Let
${\mathfrak{D}}^{\prime}=({\mathfrak{D}}\setminus\\{{\mathfrak{n}}/x\\})\cup\\{{\mathfrak{p}}_{a}\\}$.

    * –

Either ${\mathfrak{p}}\in{\mathfrak{F}}$ [reduction step].
In this case, we have
$\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}$,
so let us show that
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle$.
By definition of the interaction sequence, we have
$\mathpzc{s}^{\prime}=\langle{\mathfrak{E}}\cup{\mathfrak{F}}^{\prime}\leftarrow{\mathfrak{D}}^{\prime}\rangle$
where
${\mathfrak{F}}^{\prime}=({\mathfrak{F}}\setminus\\{{\mathfrak{p}}\\})\cup\\{\overrightarrow{({\mathfrak{m}}/x^{a})}\\}$.
Thus by induction hypothesis
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}^{\prime}|{\mathfrak{D}}^{\prime}}]\\!)\rangle$.
But by Lemma 59,
$\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}^{\prime}|{\mathfrak{D}}^{\prime}}]\\!)\rangle=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle$
because the negatives among $\overrightarrow{({\mathfrak{m}}/x^{a})}$ in
$(\\![\mathfrak{Cut}_{{\mathfrak{F}}^{\prime}|{\mathfrak{D}}^{\prime}}]\\!)$
will not interfere in the interaction with ${\mathfrak{E}}$, since the
variables $\overrightarrow{x^{a}}$ do not appear in ${\mathfrak{E}}$. Hence
the result.

    * –

Or ${\mathfrak{p}}\in{\mathfrak{E}}$ [commutation step].
In this case, we have
$\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\kappa^{+}(\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}})$,
and by definition of the interaction sequence
$\mathpzc{s}^{\prime}=\langle{\mathfrak{E}}^{\prime}\cup{\mathfrak{F}}\leftarrow{\mathfrak{D}}^{\prime}\rangle$
where
${\mathfrak{E}}^{\prime}=({\mathfrak{E}}\setminus\\{{\mathfrak{p}}\\})\cup\\{\overrightarrow{({\mathfrak{m}}/x^{a})}\\}$.
Thus by induction hypothesis
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}^{\prime}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}^{\prime}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}^{\prime}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}^{\prime}}}=\langle{\mathfrak{E}}^{\prime}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}}]\\!)\rangle$.
But we have

$\displaystyle\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle$
$\displaystyle=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}\cup\\{({\mathfrak{n}}/x)\\}\setminus\\{{\mathfrak{p}}_{a}\\}}]\\!)\rangle$
$\displaystyle=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}}]\\!)\cup\\{({\mathfrak{n}}^{\prime}/x)\\}\setminus\\{{\mathfrak{p}}^{\prime}_{a}\\}\rangle$
$\displaystyle=\kappa^{+}\langle{\mathfrak{E}}^{\prime}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}}]\\!)\rangle$

where ${\mathfrak{n}}^{\prime}$ is the only negative design of
$(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)$ on variable $x$,
and ${\mathfrak{p}}_{a}^{\prime}$ the only positive design of
$(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}}]\\!)$. Hence
$\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle=\kappa^{+}(\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}})=\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}$.

  * •

If $\mathpzc{s}=\kappa^{-}\mathpzc{s}^{\prime}$ where
$\kappa^{-}=a_{x}(\overrightarrow{x^{a}})$, then ${\mathfrak{D}}$ is positive
with only positive design of the form
${\mathfrak{p}}=x|\overline{a}\langle\overrightarrow{{\mathfrak{m}}}\rangle$,
and there exists a negative design ${\mathfrak{n}}$ such that
$({\mathfrak{n}}/x)\in{\mathfrak{E}}\cup{\mathfrak{F}}$, with ${\mathfrak{n}}$
of the form
${\mathfrak{n}}=\sum_{b\in\mathcal{S}}b(\overrightarrow{x^{b}}).{\mathfrak{p}}_{b}$
where ${\mathfrak{p}}_{a}\neq\Omega$. By definition of the interaction
sequence, we have
$\mathpzc{s}^{\prime}=\langle(({\mathfrak{E}}\cup{\mathfrak{F}})\setminus\\{{\mathfrak{n}}/x\\})\cup\\{{\mathfrak{p}}_{a}\\}\leftarrow{\mathfrak{D}}^{\prime}\rangle$
where
${\mathfrak{D}}^{\prime}=({\mathfrak{D}}\setminus\\{{\mathfrak{p}}\\})\cup\\{\overrightarrow{({\mathfrak{m}}/x^{a})}\\}$.

    * –

Either ${\mathfrak{n}}\in{\mathfrak{F}}$ [reduction step].
In this case, we have
$\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}$,
so let us show that
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle$.
By induction hypothesis
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}^{\prime}|{\mathfrak{D}}^{\prime}}]\\!)\rangle$
where
${\mathfrak{F}}^{\prime}=({\mathfrak{F}}\setminus\\{{\mathfrak{n}}/x\\})\cup\\{{\mathfrak{p}}_{a}\\}$,
and by Lemma 59 we deduce
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle$,
hence the result.

    * –

Or ${\mathfrak{n}}\in{\mathfrak{E}}$ [commutation step].
In this case, we have
$\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\kappa^{-}(\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}})$.
By induction hypothesis
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}=\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}^{\prime}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}^{\prime}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}^{\prime}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}^{\prime}}}=\langle{\mathfrak{E}}^{\prime}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}}]\\!)\rangle$
where
${\mathfrak{E}}^{\prime}=({\mathfrak{E}}\setminus\\{{\mathfrak{n}}/x\\})\cup\\{{\mathfrak{p}}_{a}\\}$.
But we have

$\displaystyle\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle$
$\displaystyle=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}\cup\\{{\mathfrak{p}}\\}\setminus\\{\overrightarrow{({\mathfrak{m}}/x^{a})}\\}}]\\!)\rangle$
$\displaystyle=\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}}]\\!)\cup\\{{\mathfrak{p}}^{\prime}\\}\setminus\\{\overrightarrow{({\mathfrak{m}}^{\prime}/x^{a})}\\}\rangle$
$\displaystyle=\kappa^{-}\langle{\mathfrak{E}}^{\prime}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}}]\\!)\rangle$

where ${\mathfrak{p}}^{\prime}$ is the only positive design of
$(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)$, and for each
$i\leq ar(a)$, ${\mathfrak{m}}^{\prime}_{i}$ is the only negative design of
$(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}^{\prime}}]\\!)$ on
variable $x^{a}_{i}$. Therefore
$\langle{\mathfrak{E}}\leftarrow(\\![\mathfrak{Cut}_{{\mathfrak{F}}|{\mathfrak{D}}}]\\!)\rangle=\kappa^{-}(\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}})=\mathinner{\mathchoice{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}{\mathpzc{s}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{E}}}{\mathpzc{s}\\!\\!\upharpoonright\\!\\!{\mathfrak{E}}}}$,
which concludes the proof.

∎

##  Appendix B Proofs of Subsection 3.2

We now come back to (non “multi-”) designs, and we prove:

  * •

the form of visitable paths for each connective (§ B.2), which is needed for
next point;

  * •

that (some) connectives preserve regularity (Propositions 84, 87, 88,
corresponding to Proposition 18), purity (Proposition 19) and quasi-purity
(Proposition 21).

###  B.1 Preliminaries

####  B.1.1 Observational Ordering and Monotonicity

We consider the observational ordering $\preceq$ over designs:
${\mathfrak{d}}^{\prime}\preceq{\mathfrak{d}}$ if ${\mathfrak{d}}$ can be
obtained from ${\mathfrak{d}}^{\prime}$ by substituting:

  * •

positive subdesigns for some occurrences of $\Omega$.

  * •

$\maltese$ for some positive subdesigns.

Remark in particular that for all positive designs ${\mathfrak{p}}$ and
${\mathfrak{p}}^{\prime}$, we have
$\Omega\preceq{\mathfrak{p}}\preceq\maltese$, and if
${\mathfrak{p}}\sqsubseteq{\mathfrak{p}}^{\prime}$ then
${\mathfrak{p}}\preceq{\mathfrak{p}}^{\prime}$. We can now state the
monotonicity theorem, an important result of ludics. A proof of the theorem
formulated in this form is found in [17].

######  Theorem 67 (Monotonicity).

  * •

If ${\mathfrak{d}}\preceq{\mathfrak{e}}$ and
${\mathfrak{m}}\preceq{\mathfrak{n}}$, then
${\mathfrak{d}}[{\mathfrak{m}}/x]\preceq{\mathfrak{e}}[{\mathfrak{n}}/x]$

  * •

If ${\mathfrak{d}}\preceq{\mathfrak{e}}$ then
$(\\![{\mathfrak{d}}]\\!)\preceq(\\![{\mathfrak{e}}]\\!)$

This means that the relation $\preceq$ compares the likelihood of convergence:
if ${\mathfrak{d}}\perp{\mathfrak{e}}$ and
${\mathfrak{d}}\preceq{\mathfrak{d}}^{\prime}$ then
${\mathfrak{d}}^{\prime}\perp{\mathfrak{e}}$. In particular, if ${\mathbf{B}}$
is a behaviour, if ${\mathfrak{d}}\in{\mathbf{B}}$ and
${\mathfrak{d}}\preceq{\mathfrak{d}}^{\prime}$ then
${\mathfrak{d}}^{\prime}\in{\mathbf{B}}$.

Remark the following important fact: given a path $\mathpzc{s}$ of some design
${\mathfrak{d}}$, there is a unique design maximal for $\preceq$ such that
$\mathpzc{s}$ is a path of it. Indeed, this 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 obtained from ${\mathfrak{d}}$ by replacing all positive subdesigns
(possibly $\Omega$) whose first positive action is not in $\mathpzc{s}$ by
$\maltese$. Note that, actually, 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}$
does not depend on ${\mathfrak{d}}$ but only on the path $\mathpzc{s}$.

######  Example 68.

Consider design ${\mathfrak{d}}$ and the path $\mathpzc{s}$ below:

$\displaystyle{\mathfrak{d}}\hskip 14.22636pt$ $\displaystyle=\hskip
14.22636ptx|\overline{a}\langle
b(y).(y|\overline{e}\langle\rangle),c().\maltese+d(z).(z|\overline{e}\langle\rangle)\rangle$
$\displaystyle\mathpzc{s}\hskip 14.22636pt$ $\displaystyle=\hskip
14.22636ptx|\overline{a}\langle x_{1},x_{2}\rangle\hskip
28.45274ptb_{x_{1}}(y)\hskip 28.45274pty|\overline{e}\langle\rangle\hskip
28.45274ptc_{x_{2}}()\hskip 28.45274pt\maltese$ $x_{0}|\overline{a}\langle
x_{1},x_{2}\rangle$$d_{x_{2}}(y)$$z|\overline{e}\langle\rangle$$c_{x_{2}}()$$\maltese$$b_{x_{1}}(y)$$y|\overline{e}\langle\rangle$$\mathpzc{s}$

We have
$\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}=x|\overline{a}\langle
b(y).(y|\overline{e}\langle\rangle)+\sum_{f\neq
b}f(\overrightarrow{x^{f}}).\maltese,\sum_{f\in\mathcal{S}}f(\overrightarrow{x^{f}}).\maltese\rangle$

$x_{0}|\overline{a}\langle
x_{1},x_{2}\rangle$$\dots$$f_{x_{2}}(\overrightarrow{x^{f}})$$\maltese$$\dots$$d_{x_{2}}(y)$$\maltese$$c_{x_{2}}()$$\maltese$$b_{x_{1}}(y)$$y|\overline{e}\langle\rangle$$\dots$$f_{x_{1}}(\overrightarrow{x^{f}})$$\maltese$$\dots$$\mathpzc{s}$

######  Proposition 69.

If $\mathpzc{s}\in V_{{\mathbf{{\mathbf{B}}}}}$ then
$\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}\in{\mathbf{B}}$.

###### Proof.

There exists ${\mathfrak{d}}\in{\mathbf{B}}$ such that $\mathpzc{s}$ is a path
of ${\mathfrak{d}}$, thus
${\mathfrak{d}}\preceq\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}$.
The result then comes from monotonicity (Theorem 67). ∎

####  B.1.2 More on Paths

Let ${\mathbf{B}}$ be a behaviour.

######  Lemma 70.

If ${\mathfrak{d}}\in{\mathbf{B}}$ and $\mathpzc{s}\in V_{{\mathbf{B}}}$ is a
path of ${\mathfrak{d}}$, then $\mathpzc{s}$ is a path of $|{\mathfrak{d}}|$.

###### Proof.

Let ${\mathfrak{e}}\in{\mathbf{B}}^{\perp}$ such that
$\mathpzc{s}=\langle{\mathfrak{d}}\leftarrow{\mathfrak{e}}\rangle$, and let
$\mathpzc{t}=\langle|{\mathfrak{d}}|\leftarrow{\mathfrak{e}}\rangle$.

  * •

Since $|{\mathfrak{d}}|\sqsubseteq{\mathfrak{d}}$, the path $\mathpzc{s}$
cannot be a strict prefix of $\mathpzc{t}$, and $\mathpzc{s}$ and
$\mathpzc{t}$ cannot differ on a positive action.

  * •

If $\mathpzc{t}$ is a strict prefix of $\mathpzc{s}$ then it is positive-
ended. So $\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 $\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}}}$
are paths of ${\mathfrak{e}}$ differing on a positive action, which is
impossible.

  * •

If $\mathpzc{s}$ and $\mathpzc{t}$ differ on a negative action, say
$\mathpzc{u}\kappa^{-}_{1}$ and $\mathpzc{u}\kappa^{-}_{2}$ are respective
prefixes of $\mathpzc{s}$ and $\mathpzc{t}$ with
$\kappa^{-}_{1}\neq\kappa^{-}_{2}$, then
$\overline{\mathpzc{u}\kappa^{-}_{1}}$ and
$\overline{\mathpzc{u}\kappa^{-}_{2}}$ are paths of ${\mathfrak{e}}$ differing
on a positive action, which is impossible.

Thus we must have $\mathpzc{s}=\mathpzc{t}$, hence the result. ∎

######  Lemma 71.

Let $\mathpzc{s}\in V_{{\mathbf{B}}}$. For every positive-ended (resp.
negative-ended) prefix $\mathpzc{s}^{\prime}$ of $\mathpzc{s}$, we have
$\mathpzc{s}^{\prime}\in V_{{\mathbf{B}}}$ (resp.
$\mathpzc{s}^{\prime}\maltese\in V_{{\mathbf{B}}}$).

###### Proof.

Let $\mathpzc{s}=\langle{\mathfrak{d}}\leftarrow{\mathfrak{e}}\rangle$ where
${\mathfrak{d}}\in B$ and ${\mathfrak{e}}\in B^{\perp}$, and let
$\mathpzc{s}^{\prime}$ be a prefix of $\mathpzc{s}$.

  * •

If $\mathpzc{s}^{\prime}$ is negative-ended, let $\kappa^{+}$ be such that
$\mathpzc{s}^{\prime}\kappa^{+}$ is a prefix of $\mathpzc{s}$. The action
$\kappa^{+}$ comes from ${\mathfrak{d}}$. Consider design
${\mathfrak{d}}^{\prime}$ obtained from ${\mathfrak{d}}$ by replacing the
positive subdesign of ${\mathfrak{d}}$ starting on action $\kappa^{+}$ with
$\maltese$. Since ${\mathfrak{d}}\preceq{\mathfrak{d}}^{\prime}$, by
monotonicity ${\mathfrak{d}}^{\prime}\in{\mathbf{B}}$. Moreover
$\mathpzc{s}^{\prime}\maltese=\langle{\mathfrak{d}}^{\prime}\leftarrow{\mathfrak{e}}\rangle$,
hence the result.

  * •

If $\mathpzc{s}^{\prime}$ is positive-ended then either
$\mathpzc{s}^{\prime}=\mathpzc{s}$ and there is nothing to prove or
$\mathpzc{s}^{\prime}$ is a strict prefix of $\mathpzc{s}$, so assume we are
in the second case. $\mathpzc{s}^{\prime}$ is $\maltese$-free, hence
$\overline{\mathpzc{s}^{\prime}}$ is a negative-ended prefix of
$\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{B^{\perp}}}}$. Using the argument above, it comes
$\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}=\overline{\mathpzc{s}^{\prime}}\maltese\in
V_{{\mathbf{B^{\perp}}}}$, thus $\mathpzc{s}^{\prime}\in V_{{\mathbf{B}}}$.

∎

######  Lemma 72.

Let $\mathpzc{s}\in V_{{\mathbf{B}}}$. For every prefix
$\mathpzc{s}^{\prime}\kappa^{-}$ of $\mathpzc{s}$ and every
${\mathfrak{d}}\in{\mathbf{B}}$ such that $\mathpzc{s}^{\prime}$ is a path of
${\mathfrak{d}}$, $\mathpzc{s}^{\prime}\kappa^{-}$ is a prefix of a path of
${\mathfrak{d}}$.

###### Proof.

There exist ${\mathfrak{d}}_{0}\in{\mathbf{B}}$ and
${\mathfrak{e}}_{0}\in{\mathbf{B}}^{\perp}$ such that
$\mathpzc{s}=\langle{\mathfrak{d}}_{0}\leftarrow{\mathfrak{e}}_{0}\rangle$.
Let $\mathpzc{s}^{\prime}\kappa^{-}$ be a prefix of $\mathpzc{s}$, and let
${\mathfrak{d}}\in{\mathbf{B}}$ such that $\mathpzc{s}^{\prime}$ is a path of
${\mathfrak{d}}$. Since $\overline{\mathpzc{s}^{\prime}}$ is a prefix of a
path of ${\mathfrak{e}}_{0}$, $\mathpzc{s}^{\prime}$ is a prefix of
$\langle{\mathfrak{d}}\leftarrow{\mathfrak{e}}_{0}\rangle$. We cannot have
$\mathpzc{s}^{\prime}=\langle{\mathfrak{d}}\leftarrow{\mathfrak{e}}_{0}\rangle$,
otherwise
$\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}=\overline{\mathpzc{s}^{\prime}}\maltese$
and $\overline{\mathpzc{s}^{\prime}\kappa^{-}}$ would be paths of
${\mathfrak{e}}_{0}$ differing on a positive action, which is impossible. Thus
there exists $\kappa^{\prime-}$ such that
$\mathpzc{s}^{\prime}\kappa^{\prime-}$ is a prefix of
$\langle{\mathfrak{d}}\leftarrow{\mathfrak{e}}_{0}\rangle$, which is a path of
${\mathfrak{d}}$, and necessarily $\kappa^{-}=\kappa^{\prime-}$. Finally
$\mathpzc{s}^{\prime}\kappa^{-}$ is a prefix of a path of ${\mathfrak{d}}$. ∎

####  B.1.3 An Alternative Definition of Regularity

Define the anti-shuffle ( $\shuffle$ ) as the dual operation of shuffle, that
is:

  * •

$\mathpzc{s}\text{\rotatebox[origin={c}]{180.0}{$\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}{\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}}}$}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{16.90277pt}{0.0pt}{$\sim$}$}\hss}{\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}}}$}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{16.90277pt}{0.0pt}{$\sim$}$}\hss}{\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}}}$}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{16.90277pt}{0.0pt}{$\sim$}$}\hss}{\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}}}$}}}}$}}$
if $\mathpzc{s}$ and $\mathpzc{t}$ are paths of same polarity;

  * •

$S\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}T=\makebox[23.01039pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{23.01039pt}{0.0pt}{$\sim$}$}\hss}{\makebox[6.70831pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}$}}\shuffle\makebox[7.23265pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}$}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{23.01039pt}{0.0pt}{$\sim$}$}\hss}{\makebox[6.70831pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}$}}\shuffle\makebox[7.23265pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}$}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{23.01039pt}{0.0pt}{$\sim$}$}\hss}{\makebox[6.70831pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}$}}\shuffle\makebox[7.23265pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}$}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{23.01039pt}{0.0pt}{$\sim$}$}\hss}{\makebox[6.70831pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{6.70831pt}{0.0pt}{$\sim$}$}\hss}{S}}$}}\shuffle\makebox[7.23265pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{7.23265pt}{0.0pt}{$\sim$}$}\hss}{T}}$}}}}$}}$
if $S$ and $T$ are sets of paths of same polarity.

######  Definition 73.

  * •

A trivial view is an aj-sequence such that each proper action except the first
one is justified by the immediate previous action. In other words, it is a
view such that its dual is a view as well.

  * •

The trivial view of an aj-sequence is defined inductively by:

$\displaystyle\langle\epsilon\rangle$ $\displaystyle=\epsilon$ empty sequence
$\displaystyle\langle\mathpzc{s}\maltese\rangle$
$\displaystyle=\langle\mathpzc{s}\rangle\maltese$
$\displaystyle\langle\mathpzc{s}\kappa\rangle$ $\displaystyle=\kappa$
$\displaystyle\mbox{ if }\kappa\neq\maltese\mbox{ initial}$
$\displaystyle\langle\mathpzc{s}\kappa\rangle$
$\displaystyle=\langle\mathpzc{s}_{0}\rangle\kappa$ $\displaystyle\mbox{ if
}\kappa\neq\maltese\mbox{ justified, where }\mathpzc{s}_{0}\mbox{ prefix of
}\mathpzc{s}\mbox{ ending on }\mathrm{just}(\kappa)$

We also write $\langle\kappa\rangle_{\mathpzc{s}}$ (or even
$\langle\kappa\rangle$) instead of $\langle\mathpzc{s}^{\prime}\kappa\rangle$
when $\mathpzc{s}^{\prime}\kappa$ is a prefix of $\mathpzc{s}$.

  * •

Trivial views of a design ${\mathfrak{d}}$ are the trivial views of its paths
(or of its views). In particular, $\epsilon$ is a trivial view of negative
designs only.

  * •

Trivial views of designs in $|{\mathbf{B}}|$ are called trivial views of
${\mathbf{B}}$.

######  Lemma 74.

  1. 1.

Every view is in the anti-shuffle of trivial views.

  2. 2.

Every path is in the shuffle of views.

###### Proof.

  1. 1.

Let ${\mathbb{v}}$ be a view, the result is shown by induction on
${\mathbb{v}}$:

     * •

If ${\mathbb{v}}=\epsilon$ or ${\mathbb{v}}=\kappa$, it is itself a trivial
view, hence the result.

     * •

Suppose ${\mathbb{v}}={\mathbb{v}}^{\prime}\kappa$ with
${\mathbb{v}}^{\prime}\neq\epsilon$ and
${\mathbb{v}}^{\prime}\in{\mathbb{t}}_{1}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\dots\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}{\mathbb{t}}_{n}$
where the ${\mathbb{t}}_{i}$ are trivial views.

       * –

If $\kappa$ is negative, as ${\mathbb{v}}$ is a view, the action $\kappa$ is
justified by the last action of ${\mathbb{v}}^{\prime}$, say $\kappa^{+}$.
Hence $\kappa^{+}$ is the last action of some trivial view
${\mathbb{t}}_{i_{0}}$. Hence
${\mathbb{v}}\in{\mathbb{t}}_{1}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\dots\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}{\mathbb{t}}_{i_{0}-1}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}({\mathbb{t}}_{i_{0}}\kappa)\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}{\mathbb{t}}_{i_{0}+1}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\dots\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}{\mathbb{t}}_{n}$.

       * –

If $\kappa$ is positive, either it is initial and
${\mathbb{v}}\in{\mathbb{t}}_{1}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\dots\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}{\mathbb{t}}_{n}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\kappa$
with $\kappa$ a trivial view, or it is justified by $\kappa^{-}$ in
${\mathbb{v}}^{\prime}$. In the last case, there exists a unique $i_{0}$ such
that $\kappa^{-}$ appears in ${\mathbb{t}}_{i_{0}}$, so let
${\mathbb{t}}\kappa^{-}$ be the prefix of ${\mathbb{t}}_{i_{0}}$ ending with
$\kappa^{-}$. We have that
${\mathbb{v}}\in{\mathbb{t}}_{1}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\dots\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}{\mathbb{t}}_{n}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}({\mathbb{t}}\kappa^{-}\kappa)$
where ${\mathbb{t}}\kappa^{-}\kappa$ is a trivial view.

  2. 2.

Similar reasoning as above, but replacing  $\shuffle$ by $\shuffle$, “trivial
view” by “view”, “view” by “path”, and exchanging the role of the polarities
of actions.

∎

######  Remark.

Following previous result, note that every view (resp. path) of a design
${\mathfrak{d}}$ is in the anti-shuffle of trivial views (resp. in the shuffle
of views) of ${\mathfrak{d}}$.

######  Proposition 75.

${\mathbf{B}}$ is regular if and only if the following conditions hold:

  * •

the positive-ended trivial views of ${\mathbf{B}}$ are visitable in
${\mathbf{B}}$,

  * •

$V_{{\mathbf{B}}}$ and $V_{{\mathbf{B^{\perp}}}}$ are stable under $\shuffle$
(i.e., $V_{{\mathbf{B}}}$ is stable under $\shuffle$ and  $\shuffle$ ).

###### Proof.

Let ${\mathbf{B}}$ be a behaviour.
($\Rightarrow$) Suppose ${\mathbf{B}}$ is regular, and let ${\mathbb{t}}$ be a
positive-ended trivial view of ${\mathbf{B}}$. There exists a view
${\mathbb{v}}$ of a design ${\mathfrak{d}}\in|{\mathbf{B}}|$ such that
${\mathbb{t}}$ is a subsequence of ${\mathbb{v}}$, and such that
${\mathbb{v}}$ ends with the same action as ${\mathbb{t}}$. Since
${\mathbb{v}}$ is a view of ${\mathfrak{d}}$, ${\mathbb{v}}$ is in particular
a path of ${\mathfrak{d}}$, hence by regularity ${\mathbb{v}}\in
V_{{\mathbf{B}}}$. There exists ${\mathfrak{e}}\in{\mathbf{B}}^{\perp}$ such
that ${\mathbb{v}}=\langle{\mathfrak{d}}\leftarrow{\mathfrak{e}}\rangle$, and
by Lemma 70 we can even take ${\mathfrak{e}}\in|{\mathbf{B}}^{\perp}|$. Since
$\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 a path of ${\mathfrak{e}}$, $\ulcorner$$\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}}}}$$\urcorner$
is a view of ${\mathfrak{e}}$. But notice that
$\raisebox{2.0776pt}{$\ulcorner$}{\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}{$\urcorner$}=\raisebox{2.0776pt}{$\ulcorner$}{\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}}}}$}}}\raisebox{2.0776pt}{$\urcorner$}=\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}}}}$}}$
by definition of a view and of a trivial view. We deduce 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 view (and in particular a path) of ${\mathfrak{e}}$, hence
$\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{B^{\perp}}}}$ by regularity. Finally, ${\mathbb{t}}\in
V_{{\mathbf{B}}}$.
($\Leftarrow$) Assume the two conditions of the statement. Let $\mathpzc{s}$
be a path of some design of $|{\mathbf{B}}|$. By Lemma 74, we know that there
exist views ${\mathbb{v}}_{1}$, …, ${\mathbb{v}}_{n}$ such that
$\mathpzc{s}\in{\mathbb{v}}_{1}\shuffle\dots\shuffle{\mathbb{v}}_{n}$, and for
each ${\mathbb{v}}_{i}$ there exist trivial views ${\mathbb{t}}_{i,1}$, …,
${\mathbb{t}}_{i,m_{i}}$ such that
${\mathbb{v}}_{i}\in{\mathbb{t}}_{i,1}\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}\dots\text{\rotatebox[origin={c}]{180.0}{$\shuffle$}}{\mathbb{t}}_{i,m_{i}}$.
By hypothesis each ${\mathbb{t}}_{i,j}$ is visitable in ${\mathbf{B}}$, hence
as $V_{{\mathbf{B}}}$ is stable by anti-shuffle, ${\mathbb{v}}_{i}\in
V_{{\mathbf{B}}}$. Thus as $V_{{\mathbf{B}}}$ is stable by shuffle,
$\mathpzc{s}\in V_{{\mathbf{B}}}$. Similarly the paths of designs of
$|{\mathbf{B}}^{\perp}|$ are visitable in ${\mathbf{B}}^{\perp}$. Hence the
result. ∎

###  B.2 Form of the Visitable Paths

From internal completeness, we can make explicit the form of the visitable
paths for behaviours constructed by logical connectives; such results are
necessary for proving the stability of regularity and purity (§ B.3 and B.4
respectively).

We will use the notations given at the beginning of Subsection 2.2, and also
the following. Given an action $\kappa$ and a set of sequences $V$, we write
$\kappa V$ for $\\{\kappa\mathpzc{s}\leavevmode\nobreak\
\boldsymbol{|}\leavevmode\nobreak\ \mathpzc{s}\in V\\}$. Let us note
$\kappa_{\blacktriangledown}=x_{0}|\blacktriangledown\langle x\rangle$,
$\kappa_{\blacktriangle}=\blacktriangle_{x_{0}}(x)$,
$\kappa_{\bullet}=x_{0}|\bullet\langle x,y\rangle$ and
$\kappa_{\iota_{i}}=x_{0}|\iota_{i}\langle x_{i}\rangle$ for $i\in\\{1,2\\}$.

In this section are proved the following results:

  * •

$V_{{\mathbf{\shpos
N}}}=\kappa_{\blacktriangledown}V_{{\mathbf{N}}}^{x}\cup\\{\maltese\\}$ and
$V_{{\mathbf{\shneg
P}}}=\kappa_{\blacktriangle}V_{{\mathbf{P}}}^{x}\cup\\{\epsilon\\}$
(Proposition 78),

  * •

$V_{{\mathbf{M\oplus
N}}}=\kappa_{\iota_{1}}V_{{\mathbf{M}}}^{x_{1}}\cup\kappa_{\iota_{2}}V_{{\mathbf{N}}}^{x_{2}}\cup\\{\maltese\\}$
(Proposition 79),

  * •

$V_{{\mathbf{M\otimes N}}}=\kappa_{\bullet}(V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y})\cup\\{\maltese\\}$ if ${\mathbf{M}}$ and ${\mathbf{N}}$
are regular (Proposition 82),

  * •

the general form of the visitable paths of ${\mathbf{M}}\otimes{\mathbf{N}}$,
not as simple (Proposition 80),

  * •

finally, the case of $\multimap$ easily deduced from $\otimes$ (Corollaries 81
and 83).

####  B.2.1 Shifts

######  Lemma 76.

  1. 1.

$(\blacktriangle(x).({\mathbf{N}}^{\perp})^{x})^{\perp}\subseteq\blacktriangledown\langle{\mathbf{N}}\rangle\cup\\{\maltese\\}$.

  2. 2.

$\blacktriangle(x).({\mathbf{N}}^{\perp})^{x}\subseteq\blacktriangledown\langle{\mathbf{N}}\rangle^{\perp}$.

###### Proof.

Let $E=\blacktriangledown\langle{\mathbf{N}}\rangle$, and let
$F=\blacktriangle(x).({\mathbf{N}}^{\perp})^{x}$. To show the lemma, we must
show $F^{\perp}\subseteq E\cup\\{\maltese\\}$ and $F\subseteq E^{\perp}$.

  1. 1.

Let ${\mathfrak{q}}\in F^{\perp}$. If ${\mathfrak{q}}\neq\maltese$,
${\mathfrak{q}}$ is necessarily of the form
$\blacktriangledown\langle{\mathfrak{n}}\rangle$ where ${\mathfrak{n}}$ is a
negative atomic design. For every design
${\mathfrak{p}}\in{\mathbf{N}}^{\perp}$, we have
$\blacktriangle(x).{\mathfrak{p}}^{x}\in F$ and
${\mathfrak{q}}[\blacktriangle(x).{\mathfrak{p}}^{x}/x_{0}]\leadsto{\mathfrak{p}}[{\mathfrak{n}}/x_{0}]$,
thus
$(\\![{\mathfrak{q}}[\blacktriangle(x).{\mathfrak{p}}^{x}/x_{0}]]\\!)=(\\![{\mathfrak{p}}[{\mathfrak{n}}/x_{0}]]\\!)=\maltese$
since ${\mathfrak{q}}\perp\blacktriangle(x).{\mathfrak{p}}^{x}$. We deduce
${\mathfrak{n}}\in{\mathbf{N}}$, hence ${\mathfrak{q}}\in E$.

  2. 2.

Let ${\mathfrak{m}}=\blacktriangle(x).{\mathfrak{p}}^{x}\in F$. For every
design ${\mathfrak{n}}\in{\mathbf{N}}$, we have
$\blacktriangledown\langle{\mathfrak{n}}\rangle[{\mathfrak{m}}/x_{0}]\leadsto{\mathfrak{p}}[{\mathfrak{n}}/x_{0}]$,
thus
$(\\![\blacktriangledown\langle{\mathfrak{n}}\rangle[{\mathfrak{m}}/x_{0}]]\\!)=(\\![{\mathfrak{p}}[{\mathfrak{n}}/x_{0}]]\\!)=\maltese$
since ${\mathfrak{p}}\in{\mathbf{N}}^{\perp}$ and
${\mathfrak{n}}\in{\mathbf{N}}$. Hence ${\mathfrak{m}}\in E^{\perp}$.

∎

######  Lemma 77.

$\shneg{\mathbf{P}}=(\shpos{\mathbf{P}}^{\perp})^{\perp}$.

###### Proof.

If we take ${\mathbf{N}}={\mathbf{P}}^{\perp}$, Lemma 76 gives us:

  1. 1.

$(\blacktriangle(x).{\mathbf{P}}^{x})^{\perp}\subseteq\blacktriangledown\langle{\mathbf{P}}^{\perp}\rangle\cup\\{\maltese\\}$
and

  2. 2.

$\blacktriangle(x).{\mathbf{P}}^{x}\subseteq\blacktriangledown\langle{\mathbf{P}}^{\perp}\rangle^{\perp}$.

Let $E=\blacktriangledown\langle{\mathbf{P}}^{\perp}\rangle$, and let
$F=\blacktriangle(x).{\mathbf{P}}^{x}$. By definition
$\shneg{\mathbf{P}}=F^{\perp\perp}$. From (2) we deduce
$F^{\perp\perp}\subseteq E^{\perp}$, and from (1)
$E^{\perp}=(E\cup\\{\maltese\\})^{\perp}\subseteq F^{\perp\perp}$. Hence
$\shneg{\mathbf{P}}=F^{\perp\perp}=E^{\perp}=(\shpos{\mathbf{P}}^{\perp})^{\perp}$.
∎

######  Proposition 78.

  1. 1.

$V_{{\mathbf{\shpos
N}}}=\kappa_{\blacktriangledown}V_{{\mathbf{N}}}^{x}\cup\\{\maltese\\}$

  2. 2.

$V_{{\mathbf{\shneg
P}}}=\kappa_{\blacktriangle}V_{{\mathbf{P}}}^{x}\cup\\{\epsilon\\}$

###### Proof.

  1. 1.

$(\subseteq)$ Let ${\mathfrak{q}}\in\shpos{\mathbf{N}}$ and
${\mathfrak{m}}\in(\shpos{\mathbf{N}})^{\perp}$, let us show that
$\langle{\mathfrak{q}}\leftarrow{\mathfrak{m}}\rangle\in\kappa_{\blacktriangledown}V_{{\mathbf{N}}}^{x}\cup\\{\maltese\\}$.
By Lemma 77, ${\mathfrak{m}}\in\shneg{\mathbf{N}}^{\perp}$. If
${\mathfrak{q}}=\maltese$ then
$\langle{\mathfrak{q}}\leftarrow{\mathfrak{m}}\rangle=\maltese$. Otherwise, by
Theorem 8, ${\mathfrak{q}}=\blacktriangledown\langle{\mathfrak{n}}\rangle$
with ${\mathfrak{n}}\in{\mathbf{N}}$. We have
$\langle{\mathfrak{q}}\leftarrow{\mathfrak{m}}\rangle=\langle{\mathfrak{q}}\leftarrow|{\mathfrak{m}}|\rangle$
by Lemma 70 , where
$|{\mathfrak{m}}|\in\blacktriangle(x).|({\mathbf{N}}^{\perp})^{x}|$ by Theorem
8, hence $|{\mathfrak{m}}|$ is of the form
$|{\mathfrak{m}}|=\blacktriangle(x).{\mathfrak{p}}^{x}$ with
${\mathfrak{p}}\in{\mathbf{N}}^{\perp}$. By definition
$\langle{\mathfrak{q}}\leftarrow|{\mathfrak{m}}|\rangle=\kappa_{\blacktriangledown}\langle{\mathfrak{n}}^{x}\leftarrow{\mathfrak{p}}^{x}\rangle$,
where $\langle{\mathfrak{n}}^{x}\leftarrow{\mathfrak{p}}^{x}\rangle\in
V_{{\mathbf{N}}}^{x}$.

$(\supseteq)$ Indeed $\maltese\in V_{{\mathbf{\shpos N}}}$. Now let
$\mathpzc{s}\in\kappa_{\blacktriangledown}V_{{\mathbf{N}}}^{x}$. There exist
${\mathfrak{n}}\in{\mathbf{N}}$ and ${\mathfrak{p}}\in{\mathbf{N}}^{\perp}$
such that
$\mathpzc{s}=\kappa_{\blacktriangledown}\langle{\mathfrak{n}}^{x}\leftarrow{\mathfrak{p}}^{x}\rangle$.
Note that
$\blacktriangledown\langle{\mathfrak{n}}\rangle\in\blacktriangledown\langle{\mathbf{N}}\rangle$
and
$\blacktriangle(x).{\mathfrak{p}}^{x}\in\blacktriangle(x).({\mathbf{N}}^{\perp})^{x}$.
By Lemma 77, $\shneg{\mathbf{N}}^{\perp}=(\shpos{\mathbf{N}})^{\perp}$, hence
$\blacktriangledown\langle{\mathfrak{n}}\rangle\perp\blacktriangle(x).{\mathfrak{p}}^{x}$.
Moreover
$\langle\blacktriangledown\langle{\mathfrak{n}}\rangle\leftarrow\blacktriangle(x).{\mathfrak{p}}^{x}\rangle=\kappa_{\blacktriangledown}\langle{\mathfrak{n}}^{x}\leftarrow{\mathfrak{p}}^{x}\rangle=\mathpzc{s}$,
therefore $\mathpzc{s}\in V_{{\mathbf{\shpos N}}}$.

  2. 2.

By Lemma 77 and previous item, and remarking that
$V_{{\mathbf{B}}}=\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}}}}}}$}}$
for every behaviour ${\mathbf{B}}$, we have: $V_{{\mathbf{\shneg
P}}}=\makebox[22.82225pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{22.82225pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{(\shneg
P)^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{22.82225pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{(\shneg
P)^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{22.82225pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{(\shneg
P)^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{22.82225pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{(\shneg
P)^{\perp}}}}}}$}}=\makebox[18.46667pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{18.46667pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{\shpos
P^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{18.46667pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{\shpos
P^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{18.46667pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{\shpos
P^{\perp}}}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{18.46667pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{\shpos
P^{\perp}}}}}}$}}=\makebox[56.85059pt][c]{\mbox{\rule{0.0pt}{8.03886pt}$\mathchoice{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{56.85059pt}{0.0pt}{$\sim$}$}\hss}{(\kappa_{\blacktriangledown}V_{{\mathbf{P^{\perp}}}}^{x}\cup\\{\maltese\\})}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{56.85059pt}{0.0pt}{$\sim$}$}\hss}{(\kappa_{\blacktriangledown}V_{{\mathbf{P^{\perp}}}}^{x}\cup\\{\maltese\\})}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{56.85059pt}{0.0pt}{$\sim$}$}\hss}{(\kappa_{\blacktriangledown}V_{{\mathbf{P^{\perp}}}}^{x}\cup\\{\maltese\\})}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{56.85059pt}{0.0pt}{$\sim$}$}\hss}{(\kappa_{\blacktriangledown}V_{{\mathbf{P^{\perp}}}}^{x}\cup\\{\maltese\\})}}$}}=\kappa_{\blacktriangle}\makebox[14.26668pt][c]{\mbox{\rule{0.0pt}{8.03886pt}$\mathchoice{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{14.26668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P^{\perp}}}}^{x}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{14.26668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P^{\perp}}}}^{x}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{14.26668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P^{\perp}}}}^{x}}}{\hbox
to0.0pt{\raisebox{8.03886pt}{$\leavevmode\resizebox{14.26668pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{P^{\perp}}}}^{x}}}$}}\cup\\{\epsilon\\}=\kappa_{\blacktriangle}V_{{\mathbf{P}}}^{x}\cup\\{\epsilon\\}$.

∎

####  B.2.2 Plus

######  Proposition 79.

$V_{{\mathbf{M\oplus
N}}}=\kappa_{\iota_{1}}V_{{\mathbf{M}}}^{x_{1}}\cup\kappa_{\iota_{2}}V_{{\mathbf{N}}}^{x_{2}}\cup\\{\maltese\\}$

###### Proof.

Remark that
${\mathbf{M}}\oplus{\mathbf{N}}=(\iota_{1}\langle{\mathbf{M}}\rangle\cup\\{\maltese\\})\cup(\iota_{2}\langle{\mathbf{N}}\rangle\cup\\{\maltese\\})$
is the union of behaviours $\oplus_{1}{\mathbf{M}}$ and
$\oplus_{2}{\mathbf{N}}$, which correspond respectively to
$\shpos{\mathbf{M}}$ and $\shpos{\mathbf{N}}$ with a different name for the
first action. Moreover,
$({\mathbf{M}}\oplus{\mathbf{N}})^{\perp}=\\{{\mathfrak{n}}\leavevmode\nobreak\
\boldsymbol{|}\leavevmode\nobreak\
\mathinner{\mathchoice{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\pi_{1}}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\pi_{1}}{{\mathfrak{n}}\mkern
1.0mu\upharpoonright\mkern
1.0mu\pi_{1}}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\pi_{1}}}\in\pi_{1}(x).({\mathbf{M}}^{\perp})^{x}\mbox{
and
}\mathinner{\mathchoice{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\pi_{2}}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\pi_{2}}{{\mathfrak{n}}\mkern
1.0mu\upharpoonright\mkern
1.0mu\pi_{2}}{{\mathfrak{n}}\\!\\!\upharpoonright\\!\\!\pi_{2}}}\in\pi_{2}(x).({\mathbf{N}}^{\perp})^{x}\\}=(\with_{1}{\mathbf{M}}^{\perp})\cap(\with_{2}{\mathbf{N}}^{\perp})$,
where the behaviours $\with_{1}{\mathbf{M}}^{\perp}$ and
$\with_{2}{\mathbf{N}}^{\perp}$ correspond to $\shneg{\mathbf{M}}^{\perp}$ and
$\shneg{\mathbf{N}}^{\perp}$ with different names; note also that for every
${\mathfrak{d}}\in|\with_{1}{\mathbf{M}}^{\perp}|$ (resp.
$|\with_{2}{\mathbf{N}}^{\perp}|$) there exists
${\mathfrak{d}}^{\prime}\in({\mathbf{M}}\oplus{\mathbf{N}})^{\perp}$ such that
${\mathfrak{d}}\sqsubseteq{\mathfrak{d}}^{\prime}$, in other words such that
${\mathfrak{d}}=|{\mathfrak{d}}^{\prime}|_{\with_{1}{\mathbf{M}}^{\perp}}$
(resp. $|{\mathfrak{d}}^{\prime}|_{\with_{2}{\mathbf{N}}^{\perp}}$). Therefore
the proof can be conducted similarly to the one of Proposition 78(1). ∎

####  B.2.3 Tensor and Linear Map

The following proposition is a joint work with Fouqueré and Quatrini; in [9],
they prove a similar result in the framework of original Ludics.

######  Proposition 80.

$\mathpzc{s}\in V_{{\mathbf{M\otimes N}}}$ if and only if the two conditions
below are satisfied:

  1. 1.

$\mathpzc{s}\in\kappa_{\bullet}(V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y})\cup\\{\maltese\\}$,

  2. 2.

for all $\mathpzc{t}\in V_{{\mathbf{M}}}^{x}\shuffle V_{{\mathbf{N}}}^{y}$,
for all $\kappa^{-}$ such that
$\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}$,
$\mathpzc{t}\kappa^{-}\maltese\in V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y}$.

The proof of this proposition uses some material on multi-designs introduced
in Section A. Note also that for all negative designs ${\mathfrak{m}}$ and
${\mathfrak{n}}$, we will write ${\mathfrak{m}}\otimes{\mathfrak{n}}$ instead
of $x_{0}|\bullet\langle{\mathfrak{m}},{\mathfrak{n}}\rangle$.

###### Proof.

$(\Rightarrow)$ Let $\mathpzc{s}\in V_{{\mathbf{M\otimes N}}}$. If
$\mathpzc{s}=\maltese$ then both conditions are trivial, so suppose
$\mathpzc{s}\neq\maltese$. By internal completeness (Theorem 8), there exist
${\mathfrak{m}}\in{\mathbf{M}}$, ${\mathfrak{n}}\in{\mathbf{N}}$ and
${\mathfrak{n}}_{0}\in({\mathbf{M}}\otimes{\mathbf{N}})^{\perp}$ such that
$\mathpzc{s}=\langle{\mathfrak{m}}\otimes{\mathfrak{n}}\leftarrow{\mathfrak{n}}_{0}\rangle$.
Thus ${\mathfrak{n}}_{0}$ must be of the form
${\mathfrak{n}}_{0}=\sum_{a\in\mathcal{S}}a(\overrightarrow{z^{a}}).{\mathfrak{p}}_{a}$
with ${\mathfrak{p}}_{\wp}\neq\Omega$ (remember that
$\bullet=\overline{\wp}$), and we have
$\mathpzc{s}=\kappa_{\bullet}\mathpzc{s}^{\prime}$ where
$\mathpzc{s}^{\prime}=\langle\\{{\mathfrak{m}}^{x},{\mathfrak{n}}^{y}\\}\leftarrow\\{{\mathfrak{p}}_{\wp},{\mathfrak{n}}_{0}/x_{0}\\}\rangle=\langle\\{{\mathfrak{m}}^{x},{\mathfrak{n}}^{y}\\}\leftarrow{\mathfrak{p}}_{\wp}\rangle$.
Let us prove both properties:

  1. 1.

By Proposition 66,
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{m}}^{x}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}}=\langle{\mathfrak{m}}^{x}\leftarrow(\\![{\mathfrak{p}}_{\wp}[{\mathfrak{n}}/y]]\\!)\rangle$,
where ${\mathfrak{m}}^{x}\in{\mathbf{M}}^{x}$. Moreover,
$(\\![{\mathfrak{p}}_{\wp}[{\mathfrak{n}}/y]]\\!)\in{\mathbf{M}}^{x\perp}$,
indeed: for any ${\mathfrak{m}}^{\prime}\in{\mathbf{M}}$, we have
$(\\![(\\![{\mathfrak{p}}_{\wp}[{\mathfrak{n}}/y]]\\!)[{\mathfrak{m}}^{\prime}/x]]\\!)=(\\![{\mathfrak{p}}_{\wp}[{\mathfrak{n}}/y,{\mathfrak{m}}^{\prime}/x]]\\!)=(\\![({\mathfrak{m}}^{\prime}\otimes{\mathfrak{n}})[{\mathfrak{n}}_{0}/x_{0}]]\\!)=\maltese$
using associativity and one reduction step backwards. Thus
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{m}}^{x}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}}\in
V_{{\mathbf{M}}}^{x}$. Likewise,
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{n}}^{y}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{n}}^{y}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{n}}^{y}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{n}}^{y}}}=\langle{\mathfrak{n}}^{y}\leftarrow(\\![{\mathfrak{p}}_{\wp}[{\mathfrak{m}}/x]]\\!)\rangle$,
so
$\mathinner{\mathchoice{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{n}}^{y}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{n}}^{y}}{\mathpzc{s}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{n}}^{y}}{\mathpzc{s}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{n}}^{y}}}\in
V_{{\mathbf{N}}}^{y}$. Therefore
$\mathpzc{s}^{\prime}\in(V_{{\mathbf{M}}}^{x}\shuffle V_{{\mathbf{N}}}^{y})$.

  2. 2.

Now let $\mathpzc{t}_{1}\in V_{{\mathbf{M}}}^{x},\mathpzc{t}_{2}\in
V_{{\mathbf{N}}}^{y}$. Suppose
$\mathpzc{t}\in(\mathpzc{t}_{1}\shuffle\mathpzc{t}_{2})$ and $\kappa^{-}$ is a
negative action such that $\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}$.
Without loss of generality, suppose moreover that the action $\kappa^{-}$
comes from ${\mathfrak{m}}^{x}$, and let us show that
$\mathpzc{t}_{1}\kappa^{-}\maltese\in V_{{\mathbf{M}}}^{x}$.

Let
$\mathpzc{t}^{\prime}=\langle\\{\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}/x,\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{2}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}/y\\}\leftarrow\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\rangle$.
We will show that $\mathpzc{t}_{1}\kappa^{-}$ is a prefix of
$\mathinner{\mathchoice{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}}$
and that
$\mathinner{\mathchoice{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}}\in
V_{{\mathbf{M}}}^{x}$, leading to the conclusion by Lemma 71. Note the
following facts:

    1. (a)

$\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}=\wp(x,y).\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}+\sum_{a\neq\wp}a(\overrightarrow{z^{a}}).\maltese$,
and thus
$\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\neq\maltese$
(otherwise a path of the form
$\overline{\kappa_{\bullet}\mathpzc{t}\kappa^{-}}$ cannot be 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}$).

    2. (b)

$\mathpzc{t}$ is a path of the multi-design
$\\{\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}/x,\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{2}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}/y\\}$,
and $\overline{\mathpzc{t}}$ is a prefix of a path of
$\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$
since $\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}$,
thus $\mathpzc{t}$ is a prefix of $\mathpzc{t}^{\prime}$ by Proposition 62.

    3. (c)

Since $\mathpzc{t}$ is a $\maltese$-free positive-ended prefix of
$\mathpzc{t}^{\prime}$, we have that $\overline{\kappa_{\bullet}\mathpzc{t}}$
is a strict prefix of $\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{13.99048pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{13.99048pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{13.99048pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{13.99048pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}^{\prime}}}$.
Thus there exists a positive action $\kappa_{0}^{+}$ such that
$\overline{\kappa_{\bullet}\mathpzc{t}}\kappa_{0}^{+}$ is a prefix of
$\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{13.99048pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{13.99048pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{13.99048pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{13.99048pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{\bullet}\mathpzc{t}^{\prime}}}$.
The paths $\overline{\kappa_{\bullet}\mathpzc{t}\kappa^{-}}$ and
$\overline{\kappa_{\bullet}\mathpzc{t}}\kappa^{+}_{0}$ are both paths 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}$,
hence necessarily $\kappa^{+}_{0}=\overline{\kappa^{-}}$. We deduce that
$\mathpzc{t}\kappa^{-}$ is a prefix of $\mathpzc{t}^{\prime}$.

    4. (d)

The sequence
$\mathinner{\mathchoice{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}}$
therefore starts with
$\mathinner{\mathchoice{(\mathpzc{t}\kappa^{-})\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{(\mathpzc{t}\kappa^{-})\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{(\mathpzc{t}\kappa^{-})\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{(\mathpzc{t}\kappa^{-})\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}}$.

    5. (e)

We have
$\mathinner{\mathchoice{(\mathpzc{t}\kappa^{-})\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{(\mathpzc{t}\kappa^{-})\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{(\mathpzc{t}\kappa^{-})\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{(\mathpzc{t}\kappa^{-})\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}}=(\mathinner{\mathchoice{\mathpzc{t}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}})\kappa^{-}$
because, since $\kappa^{-}$ comes from ${\mathfrak{m}}^{x}$, it is
hereditarily justified by an initial negative action of address $x$, and thus
$\kappa^{-}$ appears in design
$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$.
We deduce
$\mathinner{\mathchoice{(\mathpzc{t}\kappa^{-})\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{(\mathpzc{t}\kappa^{-})\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{(\mathpzc{t}\kappa^{-})\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{(\mathpzc{t}\kappa^{-})\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}}=(\mathinner{\mathchoice{\mathpzc{t}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}})\kappa^{-}=\mathpzc{t}_{1}\kappa^{-}$.

    6. (f)

Moreover, by Proposition 66
$\mathinner{\mathchoice{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}}=\langle\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\leftarrow(\\![\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}[\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{2}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}/y]]\\!)\rangle$.

Hence (by d, e, f) the sequence $\mathpzc{t}_{1}\kappa^{-}$ is a prefix of
$\mathinner{\mathchoice{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}}=\langle\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\leftarrow(\\![\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}[\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{2}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}/y]]\\!)\rangle$.
Since
$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\in{\mathbf{M}}^{x}$
(by Proposition 69) and
$(\\![\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}[\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{2}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}/y]]\\!)\in{\mathbf{M}}^{x\perp}$
(by associativity, similar reasoning as item $1$), we deduce
$\mathinner{\mathchoice{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{t}_{1}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}}}\in
V_{{\mathbf{M}}}^{x}$. Finally $\mathpzc{t}_{1}\kappa^{-}\maltese\in
V_{{\mathbf{M}}}^{x}$ by Lemma 71.

$(\Leftarrow)$ Let
$\mathpzc{s}\in\kappa_{\bullet}(V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y})\cup\\{\maltese\\}$ such that the second constraint is
also satisfied. If $\mathpzc{s}=\maltese$ then $\mathpzc{s}\in
V_{{\mathbf{M\otimes N}}}$ is immediate, so suppose
$\mathpzc{s}=\kappa_{\bullet}\mathpzc{s}^{\prime}$ where
$\mathpzc{s}^{\prime}\in(V_{{\mathbf{M}}}^{x}\shuffle V_{{\mathbf{N}}}^{y})$.
Consider the design
$\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}$,
and note that
$\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}=\wp(x,y).\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}+\sum_{a\neq\wp}a(\overrightarrow{z^{a}}).\maltese$.
We will show by contradiction that
$\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}\in({\mathbf{M}}\otimes{\mathbf{N}})^{\perp}$,
leading to the conclusion.

Let ${\mathfrak{m}}\in{\mathbf{M}}$ and ${\mathfrak{n}}\in{\mathbf{N}}$ such
that
${\mathfrak{m}}\otimes{\mathfrak{n}}\not\perp\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}$.
By Proposition 64 and given the form of design
$\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}$,
the interaction with ${\mathfrak{m}}\otimes{\mathfrak{n}}$ is finite and the
cause of divergence is necessarily the existence of a path $\mathpzc{t}$ and
an action $\kappa^{-}$ such that:

  1. 1.

$\mathpzc{t}$ is a path of ${\mathfrak{m}}\otimes{\mathfrak{n}}$,

  2. 2.

$\overline{\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}$

  3. 3.

$\mathpzc{t}\kappa^{-}$ is not a path of
${\mathfrak{m}}\otimes{\mathfrak{n}}$.

Hence $\mathpzc{t}$ is of the form
$\mathpzc{t}=\kappa_{\bullet}\mathpzc{t}^{\prime}$. Choose ${\mathfrak{m}}$
and ${\mathfrak{n}}$ such that $\mathpzc{t}$ is of minimal length with respect
to all such pairs of designs non orthogonal to
$\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}$.
Let
$\mathpzc{t}_{1}=\mathinner{\mathchoice{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}{\mathpzc{t}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{m}}^{x}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}}$
and
$\mathpzc{t}_{2}=\mathinner{\mathchoice{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{n}}^{y}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{n}}^{y}}{\mathpzc{t}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{n}}^{y}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{n}}^{y}}}$,
we have
$\mathpzc{t}\in\kappa_{\bullet}(\mathpzc{t}_{1}\shuffle\mathpzc{t}_{2})$.
Consider the design
$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$,
and note that
$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}=\wp(x,y).\raisebox{2.78395pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.4289pt][c]{\mbox{\rule{0.0pt}{7.70634pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}$}}}\raisebox{2.78395pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}+\sum_{a\neq\wp}a(\overrightarrow{z^{a}}).\maltese$.
We prove the following:

  * •

$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\in({\mathbf{M}}\otimes{\mathbf{N}})^{\perp}$:
By contradiction. Let ${\mathfrak{m}}^{\prime}\in{\mathbf{M}}$ and
${\mathfrak{n}}^{\prime}\in{\mathbf{N}}$ such that
${\mathfrak{m}}^{\prime}\otimes{\mathfrak{n}}^{\prime}\not\perp\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$.
Again using Proposition 64, divergence occurs necessarily because there exists
a path $\mathpzc{v}$ and a negative action $\kappa^{\prime-}$ such that:

    1. 1.

$\mathpzc{v}$ is a path of
${\mathfrak{m}}^{\prime}\otimes{\mathfrak{n}}^{\prime}$,

    2. 2.

$\overline{\mathpzc{v}\kappa^{\prime-}}$ is a path of
$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$,

    3. 3.

$\mathpzc{v}\kappa^{\prime-}$ is not a path of
${\mathfrak{m}}^{\prime}\otimes{\mathfrak{n}}^{\prime}$.

Since the views of $\overline{\mathpzc{v}\kappa^{\prime-}}$ are views of
$\overline{\mathpzc{t}}$, $\overline{\mathpzc{v}\kappa^{\prime-}}$ 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}$.
Thus
${\mathfrak{m}}^{\prime}\otimes{\mathfrak{n}}^{\prime}\not\perp\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}$.
Moreover $\mathpzc{v}$ is strictly shorter than $\mathpzc{t}$, indeed:
$\mathpzc{v}$ and $\mathpzc{t}$ are $\maltese$-free, and since
$\overline{\mathpzc{v}\kappa^{\prime-}}$ is a path of
$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$
any action of $\mathpzc{v}\kappa^{\prime-}$ is an action of $\mathpzc{t}$.
This contradicts the fact that $\mathpzc{t}$ is of minimum length. We deduce
$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\in({\mathbf{M}}\otimes{\mathbf{N}})^{\perp}$.

  * •

$\mathpzc{t}\in\kappa_{\bullet}(V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y})$: We show $\mathpzc{t}_{1}\in V_{{\mathbf{M}}}^{x}$, the
proof of $\mathpzc{t}_{2}\in V_{{\mathbf{N}}}^{y}$ being similar. Since
$\mathpzc{t}$ is a path of ${\mathfrak{m}}\otimes{\mathfrak{n}}$ and
$\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}}}$
a path of
$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$,
we have
$\mathpzc{t}=\langle{\mathfrak{m}}\otimes{\mathfrak{n}}\leftarrow\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\rangle=\kappa_{\bullet}\langle\\{{\mathfrak{m}}^{x},{\mathfrak{n}}^{y}\\}\leftarrow\raisebox{2.78395pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.4289pt][c]{\mbox{\rule{0.0pt}{7.70634pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}$}}}\raisebox{2.78395pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\rangle$,
hence
$\mathpzc{t}^{\prime}=\langle\\{{\mathfrak{m}}^{x},{\mathfrak{n}}^{y}\\}\leftarrow\raisebox{2.78395pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.4289pt][c]{\mbox{\rule{0.0pt}{7.70634pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}$}}}\raisebox{2.78395pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\rangle$.
Thus by Proposition 66
$\mathpzc{t}_{1}=\mathinner{\mathchoice{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}{\mathpzc{t}^{\prime}\mkern
1.0mu\upharpoonright\mkern
1.0mu{\mathfrak{m}}^{x}}{\mathpzc{t}^{\prime}\\!\\!\upharpoonright\\!\\!{\mathfrak{m}}^{x}}}=\langle{\mathfrak{m}}^{x}\leftarrow(\\![\raisebox{2.78395pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.4289pt][c]{\mbox{\rule{0.0pt}{7.70634pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}$}}}\raisebox{2.78395pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}[{\mathfrak{n}}/y]]\\!)\rangle$.
Moreover
$(\\![\raisebox{2.78395pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.4289pt][c]{\mbox{\rule{0.0pt}{7.70634pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}$}}}\raisebox{2.78395pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}[{\mathfrak{n}}/y]]\\!)\in{\mathbf{M}}^{x\perp}$:
for any design ${\mathfrak{m}}^{\prime}\in{\mathbf{M}}$ we have
$(\\![\raisebox{2.78395pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.4289pt][c]{\mbox{\rule{0.0pt}{7.70634pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}$}}}\raisebox{2.78395pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}[{\mathfrak{n}}/y]]\\!)\perp{\mathfrak{m}}^{\prime
x}$ because of the equality
$(\\![(\\![\raisebox{2.78395pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.4289pt][c]{\mbox{\rule{0.0pt}{7.70634pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}$}}}\raisebox{2.78395pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}[{\mathfrak{n}}/y]]\\!)[{\mathfrak{m}}^{\prime}/x]]\\!)=(\\![\raisebox{2.78395pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.4289pt][c]{\mbox{\rule{0.0pt}{7.70634pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}{\hbox
to0.0pt{\raisebox{7.70634pt}{$\leavevmode\resizebox{5.4289pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{t}^{\prime}}}$}}}\raisebox{2.78395pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}[{\mathfrak{n}}/y,{\mathfrak{m}}^{\prime}/x]]\\!)=(\\![({\mathfrak{m}}^{\prime}\otimes{\mathfrak{n}})[\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}/x_{0}]]\\!)=\maltese$,
using associativity, one reduction step backwards, and the fact that
$\raisebox{1.2284pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\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}}}$}}}\raisebox{1.2284pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\in({\mathbf{M}}\otimes{\mathbf{N}})^{\perp}$.
It follows that $\mathpzc{t}_{1}\in V_{{\mathbf{M}}}^{x}$.

  * •

$\mathpzc{t}\kappa^{-}$ is a path of ${\mathfrak{m}}\otimes{\mathfrak{n}}$:
Remember that $\overline{\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}$,
and we have just seen that
$\mathpzc{t}\in\kappa_{\bullet}(V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y})$. Using the second constraint of the proposition, we
should have $\mathpzc{t}_{1}\kappa^{-}\maltese\in V_{{\mathbf{M}}}^{x}$ or
$\mathpzc{t}_{2}\kappa^{-}\maltese\in V_{{\mathbf{N}}}^{y}$. Without loss of
generality suppose $\mathpzc{t}_{1}\kappa^{-}\maltese\in
V_{{\mathbf{M}}}^{x}$. Since ${\mathfrak{m}}^{x}\in{\mathbf{M}}^{x}$ and
$\mathpzc{t}_{1}$ is a path of ${\mathfrak{m}}^{x}$, we should also have that
$\mathpzc{t}_{1}\kappa^{-}$ is a prefix of a path of ${\mathfrak{m}}^{x}$ by
Lemma 72, hence
$\raisebox{2.78395pt}{$\ulcorner$}{\mathpzc{t}^{\prime}\kappa^{-}}\raisebox{2.78395pt}{$\urcorner$}=\raisebox{1.2284pt}{$\ulcorner$}{\mathpzc{t}_{1}\kappa^{-}}\raisebox{1.2284pt}{$\urcorner$}$
is a view of ${\mathfrak{m}}^{x}$. But in this case, knowing that
$\mathpzc{t}$ is a path of ${\mathfrak{m}}\otimes{\mathfrak{n}}$ and that
$\raisebox{1.2284pt}{$\ulcorner$}{\mathpzc{t}\kappa^{-}}\raisebox{1.2284pt}{$\urcorner$}=\kappa_{\bullet}\raisebox{2.78395pt}{$\ulcorner$}{\mathpzc{t}^{\prime}\kappa^{-}}\raisebox{2.78395pt}{$\urcorner$}$
is a view of ${\mathfrak{m}}\otimes{\mathfrak{n}}$, we deduce that
$\mathpzc{t}\kappa^{-}$ is a path of ${\mathfrak{m}}\otimes{\mathfrak{n}}$.

Last point contradicts the cause of divergence between
${\mathfrak{m}}\otimes{\mathfrak{n}}$ and
$\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}$.
Hence
$\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}\in({\mathbf{M}}\otimes{\mathbf{N}})^{\perp}$.
Moreover, $\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 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}$,
and since $\mathpzc{s}\in\kappa_{\bullet}(V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y})$ there exist ${\mathfrak{m}}_{0}\in{\mathbf{M}}$ and
${\mathfrak{n}}_{0}\in{\mathbf{N}}$ such that $\mathpzc{s}$ is a path of
${\mathfrak{m}}_{0}\otimes{\mathfrak{n}}_{0}$ (and
${\mathfrak{m}}_{0}\otimes{\mathfrak{n}}_{0}\in{\mathbf{M}}\otimes{\mathbf{N}}$).
We deduce
$\mathpzc{s}=\langle{\mathfrak{m}}_{0}\otimes{\mathfrak{n}}_{0}\leftarrow\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}\rangle$,
hence $\mathpzc{s}\in V_{{\mathbf{M\otimes N}}}$. ∎

######  Corollary 81.

$\mathpzc{s}\in V_{{\mathbf{N\multimap P}}}$ if and only if the two conditions
below are satisfied:

  1. 1.

$\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\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\\}$

  2. 2.

for all $\mathpzc{t}\in
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}}}$}}$,
for all $\kappa^{-}$ such that
$\overline{\kappa_{\bullet}\mathpzc{t}\kappa^{-}}$ is a path of
$\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}$,
$\mathpzc{t}\kappa^{-}\maltese\in
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}}}$}}$.

####  B.2.4 Tensor and Linear Map, Regular Case

######  Proposition 82.

If ${\mathbf{M}}$ and ${\mathbf{N}}$ regular then $V_{{\mathbf{M\otimes
N}}}=\kappa_{\bullet}(V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y})\cup\\{\maltese\\}$.

###### Proof.

Suppose ${\mathbf{M}}$ and ${\mathbf{N}}$ regular. Following Proposition 80,
it suffices to show that any path
$\mathpzc{s}\in\kappa_{\bullet}(V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y})\cup\\{\maltese\\}$ satisfies the following condition:
for all $\mathpzc{t}\in V_{{\mathbf{M}}}^{x}\shuffle V_{{\mathbf{N}}}^{y}$,
for all negative action $\kappa^{-}$ such that
$\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}$,
$\mathpzc{t}\kappa^{-}\maltese\in V_{{\mathbf{M}}}^{x}\shuffle
V_{{\mathbf{N}}}^{y}$.

If $\mathpzc{s}=\maltese$, there is nothing to prove, so suppose
$\mathpzc{s}=\kappa_{\bullet}\mathpzc{s}^{\prime}$ where
$\mathpzc{s}^{\prime}\in V_{{\mathbf{M}}}^{x}\shuffle V_{{\mathbf{N}}}^{y}$.
Let $\mathpzc{t}\in V_{{\mathbf{M}}}^{x}\shuffle V_{{\mathbf{N}}}^{y}$ and
$\kappa^{-}$ be such that $\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}$,
that is $\overline{\mathpzc{t}\kappa^{-}}$ is a path of
$\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$.
Let $\mathpzc{s}_{1},\mathpzc{t}_{1}\in V_{{\mathbf{M}}}^{x}$ and
$\mathpzc{s}_{2},\mathpzc{t}_{2}\in V_{{\mathbf{N}}}^{y}$ such that
$\mathpzc{s}^{\prime}\in\mathpzc{s}_{1}\shuffle\mathpzc{s}_{2}$ and
$\mathpzc{t}\in\mathpzc{t}_{1}\shuffle\mathpzc{t}_{2}$. Without loss of
generality, suppose $\kappa^{-}$ is an action in $\mathpzc{s}_{1}$, thus we
must show $\mathpzc{t}_{1}\kappa^{-}\maltese\in V_{{\mathbf{M}}}^{x}$. Notice
that
$\langle\mathpzc{t}_{1}\kappa^{-}\rangle=\langle\mathpzc{t}\kappa^{-}\rangle=\langle\kappa^{-}\rangle_{\mathpzc{s}^{\prime}}=\langle\kappa^{-}\rangle_{\mathpzc{s}_{1}}$
(the second equality follows from the fact that
$\overline{\mathpzc{t}\kappa^{-}}$ is a path of
$\raisebox{0.9387pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\,\makebox[5.48444pt][c]{\mbox{\rule{0.0pt}{5.8611pt}$\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.48444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}^{\prime}}}$}}\,}\raisebox{0.9387pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$).
Since $\mathpzc{s}_{1}\in V_{{\mathbf{M}}}^{x}$, the sequence
$\langle\kappa^{-}\rangle_{\mathpzc{s}_{1}}=\langle\mathpzc{t}_{1}\kappa^{-}\rangle$
is a trivial view of ${\mathbf{M}}^{x}$. Let
$\mathpzc{s}_{1}^{\prime}\kappa^{-}$ be the prefix of $\mathpzc{s}_{1}$ ending
with $\kappa^{-}$. By Lemma 71 $\mathpzc{s}_{1}^{\prime}\kappa^{-}\maltese\in
V_{{\mathbf{M}}}^{x}$, so
$\langle\mathpzc{t}_{1}\kappa^{-}\maltese\rangle=\langle\mathpzc{s}^{\prime}_{1}\kappa^{-}\maltese\rangle$
is also a trivial view of ${\mathbf{M}}^{x}$; by regularity of ${\mathbf{M}}$,
we deduce $\langle\mathpzc{t}_{1}\kappa^{-}\maltese\rangle\in
V_{{\mathbf{M}}}^{x}$. We have
$\mathpzc{t}_{1}\kappa^{-}\maltese\in\mathpzc{t}_{1}\shuffle\langle\mathpzc{t}_{1}\kappa^{-}\maltese\rangle$,
where both $\mathpzc{t}_{1}$ and
$\langle\mathpzc{t}_{1}\kappa^{-}\maltese\rangle$ are in
$V_{{\mathbf{M}}}^{x}$, hence $\mathpzc{t}_{1}\kappa^{-}\maltese\in
V_{{\mathbf{M}}}^{x}$ by regularity of ${\mathbf{M}}$. ∎

######  Corollary 83.

If ${\mathbf{N}}$ and ${\mathbf{P}}$ are regular then $V_{{\mathbf{N\multimap
P}}}=\makebox[49.53105pt][c]{\mbox{\rule{0.0pt}{7.5pt}$\mathchoice{\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}}}}}$}})}}{\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}}}}}$}})}}{\hbox