Annex_open_modules.tex
\subsection{Open modules: properties of the contraction relation without completion}

\begin{proposition}[stability]\label{propStability}
Let $M$ be an \om\ st $M\wcontract M'$. 
The following properties are stable wrt contraction rules:
\begin{enumerate}
\item border set, i.e. $b(M')=b(M)$,
\item acyclicity, 
\item connexity,
\item connectablility,
\item c-correction,
\item o-correction.
\end{enumerate}
\end{proposition}

\begin{proof}
By the trivial cases of 1., 2. and 3. we have the stability of c-correction.
Regarding stability of connectability, remark that if 
$M$ is connectable by $\overline{M}$ then from 1. and 3. $M'$ is connectable by
$\widetilde{M}\circ M'$. By the way o-correction is stable wrt contraction
rules.\hfill $\qed$
\end{proof}

\begin{proposition}[inverse stability]
Let $M$ be an \om\ st $M\wcontract M'$. 
The properties of the proposition \ref{propStability} are stable wrt inverse contraction rules.
\end{proposition}

The proof uses the same arguments.

%\begin{theorem}[connectability]\label{thmConnectability}
%Let $M$ be an \om . The following statments are equivalent:
%\begin{enumerate}
%\item $M$ is connectable,
%\item $M\notcontract\notcc$.
%\item $M$ is a normal form wrt $\wcontract$ and $\notcc\not\in M$, or\\
%      there is $M'$ st $M\wcontract^1 M'$ and $M'$ is connectable.
%\end{enumerate}
%\end{theorem}
%
%\begin{proof} %
%1. $\Rightarrow$ 2. Remind that if $M$ is connectable then it is also the case for each contracted EBM of $M$. Moreover if $M$ is connectable then $\notcc\not\in M$. Over. 
%If $M$ is a normal form then 
%$\notcc\not\in M$ otherwise for every closure of $M$ there is a switch $s$ st
%$s(M)$ is not connected. Contradiction. If there is a $M'$ st 
%$M\wcontract^1 M'$ then by stability $M'$ is connectable.\\
%3. $\Rightarrow$ 2. If $M$ is a normal form and $\notcc\not\in M$ then 2. 
%holds. If there is $M'$ st $M\wcontract^1 M'$ and $M'$ is connectable then
%$M$ is connectable by inverse
%stability of connectability. And 1. $\Rightarrow$ 2.\\
%2. $\Rightarrow$ 1. If $M\notcontract\notcc$ then one can build $C\circ M$ a
%connected closure of $M$ st the module $C$ is acyclic. Let $m$ be the normal
%form of $M$ wrt $\wcontract$. There are two cases:
%\begin{itemize}
%\item[-] There is no negative pole in $m$ i.e. $m$ is a set of contracted
%  nodes. let $C_0$ be an EBM with only one negative pole
%linked to exactly one variable of each node of $m$ and let a set of inital or
%final EBM with only one variable, for each free variable of $m$. We have
%$m\circ C_0$ is an acyclic and connected closure of $m$. Then by reverse
%stability, $M\circ C_0$ is an acyclic and connected closure of $M$ st
%$\widetilde{M} =C_0$ is acyclic.
%\item[-] There is at least one negative pole. Consider $N_1$ a maximal one, we
%  have: 
%\begin{center}
%\input{Figures/figure_thmCble1}
%\end{center}
%with $\alpha\geqslant 0$ and for each $i$ we have 
%$\beta_i +\gamma_i\geqslant 1$ otherwise there is a contradiction with 
%$\notcc\not\in M $. 
%
%Let $N_1^+$ the following completion of $N_1$: for each $i$  let $b_i$ be one
%of the $\beta_i$, 
%\begin{center}
%\input{Figures/figure_thmCble2}
%\end{center}
%The module $N_1\circ N_1^+$ contracts in a form without negative pole:
%%% METTRE LE DESSIN DE N1oN1+ ->c
%\begin{center}
%FIGURE
%%\input{Figures/figure_thmCble3}
%\end{center}
%
%By iteration on the normal form of $m\circ N_1^+$ we get a
%set $\{ N_j^+\}_{j\in J}$ st $m\circ (\circ_J N_j^+)$ is without negative
%pole. We can then make completion with $C_0$: $m\circ (\circ_J
%N_j^+)\circ C_0$ is a \cm\ which contracts in a simple contracted node. By
%reverse stability of c-correction this is a c-correct module. Moreover by
%reverse stability $M\circ (\circ_J N_j^+)\circ C_0$ is c-correct. Then $M$
%is connectable.
%\end{itemize}
%\end{proof}
%
%FROM AN ONOTHER OLD VERSION:
%
%\bigskip
%
%We use the shorter notation $M\notcontract\notcc$ for the following property:
%\begin{center}
%$\notcc\not\in M$ and there is no $M'$ st $M\wcontract M'$ and $\notcc\in M'$.
%\end{center}
%
%Obviously, if $\notcc\in M$ then $M$ is not connectable as we can define a not connected switched module for every extension of $M$.




%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "MBE4"
%%% End: 


Annex_closed_modules1.tex

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%	PROOFNETS
\subsection{Proofnets}

Girard in his seminal paper~\cite{Girard87} gave a parallel syntax for multiplicative linear logic as oriented graphs called {\em proof-nets}. A {\em correctness criterion} enables one to distinguish sequentializable proof-structures (say such oriented graphs) from "bad" structures.

%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%

\begin{definition}[Proof structure]
A {\em proof structure} is a graph whose vertices are labelled with formulae and built from the following links (i.e. graphs):


\begin{itemize}
\item \parbox{.58\textwidth}{Axiom-link (two conclusions, no premise)}
\ 
\parbox{.10\textwidth}{\fullcenter{\resizebox{.10\textwidth}{!}{\input{Annex/Figures/axiom_link}}}}
\item \parbox{.58\textwidth}{Cut-link (two premises, no conclusion)}
\ 
\parbox{.30\textwidth}{\fullcenter{\resizebox{.10\textwidth}{!}{\input{Annex/Figures/cut_link}}}}
\item \parbox{.58\textwidth}{$\otimes$-link (two premises, one conclusion)}
\ 
\parbox{.10\textwidth}{\fullcenter{\resizebox{.10\textwidth}{!}{\input{Annex/Figures/times_link}}}}
\item \parbox{.58\textwidth}{$\Par$-link (two premises, one conclusion)}
\ 
\parbox{.30\textwidth}{\fullcenter{\resizebox{.10\textwidth}{!}{\input{Annex/Figures/par_link}}}}
\item \parbox{.58\textwidth}{$1$-link (no premise, one conclusion)}
\ 
\parbox{.10\textwidth}{\fullcenter{$1$}}
\end{itemize}
and every occurrence of a formula is a premise of at most one link and is a conclusion of exactly one link.

For every link $l$, a set $\mathcal S(l)$ of graphs called {\em Switching positions} is given. $\mathcal S(l) = \{l\}$ except when $l$ is a $\Par$-link. $\mathcal S(\Par$-link$)$ is defined by the two following switches:

\hfill
$\Par_L$:
\heightcenter{\resizebox{.10\textwidth}{!}{\input{Annex/Figures/par_switchL}}}
\hfill
$\Par_R$:
\heightcenter{\resizebox{.10\textwidth}{!}{\input{Annex/Figures/par_switchR}}}
\hfill\ 


A {\em switching} $s$ of a proof-structure $\Theta$ is a function which associates a switching position $s(l) \in \mathcal S(l)$ to every link $l$ of $\Theta$. The {\em switched proof-structure} $s(\Theta)$ is the graph with vertices the formulae labelling $\Theta$, and edges the ones given by the switching function $s$.

A {\em Danos-Regnier proof-net} is a proof-structure st each switched proof-structure is a tree, i.e. a connected and acyclic graph.
\end{definition}

We recall:
\begin{theorem}
A proof structure $\Theta$ is a Danos-Regnier proof net with conclusions $\Gamma$ iff there exists a proof $\pi$ of the sequent $\vdash \Gamma$ in multiplicative linear logic. Furthermore, one may define a correspondence between proofs and proof-nets.
\end{theorem}

Annex_closed_modules2.tex


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%	SEQUENT CALCULUS
\subsection{Sequent calculus style / Reduction by small steps}

%\begin{definition}[Congruence]
Let $\leadsto_C$ be the transitive closure of the following relation defined on literals of a formula $C$: let $u$ and $v$ be two literals of $C$, $u \leadsto_C v$ iff $\exists G, H$ st $C$ is of the form $C[G[u^{\bot}] \Par H[v]]$. We note $u\leadsto v$ when there is no ambiguity.
%\end{definition}

\begin{definition}[Small step reduction rule]
Let $\rightarrow$ be the reduction relation given by: 
$$C[\phi[x] \otimes \psi[x^\bot]] \rightarrow C[\phi[\psi[\bot]]] $$
if $\forall v \in fv(\psi[.]), v\not\leadsto_C x$.
\end{definition}


\begin{theorem}[Stability]
Let $x$ and $x^\bot$ appear only once in $C$, if $C[\phi[x] \otimes \psi[x^\bot]] \vdash$ is provable and the reduction rule applies, then $C[\phi[\psi[\bot]]] \vdash$ is provable.
\end{theorem}

\begin{proof} The proof consists in five main steps. In a first part we sketch the steps and give clues for the simplest ones. In a second part, we detail the more complex second step.
\begin{itemize}
\item The five steps:
\begin{enumerate}
\item a proof $\pi$ of $C[\phi[x] \otimes \psi[x^\bot]] \vdash$ exists then $\pi$ is of the form:
$$
\infer*[(1)]{C[\phi[x] \otimes \psi[x^\bot]] \vdash}
	{\infer*{\mathcal S, \phi[x], \psi[x^\bot] \vdash}{}}
$$
where $\pi'$ is the subproof of $\pi$ with conclusion $\mathcal S, \phi[x], \psi[x^\bot] \vdash$, where $\mathcal S$ is a multiset of formulae. The proof is done by recurrence (note that the language is only multiplicative).
\item a proof $\pi'$ of $\mathcal S, \phi[x], \psi[x^\bot] \vdash$ exists then there exists $\pi''$, proof of $\mathcal S, \phi[x], \psi[x^\bot] \vdash$ of the form:
$$
\infer*[(2)]{\mathcal S, \phi[x], \psi[x^\bot] \vdash}
	{\infer*{\mathcal T, x, \psi[x^\bot] \vdash}{}}
$$
we delay the proof of this step below.
\item a proof $\rho$ of $\mathcal T, x, \psi[x^\bot] \vdash$ exists then a proof $\nu$ of $\mathcal T, \psi[\bot] \vdash$ exists: the variable $x$ appears only once in the proof $\rho$, then this proof is of the form (the language is only multiplicative):
$$
\infer*{\mathcal T, x, \psi[x^\bot] \vdash}
	{\cdots
	& \infer{x, x^\bot \vdash}{}
	}
$$
Hence, by recurrence one may build a proof $\nu$ of the form:
$$
\infer*{\mathcal T, \psi[\bot] \vdash}
	{\cdots
	& \infer{\bot \vdash}{}
	}
$$
\item a proof $\nu$ of $\mathcal T, \psi[\bot] \vdash$ exists, then a proof of $\mathcal S, \phi[\psi[\bot]] \vdash$ exists: one completes the proof $\nu$ with the inference steps used in (2) (this may be proved by recurrence on the number of inference steps). 
\item a proof of $\mathcal S, \phi[\psi[\bot]] \vdash$ exists then a proof of $C[\phi[\psi[\bot]]] \vdash$ exists: as the step before, inference steps in (1) may now be applied to get the result.
\end{enumerate}
\item proof of the second step: briefly speaking, we transform the proof $\pi'$ by commuting rules with subformulae of $\psi[]$ or $\mathcal S$ as principal formula with rules with $\phi[]$ as principal formula in order to decompose $\phi[]$ before $\psi[]$ (reading the proof bottom-up). The constraint makes it possible. The demonstration is done by induction on the height of the proof and in three steps:
\begin{enumerate}
\item We mark formulae in the proof $\pi'$ in the following way:
\begin{itemize}
\item we mark $\bar{A}$ each formula $A$ that is a subformula of a formula containing a literal $w$ st $w\in \psi[]$ or $\exists v \in \psi[], v \leadsto w$.
\item we mark $\tilde{A}$ each formula $A$ that is a subformula of a formula containing a literal $w$ st $w\in \phi[]$ or $w \leadsto x$. 
Note that $\psi[]$ cannot be marked with $\tilde{.}$ because of the constraint. Suppose that a formula $A$ has two marks then it must be of the form $\bar{A_1} \otimes \tilde{A_2}$ and $A_1$ and $A_2$ have no other marks because of the constraint. Because $\otimes_L$ is asynchronous we can decompose first such a formula (that is different from $\psi[]$ as we noted above). Hence we consider for the following that a formula is not marked simultaneously $\tilde{.}$ and $\bar{.}$.
\item we mark $\dot{A}$ a formula unmarked by the two previous rules.
\end{itemize}
\item We prove now a one step inversion property (remember we "read" the proof bottom-up):
\begin{itemize}
\item if $\pi'$ contains a rule on a formula marked $\bar{.}$ followed by a rule $\otimes_L$ on a formula marked $\tilde{.}$ or $\dot{.}$, one may commute the two inferences: $\otimes_L$ is asynchronous and the marks being different, the formulae are distinct.
\item if $\pi'$ contains a rule $\Par_L$ on a formula marked $\bar{.}$ followed by a rule $\Par_L$ on a formula marked $\tilde{.}$ or $\dot{.}$, one may commute the two inferences: use either the associativity of $\Par_L$ if the inferences are done on the same formula or the fact that contexts are splitted independently.
\item if $\pi'$ contains a rule $\otimes_L$ on a formula marked $\bar{.}$ followed by a rule $\Par_L$ on a formula marked $\tilde{.}$, one may commute the two inferences: there are really two cases,
$$
\infer[\otimes_L]{\overline{a\otimes b}, \bar{B_1}, \bar{B_2}, \widetilde{\alpha \Par \beta}, \tilde{C_1}, \tilde{C_2}, \dot{D_1}, \dot{D_2} \vdash}
	{\infer[\Par]{\bar{a}, \bar{b}, \bar{B_1}, \bar{B_2}, \widetilde{\alpha \Par \beta}, \tilde{C_1}, \tilde{C_2}, \dot{D_1}, \dot{D_2} \vdash}
		{
		\bar{a}, \bar{B_1}, \tilde{\alpha}, \tilde{C_1}, \dot{D_1} \vdash
		&
		\bar{b}, \bar{B_2}, \tilde{\beta}, \tilde{C_2}, \dot{D_2} \vdash
		}
	}
$$
or
$$
\infer[\otimes_L]{\overline{a\otimes b}, \bar{B_1}, \bar{B_2}, \widetilde{\alpha \Par \beta}, \tilde{C_1}, \tilde{C_2}, \dot{D_1}, \dot{D_2} \vdash}
	{\infer[\Par]{\bar{a}, \bar{b}, \bar{B_1}, \bar{B_2}, \widetilde{\alpha \Par \beta}, \tilde{C_1}, \tilde{C_2}, \dot{D_1}, \dot{D_2} \vdash}
		{
		\bar{B_1}, \tilde{\alpha}, \tilde{C_1}, \dot{D_1} \vdash
		&
		\bar{a}, \bar{b}, \bar{B_2}, \tilde{\beta}, \tilde{C_2}, \dot{D_2} \vdash
		}
	}
$$
But one of two premises does not contain formulae marked $\bar{.}$ (the one without $x$ and $x^\bot$), hence the first one is not allowed. Then the commutation property follows.
\item other cases are treated easily.
\end{itemize}
\item we end with a classical induction on the height of the proof to show that
decomposition of $\tilde{.}$-formulae may be done before decomposition of
$\bar{.}$-formulae.\hfill $\qed$
\end{enumerate}
\end{itemize}
\end{proof}



\begin{theorem}[Inverse Stability]
If $C[\phi[\psi[\bot]]] \vdash$ is provable, then $C[\phi[x] \otimes \psi[x^\bot]] \vdash$ is provable.
\end{theorem}

\begin{proof}
If $C[\phi[\psi[\bot]]] \vdash$ is provable then there exists a proof of the following form (where $\mathcal S$ and $\mathcal T$ are multisets of formulae):
$$
\infer*{C[\phi[\psi[\bot]]] \vdash}
	{
	\infer*{\mathcal S, \phi[\psi[\bot]] \vdash}
		{
		\infer*{\mathcal T, \psi[\bot]] \vdash}
			{
			\infer{\bot \vdash}{}
			}
		}
	}
$$
As $x, x^\perp \vdash$ is provable, one may prove by induction on the height of the proof (applying the previous inference steps) that there exists a proof of the following form:
$$
\infer*{C[\phi[x] \otimes \psi[x^\bot]] \vdash}
	{
	\infer{\mathcal S, \psi[x^\perp]\otimes\phi[x] \vdash}
		{
		\infer*{\mathcal S, \psi[x^\perp], \phi[x] \vdash}
			{
			\infer*{\mathcal T, \psi[x^\perp], x \vdash}
				{
				\infer{x, x^\perp \vdash}{}
				}
			}
		}
	}
