Lutz Straßburger

A System of Interaction and Structure IV: The Exponentials and Decomposition

Keywords: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic-proof theory Deep Inference, Calculus of Structures, Linear Logic, Noncommutativity Decomposition, Cut Elimination, !-?-Flow-Graphs

We study a system, called NEL, which is the mixed commutative/non-commutative linear logic BV augmented with linear logic's exponentials. Equivalently, NEL is MELL augmented with the non-commutative self-dual connective seq. In this paper, we show a basic compositionality property of NEL, which we call decomposition. This result leads to a cut-elimination theorem, which is proved in the next paper of this series. To control the induction measure for the theorem, we rely on a novel technique that extracts from NEL proofs the structure of exponentials, into what we call !-?-Flow-Graphs.

INTRODUCTION

This is the fourth in a series of papers dedicated to the proof theory of a self-dual non-commutative operator, called seq, in the context of linear logic.

The first paper "A System of Interaction and Structure" [START_REF] Guglielmi | A system of interaction and structure[END_REF]] introduced seq in the context of multiplicative linear logic. The resulting logic is called BV. The proof system for BV is presented in the formalism called the calculus of structures, which is the simplest formalism in the methodology of deep inference. In fact, deep inference was born precisely for giving BV a normalization theory.

In the second paper "A System of Interaction and Structure II: The Need for Deep Inference" [Tiu 2006], Alwen Tiu shows that deep inference is necessary to obtain analyticity for BV. In other words, traditional Gentzen proof theory is not sufficient to deal with seq.

The third paper, currently being elaborated, explores the connection between BV and pomset logic [START_REF] Retoré | Pomset logic: A non-commutative extension of classical linear logic[END_REF]].

This fourth paper, and the fifth paper "A System of Interaction and Structure V: The Exponentials and Splitting" [START_REF] Guglielmi | A system of interaction and structure V: The exponentials and splitting[END_REF]] are devoted to the proof theory of system BV when it is enriched with linear logic's exponentials. We call NEL (non-commutative exponential linear logic) the resulting system. We can also consider NEL as MELL (multiplicative exponential linear logic [START_REF] Girard | Linear logic[END_REF]]) plus seq. NEL, which was first presented in [START_REF] Guglielmi | A non-commutative extension of MELL[END_REF], is conservative over BV and over MELL augmented by the mix and nullary mix rules [START_REF] Fleury | The mix rule[END_REF][START_REF] Retoré | Réseaux et séquents ordonnés[END_REF]; [START_REF] Abramsky | Games and full completeness for multiplicative linear logic[END_REF]. Note that, like BV, NEL cannot be analytically expressed outside deep inference. System NEL can be immediately understood by anybody acquainted with the sequent calculus, and is aimed at the same range of applications as MELL, but it offers, of course, explicit sequential composition.

NEL is especially interesting because it is Turing-complete [Straßburger 2003c]. The complexity of MELL is currently unknown, but MELL is widely conjectured to be decidable. If that was the case, then the line towards Turing-completeness would clearly be crossed by seq, which, in fact, has been interpreted already as an effective mechanism to structure a Turing machine tape. This is something that MELL, which is fully commutative, apparently cannot do.

This paper is devoted to the decomposition theorem. Together with the splitting theorem in [START_REF] Guglielmi | A system of interaction and structure V: The exponentials and splitting[END_REF] it immediately yields cut-elimination, which will be claimed in [START_REF] Guglielmi | A system of interaction and structure V: The exponentials and splitting[END_REF].

Decomposition (which was first pioneered in [START_REF] Guglielmi | Non-commutativity and MELL in the calculus of structures[END_REF]Straßburger 2003b] for BV and MELL) is as follows: we can transform every NEL derivation into an equivalent one, composed of eleven derivations carried into eleven disjoint subsystems of NEL. This means that we can study small subsystems of NEL in isolation and then compose them together with considerable more freedom than in the sequent calculus, where, for example, contraction can not be isolated in a derivation. Decomposition is made available in the calculus of structures by exploiting the top-down symmetry of derivations that is typical of deep inference. Such a result is unthinkable in formalisms lacking locality, like Gentzen systems.

The technique by which we prove the result is an evolution and simplification of a technique that was first developed in [Straßburger 2003b] for MELL, but that would not work unmodified in the presence of seq. In fact, seq makes matters more complicated, due to similar phenomena to those unveiled by Tiu [Tiu 2006], and that make seq intractable for Gentzen methods.

Some of the main results of this paper have already been presented, without proof, in [START_REF] Guglielmi | A non-commutative extension of MELL[END_REF].

THE SYSTEM

We define the language for system NEL and its variants, as an extension of the language for BV, defined in [START_REF] Guglielmi | A system of interaction and structure[END_REF]]. Intuitively, [S 1 • • • S h ] corresponds to a sequent ⊢ S 1 , . . . , S h in linear logic, whose formulae are essentially connected by pars, subject to commutativity (and associativity). The structure (S 1 • • • S h ) corresponds to the associative and commutative tensor connection of S 1 , . . . , S h . The structure S 1 ⊳ • • • ⊳ S h is associative and non-commutative: this corresponds to the new logical connective, called seq, that we add to those of MELL.1 Definition 2.1. There are countably many positive and negative atoms. They, positive or negative, are denoted by a, b, . . . . Structures are denoted by S, P , Q, 1. Basic equations for the syntactic equivalence = R, T , U , V , W , X and Z. The structures of the language NEL are generated by

• 3 Associativity [ R [ T ] U ] = [ R T U ] ( R ( T ) U ) = ( R T U ) R ⊳ T ⊳ U = R ⊳ T ⊳ U Commutativity [ R T ] = [ T R] ( R T ) = ( T R) Unit [• R] = [ R] (• R) = ( R) • ⊳ R = R R ⊳ • = R Singleton [R] = (R) = R = R Negation • = • [R 1 • • • R h ] = ( R1 • • • Rh ) (R 1 • • • R h ) = [ R1 • • • Rh ] R 1 ⊳ • • • ⊳ R h = R1 ⊳ • • • ⊳ Rh ?R = ! R !R = ? R R = R Contextual Closure if R = T then S{R} = S{T } Fig.
S ::= a | • | [ S • • • S >0 ] | ( S • • • S >0 ) | S ⊳ • • • ⊳ S >0 | ?S | !S | S ,
where •, the unit, is not an atom and S is the negation of the structure S. Structures with a hole that does not appear in the scope of a negation are denoted by S{ }. The structure R is a substructure of S{R}, and S{ } is its context. We simplify the indication of context in cases where structural parentheses fill the hole exactly: for example, S [R T ] stands for S{[R T ]}.

Structures come with equational theories establishing some basic, decidable algebraic laws by which structures are indistinguishable. These are analogous to the laws of associativity, commutativity, idempotency, and so on, usually imposed on sequents. The difference is that we merge the notions of formula and sequent, and we extend the equations to formulae. The structures of the language NEL are equivalent modulo the relation =, defined in Figure 1. There, R, T and U stand for finite, non-empty sequences of structures (elements of the sequences are separated by , ⊳ , or , as appropriate in the context).2 Definition 2.2. An (inference) rule is any scheme

T ρ R ,
where ρ is the name of the rule, T is its premise and R is its conclusion; R or T , but not both, may be missing. A (proof ) system, denoted by S , is a set of rules. A derivation in a system S is a finite chain of instances of rules of S , and is denoted by ∆; a derivation can consist of just one structure. The topmost structure in a derivation is called its premise; the bottommost structure is called conclusion. A derivation ∆ whose premise is T , conclusion is R, and whose rules are in S is denoted by

T S ∆ R .
The typical inference rules are of the kind

S{T } ρ S{R} .
This rule scheme ρ specifies that if a structure matches R, in a context S{ }, it can be rewritten as specified by T , in the same context S{ } (or vice versa if one reasons top-down). A rule corresponds to implementing in the deductive system any axiom T ⇒ R, where ⇒ stands for the implication we model in the system, in our case linear implication. The case where the context is empty corresponds to the sequent calculus. For example, the linear logic sequent calculus rule

⊢ A, Φ ⊢ B, Ψ ⊢ A B, Φ, Ψ
could be simulated easily in the calculus of structures by the rule

(Γ [A Φ] [B Ψ]) ′ (Γ [(A B) Φ Ψ]) ,
where Φ and Ψ stand for multisets of formulae or their corresponding par structures.

The structure Γ stands for the tensor structure of the other hypotheses in the derivation tree. More precisely, any sequent calculus derivation

⊢ Γ1 • • • ⊢ Γi-1 ⊢ A, Φ ⊢ B, Ψ ⊢ A B, Φ, Ψ ⊢ Γi+1 • • • ⊢ Γ h l l l l l l l l l l l l l l l l l R R R R R R R R R R R R R R R R R ∆ ⊢ Σ
containing the rule can be simulated by

(Γ ′ 1 . . . Γ ′ i-1 [A ′ Φ ′ ] [B ′ Ψ ′ ] Γ ′ i+1 . . . Γ ′ h ) ′ (Γ ′ 1 . . . Γ ′ i-1 [(A ′ B ′ ) Φ ′ Ψ ′ ] Γ ′ i+1 . . . Γ ′ h ) ∆ ′ Σ ′ ,
in the calculus of structures, where Γ ′ j , A ′ , B ′ , Φ ′ , Ψ ′ , ∆ ′ and Σ ′ are obtained from their counterparts in the sequent calculus by the obvious translation. This means that by this method every system in the one-sided sequent calculus can be ported trivially to the calculus of structures.

Of course, in the calculus of structures, rules could be used as axioms of a generic Hilbert system, where there is no special, structural relation between T and R: then all the good proof theoretical properties of sequent systems would be lost. We will

• 5 be careful to design rules in a way that is conservative enough to allow us to prove cut elimination, and such that they possess the subformula property.

In our systems, rules come in pairs,

S{T } ρ↓ S{R}
(down version) and

S{ R} ρ↑ S{ T } (up version) .
Sometimes rules are self-dual, i.e., the up and down versions are identical, in which case we omit the arrows. This duality derives from the duality between T ⇒ R and R ⇒ T , where ⇒ is the implication and (•) the negation of the logic. In the case of NEL these are linear implication and linear negation. We will be able to get rid of the up rules without affecting provability-after all, T ⇒ R and R ⇒ T are equivalent statements in many logics. Remarkably, the cut rule reduces into several up rules, and this makes for a modular decomposition of the cut elimination argument because we can eliminate up rules one independently from the other.

Let us now define system NEL by starting from an up-down symmetric variation, that we call SNEL. It is made by two sub-systems that we will call conventionally interaction and structure. The interaction fragment deals with negation, i.e., duality. It corresponds to identity and cut in the sequent calculus. In our calculus these rules become mutually top-down symmetric and both can be reduced to their atomic counterparts.

The structure fragment corresponds to logical and structural rules in the sequent calculus; it defines the logical connectives. Differently from the sequent calculus, the connectives need not be defined in isolation, rather complex contexts can be taken into consideration. In the following system we consider pairs of logical connectives, one inside the other.

Definition 2.3. In Figure 2, system SNEL (symmetric non-commutative exponential linear logic) is shown. The rules ai↓, ai↑, s, q↓, q↑, p↓, p↑, e↓, e↓, w↓, w↑, b↓, b↑, g↓, and g↑ are called respectively atomic interaction, atomic cut, switch, seq, coseq, promotion, copromotion, empty, coempty, weakening, coweakening, absorption, coabsorption, digging, and codigging. The down fragment of SNEL is {ai↓, s, q↓, p↓, e↓, w↓, b↓, g↓}, the up fragment is {ai↑, s, q↑, p↑, e↑, w↑, b↑, g↑}.

There is a straightforward two-way correspondence between structures not involving seq and formulae of MELL: for example

![(?a b) c ! d] corresponds to !((?a b) c ⊥ !d ⊥ ) ,
and vice versa. Units are mapped into • (since 1 ≡ ⊥, when mix and mix0 are added to MELL). System SNEL is just the merging of systems SBV (which is the symmetric version of BV) and SELS (which is the symmetric presentation of MELL in the calculus of structures) shown in [START_REF] Guglielmi | A system of interaction and structure[END_REF][START_REF] Guglielmi | Non-commutativity and MELL in the calculus of structures[END_REF]Straßburger 2003b;2003a]; there one can find details on the correspondence between our systems and linear logic. 3 The rules s, q↓ and q↑ are the same as in pomset logic viewed as a calculus of cographs [START_REF] Retoré | Pomset logic as a calculus of directed cographs[END_REF]].

S{•} ai↓ S [a ā] S(a ā) ai↑ S{•} S([R U ] T ) s S [(R T ) U ] S [R U ] ⊳ [T V ] q↓ S [ R ⊳ T U ⊳ V ] S( R ⊳ U T ⊳ V ) q↑ S (R T ) ⊳ (U V ) S{![R T ]} p↓ S [!R ?T ] S(?R !T ) p↑ S{?(R T )} S{•} e↓ S{!•} S{?•} e↑ S{•} S{•} w↓ S{?R} S{!R} w↑ S{•} S [?R R] b↓ S{?R} S{!R} b↑ S(!R R) S{??R} g↓ S{?R} S{!R} g↑ S{!!R} Fig. 2. System SNEL
All equations are typical of a sequent calculus presentation, save those for units and contextual closure. Contextual closure just corresponds to equivalence being a congruence, it is a necessary ingredient of the calculus of structures. All other equations can be removed and replaced by rules (see, e.g., [START_REF] Straßburger | A system of interaction and structure II: The need for deep inference[END_REF]), as in the sequent calculus. This might prove necessary for certain applications. For our purposes, this setting makes for a much more compact presentation, at a more effective abstraction level.

