# Ludics Characterization of Multiplicative-Additive Linear Behaviours

Christophe Fouqueré Université Paris 13, Sorbonne Paris Cité, LIPN, F–93430,
Villetaneuse, France
CNRS, UMR 7030, F–93430, Villetaneuse, France<EMAIL_ADDRESS>paris13.fr Myriam Quatrini IML –FRE 35-29, Université Aix-Marseille & CNRS,
F–13284 Marseille Cedex 07, France<EMAIL_ADDRESS>
###### Abstract

Ludics is a logical theory that J.-Y. Girard developed around $2000$. At first
glance, it may be considered as a Brouwer-Heyting-Kolmogorov interpretation of
Logic as a formula is denoted by the set of its proofs. More primitively,
Ludics is a theory of interaction that models (a variant of) second-order
multiplicative-additive Linear Logic. A formula is denoted by a set of objects
called a behaviour, a proof by an object that satisfies some criteria. Our aim
is to analyze the structure of behaviours in order to better understand and
refine the usual notion of formulas or types. More precisely, we study
properties that guarantee a behaviour to be recursively decomposable by means
of multiplicative-additive linear connectives and linear constants.111This
work has been partially funded by the French ANR projet blanc “Locativity and
Geometry of Interaction” LOGOI ANR-10-BLAN-0213 02.

##  1 Introduction

Ludics is a logical theory that J.-Y. Girard developed around $2000$. At first
glance, it may be considered as a Brouwer-Heyting-Kolmogorov interpretation of
Logic as a formula is denoted by the set of its proofs. More primitively,
Ludics is a theory of interaction, where interaction is the fact that a
meeting happens between two objects together with the dynamical process that
this meeting creates. This notion is primitive in the sense that the main
objects of Ludics, called designs, are defined with respect to interaction:
they are objects between which meetings may happen and on which rewriting
processes may be described. Hence, among the computational theoretical and
methodological frameworks, Ludics is ontologically closer to Game Semantics
than to Proof Theory or Type Theory. Indeed, if interaction corresponds to cut
and cut-elimination in Proof Theory, and to application rule and normalization
in Type Theory, it presupposes more primitive notions fixed: formulas and
formal proofs in Proof Theory, types and terms in Type Theory. On the
opposite, the concept of play in Game Theory serves as a means for
interaction. However we should notice that, in Game Semantics, the definition
of a game is external to interaction, whereas in Ludics the corresponding
notion of behaviour is internal: it is a closure of a set of designs with
respect to interaction. In other words, Ludics may be considered as an untyped
computational theoretical framework, but with types subsequently recovered. In
[12], Terui showed that such a notion of interactive type may be applied with
success to the study of formal grammars. Our aim is to analyze the structure
of interactive types in order to better understand and refine the usual notion
of formulas or types. More precisely, we characterize in this paper behaviours
that correspond to (linear) logical formulas.

We give properties that guarantee a behaviour to be recursively decomposable
by means of multiplicative-additive linear connectives and linear constants.
First of all, essential finiteness (or uniform boundedness when infinite sums
are accepted) ensures that such a decomposition indeed terminates on
constants. Additive decomposition is immediate as it is already present in
Ludics. Multiplicative decomposition is a more complex problem to tackle. For
that purpose, two notions turn out to be fundamental: (1) incarnation, a
specific concept of Ludics, enables to characterize which part of a behaviour
is used during interaction, (2) the presentation of a design as a set of paths
instead of a set of chronicles as originally introduced by Girard. These
notions help also study the relation between Ludics and Game semantics [7, 8,
1]. In a previous work [9], the presentation of a design as a set of paths was
the key point that allows the authors to compute the incarnation of a set of
designs without computing the behaviour. To be able to fully characterize
behaviours that are linearly decomposable, we investigate two new notions:
visitability and regularity. A visitable path is a path that may be travelled
by interaction. A regular behaviour is such that its set of visitable paths is
exactly the set of positive-ended chronicles of its incarnation, stable by
shuffle and dual operations, where a shuffle of two paths is an interleaving
of actions that respects polarity. With that given, we prove the following
result:

${\mathbf{A}}\in\mathcal{C}_{\infty}$ iff ${\mathbf{A}}$ is a regular
uniformly bounded behaviour.

where
$\mathcal{C}_{\infty}=\mathcal{C}_{\infty}^{+}\cup\mathcal{C}_{\infty}^{-}$,
defined inductively in the following way:

$\begin{array}[]{ccc}\mathcal{C}_{\infty}^{+}\leavevmode\nobreak\
=\leavevmode\nobreak\ {\mathbf{0}}\leavevmode\nobreak\ |\leavevmode\nobreak\
{\mathbf{1}}\leavevmode\nobreak\ |\leavevmode\nobreak\
\bigoplus_{n\in[1,\infty]}(\bigotimes_{q\in[1,\infty[}\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}\mathcal{C}_{\infty}^{-})&&\mathcal{C}_{\infty}^{-}\leavevmode\nobreak\
=\leavevmode\nobreak\ \mathinner{\mkern
4.0mu\raise-0.3pt\hbox{$\top$}\mkern-14.5mu\hbox{$\top$}\mkern-14.5mu\raise
0.3pt\hbox{$\top$}\mkern 2.0mu}|\mathinner{\mkern
4.0mu\raise-0.3pt\hbox{$\bot$}\mkern-13.5mu\hbox{$\bot$}\mkern-13.5mu\raise
0.3pt\hbox{$\bot$}\mkern 2.0mu}|\leavevmode\nobreak\
\bigwith_{n\in[1,\infty]}(\bigparr_{q\in[1,\infty[}\mathinner{\mathchoice{\vbox{\hbox{$\shneg$}}}{\vbox{\hbox{$\shneg$}}}{\vbox{\hbox{$\shneg$}}}{\vbox{\hbox{$\shneg$}}}}\mathcal{C}_{\infty}^{+})\end{array}$

The paper is organized as follows. In section 2, we recall the main facts
concerning Ludics. In particular, we make explicit the equivalence between the
two presentations of a design, as set of paths versus set of chronicles. We
define what is a shuffle of paths. To our knowledge, the shuffle operation,
largely used in combinatorics and to study parallelism (see for example [6,
11]), appears in Logics only to study non-commutativity [2, 3]. We give a few
properties concerning orthogonality in terms of path travelling, introducing
visitable paths, i.e., paths that are visited by orthogonality. In section 3
additive and multiplicative operations on behaviours are studied with respect
to visitability. The main result is a characterization of a tensor of
behaviours mainly as a shuffle operation on paths. Section 4 is devoted to
prove our main theorem already stated above.

##  2 Ludics from Paths, Incarnation from Visitable Paths

###  2.1 Chronicles and Paths

The main objects of Ludics, the designs, are defined by Girard [10] in order
to be the support of interaction and of its dynamics. The interaction between
two designs occurs when their respective bases share a same address in dual
positions. The dynamic part of interaction is decomposed in elementary steps
called actions (moves in Game Semantics). The (dynamics of the) interaction
consists in following two dual alternate sequences of actions, one in each
design.

######  Definition 2.1 (Base, Action, Sequence)

  * •

A base $\beta$ is a non-empty finite set of sequents of pairwise disjoint
addresses: $\Gamma_{1}\vdash\Delta_{1}$, …, $\Gamma_{n}\vdash\Delta_{n}$ such
each $\Delta_{j}$ is a finite set of addresses, at most one $\Gamma_{i}$ may
be empty and the other $\Gamma_{i}$ contain each exactly one address. An
address is noted as a sequence of integers.

  * •

An action $\kappa$ is

    * –

either a triple: a polarity that may be positive ($+$) or negative ($-$); an
address $\xi$ that is the focus of $\kappa$; a finite set of integers
$\\{k_{1},\dots,k_{n}\\}$ called a ramification. When used in an interaction,
the action $\kappa$ creates the finite set of new addresses
$\\{\xi.k_{1},\dots,\xi.k_{n}\\}$ on which the interaction may continue. An
action with focus $\xi.k_{i}$ is said justified by $\kappa$.

    * –

or the positive action daimon denoted by ${\scriptstyle\maltese}$.

  * •

A sequence of actions $\mathpzc{s}$ is based on $\beta$ if each action of
$\mathpzc{s}$ is either justified by a previous action in $\mathpzc{s}$, or
has its focus in $\beta$, or is a daimon which should be, in this case, the
last action of $\mathpzc{s}$. An action $\kappa$ of $\mathpzc{s}$ is initial
when the focus of $\kappa$ is in $\beta$.

For ease of reading, one may put as superscript of an action its polarity:
$\kappa^{+}$ is a positive action whereas $\kappa^{-}$ is a negative action.

Two kinds of sequences of actions, paths and chronicles, may equivalently be
used to define designs. Roughly speaking, a path is an alternate sequence that
allows to recover the justification relation between actions, a chronicle is a
path with an additional constraints on the justification relation: a negative
action should be justified by the immediate previous action in the sequence.

######  Definition 2.2 (Path, Chronicle)

  * •

A path $\mathpzc{p}$ based on $\beta$ is a finite sequence of actions based on
$\beta$ such that

    * –

Alternation: The polarity of actions alternate between positive and negative.

    * –

Justification: A proper action is either justified, i.e., its focus is built
by one of the previous actions in the sequence, or it is called initial with a
focus in one of $\Gamma_{i}$ (resp. $\Delta_{i}$) if the action is negative
(resp. positive).

    * –

Negative jump: (There is no jump on positive action) Let $\mathpzc{q}\kappa$
be a subsequence of $\mathpzc{p}$,
\- If $\kappa$ is a positive proper action justified by a negative action
$\kappa^{\prime}$ then there is a sub-sequence
$\alpha_{0}^{+}\alpha_{0}^{-}\dots\alpha_{n}^{+}\alpha_{n}^{-}$ of
$\mathpzc{p}$ such that $\alpha_{0}^{+}=\kappa$,
$\alpha_{n}^{-}=\kappa^{\prime}$ and for all $i\in\\{0,\dots,n\\}$,
$\alpha_{i}^{+}$ is immediately preceded by $\alpha_{i}^{-}$ and
$\alpha^{-}_{i}$ is justified by $\alpha_{i+1}^{+}$ in $\mathpzc{p}$.
\- If $\kappa$ is an initial positive proper action then its focus belongs to
one $\Delta_{i}$ and either $\kappa$ is the first action of $\mathpzc{p}$ and
$\Gamma_{i}$ is empty, or $\kappa$ is immediately preceded in $\mathpzc{p}$ by
a negative action with a focus hereditarily justified by an element of
$\Gamma_{i}\cup\Delta_{i}$.

    * –

Linearity: Actions have distinct focuses.

    * –

Daimon: If present, a daimon ends the path. If it is the first action in
$\mathpzc{p}$ then one of $\Gamma_{i}$ is empty.

    * –

Totality: If there exists an empty $\Gamma_{i}$, then $\mathpzc{p}$ is non-
empty and begins either with ${\scriptstyle\maltese}$ or with a positive
action with a focus in $\Delta_{i}$.

  * •

A chronicle ${\mathfrak{c}}$ based on $\beta$ is a non-empty path such that
each non-initial negative action is justified by the immediate previous
(positive) action.

The polarity of a path is given by the polarity of its first action if the
path is not empty: a negative path is a path with a first action that is
negative. A positive-ended path is a path whose last action is positive.
Abusively, we may say that an empty path is also negative or positive, a
positive-ended path may be empty.

$\mathpzc{p}$$\kappa^{\prime-}$$\alpha_{n}^{-}$$\alpha_{n}^{+}$…$\alpha_{n-1}^{-}$……$\alpha_{i+1}^{+}$…$\alpha_{i}^{-}$$\alpha_{i}^{+}$……$\alpha_{1}^{+}$…$\alpha_{0}^{-}$$\alpha_{0}^{+}$$\kappa^{+}$

Figure 1: Path $\mathpzc{p}$: Constraint of negative jump between $\kappa^{+}$
justified by $\kappa^{\prime-}$

Note that the negative jump condition (see Fig.1) in the definition of a path
is satisfied as soon as each non-initial negative action is justified by the
immediate previous action, as it is the case with in the definition of a
chronicle. Furthermore, the sequence of actions induced in the negative jump
condition defines a chronicle. Such a sequence is a view of the path. In the
other direction, a set of chronicles may give rise to a path by shuffling the
chronicles.

######  Definition 2.3 (View)

Let $\mathpzc{s}$ be a sequence of actions based on $\beta$, the view
$\raisebox{1.29167pt}{$\ulcorner$}{\mathpzc{s}}\raisebox{1.29167pt}{$\urcorner$}$
is the subsequence of $\mathpzc{s}$ defined as follows:
\-
$\raisebox{1.29167pt}{$\ulcorner$}{\epsilon}\raisebox{1.29167pt}{$\urcorner$}=\epsilon$
where $\epsilon$ is the empty sequence;
\-
$\raisebox{1.29167pt}{$\ulcorner$}{\kappa}\raisebox{1.29167pt}{$\urcorner$}=\kappa$;
\-
$\raisebox{1.29167pt}{$\ulcorner$}{w\kappa^{+}}\raisebox{1.29167pt}{$\urcorner$}=\raisebox{1.29167pt}{$\ulcorner$}{w}\raisebox{1.29167pt}{$\urcorner$}\kappa^{+}$;
\-
$\raisebox{1.29167pt}{$\ulcorner$}{w\kappa^{-}}\raisebox{1.29167pt}{$\urcorner$}=\raisebox{1.29167pt}{$\ulcorner$}{w_{0}}\raisebox{1.29167pt}{$\urcorner$}\kappa^{-}$
where $w_{0}$ either is empty if $\kappa^{-}$ is initial or is the prefix of
$w$ ending with the positive action which justifies $\kappa^{-}$.

A path $\mathpzc{p}$ being given, we remark that
$\raisebox{1.29167pt}{$\ulcorner$}{\mathpzc{p}}\raisebox{1.29167pt}{$\urcorner$}$
is a chronicle. We may also notice that the negative jump condition on a
positive action $\kappa^{+}$ justified by a negative one $\kappa^{-}$ may be
rephrased as follows: let $\mathpzc{q}\kappa^{+}$ be the prefix of
$\mathpzc{p}$ ending on $\kappa^{+}$,
$\kappa^{-}\in\raisebox{1.29167pt}{$\ulcorner$}{\mathpzc{q}}\raisebox{1.29167pt}{$\urcorner$}$.

If we consider the set $\mathpzc{p}^{*}$ of all prefixes $\mathpzc{q}$ of a
path $\mathpzc{p}$, we obtain the set of chronicles
$\raisebox{1.29167pt}{$\ulcorner$}{\mathpzc{q}}\raisebox{1.29167pt}{$\urcorner$}$
induced by $\mathpzc{p}$, this set is denoted
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}^{*}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.
Conversely, it is possible to rebuild the path $\mathpzc{p}$ from the set of
chronicles
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}^{*}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.
The relevant operation to build paths from chronicles is the operation of
shuffle. The shuffle operation may more generally be defined on paths. The
standard shuffle operation consists in interleaving sequences keeping each
element and respecting order. We depart from this definition first by imposing
that alternate polarities should also be satisfied, second by taking care of
the daimon that should only appear at the end of a path.

######  Definition 2.4 (Shuffle of paths)

  * •

Let $\mathpzc{p}$ and $\mathpzc{q}$ be two positive-ended negative paths on
disjoint bases: $\beta$ and $\gamma$, and such that at least one path does not
end on a daimon. The shuffle of $\mathpzc{p}$ and $\mathpzc{q}$, noted
$\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}$,
is the set of sequences
$\mathpzc{p}_{1}\mathpzc{q}_{1}\dots\mathpzc{p}_{n}\mathpzc{q}_{n}$, based on
$\beta\cup\gamma$ such that:
\- each sequence $\mathpzc{p}_{i}$ and $\mathpzc{q}_{i}$ is either empty or a
positive-ended negative path,
\- $\mathpzc{p}_{1}\dots\mathpzc{p}_{n}=\mathpzc{p}$ and
$\mathpzc{q}_{1}\dots\mathpzc{q}_{n}=\mathpzc{q}$,
\- if $\mathpzc{p}_{n}$ ends with ${\scriptstyle\maltese}$ then
$\mathpzc{q}_{n}$ is empty.

  * •

