A repetition is a pair \( (u ,v) \in P \times P \) of vertices labelled by the same a-sequent such that \( u < v \).
As \( \alpha \) is guarded, if \( ( u , v ) \) is a repetition then there is a vertex \( w \in [ u , v) \) such that \( \rul r_w = (\square ) \).
As observed, every branch of the pre-template contains infinitely many repetitions.
For the present construction, the invariant of a repetition \( ( u , v ) \) will be a pair \( ( c , k ) \in \ann \times \setof{ 0,1 } \) where \( c \) is a non-trivial prefix of all controls on the path interval \( (u,v) \) and \( k \) records whether the final name in \( c \) is covered in one of these sequents (in which case \( k = 0 \)).
If there is no such control, then \( c \) is the longest prefix of all controls and \( k = 1 \).
Thus, the invariant of a repetition \( (u , v) \) is the pair \( \inv {u,v} = ( c , k ) \in \ann \times \setof{ 0,1 } \) where:

* \( c \) is the longest annotation that is a prefix of every vertex in the path segment \( [ u , v ] \) and is such that if \( \rul r_w = (\cover^{c(i)}) \)  for some \( w \in [u , v ) \) then \( i = \lh c - 1 \),

* \( k = 0 \) iff \( \rul r_w = (\cover^{c(i)}) \) for some \( w \in [ u , v ) \) and \( i < \lh{c} \).

Invariants are compared lexicographically:
\( ( c , k ) \sqsubseteq ( d , l ) \) iff \( c < d \) or \( c = d \) and \( k \le l \).
In particular, \( ( c , 1 ) \sqsubseteq ( d , 0 ) \) iff \( c \) is a proper prefix of \( d \).
The relation \( \sqsubseteq \) forms a partial order on invariants.