Negation is involutive and can be pushed to atoms; it is convenient always to imagine it directly over atoms. Please note that negation does not swap arguments of seq, as happens in the systems of Yetter [START_REF] Yetter | Quantales and (noncommutative) linear logic[END_REF]] and Abrusci-Ruet [START_REF] Abrusci | Non-commutative logic I: The multiplicative fragment[END_REF]. The unit • is self-dual and common to par, times and seq. One may think of it as a convenient way of expressing the empty sequence. Rules become very flexible in the presence of the unit. For example, the following notable derivation 2003b] (see also [Straßburger 2003a]). From the viewpoint of provability, there is no difference between the two approaches, but certain properties of the system, in particular decomposition, can be demonstrated in a cleaner way. Also from the viewpoint of denotational semantics, our system is now more easily accessible. For example in coherence spaces [START_REF] Girard | Linear logic[END_REF] we do not have an isomorphism between !R and !!R.

• 7 is valid:

(a b) q↑ a ⊳ b q↓ [a b] ≡ (a b) = ( a ⊳ • • ⊳ b ) q↑ (a •) ⊳ (• b) = a ⊳ b = [a •] ⊳ [• b] q↓ [ a ⊳ • • ⊳ b ] = [a b]
.

The right-hand side above is just a complicated way of writing the left-hand side.

Using the "fake inference rule =" sometimes eases the reading of a derivation.

Remark 2.4. We will also use the following variants of the rules s, p↓, and p↑, which allows us to save some space by omitting the = rule:

S([U R] T ) s S [U (R T )] S(R [T U ]) s S [(R T ) U ] S(R [U T ]) s S [U (R T )] S{![T R]} p↓ S [?T !R] S(!T ?R) p↑ S{?(T R)}
Each inference rule in Figure 2 corresponds to a linear implication that is sound in MELL plus mix and mix0. For example, promotion corresponds to the implication !(R T ) ⊸ (!R ?T ). Notice that interaction and cut are atomic in SNEL; we can define their general versions as follows.

Definition 2.5. The following rules are called interaction and cut:

S{•} i↓ S [R R] and S(R R) i↑ S{•} ,
where R and R are called principal structures.

The sequent calculus cut rule

⊢ A, Φ ⊢ A ⊥ , Ψ cut ⊢ Φ, Ψ
is realized as

([A Φ] [ Ā Ψ]) s [([A Φ] Ā) Ψ] s [(A Ā) Φ Ψ] i↑ [Φ Ψ]
,

where Φ and Ψ stand for multisets of formulae or their corresponding par structures. Notice how the tree shape of derivations in the sequent calculus is realized by making use of tensor structures: in the derivation above, the premise corresponds to the two branches of the cut rule. For this reason, in the calculus of structures rules are allowed to access structures deeply nested into contexts. The cut rule in the calculus of structures can mimic the classical cut rule in the sequent calculus in its realization of transitivity, but it is much more general. We believe a good way of understanding it is thinking of the rule as being about lemmas in context. The sequent calculus cut rule generates a lemma which is valid in the most general context; the new cut rule does the same, but the lemma only affects the limited portion of structure that can interact with it.

Definition 2.6. A rule ρ is derivable in the system S if ρ / ∈ S and for every instance We easily get the next two propositions, which say: 1) The interaction and cut rules can be reduced into their atomic forms-note that in the sequent calculus it is possible to reduce interaction to atomic form, but not cut. 2) The cut rule is as powerful as the whole up fragment of the system, and vice versa.

Proposition 2.7. The rule i↓ is derivable in {ai↓, s, q↓, p↓, e↓}, and, dually, the rule i↑ is derivable in the system {ai↑, s, q↑, p↑, e↑}.

Proof. Induction on principal structures. We show the inductive cases for i↑:

S(P Q [ P Q]) s S(Q [(P P ) Q]) s S [(P P ) (Q Q)] i↑, i↑ S [• •] = S{•} S( P ⊳ Q P ⊳ Q ) q↑ S (P P ) ⊳ (Q Q) i↑, i↑ S • ⊳ • = S{•} S(?P ! P ) p↑ S{?(P P )} i↑ S{?•} e↑ S{•} .
The cases for i↓ are dual.

Note that in the proof above we tacitly used (for the sake of saving paper) another helpful notation: writing i↑, i↑ just means that two instances of i↑ applied one after the other, where the order does not matter.

Proposition 2.8. Each rule ρ↑ in SNEL is derivable in {i↓, i↑, s, ρ↓}, and, dually, each rule ρ↓ in SNEL is derivable in the system {i↓, i↑, s, ρ↑}.

Proof. Each instance

S{T } ρ↑ S{R}
can be replaced by

S{T } i↓ S(T [R R]) s S [R (T R)] ρ↓ S [R (T T )] i↑ S{R}
and dually.

In the calculus of structures, we call core the set of rules that is used to reduce interaction and cut to atomic form. We use the term hard core to denote the set of rules in the core other than atomic interaction/cut and empty/coempty. Rules that are not in the core are called non-core.

Definition 2.9. The core of SNEL is {ai↓, ai↑, s, q↓, q↑, p↓, p↑, e↓, e↑}, denoted by SNELc. The hard core, denoted by SNELh, is {s, q↓, q↑, p↓, p↑}, and the non-core is {w↓, w↑, b↓, b↑, g↓, g↑}.

System SNEL is up-down symmetric, and the properties we saw are also symmetric. Provability is an asymmetric notion: we want to observe the possible conclusions that we can obtain from a unit premise. We now break the up-down symmetry by adding an inference rule with no premise, and we join this logical axiom to the down fragment of SNEL.

• 9 •↓ • S{•} ai↓ S [a ā] S{•} e↓ S{!•} S([R U ] T ) s S [(R T ) U ] S [R U ] ⊳ [T V ] q↓ S [ R ⊳ T U ⊳ V ] S{![R T ]} p↓ S [!R ?T ]
Definition 2.10. System NEL is shown in Fig. 3, where the rule •↓ is called unit.

As an immediate consequence of Propositions 2.7 and 2.8 we get:

Proposition 2.11. NEL ∪ {i↑} and SNEL ∪ {•↓} are strongly equivalent.

Definition 2.12. A derivation with no premise is called a proof, denoted by Π. A system S proves R if there is in S a proof Π whose conclusion is R, written as

- S Π R .
We say that a rule ρ is admissible for the system S if ρ / ∈ S and for every proof

- S ∪ {ρ} Π R there is a proof - S Π ′ R
. Two systems are equivalent if they prove the same structures.

Except for ai↑ and w↑, all rules in the systems SNEL and NEL enjoy a kind of subformula property (which we treat as an asymmetric property, by going from conclusion to premise): premises are made of substructures of the conclusions. To get cut elimination, so as to have a system whose rules all enjoy the subformula property, we could just get rid of ai↑ and w↑, by proving their admissibility for the other rules. But we can do more than that: the whole up fragment of SNEL (except for s which also belongs to the down fragment) is admissible. This entails a modular scheme for proving cut elimination. We state here the cut elimination theorem, but its complete proof is shown in the accompanying paper [START_REF] Guglielmi | A system of interaction and structure V: The exponentials and splitting[END_REF].

Theorem 2.13. System NEL is equivalent to SNEL ∪ {•↓}.

Corollary 2.14. The rule i↑ is admissible for system NEL.

Any linear implication T ⊸ R, i.e., [ T R], is related to derivability by:

• Lutz Straßburger and Alessio Guglielmi Corollary 2.15. For any two structures T and R, we have

T SNEL R if and only if - NEL [ T R] .
Proof. For the first direction, perform the following transformations:

T SNEL ∆ R 1 ; [ T T ] SNEL ∆ ′ [ T R] 2 ; •↓ • i↓ [ T T ] SNEL ∆ ′ [ T R] 3 ; - NEL Π [ T R] .
In the first step we replace each structure S occurring inside ∆ by [ T S ], or, in other words, the derivation ∆ ′ is obtained by putting ∆ into the context [ T { }]. This is then transformed into a proof by adding an instance of i↓ and •↓. Then we apply Proposition 2.7 and cut elimination (Theorem 2.13) to obtain a proof in system NEL. For the other direction, we proceed as follows:

- NEL Π [ T R] ; • NEL \ {•↓} ∆ [ T R] ; T NEL \ {•↓} ∆ ′ (T [ T R]) s [(T T ) R] i↑ R ; T SNEL R ,
where the first two steps are trivial, and the last one is an application of Proposition 2.7.

It is easy to prove that system NEL is a conservative extension of BV and of MELL plus mix and mix0 (see [START_REF] Guglielmi | A system of interaction and structure[END_REF]Straßburger 2003a]). The locality properties shown in [START_REF] Guglielmi | Non-commutativity and MELL in the calculus of structures[END_REF]Straßburger 2003b] still hold in this system, of course. In particular, the promotion rule is local, as opposed to the same rule in the sequent calculus.

DECOMPOSITION

The new top-down symmetry of derivations in the calculus of structures allows us to study properties that are not observable in the sequent calculus. The most remarkable results so far are decomposition theorems. In general, a decomposition theorem says that a given system S can be divided into n pairwise disjoint subsystems S 1 , . . . , S n such that every derivation ∆ in system S can be rearranged as composition of n derivations ∆ 1 , . . . , ∆ n , where ∆ i uses only rules of S i , for every 1 ≤ i ≤ n.

System SNEL can be decomposed into eleven subsystems, and there are many different possibilities to transform a derivation into eleven subderivations. We state here only four of them, but, due to the modular proof, the others are evident. For simplicity we will in the following call the four statements first, second, third, and fourth decomposition (from left to right). The fourth decomposition is crucial for the cut elimination proof in [START_REF] Guglielmi | A system of interaction and structure V: The exponentials and splitting[END_REF].

Apart from a decomposition into eleven subsystems, the first and the second decomposition can also be read as a decomposition into three subsystems that could be called creation, merging and destruction. In the creation subsystem, each rule increases the size of the structure; in the merging system, each rule does some rearranging of substructures, without changing the size of the structures; and in the destruction system, each rule decreases the size of the structure. Here, the size of the structure incorporates not only the number of atoms in it, but also the modality-depth for each atom. In a decomposed derivation, the merging part is in the middle of the derivation, and (depending on your preferred reading of a derivation) the creation and destruction are at the top and at the bottom, as shown in the left of Figure 4. In system SNEL the merging part contains the rules s, q↓, q↑, p↓ and p↑, which coincides with the hard core. In the top-down reading of a derivation, the creation part contains the rules e↓, g↑, b↑, w↓ and ai↓, and the destruction part consists of e↑, g↓, b↓, w↑ and ai↑. In the bottom-up reading, creation and destruction are exchanged. Note that this kind of decomposition (creation, merging, destruction) is quite typical for logical systems presented in the calculus of structures, and is not restricted to system SNEL. It holds, for example, also for systems SBV and SELS [START_REF] Guglielmi | Non-commutativity and MELL in the calculus of structures[END_REF]Straßburger 2003b], for classical logic [START_REF] Brünnler | A local system for classical logic[END_REF], and for full propositional linear logic [START_REF] Straßburger | A local system for linear logic[END_REF]].

The third decomposition allows a separation between hard core and noncore of the system, such that the up fragment and the down fragment of the noncore are not merged, as it is the case in the first and second decomposition. More precisely, we can separate the seven subsystems shown in the middle of Figure 4. The fourth decomposition is even stronger in this respect: it allows a complete separation between core and noncore, as shown on the right of Figure 4. This kind of decomposition is usually more difficult to achieve than the decomposition into creation-merging-destruction. In fact, it is not known whether it holds for full linear logic. Furthermore, the separation between non-core up and non-core down has not been achieved in [Straßburger 2003b] for system SELS. But it is easy to see how the proof in this paper can be adapted to the case of system SELS presented in [Straßburger 2003b]. For classical logic such a decomposition can be proved by using the cut-elimination result for the sequent calculus LK together with the results in [START_REF] Brünnler | Deep inference and its normal form of derivations[END_REF]]. But there is no known direct proof in the calculus of structures.