The definition is extended to paths
$\mathpzc{p}\kappa_{1}{\scriptstyle\maltese}$ and
$\mathpzc{q}\kappa_{2}{\scriptstyle\maltese}$ where $\mathpzc{p}$ and
$\mathpzc{q}$ are two positive-ended negative paths on disjoint bases:

$\mathpzc{p}\kappa_{1}{\scriptstyle\maltese}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}\kappa_{2}{\scriptstyle\maltese}=(\mathpzc{p}\kappa_{1}{\scriptstyle\maltese}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q})\cup(\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}\kappa_{2}{\scriptstyle\maltese})$

  * •

The definition is extended to paths $\mathpzc{r}\mathpzc{p}$ and
$\mathpzc{r}\mathpzc{q}$ where $\mathpzc{r}$ is a positive-ended path and
$\mathpzc{p}$ and $\mathpzc{q}$ are two positive-ended negative paths on
disjoint bases:

$\mathpzc{r}\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{r}\mathpzc{q}=\mathpzc{r}(\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q})$

###### Remark 2.5

Note that each path in
$\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}$
respects the order of actions in paths $\mathpzc{p}$ and $\mathpzc{q}$.
Furthermore, if at least one of $\mathpzc{p}$ or $\mathpzc{q}$ does not end
with a daimon, each path in
$\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}$
contains exactly once all actions from $\mathpzc{p}$ and $\mathpzc{q}$.

###### Proposition 2.6

Let $\mathpzc{p}$ and $\mathpzc{q}$ be two paths such that
$\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}$
is defined, i.e., up to their (positive-ended or empty) prefix, they have
disjoint bases. Let $\mathpzc{r}$ be a sequence belonging to
$\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}$,
then $\mathpzc{r}$ is a path.

  * Proof

    * –

Suppose that $\mathpzc{p}$ and $\mathpzc{q}$ have an empty prefix and at least
one of them does not end with a daimon. We check below that $\mathpzc{r}$
satisfies criteria for being a path:
– By construction, the conditions of alternation, justification, linearity,
daimon and totality are satisfied.
– Since all subsequences $\mathpzc{p}_{j}$ and $\mathpzc{q}_{j}$ start with a
negative action, for all action $\kappa$ belonging to $\mathpzc{r}$ and such
that $\mathpzc{w}\kappa$ is a prefix of $\mathpzc{r}$,
$\raisebox{1.29167pt}{$\ulcorner$}{\mathpzc{w}\kappa}\raisebox{1.29167pt}{$\urcorner$}$
is either completely in $\mathpzc{p}$ if $\kappa$ is in $\mathpzc{p}$ or in
$\mathpzc{q}$ if $\kappa$ is in $\mathpzc{q}$. Then the negative jump
condition on $\mathpzc{r}$ is directly inherited from $\mathpzc{p}$ and
$\mathpzc{q}$.

    * –

Suppose that
$\mathpzc{p}=\mathpzc{p}^{\prime}\kappa_{1}{\scriptstyle\maltese}$ and
$\mathpzc{q}=\mathpzc{q}^{\prime}\kappa_{2}{\scriptstyle\maltese}$ with empty
common prefix. Remark that $\mathpzc{p}^{\prime}$ and $\mathpzc{q}^{\prime}$
are positive-ended paths with empty-common prefix. Furthermore either
$\mathpzc{r}\in\mathpzc{p}^{\prime}\kappa_{1}{\scriptstyle\maltese}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}$
or
$\mathpzc{r}\in\mathpzc{p}\kappa_{1}{\scriptstyle\maltese}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}^{\prime}$.
Hence it follows from the previous item that $\mathpzc{r}$ is a path.

    * –

Suppose that $\mathpzc{p}=\mathpzc{s}\mathpzc{p}^{\prime}$ and
$\mathpzc{q}=\mathpzc{s}\mathpzc{q}^{\prime}$ where $\mathpzc{s}$ is a
positive-ended path and $\mathpzc{p}^{\prime}$ and $\mathpzc{q}^{\prime}$ are
two positive-ended negative paths on disjoint bases. The same reasoning as in
the first item applies as the prefix $\mathpzc{s}$ may be viewed either as in
$\mathpzc{p}$ or $\mathpzc{q}$.

It is possible to build paths from a given set of chronicles, provided that
these chronicles are pairwise coherent. Indeed, coherence ensures that, after
a common positive-ended prefix, chronicles are made of negative paths either
on disjoint bases or with first actions of same focus.

######  Definition 2.7 (Coherence)

  * •

Two chronicles ${\mathfrak{c_{1}}}$ and ${\mathfrak{c_{2}}}$ of same base are
coherent, noted ${\mathfrak{c_{1}}}\coh{\mathfrak{c_{2}}}$, when the two
following conditions are satisfied:

    * –

Comparability: Either one extends the other or they first differ on negative
actions, i.e., if $w\kappa_{1}\coh w\kappa_{2}$ then either
$\kappa_{1}=\kappa_{2}$ or $\kappa_{1}$ and $\kappa_{2}$ are negative actions.

    * –

Propagation: When they first differ on negative actions and these negative
actions have distinct focuses then the focuses of following actions in
${\mathfrak{c_{1}}}$ and ${\mathfrak{c_{2}}}$ are pairwise distinct, i.e., if
$w(-,\xi_{1},I_{1})w_{1}\sigma_{1}\coh w(-,\xi_{2},I_{2})w_{2}\sigma_{2}$ with
$\xi_{1}\neq\xi_{2}$ then $\sigma_{1}$ and $\sigma_{2}$ have distinct focuses.

  * •

Two paths $\mathpzc{p}_{1}$ and $\mathpzc{p}_{2}$ of same base are coherent,
noted $\mathpzc{p}_{1}\coh\mathpzc{p}_{2}$, if
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{p_{1}^{*}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}\cup\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{p_{2}^{*}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$
is a clique with respect to $\coh$.

Let $\mathpzc{p}$ be a path, it follows from the definition of a view and the
coherence relation that
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$
as well as
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}^{*}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$
are cliques of chronicles.

###### Definition 2.8

  * •

Let $P$ and $Q$ be two sets of positive-ended paths, the shuffle of $P$ and
$Q$, noted
$P{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}Q$,
is the set
$\bigcup(\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q})$,
the union being taken on paths $\mathpzc{p}\in P,\mathpzc{q}\in Q$ where
$\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}$
is defined.

  * •

Let $P$ be a set of positive-ended paths, the shuffle closure of $P$, noted
$P^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}$,
is the smallest set such that
$P^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}=P^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}P^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}$
and $P\subset
P^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}$.

###  2.2 Designs as Sets of Chronicles or Sets of Paths

The notions of cliques of chronicles or cliques of paths are both relevant to
define designs. The first one is closer to a tree-like presentation of formal
proofs, the second one is closer to the definition of a strategy as set of
plays. The first one was the one introduced by Girard in [10].

######  Definition 2.9 (Design, Slice, Net)

  * $\bullet$

A design ${\mathfrak{D}}$, based on $\Gamma\vdash\Delta$, is a prefix-closed
clique of chronicles based on $\Gamma\vdash\Delta$, such that chronicles
without extension in ${\mathfrak{D}}$ end with a positive action and the
clique is non empty when the base is positive, i.e., when $\Gamma$ is empty.

  * $\bullet$

A slice is a design ${\mathfrak{S}}$ such that if
$w(-,\xi,I_{1}),w(-,\xi,I_{2})\in{\mathfrak{S}}$ then $I_{1}=I_{2}$.

  * $\bullet$

A net of designs is a finite set of designs such that foci of the bases do not
appear twice on the same part of sequents.

Abusively, in the following, we consider also a net of designs as a set of
chronicles, recovering the designs as the maximal cliques of this set of
chronicles.

###### Example 2.10

Let us consider the following design ${\mathfrak{D}}$, drawn in a proof-like
manner222For ease of reading, throughout the paper, designs are drawn in a
proof-like way with actions omitted.:

$\textstyle\xi 000\vdash\sigma 00$ $\textstyle\vdash\sigma 00,\xi 00$
$\textstyle\scriptstyle(+,\xi 00,\\{0\\})$ $\textstyle\sigma 0\vdash\xi 00$
$\textstyle\scriptstyle(-,\sigma 0,\\{0\\})$ $\textstyle\vdash\xi 00,\sigma$
$\textstyle\scriptstyle(+,\sigma,\\{0\\})$ $\textstyle\xi 0\vdash\sigma$
$\textstyle\scriptstyle(-,\xi 0,\\{0\\})$ $\textstyle\xi 100\vdash$
$\textstyle\vdash\xi 10$ $\textstyle\scriptstyle(+,\xi 10,\\{0\\})$
$\textstyle\xi 1\vdash$ $\textstyle\scriptstyle(-,\xi 1,\\{0\\})$
$\textstyle\vdash\xi,\sigma$ $\textstyle\scriptstyle(+,\xi,\\{0,1\\})$