Assume a companion function on \( P \) is available, i.e., a partial function \( u \mapsto u^c \) such that if \( u^c \) is defined then \( ( u^c , u ) \) is a repetition.
If \( u^c \) is defined we write \( \inv u \) for \( \inv {u^c , u} \).
The companion function induces a more liberal `reachability' relation \( \rightsquigarrow \) on \( P \) by \( u \rightsquigarrow v \) iff \( u^c \) and \( v^c \) are both defined and \( u^c \le v^c < u \).
Note, \( \rightsquigarrow \) is not transitive in general.
However, if \( u \rightsquigarrow v \) then \( \inv u \) and \( \inv v \) are comparable: \( \inv { u } \sqsubseteq \inv { v } \) or \( \inv { v } \sqsubseteq \inv { u } \).
The template is given by a choice of companion function such that the two orderings are in agreement:

A template of \( \alpha \) is a finite initial subderivation \( T \subseteq P \) and a companion function \( u \mapsto u^c \) defined on the buds of \( T \) such that if \( u \rightsquigarrow v \) for buds \( u , v \) then \( \inv u \sqsubseteq \inv v \).

Existence of a template \( T \) of \( \alpha \) is straightforward and can be obtained by isolating the buds of \( T \) by recursion through the finitely many invariants in \( P \).
Any template implicitly witnesses regularity of the pre-template in the sense that for every bud \( u \in T \) the maximal sub-derivations of \( P \) rooted at \( u \) and \( u^c \) are identical.

In the following we assume a fixed template of \( \alpha \), denoted \( T \).
A bud \( u \) is successful if its invariant \( \inv u = ( c , 0 ) \) for some \( c \); otherwise \( u \) is unsuccessful.
If \( u \) and \( v \) are buds with the same companion, then \( \inv u = \inv v \), so \( u \) is successful iff \( v \) is successful.
Thus we can unambiguously refer to a companion \( u^c \) as (un)successful if \( u \) is (un)successful.

We now proceed with the definition of the conjunctive formula \( \gamma \).
As discussed, this formula simply encodes the pre-template of \( \alpha \) via the chosen template.
We assume a distinct variable \( x_u \) is available for each vertex \( u \in T \), let \( \rul r_u \) be the rule labelling \( u \) and let \( \Phi_u \) be the set of formulas labelling \( u \in T \) with all annotations removed.
The construction of \( \gamma \) proceeds by associating to each \( u \in T \) conjunctive formulas \( \alpha_u \) and \( \beta_u \) in the following way.
An example of the association is given in fig. <ref>.

ϵ: ∅
1[$\square ^*$] ϵ: ∅
ϵ: α
2[$\square ^*$] ϵ: □α
1[$\mu $] ϵ: α
1[$\cw$] n : α
n : ♢α, □[n] ϕ
1[$\dup$] n : ♢α, ♢α, □[n] ϕ
1[$\disj$] n : ♢α, ϕ( [n] ϕ)
1[$\cover$] n m : ♢α, ϕ( [nm] ϕ)
1[$ \nu ^m$] n : ♢α, [n] ϕ
1[$\mu $] n : α, [n] ϕ
2[$\square ^*$] n : ♢α, □[n] ϕ
1[$\disj$] n : ♢α∨□[n] ϕ
1[$\nu ^n$] ϵ: νϕ

1 μx.  ♢x
[separation=4em]2 □y ∨♢( y ∧μx .  ♢x )
1 μψ
1 μψ
1 z
1 z
1 z
1 z
1 z
[separation=3em]2 νz.  □z ∨♢( z ∧μψ)
1 νz.  □z ∨♢( z ∧μψ)
1 νz.  □z ∨♢( z ∧μψ)

An example of a template (left) for the formula \( \nu  \phi \) where \( \phi = \lambda  x.\, \diamond\alpha \vee \square  x \) and \( \alpha = \mu  x.\, \square  x \). On the right is the corresponding conjunctive companion showing the formula \( \alpha_u \) induced by each vertex of the template, and \( \psi \) abbreviates \( \lambda  y.\, \square  y \vee \diamond ( y \wedge \mu  x .\, \diamond x ) \).

The formulas \( \alpha_u \) and \( \beta_u \) are defined by recursion through \( u \in T \).
Assuming that \( \beta_u \) is defined, set

\[ \alpha_u \coloneqq
\begin{cases}
\nf x_u \, \beta_u, &\text{if \( u \) is successful,}
\\
\mf x_u \, \beta_u, &\text{otherwise.}
\end{cases} \]

The formula \( \beta_u \) is built from the formulas \( \setof{\alpha_v}[v \in \Suc [T] u] \) in a way determined by the rule at \( u \in T \).
Assume that \( \alpha_v \) is defined for each \( v \in \Suc[T]u \).

* If \( u \) is a bud, set \( \beta_u = x_{u^c} \).

* If \( \rul r_u = (\conj) \), define \( \beta_u = \conj \setof{ \alpha_v }[v\in \Suc[t]{u}] \).

* If \( \rul r_u = (\square ^*) \) and \( \Phi_u \) contains both \( x , \neg x \) for some variable \( x \) then \( \beta_u = \top \).

* If \( \rul r_u = (\square ^*) \) and \( \Phi_u \) is not of the form above then \( \beta_u = \Gamma \supp[L] \conj \Delta \) where \( \Gamma \), \( \Delta \) and \( L \) are given as follows.
As \( \Phi_u \) is modal, let \( \Phi_u = L , \diamond\Psi , \square \delta_1 , \dotsc, \square \delta_n \) where \( L \subseteq \Lit \) and let \( \Suc[T] u = \setof{ u_0 , \dotsc , u_n } \) such that \( \Phi_{u_0} = \Psi \) and \( \Phi_{u_i} = \Psi , \delta_i \).
Set \( \beta_u = \Gamma \supp[L] \conj \Delta \) where \( \Gamma = \setof{ \alpha_{u_{i}} }[ 1 \le i \le n ] \) and \( \Delta = \Gamma \cup \setof{ \alpha_{u_{0}} } \).

* In all other cases \( u \) has exactly one child \( u^+ \), whence define \( \beta_u = \alpha_v \).

This concludes the definition of formulas \( \alpha_u \) and \( \beta_u \).

The conjunctive companion to a guarded formula \( \alpha \) is the formula \( \gamma \coloneqq \alpha_\epsilon \) associated to the root of the template as per the previous definition.
More generally, the conjunctive formula associated to a vertex \( u \in T \) is the formula

\[ \gamma_u \coloneqq \alpha_u \subs[x_{u_n}]{ \alpha_{u_n} } \dotsm \subs[x_{u_1}]{ \alpha_{u_1} }
\]

where \( \epsilon = u_1 < \dotsm < u_n < u \) enumerate the ancestors of \( u \).
The conjunctive companion to a non-guarded formula is the conjunctive formula associated to the canonical guarded equivalent formula determined by proposition <ref>.

We begin with a few useful observations.

For \( \gamma_u \) defined as above,

* \( \gamma_u \) is a guarded conjunctive formula.

* If \( u \in T \) is axiomatic then \( \kmm \vdash \gamma_u \).

* If \( u \rightsquigarrow v \) then \( \gamma_u \sf_{\gamma_v} \gamma_v \).

§.§ Validation

With \( \gamma \) as the conjunctive companion to \( \alpha \) defined as above we establish the two properties of theorem <ref>: \( \alpha \Vdash \gamma \) and \( \gamma \Vdash \alpha \).
Both admissibility claims are witnessed by tight co-proofs of the corresponding sequents.
The two co-proofs are similar in construction.
As the latter is a more involved argument, we present it in detail and sketch the verification of the other claim.
Both claims are implicit in the results of <cit.>.

The \( \neg{\gamma} \)-tight co-proof of \( \gamma \Rightarrow \alpha \) will be such that the \( \alpha \)-descendants of each vertex will match the annotated formulas at a corresponding vertex of the pre-template for \( \alpha \).
To confirm that each branch of the co-proof carries a good thread it is necessary to trace branches of the pre-template \( P \) in the template \( T \).
Regularity of the pre-template means that every \( u \in P \setminus T \) has the form \( u = v w \) where \( v \) is a bud of \( T \) and \( v^c w \in P \).
Thus, the companion function of \( T \) induces a canonical projection \( p \colon P \to T \colon u \mapsto u^p \) of \( P \) into \( T \) defined as: if \( u = v w \) for a bud \( v \in T \) then \( u^p = ( v^c w )^p \); otherwise \( u^p = u \).
Note that \( u^p \) is never a bud of \( T \).

We rely on the following observation relating invariants to the existence of good threads in the pre-template.
Recall that a non-bud vertex is successful iff it is the companion to a successful bud.

Let \( B \) be a branch of the pre-template of \( \alpha \) and let \( u_B \in T \) be the \( \le \)-minimal vertex such that \( u_B = B(i)^p \) for infinitely many \( i \).
Then \( B \) carries a good thread (in the sense of the unannotated calculi where \( (\dup) \) is interpreted as weakening) iff \( u_B \) is a successful companion.

For the proof of the proposition it is helpful to fix invariants to companions.
Since buds with the same companion are associated identical invariants we can, without confusion, refer to the invariant of a companion.

Let \( B^p \) be the vertices in \( T \) that are projection of infinitely many vertices in \( B \).
Let \( C_B \) be the set of companions in \( B^p \).
There is a unique \( \le \)-minimal element of \( B^p \) and this is also an element of \( C_B \).
Let \( u_B \) be this vertex and \( ( c , k ) \) the associated invariant.
By the choice of \( T \), for every \( v \in C_B \) we have \( \inv {u_B} \sqsubseteq \inv v \).
Let \( c_B \) be the longest prefix of all controls for vertices in \( B^p \).
In particular, \( c \le c_B \).
Henceforth, we treat only the template and pre-template rooted at \( u_B \) and assume \( B(0) = u_B \).

Suppose \( B \) carries a good thread and, seeking a contradiction, that \( k = 1 \).
So \( c_B = c \).
Consider the plain formula \( \nf \phi \) of least rank for which annotations occur infinitely often in the thread and let \( \tau \) be the suffix of the thread in which all formulas have rank at least \( \rk{\nf \phi} \).
Let \( ( \nf[a_i] \phi_i )_i \) enumerate the annotations of \( \nf \phi \) through which \( \tau \) passes.
Linearity of the annotations means that \( \phi_i = \phi_j \) for all \( i,j \). Let \( \psi = \phi_0 \).
Let \( a \) be the longest common prefix among the \( a_i \).
Consider the vertex at which \( \nf[a_i] \psi \) is principal. The minor formula of this rule is the a-formula \( \psi(\nf[a_i n] \psi) \) for some name \( n \) that is not in the control of the conclusion.
As \( \nf[a_{i+1}] \psi \) is a descendent of \( \psi(\nf[a_i n] \psi ) \) in the pre-template \( P \), we have that either \( a_i < a_{i+1} \) or there is a sequent on the path between the two formulas at which a name in \( a_i \) is covered.
Given that there are finitely many annotations in the template, there is a shortest annotation \( a \) such that \( a = a_i \) for infinitely many \( i \) and the last name in \( a \), say \( m \), must be covered in some sequent in \( B^p \).
Since \( a \) is the prefix of an annotation that occurs in every sequent in \( B^p \) it follows that \( a \) is a subsequence of \( c_B \).
But then the invariant of the repetition \( ( v^c, v) \) that surrounds the instance of \( (\cover^m) \) must have invariant \( ( c , 0 ) \), contradicting that \( \inv {u_B} \sqsubseteq \inv v \).

For the converse direction, suppose \( \inv {u_B} = ( c , 0 ) \).
Let \( n \) be the final name in \( c \) and
consider the tree of a-formula traces through \( B \) that follow only formulas in which \( n \) occurs.
By the choice of \( u_B \), \( n \) occurs in all controls of \( B^p \), whence  this tree of traces is infinite.
By weak König's lemma there is therefore an infinite such a-formula trace. Call this \( t \).
From the assumption that \( u_B \) is successful, some instance of \( (\cover^n) \) is applied infinitely often in \( B \).
For this to be the case, \( t \) must infinitely often pass through a formula in which \( n \) is covered, whence \( t \) must pass through a formula \( \nf[an] \phi \) followed by \( \phi(\nf[anm] \phi) \) infinitely often for some \( a \) and \( m \).
Linearity of the annotations enforces that it is specifically the formula \( \nf[an] \phi \) which witnesses that \( t \) carries a good thread.

\( \gamma \Vdash \alpha \).

The desired tight co-proof \( \pi \) can be obtained directly from the template of \( \alpha \) by essentially replacing the sequent \( \Phi_u \) labelling each \( u \in T \) by \( \gamma_u \Rightarrow \Phi_u \) and viewing the result as a maximal derivation in \( \kmo \) by identifying buds with their companions.
That every branch of \( \pi  \) carries a good thread is guaranteed by the choice of \( \gamma \): If a branch of \( \pi \) does not carry a good \( \alpha \)-thread then, by virtue of proposition <ref> the unique \( \neg{\gamma} \)-thread carried by the branch will be good.

We present the definition of \( \pi \) in more detail.
For \( u \in T \), let \( \alpha_u \), \( \beta_u \) be as in definition <ref> and let \( \Phi_u \) be the formulas in the sequent at \( u \) with annotations removed.
For each \( u \in T \), define \( \hat{\beta}_u \) to be the subformula of \( \gamma_u \) corresponding to the choice of \( \beta_u \), namely the following formula where \( \epsilon = u_1 < \dotsm < u_n < u \) is an enumeration of the ancestors of \( u \):

\[
\begin{aligned}
\hat{\beta}_u &\coloneqq \beta_u \subs[x_u]{ \alpha_u } \subs[x_{u_n}]{ \alpha_{u_n} } \dotsm \subs[x_{u_1}]{ \alpha_{u_1} }
\\
&\thinspace = \beta_u\subs[x_{u_n}]{ \alpha_{u_n} } \dotsm \subs[x_{u_1}]{ \alpha_{u_1} } \subs[x_u]{ \gamma_u }
&&\text{by definition of $\gamma_u$.}
\end{aligned}
\]

We define for each \( u \in T \) a derivation \( d_u \) with endsequent \( \gamma_u \Rightarrow \Phi_u \). The desired proof \( \pi \) results from transforming \( d_\epsilon \) into a maximal derivation.
Suppose \( d_v \) (with endsequent \( \gamma_v \Rightarrow \Phi_v \)) is defined for all \( v \in \Suc [T] u \).
The construction of \( d_u \) proceeds by case distinction on the rule labelling \( u \) in \( T \):

Case bud. For \( u \in T \) a bud \( d_u \) is the trivial derivation comprising the sequent \( \gamma_u \Rightarrow \Phi_u \).

Case \( \boldsymbol{(\conj)} \). In this case \( \beta_u = \conj\setof{ \alpha_v }[v \in \Suc[T]{u}] \).
For each \( v \in \Suc [T] u \), \( d_v \) is a derivation with endsequent \( \gamma_v \Rightarrow \Phi_v \). A derivation of \( \hat{\beta}_u \Rightarrow \Phi_u \) is obtained in the natural way:

\[
\begin{prooftree}
\subproof[d_v]{\gamma_v \Rightarrow \Phi_v }
\infer1[$\disj$]{ \hat{\beta}_u \Rightarrow \Phi_v }
\hypo{\text{each } v \in \Suc [T] u }
\infer[separation=1ex]2[$\conj$]{ \hat{\beta}_u \Rightarrow \Phi_u }
%		\delims{e = \left\{}{\right.}
\infer1[$\mu  $ or $ \nu  $]{ \gamma_u \Rightarrow \Phi_u }
\end{prooftree}
\]

The instances of \( (\disj) \) are all tight.
Observe that \( \sigma  = \mu  \) iff \( u \) is a successful companion.

Case $\boldsymbol{(\square ^*)}$.
Let \( \Phi_u = \diamond \Psi , \square \delta_1 , \dotsc, \square \delta_n, L \) where \( L \subseteq \Lit \).
Following the notation of the construction, we have either \( \hat{\beta}_u = \top \) or \( \hat{\beta}_u = \setof{ \gamma_{u_1} , \dotsc, \gamma_{u_n} } \supp[L] \conj \setof{ \gamma_{u_0} , \dotsc, \gamma_{u_n} } \) where \( u_0 , \dotsc, u_n \) enumerate the children of \( u \) starting with the child with no minor formula.
In the former case, \( \Phi_u \) is axiomatic and we are done; in the latter case, \( d_u \) is given as the derivation:

[$l$]l ⇒Φ_u
(each  l ∈L)
[d_u_i] γ_u_i    ⇒Ψ, δ_i
1[$\square $] □γ_u_i    ⇒Φ_u
(each  i > 0 )
[d_u_0] γ_u_0    ⇒Ψ
1[$\disj$]  γ_u_0 , …, γ_u_n     ⇒Ψ
1[$\square $] ♢ γ_u_0 , …, γ_u_n     ⇒Φ_u
5[$\conj$] β̂_u ⇒Φ_u
1[$ \mu  $ or $ \nu  $] γ_u ⇒Φ_u

Other cases. The other rules are all unary and \( \hat {\beta}_u = \gamma_v \) in each case where \( v \) is the unique successor of \( u \). The construction of \( d_u \) simply repeats the corresponding rule in \( T \) and, as in the cases above, inserts a fixed point rule to obtain \( \gamma_u \) from \( \hat{\beta}_u \). In the case that the rule at \( u \) is \( (\disj) \), \( d_u \) is:

\[
\begin{prooftree}
\subproof[d_v]{ \hat{\beta}_u \Rightarrow \Phi_v }
\infer1[$\disj$]{ \hat{\beta}_u \Rightarrow \Phi_u }
\infer1[$\mu  $ or $ \nu  $]{ \gamma_u \Rightarrow \Phi_u }
\end{prooftree}
\]

With \( d_\epsilon \) defined, let \( \pi \) be the maximal \( \kmo \)-derivation obtained by identifying buds with their companions.
This operation forms a derivation as \( \gamma_u = \gamma_{u^c} \) and \( \Phi_u = \Phi_{u^c} \) for each bud-companion pair \( ( u, u^c) \) in \( T \).

The converse admissibility claim is similar.

\( \alpha \Vdash \gamma \).

By recursion through the template an \( \neg{\alpha} \)-tight derivation of \( \alpha \Rightarrow \gamma \) can be constructed such that every sequent has the form \( \gamma \Rightarrow \gamma_u \) for some \( \gamma \in \Phi_u \).
Now consider a branch \( B \) through this derivation.
By design the branch carries a thread \( \tau \) with \( \tau(0) = \neg{\alpha} \). Assume \( \tau \) is not good.
Let \( B' = (u_i)_i \) be the corresponding branch through the pre-template, i.e., \( B(i) \) is labelled by \( \gamma_{i} \Rightarrow \gamma_{u_i} \) where \( \gamma_i \in \Phi_{u_i} \).
In particular, \( \neg{\tau} \) is a good thread carried by \( B'  \), whence proposition <ref> implies that the weak thread \( (\alpha_{u_i})_i \) is good.

§ COMPLETENESS

We establish completeness of \( \cmu \) and \( \kmu \) by associating to each formula \( \alpha \) an equivalent \( \SC \)-formula \( \hat{\alpha} \) such that \( \cmu\vdash \seq{\hat{\alpha}}{\alpha} \).
A natural candidate for \( \hat{\alpha} \) is the conjunctive formula of the previous theorem.
While this choice is sufficient (and is essentially the choice in <cit.>), the argument for \( \cmu \vdash \hat{\alpha} \Rightarrow \alpha \) can be streamlined by a more sophisticated choice.

We define the companion formula \( \hat{\alpha} \) by induction on \( \alpha \).
Let \( \alpha_c \) be the conjunctive companion of \( \alpha \).

* If \( \alpha \) is atomic, \( \hat{\alpha} \coloneqq \alpha \).

* If \( \alpha = \bigcirc\Gamma \) for \( \bigcirc \in \setof{ \disj, \conj } \), then \( \hat{\alpha} \coloneqq \bigcirc\setof{ \hat{\gamma} }[\gamma \in \Gamma] \).

* If \( \alpha = \triangle \beta \) for \( \triangle \in \setof{ \square   , \diamond  } \), then \( \hat{\alpha} \coloneqq \triangle  \hat{\beta} \).

* If \( \alpha = \mf \phi \), then \( \hat{\alpha} \coloneqq \mf {\hat{\phi}} \) where \( \hat{\phi} = \lambda  x.\, \widehat{\phi x} \).

* If \( \alpha = \nf \phi \), then \( \hat{\alpha} \coloneqq (\nf {{\phi}})_c \).

Definition <ref> applies the conjunctive normal form theorem at most once to each subformula of \( \alpha \). That is, for \( \alpha \in \SF F \) we have \( \hat{\alpha} \in \SF {\hat F} \) where \( \hat F = \setof{ \hat{\gamma} }[\gamma \in F] \).

In the following let \( \alpha \) be any formula and \( \hat{\alpha} \) its companion in \( \SC \).

\( \hat{\alpha} \in \SC \) and \( \alpha \VdashV \hat{\alpha} \).

By definition and corollary <ref>.

\( \cmu\vdash \seq{\alpha}{\hat{\alpha}} \).

Theorem <ref> on account that \( \alpha \Vdash \hat{\alpha} \) and the latter formula is \( \SC \).

\( \cmu \vdash \seq{\hat{\alpha}}{\alpha} \).

By induction on \( \alpha \). We present the case that \( \alpha \) is quantified; the other cases being straightforward.
Let \( \vdash \) denote provability in \( \cmu \).

Suppose \( \alpha = \mf \phi \). Then \( \hat{\alpha} = \mf \hat{\phi} \) and the induction hypothesis yields \( \vdash \hat{\phi} x \Rightarrow \phi x \).
So \( \vdash \hat{\phi} \alpha \Rightarrow \alpha \) by substitution and \( \vdash \seq{\hat{\alpha}}{\alpha} \) by simulated induction (figure <ref>).

Now suppose \( \alpha = \nf \phi \).
The definition of \( \hat{\alpha} \) and applications of corollary <ref> yields

\[
\hat{\alpha}
\Vdash \nf \phi
\Vdash \phi(\nf {\phi})
\Vdash \hat{\phi} \hat{\alpha} .
\]

As \( \hat\phi \hat\alpha \in \SC \), theorem <ref> implies \( \vdash \hat{\alpha} \Rightarrow \hat{ \phi } \hat { \alpha } \).
An application of simulated induction yields \( \vdash \hat{\alpha} \Rightarrow \nf {\hat{\phi}} \).
From the induction hypothesis and corollary <ref> we obtain also \( \vdash \nf {\hat{\phi}} \Rightarrow \alpha \).
Thus \( \vdash \hat{\alpha} \Rightarrow {\alpha} \).

If \( \kmo \vdash \alpha \) then \( \cmu \vdash \alpha \).

By h-admissiblity we have \( \kmo \vdash \hat{\alpha} \), whence \( \cmu \vdash \hat{\alpha} \) by theorem <ref>. An application of the previous proposition implies \( \cmu \vdash \alpha \).

\( \cmu \) and \( \kmu \) are complete.

Corollary <ref> and theorems <ref> and <ref>.

§ THREAD MATTERS

This section collects some basic properties of threads appealed to in the main paper.

For every thread \( \tau \colon \alpha \sf \beta \) there exist threads \( ( \tau_i \colon \alpha_i \sf \beta_i )_{i \le n} \) such that:

* \( \alpha_0 = \alpha \) and \( \beta_{i} = \mnf[\sigma_{i+1}] x_{i+1} \alpha_{i+1} \) for each \( i < n \),

* each \( \tau_i \) strictly decreases in rank: \( \rk{\tau_i({j+1})} < \rk{\tau_i(j)} \) for all \( j < \lh {\tau_i} \) and \( i \le n \),

* \( \tau(j) = \tau_k(j_k) \subs[x_{k-1}]{\beta_{k-1}} \dotsm \subs [x_0]{\beta_0} \) where \( j_k < \lh{\tau_k} \) is such that \( j = \sum_{i<k} \lh{\tau_i} + j_k \).

Induction on \( \lh \tau \).
Let \( \phi_0 = \lambda  x_0 \alpha \) where \( x_0 \) does not occur in \( \alpha \).
If \( \lh{\tau} = 1 \) then \( \beta = \alpha \) and the claim holds with \( n=0 \) and \( \gamma = \alpha \).
Otherwise, \( \lh{\tau} > 1 \). Let \( n \ge 0 \), \( (\sigma _i \phi_i)_{i\le n} \) and \( (\tau_i)_{i\le n} \) be given by applying the induction hypothesis to the prefix of \( \tau \) lacking its final component.
We compare the penultimate formula in \( \tau \) with \( \beta \). Let \( l = \lh{\tau} - 1 \), so \( \beta = \tau(l) \). If \( \rk{\tau(l)} < \rk{ \tau(l-1)} \) then \( \tau_n \) can be extended to satisfy the claim.
Otherwise, \( \tau(l-1) = \sigma  \psi \) and \( \tau(l) = \psi ( \sigma  \psi ) \) for a predicate \( \psi \).
In this case, we add a further (trivial) thread \( \tau_{n+1} = ( \psi x )\).

If \( \alpha \sf_\alpha \beta \) and \( \alpha \neq \beta \) then  \( \beta = \gamma \subs[x] \alpha \) for some \( \gamma \) such that \( \rk \gamma < \rk \beta \).

From the hypothesis we have that \( \rk \alpha \le \rk \beta \).
Let \( \tau \colon \alpha \sf_\alpha \beta \).
As \( \tau \) is not trivial (as otherwise \( \alpha = \beta \)) it follows that \( \alpha = \mnf \phi \) for some predicate and quantifier.
We appeal to the decomposition of \( \tau \) provided by proposition <ref>.
By points 1 & 2, \( \rk{\beta_k} < \rk\alpha \) for all \( k > 0 \).
Let \( \gamma_k = \beta_{k} \subs[x_{k-1}]{\beta_{k-1}} \dotsm \subs[x_0]{\beta_0} \).
As \( \rk \alpha \le \rk{\gamma_k} \) for each \( k \le n \) but \( \rk{\beta_k} < \rk\alpha \) for all \( k > 0 \), it follows that at least one of \( x_0 \), …, \( x_{k-1} \) occurs free in each \( \beta_{k} \).
But then \( x_0 \) occurs in \( \gamma \coloneqq \beta_{n} \subs[x_{n-1}]{\beta_{n-1}} \dotsm \subs[x_1]{\beta_1} \) and \( \beta = \gamma \subs [x_0]{\alpha} \) as required.

We are now in a position to prove proposition <ref>:

Let \( \tau \) be an infinite thread and \( I \) the set of formulas through which \( \tau \) passes infinitely often.
Pick \( \eta \in I \) with minimal rank.
By definition, \( I \) is a strongly connected subgraph of \( \subform{\eta} \): for every \( \alpha \in I \) we have \( \eta \sf_\eta \alpha \).
In particular, each \( \alpha \in I \) can be expressed as \( \alpha = \beta \subs [x]{\eta} \) for some \( \beta \) with \( \rk{\beta} < \rk {\alpha} \), meaning that \( \rk {\alpha} = \rk{\eta} \) iff \( \alpha = \eta \).

An alternative proof of the proposition utilises the subsumption order on formulas.
We say that \( \alpha \) subsumes \( \beta \) if \( \alpha \sf_\alpha \beta \).
Expressed in terms of subsumption, proposition <ref> is the statement that among the formulas occurring infinitely often in an infinite thread there is a unique most subsuming formula. In other words:

In every strongly connected component of \( \form \) there is a (unique) formula that subsumes all formulas in this subgraph.

Let us denote by \( {\le} \subseteq \form \times \form \) the subsumption relation: \( \alpha \le \beta \) iff \( \alpha \sf_\alpha \beta \).
Reflexivity and transitivity of \( \le \) are immediate.
Antisymmetry is a consequence of proposition <ref>.
For the final claim, let \( C \subseteq \form \) be strongly connected, i.e., \( \alpha \sf \beta \) for all \( \alpha , \beta \in C \).
Choose \( \eta \in C \) with minimal rank. Then \( \eta \le \alpha \) for all \( \alpha \in C \).

§ EQUIVALENCE OF INDUCTIVE AND CYCLIC PROOFS

In this section we complete the proof of

The embedding of \( \kmu \) into \( \cmu \) was established in section <ref>. It remains to treat the other direction.
The argument follows the sketch in section <ref> but with a slight complication to the definition of \( [v] \) to ensure a smoother handling of bud-companion pairs.

In the following we refer to formulas in \( \form \) as plain formulas.
Let \( * \colon \nms \to \form  \) be a partial function of names to plain formulas; we call such functions assignments.
An assignment induces an interpretation of a-formulas as plain formulas in the following way.
First, given a plain predicate \( \phi \) and annotation \( a \) we introduce a plain formula \( \nf[a*] \phi \)  defined by

\[
\nf[a*] \phi \coloneqq
\begin{cases}
\nf \phi , &\text{if \( a = \epsilon \),}
\\
\nf[ b* ] \phi , &\text{if \( a = b n \) and \( n \not\in \mathsf{dom} \,* \),}
\\
*n \rightarrow \nf[ b*] x.\, \phi ( *n \rightarrow \var x), &\text{if \( a = b n \)  and \( n \in \mathsf{dom} \,* \).}
\end{cases}
\]

Now, given an annotated \( \alpha \) we define \( \alpha^* \) by structural recursion compositionally with \( ( \nf[ a ] \phi )^* = \nf[ a* ] {\phi^*} \) and \( (\lambda x.\,\alpha)^* = \lambda  x.\, \alpha^* \).

It is clear that independent of the choice of \( * \), the \( * \)-translations of all \( \cmu \)-rules except \( (\nu^n) \) are \( \kmu \)-derivable.

The translation of \( (\nu^n) \) is also derivable in \( \kmu \) if \( n \in \mathsf{dom} \,* \) and \( *n \) is the disjunction of side formulas:
Let \( \phi \) be an a-predicate and consider an instance of the annotated \( \nu \)-rule

\begin{equation}
\label{e-nu-a}
\begin{prooftree}
\hypo{ c n : \Phi , \phi ( { \nf[ a n ] \phi } ) }
\infer1[$\nu ^n$]{ c : \Phi , \nf[ a ] \phi  }
\end{prooftree}
\end{equation}

Suppose that \( *n = \disj \Phi^* \) where \( \Phi^* = \setof{ \delta^* }[ \delta \in \Phi ] \).

\[
\phi ( { \nf[ a n ] \phi }) ^*
= \phi^* ( { \disj \Phi^* \rightarrow \nf[ a* ] x.\, \phi ( { { \disj \Phi^* \rightarrow x}}) } )
\]

and the following is a derivation in \( \kmu \):

\begin{equation}
\label{e-nu-a-in-koz}
\begin{prooftree}
\hypo{ \Phi^* , \phi (\nf[ a n ] \phi ) ^* }
\infer1[$\nu,\weak,\disj$]{ \Phi^* , \nf[ a* ] x.\, \phi^* ( {\disj \Phi^* \rightarrow x } ) }
\infer1[\ind]{ \Phi^* , \nf[ a* ] \phi^* }
\end{prooftree}
\end{equation}

One final derivable rule is required before proceeding with the proof.

For \( \Gamma , \Delta  \) sets of a-formulas, let \( \Gamma \le \Delta \) express that \( \Delta \) is an a-weakening of \( \Gamma \), i.e., \( c : \Delta \) is derivable from \( c : \Gamma \) by instances of \( (\aw) \) and \( (\exc) \) alone, where \( c \) is any annotation for which \( c : \Delta \) is an a-sequent.

If \( \Gamma \le \Delta \), then for every assignment \( * \), (plain) predicate \( \phi \) and annotation \( a \),

* if \( \kmu \vdash \Gamma^* \), then \( \kmu \vdash \Delta^* \).

* if \( *n = \disj \Gamma^* \) for some \( n \) in \( a \), then \( \kmu \vdash \Delta^* , \nf[ a*] \phi \).

It suffices to show derivability of \( \nf \phi  \Rightarrow  \nf x .\, { \phi ( {\beta \rightarrow \var x} ) } \) for arbitrary \( \phi \) and \( \beta \).
The derivation employs the simple induction rule:

[$\nf \phi$] ϕ , β⇒ϕ

ϕ( ϕ ) ⇒ϕ(  β→ϕ )
1[$\mu $] ϕ⇒ϕ( β→ϕ )

1[] νϕ⇒x.   ϕ( β→x )

For the second claim we show \( \kmu \vdash \Gamma^* , \nf[ a* ]\phi \) and invoke case 1. This is trivial as

\[
\nf[a*] \phi = \beta_1 \rightarrow \dotsm \rightarrow \beta_k \rightarrow \disj \Gamma^* \rightarrow \gamma
\]

for some \( \beta_1 \), …, \( \beta_k \), \( \gamma \).

We can now proceed with the proof of theorem <ref>.

Let \( \pi \) be a \( \cmu \)-proof with endsequent \( \Phi \).
To each vertex \( u \) is associated a particular assignment \( [u] \colon \nms \to \form \) defined as follows.
Let \( u \) be labelled by the a-sequent \( c_u : \Phi_u \).
The domain of \( [u] \) is the set of names in \( c_u = ( n_i )_{i < k }\).
The value \( [u] (n_{i}) \) is defined by recursion on in \( \pi \) and \( i < k \).

Let \( c n \le c_u \) and suppose \( [u](n_i) \) is defined for all \( i < \lh c \). There is a unique application of the rule \( ( \nu^{n}) \) on the path from \( u \) to the root such that \( c n \) is a prefix of the control of all sequents on the path from \( u \) to the premise of the rule.
Let \( v \) name this vertex.
In particular, \( c \) is a subword of \( c_v \) and the premise of this rule is a sequent of the form \( c_v n : \Psi , \phi (\nf[ a n ] \phi ) \).
Since every name occurring in \( \Psi \) is present in \( c_v \) and \( n \) does not occur in \( c_v \) we set \( [u](n) = \disj \Psi^{[v]} \).

It remains to be shown that \( \kmu \vdash (\Phi_u)^{[u]} \)  for every \( u \in \pi \).
As the control of a sequent is only modified via the rules \( (\nu^n) \) and \( (\cw) \), if no applications of either rules occurs on a path from \( u < v \) to \( v \), then the assignments \( [u] \) and \( [v] \) are identical.
Thus, by the observations above, it suffices to consider the case that \( u \) is the conclusion of either of these rules or is a bud.
Starting with the first, suppose that \( u \) is the conclusion of an instance of \( (\nu^n) \) with the form as in (<ref>) above.
Let \( v \) be the premise.
Then \( \mathsf{dom}\,[v] = \mathsf{dom}\, [u] \cup \setof{ n } \), \( [v](n) = \disj \Delta^{[v]} \) and \( [v](m) = [u](m) \) for all \( m \) occurring in \( c \).
In particular, \( \Delta^{[v]} = \Delta^{[u]} \) and  \( \kmu \vdash (\Phi_u)^{[u]} \) by the derivation in (<ref>).
The case of \( (\cw) \) is immediate.

This leaves the case that \( u \) is a bud.
As \( \pi \) is a proof, \( u \) is closed.
Let \( c_u = c n \) and \( \Phi_u = \Phi \cup \setof{ \nf[ a n ] \phi } \).
By the definition of \( [u] \) we have \( [u](n) = \disj \Phi^{[u]} \), and \( \kmu \vdash (\Phi_u)^{[u]} \) by lemma <ref>.

§ CUT ELIMINATION FOR TIGHT DERIVATIONS

In this section we establish the cut elimination for tight multicuts that proivdes the missing detail in the proof of theorem <ref>.
We recall the main definition.

A multicut is a sequence of maximal derivations \( e , d^0 , \dotsc , d^n \) satisfying

* \( e \vdash \Theta , \alpha_1 , \dotsc , \alpha_n \) is \( \setof{ \alpha_1 , \dotsc, \alpha_n } \)-full

* \( d^i \vdash \seq{\alpha_i} {\Psi_i} \) for each \( 0 \le i \le n \).

We refer to the formulas \( \alpha_i \) as cut-formulas.
The multicut is tight if \( d^i \) is \( \neg{\alpha_i} \)-tight for each \( i \).

The above multicut is visualised as the rule

*[e] Θ, α_0 , …, α_n
*[d^0] α_0 Ψ_0
*[d^n] α_nΨ_n
4[] Θ, Ψ_0 , …, Ψ_n

The derivation \( e \) is referred to as the major premise of the multicut, and  \( d^0 ,  \dotsc \) as minor premises.

We show that given the tight multicut above, there is a co-inductive derivation \( \hat e \) with endsequent \( \Theta , \Psi_0 , \dotsc , \Psi_n \).
As outlined in the proof sketch to theorem <ref> the argument proceeds by a process of multicut elimination: the sequence of rewrite rules are applied sequentially to each multicut which permutes the rules in \( e, d^0, \dotsc \) revealing an ever-larger initial segment of a derivation of the endsequent.

In the following we refer to a formula occurrence as principal in \( e \) if it is principal in the inference at the root of \( e \).
It is also convenient to distinguish the two kind of side-formula of the modal rule \( (\square) \).
For the inference

\[
\begin{prooftree}
\hypo{ \Phi , \alpha }
\infer1[$\square $]{ \diamond \Phi , \square  \alpha , \Psi }
\end{prooftree}
\]

we refer to \( \diamond \Phi, \square \alpha \) as active formulas of the inference and \( \Psi \) as inactive.
In all other rules of \( \kmo \) only the principal formula(s) are active.

A multicut is said to be active if some cut formula in the major premise is active and every cut formula in each minor premise is active in the final inference of that derivation.

We present the multicut reductions below. These are split into two categories based on activity of the multicut.

§.§ Multicut inactive

This scenario breaks into four cases:

Case A: The final rule of \( e \) is \( (\square  ) \) and a cut formula is inactive.

Suppose \( \alpha_0 \) is inactive in \( e \). That is, if the final inference of \( e \) is written in the form displayed above then \( \alpha_0 \in \Psi \).
The multi-cut reduction in this scenario simply discards the derivation \( d^0 \) and replaces the inactive cut formula the dropped sequent via the reduction:

\begin{multline*}
\begin{prooftree}
\subproof{ \Theta' }
\infer1[$\square  $]{ \Theta , \alpha_0 , \dotsc , \alpha_{n} }
\subproof{ \seq {\alpha_0} {\Psi_0} }
\hypod
\subproof{ \seq {\alpha_n} {\Psi_n} }
\infer4[\mcut]{ \Theta , \Psi_0 , \dotsc , \Psi_n }
\end{prooftree}
\\%[2ex]
\qquad\text{reduces to}\qquad
\begin{prooftree}
\subproof{ \Theta' }
\infer1[$\square  $]{ \Theta , \Psi_0 , \alpha_{1} , \dotsc, \alpha_{n} }
\subproof{ \seq {\alpha_{1}} {\Psi_{1}} }
\hypod
\subproof{ \seq {\alpha_n} {\Psi_n} }
\infer4[\mcut]{ \Theta , \Psi_{0} , \dotsc, \Psi_n }
\end{prooftree}
\end{multline*}

Case B: The final rule of \( d^i \) is \( (\square  ) \) and \( \neg{\alpha_i} \) is inactive.

The multicut is eliminated by a similar reduction:

\[
\begin{prooftree}
\subproof{ \Theta , \alpha_0 , \dotsc , \alpha_{n} }
\hypod
\subproof[d^i_0]{ \Rightarrow \Psi_i' }
\infer1[$\square  $]{ \seq {\alpha_i} {\Psi_i} }
\hypod
\infer4[\mcut]{ \Theta , \Psi_0 , \dotsc , \Psi_n }
\end{prooftree}
\qquad\text{reduces to}\qquad
\begin{prooftree}
\subproof[\hat d^i_0]{ \Psi_i' }
\infer1[$\square  $]{ \Theta , \Psi_{0} , \dotsc, \Psi_n }
\end{prooftree}
\]

Case C: The final rule of \( e \) is not \( (\square  ) \) and no cut formula is principal in \( e \).

As the final inference in \( e \) is not \( (\square  ) \) the principal (and active) formula occurrences are all present in \( \Theta \).
This implies that each cut formula occurs in all premises of the applied rule, whence the multicut and final inference in \( e \) can be permuted.

As an example, we suppose the final rule in \( e \) is \( (\disj) \) and \( \Theta = \Theta' , \disj \Gamma \) with the final formula being the principal formula.
Let \( \Delta \subseteq \Gamma \) be the minor formulas of the rule instance.
The following reduction applies.

\begin{multline*}
\begin{prooftree}
\subproof{ \Theta' , \Delta , \alpha_0 , \dotsc, \alpha_n }
\infer1[$\disj$]{ \Theta , \alpha_0 , \dotsc, \alpha_n }
\subproof{ \seq {\alpha_0} {\Psi_0} }
\hypod
\subproof{ \seq{\alpha_n}{\Psi_n} }
\infer4[\mcut]{ \Theta , \Psi_0 , \dotsc , \Psi_n }
\end{prooftree}
\\[1ex]
\qquad\text{reduces to}\qquad
\begin{prooftree}
\subproof{ \Theta' , \Delta , \alpha_0 , \dotsc, \alpha_n }
\subproof{ \seq {\alpha_0} {\Psi_0} }
\hypod
\subproof{ \seq{\alpha_n}{\Psi_n} }
\infer4[\mcut]{ \Theta' , \Delta , \Psi_0 , \dotsc , \Psi_n }
\infer1[$\disj$]{ \Theta , \Psi_0 , \dotsc , \Psi_n }
\end{prooftree}
\end{multline*}

The cases of this reduction are similar.
Observe that if \( \Theta \) or \( \Psi_i \) is axiomatic, then so is \( \Theta , \Psi_0 , \dotsc, \Psi_n \).

Case D: The final rule of \( d^i \) is not \( (\square  ) \) and \( \neg{\alpha_i} \) is not principal in \( d^i \).

Analogous to the previous case.

§.§ Multicut active

Suppose the multicut is active.
Furthermore, we have that \( \neg{\alpha_i} \) is active in each \( d^j \).
Without loss of generality suppose \( \alpha_0 \) is active in \( e \).
One of the following reduction rules is applicable depending on the main connective of \( \alpha_0 \).

A literal is active in a rule iff it is principal.
If \( \alpha_0 \) is a literal, then the endsequents of \( e \) and \( d^0 \) are instances of the axiom \( (x) \) where \( \alpha_0 \in \setof{ x , \neg x } \).
For simplicity, suppose \( \alpha_0 = x \).
In particular, \( \neg{x} \) occurs among \( \Theta , \alpha_0 , \dotsc, \alpha_n \) and \( x \in \Psi_0 \).
The multicut reduction is a simple one:

\[
\begin{prooftree}
\axiom[$x$]{ \Theta , x , \alpha_1 , \dotsc , \alpha_{n} }
\axiom[$x$]{ x \Rightarrow \Psi_0 }
\hypod
\infer3[\mcut]{ \Theta , \Psi_0 , \dotsc , \Psi_n }
\end{prooftree}
\qquad\text{reduces to}\qquad
\begin{prooftree}
\axiom[$x$]{ \Theta , \Psi_0 , \dotsc, \Psi_n }
\end{prooftree}
\]

It requires to check that \( \Theta , \Psi_0 , \dotsc, \Psi_n \) is a valid conclusion of \( (x) \).
If \( \neg x \in \Theta \), then this is immediate.
Otherwise, \( \neg x \) is also a cut formula, say \( \alpha_j = \neg x \).
As \( x \) is therefore active in \( d^j \), the final rule in \( d^j \) is \( (x) \), i.e., \( \neg x \in \Psi_j \).
So \( \Psi_0 , \Psi_j \) is axiomatic.

Assume \( \alpha_0 = \disj \Gamma \) for \( \Gamma = \setof{ \gamma_1 , \dotsc, \gamma_k } \) and the final rule of \( e \) is \( (\disj) \).

As \( e \) is \( \alpha_0 \)-full the minor formulas of this inference are \( \Gamma \).
The final rule in \( d^0 \) is therefore \( (\conj) \) with principal formula \( \neg{\alpha_0} \).
If \( k \neq 0 \) the applies multicut reduction is:

\begin{multline*}
\begin{prooftree}
\subproof{ \Theta , \Gamma , \alpha_{1} , \dotsc , \alpha_{n} }
\infer1[$\disj$]{\Theta , \disj \Gamma , \alpha_1 , \dotsc , \alpha_{n} }
\subproof{ \seq{\gamma_1}{\Psi_0} }
\hypod
\subproof{ \seq{\gamma_k}{\Psi_0} }
\infer3[$\conj$]{\seq {\disj \Gamma } {\Psi_0} }
\subproof{ \seq{\alpha_{1}}{\Psi_{1}} }
\hypod
\infer4[\mcut]{ \Theta , \Psi_0 , \dotsc , \Psi_n }
\end{prooftree}
\\[1ex]
\qquad\text{reduces to}\qquad
\begin{prooftree}%[small,]
\subproof{\Theta , \Gamma , \alpha_{1} , \dotsc , \alpha_{n}}
\subproof{ \seq{\gamma_1}{\Psi_0} }
\hypod
\subproof{ \seq{\gamma_k}{\Psi_0} }
\subproof{ \seq{\alpha_{1}}{\Psi_{1}} }
\hypod
\infer6[\mcut]{ \Theta , \Psi_{0} , \dotsc, \Psi_0 , \Psi_1 , \dotsc, \Psi_n }
\infer1[$\con^*$]{ \Theta , \Psi_0 , \dotsc, \Psi_n }
\end{prooftree}
\end{multline*}

The final inference in the resolved derivation is a sequence of \( (\con) \) if \( \card{\Gamma} > 1 \).
If \( \Gamma = \emptyset \) then the following reduction is utilised which avoids the need for an explicit weakening rule:

\begin{multline*}
\begin{prooftree}
\subproof{ \Theta , \alpha_{1} , \dotsc , \alpha_{n} }
\infer1[$\disj$]{\Theta , \disj \Gamma , \alpha_1 , \dotsc , \alpha_{n} }
\subproof{\seq {\disj \Gamma } {\Psi_0} }
\subproof[d^1]{\seq { \alpha_1 } {\Psi_1} }
\hypod
\infer4[\mcut]{ \Theta , \Psi_0 , \dotsc , \Psi_n }
\end{prooftree}
\\[1ex]
\qquad\text{reduces to}\qquad
\begin{prooftree}%[small,]
\subproof{\Theta , \alpha_{1} , \dotsc , \alpha_{n}}
\subproof[\hat d^1]{ \seq{\alpha_{1}}{ \Psi_0 , \Psi_{1}} }
\hypod
\infer3[\mcut]{ \Theta , \Psi_{0} , \Psi_1 , \dotsc, \Psi_n }
\end{prooftree}
\end{multline*}

where \( \hat{d}^1 \) is the weakening of \( d^1 \) as described in proposition <ref>.

Assume \( \alpha_0 = \conj \Gamma \) for some \( \Gamma \) and the final rule of \( e \) is \( (\conj) \).
As the multicut is active, \( d^0 \) end with an instance of \( (\disj) \) with principal formula \( \disj \neg{\Gamma} \).
By tightness, there is just one minor formula, \( \neg{\gamma} \) say.

The multicut reduction is:

\begin{multline*}
\begin{prooftree}
\subproof{ \setof{ \Theta , \gamma , \alpha_1 , \dotsc  }[ \gamma \in \Gamma ] }
\infer1[$\conj$]{ \Theta , \conj \Gamma , \alpha_1 , \dotsc }
\subproof{ \gamma \Rightarrow \Psi_0 }
\infer1[$\disj$]{ \conj \Gamma \Rightarrow  \Psi_0 }
\subproof{ \alpha_1 \Rightarrow \Psi_1 }
\hypod
\infer4[\mcut]{ \Theta , \Psi_0 , \Psi_1 , \dotsc  }
\end{prooftree}
\\[1ex]
\qquad\text{reduces to}\qquad
\begin{prooftree}%[small,]
\subproof{ \Theta , \gamma , \alpha_1 , \dotsc }
\subproof{ \gamma \Rightarrow \Psi_0  }
\subproof{ \alpha_1 \Rightarrow \Psi_1  }
\hypod
\infer4[\mcut]{ \Theta ,  \Psi_0 , \Psi_1 , \dotsc }
\end{prooftree}
\end{multline*}

Suppose \( \alpha_0 = \mnf \phi \) for \( \sigma  \in \setof{\mu ,\nu } \) and the final rule of \( d \) is \( (\sigma ) \).
The reduction is

\begin{multline*}
\begin{prooftree}
\subproof{ \Theta , \phi ( \mnf \phi ) , \alpha_{1} , \dotsc , \alpha_{n} }
\infer1[$\sigma $]{ \Theta , \mnf \phi , \alpha_1 , \dotsc , \alpha_{n} }
\subproof{ { \phi ( \mnf \phi )  } \Rightarrow {\Psi_0} }
\infer1[$\sigma ^\bot$]{ { \mnf \phi } \Rightarrow {\Psi_0} }
\hypod
\infer3[\mcut]{ \Theta , \Psi_0 , \dotsc , \Psi_n }
\end{prooftree}
\\[1ex]
\qquad\text{reduces to}\qquad
\begin{prooftree}%[small,]
\subproof{ \Theta , \phi ( \mnf \phi ) , \alpha_{1} , \dotsc , \alpha_{n} }
\subproof{ \phi ( \mnf \phi )  \Rightarrow {\Psi_0} }
\hypod
\infer3[\mcut]{ \Theta , \Psi_0 , \dotsc , \Psi_n }
\end{prooftree}
\end{multline*}

The multicut is active and the final rule in all derivations is \( (\square  ) \).
We present the generic case of this reduction involving three cut formulas that are, respectively, principal, active but not principal, and non-active, :

\begin{multline*}
\begin{prooftree}
\subproof{ \Theta' , \alpha_0 , \alpha_1 }
\infer1[$\square  $]{ \Theta , \square \alpha_0 , \diamond  \alpha_1 , \alpha_2 }
%	\hypod
\subproof{ \alpha_0 \Rightarrow \Psi_0' }
\infer1[$\square  $]{ \square \alpha_0 \Rightarrow \Psi_0 }
\subproof{ \alpha_1 \Rightarrow \Psi_1' }
\infer1[$\square  $]{ \diamond \alpha_1 \Rightarrow \Psi_1 }
\subproof{ \alpha_2 \Rightarrow \Psi_2 }
\infer4[\mcut]{ \Theta , \Psi_0 , \Psi_1 , \Psi_2 }
\end{prooftree}
\\[1ex]
\qquad\text{reduces to}\qquad
\begin{prooftree}
\subproof{ \Theta' , \alpha_0 , \alpha_1 }
\subproof{ \alpha_0 \Rightarrow \Psi_0' }
\subproof{ \alpha_1 \Rightarrow \Psi_1' }
\infer3[\mcut]{ \Theta' , \Psi_0' , \Psi_1' }
\infer1[$\square  $]{ \Theta , \Psi_0 , \Psi_1 , \Psi_2 }
\end{prooftree}
\end{multline*}

The principal formula of \( (\square  ) \) in the ‘reduced’ proof is the principal formula in derivation \( d_1 \).

§.§ Multicut elimination

We now complete the proof of theorem <ref>.

Let \( d , d' \) be derivations and \( R \subseteq d \times d' \).
For branches \( b  \) and \( b' \) through \( d \) and \( d' \) respectively,
we write \( B \, R \, B' \) iff for every \( v \in B \) there exists \( v' \in B' \) s.t. \( ( v , v' ) \in R \) and for every \( v' \in B' \) there exists \( v \in B \) s.t. \( ( v , v' ) \in R \).
If \( T \) is a set of threads, \( \neg{T} \coloneqq \setof{ \neg{\tau} }[\tau \in T] \).

To complete the theorem we require a lemma relating paths in the result of multicut elimination.

Let \( \pi , \rho^0 , \dotsc, \rho^n \) be a tight multicut with \( \pi \vdash \Theta , \alpha_0 , \dotsc, \alpha_n \) and \( \rho^i \vdash \seq{\alpha_i}{\Psi_i} \) for each \( n \).
There exists a maximal illfounded derivation \( d \) in \( \kmo + \con \) with endsequent \( \Theta , \Psi_0 , \dotsc , \Psi_n \), a homomorphism \( h \colon d \le_\Theta \pi \) and relations \( \setof{G_i \subseteq d \times \rho^i }[i \le n] \) such that for every branch \( B \subseteq d \):

* \( \Tr[\Theta]{ d,B} = \Tr[\Theta]{\pi ,h(B)} \).

* For each \( i \le n \),
\( \Tr[\Psi_i]{ d,B} = \bigcup \Setof{ \Tr[\Psi_i]{ \rho^i, B' }}[ B \, G_i \, B' ] \).

* For all \( i \le n \), \( \neg {\Tr[\alpha_i]{\pi,h(B)}}  = \bigcup \Setof{ \Tr[\neg{\alpha_i}]{ \rho^i, B'}}[ B \, G_i \, B' ] \).

The desired derivation is given as the result of continuous cut elimination according to the reduction rules described above.
That is, \( d \) is the limit of an increasing sequence of finite (non-maximal) derivations \( (d_i)_{i<\omega} \) and likewise \( h = \bigcup_i h_i \) is a limit of partial functions and \( G_j = \bigcup_{i} G_{j,i} \).
Each bud of \( d_i \) will be associated a tight multicut with the sequent at the leaf corresponding to the conclusion of the multicut.
The construction begins with
\( d_0 \) being the trivial derivation comprising the endsequent \( \Theta , \Psi_0 , \dotsc, \Psi_n  \) only which is associated the initial multicut

*[π] Θ, α_0 , …, α_n
*[ρ^0] α_0 Ψ_0
*[ρ^n] α_nΨ_n
4[] Θ, Ψ_0 , …, Ψ_n

Define \( h_0 \colon \epsilon \mapsto \epsilon \) and \( G_{j,0} = \setof{ ( \epsilon , \epsilon ) } \) that relate the root of \( d_0 \) to the root of each corresponding co-proof.

Suppose \( d_i \), \( h_i \colon d_i \to \pi \), and \( G_{j,i} \subseteq d_i \times \rho^j \) has been defined.
We obtain \( d_{i+1} \), etc., by the following construction applied to each bud of \( d_i \).
Fix such a bud \( b \) and suppose it is associated the tight multicut

\[
\begin{prooftree}
\subproof*[\pi_u]{ \Theta' , \alpha'_0 , \dotsc , \alpha'_n }
\subproof*[\rho^{k_0}_{u_0}]{ \seq {\alpha'_0} {\Psi'_0} }
\hypod
\subproof*[\rho^{k_m}_{u_m}]{ \seq{\alpha'_m}{\Psi'_m} }
\infer4[\mcut]{ \Theta' , \Psi_0' , \dotsc , \Psi_m' }
\end{prooftree}
\]

where \( u \in \pi \), \( k_j \le n \) and \( u_j \in \rho^{k_j} \) for each \( j \le m \). (Recall, \( \pi_u \) denotes the maximal subderivation of \( \pi \) rooted at \( u \).)
As some multicut reductions duplicate or discard minor premises, the derivations \( \rho^{k_0}_{u_0} \), …, \( \rho^{k_n}_{u_n} \) list some subproofs of \( \rho^{0} \), …, \( \rho^n \).
We will assume that \( ( b , u_{j'} ) \in G_{j,i} \) iff \( k_{j'} = j \).

Inspection of the rules of the calculus show that at least one multicut reduction is applicable.
Applying that multicut reduction replaces the multicut at \( b \) by a derivation in which each non-axiomatic leaf is associated a tight multicut built from sub-derivations of \( \pi_u \), etc.
The derivation \( d_{i+1} \) extends the bud \( b \) by this derivation with the associated multicuts.
If \( d_{i+1} \) properly extends \( b \), such as if the multicut is permuted with the inference at one of the premise derivations, the relations \( h_{i+1} \) and \( G_{i+1} \) are extended accordingly.
We give three examples.

Reduction <ref>.C: inactive disjunction case.

\begin{multline*}
\begin{prooftree}
\subproof*[\pi_{u0}]{ \Theta'' , \Delta , \alpha_0 , \dotsc, \alpha_m' }
\infer1[$\disj$]{ \Theta'' , \disj \Gamma , \alpha_0' , \dotsc, \alpha_m' }
\subproof*[\rho^{k_0}_{u_0}]{ \seq {\alpha_0'} {\Psi_0'} }
\hypod
\infer3[\mcut]{ \Theta' , \Psi_0' , \dotsc , \Psi_m' }
\end{prooftree}
\;\text{to}\quad
\begin{prooftree}
\subproof*[\pi_{u0}]{ \Theta'' , \Delta , \alpha_0' , \dotsc, \alpha_m' }
\subproof*[\rho^{k_0}_{u_0}]{ \seq {\alpha_0'} {\Psi_0'} }
\hypod
\infer3[\mcut]{ \Theta'' , \Delta , \Psi_0' , \dotsc , \Psi_m' }
\infer1[$\disj$]{ \Theta' , \Psi_0' , \dotsc , \Psi_m' }
\end{prooftree}
\end{multline*}

In forming \( d_{i+1} \), the bud \( b \) (labelled by \( \Theta' , \Psi_0' , \dotsc , \Psi_m' \) and associated the multicut to the left) is extended by an instance of \( (\disj) \) to \( b' = b0 \) labelled by \( \Theta'' , \Delta , \Psi_0' , \dotsc , \Psi_m' \) and associated the multicut on the right.
\( h_{i+1} \) extends \( h_i \) by \( b' \mapsto  u0 \) which maps the new bud to the vertex of \( \pi \) corresponding to the new major premise.
\( G_{j,i+1} \) extends \( G_{j,i} \) by \( \setof{ ( b' , u_{j'} ) }[ k_{j'} = j ] \) which associates the new bud to the root of each corresponding minor premise.

Reduction <ref>, disjunction reduction. A cut formula is a principal disjunction inducing the multicut reduction:

\begin{multline*}
\begin{prooftree}
\subproof*[\pi_{u0}]{ \Theta' , \Gamma , \alpha_{1}' , \dotsc , \alpha_m' }
\infer1[$\disj$]{ \Theta' , \disj \Gamma , \alpha_1' , \dotsc , \alpha_m' }
\subproof*[\rho^{k_0}_{u_00}]{ \seq{ \gamma_0 }{\Psi_0'} }
\hypod
\subproof*[\rho^{k_0}_{u_0 l}]{ \seq{ \gamma_{l} }{\Psi_0'} }
\infer3[$\conj$]{\seq {\disj \Gamma } {\Psi_0'} }
\hypod
\infer3[\mcut]{ \Theta' , \Psi_0' , \dotsc , \Psi_n' }
\end{prooftree}
\\[1ex]
\qquad\text{reduces to}\qquad
\begin{prooftree}%[small,]
\subproof*[\pi_{u0}]{ \Theta' , \Gamma , \alpha_{1}' , \dotsc , \alpha_{m}' }
\subproof*[\rho^{k_0}_{u_0 0 }]{ \seq{\gamma_0}{\Psi_0'} }
\hypod
\subproof*[\rho^{k_0}_{u_0 l }]{ \seq{\gamma_l}{\Psi_0'} }
\subproof{ \seq{\alpha_{1}'}{\Psi_{1}'} }
\hypod
\infer6[\mcut]{ \Theta' , \Psi_{0}' , \dotsc, \Psi_0' , \Psi_1' , \dotsc, \Psi_m' }
\infer1[$\con^*$]{ \Theta' , \Psi_0' , \dotsc, \Psi_m' }
\end{prooftree}
\end{multline*}

The construction of \( d_{i+1} \) is analogous except that if \( l = 1 \) there is no extension of \( b \) (as there is no contraction to be inserted).
Only the function \( h_i \) needs to be extended if \( d_{i+1} \) extends \( d_i \) (so that it remains total) by setting \( h_{i+1} \colon b0 \mapsto u0 \).
Set \( G_{j,i+1} = G_{j,i} \) for all \( j \le n \).

Reduction <ref>, modal reduction.
A cut formula is a principal disjunction inducing the multicut reduction. For the purpose of illustration we assume two cut formulas are active in the inference:

\begin{multline*}
\begin{prooftree}
\subproof*[\pi_{u0}]{ \Theta'' , \alpha_0' , \alpha_1' }
\infer1[$\square  $]{ \Theta' , \square \alpha_0' , \diamond \alpha_1' , \dotsc  }
%	\hypod
\subproof*[\rho^{k_0}_{u_00}]{ \alpha_0' \Rightarrow \Psi_0'' }
\infer1[$\square  $]{ \square \alpha_0' \Rightarrow \Psi_0' }
\subproof*[\rho^{k_1}_{u_10}]{ \alpha_1' \Rightarrow \Psi_1'' }
\infer1[$\square  $]{ \diamond \alpha_1' \Rightarrow \Psi_1' }
\hypod
\infer4[\mcut]{ \Theta' , \Psi_0' , \Psi_1' , \dotsc }
\end{prooftree}
\\[1ex]
\qquad\text{reduces to}\qquad
\begin{prooftree}
\subproof*[\pi_{u0}]{ \Theta'' , \alpha_0' , \alpha_1' }
\subproof*[\rho^{k_0}_{u_00}]{ \alpha_0' \Rightarrow \Psi_0'' }
\subproof*[\rho^{k_1}_{u_10}]{ \alpha_1' \Rightarrow \Psi_1'' }
\infer3[\mcut]{ \Theta'' , \Psi_0'' , \Psi_1'' }
\infer1[$\square  $]{ \Theta' , \Psi_0' , \Psi_1' , \dotsc }
\end{prooftree}
\end{multline*}

Let \( d_{i+1} \) extend the bud \( b \) by a single bud labelled by the sequent \( \Theta'' , \Psi_0'' , \Psi_1'' \) as the inference \( (\square) \).
\( h_{i+1} \) extends \( h_i \) by \( b0 \mapsto u0 \) (the root of the major premise).
For each \( j \le n \), set \( G_{j,i+1} = G_{j,i} \cup \setof{ (b0 , u_{j'}0 ) }[ k_{j'} = j ] \).

The desired properties of the lemma are consequences of the construction.
Conditions 1 & 2 are by design: every branch of \( d \) is built progressively through a sequence of multicut reductions.
This sequence might be finite if some multicut reductions eliminates the multicut, such as in the literal reduction. If so, the branch of \( d \) will have a suffix that is a branch in one of the original derivations \( \pi , \rho^0 , \dotsc, \rho^n \).
If, however, every vertex on the branch is extended by a bud in some approximation \( d_i \), then the branch is generated by the infinite sequence of multicut reductions applied through the approximations. In that case, this branch \( B \) is assigned a unique branch of \( \pi \) (via the homomorphism \( h \)) carrying the same \( \Theta \)-threads and a collection of branches \( \mathcal B_j = \setof{ B' \subseteq d^j }[ B \, G_j \, B'] \) for each \( j \le n \) carrying the same \( \Psi_j \)-threads.
If \( h(B) \) carries an infinite \( \alpha_j \)-thread then at every approximation of \( B \) in the construction has a subderivation of \( \rho^j \) as a minor premise, whence \( \mathcal B_j \) is necessarily non-empty.
Furthermore, every branch \( B' \in \mathcal B_j \) carries an \( \neg{\alpha_j} \)-thread whose negation is carried by \( B \).
These observations confirm condition 3 of the lemma.

The only property we have not yet confirmed is maximality of \( d \). By the reasoning above, \( d \) can only fail to be a maximal derivation if there is some approximation \( d_i \) and a bud \( b \in d_i \) which remains a bud in each derivation \( d_{i+j} \).
This bud must be associated a multicut that is subject to infinitely many `reductions' but which never produces a logical inference with which to extend the bud \( b \).
The active reductions of kind <ref> are not productive in this sense with except for the modal reduction (as some premise must have a principal formula that is not the cut formula).
Thus, if an infinite sequence of reductions is not productive, from some point on only reductions of the active but non-modal kind are applied (although the reduction <ref>.A is not productive in the above sense it is only applicable if either some other non-active reduction or the active modal reduction is eventually applicable).
Such a scenario can occur only if a cut formula is unguarded; it induces branches \( B' \subseteq \pi \) and \( B'' \subseteq \rho^j \) (for some \( j \)) such that \( B' \) carries a good cut-formula thread and \( B'' \) carries the negation of this thread.
As \( \rho^j \) is a co-proof it must carry a good thread which, by tightness, cannot be from the cut formula.

