AFII.tex

\documentclass[a4paper]{amsart}

\usepackage[lutzsyntax]{virginialake}\aftrianglefalse
\usepackage[urw-garamond]{mathdesign} % Comment this to use Times fonts
  \expandafter\ifx\csname leqslant\endcsname\relax\usepackage{txfonts}\fi
\usepackage[pdfborder={0 0 0}]{hyperref}
%\usepackage[dvipsnames,usenames]{color}
%\usepackage{draftwatermark}

%-------------------------------------------

\hyphenation{co-weak-en-ing}
\hyphenation{La-mar-che}
\hyphenation{quasi-poly-no-mial}

\renewcommand{\le}{\leqslant}
\renewcommand{\ge}{\geqslant}

%-------------------------------------------

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}

\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
%-------------------------------------------

%=========
\definecolor{darkgreen}{rgb}{0.0,0.4,0.0}
\definecolor{darkred}{rgb}{0.4,0.0,0.0}
\newif\ifnonotes\nonotesfalse
\newcommand{\Tom }[1]{\ifnonotes\else{\color{darkred}  \noindent{\bf T: }#1}\fi}
%=========


\begin{document}

\title[Normalisation Control in Deep Inference via Atomic Flows II]{Normalisation Control in Deep Inference \\ via Atomic Flows II}

\author{Alessio Guglielmi}
\address{University of Bath, Bath BA2 7AY, UK \and INRIA, Nancy-Grand Est, France}
\thanks{Guglielmi is supported by EPSRC grant EP/E042805/1 \emph{Complexity and Non-determinism in Deep Inference} and by an ANR \emph{Senior Chaire d'Excellence} titled \emph{Identity and Geometric Essence of Proofs}.}

\author{Tom Gundersen}
\address{University of Bath, Bath BA2 7AY, UK}
\thanks{Gundersen is supported by an \emph{Overseas Research Scholarship} and a \emph{Research Studentship} both of the University of Bath.}



%===============================================================================

\maketitle

%===============================================================================
\section{Introduction}

%TODO: say something clever at the start of the second sentence

We are interested in the normalisation of deep-inference derivations in propositional classical logic. Cuts are admissible from proofs and, dually, identities are admissible from refutations. However, neither are admissible from derivations. We therefore work with \emph{streamlining}, introduced in \cite{GuglGund:07:Normalis:lr}, a new, symmetric, notion of normalisation for derivations, which generalises both cut and identity elimination.

At the core of our work lie \emph{atomic flows}, which were introduced in \cite{GuglGund:07:Normalis:lr}. Atomic flows are graphs, similar to Buss flow graphs \cite{Buss:91:The-Unde:uq} and proof nets \cite{Gira:87:Linear-L:wm}, obtained from derivations by tracing their atom occurrences and forgetting everything except how atoms are created, copied, contracted and destroyed. Atomic flows are largely syntax independent and bureaucracy free (in the sense of Girard \cite{Gira:89:Geometry:sh}). We have shown how atomic flows are useful in defining new normal forms for derivations and in arguing about normalisation.

In particular, streamlining was defined based on atomic flows. Intuitively, a derivation is streamlined if every path in the associated atomic flow can be extended to reach the top or the bottom of the flow. Seen from the point of view of derivations it means; given an atom occurrence in a streamlined derivation, either all possible ways of tracing the atom upwards will reach the premiss or all possible ways of tracing the atom downwards will reach the conclusion. Since a proof has no atoms in its premiss (only the unit `true'), tracing atom occurrences upwards from a cut can not lead to the premiss. Hence, a streamlined proof is cut free.

In this paper, we present a new streamlining procedure. Similarly to our previous result the procedure is based on a particular way of gluing together pieces of derivation, which is possible due to the symmetries of deep inference. However, the novelty is that much less information about the atomic flow associated with the derivation is used to guide the procedure. In particular, we only need to know which identities are connected with which cuts. Since we use less information, all the identities and cuts we are eliminating are indistinguishable, so, unlike the previous procedures, no strategy for streamlining is necessary.

Contrary to what one might expect from cut elimination, the complexity of the procedure is not determined by the number of cuts being eliminated. The complexity is $O(2^n)$, where $n$ is the number of atoms which occur in at least one of the cuts we eliminate. In particular, every step of the procedure eliminate all the cuts where a given atom occurs, making termination a triviality.

We present our streamlining procedure as an operator, called the \emph{normaliser}. The normaliser can be thought of as a `shape' with holes. To streamline a derivation, it is inserted into the holes of the normaliser and the atoms of the derivation are associated with parts of the shape. We can observe that features of the shape are analogous to properties of a normalisation procedure. The fact that the shape is finite gives termination, its size givse the complexity, its asymmetries gives non-determinism, etc.

\newcommand{\SKS}{\mathsf{SKS}}
The results in this paper are presented in the deep-inference formalism the calculus of structures \cite{Gugl:06:A-System:kl}, in particular system $\SKS$ \cite{BrunTiu:01:A-Local-:mz,Brun:04:Deep-Inf:rq}, but we strive at generality and it should not be difficult to adapt our results to any deep-inference formalism and any propositional system as long as we have atomic structural rules and linear logical rules (something we always expect in deep inference and something which is not achievable elsewhere).

In the future, we believe it will be possible to improve on these results by extending them to modal \cite{Brun:07:Deep-Seq:fk,HeinStew:05:Purity-T:tg,StewStou:05:A-System:tg,Stou:06:A-Deep-I:rt} and first order \cite{Brun:04:Deep-Inf:rq,Brun:06:Cut-Elim:cq} logics and by making the procedure quasipolynomial, along the lines of a quasipolynomial cut-elimination procedure we are working on.

%===============================================================================
\section{Propositional Logic in Deep Inference}\label{SectDI}

\Tom{"For example" sounds wrong here. It is not examples of deep inference formalisms.}

In the range of the deep-inference methodology, we can define several formalisms, \emph{i.e.} general prescriptions on how to design proof systems. For example, the sequent calculus and natural deduction are formalisms in Gentzen-style proof theory, where the structure of proofs is determined by the tree structure of the formulae they prove.

The first, and conceptually simplest, formalism that has been defined in deep inference is called the \emph{calculus of structures}, or \emph{CoS} \cite{Gugl:06:A-System:kl}. CoS is now well developed for classical \cite{Brun:03:Atomic-C:oz,Brun:06:Cut-Elim:cq,Brun:06:Locality:zh,BrunTiu:01:A-Local-:mz,Brun:06:Deep-Inf:qy}, intuitionistic \cite{Tiu:06:A-Local-:gf}, linear \cite{Stra:02:A-Local-:ul,Stra:03:MELL-in-:oy}, modal \cite{Brun::Deep-Seq:ay,GoreTiu:06:Classica:uq,Stou:06:A-Deep-I:rt} and com\-mu\-ta\-tive/non-commutative logics \cite{Gugl:06:A-System:kl,Tiu:06:A-System:ai,Stra:03:Linear-L:lp,Brus:02:A-Purely:wd,Di-G:04:Structur:wy,GuglStra:01:Non-comm:rp,GuglStra:02:A-Non-co:lq,GuglStra:02:A-Non-co:dq,Kahr:06:Reducing:hc,Kahr:07:System-B:fk}.

\Tom{Say what the basics of SKS are and where it has been studied in respect to this paper.}
The standard proof system of propositional logic in CoS is called $\SKS$.
%The basic proof-complexity properties of $\SKS$, and, as a consequence, of propositional logic in CoS, have been studied in \cite{BrusGugl:07:On-the-P:fk}:
%\begin{itemize}
%%---------------------------------------
%\item $\SKS$ is polynomially equivalent to Frege proof systems.
%%---------------------------------------
%\item $\SKS$ can be extended with Tseitin's extension and substitution, and the proof systems so obtained are polynomially equivalent to Frege proof systems augmented by extension and substitution.
%%---------------------------------------
%\item Analytic $\SKS$ polynomially simulates analytic Gentzen proof systems, but the converse does not hold: in fact, Statman's tautologies admit polynomial proofs in analytic $\SKS$ but, as is well known, only exponential ones in analytic Gentzen \cite{Stat:78:Bounds-f:fj}.
%%---------------------------------------
%\end{itemize}

\Tom{Talk about `ways of composing derivations' instead of `certain derivations related to threshold formulae'}
In this paper, we work in CoS and $\SKS$, but we introduce a new notation for CoS. We do so to conveniently describe certain ways of composing derivations, which would seem very cumbersome otherwise (we mainly have in mind Definition~\ref{DefPathBreak}). In related work, we are defining a new formalism, currently dubbed \emph{Formalism A}, which generalises CoS and formally allows for the new notation.

In this section, we quickly introduce all the necessary notions. The standard reference for $\SKS$ in CoS and its typical constructions is \cite{Brun:04:Deep-Inf:rq}.

\newcommand{\fff}{\mathsf f}
\newcommand{\ttt}{\mathsf t}
\emph{Formulae}, denoted by $\alpha$, $\beta$, $\gamma$ and $\delta$ are freely built from: \emph{units}, $\fff$ (false), $\ttt$ (true); \emph{atoms}, denoted by $a$, $b$, $c$, $d$ and $e$; \emph{disjunction} and \emph{conjunction}, ${\vlsbr[\alpha.\beta]}$ and $\vlsbr(\alpha.\beta)$. The different brackets have the only purpose of improving legibility; we usually omit external brackets of formulae, and sometimes we omit superfluous brackets under associativity. On the set of atoms a (non-identical) involution $\bar\cdot$ is defined and called \emph{negation}; $a$ and $\bar a$ are \emph{dual} atoms. We denote \emph{contexts}, \emph{i.e.}, formulae with a hole, by $\xi\vlhole$ and $\zeta\vlhole$; for example, if $\xi\vlscn[a]$ is $\vls(b.[a.c])$, then $\xi\vlhole$ is $\vls(b.[\vlhole.c])$, $\xi\{b\}$ is $\vls(b.[b.c])$ and $\xi\vlscn(a.d)$ is $\vls(b.[(a.d).c])$.

Note that negation is only defined for atoms, and this is not a limitation because, thanks to De Morgan laws, negation can always be `pushed to' atoms. Also, note that there are no negative or positive atoms in an absolute sense; we can only say that if we arbitrarily consider $\bar a$ positive, then $a$ must be negative, for example.

A CoS (\emph{inference}) \emph{rule} $\rho$ is an expression $\vlinf\rho{}\beta\alpha$, where the formulae $\alpha$ and $\beta$ are called \emph{premiss} and \emph{conclusion}, respectively; an inference rule \emph{instance} $\vlupsmash{\vlinf\rho{}\delta\gamma}$, where $\gamma$ and $\delta$ are instances of $\alpha$ and $\beta$, respectively, generates an (\emph{inference}) \emph{step} $\vlinf\rho{}{\xi\vlscn[\delta]}{\xi\vlscn[\gamma]}$, for each context $\xi\vlhole$. A \emph{derivation}, $\Phi$, \emph{from} $\alpha$ (\emph{premiss}) \emph{to} $\beta$ (\emph{conclusion}) is a chain of inference steps with $\alpha$ at the top and $\beta$ at the bottom, and is usually indicated by $\vlder\Phi{\mathcal S}{\beta}{\alpha}$, where $\mathcal S$ is the name of the proof system or a set of inference rules (we might omit $\Phi$ and $\mathcal S$); a \emph{proof} is a derivation with premiss $\ttt$ and a \emph{refutation} is a derivation with conclusion $\fff$; besides $\Phi$, we denote derivations with $\Psi$.

\newcommand{\ai  }{\mathsf{ai}}
\newcommand{\aw  }{\mathsf{aw}}
\newcommand{\ac  }{\mathsf{ac}}
\newcommand{\aid }{{\ai{\downarrow}}}
\newcommand{\awd }{{\aw{\downarrow}}}
\newcommand{\acd }{{\ac{\downarrow}}}
\newcommand{\aiu }{{\ai{\uparrow}}}
\newcommand{\awu }{{\aw{\uparrow}}}
\newcommand{\acu }{{\ac{\uparrow}}}
\newcommand{\swi }{\mathsf{s}}
\newcommand{\med }{\mathsf{m}}
\emph{System\/ $\SKS$} is a CoS proof system, defined by the following \emph{structural} inference rules:
\[
\begin{array}{@{}c@{}c@{}c@{}}
      \vlinf\aid{}{\vls[a.{\bar a}]}\ttt&
\qquad\vlinf\awd{}a\fff                 &
\qquad\vlinf\acd{}a{\vls[a.a]}          \\
\noalign{\smallskip}
      \emph{identity}                   &
\qquad\emph{weakening}                  &
\qquad\emph{contraction}                \\
\noalign{\bigskip}
      \vlinf\aiu{}\fff{\vls(a.{\bar a})}&
\qquad\vlinf\awu{}\ttt a                &
\qquad\vlinf\acu{}{\vls (a.a)}a         \\
\noalign{\smallskip}
      \emph{cut}&
\qquad\emph{coweakening}&
\qquad\emph{cocontraction}\\
\end{array}
\quad,
\]
and by the following two \emph{logical} inference rules:
\[
\begin{array}{@{}c@{}c@{}}
\vlinf\swi{}{\vls[(\alpha.\beta).\gamma]}{\vls(\alpha.[\beta.\gamma])}&\qquad
\vlinf\med{}{\vls([\alpha.\gamma].[\beta.\delta])}
            {\vls[(\alpha.\beta).(\gamma.\delta)]}                    \\
\noalign{\smallskip}
\emph{switch}                                                         &\qquad
\emph{medial}                                                         \\
\end{array}
\quad.
\]
In addition to these rules, there is a rule $\vlsmash{\vlinf={}\delta\gamma}$, such that $\gamma$ and $\delta$ are opposite sides in one of the following equations:
\begin{equation}
\begin{array}{@{}r@{}l@{}r@{}l@{}}
\vls[\alpha.\beta]         &{}=\vls[\beta.\alpha]         &\qquad\qquad
\vls[\alpha.\fff]          &{}=\vls[\alpha]               \\
\noalign{\smallskip}
\vls(\alpha.\beta)         &{}=\vls(\beta.\alpha)         &\qquad\qquad
\vls(\alpha.\ttt)          &{}=\vls(\alpha)               \\
\noalign{\smallskip}
\vls[[\alpha.\beta].\gamma]&{}=\vls[\alpha.[\beta.\gamma]]&\qquad\qquad
\vls[\ttt.\ttt]            &{}=\vls[\ttt]                 \\
\noalign{\smallskip}
\vls((\alpha.\beta).\gamma)&{}=\vls(\alpha.(\beta.\gamma))&\qquad\qquad
\vls(\fff.\fff)            &{}=\vls(\fff)                 
\end{array}
\quad.
\end{equation}
We do not always show the instances of rule $=$, and when we do show them, we gather several contiguous instances into one. We consider the $=$ rule as implicitly present in all systems. The first row in Figure~\ref{FigExAF} shows some $\SKS$ example derivations.


\Tom{Removed all talk of SKSg, but define contraction up and down later on in a remark}
%\newcommand  {\SKSg}{\mathsf{SKSg}}
%Besides $\SKS$, another standard deep-inference system is $\SKSg$, which is the same as $\SKS$, except that it does not contain medial and its structural rules are not restricted to atoms. In particular, we use in this paper the rules
%\[
%\vlinf\cod{}\alpha{\vls[\alpha.\alpha]}
%\qquad\text{and}\qquad
%\vlinf\cou{}{\vls(\alpha.\alpha)}\alpha
%\quad.
%\]
%Clearly, a derivation in $\SKS$ is also a derivation in $\SKSg$. It can easily be proved that $\SKS$ and all its fragments containing the logical and $=$ rules polynomially simulate, respectively, $\SKSg$ and its corresponding fragments \cite{BrusGugl:07:On-the-P:fk}. For example, $\{\swi,\med,=,\acd\}$ polynomially simulates $\{\swi,=,\cod\}$.

%We can replace instances of nonatomic structural rules by derivations with the same premiss and conclusion, and that only contain atomic structural rules. The price to pay is a quadratic growth in size. An example is the rightmost upper derivation in Figure~\ref{FigExAF}, which stands for a nonatomic cocontraction.

%Sometimes, we use a nonatomic rule instance to stand for some derivation in $\SKS$ that derives that instance, as per Remark~\ref{RemGenericContraction}.

For CoS proofs, we adopt a special notation that allows us considerable efficiency in describing derivations, especially in the crucial Definition~\ref{DefPathBreak}. We denote with $\xi\vlscn[\Phi]$ the result of including every formula of $\Phi$ into the context $\xi\vlhole$: since we adopt deep inference, $\xi\vlscn[\Phi]$ is a valid derivation. Then, given the two derivations $\vldownsmash{\vlder\Phi{}\beta\alpha}$ and $\vldownsmash{\vlder\Psi{}\delta\gamma}$, by $\vls[\Phi.\Psi]$ and $\vls(\Phi.\Psi)$ we denote, respectively,
\[
\vlinf={}{\vlsbr[\beta\;\;.\;\;\vlder\Psi{}\delta\gamma]}
         {\vlsbr[\vlder\Phi{}\beta\alpha\;\;.\;\;\gamma]}
\qquad\text{and}\qquad
\vlinf={}{\vlsbr(\beta\;\;.\;\;\vlder\Psi{}\delta\gamma)}
         {\vlsbr(\vlder\Phi{}\beta\alpha\;\;.\;\;\gamma)}
\quad,
\]
or any other CoS derivations obtained by interleaving $\Phi$ and $\Psi$ and respecting the specified logical relations between $\Phi$ and $\Psi$. We call this the \emph{Formalism A} notation. Examples of Formalism A derivations are in the second row of Figure~\ref {FigExAF}, in correspondence with CoS derivations in the first row. Note that we omit structural rule names in Formalism A notation (since they are easily inferable, this improves legibility). Because of its convenience, the Formalism A notation is currently being developed as a full-fledged deep-inference formalism.

%===============================================================================
\section{Atomic Flows}\label{SectAF}

\Tom{Changed last two sentences... Need to rewrite the last one}
Atomic flows, which have been introduced in \cite{GuglGund:07:Normalis:lr}, are, essentially, specialised Buss flow graphs \cite{Buss:91:The-Unde:uq}. They are particular directed graphs associated with $\SKS$ derivations: every derivation yields one atomic flow obtained by tracing the atom occurrences inside the derivation. Infinitely many derivations correspond to each atomic flow; this suggests that much of the information inside a derivation is lost in its associated atomic flow; in particular, there is no information about instances of logical rules, only structural rules play a role. As shown in \cite{GuglGund:07:Normalis:lr}, it turns out that atomic flows contain sufficient structure to control normalisation procedures, providing in particular induction measures that can be used to ensure termination. Such normalisation procedures \Tom{state a problem about the old stuff}. In the present work we show a strongly normalising procedure and we greatly restrict the non-confluency. As in our previous work all the necessary information to perform normalisation is contained in the atomic flows. Furthermore, we now use much less of the available information compared to before.

We can single out three features of atomic flows that, in general, and not just in this work, help in designing normalisation procedures:

\Tom{Changed the second item completely (need to rewrite), talk about cut free proofs instead of analytic proofs.}
\begin{enumerate}
%---------------------------------------
\item\label{ItemUseTop} Atomic flows conveniently express the topological structure of atom occurrences in a proof. This is especially useful for defining the `core' of derivations, in Definitions~\ref{DefDerCore} and \ref{DefFlowCore}.
%---------------------------------------
\item\label{ItemUseUnique} Atomic flows forget much bureaucracy, so whereas it is near to impossible to define procedures which give us unique derivations, without making arbitrary choices, the atomic flows of the derivations are often unique. \Tom{refer to the places where we say that atomic flows are unique modulo associativity of contraction}.
%---------------------------------------
\item\label{ItemUseNorm} We can define graph rewriting systems over atomic flows that control normalisation procedures on derivations. This could be used for obtaining cut-free proofs, as we do in Theorem~\ref{TODO}. 
\end{enumerate}
Our aim now is to quickly and informally provide the necessary notions about atomic flows, especially concerning aspects \eqref{ItemUseTop} and \eqref{ItemUseUnique} above. Although the feature \eqref{ItemUseNorm} of atomic flows did help us in obtaining cut-free proofs, we estimate that formally introducing the necessary machinery is unjustified in this paper. In fact, given our limited needs here, we can operate directly on derivations, without the intermediate support of atomic flows. Nonetheless, being aware of the underlying atomic-flow methods is useful for the reader who wishes to further investigate this matter. So, we informally provide, in Section~\ref{TODO}, enough material to make the connection with the atomic-flow techniques that are fully developed in \cite{GuglGund:07:Normalis:lr}.

We obtain one atomic flow from each derivation by tracing all its atom occurrences and by keeping track of their creation and destruction (in identity/cut and weakening/coweakening instances), their duplication (in contraction/cocontraction instances) and their duality (in identity/cut instances). Technically, atomic flows are directed graphs of a special kind, but it is more intuitive to consider them as diagrams generated by composing \emph{elementary atomic flows} that belong to one of seven kinds.

The first kind of elementary atomic flow is the \emph{edge}
\[
\atomicflow{
(0,0)*{\afvj4{}{}{}{}}}\quad,
\]
which corresponds to one or more occurrences of the same atom in a given derivation, all of which are not active in any structural rule instance, \emph{i.e.}, they are not the atom occurrences that instantiate a structural rule.

The other six kinds of elementary diagrams are associated with the six structural inference rules, as shown in Figure~\ref{FigVertAF}, and they are called \emph{vertices}; each vertex has some incident edges. At the left of each arrow, we see an instance of a structural rule, where the atom occurrences are labelled by small numerals; at the right of the arrow, we see the vertex corresponding to the rule instance, whose incident edges are labelled in accord with the atom occurrences they correspond to. We qualify each vertex according to the rule it corresponds to; for example, in a given atomic flow, we might talk about a \emph{contraction vertex}, or a \emph{cut vertex}, and so on. Instead of small numerals, sometimes we use $\epsilon$ or $\iota$ or colour to label edges (as well as atom occurrences), but we do not always use labels.

\newcommand{\one  }{{\mathchoice{\scriptstyle      \mathbf1}
                                {\scriptstyle      \mathbf1}
                                {\scriptstyle      \mathbf1}
                                {\scriptscriptstyle\mathbf1}}}
\newcommand{\two  }{{\mathchoice{\scriptstyle      \mathbf2}
                                {\scriptstyle      \mathbf2}
                                {\scriptstyle      \mathbf2}
                                {\scriptscriptstyle\mathbf2}}}
\newcommand{\three}{{\mathchoice{\scriptstyle      \mathbf3}
                                {\scriptstyle      \mathbf3}
                                {\scriptstyle      \mathbf3}
                                {\scriptscriptstyle\mathbf3}}}
\newcommand{\four }{{\mathchoice{\scriptstyle      \mathbf4}
                                {\scriptstyle      \mathbf4}
                                {\scriptstyle      \mathbf4}
                                {\scriptscriptstyle\mathbf4}}}
\newcommand{\five }{{\mathchoice{\scriptstyle      \mathbf5}
                                {\scriptstyle      \mathbf5}
                                {\scriptstyle      \mathbf5}
                                {\scriptscriptstyle\mathbf5}}}
%-------------------------------------------------------------------------------
\begin{figure}
\[
\begin{array}{@{}c@{}c@{}c@{}c@{}c@{}c@{}}
\vlinf\aid{}{\vls[a^\one.\bar a^\two]}\ttt&\quad{\to}\quad
	\atomicflow{(0,0)*{\afaid\one{}{}\two{}{}}}&\qquad\qquad
\vlinf\awd{}{a^\one}\fff&\quad{\to}\quad
	\atomicflow{(0,0)*{\afawd{}{}{}\one}}&\qquad\qquad
\vlinf\acd{}{a^\three}{\vls[a^\one.a^\two]}&\quad{\to}\quad
	\atomicflow{(0,0)*{\afacd\one{}{}\two{}\three}}
\\
\noalign{\bigskip}
\vlinf\aiu{}\fff{\vls(a^\one.\bar a^\two)}&\quad{\to}\quad
	\atomicflow{(0,0)*{\afaiu\one{}{}\two{}{}}}&\qquad\qquad
\vlinf\awu{}\ttt{a^\one}&\quad{\to}\quad
	\atomicflow{(0,0)*{\afawu{}{}{}\one}}&\qquad\qquad
\vlinf\acu{}{\vls(a^\one.a^\two)}{a^\three}&\quad{\to}\quad
	\atomicflow{(0,0)*{\afacu\one{}{}\two{}\three}}\\
\end{array}
\]
\caption{Vertices of atomic flows.}
\label{FigVertAF}
\end{figure}

All edges are directed, but we do not explicitly show the orientation. Instead, we consider it as implicitly given by the way we draw them, namely, edges are oriented along the vertical direction. So, the vertices corresponding to dual rules, in Figure~\ref{FigVertAF}, are distinct, for example, an identity vertex and a cut vertex are different because the orientation of their edges is different. On the other hand, the horizontal direction plays no role in distinguishing atomic flows; this corresponds to commutativity of logical relations.

\newcommand{\ppl}{{\mathchoice{\scriptstyle+}
                              {\scriptstyle+}
                              {\scriptstyle+}
                              {\scriptscriptstyle+}}}
\newcommand{\pmi}{{\mathchoice{\scriptstyle-}
                              {\scriptstyle-}
                              {\scriptstyle-}
                              {\scriptscriptstyle-}}}
We can define (\emph{atomic}) \emph{flows} as the smallest set of diagrams containing elementary atomic flows, and closed under the composition operation consisting in identifying zero or more edges such that no cycle is created. In addition, for a diagram to be an atomic flow, it must be possible to assign it a polarity, according to the following definition. A \emph{polarity assignment} is a mapping of each edge to an element of $\{\pmi,\ppl\}$, such that the two edges of each identity or cut vertex map to different values and the three edges of each contraction or cocontraction vertex map to the same value. We denote atomic flows by $\phi$ and $\psi$. An edge $\epsilon$ is an \emph{upper (resp., lower) edge} of the vertex $\nu$ if $\epsilon$ is above (resp., below) and incident to $\nu$. An edge $\epsilon$ in the atomic flow $\phi$ is an upper (resp., lower) edge of $\phi$ if there is no vertex $\nu$ in $\phi$ such that $\epsilon$ is a lower (resp., upper) edge of $\nu$.

\Tom{Defined upper/lower edges in last sentence.}

Let us see some examples. The flow
\begin{equation}\label{ExFlow}
\atomicflow{
(17,12)*{\afaid{}{}{}{}{}{}};
(-3, 8)*{\afvjd8{}{}};
(-1, 8)*{\afvjd8{}{}};
( 1, 8)*{\afvjd8{}{}};
( 4, 8)*{\afvjd8{}{}};
(10, 8)*{\afacu{}{}{}{}{}{}};
(17, 4)*{\afaiu{}{}{}{}{}{}};
( 6, 2)*{\afaiunw{}{}}}
\end{equation}
is obtained by juxtaposing (\emph{i.e.}, composing by identifying zero edges):
\begin{itemize}
\item three edges, 
\item a flow obtained by composing a cut vertex with a cocontraction vertex, and
\item a flow obtained by composing an identity vertex with a cut vertex.
\end{itemize}
Note that there are no cycles in the flow, and that we can find 32 different polarity assignments, \emph{i.e.}, two for each of the five connected components of the flow (this is a general rule).

Let us see another example. These are three different representations of the same flow:
\[
\atomicflow{
(10,8)*{\afacu\four{}{}{}{}\two};
( 0,8)*{\afvjd8\one{}};
( 4,8)*{\afvjd8{}\five};
( 6,2)*{\afaiunw{}{}};
( 6,0)*{\afaiuex{}{}{}\three{}{}31}}
\quad,\qquad
\atomicflow{
( 0,6)*{\afvjd{8}\one\ppl};
( 6,6)*{\afacu\three{}{}\four\two\pmi};
(12,6)*{\afvjd{8}\ppl\five};
(10,0)*{\afaiunw{}{}};
( 2,0)*{\afaiunw{}{}}}
\qquad\text{and}\qquad
\atomicflow{
( 8,10)*{\afacu{}\three{}\four\two\ppl};
( 0, 8)*{\afvjd{12}\one\pmi};
( 4,10)*{\afvjd{8}\five\pmi};
( 5, 4)*{\afex24};
(10, 4)*{\afvj4};
( 2, 0)*{\afaiunw{}{}};
( 8, 0)*{\afaiunw{}{}}}
\quad,
\]
where we label edges to show their correspondence. In the two rightmost flows, we indicate the two different polarity assignments that are possible.

The following two diagrams are not atomic flows:
\[
\atomicflow{
(4,11.7)*{\afacu{}{}{}{}{}{}};
(0, 3.7)*{\afacd{}{}{}{}{}{}};
(8, 7.7)*{\afvj{16}};
(4,16);(8,16)**[|<\atflowthickone>]\crv{(4,18)&(6,20)&(8,18)};
(0,0);(8,0)**[|<\atflowthickone>]\crv{(0,-2)&(4,-4)&(8,-2)}}
\qquad\text{and}\qquad
\atomicflow{
(0,4)*{\afaidnw{}{}};
(0,0)*{\afacd{}{}{}{}{}{}}}
\quad.
\]
The left one is not a flow because it contains a cycle, and the right one because there is no possible polarity assignment.

\Tom{The definition of path is correct, but not complete. It does however include all the paths we care about in this paper. We would also need to add that $\epsilon_1$, $\dots$, $\epsilon_n$ is a path from $\nu_n$ to $\nu_0$ and from $\epsilon_n$ to $\epsilon_0$ for the definition to coincide with Atomic Flows 1.}

Given two vertices $\nu_0$ and $\nu_n$ in an atomic flow $\phi$, a sequence of edges $\epsilon_1,\dots,\epsilon_n$ in $\phi$ is a \emph{path from $\nu_0$ to $\nu_n$ in $\phi$} or a \emph{path from $\epsilon_1$ to $\epsilon_n$ in $\phi$} if there exist vertices $\nu_1,\dots,\nu_{n-1}$ in $\phi$ such that, for every $1\le i\le n$, $\epsilon_i$ is a lower edge of $\nu_{i-1}$ and an upper edge of $\nu_i$. A path $\epsilon_1,\dots,\epsilon_n$ is a \emph{maximal path in $\phi$} if there is no edge $\epsilon$ in $\phi$ such that $\epsilon_1,\dots,\epsilon_n,\epsilon$ or $\epsilon,\epsilon_1,\dots,\epsilon_n$ is a path in $\phi$.

Let us see how to extract atomic flows from derivations. Given an $\SKS$ derivation $\Phi$, we obtain, by the following prescriptions, a unique atomic flow $\phi$, such that there is a surjective map between atom occurrences in $\Phi$ and edges of $\phi$:
\begin{itemize}
%-------------------
\item Each structural inference step in $\Phi$ is associated with one and only one vertex in $\phi$, such that active atom occurrences in the rule instance map to edges incident with the vertex. The correspondence is indicated in Figure~\ref{FigVertAF}. For example, the flow associated with the inference step at the left is indicated at the right:
\[
\vlinf\acd
      {}
      {\vls(a^\one.[b^\two.a^\five])}
      {\vls(a^\one.[b^\two.[a^\three.a^\four]])}
\qquad\text{and}\qquad
\vcenter{\hbox{$\atomicflow{
( 0,0)*{\afvjd8\one{}};
( 4,0)*{\afvjd8\two{}};
(10,0)*{\afacd\three{}{}\four{}\five}}$}}
\quad.
\]
Note that the nonactive atoms are `traced' by associating each trace with one edge; this corresponds well to abbreviating, say, the inference step $\vldownsmash{\vlinf\acd{}{\xi\vlscn[a]}{\xi\vlscn[a.a]}}$ by $\xi\left\{\vlinf{}{}a{\vls[a.a]}\right\}$.
%-------------------
\item For each other inference step in $\Phi$, all the atom occurrences in the premiss are respectively mapped to the same edges of $\phi$ as the atom occurrences in the conclusion. For example, the flow associated with the inference step
\[
\vlinf\med
      {}
      {\vls(a^\one.([b^\two.d^\four]).([c^\three.e^\five]))}
      {\vls(a^\one.[(b^\two.c^\three).(d^\four.e^\five)])}
\qquad\text{is}\qquad
\atomicflow{
( 0,0)*{\afvjd8\one{}};
( 4,0)*{\afvjd8\two{}};
( 8,0)*{\afvjd8\three{}};
(12,0)*{\afvjd8\four{}};
(16,0)*{\afvjd8\five{}}}
\quad.
\]
\end{itemize}
The flow $\phi$ so obtained is called the atomic flow \emph{associated with} the derivation $\Phi$. We show three examples in Figure~\ref{FigExAF}: in the top row we see three $\SKS$ derivations in the standard CoS syntax; in the row below, we show the same derivations in the Formalism A notation; in the bottom row, we see the three corresponding atomic flows.

\newcommand{\RD}[1]{{\color{Red}#1}}
\newcommand{\GR}[1]{{\color{Green}#1}}
\newcommand{\DO}[1]{{\color{DarkOrchid}#1}}
\newcommand{\PB}[1]{{\color{ProcessBlue}#1}}
\newcommand{\MG}[1]{{\color{Magenta}#1}}
\newcommand{\SG}[1]{{\color{SpringGreen}#1}}
\newcommand{\RS}[1]{{\color{RawSienna}#1}}
\newcommand{\YO}[1]{{\color{YellowOrange}#1}}
\newcommand{\PW}[1]{{\color{Periwinkle}#1}}
%-------------------------------------------------------------------------------
\begin{figure}
\[
%---------------------------------------
\begin{array}{@{}c@{}c@{}c@{}}
\vlderivation                                                {
\vlin=   {}{\ttt                                  }         {
\vlin\aiu{}{\vls[\fff.\ttt]                       }        {
\vlin=   {}{\vls[(\GR{a}.\RD{\bar a}).\ttt]       }       {
\vlin\swi{}{\vls[[(\RD{\bar a}.\GR{a}).\ttt].\ttt]}      {
\vlin=   {}{\vls[(\RD{\bar a}.[\GR{a}.\ttt]).\ttt]}     {
\vlin\swi{}{\vls[([\GR{a}.\ttt].\RD{\bar a}).\ttt]}    {
\vlin=   {}{\vls([\GR{a}.\ttt].[\RD{\bar a}.\ttt])}   {
\vlin\med{}{\vls([\GR{a}.\ttt].[\ttt.\RD{\bar a}])}  {
\vlin=   {}{\vls[(\GR{a}.\ttt).(\ttt.\RD{\bar a})]} {
\vlin\aid{}{\vls[\GR{a}.\RD{\bar a}]              }{
\vlhy      {\ttt                                  }}}}}}}}}}}}
\qquad&
%-------------------
\vlderivation                                                              {
\vlin\aiu{}
   {\vls(\DO{a}.\fff)                                            }        {
\vlin=   {}
   {\vls(\DO{a}.(\PB{a}.\MG{\bar a}))                            }       {
\vlin\acu{}
   {\vls((\DO{a}.\PB{a}).\MG{\bar a})                            }      {
\vlin=   {}
   {\vls(\SG{a}.\MG{\bar a})                                     }     {
\vlin\aiu{}
   {\vls([\fff.\SG{a}].\MG{\bar a})                              }    {
\vlin\acd{}
   {\vls([(\RD{a}.\RS{\bar a}).\SG{a}].\MG{\bar a})              }   {
\vlin\swi{}
   {\vls([(\RD{a}.[\GR{\bar a}.\YO{\bar a}]).\SG{a}].\MG{\bar a})}  {
\vlin=   {}
   {\vls((\RD{a}.[[\GR{\bar a}.\YO{\bar a}].\SG{a}]).\MG{\bar a})} {
\vlin\aid{}
   {\vls((\RD{a}.[\GR{\bar a}.[\YO{\bar a}.\SG{a}]]).\MG{\bar a})}{
\vlhy        
   {\vls((\RD{a}.[\GR{\bar a}.\ttt]).\MG{\bar a})                }}}}}}}}}}}
\qquad&
%-------------------
\vlderivation                                                            {
\vlin=   {}{\vls(([\RS{a}.\YO{b}].\PW{a}).([\GR{a}.\DO{b}].\SG{a}))}    {
\vlin\med{}{\vls(([\RS{a}.\YO{b}].[\GR{a}.\DO{b}]).(\PW{a}.\SG{a}))}   {
\vlin\acu{}{\vls([(\RS{a}.\GR{a}).(\YO{b}.\DO{b})].(\PW{a}.\SG{a}))}  {
\vlin\acu{}{\vls([(\RS{a}.\GR{a}).(\YO{b}.\DO{b})].\MG{a})         } {
\vlin\acu{}{\vls([(\RS{a}.\GR{a}).\PB{b}].\MG{a})                  }{
\vlhy      {\vls([\RD{a}.\PB{b}].\MG{a})                           }}}}}}}
\\
\noalign{\bigskip}
%---------------------------------------
\vlderivation                                                      {
\vlin\swi{}{\vlsbr[\vlinf{\swi}
                         {}
                         {\vlsbr[\vlinf{}
                                     {}
                                     {\fff}
                                     {\vls(\GR{a}.\RD{\bar a})}
                              \;.\;
                              \ttt]}
                         {\vls([\GR{a}.\ttt].\RD{\bar a})}
                  \;\;.\;\;
                   \ttt
                  ]                                            }  {
\vlin\med{}{\vls([\GR{a}.\ttt].[\ttt.\RD{\bar a}])             } {
\vlin{}  {}{\vls[\GR{a}.\RD{\bar a}]                           }{
\vlhy      {\ttt                                               }}}}}
\qquad&
%-------------------
\vlinf=
      {}
      {\vlsbr(\DO{a}\;.\;\vlinf{}{}\fff{\vls(\PB{a}.\MG{\bar a})})}      
      {\vlsbr(\vlinf\swi
                    {}
                    {\vlsbr[\vlinf{}
                                {}
                                \fff
                                {\vlsbr(\RD{a}
                                     \;.\;\vlinf{}
                                            {}
                                            {\RS{\bar a}}
                                            {\vls[\GR{\bar a}.\YO{\bar a}]}
                                     )}
                         \;\;.\;\;
                         \vlinf{}{}{\vls(\DO{a}.\PB{a})}{\SG{a}}
                         ]}
                    {\vlsbr(\RD{a}
                         \;.\;[\GR{\bar a}
                          \;.\;\vlinf{}
                                 {}
                                 {\vls[\YO{\bar a}.\SG{a}]}
                                 \ttt
                          ]
                         )}
            \;\;\;.\;\;\;
            \MG{\bar a}
            )}
\qquad&
%-------------------
\vls(\vlinf\med
           {}
           {\vls([\RS{a}.\YO{b}].[\GR{a}.\DO{b}])}
           {\vlsbr[\vlinf{}{}{\vls(\RS{a}.\GR{a})}{\RD{a}}
                \;.\;{\vlinf{}{}{\vls(\YO{b}.\DO{b})}{\PB{b}}}
                ]}
    \;\;.\;\;
     \vlinf{}{}{\vls(\PW{a}.\SG{a})}{\MG{a}}
    )
\\
\noalign{\bigskip}
%---------------------------------------
\atomicflow{
(0,0)*{\afaiucol{}{}{}{}{}{}{Green}{Red}{}};
(0,4)*{\afaidnw{}{}}}
\qquad&
%-------------------
\atomicflow{
( 2,14)*{\afvjcol4{Green}};
( 0,10)*{\afvjcol{12}{Red}};
(16,10)*{\afvjcol{12}{Magenta}};
( 4, 8)*{\afacdcol{}{}{}{}{}{}{Green}{YellowOrange}{RawSienna}};
(10, 8)*{\afacucol{}{}{}{}{}{}{DarkOrchid}{ProcessBlue}{SpringGreen}};
( 2, 2)*{\afaiunw{}{}};
( 8, 2)*{\afvjcol4{DarkOrchid}};
(14, 2)*{\afaiunw{}{}};
( 8,12)*{\afaidnw{}{}}}
\qquad&
%-------------------
\atomicflow{
( 0,0)*{\afacucol{}{}{}{}{}{}{RawSienna}{Green}{Red}};
( 6,0)*{\afacucol{}{}{}{}{}{}{YellowOrange}{DarkOrchid}{ProcessBlue}};
(12,0)*{\afacucol{}{}{}{}{}{}{Periwinkle}{SpringGreen}{Magenta}}}
\end{array}
\]
\caption{Examples of derivations in CoS and Formalism A notation, and associated atomic flows.}
\label{FigExAF}
\end{figure}

Perhaps surprisingly, it can be proved that every flow is associated with infinitely many $\SKS$ derivations (see \cite{GuglGund:07:Normalis:lr}).

We introduce now some graphical shortcuts. When certain details of a flow are not important, but only the vertex kinds and its upper and lower edges are, we can use boxes, labelled with all the vertex kinds that can appear in the flow they represent. For example, the following left and centre flows could represent the previously seen flow~\eqref{ExFlow}, whereas the right flow cannot:
\newbox\contrup\setbox\contrup=\hbox{$
   \divide\atflowunit by6\multiply\atflowunit by3\afsetunits
   \atomicflow{(0,0)*{\afacu{}{}{}{}{}{}}}$}
\newbox\contrdown\setbox\contrdown=\hbox{$
   \divide\atflowunit by6\multiply\atflowunit by3\afsetunits
   \atomicflow{(0,0)*{\afacd{}{}{}{}{}{}}}$}
\newbox\interdown\setbox\interdown=\hbox{$
   \divide\atflowunit by6\multiply\atflowunit by3\afsetunits
   \atomicflow{(0,0)*{\afaid{}{}{}{}{}{}}}$}
\newbox\interup\setbox\interup=\hbox{$
   \divide\atflowunit by6\multiply\atflowunit by3\afsetunits
   \atomicflow{(0,0)*{\afaiu{}{}{}{}{}{}}}$}
\newbox\weakdown\setbox\weakdown=\hbox{$
   \divide\atflowunit by6\multiply\atflowunit by3\afsetunits
   \atomicflow{(0,0)*{\afawd{}{}{}{}{}{}}}$}
\newbox\weakup\setbox\weakup=\hbox{$
   \divide\atflowunit by6\multiply\atflowunit by3\afsetunits
   \atomicflow{(0,0)*{\afawu{}{}{}{}{}{}}}$}
\[
%---------------------------------------
\atomicflow{
( 1   ,12)*{\afvj4};
( 3.75,12)*{\afvj4};
( 6.5 ,12)*{\afvj4};
( 9.25,12)*{\afvj4};
(12   ,12)*{\afvj4};
(11   , 9)*{\aflabelright\phi};
( 2   , 6)*{\copy\interdown};
( 6   , 6)*{\copy\interup};
( 6.5 , 6)*{\affr{13}8};
(10   , 6)*{\copy\contrup};
( 1   , 0)*{\afvj4};
( 4.67, 0)*{\afvj4};
( 8.33, 0)*{\afvj4};
(12   , 0)*{\afvj4}}
\quad,\qquad
%---------------------------------------
\atomicflow{
(11  ,14  )*{\afaid{}{}{}{}{}{}};
(-3  ,12.5)*{\afvj5};
(-1  ,12.5)*{\afvj5};
( 3  ,12.5)*{\afvj5};
( 5  ,12.5)*{\afvj5};
( 7  ,12.5)*{\afvj5};
(-2  , 9  )*{\aflabelright\psi};
( 7.5, 9  )*{\aflabelright{\psi'}};
(-2  , 6  )*{\affr48};
(-2  , 6  )*{\copy\weakdown};
( 6  , 6  )*{\affr88};
( 4  , 6  )*{\copy\interup};
( 7  , 6  )*{\copy\contrup};
(13  , 6  )*{\afvj8};
(11  ,-2  )*{\afaiu{}{}{}{}{}{}};
(-3  ,-0.5)*{\afvj5};
(-1  ,-0.5)*{\afvj5};
( 3  ,-0.5)*{\afvj5};
( 6  ,-0.5)*{\afvj5}}
\qquad\text{and}\qquad
%---------------------------------------
\atomicflow{
(11,14  )*{\afaid{}{}{}{}{}{}};
(-3,12.5)*{\afvj5};
(-1,12.5)*{\afvj5};
( 3,12.5)*{\afvj5};
( 5,12.5)*{\afvj5};
( 7,12.5)*{\afvj5};
(-2, 6  )*{\affr48};
(-2, 6  )*{\copy\weakdown};
( 4, 6  )*{\copy\contrdown};
( 6, 6  )*{\affr88};
( 7, 6  )*{\copy\contrup};
(13, 6  )*{\afvj8};
(11,-2  )*{\afaiu{}{}{}{}{}{}};
(-3,-0.5)*{\afvj5};
(-1,-0.5)*{\afvj5};
( 5,-0.5)*{\afvj5}}
\quad.
\]
The flow at the right cannot represent flow~\eqref{ExFlow} because it has the wrong number of lower edges and because a necessary cut vertex is not allowed by the labelling of the boxes. As just shown, we sometimes label boxes with the name of the flow they represent. For example, flow $\phi$ above could represent flow~\eqref{ExFlow}, and, if the centre flow stands for \eqref{ExFlow}, then flows $\psi$ and $\psi'$ are, respectively,
\[
\atomicflow{
(0,7.5)*{\afvjd9{}{}};
(2,7.5)*{\afvjd9{}{}}}
\qquad\text{and}\qquad
\atomicflow{
( 4,8  )*{\afvjd8{}{}};
(10,8  )*{\afacu{}{}{}{}{}{}};
( 1,7.5)*{\afvjd9{}{}};
(14,7.5)*{\afvjd9{}{}};
(12,2.5)*{\afvjd1{}{}};
( 6,2  )*{\afaiunw{}{}}}
\quad.
\]
When no vertex labels appear on a box, we assume that the vertices in the corresponding flow can be any (so, it does not mean that there are no vertices in the flow).

\Tom{Made the following more ambiguous (as this is all we need in the rest of the paper). The double lines are now labelled with a boldface label without indicating the number of edges. Removed sentence about labeling edges with formulae.}

We sometimes use a double line notation for representing multiple edges. For example, the following diagrams represent the same flow:
\[
\atomicflow{
(0,10)*{\afvjd4{\epsilon_1}{}};
(2,10)*{\cdots};
(4,10)*{\afvjd4{}{\epsilon_l}};
(4, 7)*{\aflabelright\psi};
(2, 5)*{\affr86};
(0, 0)*{\afvju4{\iota_1}{}};
(2, 0)*{\cdots};
(4, 0)*{\afvju4{}{\iota_m}}}
\qquad\text{and}\qquad
\atomicflow{
(2,10)*{\afvjdm4{}{\boldsymbol\epsilon}};
(4, 7)*{\aflabelright\psi};
(2, 5)*{\affr86};
(2, 0)*{\afvjum4{}{\boldsymbol\iota}}}
\quad,
\]
where $l,m\ge0$; where we use  $\boldsymbol\epsilon$ to denote the vector $(\epsilon_1,\dots,\epsilon_l)$.

\Tom{Removed sub and super script from the labels in the second atomic flow. In accordance with the convention above.}
We extend the double line notation to collections of isomorphic flows. For example, for $m\ge0$, the following diagrams represent the same flow:
\[
\atomicflow{
( 4,6)*{\afawd{}{}{\iota_1}{}};
(14,6)*{\afawd{}{}{\iota_m}{}};
( 0,4)*{\afvj4};
( 7,4)*{\cdots};
(10,4)*{\afvj4};
( 2,0)*{\afaiunw{}{}};
(12,0)*{\afaiunw{}{}}}
\qquad\text{and}\qquad
\atomicflow{
( 4,6)*{\afawdm{}{}{}{\boldsymbol\iota}};
( 0,4)*{\afvjm4};
( 2,0)*{\afaiunw{}{}}}
\quad.
\]

\Tom{Added definition.}

\begin{definition}
An atomic flow is \emph{unique modulo associativity of contraction} if it is unique modulo the equivalence relation generated by the following flow rewriting system:
\[
\atomicflow
{
(-2,2.4)*{\afacdnw{\one}{}{\two}{}};
(0,-2)*{\afacd{}{}{}{}{\four}{}};
(2,4.2)*{\afvju{4.4}{\three}{}}
}\quad\rightarrow\quad
\atomicflow
{
(2,2.4)*{\afacdnw{\two}{}{\three}{}};
(0,-2)*{\afacd{}{}{}{}{\four}{}};
(-2,4.2)*{\afvju{4.4}{\one}{}}
}\quad,\qquad
\atomicflow
{
(-2,-4.4)*{\afacunw{\two}{}{\three}{}};
(0,2)*{\afacu{}{}{}{}{\one}{}};
(2,-4.2)*{\afvju{4.4}{\four}{}}
}\quad\rightarrow\quad
\atomicflow
{
(2,-4.4)*{\afacunw{\three}{}{\four}{}};
(0,2)*{\afacu{}{}{}{}{\one}{}};
(-2,-4.2)*{\afvju{4.4}{\two}{}}
},
\]
\end{definition}

In particular, the following atomic flows are unique modulo associativity of contraction:
\[
\atomicflow
{
(0,5.5)*{\afvjm3};
(0,0)*{\affr88};
(0,0)*{\copy\contrdown};
(0,-5.5)*{\afvj3};
}\quad
\atomicflow
{
(0,5.5)*{\afvj3};
(0,0)*{\affr88};
(0,0)*{\copy\contrup};
(0,-5.5)*{\afvjm3};
}\quad.
\]

\Tom{Added comment:}

Considering atomic flows modulo associativity of contraction is uncontroversial, as we could instead have transformed all the derivations and their associated atomic flows to a canonical form.

\Tom{why $m$ and not $n$? Removed comment about not insisting on connected components, because we DO insist on connected components. If we decide to have a remark later on which does not insist on connectedness, then I suggest we explain all of this in the remark.}

We observe that the flow of every $\SKS$ derivation can always be represented as a collection of $m\ge0$ connected components as follows:
\[
%---------------------------------------
\atomicflow{
(13  ,8  )*{\afaidmex{}{}{}{}{}{}21};
( 2  ,6.5)*{\afvjm5};
(24  ,6.5)*{\afvjm5};
( 9.5, 3  )*{\aflabelright{\phi'_1}};
(24.5, 3  )*{\aflabelright{\phi''_1}};
( 1  , 0  )*{\copy\weakdown};
( 3  , 0  )*{\copy\weakup};
( 5.5, 0  )*{\affr{13}8};
( 6  , 0  )*{\copy\contrdown};
( 9  , 0  )*{\copy\contrup};
(16  , 0  )*{\copy\weakdown};
(18  , 0  )*{\copy\weakup};
(20.5, 0  )*{\affr{13}8};
(21  , 0  )*{\copy\contrdown};
(24  , 0  )*{\copy\contrup};
( 2  ,-6.5)*{\afvjm5};
(24  ,-6.5)*{\afvjm5};
(13  ,-8  )*{\afaiumex{}{}{}{}{}{}21};
%-------------------
(30,0)*{\cdots};
(34,0)="A";
"A"+(13  ,8  )*{\afaidmex{}{}{}{}{}{}21};
"A"+( 2  ,6.5)*{\afvjm5};
"A"+(24  ,6.5)*{\afvjm5};
"A"+( 9  , 3  )*{\aflabelright{\phi'_m}};
"A"+(24  , 3  )*{\aflabelright{\phi''_m}};
"A"+( 1  , 0  )*{\copy\weakdown};
"A"+( 3  , 0  )*{\copy\weakup};
"A"+( 5.5, 0  )*{\affr{13}8};
"A"+( 6  , 0  )*{\copy\contrdown};
"A"+( 9  , 0  )*{\copy\contrup};
"A"+(16  , 0  )*{\copy\weakdown};
"A"+(18  , 0  )*{\copy\weakup};
"A"+(20.5, 0  )*{\affr{13}8};
"A"+(21  , 0  )*{\copy\contrdown};
"A"+(24  , 0  )*{\copy\contrup};
"A"+( 2  ,-6.5)*{\afvjm5};
"A"+(24  ,-6.5)*{\afvjm5};
"A"+(13  ,-8  )*{\afaiumex{}{}{}{}{}{}21};
}\quad,
\]
such that each edge in flow $\phi'_i$ is associated with some occurrence of some atom $a_i$, and each edge in flow $\phi''_i$ is associated with some occurrence of atom $\bar a_i$. Note that it might happen that for $i\ne j$ we have $\vlsmash{a_i\equiv a_j}$.

\begin{definition}
Given a derivation $\Phi$ where the atom $a$ occurs, we say that the atomic flow associated with $a$ in $\Phi$ is the smallest subflow of the atomic flow associated with $\Phi$ containing all the edges mapped to from occurrences of $a$ and $\bar a$.
\end{definition}

\Tom{at the very end of writing the paper check what if anything of this paragraph is applicable.}
In the following, when informally dealing with derivations, we freely transfer to them notions defined for their flows. For example, we can say that an atom occurrence is negative for a given polarity assignment (if the edge associated with the atom occurrence maps to $\pmi$) or that two atom occurrences are connected (if the associated edges belong to the same connected component). In fact, one of the advantages of working with flows is that they provide us with convenient geometrical notions.


%===============================================================================
\section{Streamlining}\label{SectStreamlining}

We know that the cut rule is admissible for derivations with premiss $\ttt$ (proofs) and, dually, that the identity rule is admissible for derivations with conclusion $\fff$ (refutations). However, neither the cut nor the identity are admissible for generic derivations, which motivated the definition of `streamlining'. Streamlining is a generalisation of both cut and identity elimination to derivations with no restrictions on their premiss or conclusion.

%TODO: which way do we direct the paths? (depends on which way we direct the edges)

Intuitively, a derivation is streamlined if every maximal path in the atomic flow associated with the derivation starts at the top or ends at the bottom of the flow. We recall the definition from \cite{GuglGund:07:Normalis:lr}:

%---------------------------------------
\begin{definition}
A derivation is \emph{streamlined} if its associated atomic flow can be represented as 
\[
\atomicflow{
(-10,11)*{\afvjm4};
%---
(-15, 5)*{\copy\contrup};
(-10, 5)*{\affr{28}8};
( -5, 5)*{\copy\contrdown};
( 10, 5)*{\copy\interdown};
( 10, 5)*{\affr88};
( 20, 5)*{\copy\weakdown};
( 20, 5)*{\affr88};
%---
(-20, 0)*{\afvjm2};
(-10, 0)*{\afvjm2};
(  0, 0)*{\afvjm2};
( 10, 0)*{\afvjm2};
( 20, 0)*{\afvjm2};
%---
(-20,-5)*{\copy\weakup};
(-20,-5)*{\affr88};
(-10,-5)*{\copy\interup};
(-10,-5)*{\affr88};
(  5,-5)*{\copy\contrup};
( 10,-5)*{\affr{28}8};
( 15,-5)*{\copy\contrdown};
%---
(  10,-11)*{\afvjm4};
}\quad.
\]
\end{definition}

Note that an atomic flow associated with a proof has no upper edges, so the top left and the two bottom left boxes in the above atomic flow would be empty. Hence, a streamlined proof is cut free and, dually, a streamlined refutation is identity free.

The main challenge in streamlining a derivation is to make sure there are no path from an identity instance to a cut instance. Once this is achieved it is straightforward, as shown in \cite{GuglGund:07:Normalis:lr}, to use confluent and strongly normalising weakening reductions to obtain (in linear time) a streamlined derivation. This motivates the following definition:

%---------------------------------------
\begin{definition}
A derivation is \emph{weakly streamlined} if its associated atomic flow can be represented as
\[
\atomicflow{
(-5, 11)*{\afvjm4};
%---
( -5, 5)*{\affr{18}8};
(-10, 5)*{\copy\contrup};
( -5, 5)*{\copy\weakdown};
(  0, 5)*{\copy\contrdown};
( 10, 5)*{\affr88};
( 10, 5)*{\copy\interdown};
%---
(-10, 0)*{\afvjm2};
(  0, 0)*{\afvjm2};
( 10, 0)*{\afvjm2};
%---
(-10,-5)*{\affr88};
(-10,-5)*{\copy\interup};
(  5,-5)*{\affr{18}8};
(  0,-5)*{\copy\contrup};
(  5,-5)*{\copy\weakup};
( 10,-5)*{\copy\contrdown};
%---
(  5,-11)*{\afvjm4};
}\quad.
\]
An atom $a$ is \emph{weakly streamlined in $\Phi$} if the atomic flow associated with $a$ in $\Phi$ is weakly streamlined.
\end{definition}

In the rest of this section we show how to weakly streamline a derivation. This is done in three steps:
\begin{enumerate}
\item remove identity and cut instances, at the expense of creating new atom occurrences in the premiss and conclusion of the derivation;
\item break the paths between all the atom occurrences added in the first step, at the expense of growing the derivation exponentially; and
\item remove the atom occurrences created in the first step by adding identity and cut instances.
\end{enumerate}

In this way we create a new derivation with the same premiss and conclusion as the original one, but whose atomic flow has no paths from identity to cut vertices.

\subsection{The Core}

%TODO: reread

In this subsection, we show a procedure for removing connected identity and cut vertices from a derivation at the expense of introducing more atoms to the premiss and conclusion. The result of this procedure is weakly streamlined and we call it the `core' of the derivation. We first define the procedure in terms of atomic flows, where the reason for the name `core' is made clear. We remove the the identity and the cut vertices of the atomic flow and join the newly formed upper and lower edges by (co)contractions where possible, what remains is the core. Based on the definition of the core of an atomic flow, the core of a derivation follows naturally.

We define the core of an atomic flow.

\Tom{Changed Definition to include new upper/lower edges and an ordered choice of components.}

\begin{definition}\label{DefFlowCore}
Given an atomic flow
\[
\phi\;\;=\;\;\atomicflow
{
(-13,0)*{\affr{22}{20}};
(-5,8)*{\aflabelright{\phi_1}};
%
(-20, 9)*{\afvjdm{10}{\boldsymbol\epsilon'_1}{}};
(-13, 8)*{\afaidm{}{}{}{}{}{}};
( -6, 9)*{\afvjdm{10}{}{\boldsymbol\epsilon''_1}};
(-18, 0)*{\affr{8}{8}};
(-17, 2)*{\aflabelright{\phi'_1}};
( -8, 0)*{\affr{8}{8}};
( -7, 2)*{\aflabelright{\phi''_1}};
( -6,-9)*{\afvjum{10}{}{\boldsymbol\iota''_1}};
(-13,-8)*{\afaium{}{}{}{}{}{}};
(-20,-9)*{\afvjum{10}{\boldsymbol\iota'_1}{}};
%------------
(0,0)*{\cdots};
%------------
(13,0)*{\affr{22}{20}};
(21,8)*{\aflabelright{\phi_n}};
%
(20, 9)*{\afvjdm{10}{}{\boldsymbol\epsilon''_n}};
(13, 8)*{\afaidm{}{}{}{}{}{}};
( 6, 9)*{\afvjdm{10}{\boldsymbol\epsilon'_n}{}};
( 8, 0)*{\affr{8}{8}};
( 9, 2)*{\aflabelright{\phi'_n}};
(18, 0)*{\affr{8}{8}};
(19, 2)*{\aflabelright{\phi''_n}};
( 6,-9)*{\afvjum{10}{\boldsymbol\iota'_n}{}};
(13,-8)*{\afaium{}{}{}{}{}{}};
(20,-9)*{\afvjum{10}{}{\boldsymbol\iota''_n}};
%------------
(  35,12)*{\afvjm4};
%---
(  35, 6)*{\affr{18}8};
(41.5, 8)*{\aflabelright{\psi_1}};
(  30, 6)*{\copy\contrup};
(  35, 6)*{\copy\weakdown};
(  40, 6)*{\copy\contrdown};
(  50, 6)*{\affr88};
(51.5, 8)*{\aflabelright{\psi_2}};
(  50, 6)*{\copy\interdown};
%---
( 30, 0)*{\afvjum4{}{\tilde{\boldsymbol\epsilon}_1}};
( 40, 0)*{\afvjum4{}{\tilde{\boldsymbol\epsilon}_2}};
( 50, 0)*{\afvjum4{}{\tilde{\boldsymbol\epsilon}_3}};
%---
(  30,-6)*{\affr88};
(31.5,-4)*{\aflabelright{\psi_3}};
(  30,-6)*{\copy\interup};
(  45,-6)*{\affr{18}8};
(51.5,-4)*{\aflabelright{\psi_4}};
(  40,-6)*{\copy\contrup};
(  45,-6)*{\copy\weakup};
(  50,-6)*{\copy\contrdown};
%---
( 45,-12)*{\afvjm4};
}\quad,
\]
where, for $1\le i\le n$, $\phi'_i$ and $\phi''_i$ contain no identity and no cut vertices and $\phi_i$ is a connected, non-weakly-streamlined subflow, we define a \emph{core of $\phi$} to be
\[
\atomicflow
{
(-21,11)*{\afvjdm{14}{\boldsymbol\epsilon'_1}{}};
(-17,16)*{\afvjd4{}{\lambda'_1}};
(-17,10)*{\affr{6}{8}};
(-17,10)*{\copy\contrup};
(-17, 5)*{\afvjm{2}};
(-18, 0)*{\affr{8}{8}};
(-17, 2)*{\aflabelright{\phi'_1}};
(-21,-11)*{\afvjum{14}{\boldsymbol\iota'_1}{}};
(-17,-16)*{\afvju4{}{\mu'_1}};
(-17,-10)*{\affr{6}{8}};
(-17,-10)*{\copy\contrdown};
(-17, -5)*{\afvjm{2}};
%
( -9,16)*{\afvjd4{}{\lambda''_1}};
( -9,10)*{\affr{6}{8}};
( -9,10)*{\copy\contrup};
( -9, 5)*{\afvjm{2}};
( -5,11)*{\afvjdm{14}{}{\boldsymbol\epsilon''_1}};
( -8, 0)*{\affr{8}{8}};
( -7, 2)*{\aflabelright{\phi''_1}};
( -9,-16)*{\afvju4{}{\mu''_1}};
( -9,-10)*{\affr{6}{8}};
( -9,-10)*{\copy\contrdown};
( -9, -5)*{\afvjm{2}};
( -5,-11)*{\afvjum{14}{}{\boldsymbol\iota''_1}};
( -8, 0)*{\affr{8}{8}};
%------------
(0,0)*{\cdots};
%------------
( 9,16)*{\afvjd4{}{\lambda'_n}};
( 9,10)*{\affr{6}{8}};
( 9,10)*{\copy\contrup};
( 9, 5)*{\afvjm{2}};
( 5,11)*{\afvjdm{14}{\boldsymbol\epsilon'_n}{}};
( 8, 0)*{\affr{8}{8}};
( 9, 2)*{\aflabelright{\phi'_n}};
( 9,-16)*{\afvju4{}{\mu'_n}};
( 9,-10)*{\affr{6}{8}};
( 9,-10)*{\copy\contrdown};
( 9, -5)*{\afvjm{2}};
( 5,-11)*{\afvjum{14}{\boldsymbol\iota'_n}{}};
( 8, 0)*{\affr{8}{8}};
%
(21,11)*{\afvjdm{14}{}{\boldsymbol\epsilon''_n}};
(17,16)*{\afvjd4{}{\lambda''_n}};
(17,10)*{\affr{6}{8}};
(17,10)*{\copy\contrup};
(17, 5)*{\afvjm{2}};
(18, 0)*{\affr{8}{8}};
(19, 2)*{\aflabelright{\phi''_n}};
(21,-11)*{\afvjum{14}{}{\boldsymbol\iota''_n}};
(17,-16)*{\afvju4{}{\mu''_n}};
(17,-10)*{\affr{6}{8}};
(17,-10)*{\copy\contrdown};
(17, -5)*{\afvjm{2}};
%---------
(  35,14)*{\afvjm8};
%---
(  35, 6)*{\affr{18}8};
(41.5, 8)*{\aflabelright{\psi_1}};
(  30, 6)*{\copy\contrup};
(  35, 6)*{\copy\weakdown};
(  40, 6)*{\copy\contrdown};
(  50, 6)*{\affr88};
(51.5, 8)*{\aflabelright{\psi_2}};
(  50, 6)*{\copy\interdown};
%---
( 30, 0)*{\afvjum4{}{\tilde{\boldsymbol\epsilon}_1}};
( 40, 0)*{\afvjum4{}{\tilde{\boldsymbol\epsilon}_2}};
( 50, 0)*{\afvjum4{}{\tilde{\boldsymbol\epsilon}_3}};
%---
(  30,-6)*{\affr88};
(31.5,-4)*{\aflabelright{\psi_3}};
(  30,-6)*{\copy\interup};
(  45,-6)*{\affr{18}8};
(51.5,-4)*{\aflabelright{\psi_4}};
(  40,-6)*{\copy\contrup};
(  45,-6)*{\copy\weakup};
(  50,-6)*{\copy\contrdown};
%---
( 45,-14)*{\afvjm8};
}\quad.
\]
For every $1\le i\le n$, the \emph{new upper edge of} $\phi'_i$ (resp., $\phi''_i$) is $\lambda'_i$ (resp., $\lambda''_i$), the \emph{new lower edge of} $\phi'_i$ (resp., $\phi''_i$) is $\mu'_i$ (resp., $\mu''_i$) and the \emph{new upper} (resp., \emph{lower}) \emph{edges of} $\phi_i$ are $\lambda'_i$ and $\lambda''_i$ (resp., $\mu'_i$ and $\mu''_i$).
We say that $\phi_1$, $\dots$, $\phi_n$ is an \emph{ordered choice of components from $\phi$}.
\end{definition}

\Tom{In previous definition: The ordered choice of components is given by the definition and needs not be made explicit.}

\Tom{`Make 4.3 and 4.4 into a remark, use this in def 4.5'. I haven't figured out how to do this elegantly.}

%TODO: give an example

\begin{proposition}\label{PropAssoContr}
Given an atomic flow $\phi$, two cores of $\phi$ are equivalent modulo associativity of contraction.
\end{proposition}

By Proposition~\ref{PropAssoContr} we can consider a core of an atomic flow to be unique and we therefore refer to \emph{the core}.

\newcommand{\Core}{\mathsf{Core}}

\begin{definition}
Given an atomic flow $\phi$ we denote the core of $\phi$ by $\Core(\phi)$.
\end{definition}

A core of a derivation is defined based on the core of its atomic flow:

\Tom{Changed definition to make sure that the atom occurrences in the premiss and in the conclusion pair up the way they should.}

\begin{definition}\label{DefDerCore}
Given a derivation $\vlder{\Phi}{}{\beta}{\alpha}$ with associated atomic flow $\phi$, such that $\phi_1$, $\dots$, $\phi_n$ are all the non-weakly-streamlined, connected subflows of $\phi$, a \emph{core of\/ $\Phi$} is defined to be a derivation
\[
\vlder{}{}{\vls[\beta.(a^{\mu'_n}_n.{\bar a^{\mu''_n}_n}).\cdots.(a^{\mu'_1}_1.{\bar a^{\mu'_1}_1})]}{\vls([a^{\lambda'_1}_1.{\bar a^{\lambda''_1}_1}].\cdots.[a^{\lambda'_n}_n.{\bar a^{\lambda'_n}_n}].\alpha)}
\]
with associated atomic flow $\Core(\phi)$, such that, for every $1\le i\le n$, $\lambda'_i$ and $\lambda''_i$ (resp., $\mu'_i$ and $\mu''_i$) are the new upper (resp., lower) edges of $\phi_i$.
\end{definition}

The core of a derivation does not have the same premiss and conclusion as the original derivation. In the next subsection we see how we can glue several cores together to obtain a weakly streamlined derivation with the correct premiss and conclusion.

The following proposition can easily by verified by studying the atomic flows in Definition~\ref{DefFlowCore}.

\begin{proposition}\label{PropStreamlinedCore}
A core of a derivation $\Phi$ is weakly streamlined and every non-weakly-streamlined atom in $\Phi$ does not occur in an identity or cut instance in a core of\/ $\Phi$.
\end{proposition}

Given a derivation, we can construct several cores with trivial differences. However, we show how a core can be extracted, and we will single out the core obtained in this way and refer to it as \emph{the core}.

To be able to remove identity and cut instances from a derivation, they must first be `pulled' towards the premiss and conclusion, respectively. The following lemma shows how a subformula can be `pulled' towards the `outside' of the derivation, both going up and going down.

\begin{lemma}\label{LemSuperSwitch}
Given a context $\xi\vlhole$ and a formula $\alpha$ there exist derivations $\vldownsmash{\vlder{}{\{\swi\}}{\xi\{\alpha\}}{\vls(\alpha.\xi\{\ttt\})}}$ and $\vlder{}{\{\swi\}}{\vls[\xi\{\fff\}.\alpha]}{\xi\{\alpha\}}$.
\end{lemma}

\begin{proof}
We show how to construct the first derivation, the second one can be done symmetrically. We argue by induction on the number of atoms in $\xi\vlhole$. The base case, $\xi\vlhole=\vlhole$, is trivial and the inductive cases are:

\[
\vlderivation
{
 \vlin{=}{}{\xi\{\alpha\}}
 {
  \vlin{\swi}{}{\vlsbr[\vlder{\Psi}{\{\swi\}}{\xi'\{\alpha\}}{\vls(\alpha.\xi'\{\ttt\})}\;\;.\;\;\beta]}
  {
   \vlin{=}{}{\vls(\alpha.[\xi'\{\ttt\}.\beta])}
   {
    \vlhy{\vls(\alpha.\xi\{\ttt\})}
   }
  }
 }
}\qquad\mbox{and}\qquad
\vlderivation
{
 \vlin{=}{}{\xi\{\alpha\}}
 {
  \vlin{=}{}{\vlsbr(\vlder{\Psi'}{\{\swi\}}{\xi'\{\alpha\}}{\vls(\alpha.\xi'\{\ttt\})}\;\;.\;\;\beta)}
  {
   \vlhy{\vls(\alpha.\xi\{\ttt\})}
  }
 }
}\quad,
\]
for some $\xi'\vlhole$ and $\beta$ where $\beta$ is not a unit and $\Psi$ and $\Psi'$ exist by the inductive hypothesis.
\end{proof}

We show how the previous lemma can be used to pull identity instances out and up and cut instances out and down, without affecting the atomic flow.

\begin{lemma}\label{LemDecompInt}
Given a derivation $\vlder{}{}{\beta}{\alpha}$ with associated atomic flow $\phi$, there exists a derivation
\[
\vlder{}{\SKS\setminus\{\aid,\aiu\}}{\vlsbr[\beta\;.\;\vlinf{}{}{\fff}{\vls(b_m.\bar b_m)}\;.\;\cdots\;.\;\vlinf{}{}{\fff}{\vls(b_1.\bar b_1)}]}{\vlsbr(\vlinf{}{}{\vls[a_1.\bar a_1]}{\ttt}\;.\;\cdots\;.\;\vlinf{}{}{\vls[a_n.\bar a_n]}{\ttt}\;.\;\alpha)}
\]
with associated atomic flow $\phi$, for some atoms $a_1,\dots,a_n,b_1,\dots,b_m$.
\end{lemma}

\begin{proof}
Using Lemma~\ref{LemSuperSwitch} apply the following transformations to each of the identity and cut instances in $\Phi$:
\[
\vlderivation
{
 \vlde{\Psi'}{}{\beta}
 {
  \vlde{\Psi}{}{\xi\left\{\vlinf{}{}{\vls[a.{\bar a}]}{\ttt}\right\}}
  {
   \vlhy{\alpha}
  }
 }
}\quad\rightarrow\quad
\vlderivation
{
 \vlde{\Psi'}{}{\beta}
 {
  \vlde{}{\{\swi\}}{\xi\vlsbr[a.{\bar a}]}
  {
   \vlhy{\vlsbr(\vlinf{}{}{\vls[a.{\bar a}]}{\ttt}\;\;.\;\;\vlder{\Psi}{}{\xi\{\ttt\}}{\alpha})}
  }
 }
}\qquad\mbox{and}\qquad
\vlderivation
{
 \vlde{\Psi'}{}{\beta}
 {
  \vlde{\Psi}{}{\xi\left\{\vlinf{}{}{\fff}{\vls(a.{\bar a})}\right\}}
  {
   \vlhy{\alpha}
  }
 }
}\quad\rightarrow\quad
\vlderivation
{
 \vlde{}{\{\swi\}}{\vlsbr[\vlder{\Psi'}{}{\beta}{\xi\{\fff\}}\;\;.\;\;\vlinf{}{}{\fff}{\vls(a.{\bar a})}]}
 {
  \vlde{\Psi}{}{\xi\vlsbr(a.{\bar a})}
  {
   \vlhy{\alpha}
  }
 }
}\quad.
\]
\end{proof}

\begin{remark}
The derivation obtained in the proof of Lemma~\ref{LemDecompInt} is unique modulo equations. Should we wish to obtain a syntactically unique derivation we need only fix the order in which we do the transformations (\emph{e.g.}\ top-to-bottom).
\end{remark}

%TODO: rewrite and say that it is routine
%The way the normaliser in the next section works is by stitching together atoms from the conclusion in one copy of the core with atoms from the premiss of another copy of the core. It is therefore convenient that the number of occurrences of each atom is the same in the premiss and in the conclusion. We use (co)contractions to make sure we have exactly one occurrence of every atom.

\begin{lemma}\label{LemGenericContraction}
Given a formula $\alpha$ and a positive integer $n$, there exist derivations $\vlupsmash{\vlder{}{\{\acd,\med\}}{\alpha}{\bigvee_{i=1}^{n}\alpha}}$ and $\vlupsmash{\vlder{}{\{\acu,\med\}}{\bigwedge_{i=1}^{n}\alpha}{\alpha}}$.
\end{lemma}

\begin{proof}
We show how to construct the first derivation, the second one can be done symmetrically. We argue by induction on $n$. The first base case, $n=1$, is trivial and for the second base case, $n=2$, we argue by induction on the number of atom occurrences in $\alpha$. We have to consider the following base case and two inductive cases:
\[
\vlinf{\acd}{}{a}{\vls[a.a]}
\qquad\hbox{,}\qquad
\vlderivation
{
 \vlin{=}{}{\vls(\alpha.\beta)}
 {
  \vlin{\med}{}{\vlsbr(\vlder{}{\{\acd,\med\}}{\alpha}{\vls[\alpha.\alpha]}\;\;.\;\;\vlder{}{\{\acd,\med\}}{\beta}{\vls[\beta.\beta]})}
  {
   \vlhy{\vls[(\alpha.\beta).(\alpha.\beta)]}
  }
 }
}\qquad\hbox{and}\qquad
\vlderivation
{
 \vlin{=}{}{\vls[\alpha.\beta]}
 {
  \vlin{=}{}{\vlsbr[\vlder{}{\{\acd,\med\}}{\alpha}{\vls[\alpha.\alpha]}\;\;.\;\;\vlder{}{\{\acd,\med\}}{\beta}{\vls[\beta.\beta]}]}
  {
   \vlhy{\vls[[\alpha.\beta].[\alpha.\beta]]}
  }
 }
}\quad.
\]
Finally, we show the inductive case, $n>2$:
\[
\vlderivation
{
 \vlde{}{\{\acd,\med\}}{\alpha}
 {
  \vlin{=}{}{\vlsbr[\vlder{}{\{\acd,\med\}}{\alpha}{\bigvee_{i=1}^{n-\lfloor n/2\rfloor}\alpha}\;\;.\;\;\vlder{}{\{\acd,\med\}}{\alpha}{\bigvee_{i=1}^{\lfloor n/2\rfloor}\alpha}]}
  {
   \vlhy{\bigvee_{i=1}^{n}\alpha}
  }
 }
}\quad.
\]
\end{proof}

\newcommand{\contr}{\mathsf{c}}
\newcommand{\cod}{{\contr{\downarrow}}}
\newcommand{\cou}{{\contr{\uparrow}}}
\begin{remark}\label{RemGenericContraction}
In the non-atomic version of system $\SKS$ the derivations shown in Lemma~\ref{LemGenericContraction} correspond to repeated applications of (co)contractions. For this reason we sometimes write the inference rules $\vlinf{n\cdot\cod}{}{\alpha}{\bigvee_{i=1}^{n}\alpha}$ and $\vlinf{n\cdot\cou}{}{\bigwedge_{i=1}^{n}\alpha}{\alpha}$ instead of the derivations $\vlder{}{\{\acd,\med\}}{\alpha}{\bigvee_{i=1}^{n}\alpha}$ and $\vlupsmash{\vlder{}{\{\acu,\med\}}{\bigwedge_{i=1}^{n}\alpha}{\alpha}}$, respectively.
\end{remark}

\begin{remark}
The derivations shown in Lemma~\ref{LemGenericContraction} can be constructed in many ways and, treating the atom occurrences in $\alpha$ as distinct, they are all equal modulo associativity of contraction. The way in which the derivations are constructed is therefore not important, but should we wish to fix one we consider the derivations in the proof of the lemma to be canonical.
\end{remark}

\begin{theorem}\label{ThmExistCore}
Given a derivation $\vlder{\Phi}{}{\beta}{\alpha}$, a core of\/ $\Phi$ can be constructed.
\end{theorem}

\begin{proof}
Let $\phi$ be the atomic flow of $\Phi$ and label the sublfows of $\phi$ as in Definition~\ref{DefFlowCore}. Let atom occurrences of the atoms $a_1,\dots,a_n$ map to edges in the subflows $\phi_1,\dots,\phi_n$ respectively, let atom occurrences of the atoms $b_1,\dots,b_k$ map to edges in the subflow $\psi_2$ and let atom occurrences of the atoms $c_1,\dots,c_l$ map to edges in the subflow $\psi_3$. Then we build a core of $\Phi$ as follows:
\[
\vlderivation
{
 \vlde{\Psi_2}{\{\acd,\med\}}{\vls[\beta.(a_n.{\bar a_n}).\cdots.(a_1.{\bar a_1})]}
 {
  \vlde{\Phi'}{\SKS\setminus\{\aid,\aiu\}}{{\vlsbr[\beta\;.\;\vlinf{}{}{\fff}{\vls(c_l.\bar c_l)}\;.\;\cdots\;.\;\vlinf{}{}{\fff}{\vls(c_1.\bar c_1)}\;.\;(a_n.\bar a_n)\;.\;\cdots\;.\;(a_n.\bar a_n)\;.\;\cdots\;.\;(a_1.\bar a_1)\;.\;\cdots\;.\;(a_1.\bar a_1)]}}
  {
   \vlde{\Psi_1}{\{\acu,\med\}}{{\vlsbr([a_1.\bar a_1]\;.\;\cdots\;.\;[a_1.\bar a_1]\;.\;\cdots\;.\;[a_n.\bar a_n]\;.\;\cdots\;.\;[a_n.\bar a_n]\;.\;\vlinf{}{}{\vls[b_1.\bar b_1]}{\ttt}\;.\;\cdots\;.\;\vlinf{}{}{\vls[b_k.\bar b_k]}{\ttt}\;.\;\alpha)}}
   {
    \vlhy{\vls([a_1.{\bar a_1}].\cdots.[a_n.{\bar a_n}].\alpha)}
   }
  }
 }
}\quad,
\]
where $\Phi'$ exists by Lemma~\ref{LemDecompInt} and $\Psi_1$ and $\Psi_2$ exist by Lemma~\ref{LemGenericContraction}. By studying the proofs of Lemma~\ref{LemDecompInt} and Lemma~\ref{LemGenericContraction}, we can observe that the derivation has atomic flow $\Core(\phi)$.
\end{proof}

%TODO: by the above remarks it is obvious how this is unique, but maybe we should make a final remark?

\begin{definition}
Given a derivation $\Phi$, the core of $\Phi$ obtained as described in the proof of Theorem~\ref{ThmExistCore} is called \emph{the core of\/ $\Phi$}, denoted $\Core(\Phi)$.
\end{definition}

\subsection{The Path Breaker}\label{SectBreak} 

\Tom{Explain `correspondence'.}

\newcommand{\Break}{\mathsf{Break}}
\begin{definition}\label{DefPathBreak}
The \emph{path breaker}, $\Break$, is an operator whose arguments are a derivation $\vlder{\Phi}{}{\beta}{\alpha}$ and the atom occurrences $a^\lambda$ and $a^\mu$, such that $\alpha=\vlsmallbrackets\vls([a^\lambda.\bar a].\gamma)$, $\beta=\vls[\delta.(a^\mu.\bar a)]$, and the results are a derivation and two atom occurrences $a^\epsilon$ and $a^\iota$ such that $\Break(\Phi,a^\lambda,a^\mu)=(\Psi,a^\epsilon,a^\iota)$, where:
\newbox\DeltaTopK
\setbox\DeltaTopK=
\hbox{$
\vlderivation
{
 \vlin{=}{}{\vls[\delta.(\vlinf{}{}{\ttt}{a^{\mu'}}.\bar a)]}
 {
  \vlde{\Phi}{}{\beta}
  {
   \vlhy{\alpha}
  }
 }
}$
}
\newbox\DeltaK
\setbox\DeltaK=
\hbox{$
\vlderivation
{
 \vlin{=}{}{\vls[\delta.(a^{\epsilon'}.\vlinf{}{}{\ttt}{\bar a})]}
 {
  \vlde{\Phi}{}{\beta}
  {
   \vlin{=}{}{\alpha}
   {
    \vlhy{\vls([\vlinf{}{}{a^{\lambda'}}{\fff}.\bar a].\gamma)}
   }
  }
 }
}$
}
\newbox\DeltaBotK
\setbox\DeltaBotK=
\hbox{$
\vlderivation
{
 \vlde{\Phi}{}{\beta}
 {
  \vlin{=}{}{\alpha}
  {
   \vlhy{\vls([a^{\epsilon'}.\vlinf{}{}{\bar a}{\fff}].\gamma)}
  }
 }
}$
}
\[
\Psi\quad=\quad
\vlderivation
{
 \vlin{=}{}{\vls[\vlinf{2\cdot\cod}{}{\delta}{\vls[\delta.\delta.\delta]}\;.\;(a^\iota.\bar a)]}
 {
  \vlin{=}{}{\vlsbr[\delta\;\;\;.\;\;\;\delta\;\;\;.\;\;\;\box\DeltaBotK]}
  {
   \vlin{\swi}{}{\vlsmallbrackets\vls[(\gamma.a^{\epsilon'}).[\delta.\delta]]}
   {
    \vlin{=}{}{\vlsmallbrackets\vls(\gamma.[a^{\epsilon'}.[\delta.\delta]])}
    {
     \vlin{=}{}{\vlsbr([\delta\;\;\;\;\;.\;\;\;\;\;\box\DeltaK]\;\;\;\;\;.\;\;\;\;\;\gamma)}
     {
      \vlin{=}{}{\vls(\vlinf{\swi}{}{\vls[(\gamma.\bar a).\delta]}{\vls(\gamma.[\bar a.\delta])}\;.\;\gamma)}
      {
       \vlin{=}{}{\vlsbr(\box\DeltaTopK\;\;\;.\;\;\;\gamma\;\;\;.\;\;\;\gamma)}
       {
        \vlhy{\vls([a^\epsilon.\bar a]\;.\;\vlinf{2\cdot\cou}{}{\vls(\gamma.\gamma.\gamma)}{\gamma})}
       }
      }
     }
    }
   }
  }
 } 
}\quad,
\]
where $\epsilon$, $\lambda'$ and $\epsilon'$ correspond to $\lambda$ and $\mu'$, $\epsilon'$ and $\iota$ correspond to $\mu$ in the atomic flow of $\Phi$.
\end{definition}

%TODO: superposition of colors

\Tom{Changed the next proposition.}

\begin{proposition}\label{PropPathBreak}
If, for some flows $\phi$ and $\psi$, the atomic flow of $\vlder{\Phi}{}{\vlsmallbrackets\vls[\beta.(a^{\mu}.\bar a^{\mu'})]}{\vlsmallbrackets\vls([a^{\lambda}.\bar a^{\lambda'}].\alpha)}$ is of shape
\[
\atomicflow
{
(-8, 6)*{\afvjm{4}};
(-2, 6)*{\afvju{4}{\lambda}{}};
( 2, 6)*{\afvju{4}{}{\lambda'}};
( 8, 6)*{\afvjm{4}};
(-5, 0)*{\affr{8}{8}};
(-4, 2)*{\aflabelright\phi};
%---
( 5, 0)*{\affr{8}{8}};
( 6, 2)*{\aflabelright{\psi}};
( 8,-6)*{\afvjm{4}};
(-2,-6)*{\afvjd{4}{\mu}{}};
( 2,-6)*{\afvjd{4}{}{\mu'}};
(-8,-6)*{\afvjm{4}};
}\quad,
\]
and if\/ $\Break(\Phi,a^\lambda,a^\mu)=\left(\vlder{\Psi}{}{\beta}{\alpha},a^\epsilon,a^\iota\right)$, where $\alpha=\vlsmallbrackets\vls([a^\epsilon.\bar a^{\epsilon'}].\gamma)$ and $\beta=\vlsmallbrackets\vls[\delta.(a^\iota.\bar a^{\iota'})]$, then
\begin{itemize}
	\item there are no paths from $\epsilon$ to $\iota$ and no paths from $\epsilon'$ to $\iota'$ in the atomic flow of\/ $\Psi$; and
	\item there are no paths from an upper path $\epsilon''$ to a lower path $\iota''$ in the atomic flow of $\Psi$ unless there is a path from the corresponding upper path $\lambda''$ to the lower path $\mu''$ in the atomic flow of $\Phi$.
\end{itemize}
\end{proposition}

\begin{figure}
\[
\atomicflow
{
(-8, 6)*{\afvjm{4}};
(-2, 6)*{\afvju{4}{\lambda}{}};
( 2, 6)*{\afvju{4}{}{\lambda'}};
( 8, 6)*{\afvjm{4}};
(-5, 0)*{\affr{8}{8}};
(-4, 2)*{\aflabelright\phi};
%---
( 5, 0)*{\affr{8}{8}};
( 6, 2)*{\aflabelright{\psi}};
( 8,-6)*{\afvjm{4}};
(-2,-6)*{\afvjd{4}{\mu}{}};
( 2,-6)*{\afvjd{4}{}{\mu'}};
(-8,-6)*{\afvjm{4}};
}\qquad\qquad
\atomicflow
{
%%%%% RED %%%%%
(0,-20)="D";
(0,-10)="Dhalf";
%% contractions
"D"+"D"="A";
%left
"A"+(-14,-15.5)-"D"*{\afvjmcol{23}{Red}};
"A"+(-11,-16.5)*{\afvjmcol{3}{Red}};
%right
"A"+(11,-11.5)-"Dhalf"*{\afvjmcol{11}{Red}};
"A"+(14,-15.5)-"D"*{\afvjmcol{23}{Red}};
"A"+(11,-16.5)*{\afvjmcol{3}{Red}};
% top boxes
(0,0)="A";
"A"+(-11,-14)*{\afcjrmcol{6}{20}{Red}};
"A"+(11,-14)*{\afcjlmcol{6}{20}{Red}};
"A"+(-2, 11)*{\afvjdcol{14}{\epsilon}{}{Red}};
"A"+( 2, 11)*{\afvjdcol{14}{}{\epsilon'}{Red}};
"A"+(-2, -8)*{\afawucol{}{}{\mu}{}{}{Red}};
% join one
"A"+(2,-7)*{\afvjdcol6{}{\mu'}{Red}};
"A"+(2,-13)*{\afvjucol6{}{\lambda'}{Red}};
% middle boxes
"A"+"D"="A";
"A"+(9.5,-10)*{\afcjlmcol{3}{12}{Red}};
"A"+( 2,-8)*{\afawucol{}{}{}{\mu'}{}{Red}};
%%%%% GREEN %%%%%
%% cocontractions
(0,0)="A";
%left
"A"+(-11,16.5)*{\afvjmcol{3}{OliveGreen}};
"A"+"D"+(-14,15.5)*{\afvjmcol{23}{OliveGreen}};
"A"+"Dhalf"+(-11,11.5)*{\afvjmcol{11}{OliveGreen}};
%right
"A"+(11,16.5)*{\afvjmcol{3}{OliveGreen}};
"A"+"D"+(14,15.5)*{\afvjmcol{23}{OliveGreen}};
% middle boxes
"A"+"D"="A";
"A"+(-9.5,10)*{\afcjlmcol{3}{12}{OliveGreen}};
"A"+(-2, 8)*{\afawdcol{}{}{\lambda}{}{}{OliveGreen}};
% join two
"A"+(-2, -7)*{\afvjdcol6{\mu}{}{OliveGreen}};
"A"+(-2,-13)*{\afvjucol6{\lambda}{}{OliveGreen}};
% bottom boxes
"A"+"D"="A";
"A"+(-11,14)*{\afcjlmcol{6}{20}{OliveGreen}};
"A"+(11,14)*{\afcjrmcol{6}{20}{OliveGreen}};
"A"+(-2,-11)*{\afvjucol{14}{\iota}{}{OliveGreen}};
"A"+( 2,-11)*{\afvjucol{14}{}{\iota'}{OliveGreen}};
"A"+( 2, 8)*{\afawdcol{}{}{}{\lambda'}{}{OliveGreen}};
%%%%% BLACK %%%%%
%% cocontractions
(0,0)="A";
%left
"A"+(-8,5.5)*{\afvjm3};
"A"+(-11,11)*{\affr88};
"A"+(-11,11)*{\copy\contrup};
%right
"A"+(8,5.5)*{\afvjm3};
"A"+"Dhalf"+(11,11.5)*{\afvjm{11}};
"A"+(11,11)*{\affr88};
"A"+(11,11)*{\copy\contrup};
%% contractions
"D"+"D"="A";
%left
"A"+(-11,-11.5)-"Dhalf"*{\afvjm{11}};
"A"+(-8,-5.5)*{\afvjm3};
"A"+(-11,-11)*{\affr88};
"A"+(-11,-11)*{\copy\contrdown};
%right
"A"+(8,-5.5)*{\afvjm3};
"A"+(11,-11)*{\affr88};
"A"+(11,-11)*{\copy\contrdown};
% top boxes
(0,0)="A";
"A"+(-5,  0)*{\affr{8}{8}};
"A"+(-4,  2)*{\aflabelright{\phi}};
"A"+( 5,  0)*{\affr{8}{8}};
"A"+( 6,  2)*{\aflabelright{\psi}};
% middle boxes
"A"+"D"="A";
"A"+(9.5,10)*{\afcjrm{3}{12}};
"A"+(-9.5,-10)*{\afcjrm{3}{12}};
"A"+(-5, 0)*{\affr{8}{8}};
"A"+(-4, 2)*{\aflabelright{\phi}};
"A"+( 5, 0)*{\affr{8}{8}};
"A"+( 6, 2)*{\aflabelright{\psi}};
% bottom boxes
"A"+"D"="A";
"A"+(-5, 0)*{\affr{8}{8}};
"A"+(-4, 2)*{\aflabelright{\phi}};
"A"+( 5, 0)*{\affr{8}{8}};
"A"+( 6, 2)*{\aflabelright{\psi}};
}
\]
\caption{The atomic flows of $\Phi$ (left) and $\Psi$ (right) such that $\Break(\Phi,a^\lambda,a^\mu)=(\Psi,a^\epsilon,a^\iota)$.}
\label{FigFlowBreak}
\end{figure}

\begin{proof}
Refer to the atomics in Figure~\ref{FigFlowBreak}.
\begin{itemize}
	\item All the edges that might be in paths from $\epsilon$ or $\epsilon'$ are coloured in red and all the edges that might be in paths to $\iota$ or $\iota'$ are coloured in green. Since the red and the green paths do not overlap, there are no paths from $\epsilon$ to $\iota$ and no paths from $\epsilon'$ to $\iota'$; and
	\item If there is a path from an upper edge $\epsilon''$ to a lower edge $\mu''$ in the atomic flow of $\Psi$ the path must pass through one of the three copies of either $\phi$ or $\psi$, hence there must be a path from the corresponding upper edge $\lambda''$ to the corresponding lower edge $\mu''$ in the atomic flow of $\Phi$.
\end{itemize}
\end{proof}

\Tom{Changed `restriction' into `assumption'. I don't know if this improves anything... I thought it would be clear.}

\begin{remark}
A stronger version of Proposition~\ref{PropPathBreak}, without any assumptions about the atomic flow of $\Phi$, also holds. However, assuming $\phi$ and $\psi$ are disconnected makes the atomic flow of $\Psi$ easier to visualise and the stronger version of the proposition is not needed for the main result in this paper.
\end{remark}

\subsection{The Normaliser}\label{SectNorm}

\newcommand{\Norm}{\mathsf{Norm}}
\begin{definition}
For every $n\ge0$ the \emph{normaliser of degree n}, $\Norm_n$, is an operator whose arguments are a derivation $\vlder{\Phi}{}{\beta}{\alpha}$, with atomic flow $\phi$, and $\phi_1$, $\dots$, $\phi_n$, an ordered choice of components from $\phi$; let
\[
\Core(\Phi)=
\vlder{}{}{\vls[\beta.(a_1^{\mu'_1}.\bar a_1).\dots.(a_n^{\mu'_n}.\bar a_n)]}{\vls([a_1^{\lambda'_1}.\bar a_1].\dots.[a_n^{\lambda'_n}.\bar a_n].\alpha)}
\]
such that for every $1\le i\le n$, we have that $\lambda'_i$ (resp., $\mu'_i$) is the new upper (resp., lower) edge of $\phi_i$, and let
\[
\Psi=\Break(\Break(\dots(\Break(\Core(\Phi),a^{\lambda'_n}_n,a^{\mu'_n}_n))\dots),a^{\lambda'_1}_1,a^{\mu'_1}_1)\quad,
\]
then
\[
\Norm_n(\Phi,\phi_1,\dots,\phi_n)=
\vlder{\Psi}{}{\vlsbr[\beta\;.\;\vlinf{}{}{\fff}{\vls(a_1.\bar a_1)}\;.\;\cdots\;.\;\vlinf{}{}{\fff}{\vls(a_n.\bar a_n)}]}{\vlsbr(\vlinf{}{}{\vls[a_1.\bar a_1]}{\ttt}\;.\;\cdots\;.\;\vlinf{}{}{\vls[a_n.\bar a_n]}{\ttt}\;.\;\alpha)}\quad.
\]
\end{definition}

%TODO: spacing of lists throughout the paper

\Tom{Changed Theorem due to changes in def.}

\begin{theorem}
Given a derivation $\vlder{\Phi}{}{\beta}{\alpha}$, with atomic flow $\phi$, and $\phi_1$, $\dots$, $\phi_n$, an ordered choice of components from $\phi$, the derivation $\Norm_n(\Phi,\phi_1,\dots,\phi_n)$ is weakly streamlined and has the same premiss and conclusion as $\Phi$.
\end{theorem}

\Tom{Added proof.}

\begin{proof}
Let
\[
\Norm_n(\Phi,\phi_1,\dots,\phi_n)=
\vlder{\Psi}{}{\vlsbr[\beta\;.\;\vlinf{}{}{\fff}{\vls(a^{\mu'_1}_1.\bar a^{\mu''_1}_1)}\;.\;\cdots\;.\;\vlinf{}{}{\fff}{\vls(a^{\mu'_n}_n.\bar a^{\mu''_n}_n)}]}{\vlsbr(\vlinf{}{}{\vls[a^{\lambda'_1}_1.\bar a^{\lambda''_1}_1]}{\ttt}\;.\;\cdots\;.\;\vlinf{}{}{\vls[a^{\lambda'_n}_n.\bar a^{\lambda'_n}_n]}{\ttt}\;.\;\alpha)}\quad.
\]
By induction on Proposition~\ref{PropPathBreak} it follows that, for $1\le i\le n$, there are no paths from $a^{\lambda'_i}_i$ to $a^{\mu'_i}_i$ and no paths from $\bar a^{\lambda''_i}_i$ to $\bar a^{\mu''_i}_i$. It then follows, by Definition~\ref{DefFlowCore}, that $\Norm_n(\Phi,\phi_1,\dots,\phi_n)$ is weakly streamlined.
\end{proof}

\Tom{Changed Example due to changes in def.}

\begin{example}
Given a derivation $\Phi$ with atomic flow
\[
\phi\;\;=\;\;\atomicflow
{
(-13,0)*{\affr{22}{20}};
(-5,8)*{\aflabelright{\phi_1}};
%
(-20, 9)*{\afvjm{10}};
(-13, 8)*{\afaid{}{}{}{}{}{}};
( -6, 9)*{\afvjm{10}};
(-18, 0)*{\affr{8}{8}};
(-17, 2)*{\aflabelright{\phi'_1}};
( -8, 0)*{\affr{8}{8}};
( -7, 2)*{\aflabelright{\phi''_1}};
( -6,-9)*{\afvjm{10}};
(-13,-8)*{\afaiu{}{}{}{}{}{}};
(-20,-9)*{\afvjm{10}};
%------------
(13,0)*{\affr{22}{20}};
(21,8)*{\aflabelright{\phi_2}};
%
(20, 9)*{\afvjm{10}};
(13, 8)*{\afaid{}{}{}{}{}{}};
( 6, 9)*{\afvjm{10}};
( 8, 0)*{\affr{8}{8}};
( 9, 2)*{\aflabelright{\phi'_n}};
(18, 0)*{\affr{8}{8}};
(19, 2)*{\aflabelright{\phi''_n}};
( 6,-9)*{\afvjm{10}};
(13,-8)*{\afaiu{}{}{}{}{}{}};
(20,-9)*{\afvjm{10}};
}\qquad
\atomicflow
{
(0,9)*{\afvjm{10}};
(0,0)*{\affr88};
(2,2)*{\aflabelright{\psi}};
(0,-9)*{\afvjm{10}};
}\quad,
\]
where $\phi'_1$, $\phi''_1$, $\phi'_2$ and $\phi''_2$ contain no identity and no cut vertices and $\phi_1$ and $\phi_2$ are connected, non-weakly-streamlined subflows, the atomic flow of $\Norm_2(\Phi,\phi'_1,\phi'_2)$ is
\[
\atomicflow
{
%cocontraction - top
(12,43.5)*{\afvjm{3}};
(12,38)*{\affr{34}8};
(12,38)*{\copy\contrup};
(-18,46)*{\afaidex{}{}{}{}{}{}31};
(-24,38)*{\affr{10}8};
(-24,38)*{\copy\contrup};
(-12,38)*{\affr{10}8};
(-12,38)*{\copy\contrup};
%contraction - bot
(-12,-43.5)*{\afvjm{3}};
(-12,-38)*{\affr{34}8};
(-12,-38)*{\copy\contrdown};
(18,-46)*{\afaiuex{}{}{}{}{}{}31};
(24,-38)*{\affr{10}8};
(24,-38)*{\copy\contrdown};
(12,-38)*{\affr{10}8};
(12,-38)*{\copy\contrdown};
%---------------------
(4,-20)="D";
(0,-10)="Dhalf";
%----------------
%%first
(-20,0)="B";
% cocontractions
"B"-"D"-"D"-(-12,7)="A";
"A"+(4,-4)*{\afcjrm{16}{10}};
"A"+(8,-4)*{\afcjrm{16}{10}};
"A"+(12,-4)*{\afcjrm{16}{10}};
"A"+"Dhalf"+"Dhalf"+(4,-9)*{\afvjm{40}};
"A"+"Dhalf"+(0,-9)*{\afvjm{20}};
"A"+(-12,-4)*{\afvj{10}};
"A"+(-4,-4)*{\afcjr{8}{10}};
% contractions
"B"+"D"+"D"+(-12,7)="A";
"A"+(4,4)*{\afvjm{10}};
"A"+(0,4)-"Dhalf"*{\afvjm{30}};
"A"+(-4,4)-"Dhalf"-"Dhalf"*{\afvjm{50}};
"A"-(-20,-4)*{\afcjl{24}{10}};
"A"-(-28,-4)*{\afcjl{32}{10}};
%---
% top boxes
"B"-"D"="A";
"A"+( 0,-8)*{\afawu{}{}{}{}{}};
"A"+( 0, 0)*{\affr{10}{8}};
"A"+( 2, 2)*{\aflabelright{\phi_1}};
% join one
"A"+(4,-10)*{\afvjcol{12}{Red}};
% middle boxes
"B"="A";
"A"+(-4, 8)*{\afawd{}{}{}{}{}};
"A"+( 4,-8)*{\afawu{}{}{}{}{}};
"A"+( 0, 0)*{\affr{10}{8}};
"A"+( 2, 2)*{\aflabelright{\phi_1}};
% join two
"A"+(0,-10)*{\afvjcol{12}{Red}};
% bottom boxes
"B"+"D"="A";
"A"+(0, 8)*{\afawd{}{}{}{}{}};
"A"+(0, 0)*{\affr{10}{8}};
"A"+( 2, 2)*{\aflabelright{\phi_1}};
%----------------
%%second
(0,0)="B";
% cocontractions
"B"-"D"-"D"-(-12,7)="A";
"A"+(0,-4)*{\afcjrm8{10}};
"A"+(4,-4)*{\afcjrm8{10}};
"A"+(8,-4)*{\afcjrm8{10}};
"A"+"Dhalf"+"Dhalf"+(4,-9)*{\afvjm{40}};
"A"+"Dhalf"+(0,-9)*{\afvjm{20}};
"A"+(-20,-4)*{\afcjl{16}{10}};
"A"+(-12,-4)*{\afcjl{8}{10}};
% contractions
"B"+"D"+"D"+(-12,7)="A";
"A"-(0,-4)*{\afcjrm8{10}};
"A"-(4,-4)*{\afcjrm8{10}};
"A"-(8,-4)*{\afcjrm8{10}};
"A"-"Dhalf"-"Dhalf"-(4,-9)*{\afvjm{40}};
"A"-"Dhalf"-(0,-9)*{\afvjm{20}};
"A"-(-20,-4)*{\afcjl{16}{10}};
"A"-(-12,-4)*{\afcjl{8}{10}};
%---
% top boxes
"B"-"D"="A";
"A"+( 0,-8)*{\afawu{}{}{}{}{}};
"A"+( 0, 0)*{\affr{10}{8}};
"A"+( 2, 2)*{\aflabelright{\phi_1}};
% join one
"A"+(4,-10)*{\afvjcol{12}{Red}};
% middle boxes
"B"="A";
"A"+(-4, 8)*{\afawd{}{}{}{}{}};
"A"+( 4,-8)*{\afawu{}{}{}{}{}};
"A"+( 0, 0)*{\affr{10}{8}};
"A"+( 2, 2)*{\aflabelright{\phi_1}};
% join two
"A"+(0,-10)*{\afvjcol{12}{Red}};
% bottom boxes
"B"+"D"="A";
"A"+(0, 8)*{\afawd{}{}{}{}{}};
"A"+(0, 0)*{\affr{10}{8}};
"A"+( 2, 2)*{\aflabelright{\phi_1}};
%----------------
%%third
(20,0)="B";
% cocontractions
"B"-"D"-"D"-(-12,7)="A";
"A"+"Dhalf"+"Dhalf"+(4,-4)*{\afvjm{50}};
"A"+"Dhalf"+(0,-4)*{\afvjm{30}};
"A"+(-4,-4)*{\afvjm{10}};
"A"+(-20,-4)*{\afcjl{24}{10}};
"A"+(-28,-4)*{\afcjl{32}{10}};
% contractions
"B"+"D"+"D"+(-12,7)="A";
"A"-(4,-4)*{\afcjrm{16}{10}};
"A"-(8,-4)*{\afcjrm{16}{10}};
"A"-(12,-4)*{\afcjrm{16}{10}};
"A"-"Dhalf"-"Dhalf"-(4,-9)*{\afvjm{40}};
"A"-"Dhalf"-(0,-9)*{\afvjm{20}};
"A"-(-12,-4)*{\afvj{10}};
"A"-(-4,-4)*{\afcjr{8}{10}};
%---
% top boxes
"B"-"D"="A";
"A"+( 0,-8)*{\afawu{}{}{}{}{}};
"A"+( 0, 0)*{\affr{10}{8}};
"A"+( 2, 2)*{\aflabelright{\phi_1}};
% join one
"A"+(4,-10)*{\afvjcol{12}{Red}};
% middle boxes
"B"="A";
"A"+(-4, 8)*{\afawd{}{}{}{}{}};
"A"+( 4,-8)*{\afawu{}{}{}{}{}};
"A"+( 0, 0)*{\affr{10}{8}};
"A"+( 2, 2)*{\aflabelright{\phi_1}};
% join two
"A"+(0,-10)*{\afvjcol{12}{Red}};
% bottom boxes
"B"+"D"="A";
"A"+(0, 8)*{\afawd{}{}{}{}{}};
"A"+(0, 0)*{\affr{10}{8}};
"A"+( 2, 2)*{\aflabelright{\phi_1}};
}
\]
\[
\atomicflow
{
(12,-52)="D";
% cocontractions
(18,-11)="A";
%
"A"+(6,5.5)*{\afvjm3};
"A"+(6,0)*{\affr{34}8};
"A"+(6,0)*{\copy\contrup};
"A"+(2,-30)*{\afvjm{52}};
"A"+(6,-30)*{\afvjm{52}};
"A"+(10,-34)*{\afvjm{60}};
"A"+(14,-56)*{\afvjm{104}};
"A"+(18,-56)*{\afvjm{104}};
"A"+(22,-60)*{\afvjm{112}};
% === BOX ONE ===
(0,-27)="A";
%-
"A"+( -6,24)*{\afaidex{}{}{}{}{}{}31};
%-
"A"+(-12,16)*{\affr{10}8};
"A"+(-12,16)*{\copy\contrup};
"A"+(  0,16)*{\affr{10}8};
"A"+(  0,16)*{\copy\contrup};
%-
"A"+(-16,8)*{\afvj8};
"A"+(-8,8)*{\afcjr88};
"A"+(0,8)*{\afcjrm{16}8};
%
"A"+(-8,8)*{\afcjl88};
"A"+(0,8)*{\afvj8};
"A"+(8,8)*{\afcjrm88};
%
"A"+(0,8)*{\afcjl{16}8};
"A"+(8,8)*{\afcjl88};
"A"+(16,8)*{\afvjm8};
%-
"A"+(-12,0)*{\affr{10}8};
"A"+(0,0)*{\affr{10}8};
"A"+(12,0)*{\affr{10}8};
"A"+(-10,2)*{\aflabelright{\phi_2}};
"A"+(2,2)*{\aflabelright{\phi_2}};
"A"+(14,2)*{\aflabelright{\phi_2}};
%-
"A"+(-8,-8)*{\afcjl88};
"A"+(0,-8)*{\afcjlcol{16}8{Red}};
%-
"A"+(-8,-8)*{\afcjrm88};
"A"+(0,-8)*{\afvj8};
"A"+(8,-8)*{\afcjlcol88{Red}};
%
"A"+(0,-8)*{\afcjrm{16}8};
"A"+(8,-8)*{\afcjr88};
"A"+(16,-8)*{\afvjcol8{Red}};
%
"A"+(  0,-16)*{\affr{10}8};
"A"+(  0,-16)*{\copy\contrdown};
"A"+( 12,-16)*{\affr{10}8};
"A"+( 12,-16)*{\copy\contrdown};
%---
"A"+(0,-24)*{\afawu{}{}{}{}};
"A"+(12,-26)*{\afvjcol{12}{Red}};
% === BOX TWO ===
"A"+"D"="A";
%-
"A"+(-12,24)*{\afawd{}{}{}{}};
%-
"A"+(-12,16)*{\affr{10}8};
"A"+(-12,16)*{\copy\contrup};
"A"+(  0,16)*{\affr{10}8};
"A"+(  0,16)*{\copy\contrup};
%-
"A"+(-16,8)*{\afvj8};
"A"+(-8,8)*{\afcjrcol88{Red}};
"A"+(0,8)*{\afcjrm{16}8};
%
"A"+(-8,8)*{\afcjl88};
"A"+(0,8)*{\afvjcol8{Red}};
"A"+(8,8)*{\afcjrm88};
%
"A"+(0,8)*{\afcjl{16}8};
"A"+(8,8)*{\afcjlcol88{Red}};
%-
"A"+(-12,0)*{\affr{10}8};
"A"+(0,0)*{\affr{10}8};
"A"+(12,0)*{\affr{10}8};
"A"+(-10,2)*{\aflabelright{\phi_2}};
"A"+(2,2)*{\aflabelright{\phi_2}};
"A"+(14,2)*{\aflabelright{\phi_2}};
%-
"A"+(-8,-8)*{\afcjlcol88{Red}};
"A"+(0,-8)*{\afcjl{16}8};
%-
"A"+(-8,-8)*{\afcjrm88};
"A"+(0,-8)*{\afvjcol8{Red}};
"A"+(8,-8)*{\afcjl88};
%
"A"+(0,-8)*{\afcjrm{16}8};
"A"+(8,-8)*{\afcjrcol88{Red}};
"A"+(16,-8)*{\afvj8};
%
"A"+(  0,-16)*{\affr{10}8};
"A"+(  0,-16)*{\copy\contrdown};
"A"+( 12,-16)*{\affr{10}8};
"A"+( 12,-16)*{\copy\contrdown};
%---
"A"+(12,-24)*{\afawu{}{}{}{}};
"A"+(0,-26)*{\afvjcol{12}{Red}};
% === BOX THREE ===
"A"+"D"="A";
%-
"A"+(  0,24)*{\afawd{}{}{}{}};
%-
"A"+(-12,16)*{\affr{10}8};
"A"+(-12,16)*{\copy\contrup};
"A"+(  0,16)*{\affr{10}8};
"A"+(  0,16)*{\copy\contrup};
%-
"A"+(-16,8)*{\afvjcol8{Red}};
"A"+(-8,8)*{\afcjr88};
"A"+(0,8)*{\afcjrm{16}8};
%
"A"+(-8,8)*{\afcjlcol88{Red}};
"A"+(0,8)*{\afvj8};
"A"+(8,8)*{\afcjrm88};
%
"A"+(0,8)*{\afcjlcol{16}8{Red}};
"A"+(8,8)*{\afcjl88};
%-
"A"+(-12,0)*{\affr{10}8};
"A"+(0,0)*{\affr{10}8};
"A"+(12,0)*{\affr{10}8};
"A"+(-10,2)*{\aflabelright{\phi_2}};
"A"+(2,2)*{\aflabelright{\phi_2}};
"A"+(14,2)*{\aflabelright{\phi_2}};
%-
"A"+(-16,-8)*{\afvjm8};
"A"+(-8,-8)*{\afcjl88};
"A"+(0,-8)*{\afcjl{16}8};
%-
"A"+(-8,-8)*{\afcjrm88};
"A"+(8,-8)*{\afcjl88};
"A"+(0,-8)*{\afvj8};
%
"A"+(0,-8)*{\afcjrm{16}8};
"A"+(8,-8)*{\afcjr88};
"A"+(16,-8)*{\afvj8};
%
"A"+(  0,-16)*{\affr{10}8};
"A"+(  0,-16)*{\copy\contrdown};
"A"+( 12,-16)*{\affr{10}8};
"A"+( 12,-16)*{\copy\contrdown};
%-
"A"+(  6,-24)*{\afaiuex{}{}{}{}{}{}31};
% contractions
"A"+(-20,-16)="A";
"A"+(-20,60)*{\afvjm{112}};
"A"+(-16,56)*{\afvjm{104}};
"A"+(-12,56)*{\afvjm{104}};
"A"+(-8,34)*{\afvjm{60}};
"A"+(-4,30)*{\afvjm{52}};
"A"+( 0,30)*{\afvjm{52}};
"A"+(-4,0)*{\affr{34}8};
"A"+(-4,0)*{\copy\contrdown};
"A"+(-4,-5.5)*{\afvjm3};
}
\]
\[
\atomicflow{
(0,34.5)*{\afvjm3};
(0,29)*{\affr{82}8};
(0,29)*{\copy\contrup};
%
(0,-29)*{\affr{82}8};
(0,-29)*{\copy\contrdown};
(0,-34.5)*{\afvjm3};
%-------------------
(30,0)="B";
%---------------
(0,0)-"B"="A";
"A"+(-10,14.5)*{\afvjm{21}};
"A"+(0,14.5)*{\afvjm{21}};
"A"+(10,14.5)*{\afvjm{21}};
%---
"A"+(-10,0)*{\affr88};
"A"+( -9,2)*{\aflabelright\psi};
"A"+(  0,0)*{\affr88};
"A"+(  1,2)*{\aflabelright\psi};
"A"+( 10,0)*{\affr88};
"A"+( 11,2)*{\aflabelright\psi};
%---
"A"+(-10,-14.5)*{\afvjm{21}};
"A"+(0,-14.5)*{\afvjm{21}};
"A"+(10,-14.5)*{\afvjm{21}};
%---------------
(0,0)="A";
%---
"A"+(-10,14.5)*{\afvjm{21}};
"A"+(0,14.5)*{\afvjm{21}};
"A"+(10,14.5)*{\afvjm{21}};
%---
"A"+(-10,0)*{\affr88};
"A"+( -9,2)*{\aflabelright\psi};
"A"+(  0,0)*{\affr88};
"A"+(  1,2)*{\aflabelright\psi};
"A"+( 10,0)*{\affr88};
"A"+( 11,2)*{\aflabelright\psi};
%---
"A"+(-10,-14.5)*{\afvjm{21}};
"A"+(0,-14.5)*{\afvjm{21}};
"A"+(10,-14.5)*{\afvjm{21}};
%---------------
"A"+"B"="A";
%---
"A"+(-10,14.5)*{\afvjm{21}};
"A"+(0,14.5)*{\afvjm{21}};
"A"+(10,14.5)*{\afvjm{21}};
%---
"A"+(-10,0)*{\affr88};
"A"+( -9,2)*{\aflabelright\psi};
"A"+(  0,0)*{\affr88};
"A"+(  1,2)*{\aflabelright\psi};
"A"+( 10,0)*{\affr88};
"A"+( 11,2)*{\aflabelright\psi};
%---
"A"+(-10,-14.5)*{\afvjm{21}};
"A"+(0,-14.5)*{\afvjm{21}};
"A"+(10,-14.5)*{\afvjm{21}};
}\quad.
\]
By comparing the copies of $\phi_1$ with the copies of $\phi_2$ in $\Norm_2(\Phi,\phi_1,\phi_2)$ we can see why the procedure is non-confluent. We could trivially change our procedure to make the subflows more similar by permuting the weakening (resp., coweakening) vertices down (resp., up) in the second subflow. However, the subflows marked in red will still differ.
\end{example} 
%===========================================
\section{Conclusion}

\bibliographystyle{alpha}
\bibliography{biblio}

\end{document}