The maximal chronicles are ${\mathfrak{c}}$ and ${\mathfrak{d}}$ given below,
i.e.,
${\mathfrak{D}}={\mathfrak{c}}^{*}\cup{\mathfrak{d}}^{*}\setminus\\{\epsilon\\}$:
${\mathfrak{c}}=$ $(+,\xi,\\{0,1\\})(-,\xi
0,\\{0\\})(+,\sigma,\\{0\\})(-,\sigma 0,\\{0\\})(+,\xi 00,\\{0\\})$ ,
${\mathfrak{d}}=$ $(+,\xi,\\{0,1\\})(-,\xi 1,\\{0\\})(+,\xi 10,\\{0\\})$ .
The maximal paths are obtained as shuffles of these chronicles. Namely:
$\mathpzc{p}=$ $(+,\xi,\\{0,1\\})(-,\xi 0,\\{0\\})(+,\sigma,\\{0\\})(-,\sigma
0,\\{0\\})(+,\xi 00,\\{0\\})(-,\xi 1,\\{0\\})(+,\xi 10,\\{0\\})$ .
$\mathpzc{q}=$ $(+,\xi,\\{0,1\\})(-,\xi 0,\\{0\\})(+,\sigma,\\{0\\})(-,\xi
1,\\{0\\})(+,\xi 10,\\{0\\})(-,\sigma 0,\\{0\\})(+,\xi 00,\\{0\\})$ .
$\mathpzc{r}=$ $(+,\xi,\\{0,1\\})(-,\xi 1,\\{0\\})(+,\xi 10,\\{0\\})(-,\xi
0,\\{0\\})(+,\sigma,\\{0\\})(-,\sigma 0,\\{0\\})(+,\xi 00,\\{0\\})$ .
Chronicles ${\mathfrak{c}}$ and ${\mathfrak{d}}$ (and their prefixes) are
obtained as views of paths $\mathpzc{p}$, $\mathpzc{q}$, $\mathpzc{r}$ (and
their prefixes). In particular,
${\mathfrak{c}}=\raisebox{1.29167pt}{$\ulcorner$}{\mathpzc{q}}\raisebox{1.29167pt}{$\urcorner$}=\raisebox{1.29167pt}{$\ulcorner$}{\mathpzc{r}}\raisebox{1.29167pt}{$\urcorner$}$
and
${\mathfrak{d}}=\raisebox{1.29167pt}{$\ulcorner$}{\mathpzc{p}}\raisebox{1.29167pt}{$\urcorner$}$.

We may notice on this example that shuffles of paths are paths, as we stated
in proposition 2.6. For example, the sequence
$s=\scriptstyle(+,\xi,\\{0,1\\})(-,\xi 0,\\{0\\})(+,\sigma,\\{0\\})(-,\xi
1,\\{0\\})(+,\xi 00,\\{0\\})$, which interleaves chronicles ${\mathfrak{c}}$
and ${\mathfrak{d}}$, does not keep all actions of ${\mathfrak{c}}$ and
${\mathfrak{d}}$. Note also that it satisfies all constraints to be a path
except the negative jump condition: $\scriptstyle(+,\xi 00,\\{0\\})$ is
justified by $\scriptstyle(-,\xi 0,\\{0\\})$, however one cannot find a
sequence $(\alpha_{i})$ that satisfies the condition.

We recall below a result we proved in [9] that states that a non-empty clique
of non-empty paths may give rise to a net of designs. Furthermore it follows
from proposition 2.6 that
${\mathfrak{R}}^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}$
is a set of paths when ${\mathfrak{R}}$ is a net of designs. Hence that makes
explicit the link between paths and chronicles of a design, and more generally
of a net of designs, hence justifies the switch from/to the reading of designs
or nets as cliques of chronicles to/from the reading of designs or nets as
cliques of paths. Thus we say that $\mathpzc{p}$ is a positive-ended path of a
net ${\mathfrak{R}}$ whenever $\mathpzc{p}$ is in
${\mathfrak{R}}^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}$.

###### Proposition 2.11

[9] Let $V$ be a non-empty clique of non-empty paths based on $\beta$ such
that maximal ones are positive-ended and let $V^{*}$ be the closure by
prefixes of $V$. The set of chronicles
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{V^{*}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$
defined as the union of views of paths of $V^{*}$ forms a net of designs based
on $\beta$.

###### Proposition 2.12

Let $\mathpzc{p}$ be a positive-ended path of a net of designs
${\mathfrak{R}}$ then
$\mathpzc{p}\in{\mathfrak{R}}^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}$.

  * Proof

Let $\mathpzc{p}$ be a positive-ended path of ${\mathfrak{R}}$, we prove that
$\mathpzc{p}\in{\mathfrak{R}}^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}$
by induction on the length of $\mathpzc{p}$.
– If $\mathpzc{p}=\epsilon$ or $\mathpzc{p}=\kappa^{+}$, the result is obvious
as in the two cases
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}=\\{\mathpzc{p}\\}$.
– Otherwise $\mathpzc{p}$ is of the form $w\kappa^{-}\kappa^{+}$. As
$\mathpzc{p}$ is a path,
$\raisebox{1.29167pt}{$\ulcorner$}{w\kappa^{-}\kappa^{+}}\raisebox{1.29167pt}{$\urcorner$}=w^{\prime}\kappa^{-}\kappa^{+}$,
i.e., $\kappa^{-}\kappa^{+}$ are the two last actions of a (positive-ended)
chronicle of ${\mathfrak{R}}$. Let us define a sequence $\mathpzc{q}$ as
$\mathpzc{p}$ where one deletes actions in $w^{\prime}\kappa^{-}\kappa^{+}$.
It is straightforward to prove that $\mathpzc{q}$ is a path of
${\mathfrak{R}}$ and that
$\mathpzc{r}\in\mathpzc{q}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}w^{\prime}\kappa^{-}\kappa^{+}$.
Thus the result follows by induction hypothesis.

Note that a path $\mathpzc{p}$ made of actions present in a net of designs
${\mathfrak{R}}$ may not be a path of ${\mathfrak{R}}$.

###### Example 2.13

Let us consider the following design ${\mathfrak{E}}$ drawn on the left:

$\textstyle\vdash\xi 000,\xi 111$ $\textstyle{\scriptstyle\maltese}$
$\textstyle\xi 11\vdash\xi 000$ $\textstyle\vdash\xi 000,\xi 1$ $\textstyle\xi
00\vdash\xi 1$ $\textstyle\vdash\xi 0,\xi 1$ $\textstyle\xi\vdash$

The two following sequences are paths:

$\mathpzc{p}=$ $(-,\xi,\\{0,1\\})(+,\xi 0,\\{0\\})(-,\xi 00,\\{0\\})(+,\xi
1,\\{1\\})(-,\xi 11,\\{1\\}){\scriptstyle\maltese}$ .

$\mathpzc{q}=$ $(-,\xi,\\{0,1\\})(+,\xi 1,\\{1\\})(-,\xi 11,\\{1\\})(+,\xi
0,\\{0\\})(-,\xi 00,\\{0\\}){\scriptstyle\maltese}$ .

However
$\mathpzc{p}\in{\mathfrak{E}}^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}$
and
$\mathpzc{q}\not\in{\mathfrak{E}}^{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}$.

###  2.3 Duality and Reversible Paths

We define in the next subsection the fundamental notion of interaction. Two
designs may then be orthogonal as soon as their interaction behaves ‘well’ in
a sense that will be made clear later. The closure by bi-orthogonality of a
set of designs allows to recover the notion of type, called in Ludics
behaviour. The study of these behaviours is in some aspects more graspable
when interaction is defined on designs presented as cliques of paths. It is
the case for visitability that characterizes sequences of actions visited
during an interaction, or incarnation that defines designs of a behaviour that
are fully visited by interaction. Indeed, as we shall prove in lemma 2.20, the
sequence of actions visited during an interaction is a path. Furthermore paths
visited during an interaction between a design and another design (or a net)
are duals in the following sense.

######  Definition 2.14 (Duality, Reversibility)

Let $\mathpzc{p}$ be a positive-ended alternate sequence.

  * •

The dual of $\mathpzc{p}$ (possibly empty) is the positive-ended alternate
sequence of actions $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
(possibly empty) such that333The notation $\overline{\kappa}$ is simply $\hbox
to0.0pt{$\overline{\makebox[33.99998pt][c]{ \rule{0.0pt}{7.5pt} }}$
\hss}(\pm,\xi,I)=(\mp,\xi,I)$ and may be extended on sequences by $\hbox
to0.0pt{$\overline{\makebox[4.05904pt][c]{ \rule{0.0pt}{4.30554pt} }}$
\hss}\epsilon=\epsilon$ and $\hbox to0.0pt{$\overline{\makebox[13.18983pt][c]{
\rule{0.0pt}{4.30554pt} }}$ \hss}w\kappa=\hbox
to0.0pt{$\overline{\makebox[7.42825pt][c]{ \rule{0.0pt}{4.30554pt} }}$
\hss}w\,\hbox to0.0pt{$\overline{\makebox[5.76158pt][c]{
\rule{0.0pt}{4.30554pt} }}$ \hss}\kappa$.:

    * –

If $\mathpzc{p}=w{\scriptstyle\maltese}$ then
$\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$}}:=\hbox
to0.0pt{$\overline{\makebox[7.42825pt][c]{ \rule{0.0pt}{4.30554pt} }}$
\hss}w$.

    * –

Otherwise
$\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$}}:=\hbox
to0.0pt{$\overline{\makebox[5.55557pt][c]{ \rule{0.0pt}{4.30554pt} }}$
\hss}\mathpzc{p}{\scriptstyle\maltese}$.

  * •

When $\mathpzc{p}$ and $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
are positive-ended paths, we say that $\mathpzc{p}$ is reversible.

###### Example 2.15

There exist paths such that their duals are not paths. Let us consider the
following design:

$\textstyle\xi 000\vdash\sigma 00$ $\textstyle\vdash\sigma 00,\xi 00$
$\textstyle\sigma 0\vdash\xi 00$ $\textstyle\vdash\xi 00,\sigma$
$\textstyle\xi 0\vdash\sigma$ $\textstyle\xi 100\vdash$ $\textstyle\vdash\xi
10$ $\textstyle\xi 1\vdash$ $\textstyle\vdash\xi,\sigma$

The sequence $s=$ $(+,\xi,\\{0,1\\})(-,\xi 0,\\{0\\})(+,\sigma,\\{0\\})(-,\xi
1,\\{0\\})(+,\xi 10,\\{0\\})$ is a path based on $\vdash\xi,\sigma$. On the
contrary its dual $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.6875pt}{0.0pt}{$\sim$}$}\hss}{s}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.6875pt}{0.0pt}{$\sim$}$}\hss}{s}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.6875pt}{0.0pt}{$\sim$}$}\hss}{s}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.6875pt}{0.0pt}{$\sim$}$}\hss}{s}}$
is not a path: it does not satisfy the negative jump condition.

In fact, when $\mathpzc{p}$ is a path, the sequence $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
satisfies automatically alternation, justification, totality, and daimon
conditions. The only condition which may be not satisfied is the negative jump
condition. In [9] we call “restrictive negative jump condition” the fact that
$\mathpzc{p}$ is reversible, i.e., $\mathpzc{p}$ is a path such that
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
satisfies the negative jump condition (see Fig. 2). The restrictive negative
jump constraint is nothing but the dual of the negative jump constraint. In
the next lemma we prove that this restrictive negative jump constraint is
always satisfied on chronicles.

$\mathpzc{p}$$\kappa^{\prime+}$$\alpha_{n}^{+}$$\alpha_{n}^{-}$…$\alpha_{n-1}^{+}$……$\alpha_{i+1}^{-}$…$\alpha_{i}^{+}$$\alpha_{i}^{-}$……$\alpha_{1}^{-}$…$\alpha_{0}^{+}$$\alpha_{0}^{-}$$\kappa^{-}$

Figure 2: Path $\mathpzc{p}$: Constraint of restrictive negative jump between
$\kappa^{-}$ justified by $\kappa^{\prime+}$

###### Lemma 2.16

The dual of a chronicle is a path.

  * Proof

Let ${\mathfrak{c}}$ be a chronicle. By definition of $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}$,
the sequence is alternate, justified and the daimon may only be the last
action of the sequence. The negative jump condition results directly from the
definition of chronicles. Finally, if $\kappa^{+}$ is justified by
$\kappa^{-}$ in $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}$
then $\overline{\kappa^{+}}$ is justified by $\overline{\kappa^{-}}$ in
${\mathfrak{c}}$. Thus $\overline{\kappa^{-}}$ immediately precedes
$\overline{\kappa^{+}}$ in ${\mathfrak{c}}$ as ${\mathfrak{c}}$ is a
chronicle. Hence, if $w\kappa^{+}$ is the prefix of $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}$,
since
$\raisebox{1.29167pt}{$\ulcorner$}{w\kappa^{+}}\raisebox{1.29167pt}{$\urcorner$}=\raisebox{1.29167pt}{$\ulcorner$}{w}\raisebox{1.29167pt}{$\urcorner$}\kappa^{+}$
and since $\kappa^{-}$ is the last action of $w$,
$\kappa^{-}\in\raisebox{1.29167pt}{$\ulcorner$}{w}\raisebox{1.29167pt}{$\urcorner$}$.
This proves that restrictive negative jump is satisfied. Hence
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{4.44444pt}{0.0pt}{$\sim$}$}\hss}{{\mathfrak{c}}}}$
is a path.