We now prove preservation of proofhood through tight multicut elimination.

\( 1 \Rightarrow 2 \) was proved in the main text. For the direction
\( 2 \Rightarrow 1 \), let \( \pi \vdash \Theta , \Phi \) and \( \rho^\alpha \vdash \alpha \Rightarrow \Psi \) for each \( \alpha \in \Phi \) is \( \neg{\alpha} \)-tight.
We provide a co-proof \( \hat\pi \vdash \Theta , \Psi \) such that \( \hat \pi \le_\Theta \pi \).
To that aim we may assume \( \pi \) is \( \Phi \)-full.
Let \( e \) be the derivation in \( \kmo + \con \) of \( \Phi , \Psi \) provided by lemma <ref> and \( h \colon e \le_\Phi \pi \) the associated homomorphism.
By proposition <ref> it suffices to show that \( e \) is a co-proof.
Let \( B \) be a branch of \( e \) and suppose there is no good thread among \( \Tr[\Psi] {e,B} \).
Part 2 of lemma <ref> implies that for every \( \alpha \in \Phi \) and branch \( C \) of \( \rho^\alpha \), if \( B G_\alpha C \) then \( C \) carries a good \( \neg{\alpha} \)-thread.
Moreover, these threads are unique for each choice of \( C \).
But then, by part 3, \( h(B) \) is a branch of \( \pi \) carrying a good \( \Theta \)-thread (since it carries no good \( \Phi \)-thread).
Since \( \Tr[\Theta] {\pi,f(B)} \subseteq \Tr {e,B} \) we are done.