$$\hfill $\qed$
\end{proof}

\begin{theorem}[(small steps) Correctness criterion]
Let $M$ be a closed module, $M$ is c-correct iff $t(M) \rightarrow^* \bot$, where $\rightarrow^*$ is the transitive closure of $\rightarrow$, quotiented by the neutrality of $\bot$ wrt $\Par$.
\end{theorem}

\begin{proof}
The proof relies on stability and inverse stability. Let $M$ be a closed module.
\begin{itemize}
\item $\bot$ is the type of a c-correct module, hence by inverse stability, if $t(M)$ reduces to $\bot$, $M$ is c-correct.
\item Suppose $M$ is c-correct. The proof is done by induction on the number of variables appearing in $M$.
	\begin{itemize}
	\item If $t(M)$ does not contain variables, $t(M)$ is of the form $\bot$, $\bot\Par F$ or $\bot\otimes F$ where $F$ is built with $\bot, \Par$ and $\otimes$. The last case is not provable hence contradicting the fact that $M$ is c-correct. The second case is equivalent to $F$ (neutrality of $\bot$ wrt $F$). We conclude by induction on the number of symbols appearing in $t(M)$.
	\item If $t(M)$ contains variables. Remember that $t(M)$ is of the form $\bigotimes (\bigPar_{\!\!i} h_i^\perp \Par \bigPar_{\!\!k} \bigotimes_{j_k} c^{j_k}_k)$. As $t(M) \vdash$ is provable, there exists a polarized proof where each step is a complete decomposition of a formula
corresponding to an elementary module (one of the elements of the tensor). Let us now consider one of the last (when we read the proof bottom-up) polarized decomposition, it has the following form:
$$
\infer{\dots,x_l, \dots, \bigPar_{\!\!l} x_l^\perp \vdash}
	{
	\dots
	&
	\infer{x_l,x_l^\perp \vdash}{}
	&
	\dots
	}
$$
Remark that the remainder of the proof does not contain with $\bigPar_{\!\!l} x_l^\perp$ as one premise an application of (i) a $\otimes$ except for the last step because $M$ is a composition of elementary modules, (ii) a $\Par$ because the proof is polarized. If $t(M)\vdash$ is obtained by application of a tensor rule, then the reduction rule applies considering whatever literal $x_l$. Otherwise, the previous proof follows with a polarized step $\otimes$ then $\Par$:
$$
\infer*{t(M) \vdash}
	{
	\infer[\{j\}\cup\{j'\}=\{l\}]{\dots, y \Par \bigotimes_j x_l^j, \dots, \bigPar_{\!\!j} x_l^{j\perp} \Par \bigPar_{\!\!j'} x_l^{j'\perp}, \dots\vdash}
		{
		\infer{\dots,x_l, \dots, \bigPar_{\!\!l} x_l^\perp \vdash}
			{
			\dots
			&
			\infer{x_l,x_l^\perp \vdash}{}
			&
			\dots
			}
		}
	}
$$ 
Then $t(M)$ is of the form $C[\psi[\bigotimes_j x_l^j]\otimes(\bigPar_{\!\!j} x_l^{j\perp} \Par \bigPar_{\!\!j'} x_l^{j'\perp})]$ for each $l$. The reduction criterion is satisfied for each $x_l^j$ hence the reduction rule applies. Finally, we note that the formula we get after reduction (and possibly using the neutrality of $\bot$ wrt $\Par$) is the type of the composition of elementary modules.
	\hfill $\qed$\end{itemize}
\end{itemize}
\end{proof}


Annex_closed_modules3.tex


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%	NET / SMALL STEPS
\subsection{(standard) Proof-net style / Small steps}

The correctness of (closed) modules may be tested by means of a contraction criterion. In this subsection, we consider that modules are represented as proof structures and we use extensively the Danos-Regnier criterion to test that a proof-structure is correct. Let $\leadsto_\Theta$ be the transitive closure of the following relation defined on literals of a proof-structure $\Theta$: let $u$ and $v$ be two literals of $\Theta$, $u \leadsto_{\Theta} v$ iff $u^\bot$ and $v$ are in the same subtree with root $\otimes$ of the formula corresponding to $\Theta$. We note $u\leadsto v$ when there is no ambiguity.
In the following, we consider proof-structures modulo neutrality of the constant $\mathbf 1$ and associativity of connective $\Par$.

\begin{definition}[Small step reduction rule]
Let $\rightarrow$ be the reduction relation given by: 

\begin{figure}[h]
\begin{center}
\begin{tabular}{ccc}
\heightcenter{\input{Annex/Figures/redNet1}}
& \heightcenter{$\longrightarrow$}
& \heightcenter{\input{Annex/Figures/redNet2}}
\end{tabular}
\end{center}
\end{figure}

when $\forall v$ a literal of $\psi$, $v\not\leadsto x^\perp$
\end{definition}

\begin{theorem}[Stability]
Let $\Theta$ be a proof-structure, if $\Theta$ is DR-correct and $\Theta \rightarrow \Theta'$ then $\Theta'$ is DR-correct.
\end{theorem}

%%%%%%%%%%%%%%%%%			SMALL STEPS stability

\begin{proof}
Let $\Theta$ be a proof-net satisfying the criterion of the theorem, let $x$ be the variable involved in the reduction rule and $\phi$ and $\psi$ as given by the rule. We have to prove acyclicity and connexity of $\Theta'$. 
We prove connexity of $\Theta'$ by contradiction. Suppose there exists a switching function $s'()$ for $\Theta'$ and $u$ in $\phi$ and $v$ in $\psi$ are not connected. We consider the switching function $s()$ in $\Theta$ extending $s'()$ with a link for the connective $\Par$ (use $\Par_L$). As $\Theta$ is DR-correct, $u$ and $v$ are linked in $s(\Theta)$. $x$ must be in the path, otherwise the path remains in $s'(\Theta')$ and $u$ and $v$ are linked. So there is a path $u\dots x^\bot x \dots v$, hence there is a path in $s'(\Theta')$ from $u$ to point 2 (the previous path cannot go twice by $x$ otherwise there is a cycle). Finally, because we choose the link $\Par_L$, in $s(\Theta)$ either the path from $v$ to the root of $\psi$ $r_\psi$ does not pass through $x$ and there is a path in $s'(\Theta')$ from the point 2 to $v$ (and $u$ and $v$ are linked), or there exists $w$ in $\psi$ and a path $r_\psi \dots w w^\bot ... u \dots x^\bot$. In this latter case, $w\leadsto x^\bot$ and there is a contradiction.

The demonstration of acyclicity is done by induction on the height of $\psi$. We first prove commutation properties:
\begin{itemize}
\item suppose the principal connective of $\phi$ is a $\Par$, then $\Theta$ is of the left form below. $\Par$ being associative, $\Theta$ is correct iff the right proof-structure $\Pi$ below is correct.

\ \hfill
\heightTOcenter{$\Theta$: }{\input{Annex/Figures/redNet1par}}
\hfill
\heightTOcenter{$\Pi$: }{\input{Annex/Figures/redNet2par}}
\hfill\ 

\item  suppose the principal connective of $\phi$ is a $\otimes$, then $\Theta$ is of the left following form. We prove the commutation (i.e. acyclicity of the right proof-structure $\Pi$) by contradiction.

\ \hfill
\heightTOcenter{$\Theta$: }{\input{Annex/Figures/redNet1otimes}}
\hfill
\heightTOcenter{$\Pi$: }{\input{Annex/Figures/redNet2otimes}}
\hfill\ 

Let us suppose that there exists a cycle in $\Pi$ in one of the switched proof-structures, say $s(\Pi)$. Remark that the switched proof-structures issued from the sub-structures $\alpha$, $\beta$ and $\gamma$ of $\Pi$ are acyclic as this is true by hypothesis. We prove the result by studying cases wrt the switch chosen for $\Par$:
\begin{itemize}
\item if there is a cycle, this one goes through at least one of the two nodes labelled $\otimes$ and $\Par$. Otherwise, this cycle is also a cycle in $\Theta$.
\item suppose $s(\Par) = \Par_R$:
	\begin{itemize}
	\item if there exists a cycle $\pi$ going through the node labelled $\Par$ but not through $\beta$, then $\exists v$ literal of $\gamma$ and $w$ literal of $\alpha$ st $\pi$ is of the form $w \dots r_\alpha \otimes \Par r_\gamma \dots v \dots w$. Hence, there exist switched proof-structures for $\Theta$ with path $r_\gamma \dots v \dots w \dots r_\alpha$ that do not go through $\Par$ and $\otimes$. Amongst these, one can choose at least one switched proof-structure with the path  $v \dots w \dots r_\alpha \otimes r_\beta x^\perp$. Hence, $v$ is a literal of $\psi$ and $v\leadsto x^\perp$. Contradiction.

\ \hfill
\heightTOcenter{$s(\Theta)$: }{\input{Annex/Figures/redNet1otimes_1}}
\hfill
\heightTOcenter{$s(\Pi)$: }{\input{Annex/Figures/redNet2otimes_1}}
\hfill\ 

	\item if there exists a cycle $\pi$ going through the node labelled $\Par$ and through $\beta$, then either this cycle goes through $x$ or not:
		\begin{itemize}
		\item if $\pi$ goes through $x$ then there exists $v \in \beta, v \not= x^\perp$ and $s(\Pi)$ looks like the right figure. Hence one may choose a switch for $\Theta$ that defines a cycle as in the left one.

\ \hfill
\heightTOcenter{$s(\Theta)$: }{\input{Annex/Figures/redNet1otimes_2}}
\hfill
\heightTOcenter{$s(\Pi)$: }{\input{Annex/Figures/redNet2otimes_2}}
\hfill\ 

		\item if $\pi$ does not go through $x$ then there exist $v$ and $w$ distinct from $x^\perp$ in $\beta$ and $u\not= x$ in $\gamma$ st the cycle looks like the figure in the right. We define a path linking $u$ to $x^\perp$ in a switched proof-structure of $\Theta$ depending on the main connective of the formula labelling the node joining $v$ and $x^\perp$. If this connective is $\otimes$ then one may define a switch joining $u$ and $x^\perp$ via $v$, hence $u \leadsto x^\bot$. If the connective is a $\Par$, one may define a switch joining also $u$ and $x^\perp$ as in the figure on the left.

\ \hfill
\heightTOcenter{$s(\Theta)$: }{\input{Annex/Figures/redNet1otimes_3}}
\hfill
\heightTOcenter{$s(\Pi)$: }{\input{Annex/Figures/redNet2otimes_3}}
\hfill\ 

		\end{itemize}
	\item if there exists a cycle $\pi$ not going through the node labelled $\Par$, then this is also a cycle wrt a switched proof-structure of $\Theta$.
	\end{itemize}
\item suppose $s(\Par) = \Par_L$. From a switch for $\Pi$ including a cycle that goes through $\Par$, one may define a switch for $\Theta$ including a cycle that goes through $\otimes$, hence contradiction with acyclicity of $\Theta$.
\end{itemize}
\item Finally, let us suppose that $\phi$ contains only one node labelled $x^\perp$, the following reduction is stable under correctness:

\ \hfill
\heightTOcenter{$\Theta$: }{\input{Annex/Figures/redNet1otimes_4}}
\hfill
\heightTOcenter{$\Pi$: }{\input{Annex/Figures/redNet2otimes_4}}
\hfill $\qed$\ 

\end{itemize}
\end{proof}



\begin{theorem}[Inverse Stability]
Let $\Theta$ be a proof-structure, if $\Theta \rightarrow \Theta'$ and $\Theta'$ is DR-correct then $\Theta$ is DR-correct.
\end{theorem}

%%%%%%%%%%%%%%%%%			SMALL STEPS inverse stability

\begin{proof}
Let $\Theta$ and $\Theta'$ be as in the theorem.
Suppose there exists $s()$ and $s(\Theta)$ is not connected. Let $u$ and $v$ be variables not connected in $s(\Theta)$. We can suppose that $u \in \phi$ and $v \in \psi$: in other cases, either connexity remains as graph is unchanged or the cases reduce to the one we consider. Define $s'()$ as $s()$ without the switch for the $\Par$ (bottom of the figure for $\Theta$). $s'()$ is a switching function for $\Theta'$. As $\Theta'$ is DR-correct, $u$ and $v$ are connected in $s'(\Theta')$. Either the path from $v$ to $u$ goes through point 2 or not. If it does not go through point 2, it goes through point 1 and exits $\psi$ by a variable $w$. Then $w\in \psi$ and $w\leadsto x^\bot$ (principal connectives must be $\otimes$ otherwise the path in $s'(\Theta')$ is not valid). Contradiction. It it goes through point 2: there is a path in $s'(\Theta')$ from $u$ to point 2, then in $s(\Theta)$ there is a link from $u$ to $x^\bot$,  there is a path in $s'(\Theta')$ from $v$ to $\mathbf 1$ (point 3) because $\Theta'$ is DR-correct, then in $s(\Theta)$ there is a link from $v$ to $x$. Hence $u$ and $v$ are connected.

Suppose there exists $s()$ and there is a cycle in $s(\Theta)$. Let $s'()$ be
$s()$ without the switch for the $\Par$ (bottom of the figure for $\Theta$).
Either the cycle goes through $x$ or not. If it does not go through $x$, either
the switch for $\Par$ is a $\Par_L$ or a $\Par_R$. If it is a $\Par_L$, then
one has immediately a cycle in $s'(\Theta')$. If it is a $\Par_R$ and does not
go through $\phi$, one has still a cycle in $s'(\Theta')$. Otherwise one can
modify $s()$ st one keeps the cycle and there is a direct path from the root of
$\phi$ to one of the variables of $\phi$ in the cycle. In this case there is a
cycle choosing $\Par_L$ that does not go through $x$ and we are done. Finally,
if it goes through $x$, suppose first that it does not go through $\Par$, there
must exist $u\not= x^\bot$ exiting $\phi$ and $v\not= x$ exiting $\psi$ in the
cycle. There is a path from $u$ to $v$ that does not go through $\phi$ and
$\psi$, and a path from $u$ to point 2 that does not go through $x$. Hence it
is possible to define a switching function st there is a cycle in $\Theta'$. If
it goes through $\Par_R$ then there must exist a variable $u$ in $\phi$ where
the cycle exits $\phi$ to go to point 1 without going through $\phi$, hence the
cycle in $\Theta'$ is obvious. If it goes through $\Par_L$, it goes from point
2 to point 1 and from point 1 to $\psi$ entering at a variable, say $v$ without
going through $\phi$. We can define a switching function for $\Theta'$ st there
is a cycle.\hfill $\qed$
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%						THEOREM SMALL STEPS
\begin{theorem}[(small steps) Correctness criterion]
Let $M$ be a closed BM, $M$ is correct iff $M^* \rightarrow^\star \mathbf 1$.
\end{theorem}

\begin{proof}
\begin{itemize}
\item Obviously the proof-structure $\mathbf 1$ is DR-correct. Furthermore there is no other DR-correct proof-structures without variables modulo neutrality of $\mathbf 1$ wrt $\otimes$.

\item Suppose $M^*$ is DR-correct, has still variables and is not reducible. For each variable $v$, the pattern of the left hand side of the rule is satisfied (otherwise it is easy to define a switch that gives a cycle), hence the condition on $\leadsto$ is not satisfied: there exists a variable $v'$ blocking $v$, i.e. $v' \leadsto v^\bot$. Let $v_0$ be a variable. From the previous remark and the fact that the number of variables is finite, one can define a circular list of variables $v_0, \dots, v_n$ st $v_i$ blocks $v_{i+1}$ ($i$ modulo $n$). One may then define a cycle on the proof-structure that does not intersect with $\otimes$ as minimal connectives. Then we can define a switching function st there is a cycle in the switched structure. Contradiction.

\item the rewriting rule is stable wrt DR-correctness and reducibility must occur until there is no variable then if $M$ is correct then $M^* \rightarrow^\star \mathbf 1$.

\item the rewriting rule is stable wrt the inverse rewriting rule, then if $M^*
\rightarrow^\star \mathbf 1$ then $M$ is correct.\hfill $\qed$
\end{itemize}
\end{proof}