We proved in proposition 2.6 that being a path is stable by the shuffle
operation. However, as we show in next example, being a reversible path is not
stable by shuffle.

###### Example 2.17

Let us consider the design drawn on the left:
$\textstyle\xi 000\vdash\sigma 00$ $\textstyle\vdash\sigma 00,\xi 00$
$\textstyle\sigma 0\vdash\xi 00$ $\textstyle\vdash\xi 00,\sigma$
$\textstyle\xi 0\vdash\sigma$ $\textstyle\xi 100\vdash$ $\textstyle\vdash\xi
10$ $\textstyle\xi 1\vdash$ $\textstyle\vdash\xi,\sigma$ The path
$\mathpzc{s}=\scriptstyle(+,\xi,\\{0,1\\})(-,\xi
0,\\{0\\})(+,\sigma,\\{0\\})(-,\xi 1,\\{0\\})(+,\xi 10,\\{0\\})$ is in the
shuffle of the two chronicles $\scriptstyle(+,\xi,\\{0,1\\})(-,\xi
0,\\{0\\})(+,\sigma,\\{0\\})$ and $\scriptstyle(+,\xi,\\{0,1\\})(-,\xi
1,\\{0\\})(+,\xi 10,\\{0\\})$. As we prove it in lemma 2.16, the duals of
these two chronicles are paths. But $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.94444pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{s}}}$
is not a path.

Nevertheless, not being reversible is stable by shuffle as shown in the next
lemma.

###### Lemma 2.18

Let $\mathpzc{p}$ and $\mathpzc{q}$ be two positive-ended paths and
$\mathpzc{r}\in\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}$
be a path such that its dual $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.91667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.91667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.91667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.91667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}}}$
is a path, then duals $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
and $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
are paths.

  * Proof

We prove the result by contradiction: let us suppose that $\mathpzc{p}$ and
$\mathpzc{q}$ are two paths,
$\mathpzc{r}\in\mathpzc{p}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}$
is a path such that its dual $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.91667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.91667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.91667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{3.91667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}}}$
is a path, and at least one of the duals $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
and $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
is not a path. Without loss of generality, we can suppose that
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
is not a path.

    * –

Remark the following. Let $\mathpzc{p},\mathpzc{q},\mathpzc{r}$ defined as
above then there exist
$\mathpzc{p}^{\prime},\mathpzc{q}^{\prime},\mathpzc{r}^{\prime}$ satisfying
the same requirements as for $\mathpzc{p},\mathpzc{q},\mathpzc{r}$ and such
that $\mathpzc{r}^{\prime}=w{\scriptstyle\maltese}$ where $w$ is a prefix of
$\mathpzc{r}$. Indeed, as $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
is not a path, there exists an action $\kappa^{-}$ justified by $\kappa^{+}$
such that $\mathpzc{p}=w_{1}\kappa^{+}w_{2}\kappa^{-}w_{3}$ and the
(Restrictive Negative Jump) constraint is not satisfied on $\kappa^{-}$. Hence
$\mathpzc{p}^{\prime}:=w_{1}\kappa^{+}w_{2}\kappa^{-}{\scriptstyle\maltese}$
is a path such that $\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{7.09557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{7.09557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{7.09557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{7.09557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}^{\prime}}}$
is not a path. Let $\mathpzc{r}=x_{1}\kappa^{-}x_{2}$ and note that
$w_{1}\kappa^{+}w_{2}$ is a subsequence of $x_{1}$. Let $\mathpzc{q}^{\prime}$
be the subsequence of $x_{1}\kappa^{-}$ with actions in $\mathpzc{q}$, then
$\mathpzc{q}^{\prime}$ is a positive-ended prefix of $\mathpzc{q}$, hence a
path. Finally let
$\mathpzc{r}^{\prime}:=x_{1}\kappa^{-}{\scriptstyle\maltese}$ then
$\mathpzc{r}^{\prime}$ and $\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.45667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.45667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.45667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.45667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}^{\prime}}}$
are paths such that
$\mathpzc{r}^{\prime}\in\mathpzc{p}^{\prime}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}^{\prime}$
(by following the same construction steps as for $\mathpzc{r}$).

    * –

Hence for proving the lemma, it suffices to consider triples
$(\mathpzc{p}^{\prime},\mathpzc{q}^{\prime},\mathpzc{r}^{\prime})$ satisfying
the following:
$\mathpzc{r}^{\prime}\in\mathpzc{p}^{\prime}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}^{\prime}$
is such that $\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.45667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.45667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.45667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{5.45667pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{r}^{\prime}}}$
is a path ($\mathpzc{r}^{\prime}$ satisfies the restrictive negative jump),
$\mathpzc{r}^{\prime}=w\kappa^{-}{\scriptstyle\maltese}$ and the restrictive
negative jump is not satisfied on action $\kappa^{-}$ present in
$\mathpzc{p}^{\prime}$.

    * –

Remark also that if lengths of $\mathpzc{p}^{\prime}$ and
$\mathpzc{q}^{\prime}$ are less or equal to $2$ then $\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{7.09557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{7.09557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{7.09557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{7.09557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}^{\prime}}}$
and $\mathchoice{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{6.81778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{6.81778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{6.81778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}^{\prime}}}{\hbox
to0.0pt{\raisebox{5.8611pt}{$\leavevmode\resizebox{6.81778pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}^{\prime}}}$
are paths.

    * –

Let $(\mathpzc{p}_{0},\mathpzc{q}_{0},\mathpzc{r}_{0})$ be such a triple with
length of $\mathpzc{r}_{0}$ minimal with respect to all such triples
$(\mathpzc{p}^{\prime},\mathpzc{q}^{\prime},\mathpzc{r}^{\prime})$. Notice
that $\kappa^{-}$ is not initial, otherwise (Restrictive Negative Jump) would
be satisfied for $\mathpzc{p}_{0}$. As $\mathpzc{r}_{0}$ satisfies the
(Restrictive Negative Jump), there exists a sequence
$(\alpha_{n}^{+}=\kappa^{+},\alpha_{n}^{-},\dots,\alpha_{0}^{+},\alpha_{0}^{-}=\kappa^{-})$
where $\kappa^{+}$ justifies $\kappa^{-}$ and the sequence is defined as in
the definition of (Restrictive Negative Jump). Let us suppose
$\mathpzc{r}_{0}=w^{\prime}\alpha_{1}^{-}w^{\prime\prime}\alpha_{0}^{+}\kappa^{-}{\scriptstyle\maltese}$.

      * *

Suppose $\alpha_{0}^{+}$ is an action of $\mathpzc{p}_{0}$, then it is also
the case for its justifier $\alpha_{1}^{-}$. Define
$\mathpzc{r}_{1}=w^{\prime}\kappa^{-}{\scriptstyle\maltese}$. Remark that
$\mathpzc{r}_{1}$ is a path and its dual is a also a path. Furthermore, we can
define $\mathpzc{q}_{1}$ (resp. $\mathpzc{p}_{1}$) as the subsequence of
$\mathpzc{q}_{0}$ (resp. $\mathpzc{p}_{0}$) present in $\mathpzc{r}_{1}$.
Remark that
$\mathpzc{r}_{1}\in\mathpzc{p}_{1}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}\mathpzc{q}_{1}$
and $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{8.35558pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}_{1}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{8.35558pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}_{1}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{8.35558pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}_{1}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{8.35558pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}_{1}}}$
is not a path. This contradicts the fact that $\mathpzc{r}_{0}$ is minimal.

      * *

Otherwise $\alpha_{0}^{+}$ is an action of $\mathpzc{q}_{0}$, then it is also
the case for its justifier $\alpha_{1}^{-}$. If actions in $w^{\prime\prime}$
are actions of $\mathpzc{q}_{0}$, we define $\mathpzc{r}_{1}$,
$\mathpzc{q}_{1}$, $\mathpzc{p}_{1}$ as before and this yields a
contradiction. Else let $\beta^{+}$ be the last action of $\mathpzc{p}_{0}$ in
$w^{\prime\prime}$. There is also an action $\gamma^{-}$ of
${\mathpzc{p}}_{0}$ which immediately precedes $\beta^{+}$ in
$w^{\prime\prime}$. One can delete from $\mathpzc{r}_{0}$ the actions
$\gamma^{-}$ and $\beta^{+}$. Then we get a shorter sequence $\mathpzc{r}_{1}$
together with paths $\mathpzc{p}_{1}$ and $\mathpzc{q}_{1}$ such that
$\mathpzc{p}_{1}$ does not satisfy the (Restrictive Negative Jump). Hence a
contradiction.

###  2.4 Interaction on Designs as Clique of Chronicles or as Cliques of Paths

The interaction, also named normalization, is defined by Girard in [10] when
designs are presented as cliques of chronicles:

######  Definition 2.19 (Closed Cut-net, Interaction, Orthogonality,
Behaviour)

  * •

Let ${\mathfrak{R}}$ be a net of designs, ${\mathfrak{R}}$ is a closed cut-net
if

    * –

addresses in bases are either distinct or present twice, once in a left part
of a base and once in a right part of another base,

    * –

the net of designs is acyclic and connex with respect to the graph of bases
and cuts.

An address presents in a left part and in a right part defines a cut. Note
that a closed cut-net has a unique design with positive base, called its main
design.

  * •

Interaction on closed cut-nets Let ${\mathfrak{R}}$ be a closed cut-net. The
design resulting from interaction, denoted by $[\\![{\mathfrak{R}}]\\!]$, is
defined in the following way: let ${\mathfrak{D}}$ be the main design of
${\mathfrak{R}}$, with first action $\kappa$,

    * –

if $\kappa$ is a daimon, then
$[\\![{\mathfrak{R}}]\\!]=\\{{\scriptstyle\maltese}\\}$,

    * –

otherwise $\kappa$ is a proper positive action $(+,\sigma,I)$ such that
$\sigma$ is part of a cut with another design with last rule
$(-,\sigma,{\mathcal{N}})$ (aggregating ramifications of actions on the same
focus $\sigma$):

      * *

If $I\not\in\mathcal{N}$, then interaction fails.

      * *

Otherwise, interaction follows with the connected part of subdesigns obtained
from $I$ with the rest of ${\mathfrak{R}}$.

  * •

Orthogonality

    * –

Two designs ${\mathfrak{D}}$ and ${\mathfrak{E}}$ respectively based on
$\vdash\xi$ and $\xi\vdash$ are said to be orthogonal when
$[\\![{\mathfrak{D}},{\mathfrak{E}}]\\!]=\\{{\scriptstyle\maltese}\\}$.

    * –

Let ${\mathfrak{D}}$ be a design of base
$\xi\vdash\sigma_{1},\dots,\sigma_{n}$ (resp.
$\vdash\sigma_{1},\dots,\sigma_{n}$), let ${\mathfrak{R}}$ be the net of
designs $({\mathfrak{A}},{\mathfrak{B}}_{1},\dots,{\mathfrak{B}}_{n})$ (resp.
${\mathfrak{R}}=({\mathfrak{B}}_{1},\dots,{\mathfrak{B}}_{n})$), where
${\mathfrak{A}}$ has base $\vdash\xi$ and ${\mathfrak{B}}_{i}$ has base
$\sigma_{i}\vdash$, ${\mathfrak{R}}$ belongs to ${\mathfrak{D}}^{\perp}$ if
$[\\![{\mathfrak{D}},{\mathfrak{R}}]\\!]=\\{{\scriptstyle\maltese}\\}$.

    * –

Let ${\mathrm{E}}$ be a set of designs of the same base,
${\mathrm{E}}^{\perp}=\bigcap_{{\mathfrak{D}}\in{\mathrm{E}}}{\mathfrak{D}}^{\perp}$.

    * –

A set of designs ${\mathrm{E}}$ is a behaviour if
${\mathrm{E}}={\mathrm{E}}^{\perp\perp}$.

With the following lemma, we prove that interaction gives rise to two dual
paths.

###### Lemma 2.20