This decomposition into noncore-up, core, and noncore-down also plays a crucial rule for the cut elimination argument in [START_REF] Guglielmi | A system of interaction and structure V: The exponentials and splitting[END_REF]. Recall that cut elimination means to get rid of the entire up-fragment. Because of the decomposition, the elimination of the non-core up-fragment is now trivial. Furthermore, recall that for cut elimination in the sequent calculus, the most problematic cases are usually the ones where cut interacts with rules like contraction and weakening, and that in our system these rules appear as the non-core down rules. In the fourth decomposition these are below the actual cut rules (i.e., the core up rules, cf. Propositions 2.7, 2.8, and 2.11) and can therefore no longer interfere with the cut elimination. This considerably simplifies our cut elimination argument in [START_REF] Guglielmi | A system of interaction and structure V: The exponentials and splitting[END_REF]]. However, it is well-known that there is no free lunch. We cannot expect that the proof of the decomposition theorem is trivial. At least, we have to expect problems when the non-core rules (which in case of SNEL do all deal with the modalities ! and ?) do interact with the rules p↓ and p↑ (which are the only core rules that properly deal with ! and ?). The good news is that these are indeed the only cases where the proof of the decomposition theorem becomes problematic.

• 13 T SNEL R 1 ----→ ↑
We will now continue with a very brief sketch of the proof and in the remainder of this paper we will fill in the details.

Proof of Theorem 3.1 (Sketch). The third and fourth decomposition are obtained via the five steps shown in Figure 5, where S 1 = SNEL \ {e↓, e↑} and S 2 = {ai↓, ai↑} ∪ SNELh. The first and second decomposition are reached as shown in Figure 6, where S 3 = {ai↓, ai↑, w↓, w↑} ∪ SNELh. In these figures we also indicated which lemmas are used for achieving which step in the decomposition. Some explanation: Step 1 is performed via a rather simple rule permutation. The rule e↓ is permuted up in the derivation, and the rule e↑ is permuted down via the dual procedure. The concept of permuting rules in the calculus of structures is explained in more detail in Section 4.

Step 2 is the most critical one. In some sense it can also be considered as a simple rule permutation. However, contrary to Step 1, it is not obvious at all that Step 2 does terminate: while permuting g↑, b↑, and w↑ up, new instances of g↓, b↓, and w↓ are introduced, and vice versa. For showing termination, we introduce in Section 5.1 the concept of !-?-flow-graph. Steps 3, 4 and 5 are again rather simple rule permutations and are detailed out in Section 4 as well. Steps 6 and 8 are essentially the same as Steps 1-3 and 5 with the only difference that the rules w↑ and w↓ do not need attention. Steps 7 and 9 are only slight variations of each other and are not more complicated than Step 4. They are also done in Section 4. One last remark: Treating the rules g↑, b↑, w↑ together in Step 2 and separating them afterwards in Step 3 has been done on purpose.

Treating them separately from the very beginning would not give termination in the general case.

Remark 3.2. None of the four decompositions relies on the presence of mix nor nullary mix. All decompositions presented here work equally well for MELL, as presented in [Straßburger 2003b], where the units 1 and ⊥ are not equivalent to each other. However, in [Straßburger 2003b] only our second decomposition is given. The proof of the decomposition theorems works equally well for the logic which does not have the logical equivalences !!R ≡ !R and ??R ≡ ?R. One just has

• 15 to remove the rules g↓ and g↑ from the system. As a matter of fact, the structure of the modalities (e.g., the fact that there are 7 idempotent modalities in MELL or NEL) does not influence decomposition.

PERMUTATION OF RULES

Permutation of rules in the calculus of structures serves the same purpose as rule permutations on the sequent calculus, with the only difference that due to the greater flexibility of the formalism, there are more cases to consider. Definition 4.1. A rule π permutes over a rule ρ (or ρ permutes under π) if for every derivation

Q ρ U π P
there is a derivation

Q π V ρ P
for some structure V .

For obtaining our decompositions, this definition is too strict. We would need, for example, that the rule e↓ permutes over all other rules in the system, which is not the case. We give a weaker concept: Definition 4.2. A rule π permutes over a rule ρ by a system S , if for every derivation

Q ρ U π P
there is a derivation

Q π V ρ W S P
for some structures V and W . Dually, ρ permutes under π by S , if for every derivation

Q ρ U π P
there is a derivation

Q S W π V ρ P
for some structures V and W .

Additionally, we will use the following terminology borrowed from term rewriting.

In a rule instance

S{W } ρ S{Z }
we call Z the redex and W the contractum of the rule's instance. If we have Z = W , then the rule instance is called trivial. (This can happen because of the equational theory and the involvement of the unit •.) In the following we will assume, without loss of generality, that the trivial rule instances are removed from all derivations. When reading this section, the reader might notice some similarity to the analysis of critical pairs for local confluence in term rewriting. In fact, the basic idea is the same but the conceptual goal is different, as it is shown in Figure 7.

local confluence permutability of rules have:

• ρ { { v v v v v π 5 # H H H H H • • • ρ { { v v v v v • π 5 # H H H H H • want: • ρ { { v v v v v π 5 # H H H H H • S 5 # • S { { • • ρ ~~~~~π 9 ' P P P P • ρ • π 2 @ @ @ @ @ • S w w • or • ρ ~~~~~S 9 ' • π • π 2 @ @ @ @ @ • ρ w w n n n n • S is the full system
S is as small and restricted as possible We now begin by showing that e↓ can be permuted over all rules except w↓, b↓, b↑, and g↑ which will be discussed later. In each of the following lemmas we also indicate for which step in the proof of Theorem 3.1 they are needed.

Lemma 4.3 (Step 1 in Fig. 5). The rule e↓ permutes over the rules e↑, ai↓, ai↑, s, q↓, q↑, p↓, p↑, w↑, and g↓ by the system {s, q↓, q↑}.

The proofs of this and the following lemmas about rule permutations are done by routine case analysis4 and the reader is invited to skip these proofs in the first reading. In such a case analysis most cases are trivial and some cases are nontrivial. For the sake of completeness, this time we explain the case analysis in detail, and for similar lemmas that come later, we show only the nontrivial cases.

Proof of Lemma 4.3.

Consider S{W } ρ S{Z} e↓ , S ′ {Z ′ }
where ρ ∈ {e↑, ai↓, ai↑, s, q↓, q↑, p↓, p↑, w↑, g↓} = SNEL \ {e↓, w↓, b↓, b↑, g↑}. We have to check all possibilities where the contractum • of e↓ can appear inside S{Z}. We start with the two trivial cases:

(i) The contractum • of e↓ is inside the context S{ }. That means that Z ′ = Z,
and we can replace

S{W } ρ S{Z} e↓ S ′ {Z} → S{W } e↓ S ′ {W } ρ S ′ {Z}
• 17

(ii) The contractum • of e↓ appears inside Z, but only inside a substructure of Z that is not affected by the rule ρ. Instead of getting too formal, we show an example:

S([R{•} U ] T ) s S [(R{•} T ) U ] e↓ S [(R{!•} T ) U ] → S([R{•} U ] T ) e↓ S([R{!•} U ] T ) s S [(R{!•} T ) U ]
The cases where the • appears inside U or T are similar. The same situation can occur with the rules q↓, q↑, p↓, p↑, and g↓.

The next case is in fact a subcase of (i), but for didactic reasons we list it separately.

(iii) The contractum • of e↓ is the redex of ρ (which is one of e↑, ai↑, w↑). Then we have

S(a ā) ai↑ S{•} e↓ S{!•} → S(a ā) = S [(a ā) •] e↓ S [(a ā) !•] ai↑ S [• !•] = S{!•}
Finally, we come to the case which is nontrivial. It is the one where we need the system {s, q↓, q↑}.

(iv) The contractum • of e↓ actively interferes with the rule ρ. This can happen because of the equational theory for •. First, let ρ = ai↓ and consider the two derivations:

S{•} ai↓ S [a ā] = S [(a •) ā] e↓ S [(a !•) ā]
and

S{•} ai↓ S [a ā] = S [ a ⊳ • ā] e↓ S [ a ⊳ !• ā]
They can be replaced by

S{•} = S(• •) e↓ S(• !•) ai↓ S([a ā] !•) s S [(a !•) ā]
and

S{•} = S • ⊳ • e↓ S • ⊳ !• ai↓ S [a ā] ⊳ !• q↓ S [ a ⊳ !• ā]
respectively. Here we used the rules s and q↓ to move the redex !• of e↓ out of the way of the rule ai↓ such that the situation could be handled similarly to case (i). A similar situation can occur with the rules s, p↓, and q↓. We will not show all possibilities here, but it should be clear that they all work because of the same principle. We content ourselves of presenting only the most complicated case (where ρ = q↓):

S [ R ⊳ R ′ U ] ⊳ [ T ⊳ T ′ V ] q↓ S [ R ⊳ R ′ ⊳ T ⊳ T ′ U ⊳ V ] = S [ R ⊳ ( R ′ ⊳ T •) ⊳ T ′ U ⊳ V ] e↓ S [ R ⊳ ( R ′ ⊳ T !•) ⊳ T ′ U ⊳ V ] → S [ R ⊳ R ′ U ] ⊳ [ T ⊳ T ′ V ] = S( [ R ⊳ R ′ U ] ⊳ [ T ⊳ T ′ V ] •) e↓ S( [ R ⊳ R ′ U ] ⊳ [ T ⊳ T ′ V ] !•) q↓ S( [ R ⊳ R ′ ⊳ T ⊳ T ′ U ⊳ V ] !•) s S [( R ⊳ R ′ ⊳ T ⊳ T ′ !•) U ⊳ V ] q↑ S [ R ⊳ ( R ′ ⊳ T ⊳ T ′ !•) U ⊳ V ] q↑ S [ R ⊳ ( R ′ ⊳ T !•) ⊳ T ′ U ⊳ V ]
Here, two instances of q↑ and one instance of s are needed to move the !• out of the way of q↓. A different situation can occur when ρ = p↑. Consider the two derivations

S(?(R R ′ ) !(T T ′ )) p↑ S{?(R R ′ T T ′ )} = S{?(R [(R ′ T ) •] T ′ )} e↓ S{?(R [(R ′ T ) !• ] T ′ )} and S(?(R R ′ ) !(T T ′ )) p↑ S{?(R R ′ T T ′ )} = S{?(R (R ′ T ) ⊳ • T ′ )} e↓ S{?(R (R ′ T ) ⊳ !• T ′ )}
which can be replaced by:

S(?(R R ′ ) !(T T ′ )) = S(?(R [R ′ •]) !(T T ′ )) e↓ S(?(R [R ′ !• ]) !(T T ′ )) p↑ S{?(R [R ′ !•] T T ′ )} s S{?(R [(R ′ T ) !•] T ′ )} and S(?(R R ′ ) !(T T ′ )) = S(?(R R ′ ⊳ • ) !(T T ′ )) e↓ S(?(R R ′ ⊳ !• ) !(T T ′ )) p↑ S{?(R R ′ ⊳ !• T T ′ )} q↑ S{?(R (R ′ T ) ⊳ !• T ′ )}
Here the !• has not been moved to the outside but to the inside, such that the permutation could be handled as in case (ii) above. A similar situation can occur with the rules ρ = s, q↓, q↑. Again, we do not show all possibilities.

But the reader should be able to convince himself that it is always possible to move the !• out of the way of ρ.5

Observation 4.4 (Step 1 in Fig. 5). Let us now see how to permute e↓ over the rules w↓, b↓, b↑, and g↑, which have been left out in Lemma 4.3. The nontrivial cases are as follows:

-for w↓:

S{•} w↓ S{?R{•}} e↓ S{?R{!•}} → S{•} w↓ S{?R{!•}} (1)
-for b↓:

S [?R{•} R{•}] b↓ S{?R{•}} e↓ S{?R{!•}} → S [?R{•} R{•}] e↓, e↓ S [?R{!•} R{!•}] b↓ S{?R{!•}} (2)
• 19

-for b↑:

S{!R{•}} b↑ S(!R{•} R{•}) e↓ S(!R{!•} R{•}) → S{!R{•}} e↓ S{!R{!•}} b↑ S(!R{!•} R{!•}) w↑ S(!R{!•} R{•}) (3)
-for g↑:

S{!R} g↑ S{!!R} = S{!(• !R)} e↓ S{!(!• !R)} → S{!R} g↑ S{!!R} g↑ S{!!!R} b↑ S{!(!!R !R)} w↑ S{!(!• !R)} (4)
Note that these cases do not follow the statement of Definitions 4.1 or 4.2, which is the reason why they have been left out in Lemma 4.3.

Lemma 4.5 (Step 1 in Fig. 5). Every SNEL derivation ∆ can be decomposed as indicated in Step 1 in Figure 5.

Proof. We show by induction that all instances of e↓ in ∆ can be permuted to the top. For each instance π of e↓ in ∆ we define b(π) to be the number of instances of b↓ that appear above π in ∆. We say that π is at the top of ∆, if the only rules that appear above π in ∆ are instances of e↓. We let the e↓-rank of ∆ be the multiset rk e↓ (∆) = {| b(π) | π is an instance e↓ in ∆ and π is not at the top | }. By δ e↓ (∆) we denote the height of the derivation above the topmost e↓ that is not at the top of ∆. As induction measure we use the pair rk e↓ (∆), δ e↓ (∆) with the lexicographic ordering, and the multiset ordering for the first component. This measure always goes down if we permute up the topmost instance of e↓ that is not at the top (by using Lemma 4.3 and Observation 4.4). Dually, all instances of e↑ can be permuted to the bottom.

We now continue with Step 4. For this, recall that SNELh = {s, q↓, q↑, p↓, p↑}.

Lemma 4.6 (Steps 4,7,9 in Fig. 5,6). The rules w↓ and ai↓ permute over the rules e↑, ai↓, ai↑, s, q↓, q↑, p↓, p↑, w↑, and g↓ by the system {s, q↓, q↑}.

Proof. The contractum of w↓ and ai↓ is the same as of e↓, namely •. Hence, this proof is the same as the one for Lemma 4.3.

Lemma 4.7 (Step 4 in Fig. 5).

Step 4 in the proof of Theorem 3.1 can be performed as indicated in Figure 5.

Proof. We show by induction that in a derivation ∆ in the system {ai↓, ai↑} ∪ SNELh = {ai↓, ai↑, s, q↓, q↑, p↓, p↑} all instances of ai↓ can be permuted to the top. As induction measure we use the pair n ai↓ (∆), δ ai↓ (∆) with the lexicographic ordering, where n ai↓ (∆) is the number of ai↓ instances in ∆ that are not yet at the top of the derivation, and δ ai↓ (∆) is the height of the derivation above the topmost such ai↓ in ∆. This measure always goes down if we permute the topmost instance of ai↓ up, by using Lemma 4.6. This measure is simpler than the one in the proof of Lemma 4.5 because we do not have to deal with b↓. Dually, all ai↑ can be permuted to the bottom.

Lemma 4.8 (Steps 7,9 in Fig. 6). Steps 7 and 9 in the proof of Theorem 3.1 can be performed as indicated in Figure 6.

Proof. This proof is similar to the proof of Lemma 4.7 and uses Lemma 4.6. Note that for Step 7, we additionally need to permute ai↓ over w↓, for which the only nontrivial case is similar to (1).

We will now continue with Step 3, for which the following lemma (and its dual) is sufficient.

Lemma 4.9 (Step 3 in Fig. 5). All derivations W1 {g↑, b↑, w↑} W4 can be decomposed as indicated in Step 3 in Figure 5.

Proof. This is again a simple rule permutation. First, all instances of g↑ are permuted up to the top. The trivial cases are as in Lemma 4.3. The only nontrivial cases are the following:

S{!R} b↑ S(!R R) g↑ S(!!R R) → S{!R} g↑ S{!!R} b↑ S(!!R !R) b↑ S(!!R !R R) w↑ S(!!R • R) = S(!!R R) (5) S{!R{!T }} b↑ S(!R{!T } R{!T }) g↑ S(!R{!!T } R{!T }) → S{!R{!T }} g↑ S{!R{!!T }} b↑ S(!R{!!T } R(!!T )) b↑ S(!R{!!T } R(!!T !T )) w↑ S(!R{!!T } R(• !T )) = S(!R{!!T } R{!T }) (6)
Finally, all w↑ are permuted under the b↑, where

S{!R{!T }} w↑ S{!R{•}} b↑ S(!R{•} R{•}) → S{!R{!T }} b↑ S(!R{!T } R{!T }) w↑, w↑ S(!R{•} R{•}) (7)
is the only nontrivial case.

Remark 4.10. Note that the decomposition of Lemma 4.9 does not allow much variation. We can neither permute b↑ over g↑, nor can we permute w↑ over b↑, as the following examples show:

!a g↑ !!a b↑ (!!a !a)
and

!a b↑ (!a a) w↑ a
Lemma 4.11 (Step 5 in Fig. 5). The rules g↑, b↑, and w↑ permute over e↓.

• 21

Proof. The only nontrivial cases are the following.

S{•} e↓ S{!•} g↑ S{!!•} → S{•} e↓ S{!•} e↓ S{!!•} S{•} e↓ S{!•} b↑ S(!• •) → S{•} e↓ S{!•} = S(!• •) S{•} e↓ S{!•} w↑ S{•} → S{•} = S{•}
In all of them the instance of g↑, b↑, and w↑, which is permuted up disappears. The trivial cases are as in case (i) of Lemma 4.3. Case (ii) in the proof of that lemma cannot occur here.

Lemma 4.12 (Step 5 in Fig. 5).

Step 5 in the proof of Theorem 3.1 can be performed as indicated in Figure 5.

Proof. By Lemma 4.11 and its dual.

Lemma 4.13 (Steps 6,8 in Fig. 6). Steps 6 and 8 in the proof of Theorem 3.1 can be performed as indicated in Figure 6.

Proof. Steps 6 and 8, are almost identical to Steps 1 to 3 and 5, with the only difference that the rules w↑ and w↓ are omitted.

After this tour de force of simple rule permutations, the proof of Theorem 3.1 is completed, except for Step 2. At first sight one might expect that this can also be done by simple rule permutations. So, let us attempt to permute all g↑, b↑, and w↑ up to the top of a derivation. (iii) The redex Z of ρ is inside the contractum of π, i.e., we have one of the following three situations

Case

S{!R{W }} ρ S{!R{Z}} g↑ S{!!R{Z}} S{!R{W }} ρ S{!R{Z}} b↑ S(!R{Z} R{Z}) S{!R{W }} ρ S{!R{Z}} w↑ S{•}
which can be replaced by

S{!R{W }} g↑ S{!!R{W }} ρ S{!!R{Z}} S{!R{W }} b↑ S(!R{W } R{W }) ρ, ρ S(!R{Z} R{Z}) S{!R{W }} w↑ S{•} (8)
respectively.

The next case corresponds to case (iv) in the proof of Lemma 4.3.

(iv) The contractum !R of π actively interferes with the redex Z of ρ. This can only happen with ρ ∈ {w↓, b↓, p↓}. If ρ is w↓ or b↓, then the situation is similar to (1) and ( 2) above. If ρ = p↓, then we have one of

S{![R T ]} p↓ S [!R ?T ] g↑ S [!!R ?T ] S{![R T ]} p↓ S [!R ?T ] b↑ S [(!R R) ?T ] S{![R T ]} p↓ S [!R ?T ] w↑ S [• ?T ]
which can be replaced by, respectively (for the second one, see Remark 2.4):

S{![R T ]} g↑ S{!![R T ]} p↓ S{![!R ?T ]} p↓ S [!!R ??T ] g↓ S [!!R ?T ] S{![R T ]} b↑ S(![R T ] [R T ]) p↓ S([!R ?T ] [R T ]) s S [([!R ?T ] R) T ] s S [(!R R) ?T T ] b↓ S [(!R R) ?T ] S{![R T ]} w↑ S{•} = S [• •] w↓ S [• ?T ]
This means that there is indeed no objection against permuting all instances of g↑, b↑, and w↑ up to the top of a derivation, and then (by duality) permute all g↓, b↓, and w↓ down to the bottom. However, the problem is that while permuting g↑, b↑, w↑ up, we introduce, in case (iv), new instances of g↓, b↓, w↓, and dually, while permuting g↓, b↓, w↓ down, we introduce new instances of g↑, b↑, w↑. This means that this permuting up and down could run forever. At least, it is not obvious that it terminates eventually, as it is the case with Steps 1, 4, 7 and 9 in the proof of Theorem 3.1.

Please note that there is no obvious induction measure related to the size of the derivation that could be used for showing termination. The up and down permutation of w↑ and w↓ alone is unproblematic because at each critical case the disturbing instance of p↓ or p↑ is destroyed (but for convenience we will deal with all six rules g↑, b↑, w↑ and g↓, b↓, w↓ together). The up and down permutation of g↑, b↑ and g↓, b↓ is very problematic, however. The rules g↑ and g↓ cause a duplication of the disturbing instance of promotion, and the permutation of b↑ and b↓ causes an even worse increase in the size of the derivation. In fact, the ρ in the middle derivation in (8) could be an instance of a promotion that is disturbing for another g↑ or b↑.

Clearly, a different technology is needed here, and this is the purpose of the next section.

PATHS AND CYCLES IN !-?-FLOW-GRAPHS

For showing the termination of Step 2 in the proof of Theorem 3.1, we first introduce the notion of !-?-flow-graph (in Section 5.1), which is very similar to Buss' logical flow graphs [START_REF] Buss | The undecidability of k-provability[END_REF]], but instead of considering all subformulas occurring in the derivation, we consider only the !-and ?-subformulas. Based on these !-?-flowgraphs we define for each instance of g↑, g↓, b↑, b↓, w↑, w↓ its rank (in Section 5.2). The purpose of this rank is, very roughly speaking, to describe the amount of work that still has to be done to move this rule instance to its destination at the top or the bottom of the derivation. The up-rank of a derivation ∆, denoted by rk ↑ (∆)

• 23 is then the multiset of the ranks of all instances of g↑, b↑, w↑ occurring in ∆, and the down-rank, denoted by rk ↓ (∆) is the multiset of the ranks of all instances of g↓, b↓, w↓ in ∆. With this, we are able to show that the process of permuting up all g↑, b↑, w↑ does terminate (in Section 5.3), by using as induction measure the pair rk ↑ (∆), δ , where δ is the height of ∆ above the topmost g↑, b↑, w↑. This is similar to the proof of Lemma 4.5, since rk ↑ (∆) does not always go down in the permutation process. Then we define the rank of a derivation ∆, denoted by rk(∆), to be the multiset union of rk ↑ (∆) and rk ↓ (∆). For showing termination of the whole of Step 2, we need to show that eventually rk(∆) decreases. We will see that this is indeed the case, provided that the !-?-flow-graph of ∆ is acyclic (in Section 5.3). There are, in principle, two kinds of cycle in a!-?-flow-graph: forked cycles and unforked cycles. First, we show that the forked cycles disappear during the permutation process (in Section 5.4). Finally (in Section 5.5) we show that unforked cycles cannot exist inside a !-?-flow-graph, by using an acyclicity property that has independently been discovered in the theory of proof nets [START_REF] Retoré | Pomset logic: A non-commutative extension of classical linear logic[END_REF]]. This then completes the proof of Theorem 3.1.

!-?-Flow-Graphs

Definition 5.1. For instances of the rules g↓, g↑, b↓, b↑, w↓, w↑, and p↓, p↑ we define their principal structure as indicated below with a gray background:

S{??T } g↓ S{?T } S [?T T ] b↓ S{?T } S{•} w↓ S{?T } S{![R T ]} p↓ S [ !R ?T ] S{!R} g↑ S{!!R} S{!R} b↑ S(!R R) S{!R} w↑ S{•} S(?T !R) p↑ S{?(T R)}
If ρ ∈ {g↓, b↓, w↓}, then its principal structure is the redex ?T of ρ. If ρ ∈ {g↑, b↑, w↑}, then its principal structure is the contractum !R of ρ. If ρ = p↓, then its principal structure is the !-substructure of its redex, and if ρ = p↑, then its principal structure is the ?-substructure of its contractum.

The basic idea of the !-?-flow-graph of a derivation is to mark the "path" that is taken by the principal structures of instances of g↑, g↓, b↑, b↓, w↑, w↓ while they are traveling up and down in the derivation. Formally, it is defined as follows:

Definition 5.2. Let ∆ be a derivation in SNEL. The !-?-flow-graph of ∆ is a directed graph, denoted by G !? (∆), whose vertices are the occurrences of !-and ?-substructures appearing in ∆. Two such substructures are connected via an edge in G !? (∆) if they appear inside the premise and the conclusion of an inference rule according to the prescriptions in Figure 8. When visualizing the !-?-flow-graph of a derivation, we draw it inside the derivation, as indicated in Figure 8, and as shown in the example below (cf. Remark 2.4): The first two cases in Figure 8 are straightforward: The rule ρ either modifies the context of !R or ?T , or ρ works inside !R or ?T , without touching the modality. Cases (iii) and (iv) take care of the modalities that are actively involved in the redex and contractum of the absorption and digging rules. Cases (v) and (vi) involve a duplication of a modality structure due to absorption, which causes a branching in the !-?-flow-graph. The most interesting case is (vii), because the flow changes its direction. This corresponds to the introduction of a b↓ in case (iv) in 4.14. Note that in Figure 8 the cases (vi) and (vii) are the only ones where we have a "forking" in the graph. In cases (iv) and (v) the situation is better described as "merging", and in all other cases the situation is purely "linear".

(i) S{ R} ρ S ′ { R} S{!R} ρ S ′ {!R} S{ T } ρ S ′ { T } S{?T } ρ S ′ {?T } (ii) S{ R{W }} ρ S{ R{Z}} S{!R{W }} ρ S{!R{Z}} S{ T {W }} ρ S{ T {Z}} S{?T {W }} ρ S{?T {Z}} (iii) S{ R} b↑ S( R R) S{!R} b↑ S(!R R) S [ T T ] b↓ S{ T } S [?T T ] b↓ S{?T } (iv) S{ R} g↑ S{ R} S{!R} g↑ S{!!R} S{ T } g↓ S{ T } S{??T } g↓ S{?T } (v) S{ V { R}} b↑ S( V { R} V { R}) S{!V {!R}} b↑ S(!V {!R} V {!R}) S [ U { T } U { T }] b↓ S{ U { T }} S [?U {?T } U {?T }] b↓ S{?U {?T }} (vi) S [ U { R} U { R}] b↓ S{ U { R}} S [?U {!R} U {!R}] b↓ S{?U {!R}} S{ V { T }} b↑ S( V { T } V { T }) S{!V {?T }} b↑ S(!V {?T } V {?T }) (vii) S{ [R T ]} p↓ S [ R T ] S{![R T ]} p↓ S [!R ?T ] S( T R) p↑ S{ (T R)} S(?T !R) p↑ S{?(T R)}
For two vertices U and V of G !? (∆), we write U ∆ V if there is an edge from U to V in G !? (∆). We use + ∆ to denote the transitive closure of ∆ , and * ∆ to denote the reflexive transitive closure of ∆ . We use the standard notions of paths and cycles in directed graphs:

• 25 Definition 5.3. A path in the !-?-flow-graph of a derivation ∆ is a sequence of vertices V 0 , V 1 , . . . , V n , such that V i-1 ∆ V i for each i ∈ {1, . . . , n}. A cycle is a path such that the first vertex and the last vertex are identical. The !-?-flow-graph of a derivation is acyclic, if it does not contain any cycle, i.e., there is no vertex V with V + ∆ V . A path p is called cyclic, if there is a vertex which occurs more than once in p.

Clearly, every cycle is a cyclic path, and the !-?-flow-graph of a derivation is acyclic, if and only if it contains no cyclic path. To come back to our example in (9), consider the following four excerpts from its !-?-flow-graph: The first example shows a path, where the first and the last vertex in the path are marked with a gray background. The subgraph indicated in the second example is not a path (direction matters). The third example shows a cycle, and the last example a cyclic path (again, first and last vertex are marked). In particular, the !-?-flow-graph in ( 9) is not acyclic.

[ a a] p↓ [ a a] b↓ a b↑ ( a a) p↑ ( a a) p↑ ( a a) !![!a a] p↓ ![?!a !
Definition 5.4. A vertex V in G !? (∆) is called a !-vertex if it is a !-structure, and ?-vertex if it is a ?-structure. Note that an edge from a !-vertex to a !-vertex always goes upwards in a derivation. Hence, we call a path that contains only !-vertices an up-path. Similarly, a path with only ?-vertices is called a down-path. Edges from !-vertices to ?-vertices or from ?-vertices to !-vertices are called flipping edges. The number of flipping edges in a path p is called the flipping number of p, denoted by fl(p).

For example, the path indicated in the leftmost derivation in (10) has flipping number 2, and the two paths in the second derivation in (10) have both flipping number 0. Definition 5.5. Let ∆ be a derivation. A vertex V in G !? (∆) is called a p-vertex if it is the principal structure of a p↓ or p↑. The vertex V is called a b-vertex if it is the principal structure of a b↓ or b↑.

The Rank of Rules and Derivations

In this section we define the rank of a rule instance ρ as a triple in the set {0, 1} × (ω + 1) × ω equipped with the lexicographic ordering, where ω = {0, 1, 2, . . .} and ω+1 = ω∪{ω} are both equipped with the natural ordering. Roughly speaking, the first value is the status of ρ, indicating whether ρ has already reached its destination at the top or the bottom of the derivation. The second value, called the p-number of ρ, is the number of instances p↓ and p↑ that ρ might encounter on its journey. And the third value, called the onion b-number of ρ, is encoding how often ρ might get duplicated during the permutation process. This means we have to count the number of b↓ and b↑ that might cause a duplication of ρ, as in case (iii) of 4.14. To that end, we need the notions of onion and look-back tree, which are defined below.

Definition 5.6. The p-number of a path p in G !? (∆), denoted by p(p), is the number of p-vertices occurring in p. If p is cyclic, the vertices with multiple occurrences in p are counted as many times as they occur in p.

For example, the path p indicated in the leftmost example in (10), we have p(p) = 2. The rightmost one has p(p) = 3 if the path passes through the cycle once, and p(p) = 5 if the path passes through the cycle twice, and so on. Note that we do not have p(p) = fl(p) in general. But we have always p(p) ≥ fl(p).

Definition 5.7. Let ∆ be a derivation and let V be a vertex in G !? (∆). Then the p-number of V in ∆, denoted by p(V ), is defined as follows:

p(V ) = sup{ p(p) | p is a path starting in V } . ( 11
)
For a rule instance ρ in ∆ of the kind g↓, b↓, w↓, or g↑, b↑, w↑, we define its p-number, denoted by p ∆ (ρ) to be the p-number of its principal structure.

In other words, for determining p(V ), we take the maximum of all p(p), where p ranges over all paths that have V as starting vertex. If one of these paths is cyclic, then p(V ) = ω.

For example, consider again the derivation in ( 9). Below we show it again twice where in each derivation one vertex of the !-?-flow-graph is marked. Let us denote them by V 1 and V 2 , respectively. On the left, we have shown all paths starting in V 1 . There are only two of them, and both have p-number 1 (because V 1 is their only p-vertex). Hence p(V 1 ) = 1.

On the right we have shown all paths starting in V 2 . Because of the cycle, we have p(V 2 ) = ω.

Definition 5.8. Let ∆ be a derivation. A look-back tree t in ∆ is a subgraph of G !? (∆) such that -t is a directed tree whose edges are directed towards the root, -every path from a leaf to the root in t contains at most one flipping edge, and -every branching vertex of t (i.e., every vertex with two incoming edges) is the principal structure of an instance of g↓ or g↑.

The b-number of a look-back tree t, denoted by b(t), is the number of b-vertices occurring in t.

Note that because of the restriction of the flipping number of paths in t to 1, a look-back tree cannot be cyclic.

• 27

Consider for example the following derivations in which we exhibited subgraphs of the !-?-flow-graph. On the left we have a look-back tree, and its b-number is two. Its root and the two b-vertices are marked with a gray background. The second example in ( 13) is not a look-back tree because of the two flippings in the path. The third example is not a look-back because there is a branching vertex (marked with gray background) that is not the principal structure of an instance of g↓ or g↑.

[a b b] p↓ [ a [ b b] ] b↓ [ a b ] g↓ [ a b] b↑ [( a a) b ] ![a ?b b] p↓ [!a ?[?b b] ] b↓ [!a ??b ] g↓ [ !a ?b] b↑ [(!a a) ?b ] ( a [b c]) p↓ ( a [ b c]) s [( a b) c] p↑ [ (a b) c] (?a ![b c]) p↓ (?a [!b ?c]) s [(?a !b) ?c] p↑ [?(a b) ?c] [ a a] g↓ [ a a]
Definition 5.9. Let ∆ be a derivation and let V be a vertex in G !? (∆). We define the b-number of V , denoted by b(V ), as follows:

b(V ) = sup{ b(t) | t is a look-back tree with root V } . ( 14
)
Note that for the p-number of a vertex, we look forward in the graph, and for the b-number we look backwards. Furthermore, for the b-number we consider only paths with flipping number 0 or 1, and we allow branchings as in case (iv) of Figure 8, but never as in cases (v), (vi), and (vii) of that Figure.

To see some example, consider again the rightmost derivation in ( 13). Let us denote the ?a-occurrence in the conclusion by V 3 . The first two derivations below in ( 15) show two look-back tree with V 3 as root. The third derivation shows a look-back tree of the !![!a a]-vertex in the premise of the derivation in (9). Let us denote that vertex by V 4 .

[ We have b(V 3 ) = 1. The first look-back tree has b-number 1 and the second one has b-number 0. We have b(V 4 ) = 2 because both instances, b↑ and b↓ have their principal structure as vertex in the indicated look-back tree.

Definition 5.10. Let ∆ be a derivation, and !R be a !-vertex in G !? (∆), i.e., also a substructure of ∆. The onion of !R, denoted by (!R), is the set of all ?-vertices in G !? (∆) that have exactly this !R as substructure. This means, in particular, that they appear in the same line of ∆ as !R. Dually, we define the onion of a ?-vertex ?T , denoted by (?T ), to be the set of all !-vertices that have this structure ?T as substructure. For every rule instance ρ in ∆ of the kind g↓, b↓, w↓, or g↑, b↑, w↑, we define its onion ∆ (ρ) in ∆ to be the onion of its principal structure. The onion b-number of ρ in ∆, denoted by b ∆ (ρ), is the sum of the b-numbers of the

(ρ) = V ∈ ∆ (ρ) b(V ) .
For example, consider the bottommost occurrence of !a in the derivation in (9). It is marked in the rightmost derivation in (10). Its onion consists of the two ?structures in the conclusion of the derivation. Both have b-number 1. Hence, the onion b-number of a rule that had this !a as principal structure would be 2.

Finally, we define the status of a rule instance to be either 0 or 1, such that it is 1 if the rule is of the kind g↓, b↓, w↓, or g↑, b↑, w↑, and not yet at its final destination at the top or the bottom of the derivation. The status is 0 if the rule does not play any further role in the up-down-permutation. The motivation of this is that Step 2 of our decomposition process (see Figure 5) is completed if and only if all rules instances in the derivation have status 0. Formally, the status is defined as follows.

Definition 5.11. Let SNEL ′ = SNEL \ {e↓, e↑}, let ∆ be a derivation in SNEL ′ , and let ρ be a rule instance inside ∆. Then ρ splits ∆ into two parts:

Q SNEL ′ ∆1 S{W } ρ S{Z} SNEL ′ ∆2 P
The status of ρ in ∆, denoted by st ∆ (ρ) is 1 if we have one of the following two cases:

-ρ ∈ {g↑, b↑, w↑} and ∆ 1 contains an instance of a rule in SNEL ′ \ {g↑, b↑, w↑}, or -ρ ∈ {g↓, b↓, w↓} and ∆ 2 contains an instance of a rule in SNEL ′ \ {g↓, b↓, w↓}.

Otherwise st ∆ (ρ) = 0.

The reason for using SNEL ′ is that the rules e↓ and e↑ are not considered in Step 2 of Figure 5. However, all statements in this section about SNEL ′ are also valid for SNEL. Now we are using the status, the p-number, and the onion b-number of a rule instance to define its rank.

Definition 5.12. For a rule instance ρ of the kind g↓, b↓, w↓ or g↑, b↑, w↑ inside a derivation ∆, we define its rank rk ∆ (ρ) ∈ {0, 1} × (ω + 1) × ω to be the triple

rk ∆ (ρ) = st ∆ (ρ), p ∆ (ρ), b ∆ (ρ) .
For the whole of ∆, we define the rank rk(∆) to be the multiset of the ranks of its occurrences of g↓, b↓, w↓, g↑, b↑, w↑, i.e., rk(∆) = {| rk ∆ (ρ) | ρ in ∆ and ρ is one of g↓, b↓, w↓, g↑, b↑, w↑ | } .

• 29

We define the down-rank of ∆, denoted by rk ↓ (∆) by considering only the downrules g↓, b↓, w↓ in the multiset:

rk ↓ (∆) = {| rk ∆ (ρ) | ρ in ∆ and ρ is one of g↓, b↓, w↓ | } .
Similarly, the up-rank rk ↑ (∆) takes only the up-rules g↑, b↑, w↑ into account:

rk ↑ (∆) = {| rk ∆ (ρ) | ρ in ∆ and ρ is one of g↑, b↑, w↑ | } .
It follows immediately from the definition that rk(∆) = rk ↓ (∆) ⊎ rk ↑ (∆). For example, in (9), we have that the rank of the b↓ instance is 1, ω, 1 and the rank of the b↑ instance is 1, 0, 0 . Hence, the rank of the whole derivation is the multiset {| 1, ω, 1 , 1, 0, 0 | }.

Permutations Again

In this section we will first analyze the impact of the rule permutations needed for

Step 2 to the rank of the derivation, and see that Step 2 terminates if the !-?-flowgraph of the derivation is acyclic. Now, let us consider again the cases in 4.14. We begin with the trivial cases (cf. the proof of Lemma 4.3).

Case Analysis 5.13 (for permuting g↑, b↑, w↑ up). Let a derivation ∆ be given. As in 4.14, Consider a subderivation

S{W } ρ S{Z} π P , (16)
where ρ ∈ SNEL ′ \ {g↑, b↑, w↑} and π ∈ {g↑, b↑, w↑}. In the following case analysis we replace (as done in Section 4) in ∆ the subderivation in ( 16) by a new subderivation with the same premise and conclusion. We use ∆ ′ to denote the result of this replacement.

(i) The contractum !R of π is inside the context S{ }. Here is an example with π = g↑ and ρ = s:

′ { }{([ ] )} s ′ { }{[( ) ]} g↑ ′ { }{[( ) ]} S ′ {!R}{([P U ] T )} s S ′ {!R}{[(P T ) U ]} g↑ S ′ {!!R}{[(P T ) U ]} → ′ { }{([ ] )} g↑ ′ { }{([ ] )} s ′ { }{[( ) ]} S ′ {!R}{([P U ] T )} g↑ S ′ {!!R}{([P U ] T )} s S ′ {!!R}{[(P T ) U ]}
Here, we used S ′ { }{ } to denote a context with two independent holes, and we used bold light lines to indicate bunches of parallel paths going through the derivation. Clearly, in this case, neither p ∆ (π) nor b ∆ (π) change their value (but st ∆ (π) could go down). The important fact to observe is that the rank of all other rules in ∆ remains unchanged in ∆ ′ . Hence, rk ↑ (∆ ′ ) ≤ rk ↑ (∆) and rk ↓ (∆ ′ ) = rk ↓ (∆). (ii) The contractum !R of π appears inside the redex Z of ρ, but only inside a substructure of Z that is not affected by ρ. Again, we exhibit an example with π = g↑ and ρ = s:

([ { } ] ) s [( { } ) ] g↑ [( { } ) ] S([P {!R} U ] T ) s S [(P {!R} T ) U ] g↑ S [(P {!!R} T ) U ] → ([ { } ] ) g↑ ([ { } ] ) s [( { } ) ] S([P {!R} U ] T ) g↑ S([P {!!R} U ] T ) s S [(P {!!R} T ) U ]
• Lutz Straßburger and Alessio Guglielmi

As in the previous case, the values of p ∆ (π) and b ∆ (π) are not affected. This is trivial for ρ ∈ {s, q↓, q↑}, and we leave it as an instructive exercise to the reader to verify it also for ρ = p↓. For ρ = p↑, the value of p ∆ (π) remains unchanged, but b ∆ (π) could go down. As in the previous case, st ∆ (π) could go down, and the rank of all other rules in ∆ remains unchanged in ∆ ′ . Hence,

rk ↑ (∆ ′ ) ≤ rk ↑ (∆) and rk ↓ (∆ ′ ) = rk ↓ (∆). (iii) The redex Z of ρ is inside the contractum !R of π. (a) If π = w↑, then ′ { { }} ρ ′ { { }} w↑ ′ {•} S ′ {!R{W }} ρ S ′ {!R{Z}} w↑ S ′ {•} → ′ { { }} w↑ ′ {•} S ′ {!R{W }} w↑ S ′ {•} We have rk(∆ ′ ) ≤ rk(∆) because ρ is removed. (b) If π = g↑, then ′ { { }} ρ ′ { { }} g↑ ′ { { }} S ′ {!R{W }} ρ S ′ {!R{Z}} g↑ S ′ {!!R{Z}} → ′ { { }} g↑ ′ { { }} ρ ′ { { }} S ′ {!R{W }} g↑ S ′ {!!R{W }} ρ S ′ {!!R{Z}}
Note that the onion of ρ is changed if ρ is an instance of w↓, b↓, or g↓, because the number of ! in its context increased. But the b-number of the !-vertex in the premise of the derivations above is the same as the sum of the b-numbers of the two !-vertices in the conclusion. Hence, the onion b-number of ρ does not change. Therefore rk(∆ ′ ) ≤ rk(∆). (c) If π = b↑, then the situation is not entirely trivial, because ρ gets duplicated:

′ { { }} ρ ′ { { }} b↑ ′ ( { } { }) S ′ {!R{W }} ρ S ′ {!R{Z}} b↑ S ′ (!R{Z} R{Z}) → ′ { { }} b↑ ′ ( { } { }) ρ ′ ( { } { }) ρ ′ ( { } { }) S ′ {!R{W }} b↑ S ′ (!R{W } R{W }) ρ S ′ (!R{W } R{Z}) ρ S ′ (!R{Z} R{Z})
We distinguish the following cases:

(1) If ρ does not involve any modalities, i.e., ρ ∈ {ai↓, ai↑, s, q↓, q↑}, then situation is similar to cases (i) and (ii) above. No rule changes its rank, except that we could have that the status of the b↑ goes down. Hence, we have rk

↑ (∆ ′ ) ≤ rk ↑ (∆) and rk ↓ (∆ ′ ) = rk ↓ (∆). (2) If ρ = p↓, then ′ { { [ ]}} p↓ ′ { [ ]} b↑ ′ ( [ ] [ ]) S ′ {!R{![P T ]}} p↓ S ′ {!R[!P ?T ]} b↑ S ′ (!R[!P ?T ] R[!P ?T ]) → ′ { { [ ]}} b↑ ′ ( { [ ]} { [ ]}) p↓ ′ ( { [ ]} [ ]) p↓ ′ ( [ ] [ ]) S ′ {!R{![P T ]}} b↑ S ′ (!R{![P T ]} R{![P T ]}) p↓ S ′ (!R{![P T ]} R[!P ?T ]) p↓ S ′ (!R[!P ?T ] R[!P ?T ])
As before, p ∆ (π) and b ∆ (π) do not change. However, the p-number, as well as the onion b-number of other rules might go down because some paths disappear (for example the one from the left !P to the right ?T . Hence, rk ↑ (∆ ′ ) ≤ rk ↑ (∆) and rk ↓ (∆ ′ ) ≤ rk ↓ (∆).

• 31

(3) If ρ = p↑, then

′ { ( )} p↑ ′ { { ( )}} b↑ ′ ( { ( )} { ( )}) S ′ {!R(?T !P )} p↑ S ′ {!R{?(T P )}} b↑ S ′ (!R{?(T P )} R{?(T P )}) → ′ { ( )} b↑ ′ ( ( ) ( )) p↑ ′ ( ( ) { ( )}) p↑ ′ ( { ( )} { ( )}) S ′ {!R(?T !P )} b↑ S ′ (!R(?T !P ) R(?T !P )) p↑
S ′ (!R(?T !P ) R{?(T P )}) p↑ S ′ (!R{?(T P )} R{?(T P )})

Again, neither p ∆ (π) nor b ∆ (π) can change (but st ∆ (π) could go down). No other rule in ∆ changes its rank. Although the p↑-instance is duplicated, no path changes its p-number or its b-number. Hence, rk ↑ (∆ ′ ) ≤ rk ↑ (∆) and rk ↓ (∆ ′ ) = rk ↓ (∆). ( 4) Finally, we have to consider the case where ρ ∈ {g↓, b↓, w↓}. We show only the case for ρ = g↓:

′ { ( )} g↓ ′ { { }} b↑ ′ ( { } { }) S ′ {!R(??T )} g↓ S ′ {!R{?T }} b↑ S ′ (!R{?T } R{?T }) → ′ { ( )} b↑ ′ ( { } { }) g↓ ′ ( { } { }) g↓ ′ ( { } { }) S ′ {!R(??T )} b↑ S ′ (!R{??T } R{??T }) g↓ S ′ (!R{??T } R{?T }) g↓ S ′ (!R{?T } R{?T })
Again, neither p ∆ (π) nor b ∆ (π) can change (but st ∆ (π) could go down). Hence, rk ↑ (∆ ′ ) ≤ rk ↑ (∆). However, the number of g↓ instances in the derivation is increased. But both new instances of g↓ have strictly smaller rank in ∆ ′ than the original g↓ in ∆, because their onion b-number is reduced by 1. Hence, rk ↓ (∆ ′ ) < rk ↓ (∆). The same holds for ρ = b↓ and ρ = w↓. Note that for this, it is crucial that the look-back tree of a vertex in the onion (that is used for computing the onion b-number) is acyclic.

(iv) The crucial case is where the contractum !R of π actively interferes with the redex Z of ρ. There are four subcases: (a) For ρ = w↓, the situation is dual to case (iii.a). We show only the case π = g↑:

{•} w↓ { { }} g↑ { { }} S{•} w↓ S{?Z{!R}} g↑ S{?Z{!!R}} → {•} w↓ { { }} S{•} w↓ S{?Z{!!R}}
We have rk ↑ (∆ ′ ) < rk ↑ (∆) because π disappears, and rk ↓ (∆ ′ ) ≤ rk ↓ (∆) because the status of the w↓ could go down. (b) For ρ = g↓, the situation is dual to case (iii.b). We again show only the case π = g↑: We have rk ↑ (∆ ′ ) ≤ rk ↑ (∆) and rk ↓ (∆ ′ ) ≤ rk ↓ (∆) because the status of both rules could go down, and nothing else changes, for the same reason as explained in (iii.b).

(c) For ρ = b↓ the permutations are dual to the ones in case (iii.c.4) above.

For π = w↑, we have

[ { } { }] b↓ { { }} w↑ { {•}} S [?Z{!R} Z{!R}] b↓ S{?Z{!R}} w↑ S{?Z{•}} → [ { } { }] w↑ [ { } {•}] w↑ [ {•} {•}] b↓ { {•}} S [?Z{!R} Z{!R}] w↑ S [?Z{!R} Z{•}] w↑ S [?Z{•} Z{•}] b↓ S{?Z{•}}
For π = g↑, we have

[ { } { }] b↓ { { }} g↑ { { }} S [?Z{!R} Z{!R}] b↓ S{?Z{!R}} g↑ S{?Z{!!R}} → [ { } { }] g↑ [ { } { }] g↑ [ { } { }] b↓ { { }} S [?Z{!R} Z{!R}] g↑ S [?Z{!R} Z{!!R}] g↑ S [?Z{!!R} Z{!!R}] b↓ S{?Z{!!R}}
And for π = b↑, we have

[ { } { }] b↓ { { }} b↑ { ( )} S [?Z{!R} Z{!R}] b↓ S{?Z{!R}} b↑ S{?Z(!R R)} → [ { } { }] b↑ [ { } ( )] b↑ [ ( ) ( )] b↓ { ( )} S [?Z{!R} Z{!R}] b↑ S [?Z{!R} Z(!R R)] b↑ S [?Z(!R R) Z(!R R)] b↓ S{?Z(!R R)}
In all three cases, the rule π is duplicated. But both copies have a smaller onion b-number in ∆ ′ . Hence rk ↑ (∆ ′ ) < rk ↑ (∆). As in case (iii.c.4) above, this crucially relies on the fact that the look-back tree of a vertex is acyclic. We also have rk ↓ (∆ ′ ) ≤ rk ↓ (∆) because the status of the b↓ could go down, and nothing else changes.

(d) The most interesting case is when ρ = p↓. We have the following situations:

(1) For π = g↑:

{ [ ]} p↓ [ ] g↑ [ , ] S{![R T ]} p↓ S [!R ?T ] g↑ S [!!R, ?T ] → { [ ]} g↑ { [ ]} p↓ { [ ]} p↓ [ ] g↓ [ ] S{![R T ]} g↑ S{!![R T ]} p↓ S{![!R ?T ]} p↓ S [!!R ??T ] g↓ S [!!R ?T ]
A single g↑ is replaced by a g↑ and a g↓. We clearly have rk ↑ (∆ ′ ) ≤ rk ↑ (∆) because the status of the g↑-instance could go down. If G !? (∆) is acyclic, then also its p-number goes down. Note that no other uprule changes its rank. We cannot make any statements about rk ↓ (∆). But, observe that if G !? (∆) is acyclic, then the p-number of the new g↓ is strictly smaller than the p-number of the original g↑. Hence, if G !? (∆) is acyclic, then rk(∆ ′ ) < rk(∆). Note that even in the case of acyclicity of G !? (∆), we do not have rk ↓ (∆ ′ ) ≤ rk ↓ (∆).

• 33

(2) For π = b↑:

{ [ ]} p↓ [ ] b↑ [( ) ] S{![R T ]} p↓ S [!R ?T ] b↑ S [(!R R) ?T ] → { [ ]} b↑ ( [ ] [ ]) p↓ ([ ] [ ]) s [([ ] ) ] s [( ) ] b↓ [( ) ] S{![R T ]} b↑ S(![R T ] [R T ]) p↓ S([!R ?T ] [R T ]) s S [([!R ?T ] R) T ] s S [(!R R) ?T T ] b↓ S [(!R R) ?T ] ( 17
)
This case is similar to the one for g↑ above, but slightly more complicated. The b↑-instance is replaced by a b↑ and a b↓. By this, it can happen that the onion b-number of other down rules in ∆ is increased. But note that no up-rule can change its onion b-number. (This is the reason for allowing one flipping edge in a path in the look-back tree in Definition 5.8, instead of forbidding any flipping edge. Note that cases (iii.c.4) and (iv.c) above would also work without the flipping edges in the look-back tree.) Since, as before, the status of the b↑ could go down, we have rk ↑ (∆ ′ ) ≤ rk ↑ (∆). But since the rank of some down-rules can become bigger, we cannot compare rk(∆ ′ ) with rk(∆).

Nonetheless, it is important to mention that if G !? (∆) is acyclic, then the p-number of the new b↓ is strictly smaller than the p-number of the original b↑.

(3) For π = w↑:

{ [ ]} p↓ [ ] w↑ [• ] S{![R T ]} p↓ S [!R ?T ] w↑ S [• ?T ] → {![R T ]} w↑ {•} = [• •] w↓ [• ?T ] S{![R T ]} w↑ S{•} = S [• •] w↓ S [• ?T ]
This case is simpler than the other two because the instance of p↓ disappears. Hence, we have rk ↑ (∆ ′ ) ≤ rk ↑ (∆) and if G !? (∆) is acyclic also rk(∆ ′ ) < rk(∆). But we do not have rk ↓ (∆ ′ ) ≤ rk ↓ (∆).

This case analysis is enough to show the following three lemmas.

Lemma 5.14 (Step 2 in Fig. 5).

Every derivation

P SNEL ′ ∆ Q can be transformed into P {g↑, b↑, w↑} P ′ SNEL ′ \ {g↑, b↑, w↑} Q .
Proof. This transformation is obtained by permuting all instances of g↑, b↑, w↑ to the top of a derivation as described in 5.13. In all cases, we have rk ↑ (∆ ′ ) ≤ rk ↑ (∆). Termination now follows for the same reasons as in the proof of Lemma 4.5. We use as induction measure the pair rk ↑ (∆), δ in a lexicographic ordering, where δ is the number of rule instances in the derivation above the topmost instance of g↑, b↑, or w↑ with status 1. If we always choose this topmost instance of g↑, b↑, or w↑ with status 1 for performing the next permutation step, then this measure always goes down (because whenever we have rk ↑ (∆ ′ ) < rk ↑ (∆) in Case Analysis 5.13, then δ is reduced by 1).

Lemma 5.15 (Step 2 in Fig. 5). (18)

Every derivation

Proof. The derivation ∆ ′ is obtained from ∆ by a sequence of transformations:

∆ = ∆ 0 ; ∆ 1 ; ∆ 2 ; ∆ 3 ; . . . ; ∆ ′ , (19)
where ∆ i+1 is obtained from ∆ i by permuting all instances of g↑, b↑, w↑ up to the top of the derivation if i is even, and by permuting all instances of g↓, b↓, w↓ down to the bottom of the derivation if i is odd. Each of these single steps is well-defined because of Lemma 5.14 and Lemma 5.15. Now assume i is even and i ≥ 2. Then there are no instances of g↑, b↑, or w↑ with status 1 in ∆ i+1 , and all instances of g↓, b↓, w↓ in ∆ i+1 have been introduced by case (iv.d) in 5.13. Hence, for each ρ ′ of the kind g↓, b↓, w↓ in ∆ i+1 , there is a ρ of the kind g↑, b↑, w↑ in ∆ i , with st ∆i (ρ) = 1 and p ∆i (ρ) > p ∆i+1 (ρ ′ ), and therefore rk ∆i (ρ) > rk ∆i+1 (ρ ′ ). Hence rk(∆ i ) > rk(∆ i+1 ). By a similar argument we can conclude that rk(∆ i ) > rk(∆ i+1 ) for all odd i with i > 1. Since the multiset ordering is well-founded, we can conclude that the process indicated in (19) terminates eventually. The resulting derivation ∆ ′ is of the desired shape (18).

Note that the argument in the previous proof is necessary because of case (iv.d.2) in 5.13. In all other permutation steps the rank does not increase.6

Forked and Unforced Cycles

As the derivation in (9) shows, we cannot hope for a lemma saying that G !? (∆) is always acyclic. Nonetheless, the decomposition terminates for (9), and the result is

• 35
shown in Figure 9. Since in that figure, the !-?-flow-graph is acyclic, the cycle must have been broken eventually. For understanding how this is happening, we will now continue with an investigation in the structure of cycles in the !-?-flow-graph, and how they are broken. Before, we exhibit another example of a derivation with a cycle in its !-?-flow-graph:

( [b a] [c d]) p↓, p↓ ([ b a] [ c d]) b↑ ( ([ b a] [ c d]) [ b a] [ c d]) s, s ( [ a ( b c) d] [ b a] [ c d]) s, s ( [ a ( b c) d] [ b ( a d) c]) p↑, p↑ ( [ a (b c) d] [ b (a d) c]) g↑ ( [ a (b c) d] [ b (a d) c]) !(![b a] ![c d]) p↓, p↓ !([?b !a] [!c ?d]) b↑ (!([?b !a] [!c ?d]) [?b !a] [!c ?d]) s, s (![!a (?b !c) ?d] [?b !a] [!c ?d]) s, s (![!a (?b !c) ?d] [?b (!a ?d) !c]) p↑, p↑ (![!a ?(b c) ?d] [?b ?(a d) !c]) g↑ (![!!a ?(b c) ?d] [?b ?(a d) !c]) (20)
This derivation can be used to explain why we have Steps 2 and 3 in the proof of Theorem 3.1 (see Figure 5), instead of doing something like

W1 SNEL ′ Z1 2 ′ ---→ W1 {g↑} W2 SNEL ′ \ {g↓, g↑} Z2 {g↓} Z1 2 ′′ ---→ W1 {g↑} W2 {b↑} W3 SNEL ′ \ {g↓, g↑, b↓, b↑} Z3 {b↓} Z2 {g↓} Z1 • • •

Running

Step 2 ′ on the derivation in (20) does indeed fail because of nontermination. If we apply all the transformations of 5.13 together with the ones in ( 5) and (6) (and their duals), then the instances of g↑ (and g↓) get caught in the cycle in (20), and the process will run forever. Only if the b↑ is permuted up together with the g↑, the process does terminate. The reason is that when the instance of b↑ is permuted over the two p↓ on the top of the derivation, the cycle is broken, because some edges in the !-?-flow-graph disappear. This shows the importance of case (iii.c.2) in 5.13, and motivates the following definition.

Definition 5.17.

A cycle c in G !? (∆) is called forked if there is an instance of S{!R} b↑ S(!R R) or S [?T T ] b↓ S{?T }
inside ∆ such that both copies of R of the redex of the b↑, or both copies of T in the contractum of b↓ contain vertices of the cycle. We say that such an instance of b↑ or b↓ forks the cycle c. The number of b↑ and b↓ that fork a cycle c is called the forking number of c, denoted by fk(c). A cycle c with fk(c) = 0 is called unforked.

[ The cycles in ( 9) and ( 20) are both forked. The one in (9) has forking number 2 (since both, the b↓ and the b↑ fork the cycle), and the cycle in (20) has forking number 1.

a a] b↑ ( [ a a] [ a a]) b↑ ( [ a a] [ a a] [ a a]) b↑ ( [ a a] [ a a] [( a a) a]) b↑ ( [ a a] [ a a] [( a a) a] [( a a) a]) b↑ ( [ a a] [ a a] [ a a] [( a a) a] [( a a) a]) p↓ ( [ a a] [ a a] [ a a] [( a a) a] [( a a) a]) p↓ ( [ a a] [ a a] [ a a] [( a a) a] [( a a) a]) p↓ ( [ a a] [ a a] [ a a] [( a a) a] [( a a) a]) p↓ ( [ a a] [ a a] [ a a] [ ( a a) a] [( a a) a]) s ( [ a a] [ a a] [ a a] [ ( a a) ( a [( a a) a])]) s ( [ a a] [ a a] [ a a] [ ( a a) ( a a) ( a a)]) s ( [ a a] [ a a] [ ( a a) ( a a) ([ a a] a a)]) s [( [ a a] [ a a] [ ( a a) ( a a)]) ([ a a] a a)] s [( [ a a] [ ( a a) ([ a a] a a)]) ([ a a] a a)] s [( [ a a] ( a a)) ([ a a] a a) ([ a a] a a)] p↑ [ ([ a a] a a) ([ a a] a a) ([ a a] a a)] s [ [([( a a) a] a)] ([ a a] a a) ([ a a] a a)] s [ [( a a) ( a a)] ([ a a] a a) ([ a a] a a)] s [ [( a a) ( a a)] ([( a a) a] a) ([ a a] a a)] s [ [( a a) ( a a)] ( a a) ( a a) ([ a a] a a)] s [ [( a a) ( a a)] ( a a) ( a a) ([( a a) a] a)] s [ [( a a) ( a a)] ( a a) ( a a) ( a a) ( a a)] p↑ [ [ ( a
( a a) !![!a a] b↑ (!![!a a] ![!a a]) b↑ (!![!a a] ![!a a] ![!a a]) b↑ (!![!a a] ![!a a] ![(!a a) a]) b↑ (!![!a a] ![!a a] ![(!a a) a] [(!a a) a]) b↑ (!![!a a] ![!a a] ![!a a] ![(!a a) a] [(!a a) a]) p↓ (![?!a !a] ![!a a] ![!a a] ![(!a a) a] [(!a a) a]) p↓ (![?!a !a] [?!a !a] ![!a a] ![(!a a) a] [(!a a) a]) p↓ (![?!a !a] [?!a !a] [?!a !a] ![(!a a) a] [(!a a) a]) p↓ (![?!a !a] [?!a !a] [?!a !a] [?(!a a) !a] [(!a a) a]) s (![?!a !a] [?!a !a] [?!a !a] [?(!a a) (!a [(!a a) a])]) s (![?!a !a] [?!a !a] [?!a !a] [?(!a a) (!a a) (!a a)]) s (![?!a !a] [?!a !a] [?(!a a) (!a a) ([?!a !a] !a a)]) s [(![?!a !a] [?!a !a] [?(!a a) (!a a)]) ([?!a !a] !a a)] s [(![?!a !a] [?(!a a) ([?!a !a] !a a)]) ([?!a !a] !a a)] s [(![?!a !a] ?(!a a)) ([?!a !a] !a a) ([?!a !a] !a a)] p↑ [?([?!a !a] !a a) ([?!a !a] !a a) ([?!a !a] !a a)] s [?[([(?!a !a) !a] a)] ([?!a !a] !a a) ([?!a !a] !a a)] s [?[(?!a !a) (!a a)] ([?!a !a] !a a) ([?!a !a] !a a)] s [?[(?!a !a) (!a a)] ([(?!a !a) !a] a) ([?!a !a] !a a)] s [?[(?!a !a) (!a a)] (?!a !a) (!a a) ([?!a !a] !a a)] s [?[(?!a !a) (!a a)] (?!a !a) (!a a) ([(?!a !a) !a] a)]
Lemma 5.18 (Step 2 in Fig. 5). Let ∆ be a derivation in SNEL ′ , and let ∆ ′ be the result of first permuting all g↓, b↓, w↓ down (via Lemma 5.15), and then permuting all g↑, b↑, w↑ up (via Lemma 5.14). If G !? (∆ ′ ) is cyclic, then G !? (∆ ′ ) contains an unforked cycle.

Proof. We show the following claim: If G !? (∆ ′ ) contains a cycle c with fk(c) = n for some n > 0, then it also contains a cycle c ′ with fk(c ′ ) = n -1. Clearly, the cycle c must be forked by n instances of b↓ that have all been introduced by the transformation shown in (17) (because first, all b↓ have been permuted down, and then all b↑ have been permuted up). Now consider the topmost b↓ that forks c. The introduction of this b↓ causes a duplication of all up-paths and down-paths through T (we are still referring to ( 17)). Furthermore, the continued up-permutation of the b↑ (that caused the introduction of the b↓) causes a duplication of all flipping edges connecting up-paths and down-paths through T (see cases (iii.c.2) and (iii.c.3) in 5.13). This is indicated on the left of Figure 10, which shows this topmost b↓ and the cycle c in bold lines. For every path starting or ending inside the right-hand side copy of T in the contractum of the b↓, we have a path starting or ending at the same place inside the left-hand side copy of T . Hence, from c, we can construct another cycle c ′ , which does not use the right-hand side copy of T , as it is visualized in bold lines on the right of Figure 10. Thus, the b↓ does not fork c ′ . Hence fk(c ′ ) = n -1. By induction on fk(c) it follows that G !? (∆ ′ ) must contain an unforked cycle.

Let us now state the key property of !-?-flow-graphs, that in the end makes the decomposition possible.

Theorem 5.19 (Step 2 in Fig. 5). There is no derivation ∆ in SNEL, such that G !? (∆) contains an unforked cycle.

The proof of this theorem, which is the final link for completing Step 2 in the decomposition, is the purpose of the next section.

Switch and Seq

The impossibility of unforked cycles in a !-?-flow-graph is caused by a fundamental property of derivations in MLL, which remains untouched by adding seq, and which is nothing but the acyclicity condition for MLL proof nets. However, under the presence of seq, the formulation of this acyclicity is a bit more complicated and the proof a bit more involved, since we cannot rely on the sequent calculus [Tiu 2006]. We state the property we need in the following lemma (a similar result has already been shown by Retoré [START_REF] Retoré | Pomset logic as a calculus of directed cographs[END_REF]): Lemma 5.20 (Step 2 in Fig. 5). Let n > 0 and let a 0 ,a 1 , . . . , a n-1 , b 0 , b 1 , . . . , b n-1 be 2n different atoms. Further, let W 0 , . . . , W n-1 , Z 0 , . . . , Z n-1 be structures, such that -W i = [a i b i ] or W i = a i ⊳ b i , for every i = 0, . . . , n -1, -Z j = (b j a j+1 ) or Z j = b j ⊳ a j+1 , for every j = 0, . . . , n -1 (where the indices are counted modulo n).

Then there is no derivation Remark 5.21. This lemma can be used to prove that every theorem of BV is also a theorem of pomset logic. The other direction is still an open problem.

Before giving the proof of Lemma 5.20, let us state and prove the second lemma of this section, which says that an unforked cycle in the !-?-flow-graph of a derivation ∆ can be transformed into a derivation ∆ as shown in ( 21) above. The basic idea is to remove from ∆ everything that does not belong to the cycle, and then construct ∆ such that the !-?-flow-graph of ∆ becomes the atomic flow-graph of ∆.

To make this technically precise, note that in every cycle c in a !-?-flow-graph, the following numbers are all equal:

-the number of maximal !-up-paths in c, -the number of maximal ?-down-paths in c, -the number of flipping edges in c from a !-vertex to a ?-vertex, and -the number of flipping edges in c from a ?-vertex to a !-vertex.

We call this number the characteristic number of c. For example, the cycle in the derivation in (9) has characteristic number 1, and the one in (20) has characteristic number 2.

Lemma 5.22 (Step 2 in Fig. 5). Let ∆ be a derivation in SNEL ′ such that G !? (∆) contains an unforked cycle c. Then there is a derivation

for some atoms a 0 , . . . , a n-1 , b 0 , . . . , b n-1 , where n > 0 is the characteristic number of c.

Proof. First, we transform ∆ into a derivation ∆ ′ which contains only rules from SNEL ′ \ {g↓, b↓, w↓, w↑} and in which the cycle is preserved. This is done by moving the rules g↓, b↓, and w↓ down in the derivation by applying Lemma 5.15, and by moving all instances of w↑ also down in derivation (by applying the dual of Lemma 4.6, together with (7)): • 39 Since c is unforked, no transformation step destroys the cycle, which is therefore still present in G !? (∆ ′ ). It cannot be inside G !? (∆ ↓ ) because there are no flipping edges. We continue the proof by marking some structures occurring in ∆ ′ :

-We start by marking all !-and ?-vertices of c by ! • and ? • , respectively. It cannot happen that a ! • -or ? • -structure occurs inside another ! • -or ? • -structure, as it is case in the example in (9), because for having such a situation the cycle must change its "!-?-depth" twice, once at a b↓, and once at a b↑, which is not possible since there are no b↓ in ∆ ′ . -Now we replace every ! • by ! • i and every ? • by ? • j for some i, j ∈ {0, . . . , n -1}, such that -two ! • -vertices in the same up-path get the same index, and two ? • in the same down-path get the same index, and -every flipping edge in c goes from a ! • i to a ? • i vertex, or from a ? • i to a ! • i+1 vertex, where the addition is modulo n. -Note that at every flipping edge from a ! • i to a ? • i vertex there is another edge in G !? (∆) also starting at ! • i , which continues the up-path marked by ! • i up to the top of the derivation. We mark all !-vertices on this path by ! i . Since there are no instances of b↓ left in ∆ ′ , the ! i up-path is never forked, and since there are no e↓ and no w↓ in ∆ ′ , this path does not end before the top of the derivation. Hence, the premise P of ∆ ′ contains exactly n substructures, marked by ! 0 , ! 1 , . . . , ! n-1 . Let us call them ! 0 W 0 , ! 1 W 1 , . . . , ! n-1 W n-1 . We also have n instances of p↓ in ∆, marked as follows:

S{! i [R T ]} p↓ S [! • i R ? • i T ] (23)
-Now we proceed similarly and mark the continuations of the ? • i -down-paths by ? i , i.e., we obtain n instances of p↑ marked as

S(? • i T ! • i+1 R) p↑ S{? i (T R)} (24)
However, note that now it can happen that we meet during the marking process a proper forking vertex, due to the presence of b↑:

S{ V { i T }} b↑ S( V { T } V { T }) S{!V {? i T }} b↑ S(!V {?T } V {?T }) .
then we continue the marking in only one side, namely, into that copy of V {?T } in the redex of b↑, that contains already a ! • -, ? • -, ! -, or ? -marking. Note that it cannot happen that both copies of V {?T } contain such a marking because the cycle is unforked. If neither side contains a marking, we arbitrarily pick one side. Since there are no e↑ and w↑ in ∆ ′ , the ? -paths cannot end in the middle of the derivation. Hence, the conclusion Q ′ of ∆ ′ contains exactly n different marked ? -structures, that we denote by ? 0 Z 0 , ? 1 Z 1 , . . . , ? n-1 Z n-1 . Now we remove in ∆ ′ every modality that is not marked, and we replace every atom that is not inside a marked structure by the unit •. The important point is that after this rather drastic change we still have a correct derivation. Every rule

PERSPECTIVES

We now briefly mention the developments that we expect to be based on this work. Much of the arguments that we use have similarities with the techniques developed for atomic flows [START_REF] Guglielmi | Normalisation control in deep inference via atomic flows[END_REF], with the important difference that, here, we are dealing with flows of modalities rather than atoms. Nonetheless, the similarities suggest that there might be a common structure that can perhaps be unveiled and exploited in future research.

The techniques developed here for decomposition might possibly be exported to the many modal logics already available in deep inference (some of which have no known analytic presentation in Gentzen formalisms).

Both for NEL and for other modal logics, it should be possible to use decomposition for investigating interpolation, which is a classical proof theoretic concern, and that relies on a similar kind of decomposition (we can consider Herbrand-like theorems as simple examples of decomposition).

We mentioned the applications of BV to process algebras and causal quantum evolution. We expect NEL to find uses in the same directions. In the case of process algebras, this is almost obvious, given that NEL is Turing-complete and that exponentials have been justified since their first introduction as ways of controlling resources (i.e., messages, processes). The logic BV has also been used to define BVcategories [START_REF] Blute | Deep inference and probablistic coherence spaces[END_REF] for providing an axiomatic description of probabilistic coherence spaces [START_REF] Girard | Between logic and quantic : a tract[END_REF]].

What we have in this paper is a basic compositional result, so, we expect applications to be very broad in range. That said, we think that, perhaps, the most important outcome of this whole research on seq and its logical systems is one of extending the limits of proof theory and of developing new insight and new techniques.

We witness here an interesting phenomenon: on one hand, we have a very simple system in a very simple formalism (i.e., NEL in the calculus of structures); on the other hand, we have a very simple property, decomposition. In the middle, connecting the two, there's a rich and complex combinatorial phenomenon. Sometimes, in similar situations, the mathematics that arises has some lasting value, and this is our hope for this paper.

Fig. 4 .

 4 Fig. 4. Readings of the decompositions

Fig. 5 .

 5 Fig. 5. Obtaining the third and fourth decomposition

Fig. 6 .

 6 Fig. 6. Obtaining the first and second decomposition

Fig. 7 .

 7 Fig. 7. The analysis of critical pairs for local confluence and the permutability of rules

  Analysis 4.14 (for permuting g↑, b↑, w↑ up). Consider a derivation SNEL \ {g↑, b↑, w↑, e↓, e↑} and π ∈ {g↑, b↑, w↑}. The trivial cases (i) and (ii) are as in the proof of Lemma 4.3. Then there is another (almost) trivial case which does not correspond to a case in the proof of Lemma 4.3.

Fig. 8 .

 8 Fig. 8. Edges in the !-?-flow-graph

  Dual to the previous lemma.Lemma 5.16 (Step 2 in Fig.5). If the !-?-flow-graph of a derivationP SNEL ′ ∆ Q is acyclic, then ∆ can be transformed into a derivation ∆ ′ Q {g↑, b↑, w↑} Q ′ {ai↓,ai↑, s, q↓, q↑, p↓, p↑} P ′ {g↓, b↓, w↓} P .

  a) ( a a)] ( a a) ( a a) ( a a) ( a a)] p↑ [ [ ( a a) ( a a)] ( a a) ( a a) ( a a) ( a a)] p↑ [ [ ( a a) ( a a)] ( a a) ( a a)

  Fig. 9. Result of applying the decomposition to the derivation in (9)

Fig. 10 .

 10 Fig. 10. The basic idea of the proof of Lemma 5.18

(

  [a0 b0 ] [a1 b1 ] . . . [an-2 bn-2 ] [an-1 bn-1 ]) {s, q↓, q↑} ∆ [(b0 a1) (b1 a2) . . . (bn-2 an-1) (bn-1 a0)]

  {g↓, b↓, w↓, w↑} ∆ ′ Q ′ {g↓, b↓, w↓, w↑} ∆ ↓ Q . ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

•

  Lutz Straßburger and Alessio Guglielmi vertices in its onion, i.e.,

	b ∆

ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY, Pages 1-43.

Please note that we slightly change the syntax with respect to[Guglielmi

[START_REF] Guglielmi | A system of interaction and structure[END_REF] Tiu 2006]: In these papers commas where used in the places of the connectives , , and ⊳. Although there is some redundancy in having the connectives and the three different types of brackets, we think, it is easier to parse for the reader.ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

For complexity issues related to the use of equations see[START_REF] Bruscoli | On the proof complexity of deep inference[END_REF].ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

Note that there is a change of our system with respect to the system SELS in[Straßburger 2003b] and the version of SNEL presented in[START_REF] Guglielmi | A non-commutative extension of MELL[END_REF]]: Here we have added the rules e↓, e↑, g↓, and g↑, whereas previously we used the equations ??R = ?R and !!R = !R, as well as !• = • = ?• in[START_REF] Guglielmi | A non-commutative extension of MELL[END_REF] and !1 = 1 and ?⊥ = ⊥ in[Straßburger ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

This is similar to the permutation lemmas in[Straßburger 2003b], but in here the situation is a bit more complicated than in MELL because of the collapse of the units 1 = • = ⊥.ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

A complete list of all possible cases can be found in[Straßburger 2003a].ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

The paper[Straßburger 2003b] contains statements for MELL that are similar to Lemmas 5.14- 5.16, but the proofs here are simpler, due to the use of the rank in the measure for ensuring termination.ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

Acknowledgments

The referees provided unusually deep and outstanding suggestions for making this paper more accessible and, in general, better. We would like to thank Luca Roversi for the extremely insightful and technical comments, and the numerous discussions on this subject, which greatly helped us understand the matter.

instance in ∆ ′ remains valid, or becomes vacuous, i.e., premise and conclusion are identical. Note that here we make crucial use of the fact that the cycle is unforked: Doing this deletion to a b↑ which forks c would yield an incorrect inference step.

Let us call the new derivation ∆ ′′ . Its premise P ′′ is made from the structures ! 0 W 0 , ! 1 W 1 , . . . , ! n-1 W n-1 by using only the binary connectives , ⊳ , and , and its conclusion Q ′′ s made from ? 0 Z 0 , ? 1 Z 1 , . . . , ? n-1 Z n-1 by using only , ⊳ , and . Now note that for arbitrary structures A and B, we have the following three derivations:

and

and

Hence, we can extend ∆ ′′ as follows:

{q↑, s}

Let us use ∆ ′′′ to denote the derivation in (25). We finally obtain ∆ from ∆ ′′′ by replacing every ! • i -structure by a i , every ? • i -structure by b i , every ! i -structure by [a i b i ], and every ? i -structure by (b i , a i+1 ). Clearly, every inference rule remains valid, or becomes vacuous, as for example the instances of p↓ in (23) and p↑ in (24):

and S(?

If a rule does not become vacuous, it must be one of s, q↓, and q↑.

Proof of Lemma 5.20. The proof is carried out by induction on the pair n, q , where q is the number of seq-structures in the conclusion, and we endorse the lexicographic ordering on N × N. The base case (i.e., n = 1) is trivial. For the inductive case we assume by way of contradiction the existence of the derivation ∆ in (21) and consider the bottommost rule instance ρ. There are three cases.

(i) ρ = q↑. There is only one possibility to apply this rule:

We can apply the induction hypothesis to ∆ ′ because the number n did not change and the number q of seq-structures in the conclusion did decrease by ACM Transactions on Computational Logic, Vol. V, No. N, Month 20YY.

A System of Interaction and Structure IV: The Exponentials and Decomposition

• 41

1. Hence we get a contradiction. (ii) ρ = q↓. There are several possibilities to apply this rule. We show here only two representative cases and leave the others to the reader because they are very similar. The complete case analysis can be found in [Straßburger 2003a].

(a) If we have

then ∆ ′ remains valid if we replace a m and b m by • for every m > i and for m = 0. This gives us the derivation

which is a contradiction to the induction hypothesis because i < n. (b) Consider

where {1, . . . , n -1} \ {k 1 , . . . , k v } = {h 1 , . . . , h s } and s = n -v -1 and (without loss of generality) k 1 < k 2 < . . . < k v . As before, the derivation ∆ ′ remains valid if we replace a m and b m by • for every m with 1 ≤ m ≤ k v . Then we get

which is (as before) a contradiction to the induction hypothesis because v ≥ 1. (iii) ρ = s. This is similar to the case for q↓. But note that a situation like in (ii.a) cannot happen for s.

Proof of Theorem 5.19. The existence of an unforked cycle in G !? (∆) implies by Lemma 5.22 the existence of a derivation as in (22). By Lemma 5.20, this is impossible. Now we can complete the proof of Theorem 3.1 by proving the following lemma.

Lemma 5.23 (Step 2 in Fig. 5).

Step 2 in the proof of Theorem 3.1 can be performed as indicated in Figure 5.

Proof. We can first permute all g↓, b↓, w↓ down, by applying Lemma 5.15, and then permuting all g↑, b↑, w↑ up, by applying Lemma 5.14. The result has an acyclic !-?-flow-graph (otherwise, it would have by Lemma 5.18 an unforked cycle, which is impossible by Theorem 5.19). Hence, we can apply Lemma 5.16.