Annex_composition.tex
redNet1otimes_1.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1720,1950)(-220,-831)
\thinlines
%\put(-220,-831){\framebox(1720,1950){}}
% nommage des sous-arbres
\put(0,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\alpha$}}}
\put(530,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\beta$}}}
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
%% par de base de phi
\put(250, -40){$\otimes$}
\put(245,80){\line(-2,1){200}}
\put(385,80){\line(2,1){200}}
\put(245,80){\thicklines\line(-2,1){200}}
%% triangle gauche
\put(50,185){\line(-1,3){130}}
\put(50,185){\line(1,3){130}}
\put(50,185){\thicklines\line(0,1){400}}
\put(-80,574){\line(1,0){250}}
%% triangle droit
\put(580,185){\line(-1,3){130}}
\put(580,185){\line(1,3){130}}
\put(600,185){\thicklines\line(-1,4){90}}
\put(450,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% par � la base
\put(751,-511){\line( 0,-1){300}}
\put(376,-61){\line( 1,-1){300}}
\put(1126,-61){\line(-1,-1){300}}
\put(670,575){\thicklines\oval(1240,1020)[t]}
\put(1320,600){$\mathbf v$}
\put(-130,600){$\mathbf w$}
% axiome x/x^perp
\put(511,514){\line( 0, 1){300}}
\put(511,814){\line( 1, 0){540}}
\put(1051,814){\line( 0,-1){300}}
%
\put(586,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(901,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-466){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(446,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(976,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(-200, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\phi$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(601,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet1otimes_2.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1540,1950)(-40,-831)
\thinlines
%\put(-40,-831){\framebox(1540,1950){}}
% nommage des sous-arbres
\put(540,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\beta$}}}
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
%% par de base de phi
\put(250, -466){$\Par$}
%% triangle droit
\put(590,185){\line(-1,3){130}}
\put(590,185){\line(1,3){130}}
\put(460,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% ex-par � la base
\put(316,-511){\thicklines\line( 0,-1){200}}
%\put(376,-360){\thicklines\line( 3,1){300}}
\put(1126,-61){\thicklines\line(-3,-1){740}}
\put(1126,-61){\thicklines\line(1,4){160}}
% axiome x/x^perp
\put(670,574){\thicklines\line( 0, 1){240}}
\put(670,814){\thicklines\line( 1, 0){610}}
\put(1280,814){\thicklines\line( 0,-1){240}}
\put(590,574){\thicklines\oval(150,100)[b]}
\put(275,574){\thicklines\oval(480,350)[t]}
\put(35,574){\thicklines\line(0,-1){1300}}
\put(175,-661){\thicklines\oval(280,250)[b]}
\put(350,600){$\mathbf v$}
%
\put(736,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(1151,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(696,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(1226,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(375,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet1otimes_3.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1540,1950)(-40,-831)
\thinlines
%\put(-40,-831){\framebox(1540,1950){}}
% nommage des sous-arbres
\put(540,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\beta$}}}
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
%% par de base de phi
%% par de base de phi
\put(250, -40){$\otimes$}
\put(385,80){\thicklines\line(2,1){200}}
%% triangle droit
\put(590,185){\line(-1,3){130}}
\put(590,185){\line(1,3){130}}
\put(590,185){\thicklines\line(1,4){95}}
\put(460,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% par � la base
\put(751,-511){\thicklines\line( 0,-1){160}}
\put(376,-61){\thicklines\line( 1,-1){300}}
% axiome x/x^perp
\put(675,574){\line( 0, 1){240}}
\put(675,814){\line( 1, 0){405}}
\put(1080,814){\line( 0,-1){240}}
\put(570,574){\thicklines\oval(90,90)[b]}
\put(275,574){\thicklines\oval(480,350)[t]}
\put(35,574){\thicklines\line(0,-1){1300}}
\put(395,-661){\thicklines\oval(720,250)[b]}
\put(1350,600){$\mathbf u$}
\put(500,700){$\mathbf v$}
\put(350,600){$\mathbf w$}
\put(950,574){\thicklines\oval(650,1060)[t]}
%
\put(736,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(951,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-500){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(696,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(1026,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(845,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet1otimes_4.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1720,1950)(-220,-831)
\thinlines
%\put(-220,-831){\framebox(1720,1950){}}
% nommage des sous-arbres
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% par � la base
\put(751,-511){\line( 0,-1){300}}
\put(506,-161){\line( 1,-1){183}}%
\put(1126,-61){\line(-1,-1){300}}
% axiome x/x^perp
\put(511,814){\line( 0, -1){970}}
\put(511,814){\line( 1, 0){540}}
\put(1051,814){\line( 0,-1){300}}
%
\put(586,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(901,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-466){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(446,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(976,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(-200, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\phi$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(601,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

cut_link.tex
\setlength{\unitlength}{3947sp}%
\begin{picture}(537,352)(2851,-1901)
\thinlines
\put(3151,-1911){\oval(450,150)[b]}
\put(2851,-1861){$A^\perp$}
\put(3301,-1861){$A$}
\end{picture}

redNet1par.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1720,1912)(-220,-831)
\thinlines
%\put(-220,-831){\framebox(1720,1912){}}
% triangle phi
%% par de base de phi
\put(250, -40){$\Par$}
\put(245,80){\line(-2,1){200}}
\put(385,80){\line(2,1){200}}
%% triangle gauche
\put(50,185){\line(-1,3){130}}
\put(50,185){\line(1,3){130}}
\put(-80,574){\line(1,0){250}}
%% triangle droit
\put(590,185){\line(-1,3){130}}
\put(590,185){\line(1,3){130}}
\put(460,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% par � la base
\put(751,-511){\line( 0,-1){300}}
\put(376,-61){\line( 1,-1){300}}
\put(1126,-61){\line(-1,-1){300}}
% axiome x/x^perp
\put(511,514){\line( 0, 1){300}}
\put(511,814){\line( 1, 0){540}}
\put(1051,814){\line( 0,-1){300}}
%
\put(586,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(901,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-466){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(446,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(976,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(-200, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\phi$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(601,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet2otimes_1.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1720,1950)(-220,-831)
\thinlines
%\put(-220,-831){\framebox(1720,1950){}}
% nommage des sous-arbres
\put(50,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\alpha$}}}
\put(540,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\beta$}}}
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
%% par de base de phi
\put(250, -466){$\otimes$}
\put(245,-360){\line(-1,4){135}}
\put(590,180){\line(1,-3){100}}
\put(245,-360){\thicklines\line(-1,4){135}}
%% triangle gauche
\put(100,185){\line(-1,3){130}}
\put(100,185){\line(1,3){130}}
\put(100,185){\thicklines\line(0,1){400}}
\put(-30,574){\line(1,0){250}}
%% triangle droit
\put(590,185){\line(-1,3){130}}
\put(590,185){\line(1,3){130}}
\put(460,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% ex-par � la base
\put(316,-511){\line( 0,-1){300}}
\put(376,-360){\line( 3,1){300}}
\put(1126,-61){\line(-3,-1){280}}
\put(376,-360){\thicklines\line( 3,1){300}}
\put(1126,-61){\thicklines\line(-3,-1){280}}
\put(1126,-61){\thicklines\line(1,4){160}}
\put(695,590){\thicklines\oval(1190,1020)[t]}
\put(1320,600){$\mathbf v$}
\put(-80,600){$\mathbf w$}
% axiome x/x^perp
\put(511,514){\line( 0, 1){300}}
\put(511,814){\line( 1, 0){540}}
\put(1051,814){\line( 0,-1){300}}
%
\put(586,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(901,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-250){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(446,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(976,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(-200, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\phi$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(175,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet2otimes_2.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1540,1950)(-40,-831)
\thinlines
%\put(-40,-831){\framebox(1540,1950){}}
% nommage des sous-arbres
\put(540,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\beta$}}}
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
%% par de base de phi
\put(250, -466){$\otimes$}
%% triangle droit
\put(590,185){\line(-1,3){130}}
\put(590,185){\line(1,3){130}}
\put(460,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% ex-par � la base
\put(316,-511){\thicklines\line( 0,-1){200}}
\put(376,-360){\line( 3,1){300}}
\put(1126,-61){\line(-3,-1){280}}
\put(376,-360){\thicklines\line( 3,1){300}}
\put(1126,-61){\thicklines\line(-3,-1){280}}
\put(1126,-61){\thicklines\line(1,4){160}}
% axiome x/x^perp
\put(670,574){\thicklines\line( 0, 1){240}}
\put(670,814){\thicklines\line( 1, 0){610}}
\put(1280,814){\thicklines\line( 0,-1){240}}
\put(590,574){\thicklines\oval(150,100)[b]}
\put(275,574){\thicklines\oval(480,350)[t]}
\put(35,574){\thicklines\line(0,-1){1300}}
\put(175,-661){\thicklines\oval(280,250)[b]}
\put(350,600){$\mathbf v$}
%
\put(736,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(1151,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-250){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(696,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(1226,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(375,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet2otimes_3.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1540,1950)(-40,-831)
\thinlines
%\put(-40,-831){\framebox(1540,1950){}}
% nommage des sous-arbres
\put(540,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\beta$}}}
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
%% par de base de phi
\put(250, -466){$\otimes$}
%% triangle droit
\put(590,185){\line(-1,3){130}}
\put(590,185){\line(1,3){130}}
\put(460,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% ex-par � la base
\put(316,-511){\thicklines\line( 0,-1){200}}
\put(376,-360){\line( 3,1){300}}
\put(1126,-61){\line(-3,-1){280}}
\put(376,-360){\thicklines\line( 3,1){300}}
\put(1126,-61){\thicklines\line(-3,-1){280}}
\put(1126,-61){\thicklines\line(1,4){160}}
% axiome x/x^perp
\put(670,574){\line( 0, 1){240}}
\put(670,814){\line( 1, 0){410}}
\put(1080,814){\line( 0,-1){240}}
\put(570,574){\thicklines\oval(90,90)[b]}
\put(275,574){\thicklines\oval(480,350)[t]}
\put(35,574){\thicklines\line(0,-1){1300}}
\put(175,-661){\thicklines\oval(280,250)[b]}
\put(1350,600){$\mathbf u$}
\put(500,700){$\mathbf v$}
\put(350,600){$\mathbf w$}
\put(950,574){\thicklines\oval(650,1060)[t]}
%
\put(736,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(951,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-250){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(696,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(1026,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(375,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet2otimes_4.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1720,1950)(-220,-831)
\thinlines
%\put(-220,-831){\framebox(1720,1950){}}
% nommage des sous-arbres
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% par � la base
\put(751,-431){\line( 0,-1){380}}
\put(1126,-61){\line(-1,-1){380}}
% axiome 1
\put(1051,814){\line( 0,-1){300}}
\put(1005,889){$\mathbf 1$}
\put(1040,940){\circle{260}}
%
\put(901,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(601,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet1.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1350,1602)(1,-823)
\thinlines
%\put(1,-823){\framebox(1350,1602){}}
\put(226,389){\line( 1, 0){300}}
\put(526,389){\line(-1,-3){150}}
\put(376,-61){\line(-1, 3){150}}
\put(376,-61){\line( 1,-1){300}}
\put(976,389){\line( 1, 0){300}}
\put(1276,389){\line(-1,-3){150}}
\put(1126,-61){\line(-1, 3){150}}
\put(1126,-61){\line(-1,-1){300}}
\put(751,-511){\line( 0,-1){300}}
\put(451,314){\line( 0, 1){300}}
\put(451,614){\line( 1, 0){600}}
\put(1051,614){\line( 0,-1){300}}
\put(526,464){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(901,464){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-466){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(386,689){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(976,689){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(  1, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\phi$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(601,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet2.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
%\begin{picture}(612,1899)(1,-1048)
\begin{picture}(612,1602)(1,-823)
\thinlines
%\put(1,-1048){\framebox(612,1899){}}
\put(226,-286){\line( 1, 0){300}}
\put(526,-286){\line(-1,-3){150}}
\put(376,-736){\line(-1, 3){150}}
\put(376,-736){\line( 0,-1){300}}
\put(451,-61){\line( 0,-1){300}}
\put(376,314){\line( 0, 1){310}}
\put(301,389){\line( 1, 0){300}}
\put(601,389){\line(-1,-3){150}}
\put(451,-61){\line(-1, 3){150}}
\put(376,735){\circle{200}}
\put(330,689){\bf 1}
\put(526,-211){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(  1,-586){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\phi$}}}
\put(226,-1036){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\put(601,164){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(451,464){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\end{picture}

times_link.tex
\setlength{\unitlength}{4000sp}%
\begin{picture}(500,500)
\thinlines
\put(220,130){\line(-1,2){130}}
\put(220,130){\line(1,2){130}}
\put(0,0){$A\otimes B$}
\put(0,425){$A$}
\put(330,425){$B$}
\end{picture}

axiom_link.tex
\setlength{\unitlength}{3947sp}%
\begin{picture}(537,352)(2851,-1901)
\thinlines
\put(3151,-1711){\oval(450,150)[t]}
\put(2851,-1861){$A^\perp$}
\put(3301,-1861){$A$}
\end{picture}

redNet2otimes.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1720,1912)(-220,-831)
\thinlines
%\put(-220,-831){\framebox(1720,1912){}}
% nommage des sous-arbres
\put(50,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\alpha$}}}
\put(540,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\beta$}}}
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
%% par de base de phi
\put(250, -466){$\otimes$}
\put(245,-360){\line(-1,4){135}}
\put(590,180){\line(1,-3){100}}
%% triangle gauche
\put(100,185){\line(-1,3){130}}
\put(100,185){\line(1,3){130}}
\put(-30,574){\line(1,0){250}}
%% triangle droit
\put(590,185){\line(-1,3){130}}
\put(590,185){\line(1,3){130}}
\put(460,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% ex-par � la base
\put(316,-511){\line( 0,-1){300}}
\put(376,-360){\line( 3,1){300}}
\put(1126,-61){\line(-3,-1){280}}
% axiome x/x^perp
\put(511,514){\line( 0, 1){300}}
\put(511,814){\line( 1, 0){540}}
\put(1051,814){\line( 0,-1){300}}
%
\put(586,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(901,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-250){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(446,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(976,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(-200, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\phi$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(175,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

par_switchL.tex
\setlength{\unitlength}{4000sp}%
\begin{picture}(500,500)
\thinlines
\put(240,140){\line(-1,2){130}}
\put(0,0){$A\Par B$}
\put(0,430){$A$}
\put(350,430){$B$}
\end{picture}

par_switchR.tex
\setlength{\unitlength}{4000sp}%
\begin{picture}(500,500)
\thinlines
\put(240,140){\line(1,2){130}}
\put(0,0){$A\Par B$}
\put(0,430){$A$}
\put(350,430){$B$}
\end{picture}

redNet2par.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1720,1912)(-220,-831)
\thinlines
%\put(-220,-831){\framebox(1720,1912){}}
% triangle phi
%% par de base de phi
\put(250, -466){$\Par$}
\put(245,-360){\line(-1,4){135}}
\put(590,180){\line(1,-3){100}}
%% triangle gauche
\put(100,185){\line(-1,3){130}}
\put(100,185){\line(1,3){130}}
\put(-30,574){\line(1,0){250}}
%% triangle droit
\put(590,185){\line(-1,3){130}}
\put(590,185){\line(1,3){130}}
\put(460,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% ex-par � la base
\put(316,-511){\line( 0,-1){300}}
\put(376,-360){\line( 3,1){300}}
\put(1126,-61){\line(-3,-1){280}}
% axiome x/x^perp
\put(511,514){\line( 0, 1){300}}
\put(511,814){\line( 1, 0){540}}
\put(1051,814){\line( 0,-1){300}}
%
\put(586,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(901,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-250){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(446,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(976,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(-200, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\phi$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(175,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

redNet1otimes.tex
\setlength{\unitlength}{3947sp}%
%
\begingroup\makeatletter\ifx\SetFigFont\undefined%
\gdef\SetFigFont#1#2#3#4#5{%
  \reset@font\fontsize{#1}{#2pt}%
  \fontfamily{#3}\fontseries{#4}\fontshape{#5}%
  \selectfont}%
\fi\endgroup%
\begin{picture}(1720,1912)(-220,-831)
\thinlines
%\put(-220,-831){\framebox(1720,1912){}}
% nommage des sous-arbres
\put(0,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\alpha$}}}
\put(540,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\beta$}}}
\put(1070,410){\makebox(0,0)[lb]{\smash{\SetFigFont{8}{10.0}{\rmdefault}{\mddefault}{\updefault}$\gamma$}}}
% triangle phi
%% par de base de phi
\put(250, -40){$\otimes$}
\put(245,80){\line(-2,1){200}}
\put(385,80){\line(2,1){200}}
%% triangle gauche
\put(50,185){\line(-1,3){130}}
\put(50,185){\line(1,3){130}}
\put(-80,574){\line(1,0){250}}
%% triangle droit
\put(590,185){\line(-1,3){130}}
\put(590,185){\line(1,3){130}}
\put(460,574){\line(1,0){250}}
% triangle psi
\put(916,574){\line( 1, 0){415}}
\put(1126,-61){\line(1,3){210}}
\put(1126,-61){\line(-1, 3){210}}
% par � la base
\put(751,-511){\line( 0,-1){300}}
\put(376,-61){\line( 1,-1){300}}
\put(1126,-61){\line(-1,-1){300}}
% axiome x/x^perp
\put(511,514){\line( 0, 1){300}}
\put(511,814){\line( 1, 0){540}}
\put(1051,814){\line( 0,-1){300}}
%
\put(586,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}2}}}
\put(901,664){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}3}}}
\put(686,-466){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}$\Par$}}}
\put(446,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x^\bot$}}}
\put(976,889){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$x$}}}
\put(-200, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\phi$}}}
\put(1351, 89){\makebox(0,0)[lb]{\smash{\SetFigFont{12}{14.4}{\rmdefault}{\mddefault}{\updefault}$\psi$}}}
\put(601,-811){\makebox(0,0)[lb]{\smash{\SetFigFont{10}{12.0}{\rmdefault}{\mddefault}{\updefault}1}}}
\end{picture}

par_link.tex
\setlength{\unitlength}{4000sp}%
\begin{picture}(500,500)
\thinlines
\put(240,140){\line(-1,2){130}}
\put(240,140){\line(1,2){130}}
\put(0,0){$A\Par B$}
\put(0,430){$A$}
\put(350,430){$B$}
\end{picture}

figure_completion1.tex
\begin{picture}(90,62)
\thinlines
%\put(0,0){\framebox(90,60){}}
% cas simple membre gauche
\multiput(10,5)(0,2.5){2}{\circle*{1}}
\negatifDeux{10}{15}{10}{a}{b}
% 1ere fleche
\put(45,20){\makebox(0,0){$\longrightarrow_c$}}
% membre droit
\multiput(80,5)(0,2.5){2}{\circle*{1}}
\put(80,20){\circle*{5}}
\put(80,20){\line(-1,2){5}}
\put(75,35){\makebox(0,0){a}}
\put(80,20){\line(1,2){5}}
\put(85,35){\makebox(0,3){b}}
\put(80,10){\line(0,1){10}}
\end{picture}


figure_completion2.tex
\begin{picture}(85,62)(0,5)
\thinlines
%\put(0,0){\framebox(85,62){}}
% cas simple membre gauche
\multiput(10,5)(0,2.5){2}{\circle*{1}}
\negatifDeux{10}{15}{10}{a}{}
\put(15,30){\line(0,1){5}}
\positifUn{5}{37}{10}{}
\negatifc{15}{52}{10}

% 1ere fleche
\put(45,20){\makebox(0,0){$\longrightarrow_c$}}
% membre droit
\multiput(75,5)(0,2.5){2}{\circle*{1}}
\negatifDeux{75}{15}{10}{a}{}
\put(80,25){\line(0,1){10}}
\put(80,35){\circle*{5}}

\end{picture}


figure_completion3.tex
\begin{picture}(80,62)
\thinlines
%\put(0,0){\framebox(80,62){}}
% cas simple membre gauche
\put(15,30){\line(0,1){5}}
\positifUn{5}{37}{10}{}
\negatifc{15}{52}{10}
\multiput(10,5)(0,2.5){2}{\circle*{1}}
\put(10,20){\circle*{5}}
\put(10,20){\line(-1,2){5}}
\put(5,35){\makebox(0,0){a}}
\qbezier(10,20)(15,20)(15,37)
\put(10,10){\line(0,1){10}}

% 1ere fleche
\put(45,20){\makebox(0,0){$\longrightarrow_c$}}

% membre droit
\multiput(75,5)(0,2.5){2}{\circle*{1}}
\put(75,20){\circle*{5}}
\put(75,20){\line(0,1){10}}
\put(75,35){\makebox(0,0){a}}
\put(75,10){\line(0,1){10}}
\end{picture}


figure_S1contraction4bis.tex
\begin{picture}(135,50)
\thinlines
%\put(0,0){\framebox(135,50){}}

%%% max %%%
\negatifExt{30}{5}{30}{3}{1}
%\put(30,10){\makebox(0,2){$\scriptstyle max$}}
\put(30,5){\line(0,-1){5}}
% alpha
\put(5,15){\line(0,1){5}}
\multiput(7.5,20)(2.5,0){3}{\circle*{1}}
\put(15,15){\line(0,1){5}}
\put(10,25){\makebox(0,5){$\alpha$}}
%%% contracted node %%%
\put(45,30){\circle*{5}}
\put(55,30){\makebox(0,0){$\scriptstyle i\in I$}}
\put(40,15){\line(1,3){5}}
\put(50,15){\line(-1,3){5}}
\put(45,30){\line(-1,2){5}}
\put(45,30){\line(1,2){5}}
\put(43.5,39){\circle*{1}}
\put(46.5,39){\circle*{1}}
\multiput(44,18)(3,0){2}{\circle*{1}}
\put(45,45){\makebox(0,5){$\alpha_i$}}
%%% others dots
\multiput(37.5,20)(-2.5,0){3}{\circle*{1}}
\multiput(52.5,20)(2.5,0){3}{\circle*{1}}

% fleche

\put(85,17.5){\makebox(0,0){$\longrightarrow$}}

% membre droit
\put(113,35){\makebox(0,5){$\underset{i\in I}{\cup}\alpha_i\cup\alpha$}}
\put(115,17.5){\circle*{5}}
\put(115,17.5){\line(-1,2){5}}
\put(115,17.5){\line(1,2){5}}
\put(113.5,26.5){\circle*{1}}
\put(116.5,26.5){\circle*{1}}
\put(115,17.5){\line(0,-1){10}}


\end{picture}

figure_form1.tex
\begin{picture}(150,120)
\thinlines
%\put(0,0){\framebox(150,120){}}

%%% N %%%
\negatifExt{30}{35}{30}{3}{1}
\put(30,35){\line(0,-1){5}}
\multiput(30,25)(0,2.5){2}{\circle*{1}}
% alpha
\put(5,45){\line(0,1){5}}
\multiput(7.5,50)(2.5,0){3}{\circle*{1}}
\put(15,45){\line(0,1){5}}
\put(10,55){\makebox(0,0){$\alpha$}}
% autres liens
\qbezier(40,45)(40,60)(75,60)
\qbezier(50,45)(50,60)(75,60)
\multiput(44,50)(3,0){2}{\circle*{1}}

%%% contracted node %%%
% dots 
\put(75,60){\circle*{5}}
\multiput(37.5,50)(-2.5,0){3}{\circle*{1}}
\multiput(55,50)(2.5,0){3}{\circle*{1}}
%%% gamma_i 
%%\put(75,60){\line(-1,-2){5}}
%%\put(75,60){\line(1,-2){5}}
%%\put(73.5,51){\circle*{1}}
%%\put(76.5,51){\circle*{1}}
%%\put(75,40){\makebox(0,5){$\gamma_i$}}
% beta_i -----> alpha_i
\put(75,60){\line(-1,2){5}}
\put(75,60){\line(1,2){5}}
\put(73.5,69){\circle*{1}}
\put(76.5,69){\circle*{1}}
\put(75,75){\makebox(0,5){$\alpha_i$}}
% added
\put(75,50){\makebox(0,0){\scriptsize $i\in I$}}

%%% c^k_i %%%
% liens
\qbezier(110,45)(110,60)(75,60)
\qbezier(100,45)(100,60)(75,60)
\multiput(112.5,50)(2.5,0){3}{\circle*{1}}
\multiput(95,50)(-2.5,0){3}{\circle*{1}}
% negatif
\negatifExt{120}{35}{30}{3}{1}
\put(120,35){\line(0,-1){5}}
\multiput(120,25)(0,2.5){2}{\circle*{1}}
% delta -----> beta_i
\multiput(102,50)(3,0){2}{\circle*{1}}
\put(130,45){\line(0,1){5}}
\multiput(132.5,50)(2.5,0){3}{\circle*{1}}
\put(140,45){\line(0,1){5}}
\put(135,55){\makebox(0,5){$\beta_i$}}

%%% h^l_i %%%
% liens
\qbezier(110,75)(110,60)(75,60)
\multiput(107,75)(-2.5,0){3}{\circle*{1}}
\multiput(113,75)(2.5,0){3}{\circle*{1}}
% negatif
\negatifN{110}{80}{10}


%%% labels %%%
% label N_1
\put(30,15){\makebox(0,0){$\underbrace{\hspace{60pt}}$}}
\put(30,5){\makebox(0,0){$N$}}
% label c_i^k
\put(120,15){\makebox(0,0){$\underbrace{\hspace{60pt}}$}}
\put(120,5){\makebox(0,0){$c_i\in C_i$}}
% label h_i^k
\put(110,105){\makebox(0,0){$\overbrace{\hspace{20pt}}$}}
\put(110,115){\makebox(0,0){$h_i\in H_i$}}






%\multiput(10,5)(0,2.5){2}{\circle*{1}}
%\negatifDeux{10}{15}{10}{a}{}
%\positifDeux{10}{35}{15}{}{}
%\negatifc{25}{50}{10}
%\multiput(40,5)(0,2.5){2}{\circle*{1}}
%\negatifDeux{40}{15}{10}{}{b}
% 1ere fleche
%\put(85,20){\makebox(0,0){$\longrightarrow_c$}}
% membre droit
%\multiput(130,5)(0,2.5){2}{\circle*{1}}
%\negatifDeux{130}{15}{10}{a}{}
%\qbezier(135,25)(135,40)(145,40)
%\put(145,40){\circle*{5}}
%\qbezier(155,25)(155,40)(145,40)
%\multiput(160,5)(0,2.5){2}{\circle*{1}}
%\negatifDeux{160}{15}{10}{}{b}
\end{picture}

figure_exemple2.tex
{\tt
\begin{picture}(70,100)
\thinlines    
%
% EX2
%\put(0,10){\framebox(70,100){}}
\put(40,0){\makebox(0,0){$\alpha\circ_{\{b\}} \beta$}}
% MBE A + (+25,0)
\negatifDeux{45}{40}{20}{b}{c}
\positifUn{25}{25}{20}{a}
% MBE B + (0,+45)
\negatifDeux{42}{85}{10}{e}{f}
\negatifUn{17}{85}{10}{d}
\positifUn{10}{70}{20}{}

%
\end{picture}}










figure_exemple3.tex
{\tt
\begin{picture}(130,150)
\thinlines    
%\put(0,10){\framebox(130,150){}}

% EX3
\put(65,0){\makebox(0,0){$\alpha \circ \beta \circ \gamma \circ \delta$}}
% MBE \Delta
\negatifUn{65}{130}{10}{j}
\positifDeux{45}{115}{20}{}{}
% MBE \Gamma
\negatifUn{115}{85}{10}{i}
\negatifDeux{85}{85}{10}{g}{h}
\positifUn{75}{70}{25}{}
% MBE B
\negatifDeux{45}{85}{10}{e}{f}
\negatifUn{15}{85}{10}{d}
\positifUn{5}{70}{25}{}
% MBE A
\negatifDeuxExt{65}{40}{40}{b}{c}{4}{1}
\positifUn{25}{25}{40}{a}

\end{picture}}

figure_normalForm1.tex
\begin{picture}(150,110)
\thinlines
%\put(0,0){\framebox(150,120){}}

%%% N %%%
\negatifExt{30}{35}{30}{3}{1}
\put(30,35){\line(0,-1){5}}
\multiput(30,25)(0,2.5){2}{\circle*{1}}
% alpha
\put(5,45){\line(0,1){5}}
\multiput(7.5,50)(2.5,0){3}{\circle*{1}}
\put(15,45){\line(0,1){5}}
\put(10,55){\makebox(0,0){$\alpha$}}
% autres liens
\qbezier(40,45)(40,60)(75,60)
\qbezier(50,45)(50,60)(75,60)
\multiput(44,50)(3,0){2}{\circle*{1}}

%%% contracted node %%%
% dots 
\put(75,60){\circle*{5}}
\multiput(37.5,50)(-2.5,0){3}{\circle*{1}}
\multiput(55,50)(2.5,0){3}{\circle*{1}}
%%% gamma_i 
%%\put(75,60){\line(-1,-2){5}}
%%\put(75,60){\line(1,-2){5}}
%%\put(73.5,51){\circle*{1}}
%%\put(76.5,51){\circle*{1}}
%%\put(75,40){\makebox(0,5){$\gamma_i$}}
% beta_i -----> alpha_i
%\put(75,60){\line(-1,2){5}}
%\put(75,60){\line(1,2){5}}
%\put(73.5,69){\circle*{1}}
%\put(76.5,69){\circle*{1}}
\put(75,70){\makebox(0,5){$i_0$}}
% added
%\put(75,50){\makebox(0,0){\scriptsize $i\in I$}}

%%% c^k_i %%%
% liens
\qbezier(110,45)(110,60)(75,60)
\qbezier(100,45)(100,60)(75,60)
\multiput(112.5,50)(2.5,0){3}{\circle*{1}}
\multiput(95,50)(-2.5,0){3}{\circle*{1}}
% negatif
\negatifExt{120}{35}{30}{3}{1}
\put(120,35){\line(0,-1){5}}
\multiput(120,25)(0,2.5){2}{\circle*{1}}
% delta -----> beta_i
\multiput(102,50)(3,0){2}{\circle*{1}}
\put(130,45){\line(0,1){5}}
\multiput(132.5,50)(2.5,0){3}{\circle*{1}}
\put(140,45){\line(0,1){5}}
\put(135,55){\makebox(0,5){$\beta_k$}}

%%% h^l_i %%%
% liens
\qbezier(110,75)(110,60)(75,60)
\multiput(107,75)(-2.5,0){3}{\circle*{1}}
\multiput(113,75)(2.5,0){3}{\circle*{1}}
% negatif
\negatifN{110}{80}{10}


%%% labels %%%
% label N_1
%\put(30,15){\makebox(0,0){$\underbrace{\hspace{60pt}}$}}
\put(30,5){\makebox(0,0){$N$}}
% label c_i^k
\put(120,15){\makebox(0,0){$\underbrace{\hspace{60pt}}$}}
\put(120,5){\makebox(0,0){$c_k \in C$}}
% label h_i^k
\put(110,105){\makebox(0,0){$\overbrace{\hspace{20pt}}$}}
\put(110,115){\makebox(0,0){$h_l\in H$}}






%\multiput(10,5)(0,2.5){2}{\circle*{1}}
%\negatifDeux{10}{15}{10}{a}{}
%\positifDeux{10}{35}{15}{}{}
%\negatifc{25}{50}{10}
%\multiput(40,5)(0,2.5){2}{\circle*{1}}
%\negatifDeux{40}{15}{10}{}{b}
% 1ere fleche
%\put(85,20){\makebox(0,0){$\longrightarrow_c$}}
% membre droit
%\multiput(130,5)(0,2.5){2}{\circle*{1}}
%\negatifDeux{130}{15}{10}{a}{}
%\qbezier(135,25)(135,40)(145,40)
%\put(145,40){\circle*{5}}
%\qbezier(155,25)(155,40)(145,40)
%\multiput(160,5)(0,2.5){2}{\circle*{1}}
%\negatifDeux{160}{15}{10}{}{b}
\end{picture}

figure_exemple4.tex
{\tt
\begin{picture}(100,100)
\thinlines    
%
% EX 4
%\put(0,10){\framebox(60,100){}}
\put(30,0){\makebox(0,0){$\beta\circ \epsilon$}}
% MBE B + (0,0)
\negatifDeux{45}{40}{10}{e}{f}
\negatifUn{15}{40}{10}{d}
\positifUn{5}{25}{25}{b}
% MBE E + (+5,+45)
\negatifUn{26}{85}{10}{k}
\positifDeux{10}{70}{17}{}{}

\end{picture}}

figure_drawExA.tex
{\tt
\begin{picture}(44,55)
%\put(0,0){\framebox(44,55)}
\thinlines    
%
\put(6,25){\makebox(0,0){$\alpha$:}}
\negatifDeux{31}{30}{10}{b}{c}
\positifUn{21}{15}{10}{a}
\end{picture}}

figure_drawExB.tex
{\tt
\begin{picture}(74,57)
%\put(0,0){\framebox(74,57)}
\thinlines    
%
\put(6,25){\makebox(0,0){$\beta$:}}
\negatifDeux{61}{30}{10}{e}{f}
\negatifUn{31}{30}{10}{d}
\positifUn{21}{15}{25}{b}
\end{picture}}
figure_S1contraction1.tex
{\tt
\begin{picture}(140,35)
%\put(0,0){\framebox(140,35)}
\thinlines    

%%%%%%%%%%%%%%%%%%%%%%%%%%
%% traduction rule ->_t %%
%%%%%%%%%%%%%%%%%%%%%%%%%%

%membre gauche
\positifZero{0}{5}{25}
\negatifN{10}{20}{10}
\multiput(22.5,20)(2.5,0){3}{\circle*{1}}
\negatifN{40}{20}{10}
\put(20,0){\line(0,1){5}}
\multiput(22.5,0)(2.5,0){3}{\circle*{1}}
\put(30,0){\line(0,1){5}}

% fleche
\put(70,17.5){\makebox(0,0){$\longrightarrow$}}

% membre droit

\put(110,0){\line(1,2){5}}
\put(120,0){\line(-1,2){5}}
\put(113.5,1){\circle*{1}}
\put(116.5,1){\circle*{1}}
\put(115,10){\circle*{5}}
\qbezier(115,10)(100,15)(100,20)
\qbezier(115,10)(130,15)(130,20)

\negatiff{100}{20}{10}
\put(95,30){\line(0,1){5}}
\multiput(97.5,35)(2.5,0){3}{\circle*{1}}
\put(105,30){\line(0,1){5}}

\multiput(112.5,20)(2.5,0){3}{\circle*{1}}

\negatiff{130}{20}{10}
\put(125,30){\line(0,1){5}}
\multiput(127.5,35)(2.5,0){3}{\circle*{1}}
\put(135,30){\line(0,1){5}}


\end{picture}}

figure_S1contraction2.tex
{\tt
\begin{picture}(80,40)
%\put(0,0){\framebox(70,40)}
\thinlines    

%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% contraction rule ->_c %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%

%membre gauche
\negatifc{10}{5}{10}
\qbezier(5,15)(5,30)(10,30)
\qbezier(15,15)(15,30)(10,30)
%\put(5,20){\line(1,2){5}}
%\put(15,20){\line(-1,2){5}}
\multiput(7.5,20)(2.5,0){3}{\circle*{1}}
\put(10,30){\circle*{5}}
\put(10,30){\line(-1,2){5}}
\put(10,30){\line(1,2){5}}
\put(8.5,39){\circle*{1}}
\put(11.5,39){\circle*{1}}

% fleche
\put(40,20){\makebox(0,0){$\longrightarrow$}}

% membre droit
\put(65,20){\line(0,-1){10}}
\put(65,20){\circle*{5}}
\put(65,20){\line(-1,2){5}}
\put(65,20){\line(1,2){5}}
\put(63.5,29){\circle*{1}}
\put(66.5,29){\circle*{1}}

\end{picture}}

figure_S1contraction3.tex
{\tt
\begin{picture}(60,35)
%\put(0,0){\framebox(60,35)}
\thinlines    
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% contraction rules :       %%
%% simplification rules ->_c %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% membre gauche
\put(0,0){\line(1,2){5}}
\put(10,0){\line(-1,2){5}}
\put(3.5,1){\circle*{1}}
\put(6.5,1){\circle*{1}}
\put(5,10){\circle*{5}}

\put(5,10){\line(0,1){15}}

\put(5,25){\line(-1,2){5}}
\put(5,25){\line(1,2){5}}
\put(3.5,34){\circle*{1}}
\put(6.5,34){\circle*{1}}
\put(5,25){\circle*{5}}

% fleche

\put(30,17.5){\makebox(0,0){$\longrightarrow$}}

% membre droit

\put(50,7.5){\line(1,2){5}}
\put(60,7.5){\line(-1,2){5}}
\put(53.5,8.5){\circle*{1}}
\put(56.5,8.5){\circle*{1}}
\put(55,17.5){\circle*{5}}
\put(55,17.5){\line(-1,2){5}}
\put(55,17.5){\line(1,2){5}}
\put(53.5,26.5){\circle*{1}}
\put(56.5,26.5){\circle*{1}}

\end{picture}}

figure_notcc2.tex
\begin{picture}(140,60)(0,5)
\thinlines
%\put(0,0){\framebox(140,60){}}
% cas double membre gauche
\multiput(10,5)(0,2.5){2}{\circle*{1}}
\negatifDeux{10}{15}{10}{a}{}
\positifDeux{10}{35}{15}{}{}
\negatifc{25}{50}{10}
\multiput(40,5)(0,2.5){2}{\circle*{1}}
\negatifDeux{40}{15}{10}{}{b}
% 1ere fleche
\put(70,20){\makebox(0,0){$\longrightarrow_c$}}
% membre droit
\multiput(100,5)(0,2.5){2}{\circle*{1}}
\put(100,15){\line(0,-1){5}}
\negatiff{100}{15}{10}%{a}{}
\put(95,25){\line(0,1){5}}
\put(95,32){\makebox(0,5)[b]{$a$}}
\qbezier(105,25)(105,40)(115,40)
\put(115,40){\circle*{5}}
\qbezier(125,25)(125,40)(115,40)
\multiput(130,5)(0,2.5){2}{\circle*{1}}
\negatifDeux{130}{15}{10}{}{b}
\end{picture}

figure_smallStep1.tex
\begin{picture}(70,75)(-5,-1)
\thinlines
%\put(0,0){\framebox(70,75){}}

% racine
\put(30,-1){\line(0,1){10}}
\put(35,2){\makebox(0,0){\scriptsize 1}}
% noeud par
\put(30,15){\circle{12}}
\put(30,15){\makebox(0,0){$\Par$}}
% arbre gauche
\put(16,43){\makebox(0,0){$\phi$}}
\put(26,20){\line(-1,1){10}}
\put(16,30){\line(-1,2){10}}
\put(16,30){\line(1,2){10}}
\put(6,50){\line(1,0){20}}
% arbre droit
\put(44,43){\makebox(0,0){$\psi$}}
\put(34,20){\line(1,1){10}}
\put(44,30){\line(1,2){10}}
\put(44,30){\line(-1,2){10}}
\put(54,50){\line(-1,0){20}}
% axiome
\put(16,50){\line(0,1){10}}
\put(20,55){\makebox(0,0){\scriptsize 2}}
\put(16,65){\makebox(5,4){\scriptsize $x^\bot$}}

%\put(16,70){\line(0,1){4}}
%\put(16,74){\line(1,0){28}}
\put(16,60){\line(1,0){28}}
%\put(44,70){\line(0,1){4}}

\put(44,65){\makebox(0,0){\scriptsize $x$}}
\put(48,55){\makebox(0,0){\scriptsize 3}}
\put(44,50){\line(0,1){10}}

\end{picture}

figure_smallStep2.tex
\begin{picture}(30,85)
\thinlines
%\put(0,0){\framebox(30,85){}}

% racine
\put(15,0){\line(0,1){10}}
\put(20,3){\makebox(0,0){\scriptsize 1}}
% arbre bas
\put(15,23){\makebox(0,0){$\phi$}}
\put(20,35){\makebox(0,0){\scriptsize 2}}
\put(15,10){\line(-1,2){10}}
\put(15,10){\line(1,2){10}}
\put(5,30){\line(1,0){20}}
% arbre haut
\put(15,30){\line(0,1){10}}
\put(15,53){\makebox(0,0){$\psi $}}
\put(20,65){\makebox(0,0){\scriptsize 3}}
\put(15,40){\line(-1,2){10}}
\put(15,40){\line(1,2){10}}
\put(5,60){\line(1,0){20}}
% noeud 1
\put(15,60){\line(0,1){10}}
\put(15,77){\circle{12}}
\put(15,77){\makebox(0,0){$\bf 1$}}

\end{picture}

figure_contraction6.tex
\begin{picture}(75,30)
\thinlines    
%\put(0,0){\framebox(75,30){}}

% membre gauche
\put(5,0){\line(1,2){5}}
\put(15,0){\line(-1,2){5}}
\put(8.5,1){\circle*{1}}
\put(11.5,1){\circle*{1}}
\put(10,10){\circle*{5}}
\put(10,10){\line(0,1){10}}
\negatifc{10}{20}{10}

% fleche
\put(40,17.5){\makebox(0,0){$\longrightarrow$}}

% membre droit
\put(65,10){\line(1,2){5}}
\put(75,10){\line(-1,2){5}}
\put(68.5,11){\circle*{1}}
\put(71.5,11){\circle*{1}}
\put(70,20){\circle*{5}}

\end{picture}

figure_EBM.tex
{\tt
\begin{picture}(60,62)(0,3)
%\put(0,3){\framebox(60,62)}
\thinlines    

%%%%%%%%%%%%%%%%%%%%%%%%
%% General EBM figure %%
%%%%%%%%%%%%%%%%%%%%%%%%


\negatifN{15}{35}{10}
\put(17.5,59){\makebox(0,0){$c_1^{j_1}$}}
\multiput(27.5,35)(2.5,0){3}{\circle*{1}}
\negatifN{45}{35}{10}
\put(47.5,59){\makebox(0,0){$c_K^{j_K}$}}

\positifZero{5}{20}{25}	
\put(20,15){\line(0,1){5}}
\multiput(25,15)(5,0){3}{\circle*{1}}
\put(40,15){\line(0,1){5}}
\put(30,5){\makebox(0,5){$h_i$}}

\end{picture}}

figure_bigStepRed1.tex
{\tt
\begin{picture}(270,110)
%\put(0,0){\framebox(270,110)}
\thinlines    

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% big step reduction ->> first rule %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% membre gauche

% haut
\positifZero{0}{60}{25}
\negatifN{10}{75}{10}
\multiput(22.5,75)(2.5,0){3}{\circle*{1}}
\negatifN{40}{75}{10}
\put(25,95){\makebox(0,5){$\overbrace{\hspace{40pt}}$}}
\put(25,105){\makebox(0,0){$\alpha$}}


\put(10,55){\line(0,1){7}}
\multiput(12.5,55)(2.5,0){3}{\circle*{1}}
\put(20,55){\line(0,1){5}}
\put(15,45){\makebox(0,5){$\beta$}}


% composition

\put(30,45){\line(0,1){15}}
\multiput(32.5,52.5)(2.5,0){3}{\circle*{1}}
\put(40,45){\line(0,1){17}}


% bas

\negatiff{35}{35}{10}
\put(35,30){\line(0,1){5}}
\negatifN{65}{35}{10}
\multiput(77.5,35)(2.5,0){3}{\circle*{1}}
\negatifN{95}{35}{10}
\put(80,55){\makebox(0,5){$\overbrace{\hspace{40pt}}$}}
\put(80,65){\makebox(0,0){$\gamma$}}


\positifZero{25}{20}{40}
\put(60,15){\line(0,1){5}}
\multiput(62.5,15)(2.5,0){3}{\circle*{1}}
\put(70,15){\line(0,1){5}}
\put(65,5){\makebox(0,5){$\delta$}}


% fleche
\put(130,50){\makebox(0,0){$\longrightarrow\!\!\!\!\!\rightarrow$}}

% membre droit

\negatifN{170}{55}{10}
\multiput(182.5,55)(2.5,0){3}{\circle*{1}}
\negatifN{200}{55}{10}
\put(185,75){\makebox(0,5){$\overbrace{\hspace{40pt}}$}}
\put(185,85){\makebox(0,0){$\alpha$}}

\negatifN{230}{55}{10}
\multiput(242.5,55)(2.5,0){3}{\circle*{1}}
\negatifN{260}{55}{10}
\put(245,75){\makebox(0,5){$\overbrace{\hspace{40pt}}$}}
\put(245,85){\makebox(0,0){$\gamma$}}

\positifZero{160}{40}{55}
\put(200,35){\line(0,1){5}}
\multiput(202.5,35)(2.5,0){3}{\circle*{1}}
\put(210,35){\line(0,1){5}}
\put(205,25){\makebox(0,5){$\beta$}}
\put(220,35){\line(0,1){5}}
\multiput(222.5,35)(2.5,0){3}{\circle*{1}}
\put(230,35){\line(0,1){5}}
\put(225,25){\makebox(0,5){$\delta$}}

\end{picture}}

figure_bigStepRed2.tex
{\tt
\begin{picture}(260,100)
%\put(0,0){\framebox(260,100)}
\thinlines    

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% big step reduction ->> second rule %%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% membre gauche

% haut
\positifZero{0}{60}{10}
\negatifN{10}{75}{10}
\put(10,95){\makebox(0,0){$\alpha$}}


% composition

\put(5,45){\line(0,1){16}}
\multiput(7.5,52.5)(2.5,0){3}{\circle*{1}}
\put(15,45){\line(0,1){16}}


% bas

\negatifExt{20}{35}{20}{2}{1}

\put(25,45){\line(0,1){5}}
\multiput(27.5,50)(2.5,0){3}{\circle*{1}}
\put(35,45){\line(0,1){5}}
\put(30,55){\makebox(0,0){$\beta$}}
\put(20,30){\line(0,1){5}}

\negatifN{60}{35}{10}
\multiput(72.5,35)(2.5,0){3}{\circle*{1}}
\negatifN{90}{35}{10}
\put(75,55){\makebox(0,5){$\overbrace{\hspace{40pt}}$}}
\put(75,65){\makebox(0,0){$\gamma$}}

\positifZero{0}{20}{50}
\put(45,15){\line(0,1){5}}
\multiput(47.5,15)(2.5,0){3}{\circle*{1}}
\put(55,15){\line(0,1){5}}
\put(50,5){\makebox(0,5){$\delta$}}


% fleche
\put(125,50){\makebox(0,0){$\longrightarrow\!\!\!\!\!\rightarrow$}}

% membre droit

\negatifExt{175}{55}{20}{2}{1}

\put(160,65){\line(0,1){5}}
\multiput(162.5,70)(2.5,0){3}{\circle*{1}}
\put(170,65){\line(0,1){5}}
\put(165,75){\makebox(0,0){$\alpha$}}
\put(180,65){\line(0,1){5}}
\multiput(182.5,70)(2.5,0){3}{\circle*{1}}
\put(190,65){\line(0,1){5}}
\put(185,75){\makebox(0,0){$\beta$}}
\put(175,50){\line(0,1){5}}

\negatifN{215}{55}{10}
\multiput(227.5,55)(2.5,0){3}{\circle*{1}}
\negatifN{245}{55}{10}
\put(230,75){\makebox(0,5){$\overbrace{\hspace{40pt}}$}}
\put(230,85){\makebox(0,0){$\gamma$}}

\positifZero{155}{40}{50}
\put(200,35){\line(0,1){5}}
\multiput(202.5,35)(2.5,0){3}{\circle*{1}}
\put(210,35){\line(0,1){5}}
\put(205,25){\makebox(0,5){$\delta$}}

\end{picture}}

figure_cloture1.tex
\begin{picture}(85,125)
\thinlines
%\put(0,0){\framebox(85,125){}}
% \om\ exemple 
\positifZero{25}{0}{10}
\negatifDeuxExt{35}{15}{30}{}{c}{3}{1}
\positifUn{0}{35}{10}{}
\negatifDeux{10}{50}{10}{a}{}
\positifDeux{10}{70}{20}{}{b}
\negatifc{30}{85}{10}
% cloture
%\positifUn{40}{35}{20}{}
%\negatifUn{45}{50}{10}{}
%\negatifUn{75}{50}{10}{}
%\positifDeux{0}{100}{40}{}{}
%\negatifc{40}{115}{10}
%\put(5,60){\line(0,1){44}}
%\put(75,60){\line(0,1){44}}
\end{picture}

figure_cloture2.tex
\begin{picture}(85,115)
\thinlines
%\put(0,0){\framebox(85,125){}}
% \om\ exemple 
\positifZero{25}{0}{10}
\negatifDeuxExt{35}{15}{30}{}{}{3}{1}
\positifUn{0}{35}{10}{}
\negatifDeux{10}{50}{10}{}{}
\positifDeux{10}{70}{20}{}{}
\negatifc{30}{85}{10}
% cloture
\positifUn{40}{35}{20}{}
\negatifUn{45}{50}{10}{}
\negatifUn{75}{50}{10}{}
\positifDeux{0}{100}{40}{}{}
\negatifc{40}{115}{10}
\put(5,60){\line(0,1){44}}
\put(75,60){\line(0,1){44}}
\end{picture}

figure_cloture3.tex
\begin{picture}(85,115)
\thinlines
%\put(0,0){\framebox(85,125){}}
% \om\ exemple 
%\positifZero{25}{0}{10}
%\negatifDeuxExt{35}{15}{30}{}{}{3}{1}
%\positifUn{0}{35}{10}{}
%\negatifDeux{10}{50}{10}{}{}
%\positifDeux{10}{70}{20}{}{}
%\negatifc{30}{85}{10}
% cloture
\positifUn{40}{35}{20}{c}
\negatifUn{45}{50}{10}{b}
\negatifUn{75}{50}{10}{}
\positifDeux{0}{100}{40}{}{}
\negatifc{40}{115}{10}
\put(5,95){\line(0,1){9}}
\put(5,90){\framebox(0,0){a}}
\put(75,60){\line(0,1){44}}
\end{picture}

figure_polnet.tex
\begin{picture}(60,80)
\thinlines
%\put(0,0){\framebox(60,80){}}

\put(15,5){\makebox(0,0){$\otimes$}}
\put(15,5){\circle{12}}
\multiput(12.5,15)(2.5,0){3}{\circle*{1}}
\put(12.5,10){\line(-1,1){10}}
\put(17.5,10){\line(1,1){10}}

\put(28,26){\makebox(0,0){$\Par$}}
\put(28,26){\circle{12}}
\multiput(26.5,36)(2.5,0){3}{\circle*{1}}
\put(25.5,31){\line(-1,1){10}}
\put(31.5,31){\line(1,1){10}}

\put(42,47){\makebox(0,0){$\otimes$}}
\put(42,47){\circle{12}}
\multiput(39.5,57)(2.5,0){3}{\circle*{1}}
\put(38.5,52){\line(-1,1){10}}
\put(44.5,52){\line(1,1){10}}

\put(42,65){\makebox(0,5){$\overbrace{\hspace{30pt}}$}}
\put(42,75){\makebox(0,0){$\alpha$}}
\end{picture}

figure_polflatnet.tex
\begin{picture}(122,65)
\thinlines
%\put(0,0){\framebox(122,65){}}

\put(15,5){\makebox(0,0){$\otimes$}}
\put(15,5){\circle{12}}
\multiput(12.5,15)(2.5,0){3}{\circle*{1}}
\put(12.5,10){\line(-1,1){10}}
\put(17.5,10){\line(1,1){10}}

\put(28,26){\makebox(0,0){$\Par$}}
\put(28,26){\circle{12}}
\multiput(26.5,36)(2.5,0){3}{\circle*{1}}
\put(25.5,31){\line(-1,1){10}}
\put(31.5,31){\line(1,1){10}}

\put(42,47){\makebox(0,0){$p_\alpha$}}

\put(42,55){\line(0,1){5}}
\put(42,60){\line(1,0){40}}
\put(82,55){\line(0,1){5}}

\put(82,49){\makebox(0,0){$p_\alpha^\bot$}}

\put(100,5){\makebox(0,0){$\otimes$}}
\put(100,5){\circle{12}}
\put(97.5,10){\line(-1,2){15}}
\put(100,10){\line(0,1){10}}
\put(102.5,10){\line(1,1){10}}

\multiput(105,25)(2.5,0){3}{\circle*{1}}
\put(108,30){\makebox(0,5){$\overbrace{\hspace{20pt}}$}}
\put(108,40){\makebox(0,0){$\alpha$}}
\end{picture}

lmacros.tex
 % zero-width inference rule markers
 % (if they have width, they throw off centering)
\newcommand{\zwb}[1]{\makebox[0cm][l]{{\scriptsize $#1$}}}

\newcommand{\mall}{{\sc mall}}
\newcommand{\ol}{\overline}
\newcommand{\ul}{\underline}
\newcommand{\lan}{\langle}
\newcommand{\ran}{\rangle}

 % Linear Arrow
\newcommand{\la}{\mbox{$-\!\circ$}} 

 % Backwards Linear Arrow
\newcommand{\bla}{\mbox{$\circ\!-$}} 

 % Par
%\newcommand{\Par}{\,{\parfont P}\,}
%\newcommand{\Par}{\mathrel{\wp}}

 % With (Linear And) (&)
\newcommand{\with}{\,{\&}\,}

% Old par
% \newcommand{\Par}{\mbox{\raisebox{.4ex}{$\wp$}}} 

 % PDL's prettier bounded reuse operator
\newcommand{\bang}[1]{\stackrel{\scriptstyle \dagger}{\scriptstyle #1}}
 
 % Implies in Relevant Implication
\newcommand{\ra}{\mbox{$\rightarrow_{R_{\rightarrow}}$}}

 % Relevant Implication (Logic)
\newcommand{\rara}{\mbox{${R_{\rightarrow}}$}}

 % Multiplicative Linear Logic  
\newcommand{\lala}{\mbox{$LL_{\la, \otimes, !}$}}

 % (Propositional) Circular Logic
\newcommand{\cl}{\mbox{ CL }}

 % (Propositional) Multiplicative Circular Logic
\newcommand{\mcl}{\mbox{ MCL }}

 % Definition
\newcommand{\define}{\mbox{${\stackrel{\Delta}{=}}$}}

 % Derived From
\newcommand{\derive}{\mbox{${\stackrel{\vdots}{\vdash}}$}}

 % Semi-Thue Reduction
\newcommand{\stred}[1]{\mbox{$\Longrightarrow$}}

\newcommand{\stredstar}[1]{\mbox{$\Longrightarrow^*$}}

\newcommand{\deltared}[1]{\mbox{$\, \stackrel{\delta_{#1}}
                                             {\longrightarrow} \, $}}

\newcommand{\deltaredp}[1]{\mbox{$\, \stackrel{\delta'_{#1}}
                                             {\longrightarrow} \, $}}


figure_macro.tex
\newcounter{varx}  % la variable x
\newcounter{vary}  % la variable y
\newcounter{vart}  % la variable t
\newcounter{varu}  % la variable u
\newcounter{varv}  % la variable v
\newcounter{size}  % la variable size

%%%%%%%%%%%%
% POSITIFS %
%%%%%%%%%%%%

% positif sans hyp et ccl
\newcommand{\positiff}[3]{% (x,y){sizeReelle*5pt}
\setcounter{varx}{#1}
\setcounter{vary}{#2}
\addtocounter{vary}{10}
\setcounter{size}{#3}
\setcounter{vart}{#3}
\addtocounter{vart}{\value{size}}
\setcounter{varu}{#1}
\addtocounter{varu}{\value{size}}
\setcounter{varv}{#2}
\put(\value{varx},\value{vary}){\line(1,0){\value{vart}}}     
\qbezier(\value{varx},\value{vary})(\value{varx},\value{varv})(\value{varu},\value{varv})
\addtocounter{varx}{\value{size}}
\addtocounter{varx}{\value{size}}
\qbezier(\value{varx},\value{vary})(\value{varx},\value{varv})(\value{varu},\value{varv})
}

% positif 0hyp (sans ccl)
\newcommand{\positifZero}[3]{% (x,y){sizeReelle*5pt}
\positiff{#1}{#2}{#3}
}


% positif 1hyp (sans ccl)
\newcommand{\positifUn}[4]{% (x,y){sizeReelle*5pt}{label}
\positiff{#1}{#2}{#3}
\setcounter{varx}{#1}
\addtocounter{varx}{#3}
\setcounter{vary}{#2}
\put(\value{varx},\value{vary}){\line(0,-1){5}}
\addtocounter{vary}{-10}
\put(\value{varx},\value{vary}){\makebox(0,0){#4}}
}

% positif 2hyp (sans ccl)
\newcommand{\positifDeux}[5]{% (x,y){sizeReelle*5pt}{2labels}
\positiff{#1}{#2}{#3}
\setcounter{varx}{#1}
\addtocounter{varx}{5}
\setcounter{vary}{#2}
\addtocounter{vary}{-5}
\setcounter{vart}{#3}
\addtocounter{vart}{#3}
\addtocounter{vart}{-10}
\ifthenelse{#3 < 15}{%
  \put(\value{varx},\value{vary}){\line(0,1){6.5}}
}{
  \ifthenelse{#3 < 20}{%
    \put(\value{varx},\value{vary}){\line(0,1){7}}
  }{
    \put(\value{varx},\value{vary}){\line(0,1){7.5}}
  }%
}%
\addtocounter{vary}{-5}
\put(\value{varx},\value{vary}){\makebox(0,0){#4}}
\addtocounter{varx}{\value{vart}}
\put(\value{varx},\value{vary}){\makebox(0,0){#5}}
\addtocounter{vary}{5}
\ifthenelse{#3 < 15}{%
  \put(\value{varx},\value{vary}){\line(0,1){6}}
}{
  \put(\value{varx},\value{vary}){\line(0,1){7}}
}%
}

%%%%%%%%%%%%
% NEGATIFS %
%%%%%%%%%%%%

% negatif sans hyp et ccl
\newcommand{\negatiff}[3]{% (x,y){sizeReelle*5pt}
\setcounter{varx}{#1}
\setcounter{vary}{#2}
\setcounter{size}{#3}
\setcounter{vart}{#1}
\addtocounter{vart}{-\value{size}}
\setcounter{varu}{#2}
\addtocounter{varu}{10}
\ifthenelse{#3 = 10}{%
  \put(\value{varx},\value{vary}){\line(1,1){\value{size}}}     
  \put(\value{varx},\value{vary}){\line(-1,1){\value{size}}}
}{}%
\ifthenelse{#3 = 20}{%
  \put(\value{varx},\value{vary}){\line(2,1){\value{size}}}     
  \put(\value{varx},\value{vary}){\line(-2,1){\value{size}}}
}{}%
\addtocounter{size}{\value{size}}
\put(\value{vart},\value{varu}){\line(1,0){\value{size}}}     
}

% negatif sans ccl
\newcommand{\negatifc}[3]{% (x,y){sizeReelle*5pt}
\negatiff{#1}{#2}{#3}
\put(#1,#2){\line(0,-1){5}}
}

% negatif 1ccl (1hyp)
\newcommand{\negatifUn}[4]{% (x,y){sizeReelle*5pt}{label}
\negatifc{#1}{#2}{#3}
\setcounter{vary}{#2}
\addtocounter{vary}{10}
\put(#1,\value{vary}){\line(0,1){5}}
\addtocounter{vary}{7}
\put(#1,\value{vary}){\makebox(0,5)[b]{#4}}
}

% negatif 2ccl (1hyp)
\newcommand{\negatifDeux}[5]{% (x,y){sizeReelle*5pt}{2labels}
\negatifc{#1}{#2}{#3}
\setcounter{varx}{#1}
\addtocounter{varx}{-#3}
\addtocounter{varx}{5}
\setcounter{vary}{#2}
\addtocounter{vary}{10}
\setcounter{vart}{#3}
\addtocounter{vart}{#3}
\addtocounter{vart}{-10}
\multiput(\value{varx},\value{vary})(\value{vart},0){2}{\line(0,1){5}}
\addtocounter{vary}{7}
\put(\value{varx},\value{vary}){\makebox(0,5)[b]{#4}}
\addtocounter{varx}{\value{vart}}
\put(\value{varx},\value{vary}){\makebox(0,5)[b]{#5}}
}

% negatif n ccls (1hyp)
\newcommand{\negatifN}[3]{% (x,y){sizeReelle*5pt}
\negatifc{#1}{#2}{#3}
\setcounter{varx}{#1}
\addtocounter{varx}{-5}
\setcounter{vary}{#2}
\addtocounter{vary}{15}
\put(\value{varx},\value{vary}){\line(0,-1){5}}
%\put(\value{varx},\value{vary}){\makebox(0,0){$\cdot\!\!\cdot\!\!\cdot$}}
\multiput(\value{varx},\value{vary})(2.5,0){5}{\circle*{1}}% dots
\addtocounter{varx}{10}
\put(\value{varx},\value{vary}){\line(0,-1){5}}
}

%% pour les negatifs au format de triangle inhabituel
% comme \negatiff, passage en parametre de la pente
\newcommand{\negatifExt}[5]{% (x,y){sizeReelle*5pt}
\setcounter{varx}{#1}
\setcounter{vary}{#2}
\setcounter{size}{#3}
\setcounter{vart}{#1}
\addtocounter{vart}{-\value{size}}
\setcounter{varu}{#2}
\addtocounter{varu}{10}
\setcounter{varv}{#4}
  \put(\value{varx},\value{vary}){\line(\value{varv},#5){\value{size}}}     
\setcounter{varv}{-#4}
  \put(\value{varx},\value{vary}){\line(\value{varv},#5){\value{size}}}

\addtocounter{size}{\value{size}}
\put(\value{vart},\value{varu}){\line(1,0){\value{size}}}     
}

% negatif 2ccl (1hyp) avec triangle inhabituel
\newcommand{\negatifDeuxExt}[7]{% (x,y){sizeReelle*5pt}{2labels}
\negatifExt{#1}{#2}{#3}{#6}{#7}
\put(\value{varx},\value{vary}){\line(0,-1){5}}
% reste comme \negatifDeux
\setcounter{varx}{#1}
\addtocounter{varx}{-#3}
\addtocounter{varx}{5}
\setcounter{vary}{#2}
\addtocounter{vary}{10}
\setcounter{vart}{#3}
\addtocounter{vart}{#3}
\addtocounter{vart}{-10}
\multiput(\value{varx},\value{vary})(\value{vart},0){2}{\line(0,1){5}}
\addtocounter{vary}{7}
\put(\value{varx},\value{vary}){\makebox(0,5)[b]{#4}}
\addtocounter{varx}{\value{vart}}
\put(\value{varx},\value{vary}){\makebox(0,5)[b]{#5}}
}


Conclusion.tex
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%							CONCLUSION

Concurrent construction of proof-nets allows for a new approach in designing concurrent 
logic programming languages. In the framework developed by Andreoli in recent papers,
we first presented a criterion for testing the correctness of closed modules (i.e.
validity of the execution of a logic program), then we extended the criterion to open modules
after proving that correctness of open modules reduces to testing acyclicity and connectability.
Furthermore, criteria for acyclicity and connectability lead naturally to incremental verification.

Composition.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%							COMPOSITION

In the sequel we discuss an incremental criterion to test the composition of an \om\ with an EBM. 
Let $M$ be an o-correct \om\ and $E$ an EBM st $b(M)\cap
b(E)\not =\emptyset$ (otherwise the test is easy).
As seen above, acyclicity and connectability, hence o-correctness, of $M$ may be decided by computing normal forms. 
Our aim is to decide the o-correction of the composition $M\circ E$ 'incrementally'
i.e. not directly but o-correctness of $M$ being given.
From the previous section we have: 
$$M\textrm{ is o-correct iff }
M\restrict{\emptyset}\bigstep^*\testBotEbm\textrm{ and }M\contract \cc$$

Because of the restriction of $M$ to the empty border, the acyclicity condition given above does not commute with
composition. It is the same for connectability: even if 
there is preservation of the border with $\contract$, a choice is made for the completion of $M$
which may be different from the way composition with $E$ is done. For example we have:

\smallskip

\begin{center}
\heightcenter{\input{Figures/figure_completion1}}\heightcenter{ and }~
\heightcenter{\input{Figures/figure_completion3}}
\heightcenter{ but }~\heightcenter{\input{Figures/figure_completion2}}
\end{center}

In the sequel we show that if we release the restriction operation we can 
incrementally manage acyclicity. The relax of the (implicit) 
completion in the rewriting rules dealing with connectability gives also an incremental (but not so
convenient) criterion for connectability. 

\subsection{Incremental acyclicity}

Note that the restriction to empty set is stable wrt the reduction $\bigstep$ i.e. if $M$ is an \om\ st $M\bigstep^1 N$ then $M\restrict{\emptyset}\bigstep^1 N\restrict{\emptyset}$.
Hence an incremental test for acyclicity follows:

\begin{proposition}%[incremental acyclicity]
Let $M$ be an \om\ st $M\bigstep^* f$ and $E$ an EBM. 
$M\circ E$ is acyclic if $(f\circ E)\restrict{\emptyset}\bigstep^*\testBotEbm$.
\end{proposition}

\begin{proof}
If $M\bigstep^* f$ then $(M\circ E)\bigstep^* (f\circ E)$. Following previous remark,
$(M\circ E)\restrict{\emptyset}\bigstep^* (f\circ E)\restrict{\emptyset}$. 
Thus if $(f\circ E)\restrict{\emptyset}\bigstep^*\testBotEbm$ then 
 $(M\circ E)\restrict{\emptyset}\bigstep^*\testBotEbm$. \hfill $\qed$
\end{proof}
%
\subsection{Contraction relation (without completion)}

We consider the rewriting system given to test connectability where rule (4) is
restricted to the following degenerated case ($\alpha =I=\emptyset$ and application of rule (2)):

\smallskip

\begin{center}
\input{Figures/figure_contraction6}
\end{center}

We denote by $\wcontract^1$ one rewriting step and by $\wcontract$ the 
reflexive and transitive closure of $\wcontract^1$.  
As it is a subsystem of the previous one, the relation $\wcontract$ terminates and is still strongly
confluent (there is only trivial independant pairs).

\smallskip

We study the normal forms. 
By definition an \om\ contracts in a normal form composed with only 
contracted nodes or contracted modules
where each negative pole $N$ is of the following form:
\medskip

\noindent\begin{minipage}{.5\textwidth}
\begin{center}
\input{Figures/figure_form1}
\end{center}
\end{minipage}
\begin{minipage}{.5\textwidth} 
\begin{itemize}
\item[-] $I$ is a (possibly empty) set of contracted nodes,
\item[-] each $i\in I$ is linked to
a set $C_i$ of other negative poles by conclusions and to a set $H_i$ of other
negative poles by hypothesis (the sets $C_i$ and $H_i$ may be empty). Moreover
for all $c_i\in C_i$ $\beta_i\not =\emptyset$,
\item[-] $\alpha$ and $\alpha_i$ are (possibly empty) subsets of $b(M)$ for all $i\in I$.
\end{itemize}
\end{minipage}
\medskip

We focus on the two possible forms of negative pole:
\begin{itemize}
\item[-] there exists $i_0\in I$ st $\alpha_{i_0} =H_{i_0} =\emptyset$. We denote such forms by $\notcc$. 
\item[-] for all $i\in I$,  $\alpha_i\not =\emptyset$ or 
$H_i\not =\emptyset$. These negative poles may be considered in the
  previous system $\contract$. 
\end{itemize}

If a normal form has no negative poles then it is a set of 
contracted nodes. We add to the $\notcc$ forms the case where there is at least
one contracted node without pending edges and other nodes.

\smallskip

In order to compare these normal forms with the normal forms of $\contract$ observe that:
(i) by definition of normal forms, if $I=\emptyset$ then
  $\alpha\not =\emptyset$, and if $I\not =\emptyset$ then 
  $\mid I\mid\geqslant 2$ or $\alpha\not =\emptyset$, 
(ii) for all $i\in I$ for all $c_i\in C_i$ we have $\beta_i\not
=\emptyset$.
It follows that if a normal form $g$ wrt $\wcontract$ of an \om\ $M$ contains a
$\notcc$ subform then there is a
generalized switch st $g$ is not connected. The stability of
connexity wrt $\wcontract$ being given, $M$ is not connected (neither its closures), thus not connectable. 

Remark that the $\notcc$ forms are already in the previous system: they are normal forms which are not the $\cc$ forms! In fact the $\notcc$ subforms are
invariant wrt the previous system $\contract$.
Moreover as inverse stability of connectability is easily proven, we have: 

\begin{theorem}\label{thmS2Connectability}
Let $M$ be an \om , $M$ is connectable iff 
$M\wcontract g$ st $\notcc\not\in g$.
\end{theorem}

\begin{proof}
Let $M$ be st $M\wcontract g$. If $\notcc\in g$ then $g$ is not connected (neither its closures) and by stability of
connexity $M$ is not connectable. Conversely, if $\notcc\not\in g$ then
$g\contract \cc$ by invariance of $\notcc$ wrt $\contract$. By theorem
\ref{thmS1Connectability}, $g$ is connectable. The result is obtained by inverse stability of
connectability wrt $\wcontract$.\hfill $\qed$
\end{proof}

Hence, an \om\ $M$ is o-correct iff $M$ is acyclic and $M\wcontract g$ st 
$\notcc\not\in g$.
By confluence property and theorem \ref{thmS2Connectability} we have an incremental test:
Let $M$ be a connectable \om\ st $M\wcontract g$ and $E$ an EBM st $b(M)\cap
b(E)\not =\emptyset$. We have:
$$M\circ E\textrm{ is connectable iff }f\circ E\wcontract g
\textrm{ st }\notcc\not\in g.$$

\subsection{A test for composition}
Testing the composition of an EBM $E$ on a correct module $M$ may be done in the following way. We associate to such a module $M$ a pair $(f,g)$ such that $M\bigstep^* f$ and $M\wcontract g$. We compute the pair $(f',g')$ associated to $M\circ E$: $f\circ E\bigstep^* f'$ and $g\circ E \wcontract g'$. Then $E$ may be plugged onto $M$, i.e. the composition is correct, iff $f'\restrict{\emptyset}\bigstep^*\testBotEbm$ and $\notcc \not\in g'$. This test may be implemented in such a way that pre-computations are done in $M$ in order to optimize the test. Moreover this pre-computation allows for a concurrent treatment for testing composition by only locking a reduced part of the module $M$.



Introduction.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%							INTRODUCTION

In the last few years, Andreoli~\cite{Andreoli01APAL,Andreoli02CADE,Andreoli03CSL} investigated a new style of logic programming aware of resources and aiming at expressing non-determinism, concurrency and (possibly) infinite computations.  Logic programming facilitates naturally non-determinism. The other
characteristics are out of scope when logic programming is only used for
proving goals (possibly by instantiating first order variables). 
Indeed, proof construction can be goal-directed (and the hypothesis is given as a set of special clauses) or hypothesis-directed (and the goal may be empty). This latter case can be reduced to the first one
by contraposing each implication and considering negation of hypotheses as the
goal: each resolution is then interpreted as a transformation of the
environment. Computation ends when the current environment is empty. 
As computations build partial proofs, there is no difficulty to take care of (potentially) infinite computations.

It is now a well-known fact that linear logic, a resource-conscious logic, may be used as a
programming language after Andreoli's works~\cite{Andreoli92}.\footnote{Full
first-order linear logic can be used as a programming language. However, we
restrict in this paper to propositional multiplicative linear logic.} In the
paper just cited, he took a standard approach and his presentation was sequential. More recently, Andreoli takes care of concurrency by switching to proof-nets as this syntax affords a desequentialized presentation of proofs, hence a concurrent way to compute them at the expense of a correctness criterion that guarantees to recover sequentialization, i.e. validity of proofs. In this paper, we search for a generalization of his results in order to have full expressivity. For that purpose, we depart from his approach by adopting a graph point of view.
Equivalent to clauses in standard logic programming, 
{\em modules}, as graph elements, arise naturally from proof nets. 
In a few words, associativity, commutativity\footnote{and distributivity when dealing with the additive part of linear logic.} and focalization lead
to polarize formulae, hence to stratify proofnets. Bipolar structures become
computational structures as composition of such structures corresponds to some
kind of progression rule.

Andreoli set up this desequentialized framework for middleware infrastructures.
In such applications, software agents must satisfy requests or goals by
executing concurrently actions on a shared 
environment. Resources model concrete objects, e.g. documents, or high-level elements, e.g. functionalities. Actions transform the environment by deleting resources and creating sets of results exclusive each other. Andreoli focused on {\em transitory} proof-structures, i.e. actions always create new resources. Moreover, he imposes prerequisites of actions to be satisfied in order to execute them: the proof construction is exclusively done bottom-up. As we shall see in section~\ref{Open_modules}, these two hypotheses greatly simplify the problem of defining formally conditions under
which actions may be undertaken. On the contrary, we constrain neither the structure of modules, nor the application order. It is then possible to define actions that kill resources (e.g. close a branch in a plan, or withdraw a functionality or a resource) or to anticipate consequences of 
resources still to be acquired. Furthermore, we depart from Andreoli's approach for defining a correctness criterion. His method is based on a computation of domination forests in the spirit of Murawski and Ong's approach~\cite{Murawski_Ong00}. We adopt
here a completely different strategy. We define reduction relations in order
to get constraints on execution.

The following section gives basic definitions. We formally present modules from elementary ones, graphically and in terms of formulae. We specify in which sense a module is correct, i.e. the computation
is allowed. Section~\ref{Closed_modules} is devoted to closed modules. A module is closed when computation ends. Although closed modules are an extreme special case of modules, the methodology we use introduces naturally the way we consider open modules. In a first attempt, we reformulate the resolution rule as a rewriting rule on modules, the Danos-Regnier criterion being used for characterizing correct normal forms. The Danos-Regnier criterion is based on graph properties of proof nets: correct proof structures, i.e. proof nets, are in some sense the connected and acyclic ones. We deduce a correctness criterion for closed modules as our rewriting rule is stable and inverse stable wrt connexity and acyclicity. We define next a modified version of the previous rewriting system that takes care of the parallel structure of modules. Open modules, i.e. modules without constraints, are studied in section~\ref{Open_modules}. We prove that the Danos-Regnier criterion may be extended to open modules seeing that we replace connexity by connectability. We give two rewriting systems as acyclicity and connectability differ fundamentally. These two systems may be viewed as variations over the one we give for closed modules. We end with a study on incrementality wrt composition of modules. In terms of computation, elementary modules compete to modify some
current module (the environment). It is then crucial to be able to define rewriting systems that commute with composition. We show that we have to restrict previous rewriting systems for that purpose.
However, the rewriting systems have to be splitted into two parts: one commutes with composition, the other is a post-treatment necessary to test correctness of composition.\footnote{Complements and some technical proofs are available in the annex of
the submission and will be omitted in the final version but remain in a preprint version.}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%							BASIC DEFINITIONS
\section{Basic definitions}

Elementary bipolar modules are our basic blocks. They are interpreted as elementary actions that can take place during an execution. In terms of graph, applying an action is represented as a wire, i.e. composition, of the corresponding (elementary) module onto the current graph. In terms of sequent calculus, this is a resolution step.

\begin{definition}[EBM]
An {\em elementary bipolar module} (EBM) $M$ is given by a finite set ${\cal H}(M)$ of propositional variables (called hypotheses) $h_i$ 
and a non empty finite set ${\cal C}(M)$ varying over $k$ of finite sets of propositional variables (called conclusions) $c^j_k$. Variables are supposed pairwise distinct.\footnote{This restriction is taken for simplicity. The framework can be generalized if we consider multisets (of hypotheses and conclusions) instead of sets, and add as required a renaming mechanism: the results in this paper are still true.} The set of propositional variables appearing in $M$ is noted $v(M)$. Equivalently, one can define it as an oriented graph with labelled pending links and one positive pole under a finite set of negative poles. Its type $t(M)$ and draw are given in the following way:
%
%\begin{tabular}{cr}
\begin{center}
\heightcenter{$t(M) = (\bigotimes_i h_i) \la (\bigPar_{\!\!k} (\bigotimes_{j_k} c^{j_k}_k))$}\hspace{1cm}\heightcenter{\input{Figures/figure_EBM}}
\end{center}
%\end{tabular}
%
The set of variables, or equivalently the set of pending links of a module $M$, is called the {\em border} $b(M)$.
\end{definition}

This specification of modules comes from the fact that connectives are naturally split into two sets: e.g. $\otimes$ is said positive, while $\Par$ is negative. Propositional variables are declared positive, and their negation negative. Formulae alternate positive and negative levels up to propositional variables. Moreover, it is possible to flatten proofnets to get bipolar structures related by links on fresh variables as in figure~\ref{flatten_proofnets}. If we notice that a variable and its negation cannot be together linked to negative nodes (it would contradict the correctness criterion), we can always suppose that, say, positive variables are linked to negative nodes. Finally, it may be the case that some bipolar structure (thus beginning with a positive node at bottom) has no negative variable: add then the constant ${\mathbf 1}$, neutral for $\otimes$. Allowing abusively unary $\otimes$ and $\Par$ connectives, these (elementary) bipolar structures are the clauses of our programming language.  

\begin{figure}[h]
\begin{center}
%\null\vspace{-7mm}
\heightcenter{\input{Figures/figure_polnet}}
$\qquad\longrightarrow\qquad$
\heightcenter{\input{Figures/figure_polflatnet}}
\end{center}
\null\vspace{-7mm}
\caption{flatten of proof-nets}\label{flatten_proofnets}
\end{figure}

We thus conveniently suppose that $\bigPar_{\!\!k} F_k = \bigotimes_k F_k = F_1$ when 
the domain of $k$ is of cardinal 1. Moreover, if the domain of $i$ is empty, $(\bigotimes_i h_i) \la C = {\mathbf 1} \la C$ and if the domain of $j_k$ for some $k$ is
empty $(\bigotimes_{j_k} c^{j_k}_k) = \bot$.


\begin{example}
The EBMs $\alpha$ and $\beta$ of respective types $t(\alpha) = \TypeExA$ and 
$t(\beta) = \TypeExB$ are drawn in the following way:

\begin{center}
\heightcenter{\input{Figures/figure_drawExA}} 
$\qquad$ and $\qquad$
\heightcenter{\input{Figures/figure_drawExB}}
\end{center}
\end{example}

Three kinds of EBMs are of special interest:
%
An EBM is {\em initial} (resp. {\em final}) iff its set of hypotheses is empty (resp. its set of conclusions is empty).
An EBM is {\em transitory} iff it is neither initial nor final.
%
Initial EBMs allow to declare available resources, though final EBMs stop part of a computation by withdrawing a whole set of resources. Transitory EBMs are called definite clauses in standard logic programming.

Roughly speaking, a (bipolar) module (BM) is a set of EBMs such that a label appears at most once as a conclusion and at most once as a hypothesis. A label appears as a conclusion and as a hypothesis when two EBMs
are linked by this label. As we search for correctness criteria wrt composition of modules (i.e. execution
of the program), we give below an inductive definition of bipolar modules.

\begin{definition}[BM]
A {\em bipolar module} (BM) $M$ is defined with hypotheses ${\cal H}(M)$, conclusions ${\cal C}(M)$, and type $t(M)$, inductively in the following way:

\begin{itemize}
\item An EBM is a BM.
\item Let $M$ be a BM, and $N$ be an EBM, let $I = {\cal C}(M) \cap {\cal H}(N)$, their {\em composition} wrt the {\em interface} $I$, $M \circ_I N$ is a BM with :
	\begin{itemize}
	\item the multiset of hypotheses ${\cal H}(M) \cup ({\cal H}(N) - I)$
	\item the multiset of conclusions $({\cal C}(M) - I) \cup {\cal C}(N)$
	\item the type $t(M) \otimes t(N)$
	\item the variables $v(M) \cup v(N)$
	\end{itemize}
\end{itemize}
\end{definition}

The informal explanation given before is more general than this definition because we define BM incrementally. However, we abusively do not consider these differences in the following as properties will be proven in the general case. The interface will be omitted when it is clear from the context. Note that the interface may be empty: it only means that two computations are undertaken, currently without any shared resources. A BM may not correspond to a valid computation: e.g. we do not want to accept that some action uses two resources in disjunctive situation! Correctness has obviously to be defined wrt the underlying Linear Logic as we do below. Finally, note that when a BM is correct, it represents
the history of the computation whereas its conclusion is the current available environment.

\begin{figure}[h]
\begin{center}
\heightcenter{\input{Figures/figure_exemple2}
\hspace{1cm}
\input{Figures/figure_exemple3}
\hspace{1cm}
\input{Figures/figure_exemple4}}
\end{center}
\caption{examples \ref{ex2} and \ref{ex34}}\label{figureEx234}
\end{figure}

\begin{example}\label{ex2}
The composition of the EBMs $\alpha$ and $\beta$ is the BM $\alpha
\circ_{\{b\}} \beta$ drawn in figure \ref{figureEx234}. Its type is $t(\alpha) \otimes t(\beta)$.
\end{example}

\begin{definition}[Correctness (wrt sequentialization)]
Let $M$ be a BM, $M$ is {\em correct} iff there exists a formula $C$ built
with the connectives $\otimes$ and $\Par$, and the variables ${\cal C}(M)$ such
that the sequent ${\cal H}(M), t(M) \vdash C$ is provable in Linear Logic.
\end{definition}

\begin{example}\label{ex34}
Let us give two more BMs $\delta$ and $\gamma$ of respective types $\TypeExD$ 
and $\TypeExG$.

\begin{itemize}
\item The following sequent is provable in LL: $a, t(\alpha \circ \beta \circ \gamma \circ \delta) \vdash d \Par (e \otimes j \otimes h) \Par i$. The (correct) BM 
$\alpha \circ \beta \circ \gamma \circ \delta$ is drawn in the figure 
  \ref{figureEx234}.
\item Let $\epsilon$ be an EBM of type $\TypeExE$, the BM $\beta \circ
  \epsilon$ is not correct. Note the trip through $d$ and $e$ in the figure \ref{figureEx234}.
\end{itemize}
\end{example}

As we shall focus first on characterizing correctness on closed modules, and
then generalize our results to open modules, we adjoin to the term {\em
correct} the kind of modules we speak of, e.g. c-correct when the module is
closed, o-correct when it is open.


Open_modules1.tex
\subsection{O-correction}

We focus in this section on open modules. An {\em \om } is a possibly non closed BM. The bigstep reduction relation presented in the previous section is not sufficient to characterize again
correction of \om. Let $U$ be the first module of the
next example. One
cannot apply on $U$ a bigstep reduction on the negative pole with variable $a$ as this pole remains in the normal form though $U$ seems correct.
The c-correctness theorem~\ref{c-correctness} is no more valid for \om s.

Correctness of open modules is defined wrt correctness of closed extensions.
A {\em closure} $\overline{M}$ of an \om\ $M$ is a \cm\ 
such that $M$ is a submodule of $\overline{M}$.
As a BM is a graph with pending edges, one defines
submodules and induced modules as expected.
We use the notation $\widetilde{M}$ for the module
$\overline{M}$ without $M$ but with border $b(M)$.
In the following example $\overline{U}$ is a closure of $U$ st $\widetilde{U}$ is the right module. 
The composition of $U$ with a set of only initial/final EBMs is a closure too.
%
\begin{center}
\heightcenter{$U$:}~\heightcenter{\input{Figures/figure_cloture1}}~
\heightcenter{$\overline{U}$:}~\heightcenter{\input{Figures/figure_cloture2}}~
\heightcenter{$\widetilde{U}$:}~\heightcenter{\input{Figures/figure_cloture3}}
\end{center}

An \om\ $M$ is {\em o-correct} iff there exists a c-correct closure of $M$. 
The \om\ $U$ of the example is o-correct because
the given closure is c-correct. Note that there is no other c-correct closure. Hence it is not possible in general to split the problem of finding a closure into finding a completion by initial modules and final modules. In the previous section, we defined a rewriting system able to test the correctness of a closed module. As this system is stable wrt connexity and acyclicity, it is invariant wrt the Danos-Regnier criterion. In order to take care of open modules, we extend connexity to connectability (acyclicity is
treated easily) and prove that connectability and acyclicity are necessary and sufficient for o-correctness.
However, we are not able to define a single rewriting system that commutes with composition. 
%
An \om\ $M$ is {\em acyclic} if for all generalized switches $s$ on $M$, 
$s(M)$ is acyclic. Note that a submodule of an acyclic module is obviously
acyclic.

An \om\ $M$ is {\em connectable} iff there exists a connected closure 
$\overline{M}$ st $\widetilde{M}$ is acyclic.
%
As a connected \cm\ is already connectable (just take itself as closure), the connectability is an extension of the connexity property.
%
We give an equivalent definition: an \om\ $M$ is connectable iff the \cm\ $M\circ F$ is connected
where $F$ is a {\em full connector} EBM for $M$, i.e. $F$ has as hypotheses the set of conclusions of $M$, is final if $M$ has no hypothesis or has a negative pole with one conclusion for each of its hypotheses.
%
In fact if there exists a connected closure $\overline{M}$ then 
$M\circ\widetilde{M}$ is connected. So {\em a fortiori}, $M\circ F$ is
connected. The converse comes from the definition.

\begin{theorem}[o-correction]\label{thmOcorrection}
An \om\ $M$ is o-correct iff $M$ is acyclic and connectable.
\end{theorem}

\begin{proof}{\parindent=0pt
By definition o-correction implies acyclicity and connectability.

If $M$ is acyclic and there exists a connected closure $\overline{M}$ st
$\widetilde{M}$ is acyclic then by induction on the number of cycles of
$\overline{M}$, one can construct an acyclic and connected closure of $M$. 

If there is a cycle $\sigma$ in $\overline{M}$ then by hypothesis $\sigma\cap
b(M)\not =\emptyset$. Suppose there exists a hypothesis of $M$ $h\in\sigma\cap b(M)$, 
one defines $N$ to be $\widetilde{M}$ where we substitute a fresh label $h'$ to $h$.
Let $N'$ be the composition of the initial EBM of
border $\{ h\}$, the final EBM of border $\{h'\}$ and $N$. $M\circ N'$ has one cycle less than
$\overline{M}$ and is a connected closure. 

Otherwise the elements of $\sigma\cap b(M)$ are conclusions of $M$.
Let $c$ be such a conclusion. We consider the following cases:
\begin{itemize}
\item[-] if $c$ in  $\sigma\cap b(M)$ is the only conclusion of a negative pole $n$, then one can do the
same thing as in the previous case.  
\item[-] else let $d$ be a conclusion in  $\sigma\cap b(M)$ distinct from $c$ of $n$. 
One renames $c$ (resp. $d$) in $\widetilde{M}$ in $c'$ (resp. $d'$) to get $N$. One defines also an EBM $D$ with one conclusion $d'$ and two hypotheses $c$ and $d$, and an initial EBM $E$ with conclusion $c'$. Then
$X = M\circ D \circ E \circ N$ is a connected closure of $M$ and $D\circ E \circ N$ is acyclic. Hence $X$
is a connected closure of $M\circ D$ and $E\circ N$ is acyclic. We suppressed the cycle $\sigma$. However, it may be the case that there were a cycle through $d$ and $D$ doubles it ! For that purpose, we transform $M$ to get rid of this extra cycle. Let $M'$ be $M$ where we identify the two edges labelled $c$ and $d$ in one labelled $d'$. Then $M'\circ E \circ N$ is a connected closure of $M'$ and $E\circ N$ is acyclic. Moreover the number of cycles in $M'\circ E \circ N$ is one less than in $\overline{M}$. Thus there exists $N'$ acyclic such that $M'\circ N'$ is c-correct. Hence $M\circ D\circ N'$ is c-correct.\hfill $\qed$
\end{itemize}
}\end{proof}


Open_modules2.tex
\subsection{Acyclicity and Connectability Criteria}

\subsubsection{Acyclicity. }
An \om\ $M$ {\em restricted to the subset $I$} of $b(M)$ is the
subgraph of $M$ where we omit pending edges not in $I$. 
We denote it $M\restrict{I}$. 
%
Unformally an \om\ $M$ restricted to $I$ is a submodule 
of border $I$.
The restriction of
an \om\ to the empty set is a \cm.
Restriction gives naturally an equivalent definition of acyclicity for open modules: 
an \om\ $M$ is {\em acyclic} iff the \cm\ $M\restrict{\emptyset}$ is
acyclic. Hence the proposition given in the previous section applies:

\begin{proposition}[acyclicity]
An \om\ $M$ is acyclic if $M\restrict{\emptyset}\bigstep^*\testBotEbm$.
\end{proposition}

\begin{proof}
$M\restrict{\emptyset}$ is a \cm\ and $M\restrict{\emptyset}\bigstep^*\testBotEbm$ then by (inverse) stability of acyclicity $M\restrict{\emptyset}$ is acyclic. $M$ is then acyclic.\hfill $\qed$
\end{proof}

Note that the converse is not true, otherwise acyclic closed modules would be correct! A way to characterize acyclicity by means of a reduction relation is to enlarge the reduction $\bigstep$ (quotienting the set of normal forms). Splitting the negative poles suffices to continue reduction until we get a non-empty set of $\testBotEbm$: closing modules may link disjoint connected components. It is then obvious to deduce a necessary and sufficient condition for acyclicity.

Andreoli considered in \cite{Andreoli03CSL} only transitory proof-structures. 
A {\em transitory proof-structure} is equivalent to a BM without
hypothesis\footnote{In fact, there may be hypotheses in built modules but these are unused.} such that negative poles have always conclusions and obtained by a
bottom-up composition of EBMs. As negative poles have pending edges, there is always a way to
connect it to other parts of the module: if a transitory module $M$ is acyclic then $M$ is connectable.
Hence a transitory module $M$ is o-correct iff $M$ is acyclic.
The reduction relation we give to test acyclicity can be considered as an
alternative to Andreoli's method.
%
\subsubsection{Connectability : a contraction relation. }
%
The proof of the correctness of the big step reduction relation for closed modules gives the keys for finding a connectability property that relies on the structure of an open module (and not on the modules candidate to close it !). Proof of theorem~\ref{c-correctness} is based on reducing first maximal negative poles. In the case of open modules, maximal elements may have pending edges that should be connected
in the closure. But we notice that we keep connectability if we replace the whole set of pending edges for such an element by just one pending edge. 
With this in mind, we consider the following (non oriented) contraction relation on (contracted) modules:
\smallskip

\noindent\begin{center}
\begin{tabular}{lcl}
(1)\hspace{.5em}\heightcenter{\input{Figures/figure_S1contraction1}}
& \hspace{1em} & \hspace{45pt} (2)\hspace{.5em}
\heightcenter{\input{Figures/figure_S1contraction3}}\\
\\
\hspace{25pt} (3)\hspace{.5em}
\heightcenter{\input{Figures/figure_S1contraction2}} & &
(4)\hspace{.5em}\heightcenter{\input{Figures/figure_S1contraction4bis}}
\end{tabular}
\end{center}

Rule (4) is restricted to cases where the negative pole is such that for all $i\in I$,
$\alpha_i\cap b(M)\not=\emptyset$ and $\alpha\subseteq b(M)$ where $b(M)$ is
the set of pending edges of $M$, i.e. the border set. The sets $I$ and
$\alpha$ may be empty. 
We denote by $\contract^1$ one rewriting step and by $\contract$ the 
reflexive and transitive closure of $\contract^1$.  We call {\em contracted
  node} a black node. 
Note that rule (4) is simply the rewriting 
of a negative pole in a contracted node if the condition is satisfied. Thus
acyclicity is not preserved but connectability is.

\begin{proposition}
The relation $\contract$ is strongly confluent and terminates.
\end{proposition}

\begin{proof}
The first rule acts just as a mark. We can forget it: it is just for
convenience. Each rule applies locally and strictly decreases the number of
negative poles and contracted nodes. 
The rules are disjoint except for a pair of negative poles linked
by the same contracted node $i_0$ for which rule (4) can be applied 
(it is a trivial case), and except for a left member of
rule (3) st rule (4) applies too: in this case results are identical.\hfill $\qed$
\end{proof}

We extend the notions of switching to modules with contracted nodes: contracted nodes are treated as positive poles. Acyclicity, connexity, closure and connectability are extended in the same way.
As in section devoted to closed modules, our strategy consists in characterizing amongst normal forms of this relation the correct ones, and prove stability of, say, connectability.
Let $M$ be an \om\ and $f$ the corresponding normal form. By definition if $f$ does not contain a negative
pole then $f$ is a set of contracted nodes $\{ n_j\}_{j\in J}$ st all pending egdes are in $b(M)$.
We use the notation \cc\ for a set of contracted nodes $\{ n_j\}_{j\in J}$ st for all $j\in J$ $n_j$ has at least one edge in the border $b(M)$ except if $\mid J\mid =1$. 
If $f$ contains a negative pole $N$ then, $f$ being a normal form of relation $\contract$,
rule (4) does not apply on $N$. Hence the set $I$ as defined by rule (4) is st
there exists $i_0\in I$, $\alpha_{i_0}\cap b(M)=\emptyset$. Moreover this
contracted node $i_0$ is linked to hypotheses of negative poles $\{h_l\}_{l\in L}$ and to conclusions of only negative poles $\{c_k\}_{k\in K}$ st
each of them has other conclusions $\beta_k\not =\emptyset$ not linked to
$i_0$ (otherwise rule (2) applies for such nodes):
\begin{center}
\input{Figures/figure_normalForm1}
\end{center}
If we suppose the negative pole $N$ is a maximal one (i.e. $H = \emptyset$), there is a switching (on $\alpha$ or on some $i\not =i_0$ and on one of each
$\beta_k$) st $f$ (as closures of $f$) is not connected.
Thus $f$ is not connectable.

\begin{example}\label{exNotcc}
The following subforms imply not connectability:

\begin{center}
\begin{tabular}{ccc}
\heightcenter{\input{Figures/figure_completion2}} & \hspace{2cm} & \heightcenter{\input{Figures/figure_notcc2}}
\end{tabular}
\end{center}
\end{example}

\begin{proposition}[stability]\label{propS1Stability}
Connectability is stable wrt (resp. inverse) contraction rules.
\end{proposition}

\begin{proof}
The three first rules satisfy obviously stability and inverse stability.
Let $M$ be an 
\om\ st $M\rightarrow_c^1 M'$ by the contraction rule
$(4)$ and there exists $\overline{M}$ connected and $\widetilde{M}$ acyclic. 
Obviously $M'\circ \widetilde{M}$ is connected.
Concerning inverse stability, 
let $M$ be an \om\ st $M\rightarrow_c^1 M'$ by the contraction rule
$(4)$ and let $F$ be a full connector EBM for $M'$. Note that $b(M')=b(M)$. 
The connectability of $M'$ implies that $M'\circ F$ is connected. 
Wrt rule (4), because for all $i\in I$, $\alpha_i\cap b(M)\not=\emptyset$ and
$\alpha\subseteq b(M)$, for every switches $s$, $s(M\circ F)$ is
connected too. \hfill $\qed$
\end{proof}

By stability and inverse stability of connectability we have:
%
\begin{theorem}\label{thmS1Connectability}
Let $M$ be an \om , $M$ is connectable iff $M\contract \cc$. Hence an \om\ $M$ is o-correct iff $M$ is acyclic and $M\contract \cc$.
\end{theorem}


Closed_modules.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%	NET / BIG STEPS

A \cm\ is a BM where the sets of hypotheses and conclusions
are empty. Correctness of closed modules may be tested either in sequent calculus or by means of proofnets. We use this latest representation in this section.
Girard in his seminal paper~\cite{Girard87} gave a parallel syntax for multiplicative linear logic as oriented graphs called {\em proof-nets}. A {\em correctness criterion} enables one to distinguish sequentializable proof-structures (say such oriented graphs) from "bad" structures.
The reader may find in~\cite{Danos_Regnier89} the definitions of proof structures and switchings. One generalizes this definition to n-ary connectives in the obvious way (taking care of associativity and commutativity of $\otimes$ and $\Par$) in place of standard binary ones. One modifies in the same way the definitions of switching introducing generalized switches. In particular a $n$-ary $\Par$ connective has $n$ switched positions. 
One still can define switched proof-structures and a criterion 
generalizing Danos-Regnier correctness criterion: 
A \cm\ $M$ is DR-correct iff for all generalized switches $s$ on $M^*$, 
$s(M^*)$ is acyclic and connected, where $M^*$ is the proof structure associated to $t(M)^\bot$.\footnote{We abusively note $s(M)$ in place of $s(M^*)$ in the following.}
We immediately have the following proposition as a corollary of the DR-criterion theorem:
\begin{proposition}[c-correction]
Let $M$ be a \cm,
\begin{tabbing}
$M$ is c-correct 
\= iff $t(M) \vdash$ is provable in Linear Logic,\\
\> iff $M$ is DR-correct.
\end{tabbing}
\end{proposition}

Remember that the equivalent (binary) Danos correctness criterion
%~\cite{Danos90} 
may be implemented by means of a contraction relation on proof structures. However, intermediate reduced structures may not be describable in terms of (bipolar) modules. Moreover such a contraction relation does not take advantage of the incremental definition of modules as a composition of elementary bipolar modules. A first idea consists in representing the resolution step (implicit in EBMs composition) in terms of modules. We first give below such a (small step) reduction rule that is
stable wrt correctness with \testBotEbm as the correct normal form, where  \testBotEbm denotes the terminal EBM (i.e. smallest final and initial). We give then a second proposal that takes care of the focalization property. Though a resolution step reduces one variable, this second formulation uses as a whole the structure of a module thanks to focalization.

Let $\leadsto_{\Theta}$ be the transitive closure of the following relation defined on literals of a proof-structure $\Theta$: let $u$ and $v$ be two literals of $\Theta$, $u \leadsto_{\Theta} v$ iff $u^\bot$ and $v$ are in the same subtree with root $\otimes$ of the formula corresponding to $\Theta$. We note $u\leadsto v$ when there is no ambiguity.
In the following, we consider proof-structures modulo neutrality of the constant $1$ and associativity of connective $\Par$.

\begin{definition}[Small step reduction rule]
Let $\rightarrow$ be the reduction relation given by: if $\forall v$ a literal
of $\psi$, $v\not\leadsto x^\perp$ then 
%
\begin{center}
\heightcenter{\input{Figures/figure_smallStep1}}
\heightcenter{$\qquad\longrightarrow\qquad$}
\heightcenter{\input{Figures/figure_smallStep2}}
\end{center}
\end{definition}

\begin{theorem}[(small steps) Correctness criterion]
Let $M$ be a closed BM, $M$ is correct iff $M^* \rightarrow^\star 1$.
\end{theorem}

Briefly speaking, one can prove that the relation $\longrightarrow$ and the inverse relation are stable wrt DR-correctness by induction over the height of $\psi$.
One may want to get rid of the (global) condition in favor of a local condition. This is possible thanks to the structure of modules. Suppose $M$ is a correct closed module, then one may define an equivalent proof-net by sufficiently adding fresh variables as described in the introduction. It is easy to prove that the constraint is satisfied by $x$ or $x^\bot$ for each variable $x$. However, the reduction system being not strongly confluent, a reduction on a variable may lead to a proof structure on which the condition is not always satisfied. There are two cases where this does not happen: either all variables on a tensor have their negation on the same $\Par$, or the converse interchanging $\Par$ and $\otimes$. 
The following (big step) reduction relation $\twoheadrightarrow$ with two rewrite rules uses this fact. Note that this system is
confluent and terminates.

\begin{center}
\input{Figures/figure_bigStepRed1}

\input{Figures/figure_bigStepRed2}
\end{center}

\begin{proposition}[Stability]
Let $M$ and $N$ be two closed modules and $M \twoheadrightarrow N$, $M$ is c-correct iff $N$ is c-correct.
\end{proposition}

\begin{proof}
One can define a function from left switched module onto right switched module
stable wrt acyclicity, connexity, and the inverse properties.\hfill $\qed$
\end{proof}

\begin{theorem}\label{c-correctness}
A \cm\ $M$ is c-correct iff $M\bigstep^*\testBotEbm$.
\end{theorem}

\begin{proof}
As the reduction rules are stable wrt correctness, it remains to prove that a correct non-terminal \cm\ $M$ can always be reduced.
We define a partial relation on negative poles: a negative pole is smaller than another one if there exists a positive pole st the first negative pole is linked to the bottom of the positive pole and the second negative pole is linked to the top of the positive pole. We consider the transitive closure of this relation.

If maximal negative poles do not exist then there exists at least one cycle in the module alternating positive and negative poles. We can then define a switching function on the module (choosing the correct links for negative poles) st the switched module has a cycle. Hence contradiction. 

So let us consider one of the maximal negative pole, and the corresponding positive pole. We remark that such a negative pole has no outcoming links (the module is closed and the negative pole is maximal). If the positive pole has other negative poles, we can omit the maximal negative pole by neutrality. Otherwise, let us study the incoming negative poles. 

If there is no such incoming link, then $M$ is the terminal module.
If each incoming negative pole has at least one link going to another positive pole, then one can define a switching function using for each of these negative poles one of the link that does not go to the positive pole we considered first. Hence the switched module is not connected (there are no outgoing links). Hence contradiction. So there exists at least one incoming negative pole with the whole set of links associated to the positive pole: the first rule applies and we are finished.\hfill $\qed$
\end{proof}
Mlp.bbl
\begin{thebibliography}{1}

\bibitem{Andreoli92}
Jean-Marc Andreoli.
\newblock Logic programming with focusing proofs in linear logic.
\newblock {\em Journal of Logic and Computation}, 2(3):297--347, 1992.

\bibitem{Andreoli01APAL}
Jean-Marc Andreoli.
\newblock Focussing and proof construction.
\newblock {\em Annals of Pure and Applied Logic}, 107(1--3):131--163, 2001.

\bibitem{Andreoli02CADE}
Jean-Marc Andreoli.
\newblock Focussing proof-net construction as a middleware paradigm.
\newblock In Andrei Voronkov, editor, {\em CADE}, volume 2392 of {\em Lecture
  Notes in Computer Science}, pages 501--516. Springer, 2002.

\bibitem{Andreoli03CSL}
Jean-Marc Andreoli and Laurent Mazar\'e.
\newblock Concurrent construction of proof-nets.
\newblock In Matthias Baaz and Johann~A. Makowsky, editors, {\em CSL}, volume
  2803 of {\em Lecture Notes in Computer Science}, pages 29--42. Springer,
  2003.

\bibitem{Danos_Regnier89}
Vincent Danos and Laurent Regnier.
\newblock The structure of multiplicatives.
\newblock {\em Archive for Mathematical Logic}, 28(3):181--203, 1989.

\bibitem{Girard87}
Jean-Yves Girard.
\newblock Linear logic.
\newblock {\em Theoretical Computer Science}, 50:1--102, 1987.

\bibitem{Murawski_Ong00}
Andrzej Murawski and Luke Ong.
\newblock Dominator trees and fast verification of proof nets.
\newblock In {\em LICS'00}, pages 181--191. IEEE Computer Society Press, 2000.

\end{thebibliography}