Let ${\mathfrak{D}}$ be a design of base
$\xi\vdash\sigma_{1},\dots,\sigma_{n}$ (resp.
$\vdash\sigma_{1},\dots,\sigma_{n}$),
let ${\mathfrak{R}}$ be the net of designs
$({\mathfrak{A}},{\mathfrak{B}}_{1},\dots,{\mathfrak{B}}_{n})$ (resp.
${\mathfrak{R}}=({\mathfrak{B}}_{1},\dots,{\mathfrak{B}}_{n})$), where
${\mathfrak{A}}$ has base $\vdash\xi$ and ${\mathfrak{B}}_{i}$ has base
$\sigma_{i}\vdash$,
${\mathfrak{R}}$ belongs to ${\mathfrak{D}}^{\perp}$ iff there is a path
$\mathpzc{p}$ such that $\mathpzc{p}$ is a path of ${\mathfrak{D}}$ and
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
is a path of ${\mathfrak{R}}$.
We denote the path $\mathpzc{p}$ by
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$ and
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
by $\left<{\mathfrak{R}}\\!\\!\leftarrow\\!\\!{\mathfrak{D}}\right>$.

  * Proof

Remark first that with ${\mathfrak{D}}$ and ${\mathfrak{R}}$ as given in the
lemma, we have that $({\mathfrak{D}},{\mathfrak{R}})$ is a closed cut-net.

    * –

Suppose that $({\mathfrak{D}},{\mathfrak{R}}$) is a convergent closed cut-net.
The sequence
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$, is built by
induction on the number $n$ of normalization steps:
– Case $n=1$: If the interaction stops in one step: either
${\mathfrak{D}}=\\{{\scriptstyle\maltese}\\}$, in this case
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>={\scriptstyle\maltese}$,
or the main design (which is not ${\mathfrak{D}}$) is equal to
$\\{{\scriptstyle\maltese}\\}$ and in this case
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$ is the empty
sequence. Otherwise let $\kappa^{+}$ be the first action of the main design.
The first action of
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$ is
$\kappa^{+}$ if ${\mathfrak{D}}$ is the main design and is
$\overline{\kappa^{+}}$ otherwise.
– Case $n=p+1$: the prefix $\kappa_{1}\dots\kappa_{p}$ of
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$ is already
defined.

      * *

Either the interaction stops, hence the main design is
${\scriptstyle\maltese}$, and
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>=\kappa_{1}\dots\kappa_{p}$
if the main design is a subdesign of ${\mathfrak{R}}$, or
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>=\kappa_{1}\dots\kappa_{p}{\scriptstyle\maltese}$
if the main design is a subdesign of ${\mathfrak{D}}$.

      * *

Or, let $\kappa^{+}$ be the first proper action of the closed cut-net obtained
after step $p$,
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$ begins with
$\kappa_{1}\dots\kappa_{p}\overline{\kappa^{+}}$ if the main design is a
subdesign of ${\mathfrak{R}}$, or it begins with
$\kappa_{1}\dots\kappa_{p}\kappa^{+}$ if the main design is a subdesign of
${\mathfrak{D}}$.

We then check by induction on its length that the sequence
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$ is a path:
– The base case of the induction depends on the polarity of ${\mathfrak{D}}$:
If ${\mathfrak{D}}$ has a negative base then the base case is the empty
sequence, and the empty sequence is a path on ${\mathfrak{D}}$, otherwise
${\mathfrak{D}}$ has a positive base hence there exists a first action in the
sequence $\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$,
this action being the first action of ${\mathfrak{D}}$, hence a path on
${\mathfrak{D}}$.
– Suppose $\kappa_{1}\dots\kappa_{p}\kappa$ is a prefix of
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$ and that by
induction hypothesis $\kappa_{1}\dots\kappa_{p}$ is a path on
${\mathfrak{D}}$.

      * *

If $\kappa$ is a positive action then, with respect to normalization,
$\raisebox{1.29167pt}{$\ulcorner$}{\kappa_{1}\dots\kappa_{p}}\raisebox{1.29167pt}{$\urcorner$}\kappa$
is a chronicle of ${\mathfrak{D}}$ that extends
$\raisebox{1.29167pt}{$\ulcorner$}{\kappa_{1}\dots\kappa_{p}}\raisebox{1.29167pt}{$\urcorner$}$,
hence $\kappa_{1}\dots\kappa_{p}\kappa$ is a path on ${\mathfrak{D}}$.

      * *

If $\kappa$ is an initial negative action hence ${\mathfrak{D}}$ is negative
and $\kappa$ is the first action of the normalization, i.e., $p=0$, and
$\kappa$ is a path on ${\mathfrak{D}}$.

      * *

Otherwise the focus of the negative action $\kappa$ has been created during
normalization by a positive action present in $\kappa_{1}\dots\kappa_{p}$,
hence $\kappa_{1}\dots\kappa_{p}\kappa$ is a path on ${\mathfrak{D}}$.

Normalization being defined symmetrically between ${\mathfrak{D}}$ and
${\mathfrak{R}}$, we also have that
$\left<{\mathfrak{R}}\\!\\!\leftarrow\\!\\!{\mathfrak{D}}\right>$ is a path.

    * –

Suppose that there is a path $\mathpzc{p}$ of ${\mathfrak{D}}$, such that
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
is a path of ${\mathfrak{R}}$. Note that one of $\mathpzc{p}$ or
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
ends with a daimon. The proof that the closed cut-net
$({\mathfrak{D}},{\mathfrak{R}})$ normalizes to $\\{{\scriptstyle\maltese}\\}$
is done by induction on the length $k$ of a prefix of $\mathpzc{p}$. More
precisely, we prove that normalization is finished when $k=n$ if
${\mathfrak{D}}$ ends with a daimon otherwise when $k=n+1$. Furthermore, after
$k$ steps, interaction is done on two nets ${\mathfrak{S}}$ and
${\mathfrak{T}}$ such that $\mathpzc{p}=\kappa_{1}\dots\kappa_{k}\mathpzc{q}$,
the prefix $\kappa_{1}\dots\kappa_{k}$ is visited in ${\mathfrak{D}}$ during
these $k$ steps and $\mathpzc{q}$ is a path in the net of designs
${\mathfrak{S}}$ on which interaction may continue: ${\mathfrak{S}}$ is a
subnet of ${\mathfrak{D}}$. Similarly,
$\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$}}=\makebox[30.19261pt][c]{\mbox{\rule{0.0pt}{7.0pt}$\mathchoice{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{30.19261pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{1}\dots\kappa_{k}\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{30.19261pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{1}\dots\kappa_{k}\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{30.19261pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{1}\dots\kappa_{k}\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{7.0pt}{$\leavevmode\resizebox{30.19261pt}{0.0pt}{$\sim$}$}\hss}{\kappa_{1}\dots\kappa_{k}\mathpzc{q}}}$}}$,
the prefix $\overline{\kappa_{1}\dots\kappa_{k}}$ is visited in
${\mathfrak{R}}$ during these $m$ steps and $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
is a path in the net of designs ${\mathfrak{T}}$ on which interaction may
continue: ${\mathfrak{T}}$ is a subnet of ${\mathfrak{R}}$.
– Case $k=n$ and ${\mathfrak{D}}$ ends with a daimon. By induction hypothesis,
${\scriptstyle\maltese}$ is a (first) action the net ${\mathfrak{S}}$ that
remains of ${\mathfrak{D}}$. Thus normalization ends.
– Case $k=n+1$ and ${\mathfrak{D}}$ does not end with a daimon. Hence
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
ends with a daimon. By induction hypothesis, ${\scriptstyle\maltese}$ is a
(first) action the net ${\mathfrak{T}}$ that remains of ${\mathfrak{R}}$. Thus
normalization ends.
– Case $k=0$ with $k\neq n$: The induction proposition follows from the
hypotheses.
– Case $k+1$ with $k+1\neq n$ and induction hypotheses are satified for $k$:
let $\mathpzc{q}=\kappa_{k+1}\mathpzc{q}^{\prime}$, hence
$\overline{\mathpzc{q}}=\overline{\kappa_{k+1}\mathpzc{q}^{\prime}}$. Neither
$\kappa_{k+1}$ nor $\overline{\kappa_{k+1}}$ are the daimon. Without loss of
generality, we can suppose that $\kappa_{k+1}$ is a positive action. As
$\mathpzc{q}$ is a path of the net ${\mathfrak{S}}$, the main design of the
cut-net $({\mathfrak{S}},{\mathfrak{T}})$ is in the net ${\mathfrak{S}}$. We
have also that $\overline{\kappa_{k+1}}$ is a first negative action of a
design in the net ${\mathfrak{T}}$. We can then apply one step of
normalization. The process of normalization continue with a subnet
${\mathfrak{S}}^{\prime}$ of ${\mathfrak{S}}$ and a subnet
${\mathfrak{T}}^{\prime}$ of ${\mathfrak{T}}$. Remark that
$\mathpzc{q}^{\prime}$ is a path of ${\mathfrak{S}}^{\prime}$ and
$\overline{\mathpzc{q}^{\prime}}$ is a path on ${\mathfrak{T}}^{\prime}$.
Hence the result.

We finish this subsection with what could be considered at first sight of low-
interest. However we make use of it in the following situation: let us give a
path $\mathpzc{p}$ in a behaviour ${\mathbf{A}}$, then
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$
is a design. It follows from the proposition given below that its completion
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$
is a design in ${\mathbf{A}}$ whereas it may not be the case for the design
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$
itself.

######  Definition 2.21 (Completion of designs)

Let ${\mathfrak{D}}$ be a design, the completion of ${\mathfrak{D}}$, noted
${\mathfrak{D}}^{c}$, is the design obtained from ${\mathfrak{D}}$ by adding
chronicles ${\mathfrak{c}}(-,\xi,I){\scriptstyle\maltese}$ whenever
${\mathfrak{c}}\in{\mathfrak{D}}$, $I$ is a finite set of integers,
${\mathfrak{c}}(-,\xi,I){\scriptstyle\maltese}$ is a chronicle and
${\mathfrak{c}}(-,\xi,I)\not\in{\mathfrak{D}}$.

###### Proposition 2.22

Let ${\mathfrak{D}}$ be a design in a behaviour ${\mathbf{A}}$, consider a
design ${\mathfrak{C}}\subset{\mathfrak{D}}$ then
${\mathfrak{C}}^{c}\in{\mathbf{A}}$.

  * Proof

Let ${\mathfrak{E}}\in{\mathbf{A}}^{\perp}$. Hence
${\mathfrak{E}}\perp{\mathfrak{D}}$. Let $\mathpzc{p}$ be the longest
positive-ended path in the design ${\mathfrak{C}}$ that is a prefix of
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{E}}\right>$. Either
$\mathpzc{p}=\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{E}}\right>$,
hence ${\mathfrak{E}}\perp{\mathfrak{C}}$, and also
${\mathfrak{E}}\perp{\mathfrak{C}}^{c}$. Or there exist actions $\kappa^{-}$,
$\kappa^{+}$ and a sequence $w$ such that
$\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{E}}\right>=\mathpzc{p}\kappa^{-}\kappa^{+}w$.
Consider the chronicle ${\mathfrak{c}}$ such that
$\raisebox{1.29167pt}{$\ulcorner$}{\mathpzc{p}\kappa^{-}}\raisebox{1.29167pt}{$\urcorner$}={\mathfrak{c}}\kappa^{-}$.
By construction, ${\mathfrak{c}}\in{\mathfrak{C}}$. Either
${\mathfrak{c}}\kappa^{-}\in{\mathfrak{C}}$ hence also
${\mathfrak{c}}\kappa^{-}\kappa^{+}\in{\mathfrak{C}}$ as
${\mathfrak{C}}\subset{\mathfrak{D}}$ and there is a unique positive action
after a negative action. Contradiction as $\mathpzc{p}$ is then not maximal.
Or ${\mathfrak{c}}\kappa^{-}{\scriptstyle\maltese}\in{\mathfrak{C}}^{c}$ hence
${\mathfrak{E}}\perp{\mathfrak{C}}^{c}$.

###  2.5 Visitable paths, Behaviours, Incarnation

This subsection is devoted to a few properties concerning behaviours. Hence,
we always suppose that a set of designs is closed with respect to bi-
orthogonality. Visitability and incarnation are important concepts to study. A
visitable path in a behaviour, i.e., in a design of this behaviour, is a path
that may be travelled by interaction. It follows from lemma 2.20 that a path
is visitable iff its dual is visitable. The incarnation of a behaviour may be
characterized as the subset of its designs that is fully travelled by
interaction. It follows it is sufficient to study visitability and incarnation
to be able to characterize behaviours and operations on behaviours. As we
already mentionned in the previous subsection, all these properties rely
mainly on the concept of path.

######  Definition 2.23 (Visitability)

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

  * •

Let $\mathpzc{p}$ be a path of ${\mathbf{A}}$, $\mathpzc{p}$ is visitable in
${\mathbf{A}}$ if there exist a design ${\mathfrak{D}}$ in ${\mathbf{A}}$ and
a net ${\mathfrak{R}}$ in ${{\mathbf{A}}}^{\perp}$ such that
$\mathpzc{p}=\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$.

  * •

$V_{{\mathbf{A}}}$ is the set of visitable paths of ${\mathbf{A}}$.

###### Proposition 2.24

Let ${\mathbf{A}}$ be a behaviour,
$V_{\mathbf{A}}=\makebox[14.65556pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}$}}$,

  * Proof

By definition, $\mathpzc{p}\in V_{\mathbf{A}}$ iff there exist a design
${\mathfrak{D}}\in{\mathbf{A}}$ and a net
${\mathfrak{R}}\in{\mathbf{A}}^{\perp}$ such that
$\mathpzc{p}=\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>$,
i.e., $\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$}}=\left<{\mathfrak{R}}\\!\\!\leftarrow\\!\\!{\mathfrak{D}}\right>$.
Thus, as ${\mathfrak{D}}\in{\mathbf{A}}={\mathbf{A}}^{\perp\perp}$,
$\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$}}\in
V_{{\mathbf{A}}^{\perp}}$. Hence
$\makebox[12.25555pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}$}}\subset
V_{{\mathbf{A}}^{\perp}}$, i.e.,
$V_{\mathbf{A}}=\makebox[12.25555pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{\makebox[12.25555pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}$}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{\makebox[12.25555pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}$}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{\makebox[12.25555pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}$}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{\makebox[12.25555pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{12.25555pt}{0.0pt}{$\sim$}$}\hss}{V_{\mathbf{A}}}}$}}}}$}}\subset\makebox[14.65556pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}$}}$.
Replacing ${\mathbf{A}}$ by ${\mathbf{A}}^{\perp}$, we have also
$\makebox[14.65556pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}$}}\subset
V_{{\mathbf{A}}}$. So
$V_{\mathbf{A}}=\makebox[14.65556pt][c]{\mbox{\rule{0.0pt}{6.83331pt}$\mathchoice{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}{\hbox
to0.0pt{\raisebox{6.83331pt}{$\leavevmode\resizebox{14.65556pt}{0.0pt}{$\sim$}$}\hss}{V_{{\mathbf{A}}^{\perp}}}}$}}$.

######  Definition 2.25 (Incarnation)

Let ${\mathbf{A}}$ be a behaviour, ${\mathfrak{D}}$ be a design in
${\mathbf{A}}$. The design ${\mathfrak{D}}$ is material (or incarnated) in the
behaviour ${\mathbf{A}}$ if ${\mathfrak{D}}$ is minimal in ${\mathbf{A}}$ with
respect to inclusion. We denote by
$|{{\mathfrak{D}}}|_{{\mathrm{{\mathbf{A}}}}}$ the material design of
${\mathbf{A}}$ that is included in ${\mathfrak{D}}$.
The incarnation $|{{\mathrm{{\mathbf{A}}}}}|$ of a behaviour ${\mathbf{A}}$ is
the set of its material designs.

###### Proposition 2.26

Let ${\mathbf{A}}$ be a behaviour, ${\mathfrak{D}}$ be a design in
${\mathbf{A}}$.
$|{{\mathfrak{D}}}|_{{\mathrm{{\mathbf{A}}}}}=\bigcup_{{\mathfrak{R}}\in{\mathbf{A}}^{\perp}}\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.

  * Proof

Remark that
$\bigcup_{{\mathfrak{R}}\in{\mathbf{A}}^{\perp}}\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}=\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\bigcup_{{\mathfrak{R}}\in{\mathbf{A}}^{\perp}}\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.
To obtain a design ${\mathfrak{D}}_{0}$ strictly included in
$\bigcup_{{\mathfrak{R}}\in{\mathbf{A}}^{\perp}}\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$,
we have to erase at least a chronicle ${\mathfrak{c}}$ (and its extensions).
But there is at least a path
$\mathpzc{p}_{0}\in{\bigcup_{{\mathfrak{R}}\in{\mathbf{A}}^{\perp}}\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}\right>}$
such that
${\mathfrak{c}}\in\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}_{0}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$
hence if we denote by ${\mathfrak{R}}_{0}$ a net such that
$\mathpzc{p}_{0}=\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{R}}_{0}\right>$
we have by linearity constraint on designs that
${\mathfrak{D}}_{0}\not\perp{\mathfrak{R}}_{0}$. Hence
${\mathfrak{D}}_{0}\not\in{\mathbf{A}}$.

##  3 Visitable Paths and Logical Decomposition

In this section we relate MALL logical connectives, in fact $\otimes$,
$\oplus$,
$\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}$,
with operations on visitable paths. Operations $\oplus$ and
$\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}$
are quite immediate. The behaviour ${\mathbf{A}}\oplus{\mathbf{B}}$, is the
union of the two behaviours ${\mathbf{A}}$ and ${\mathbf{B}}$, hence visitable
paths of the result should be the union of the two sets of visitable paths.
The behaviour
$\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}{\mathbf{A}}$
is built by adding an identical action as root, hence visitable paths of the
resulting behaviour should be built by adding this action as prefix of
visitable paths of ${\mathbf{A}}$. As $\otimes$ models a kind of concurrency,
it is natural to consider that the set of visitable paths of a tensor should
be in some way the shuffle of the sets of underlying behaviours. However
belonging to the shuffle of visitable paths is not sufficient for being a
visitable path in the tensor of two behaviours as shown in the following
example.

###### Example 3.1

Let us consider behaviours ${\mathbf{A}}=\\{{\mathfrak{A}}\\}^{\perp\perp}$
and ${\mathbf{B}}=\\{{\mathfrak{B}}\\}^{\perp\perp}$ where:

${\mathfrak{A}}=\scalebox{0.8}{ \vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
19.13196pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\cr}}\nointerlineskip\kern
2.0pt\moveright 0.0pt\hbox{\hbox{$\textstyle\xi
10000\vdash$}}}\cr}}\nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule
width=38.26392pt}\nointerlineskip\kern 2.0pt\moveright
1.11116pt\hbox{$\textstyle\vdash\xi 1000$}}\cr}}\nointerlineskip\kern
2.0pt\moveright 1.11116pt\vbox{\hrule width=36.04161pt}\nointerlineskip\kern
2.0pt\moveright 5.00002pt\hbox{$\textstyle\xi
100\vdash$}}\cr}}\nointerlineskip\kern 2.0pt\moveright 5.00002pt\vbox{\hrule
width=28.26389pt}\nointerlineskip\kern 2.0pt\moveright
6.11118pt\hbox{$\textstyle\vdash\xi 10$}}\cr}}\nointerlineskip\kern
2.0pt\moveright 6.11118pt\vbox{\hrule width=26.04158pt}\nointerlineskip\kern
2.0pt\moveright 10.00003pt\hbox{$\textstyle\xi
1\vdash$}}\cr}}\nointerlineskip\kern 2.0pt\moveright 10.00003pt\vbox{\hrule
width=18.26385pt}\nointerlineskip\kern 2.0pt\moveright
11.11119pt\hbox{$\textstyle\vdash\xi$}} }$ and ${\mathfrak{B}}=\scalebox{0.8}{
\vbox{ \moveright 0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
0.0pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
13.29858pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\vbox{ \moveright
14.13194pt\vbox{\halign{\relax\global\@RightOffset=0pt
\@ReturnLeftOffsettrue$\inferstyle#$&& \inferTabSkip\global\@RightOffset=0pt
\@ReturnLeftOffsetfalse$\inferstyle#$\cr\textstyle\cr}}\nointerlineskip\kern
2.0pt\moveright 0.0pt\hbox{\hbox{$\textstyle\xi
210\vdash$}}}\cr}}\nointerlineskip\kern 2.0pt\moveright 0.0pt\vbox{\hrule
width=54.86107pt}\nointerlineskip\kern 2.0pt\moveright
0.0pt\hbox{$\textstyle\vdash\xi 2000,\xi 21$}}\cr}}\nointerlineskip\kern
2.0pt\moveright 0.0pt\vbox{\hrule width=54.86107pt}\nointerlineskip\kern
2.0pt\moveright 4.72221pt\hbox{$\textstyle\xi 200\vdash\xi
21$}}\cr}}\nointerlineskip\kern 2.0pt\moveright 4.72221pt\vbox{\hrule
width=45.41664pt}\nointerlineskip\kern 2.0pt\moveright
5.00002pt\hbox{$\textstyle\vdash\xi 20,\xi 21$}}\cr}}\nointerlineskip\kern
2.0pt\moveright 5.00002pt\vbox{\hrule width=44.86104pt}\nointerlineskip\kern
2.0pt\moveright 18.2986pt\hbox{$\textstyle\xi
2\vdash$}}\cr}}\nointerlineskip\kern 2.0pt\moveright 18.2986pt\vbox{\hrule
width=18.26385pt}\nointerlineskip\kern 2.0pt\moveright
19.40976pt\hbox{$\textstyle\vdash\xi$}} }$

Let us consider the path $\mathpzc{q}=$ $(+,\xi,\\{1,2\\})(-,\xi
2,\\{0,1\\})(+,\xi 20,\\{0\\})(-,\xi 1,\\{0\\})(+,\xi 10,\\{0\\})(-,\xi
200,\\{0\\})$ $(+,\xi 21,\\{0\\})(-,\xi 100,\\{0\\})(+,\xi 1000,\\{0\\})$ . We
have that $\mathpzc{q}$ is a path in ${\mathbf{A}}\otimes{\mathbf{B}}$ as
shown in Fig. 3 on the left (path in red). It is a shuffle of the two
following paths
– $\mathpzc{p}_{1}=$ $(+,\xi,\\{1,2\\})(-,\xi 2,\\{0,1\\})(+,\xi
20,\\{0\\})(-,\xi 200,\\{0\\})(+,\xi 21,\\{0\\})$
– $\mathpzc{p}_{2}=$ $(+,\xi,\\{1,2\\})(-,\xi 1,\\{0\\})(+,\xi
10,\\{0\\})(-,\xi 100,\\{0\\})(+,\xi 1000,\\{0\\})$
These two paths $\mathpzc{p}_{1}$ and $\mathpzc{p}_{2}$ are visitable
respectively in ${\mathbf{A}}$ and ${\mathbf{B}}$. However $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
is not a path. It suffices to prove that
$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$ $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$ is not a design. In fact
$\ulcorner$$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$$\urcorner$
is not even a chronicle:
$\raisebox{1.29167pt}{$\ulcorner$}{\makebox[5.27779pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$}}}\raisebox{1.29167pt}{$\urcorner$}=$
$(-,\xi,\\{1,2\\})(+,\xi 2,\\{0,1\\})(-,\xi 21,\\{0\\})(+,\xi
100,\\{0\\})(-,\xi 1000,\\{0\\}){\scriptstyle\maltese}$ and the justifier of
$\xi 100$ is not present in $\ulcorner$$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$$\urcorner$.
This may also be noticed in figure below on the right: $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
defines in blue a path in an object that cannot be completed to give rise to a
design with $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
fully present. Hence $\mathpzc{q}\not\in V_{{\mathbf{A}}\otimes{\mathbf{B}}}$.

$\textstyle\xi 10000\vdash$ $\textstyle\vdash\xi 1000$ $\textstyle\xi
100\vdash$ $\textstyle\vdash\xi 10$ $\textstyle\xi 1\vdash$ $\textstyle\xi
210\vdash$ $\textstyle\vdash\xi 2000,\xi 21$ $\textstyle\xi 200\vdash\xi 21$
$\textstyle\vdash\xi 20,\xi 21$ $\textstyle\xi 2\vdash$ $\textstyle\vdash\xi$

$\mathpzc{q}$

$\textstyle\xi 2000\vdash\xi 100$ $\textstyle\vdash\xi 100,\xi 200$
$\textstyle\xi 10\vdash\xi 200$ $\textstyle\vdash\xi 200,\xi 1$ $\textstyle\xi
20\vdash\xi 1$ $\textstyle\vdash\xi 210$ $\textstyle\xi 21\vdash$
$\textstyle\vdash\xi 1,\xi 2$ $\textstyle\xi\vdash$

$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$?

Figure 3: A path $\mathpzc{q}$ in the shuffle of two designs the dual
$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
of which is not a path.

###  3.1 Extension of a base

Extension is a technical trick to simplify the presentation of results on the
tensor $\otimes$ operation. In short, the extension is applied to positive
behaviours with a simple base $\vdash\xi$. The first action of designs of such
a behaviour is necessarily of the form $(+,\xi,I)$. The extension to $J$ is
the set of designs where the first action is replaced by $(+,\xi,I\cup J)$,
this operation is defined only when $J$ does not overlap any such $I$. Such an
operation does not change visitable paths. In fact, we conveniently present
the extension with respect to a behaviour or to a set of paths and not only to
a set of addresses $J$. We remind that two positive behaviours ${\mathbf{A}}$
and ${\mathbf{B}}$ are alien when the ramifications of the first actions of
designs belonging to ${\mathbf{A}}$ and the ramifications of the first actions
of designs belonging to ${\mathbf{B}}$ are pairwise disjoint.

######  Definition 3.2 (Extension)

Let ${\mathbf{A}}$ and ${\mathbf{B}}$ be alien positive behaviours of base
$\vdash\xi$.

  * •

The extension of ${\mathbf{A}}$ with respect to ${\mathbf{B}}$, denoted by
${\mathbf{A}}_{[{\mathbf{B}}]}$, is the set of designs ${\mathfrak{D}}$ such
that either ${\mathfrak{D}}={\mathfrak{Dai}}$ or there exist designs
${\mathfrak{A}}\in{\mathbf{A}}$ of first action $(+,\xi,I)$ and
${\mathfrak{B}}\in{\mathbf{B}}$ of first action $(+,\xi,J)$ and
${\mathfrak{D}}$ is obtained from ${\mathfrak{A}}$ by replacing its first
action by $(+,\xi,I\cup J)$.

  * •

Let $P$ (resp. $Q$) be a set of paths of ${\mathbf{A}}$ (resp.
${\mathbf{B}}$), the extension of $P$ with respect to $Q$, denoted by
$P_{[Q]}$, is the set of paths $\mathpzc{p}$ such that either
$\mathpzc{p}={\scriptstyle\maltese}$ or there exist paths $\mathpzc{r}\in P$
of first action $(+,\xi,I)$ and $\mathpzc{s}\in Q$ of first action $(+,\xi,J)$
and $\mathpzc{p}$ is obtained from $\mathpzc{r}$ by replacing its first action
by $(+,\xi,I\cup J)$.

###### Lemma 3.3

${\mathbf{A}}_{[{\mathbf{B}}]}$ is a behaviour.
$V_{({\mathbf{A}}_{[{\mathbf{B}}]})}=(V_{{\mathbf{A}}})_{[V_{\mathbf{B}}]}$.

  * Proof

It follows from the definition that $\mathpzc{p}$ is a path of
${\mathbf{A}}_{[{\mathbf{B}}]}$ iff $\mathpzc{p}$ is either the daimon or of
the form $(+,\xi,I\cup J)\mathpzc{q}$ where $(+,\xi,I)\mathpzc{q}$ is a path
of ${\mathbf{A}}$ and $(+,\xi,J)$ is the first action of a design of
${\mathbf{B}}$. Hence also a path in $({\mathbf{A}}_{[{\mathbf{B}}]})^{\perp}$
is either empty or begins with $(-,\xi,I\cup J)$.

Let ${\mathfrak{G}}\in|{\mathbf{A}}_{[{\mathbf{B}}]}^{\perp\perp}|$. For each
${\mathfrak{F}}\in{\mathbf{A}}_{[{\mathbf{B}}]}^{\perp}$, consider the path
$\left<{\mathfrak{G}}\\!\\!\leftarrow\\!\\!{\mathfrak{F}}\right>$: either it
is the daimon or it is of the form $(+,\xi,I\cup J)\mathpzc{p}_{\mathfrak{F}}$
where $(+,\xi,I)$ (resp. $(+,\xi,J)$) is a first action of a design of
${\mathbf{A}}$ (resp. ${\mathbf{B}}$). Remark that sequences $(+,\xi,I\cup
J)\mathpzc{p}_{\mathfrak{F}}$ are pairwise coherent paths. Hence it follows
from proposition 2.26 that
${\mathfrak{G}}=\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{{\mathfrak{Dai}}\cup\bigcup_{\mathfrak{F}}(+,\xi,I\cup
J)\mathpzc{p}_{\mathfrak{F}}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.
We note now that the design
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{{\mathfrak{Dai}}\cup\bigcup_{\mathfrak{F}}(+,\xi,I)\mathpzc{p}_{\mathfrak{F}}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$
is in the behaviour ${\mathbf{A}}$. Hence ${\mathfrak{G}}$ is in
${\mathbf{A}}_{[{\mathbf{B}}]}$. Thus
$|{\mathbf{A}}_{[{\mathbf{B}}]}^{\perp\perp}|\subset{\mathbf{A}}_{[{\mathbf{B}}]}$.
Note now that, ${\mathbf{A}}$ being a behaviour, let
${\mathfrak{D}}\in{\mathbf{A}}$, if ${\mathfrak{E}}$ is a design that includes
${\mathfrak{D}}$ then ${\mathfrak{E}}\in{\mathbf{A}}$. Hence also let
${\mathfrak{D}}\in{\mathbf{A}}_{[{\mathbf{B}}]}$, if ${\mathfrak{E}}$ is a
design that includes ${\mathfrak{D}}$ then
${\mathfrak{E}}\in{\mathbf{A}}_{[{\mathbf{B}}]}$. Thus
${\mathbf{A}}_{[{\mathbf{B}}]}^{\perp\perp}\subset{\mathbf{A}}_{[{\mathbf{B}}]}$.
It follows that ${\mathbf{A}}_{[{\mathbf{B}}]}$ is a behaviour.

From the previous reasoning, we deduce easily that
$V_{({\mathbf{A}}_{[{\mathbf{B}}]})}=(V_{{\mathbf{A}}})_{[V_{\mathbf{B}}]}$.

###  3.2 Visitability for Linear Operations on Behaviours

The interpretation of Multiplicative-Additive Linear Logic (MALL) in the
framework of Ludics is a real success. Not only are there full completeness
and soundness results but completeness is internal: product and sum of two
behaviours is a behaviour (without need for closing by bi-orthogonality the
result). In the original paper of Girard [10], these results are also achieved
for second-order, however we do not consider it in this paper. Before
establishing properties concerning visitability (proposition 3.6 and theorem
3.7), we recall below the main linear operations on behaviours: multiplicative
tensor ‘$\otimes$’, additive sum ‘$\oplus$’ and also the shift
‘$\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}$’
operation. The shift operation is required as the logics is polarized: it
allows for switching from/to a positive behaviour to/from a negative
behaviour. Dual operations are defined in a standard way:
${\mathbf{A}}\parr{\mathbf{B}}=({\mathbf{A}}\otimes{\mathbf{B}})^{\perp}$,
${\mathbf{A}}\with{\mathbf{B}}=({\mathbf{A}}\otimes{\mathbf{B}})^{\perp}$ and
$\mathinner{\mathchoice{\vbox{\hbox{$\shneg$}}}{\vbox{\hbox{$\shneg$}}}{\vbox{\hbox{$\shneg$}}}{\vbox{\hbox{$\shneg$}}}}{\mathbf{A}}=(\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}{\mathbf{A}})^{\perp}$.

###### Definition 3.4

  * •

Let ${\mathbf{G}}_{k}$ be a family of positive behaviours pairwise disjoint,
$\bigoplus_{k}{\mathbf{G}}_{k}=(\bigcup_{k}{\mathbf{G}}_{k})^{\perp\perp}$

  * •

Let ${\mathfrak{A}}$ and ${\mathfrak{B}}$ be two positive alien designs:
\- If ${\mathfrak{A}}$ or ${\mathfrak{B}}$ is ${\mathfrak{Dai}}$, then
${\mathfrak{A}}\otimes{\mathfrak{B}}={\mathfrak{Dai}}$.
\- Otherwise
${\mathfrak{A}}=\scalebox{0.9}{$(+,\xi,I)$}{\mathfrak{A}}^{\prime}$ and
${\mathfrak{B}}=\scalebox{0.9}{$(+,\xi,I)$}{\mathfrak{B}}^{\prime}$ then
${\mathfrak{A}}\otimes{\mathfrak{B}}=\scalebox{0.9}{$(+,\xi,I\cup
J)$}({\mathfrak{A}}^{\prime}\cup{\mathfrak{B}}^{\prime})$.

  * •

Let ${\mathbf{G}}$ and ${\mathbf{H}}$ be two positive alien behaviours,
${\mathbf{G}}\otimes{\mathbf{H}}=\\{{\mathfrak{A}}\otimes{\mathfrak{B}}\leavevmode\nobreak\
;\leavevmode\nobreak\
{\mathfrak{A}}\in{\mathbf{G}},{\mathfrak{B}}\in{\mathbf{H}}\\}^{\perp\perp}$

  * •

Let ${\mathbf{G}}$ be a negative behaviour of base $\xi i\vdash$,
$\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}{\mathbf{G}}=((+,\xi,\\{i\\}){\mathbf{G}})^{\perp\perp}$.

######  Theorem 3.5 (internal completeness [10])

  * •

Let $K\neq\emptyset$, $\bigoplus_{k\in K}{\mathbf{G}}_{k}=\bigcup_{k\in
K}{\mathbf{G}}_{k}$

  * •

A behaviour of positive base is always decomposable as a $\bigoplus$ of
connected behaviours.

  * •

Let ${\mathbf{G}}$ and ${\mathbf{H}}$ be two alien positive behaviours,
${\mathbf{G}}\otimes{\mathbf{H}}=\\{{\mathfrak{A}}\otimes{\mathfrak{B}}\leavevmode\nobreak\
;\leavevmode\nobreak\
{\mathfrak{A}}\in{\mathbf{G}},{\mathfrak{B}}\in{\mathbf{H}}\\}$.

  * •

Let ${\mathbf{G}}$ be a negative behaviour of base $\xi i\vdash$,
$\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}{\mathbf{G}}=\\{{\mathfrak{Dai}}\\}\cup(+,\xi,\\{i\\}){\mathbf{G}}$.

  * •

Ludics is fully sound and complete with respect to polarized multiplicative-
additive Linear Logic.

###### Proposition 3.6

Let ${\mathbf{A}}$ be a negative behaviour, then
$V_{\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}_{\xi
i}{\mathbf{A}}}=\\{{\scriptstyle\maltese}\\}\cup(+,\xi,\\{i\\})V_{\mathbf{A}}$.
Let $({\mathbf{A}}_{k})_{k\in K}$ be a family of pairwise disjoint positive
behaviours with $K\neq\emptyset$, then $V_{\bigoplus_{k\in
K}{\mathbf{A}}_{k}}=\biguplus_{k\in K}V_{{\mathbf{A}}_{k}}$.
Let ${\mathbf{A}}$ and ${\mathbf{B}}$ be alien positive behaviours, then
$V_{{\mathbf{A}}\otimes{\mathbf{B}}}=\\{\mathpzc{q}\leavevmode\nobreak\
;\leavevmode\nobreak\
\makebox[5.27779pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$}}$
is a path and $\mathpzc{q}\in
V_{{\mathbf{A}}_{[{\mathbf{B}}]}}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}V_{{\mathbf{B}}_{[{\mathbf{A}}]}}\\}$.

  * Proof

Let ${\mathbf{A}}$ be a negative behaviour with base $\xi i\vdash$.
$\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}_{\xi
i}{\mathbf{A}}$ is a behaviour then ${\scriptstyle\maltese}$ is visitable in
it. Let ${\mathfrak{E}}$ be a design of
$(\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}_{\xi
i}{\mathbf{A}})^{\perp}$ distinct from ${\mathfrak{Dai}}$. Note that the only
first proper action of designs of
$\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}_{\xi
i}{\mathbf{A}}$ is $(+,\xi,\\{i\\})$. Hence one can define
${\mathfrak{E}}^{\prime}=\\{{\mathfrak{c}}\leavevmode\nobreak\
;\leavevmode\nobreak\ (-,\xi,\\{i\\}){\mathfrak{c}}\in{\mathfrak{E}}\\}$. It
is immediate that ${\mathfrak{E}}^{\prime}$ is a design. As normalization is
deterministic, ${\mathfrak{E}}^{\prime}\in{\mathbf{A}}^{\perp}$. Reversely,
from a design ${\mathfrak{E}}^{\prime}\in{\mathbf{A}}^{\perp}$, one builds a
design
${\mathfrak{E}}=(-,\xi,\\{i\\}){\mathfrak{E}}^{\prime}\in(\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}_{\xi
i}{\mathbf{A}})^{\perp}$. Hence $\mathpzc{p}$ is a visitable path of
$\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}_{\xi
i}{\mathbf{A}}$ iff $\mathpzc{p}={\scriptstyle\maltese}$ or
$\mathpzc{p}=(+,\xi,\\{i\\})\mathpzc{p}^{\prime}$ where $\mathpzc{p}^{\prime}$
is a visitable path of ${\mathbf{A}}$.
Let $({\mathbf{A}}_{k})_{k\in K}$ be a family of disjoint positive behaviours
with base $\vdash\xi$.

    * –

Let $\mathpzc{p}\in V_{\bigoplus_{k\in K}{\mathbf{A}}_{k}}$: there exist
designs ${\mathfrak{D}}\in\bigoplus_{k\in K}{\mathbf{A}}_{k}$ and
${\mathfrak{E}}\in(\bigoplus_{k\in K}{\mathbf{A}}_{k})^{\perp}$ such that
$\mathpzc{p}=\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{E}}\right>$.
By the disjunction property, ([10], Th. 11), we have that $\bigoplus_{k\in
K}{\mathbf{A}}_{k}=\biguplus_{k\in K}{\mathbf{A}}_{k}$. Hence there exist
$k_{0}$ such that ${\mathfrak{D}}\in{\mathbf{A}}_{k_{0}}$ and
${\mathfrak{E}}\in\bigcap_{k\in K}{\mathbf{A}}_{k}^{\perp}$, so in particular
${\mathfrak{E}}\in{\mathbf{A}}_{k_{0}}^{\perp}$. Thus $\mathpzc{p}\in
V_{{\mathbf{A}}_{k_{0}}}\subset\biguplus_{k\in K}V_{{\mathbf{A}}_{k}}$.

    * –

Let $\mathpzc{p}\in\biguplus_{k\in K}V_{{\mathbf{A}}_{k}}$. Hence there exist
$k_{0}\in K$ such that $\mathpzc{p}\in V_{{\mathbf{A}}_{k_{0}}}$: there exist
designs ${\mathfrak{D}}\in{\mathbf{A}}_{k_{0}}$ and
${\mathfrak{E}}\in{\mathbf{A}}_{k_{0}}^{\perp}$ such that
$\mathpzc{p}=\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{E}}\right>$.
As behaviours ${\mathbf{A}}_{k}$ are pairwise disjoint, we can add to
${\mathfrak{E}}$ (or replace) chronicles of the form
$(-,\xi,I){\scriptstyle\maltese}$ where $I$ is in the directory of
${\mathbf{A}}_{k}$, $k\neq k_{0}$, to get a design ${\mathfrak{E}}^{\prime}$.
Hence ${\mathfrak{E}}^{\prime}\in\bigcap_{k\in K}{\mathbf{A}}_{k}^{\perp}$ and
$\mathpzc{p}=\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{E}}^{\prime}\right>$.
Thus $\mathpzc{p}\in V_{\bigoplus_{k\in K}{\mathbf{A}}_{k}}$.

Let ${\mathbf{A}}$ and ${\mathbf{B}}$ be alien positive behaviours with base
$\vdash\xi$.

    * –

Let $\mathpzc{p}\in V_{{\mathbf{A}}\otimes{\mathbf{B}}}$. As $\mathpzc{p}$ is
a visitable path, $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
is a path. Furthermore there exist designs
${\mathfrak{D}}\in{\mathbf{A}}\otimes{\mathbf{B}}$ and
${\mathfrak{E}}\in({\mathbf{A}}\otimes{\mathbf{B}})^{\perp}$ such that
$\mathpzc{p}=\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{E}}\right>$.
Using the independence property ([10], Th. 20), there exist designs
${\mathfrak{D}}_{1}\in{\mathbf{A}}$ and ${\mathfrak{D}}_{2}\in{\mathbf{B}}$
such that ${\mathfrak{D}}={\mathfrak{D}}_{1}\otimes{\mathfrak{D}}_{2}$.
If $\mathpzc{p}={\scriptstyle\maltese}$, then $\mathpzc{p}\in
V_{{\mathbf{A}}_{[{\mathbf{B}}]}}$. So let us consider the other cases, i.e.,
designs ${\mathfrak{D}}_{1}$ and ${\mathfrak{D}}_{2}$ are distinct from
${\mathfrak{Dai}}$.
Let $(+,\xi,I)$ (resp. $(+,\xi,J)$) be the first action of
${\mathfrak{D}}_{1}$ (resp. ${\mathfrak{D}}_{2}$). Behaviours being alien, we
have that $I\cap J=\emptyset$. Note that each action of $\mathpzc{p}$ is
either $(+,\xi,I\cup J)$, or an action of design ${\mathfrak{D}}_{1}$ or an
action of design ${\mathfrak{D}}_{2}$, the three cases being exclusive of one
another.
Let $\mathpzc{p}_{1}:=(+,\xi,I)\mathpzc{q}_{1}$ (resp.
$\mathpzc{p}_{2}:=(+,\xi,J)\mathpzc{q}_{2}$) where $\mathpzc{q}_{1}$ (resp.
$\mathpzc{q}_{2}$) is the subsequence of $\mathpzc{p}$ made of actions of
${\mathfrak{D}}_{1}$ (resp. ${\mathfrak{D}}_{2}$). Following the adjunction
theorem ([10], Th. 14), we have that
${\mathfrak{D}}_{1}\perp({\mathfrak{E}}){\mathfrak{D}}_{2}$ with
$({\mathfrak{E}}){\mathfrak{D}}_{2}$ independent from ${\mathfrak{D}}_{1}$,
i.e., $({\mathfrak{E}}){\mathfrak{D}}_{2}\in{\mathbf{A}}^{\perp}$. Similarly,
$({\mathfrak{E}}){\mathfrak{D}}_{1}\in{\mathbf{B}}^{\perp}$. Note that
$\mathpzc{p}_{1}=\left<{\mathfrak{D}}_{1}\\!\\!\leftarrow\\!\\!({\mathfrak{E}}){\mathfrak{D}}_{2}\right>\in
V_{\mathbf{A}}$ and
$\mathpzc{p}_{2}=\left<{\mathfrak{D}}_{2}\\!\\!\leftarrow\\!\\!({\mathfrak{E}}){\mathfrak{D}}_{1}\right>\in
V_{\mathbf{B}}$. Finally remark that $\mathpzc{p}\in(+,\xi,I\cup
J)\mathpzc{q}_{1}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}(+,\xi,I\cup
J)\mathpzc{q}_{2}$ (as jumps are on negative actions). Hence $\mathpzc{p}\in
V_{{{\mathbf{A}}_{[{\mathbf{B}}]}}}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}V_{{{\mathbf{B}}_{[{\mathbf{A}}]}}}$.

    * –

Let $\mathpzc{p}\in V_{\mathbf{A}}$, $\mathpzc{p}^{\prime}\in V_{\mathbf{B}}$.
If one of the two paths $\mathpzc{p}$ or $\mathpzc{p}^{\prime}$ is the daimon,
then their shuffle is the daimon, hence in
$V_{{\mathbf{A}}\otimes{\mathbf{B}}}$. Otherwise,
$\mathpzc{p}=(+,\xi,I)\mathpzc{p}_{1}$ and
$\mathpzc{p}^{\prime}=(+,\xi,J)\mathpzc{p}^{\prime}_{1}$. As $\mathpzc{p}\in
V_{\mathbf{A}}$, there exist designs ${\mathfrak{D}}\in{\mathbf{A}}$ and
${\mathfrak{E}}\in{\mathbf{A}}^{\perp}$ such that
$\mathpzc{p}=\left<{\mathfrak{D}}\\!\\!\leftarrow\\!\\!{\mathfrak{E}}\right>$.
Similarly there exist designs ${\mathfrak{D}}^{\prime}\in{\mathbf{B}}$ and
${\mathfrak{E}}^{\prime}\in{\mathbf{B}}^{\perp}$ such that
$\mathpzc{p}^{\prime}=\left<{\mathfrak{D}}^{\prime}\\!\\!\leftarrow\\!\\!{\mathfrak{E}}^{\prime}\right>$.
Let $\mathpzc{q}\in(+,\xi,I\cup
J)\mathpzc{p}_{1}{\,\mathchoice{\leavevmode\vtop{\halign{\hfil$\displaystyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\textstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}{\leavevmode\vtop{\halign{\hfil$\scriptscriptstyle#$\hfil\cr\sqcup\cr\rule{0.3pt}{6.5pt}\crcr}}}\,}(+,\xi,I\cup
J)\mathpzc{p}^{\prime}_{1}$ such that $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$
is a path. We will prove that $\mathpzc{q}$ which is a path of
${\mathfrak{D}}\otimes{\mathfrak{D}}^{\prime}$ is visitable in
${\mathbf{A}}\otimes{\mathbf{B}}$. Let us consider the design
${\mathfrak{G}}:=\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.27779pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$}}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$.
We prove by contradiction that
${\mathfrak{G}}\in({\mathbf{A}}\otimes{\mathbf{B}})^{\perp}$. Let
${\mathfrak{F}}\in{\mathbf{A}}$ and ${\mathfrak{F}}^{\prime}\in{\mathbf{B}}$.
Suppose that
${\mathfrak{F}}\otimes{\mathfrak{F}}^{\prime}\not\perp{\mathfrak{G}}$. Notice
that, since a slice of ${\mathfrak{G}}$ is finite, it is not possible that the
interaction between ${\mathfrak{G}}$ and
${\mathfrak{F}}\otimes{\mathfrak{F}}^{\prime}$ would be infinite. Let
$\mathpzc{r}$ be the sequence of actions of
${\mathfrak{F}}\otimes{\mathfrak{F}}^{\prime}$ used during the normalization
before divergence. We consider the two cases of non-convergence, due to the
fact that the next (proper positive) action in one of the designs has no dual
in the other design:
– action $\kappa^{+}$ in ${\mathfrak{F}}$ or ${\mathfrak{F}}^{\prime}$ and
$\overline{\kappa^{+}}\not\in{\mathfrak{G}}$: this contradicts the
construction of ${\mathfrak{G}}$.
– action $\kappa^{+}$ in ${\mathfrak{G}}$ and
$\overline{\kappa^{+}}\not\in{\mathfrak{F}}\otimes{\mathfrak{F}}^{\prime}$. By
construction of ${\mathfrak{G}}$,
$\kappa^{+}\in\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\makebox[5.27779pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$}}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.
Hence
$\overline{\kappa^{+}}\in\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{q}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.
Notice that
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{q}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$
is a slice, hence $\kappa^{+}$ appears only once in
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{q}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.
Thus, w.l.o.g., $\overline{\kappa^{+}}$ appears in
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\mathpzc{p}}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.
Let $\mathpzc{r}_{1}$ the subsequence of $\mathpzc{r}$ followed in
${\mathfrak{F}}$. Remark that
$\mathpzc{r}_{1}\in\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\,\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$}}\,}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$,
hence also
$\mathpzc{r}_{1}\kappa^{+}\in\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\,\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$}}\,}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}$.
The design $\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$ $\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$
$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$ is included in ${\mathfrak{E}}$,
then by proposition 2.22, the design
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\,\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$}}\,}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}$
belongs to ${{\mathbf{A}}}^{\perp}$, then,
$\raisebox{1.29167pt}{$\ulcorner\mkern-6.0mu\ulcorner\mkern-2.0mu$}{\,\makebox[5.55557pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.55557pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{p}}}$}}\,}\raisebox{1.29167pt}{$\mkern-2.0mu\urcorner\mkern-6.0mu\urcorner$}^{c}\perp{\mathfrak{F}}$
, hence a contradiction.
Thus ${\mathfrak{F}}\otimes{\mathfrak{F}}^{\prime}\perp{\mathfrak{G}}$.
Finally, by construction, we have that
$\mathpzc{q}=\left<{\mathfrak{D}}\otimes{\mathfrak{D}}^{\prime}\\!\\!\leftarrow\\!\\!{\mathfrak{G}}\right>$.
So $\mathpzc{q}\in V_{{\mathbf{A}}\otimes{\mathbf{B}}}$.

###### Theorem 3.7

Let ${\mathbf{P}}$ be a positive behaviour, ${\mathbf{N}}$ be a negative
behaviour, $({\mathbf{P}}_{k})_{k\in K}$ be a family of pairwise disjoint
positive behaviours with $K\neq\emptyset$, ${\mathbf{Q}}_{1}$ and
${\mathbf{Q}}_{2}$ be positive behaviours.
– $V_{\mathbf{P}}=\\{{\mathfrak{Dai}}\\}\cup(+,\xi,\\{i\\})V_{\mathbf{N}}$ iff
${\mathbf{P}}=\mathinner{\mathchoice{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}{\vbox{\hbox{$\shpos$}}}}_{\xi
i}{\mathbf{N}}$.
– $V_{{\mathbf{P}}}=\biguplus_{k\in K}V_{{\mathbf{P}}_{k}}$ iff
${\mathbf{P}}=\bigoplus_{k\in K}{\mathbf{P}}_{k}$.
– $V_{{\mathbf{P}}}=\\{\mathpzc{q}\leavevmode\nobreak\ ;\leavevmode\nobreak\
\makebox[5.27779pt][c]{\mbox{\rule{0.0pt}{4.30554pt}$\mathchoice{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}{\hbox
to0.0pt{\raisebox{4.30554pt}{$\leavevmode\resizebox{5.27779pt}{0.0pt}{$\sim$}$}\hss}{\mathpzc{q}}}$}}$
is a path and $\mathpzc{q}\in