As in the previous proof, we do not recall the shape of \(P, P'\); the reader is invited
to check our statements against the proofs of <ref> (<ref>). Observe first that by
<ref> we have

\[
V_{\axg{P'}} = \data{names}(\Gamma, A) = V_{\axg{P} \rst_{\Gamma, A}}.
\]

We then need to prove only that \(E_{\axg{P'}} \subseteq E_{\axg{P}}\), as this
will be enough to guarantee that \(E_{\axg{P'}} \subseteq E_{\axg{P} \rst_{\Gamma, A}}\).
We proceed by structural induction on \(P\):

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{\dl{C}
\lor \dl{D}, A \land B\}}\) with conclusion \(\th \Delta, \dl{C} \lor \dl{D}, A \land B\)
where \(\Gamma = \Delta \cup \{\dl{C} \lor \dl{D}\}\), then by <ref>

\begin{multline*}
\axg{P'} = \data{Wk}_{\Delta, \dl{D}} \sqcup \data{Id}_{\{\dl{C}, A\}}\\
\sqsubseteq \data{Wk}_\Delta \sqcup \data{Id}_{\{\dl{C}, A\}} \sqcup \data{Id}_{\{\dl{D}, B\}}
= \data{Wk}_\Delta \sqcup \data{Id}_{\{\dl{C} \lor \dl{D}, A \land B\}} = \axg{P};
\end{multline*}

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{C,\dl{D}\}}\)
with conclusion \(\th \Delta, A \land B, C, \dl{D}\) where \(\Gamma = \Delta \cup
\{C, \dl{D}\}\), then by <ref>

\[
\axg{P'} = \data{Wk}_{\Delta, A} \sqcup \data{Id}_{\{C, \dl{D}\}}
\sqsubseteq \data{Wk}_{\Delta, A \land B} \sqcup \data{Id}_{\{C, \dl{D}\}} = \axg{P};
\]

* if \(P\) ends with a -rule application introducing \(A \land B\)
whose premiss subtrees \(Q, R\) have conclusions respectively \(\th \Gamma, A\)
and \(\th \Gamma, B\), then \(P' = Q\) and the conclusion is immediate;

* if \(P\) ends with a cut-rule application on formulas \(C, \dl{C}\),
with premiss subderivations \(Q, R\), we have by induction hypothesis \(\axg{
\data{inv_l}(Q, A \land B)} \sqsubseteq \axg{Q}\) and \(\axg{\data{inv_l}(R, A \land B)}
\sqsubseteq \axg{R}\), with

\[
\axg{P'} = \axg{\data{inv_l}(Q, A \land B)} \odot_C \axg{\data{inv_l}(R, A \land B)}.
\]

By <ref>, \(xy \in E_{\axg{P'}}\) if and only if there is
an alternating path (<ref>) connecting \(x\) with \(y\)
between \(\axg{\data{inv_l}(Q, A \land B)}\) and \(\axg{\data{inv_l}(R, A \land B)}\)
on inteface \(\data{names}(C)\). It is easy to check that the same sequence of vertices
is an alternating path between \(\axg{Q}\) and \(\axg{R}\) through interface \(\data{names}(C)\),
and therefore \(xy \in E_{\axg{Q} \odot_C \axg{R}} = E_{\axg{P}}\);

* if \(P\) ends with a sum-, - or -rule
application that does not introduce \(A \land B\), we conclude by induction hypothesis
and <ref>.

Immediate by <ref> when \(A\) is a
disjunction; for conjunctions we need to show that

\[
\axg{P} = \axg{\data{inv_l}(P, A)} \sqcup \axg{\data{inv_r}(P, A)},
\]

whenever \(P\) is cut-free. In particular, it suffices to show that

\[
E_{\axg{P}} = E_{\axg{\data{inv_l}(P, A)}} \cup E_{\axg{\data{inv_r}(P, A)}}.
\]

By structural induction on \(P\), assuming \(A = A_1 \land A_2\):

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{\dl{B}_1
\lor \dl{B}_2, A\}}\) with conclusion \(\th \Delta, \dl{B}_1 \lor \dl{B}_2, A\)
where \(\Gamma = \Delta \cup \{\dl{B}_1 \lor \dl{B}_2\}\), then

\begin{gather*}
\axg{P} = \data{Wk}_\Delta \sqcup \data{Id}_{\{\dl{B}_1 \lor \dl{B}_2, A\}}
= \data{Wk}_\Delta \sqcup \data{Id}_{\{\dl{B}_1, A_1\}} \sqcup \data{Id}_{\{\dl{B}_2, A_2\}},\\
\axg{\data{inv_l}(P, A)} = \data{Wk}_{\Delta, \dl{B}_2} \sqcup \data{Id}_{\{\dl{B}_1, A_1\}},\\
\axg{\data{inv_r}(P, A)} = \data{Wk}_{\Delta, \dl{B}_1} \sqcup \data{Id}_{\{\dl{B}_2, A_2\}}.
\end{gather*}

Because the weakening graphs have no edges, we can conclude that

\[
E_{\axg{P}} = E_{\data{Id}_{\{\dl{B}_1, A_1\}}} \sqcup E_{\data{Id}_{\{\dl{B}_2, A_2\}}}
= E_{\axg{\data{inv_l}(P, A)}} \sqcup E_{\axg{\data{inv_r}(P, A)}}.
\]

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{B,\dl{C}\}}\)
with conclusion \(\th \Delta, A, B, \dl{C}\) where \(\Gamma = \Delta \cup \{B, \dl{C}\}\),
then we have

\begin{gather*}
\axg{P} = \data{Wk}_\Delta \sqcup \data{Id}_{\{B, \dl{C}\}},\\
\axg{\data{inv_l}(P, A)} = \data{Wk}_{\Delta, A_1} \sqcup \data{Id}_{\{B, \dl{C}\}},\\
\axg{\data{inv_r}(P, A)} = \data{Wk}_{\Delta, A_2} \sqcup \data{Id}_{\{B, \dl{C}\}}.
\end{gather*}

Therefore, because the weakening graphs have no edges,

\[
E_{\axg{P}} = E_{\data{Id}_{\{B, \dl{C}\}}} = E_{\axg{\data{inv_l}(P, A)}} = E_{\axg{\data{inv_r}(P, A)}},
\]

from which the conclusion follows.

* if \(P\) ends with a -rule application introducing \(A\),
the conclusion is trivial as \(P = \data{isl}(P, A)\);

* if \(P\) ends with a ⊔-, - or -rule
application that does not introduce \(A\), with premiss subtrees \(Q_1, \ldots, Q_n\),
we have by induction hypothesis

\[
E_{\axg{Q_i}} = E_{\axg{\data{inv_l}(Q_i, A)}} \cup E_{\axg{\data{inv_r}(Q_i, A)}}.
\]

for all \(1 \leq i \leq n\). The result then follows from the fact that

\[
E_{\axg{P}} = \bigcup_{i = 1}^n E_{\axg{Q_i}}
= \left(\bigcup_{i = 1}^n E_{\axg{\data{inv_l}(Q_i, A)}}\right)
\cup \left(\bigcup_{i = 1}^n E_{\axg{\data{inv_r}(Q_i, A)}}\right). \qedhere
\]

§ PROOFS OF LEMMAS REGARDING BRANCH-LABELED AXIOM GRAPHS

§.§ Properties of branch sets

For all named formulas \(A\), if \(X \in \data{Br}(A)\) then \(X \subseteq \data{names}(A)\).

Immediate by induction on \(A\).

Observe first that \(\data{names}(\Gamma) = \bigcup_{A \in \Gamma} \data{names}(A)\),
and assume \(X \in \data{Br}(\Gamma)\). By definition \(X \subseteq \data{names}(\Gamma)\),
therefore \(X = \bigcup_{A \in \Gamma} (X \cap \data{names}(A))\); we know also that
\((X \cap \data{names}(A)) \in \data{Br}(A)\) for all \(A \in \Gamma\), hence we can
choose \(X_A = X \cap \data{names}(A)\).

Conversely, assume \(X = \bigcup_{A \in \Gamma} X_A\) with \(X_A \in \data{Br}(A)\)
for all \(A \in \Gamma\). By <ref>, \(X \subseteq \data{names}(A)\);
moreover, because \(\Gamma\) is sharing-free, its elements have pairwise disjoint name
sets, hence the \(X_A\) in particular are pairwise disjoint and \(X \cap \data{names}(A)
= X_A \in \data{Br}(A)\), as desired.

Assume \(X \in \data{Br}(\Gamma \cup \Delta)\): by <ref> there
is an indexed family \((X_A)_{A \in \Gamma \cup \Delta}\) of name sets such that \(X =
\bigcup_{A \in \Gamma \cup \Delta} X_A\) and \(X_A \in \data{Br}(A)\) for all \(A \in \Gamma
\cup \Delta\). Let then \(Y = \bigcup_{A \in \Gamma} X_A\) and \(Z = \bigcup_{A \in \Delta}
X_A\): again by <ref>, \(Y \in \data{Br}(\Gamma)\) and \(Z
\in \data{Br}(\Delta)\), and obviously \(X = Y \cup Z\). The argument for the converse is
analogous, reversing the direction of all implications.

Fact (i) is left to the reader. For fact (ii), observe that \(\data{Br}(\{A, B\}) =
\data{Br}(\{A\} \cup \{B\}) = \data{Br}(A \lor B)\) as an immediate consequence of
<ref>: then we have

\begin{align*}
\data{Br}(\Gamma, A \lor B) &= \{ X \cup Y \mid X \in \data{Br}(\Gamma), Y \in \data{Br}(A \lor B) \}\\
&= \{ X \cup Y \mid X \in \data{Br}(\Gamma), Y \in \data{Br}(\{A, B\}) \}\\
&= \data{Br}(\Gamma, A, B).
\end{align*}

For fact (iii), recall that \(\data{Br}(A \land B) = \data{Br}(A) \cup \data{Br}(B)\);
then, again by <ref>,

\begin{align*}
\data{Br}(\Gamma, A \land B) &= \{ X \cup Y \mid X \in \data{Br}(\Gamma), Y \in \data{Br}(A \land B) \}\\
&= \{ X \cup Y \mid X \in \data{Br}(\Gamma), Y \in \data{Br}(A) \cup \data{Br}(B) \}\\
&= \{ X \cup Y \mid X \in \data{Br}(\Gamma), Y \in \data{Br}(A) \}\\
& \qquad\cup \{ X \cup Y \mid X \in \data{Br}(\Gamma), Y \in \data{Br}(B) \}\\
&= \data{Br}(\Gamma, A) \cup \data{Br}(\Gamma, B).
\end{align*}

For fact (iv), observe that (by an easy inductive argument) all branches of \(A\)
(resp. of \(B\)) must be non-empty, and remember that \(\Gamma, A, B\) have disjoint
name sets by hypothesis. Let then \(X \in \data{Br}(\Gamma, A) \cap \data{Br}(\Gamma, B)\):
by <ref> there is a non-empty \(Y \in \data{Br}(A)\)
such that \(Y \subseteq X\). By construction we have also \(X \subseteq \data{names}(
\Gamma, B)\), but then there should be some name \(z \in Y \subseteq \data{names}(A)\)
such that \(z \in \data{names}(\Gamma, B)\), which is impossible.

§.§ Properties of branch-labeled axiom graphs

For all bl-graphs \(G\),

\[
\data{Br}(\blwk{\Gamma}(G)) = \{ X \cup Y \mid X \in \data{Br}(G), Y \in \data{Br}(\Gamma) \}.
\]

Immediate, see <ref>.

For any pair \(A, \dl{B}\) of disjoint and sharing-free named formulas such that
\(A \equiv B\), \(\data{Br}(\blid{\{A, \dl{B}\}}) = \data{Br}(A, \dl{B})\).

By induction on the height of \(A\):

* if \(A\) is atomic, then \(\data{Br}(A, \dl{B}) = \{\data{names}(A, \dl{B})\}
= \data{Br}(\blid{\{A, \dl{B}\}})\) by <ref>;

* if \(A = A_1 \lor A_2\) and \(\dl{B} = \dl{B}_1 \land \dl{B}_2\), then
by <ref>

\begin{align*}
\data{Br}(\blid{\{A, \dl{B}\}})
&= \data{Br}(\blwk{A_2}(\blid{\{A_1, \dl{B}_1\}}) \sqcup \blwk{A_1}(\blid{\{A_2, \dl{B}_2\}})) \\
&= \data{Br}(\blwk{A_2}(\blid{\{A_1, \dl{B}_1\}})) \cup \data{Br}(\blwk{A_1}(\blid{\{A_2, \dl{B}_2\}})).
\end{align*}

By induction hypothesis, \(\data{Br}(\blid{\{A_1, \dl{B}_1\}}) = \data{Br}(A_1, \dl{B}_1)\)
and \(\data{Br}(\blid{\{A_2, \dl{B}_2\}}) = \data{Br}(A_2, \dl{B}_2)\);
by <ref>

\begin{gather*}
\begin{multlined}
\data{Br}(\blwk{A_2}(\blid{\{A_1, \dl{B}_1\}}))\\
= \{ X \cup Y \mid X \in \data{Br}(A_1, \dl{B}_1), Y \in \data{Br}(A_2) \}
= \data{Br}(A_1, A_2, \dl{B}_1),
\end{multlined}\\
\begin{multlined}
\data{Br}(\blwk{A_1}(\blid{\{A_2, \dl{B}_2\}}))\\
= \{ X \cup Y \mid X \in \data{Br}(A_2, \dl{B}_2), Y \in \data{Br}(A_1) \}
= \data{Br}(A_1, A_2, \dl{B}_2).
\end{multlined}
\end{gather*}

Then, again by <ref>,

\begin{align*}
\data{Br}(\blid{\{A, \dl{B}\}})
&= \data{Br}(A_1, A_2, \dl{B}_1) \cup \data{Br}(A_1, A_2, \dl{B}_2)\\
&= \data{Br}(A_1, A_2, \dl{B}_1 \land \dl{B}_2)\\
&= \data{Br}(A_1 \lor A_2, \dl{B}_1 \land \dl{B}_2)
= \data{Br}(A, \dl{B}). \qedhere
\end{align*}

Let \(\Gamma\) be any sharing-free set of named formulas, \(A, \dl{B}\) a pair of
disjoint and sharing free named formulas that share no names with \(\Gamma\) and
such that \(A \equiv B\): then

\[
\data{Br}(\blwk{\Gamma}(\blid{\{A, \dl{B}\}})) = \data{Br}(\Gamma, A, \dl{B}).
\]

The proof that \(V_{\blaxg{P}} = \data{names}(\Gamma)\) is analogous to that of
<ref> and left to the reader. We prove by structural
induction on \(P\) that \(\data{Br}(\blaxg{P}) \subseteq \data{Br}(\Gamma)\):

* if \(P\) is an axiom rule application, the conclusion follows immediately
from <ref>;

* if \(P\) has the form

\[
\prftree[r]{\rl{cut}}
{\prfsummary[\(Q\)]{\th \Gamma, A \vphantom{\dl{A}}}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{A}}}
{\th \Gamma}
\]

then by <ref>, if \(X \in \data{Br}(\blaxg{Q} \odot_A \blaxg{R})\)
there is either \(Y \in \data{Br}(\blaxg{Q})\) or \(Y \in \data{Br}(\blaxg{R})\)
such that \(X = Y \setminus \data{names}(A)\). By induction hypothesis we have either
\(Y \in \data{Br}(\Gamma, A)\) or \(Y \in \data{Br}(\Gamma, \dl{A})\), hence
\(X \in \data{Br}(\Gamma)\) by <ref>;

all other cases follow immediately from the induction hypothesis.

§.§ Behaviour under inversion

For all bl-graphs \(G, H\) and sharing-free sets \(\Gamma\) of named formulas,

\[
\blwk{\Gamma}(G \sqcup H) = \blwk{\Gamma}(G) \sqcup \blwk{\Gamma}(H).
\]

Left to the reader.

For all bl-graphs \(G\) and sharing-free sets \(\Gamma \cup \Delta\) of named formulas,

\[
\blwk{\Gamma}(\blwk{\Delta}(G)) = \blwk{\Gamma \cup \Delta}(G).
\]

The identity is obvious for vertices. For the edge-branch relation, let
\(e \adin_{\blwk{\Gamma}(\blwk{\Delta}(G))} X\): there are then \(Y \in \data{Br}(G)\),
\(Z \in \data{Br}(\Delta)\) and \(W \in \data{Br}(\Gamma)\) such that \(e \adin_G Y\)
and \(X = Y \cup Z \cup W\). By <ref>, \(Z \cup W \in
\data{Br}(\Gamma \cup \Delta)\), hence \(e \adin_{\blwk{\Gamma \cup \Delta}(G)} X\).
Conversely, let \(e \adin_{\blwk{\Gamma \cup \Delta}(G)} X\): there are \(Y \in
\data{Br}(G)\), \(Z \in \data{Br}(\Gamma \cup \Delta)\) such that \(e \adin_G Y\)
and \(X = Y \cup Z\). Again by <ref>, \(Z = Z' \cup Z''\)
for some \(Z' \in \data{Br}(\Gamma), Z'' \in \data{Br}(\Delta)\), hence \(e \adin_{
\blwk{\Gamma}(\blwk{\Delta}(G))} X\).

Almost identical to the proof of <ref>
(<ref>); only the base case is different (axioms).
Let \(P'\) denote the inverted derivation \(\data{inv}(P, A \lor B)\); then:

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{\dl{C}
\land \dl{D}, A \lor B\}}\) with conclusion \(\th \Delta, \dl{C} \land \dl{D}, A \lor B\)
where \(\Gamma = \Delta \cup \{\dl{C} \land \dl{D}\}\), then by <ref>
we have

\begin{gather*}
\blaxg{P} = \blwk{\Delta}(\blid{\{\dl{C} \land \dl{D}, A \lor B\}}),\\
\blaxg{P'} = \blwk{\Delta, B}(\blid{\{\dl{C}, A\}})
\sqcup \blwk{\Delta, A}(\blid{\{\dl{D}, B\}}),
\end{gather*}

and by <ref>

\[
\blaxg{P} = \blwk{\Delta}(\blwk{B}(\blid{\{\dl{C}, A\}}) \sqcup \blwk{A}(\blid{\{\dl{D}, B\}})).
\]

We apply <ref> to get

\begin{align*}
\blaxg{P} &= \blwk{\Delta}(\blwk{B}(\blid{\{\dl{C}, A\}}))
\sqcup \blwk{\Delta}(\blwk{A}(\blid{\{\dl{D}, B\}}))\\
&= \blwk{\Delta, B}(\blid{\{\dl{C}, A\}})
\sqcup \blwk{\Delta, A}(\blid{\{\dl{D}, B\}}) = \blaxg{P'}.
\end{align*}

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{C,\dl{D}\}}\)
with conclusion \(\th \Delta, A \lor B, C, \dl{D}\) where \(\Gamma = \Delta \cup
\{C, \dl{D}\}\), then by <ref>

\[
\blaxg{P'} = \blwk{\Delta, A, B}(\blid{\{C, \dl{D}\}})
= \blwk{\Delta, A \lor B}(\blid{\{C, \dl{D}\}}) = \blaxg{P}. \qedhere
\]

For all bl-graphs \(G \sqsubseteq H\) and name sets \(X \subseteq \mathcal{N}\),

\[
V_G \subseteq X \implies G \sqsubseteq H \rst_X.
\]

If \(V_G \subseteq X\) then obviously \(V_G \subseteq V_{H \rst_X} = (V_H \cap X)\).
Moreover, let \(e \adin_G Y\): we have \(Y \subseteq V_G \subseteq X\) by <ref>
and we know by hypothesis that \(e \adin_H Y\), hence \(e \adin_{H \rst_X} Y\).

Let \(\Gamma \cup \{A \land B\}\) be a sharing-free set of named formulas, \(G\)
any bl-graph with \(\data{Br}(G) \subseteq \data{Br}(\Gamma, A \land B)\): then

\[
\data{Br}(G \rst_{\Gamma, A}) \subseteq \data{Br}(\Gamma, A)
\text{ and }
\data{Br}(G \rst_{\Gamma, B}) \subseteq \data{Br}(\Gamma, B).
\]

We only prove the first half of the statement, the second half is similar. Observe
that (by an easy inductive argument) every branch of \(B\) is non-empty, and remember
that \(\Gamma, A, B\) have disjoint name sets. Let \(X \in \data{Br}(G \rst_{\Gamma, A})\)
and assume \(X \in \data{Br}(\Gamma, B)\): by <ref> there
are \(Y \in \data{Br}(\Gamma)\) and a non-empty \(Z \in \data{Br}(B)\) such that
\(X = Y \cup Z\). However, we have \(X \subseteq \data{names}(\Gamma, A)\) by construction,
hence \(Z \subseteq \data{names}(\Gamma, A)\), which is disjoint from \(\data{names}(B)\),
a contradiction. Therefore \(X \notin \data{Br}(\Gamma, B)\), and by exclusion we
have \(X \in \data{Br}(\Gamma, A)\).

We only prove the first part of the statement, i.e. that

\[
\blaxg{\data{inv_l}(P, A \land B)} = \blaxg{P} \rst_{\Gamma, A};
\]

the argument for the second part is analogous. Let \(P' = \data{inv_l}(P, A \land B)\),
As usual we reason about the shape of \(P, P'\) without recalling it; the interested
reader may inspect the proofs of <ref>
(<ref>). Observe first that by <ref>
we have

\[
V_{\blaxg{P'}} = \data{names}(\Gamma, A) = V_{\blaxg{P} \rst_{\Gamma, A}};
\]

by <ref>, then, we can prove that \(\blaxg{P'} \sqsubseteq
\blaxg{P} \rst_{\Gamma, A}\) by showing that \(\blaxg{P'} \sqsubseteq \blaxg{P}\).
For the reverse inclusion, on the other hand, it suffices to show that \({\adin_{\blaxg{P}
\rst_{\Gamma, A}}} \subseteq {\adin_{\blaxg{P'}}}\). By structural induction on \(P\):

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{\dl{C}
\lor \dl{D}, A \land B\}}\) with conclusion \(\th \Delta, \dl{C} \lor \dl{D}, A \land B\)
where \(\Gamma = \Delta \cup \{\dl{C} \lor \dl{D}\}\), then by <ref>

\[
\blaxg{P} = \blwk{\Delta}(\blid{\{\dl{C} \lor \dl{D}, A \land B\}})
\text{ and }
\blaxg{P'} = \blwk{\Delta, \dl{D}}(\blid{\{\dl{C}, A\}}).
\]

By <ref>

\begin{align*}
\blaxg{P} &= \blwk{\Delta}(\blwk{\dl{D}}(\blid{\{\dl{C}, A\}})
\sqcup \blwk{\dl{C}}(\blid{\{\dl{D}, B\}}))\\
&= \blwk{\Delta, \dl{D}}(\blid{\{\dl{C}, A\}}) \sqcup \blwk{\Delta, \dl{C}}(\blid{\{\dl{D}, B\}})\\
&= \blaxg{P'} \sqcup \blwk{\Delta, \dl{C}}(\blid{\{\dl{D}, B\}}),
\end{align*}

hence \(\blaxg{P'} \sqsubseteq \blaxg{P}\), and we have also

\[
\data{Br}(\blwk{\Delta, \dl{C}}(\blid{\{\dl{D}, B\}})) = \data{Br}(\Delta, \dl{C}, \dl{D}, B) = \data{Br}(\Gamma, B)
\]

by <ref>. Let then
\(e \adin_{\blaxg{P} \rst_{\Gamma, A}} X\): by <ref>
\(X \in \data{Br}(\Gamma, A)\), hence by <ref>,
point (iv)

\[
X \notin \data{Br}(\Gamma, B) = \data{Br}(\blwk{\Delta, \dl{C}}(\blid{\{\dl{D}, B\}})),
\]

and then by exclusion we must have \(e \adin_{\blaxg{P'}} X\);

* if \(P\) ends with an axiom rule application of the kind \(\data{ax}_{\{C,\dl{D}\}}\)
with conclusion \(\th \Delta, A \land B, C, \dl{D}\) where \(\Gamma = \Delta \cup
\{C, \dl{D}\}\), then by <ref>

\[
\blaxg{P} = \blwk{\Delta, A \land B}(\blid{\{C, \dl{D}\}})
\text{ and }
\blaxg{P'} = \blwk{\Delta, A}(\blid{\{C, \dl{D}\}}).
\]

It is easy to check, using <ref>, that

\[
\blaxg{P} = \blwk{\Delta, A}(\blid{\{C, \dl{D}\}})
\sqcup \blwk{\Delta, B}(\blid{\{C, \dl{D}\}})
= \blaxg{P'} \sqcup \blwk{\Delta, B}(\blid{\{C, \dl{D}\}})
\]

\[
\data{Br}(\blwk{\Delta, B}(\blid{\{C, \dl{D}\}})) = \data{Br}(\Delta, B, C, \dl{D}) = \data{Br}(\Gamma, B),
\]

and we conclude as in the previous case;

* if \(P\) ends with a -rule application introducing \(A \land B\)
whose premiss subtrees \(Q, R\) have conclusions respectively \(\th \Gamma, A\)
and \(\th \Gamma, B\), then \(P' = Q\). We have obviously \(\blaxg{P'} \sqsubseteq
\blaxg{Q} \sqcup \blaxg{R} = \blaxg{P}\). For the reverse inclusion, we argue
by exclusion from <ref>
and the fact that \(\data{Br}(\blaxg{R}) \subseteq \data{Br}(\Gamma, B)\),
concluding that \({\adin_{\blaxg{P} \rst_{\Gamma, A}}} \subseteq {\adin_{\blaxg{Q}}}
= {\adin_{\blaxg{P'}}}\);

* if \(P\) ends with a cut-rule application on formulas \(C, \dl{C}\),
with premiss subderivations \(Q, R\), we have by induction hypothesis

\[
\blaxg{\data{inv_l}(Q, A \land B)} = \blaxg{Q} \rst_{\Gamma, A, C}
\text{ and }
\blaxg{\data{inv_l}(R, A \land B)} = \blaxg{R} \rst_{\Gamma, A, \dl{C}},
\]

\[
\blaxg{P'} = {\blaxg{Q} \rst_{\Gamma, A, C}} \odot_C {\blaxg{R} \rst_{\Gamma, A, \dl{C}}}.
\]

Let \(e \adin_{\blaxg{P'}} X\): there is by <ref> an \(X\)-labeled
alternating path \(z_1,\ldots,z_n\) between \(\blaxg{Q} \rst_{\Gamma, A, C}\)
and \(\blaxg{R} \rst_{\Gamma, A, \dl{C}}\) through interface \(\data{names}(C)\),
with \(e = z_1 z_n\). This is obviously also an \(X\)-labeled alternating path
between \(\blaxg{Q}\) and \(\blaxg{R}\) through the same interface, hence
\(e \adin_{\blaxg{P}} X\) and \(\blaxg{P'} \sqsubseteq \blaxg{P}\).

Now let \(e \adin_{\blaxg{P} \rst_{\Gamma, A}} X\): there is, again by <ref>,
an \(X\)-labeled alternating path \(z_1,\ldots,z_n\) between \(\blaxg{Q}\)
and \(\blaxg{R}\) through interface \(\data{names}(C)\) with \(e = z_1 z_n\). We have
to show that this is also an \(X\)-labeled alternating path between \(\blaxg{Q}
\rst_{\Gamma, A, C}\) and \(\blaxg{R} \rst_{\Gamma, A, \dl{C}}\) through the same
interface, from which it follows that \(e \adin_{\blaxg{P'}} X\). Let \(I =
\data{names}(C)\) and assume \(z_i z_{i+1} \adin_{\blaxg{Q}}^I X\) for some \(1
\leq i < n\): there is \(Y \subseteq I\) such that \(z_i z_{i+1} \adin_{\blaxg{Q}}
(X \cup Y)\); we know also that \(X \subseteq \data{names}(\Gamma, A)\), hence
\((X \cup Y) \subseteq \data{names}(\Gamma, A, C)\): then

\[
z_i z_{i+1} \adin_{\blaxg{Q} \rst_{\Gamma, A, C}} (X \cup Y)
\text{ and }
z_i z_{i+1} \adin_{\blaxg{Q} \rst_{\Gamma, A, C}}^I X.
\]

Similarly, if \(z_i z_{i+1} \adin_{\blaxg{R}}^I X\) then \(z_i z_{i+1} \adin_{\blaxg{R}
\rst_{\Gamma, A, \dl{C}}}^I X\), and we conclude as desired;

* if \(P\) ends with a sum-, - or -rule
application that does not introduce \(A \land B\), we conclude by induction hypothesis
and the fact that restriction distributes over graph unions.

Observe first that

\[
\data{names}(\Gamma, A \land B)
= \data{names}(\Gamma, A) \cup \data{names}(\Gamma, B),
\]

\[
V_{\blaxg{P}} = \data{names}(\Gamma, A \land B)
= V_{\blaxg{P} \rst_{\Gamma, A}} \cup V_{\blaxg{P} \rst_{\Gamma, B}}.
\]

For the branch-label relation, we start by recalling the fact that

\[
\data{Br}(\blaxg{P}) \subseteq \data{Br}(\Gamma, A \land B) = \data{Br}(\Gamma, A) \cup \data{Br}(\Gamma, B).
\]

Now let \(e \adin_{\blaxg{P}} X\): if \(X \in \data{Br}(\Gamma, A)\), then in particular
\(X \subseteq \data{names}(\Gamma, A)\), hence \(e \adin_{\blaxg{P} \rst_{\Gamma, A}} X\);
similarly, if \(X \in \data{Br}(\Gamma, B)\) then \(e \adin_{\blaxg{P} \rst_{\Gamma, B}} X\).
We have then

\[
\blaxg{P} \sqsubseteq {\blaxg{P} \rst_{\Gamma, A}} \sqcup {\blaxg{P} \rst_{\Gamma, B}};
\]

the reverse inclusion is immediate.

§.§ Auxiliary lemmas for cut-elimination

By structural induction on \(P\); we leave the base case (axioms),
superpositions and the logical rules to the reader. For cuts, assume \(P\)
has the form

\[
\prftree[r]{\rl{cut}}
{\prfsummary[\(Q\)]{\th \Gamma, A \vphantom{\dl{A}}}}
{\prfsummary[\(R\)]{\th \Gamma, \dl{A}}}
{\th \Gamma}
\]

We have then \(\blaxg{P} = \blaxg{Q} \odot_A \blaxg{R}\). Let \(xy \in E_{\blaxg{P}}\):
there is by <ref> a labeled alternating path \(z_1, \ldots, z_n\)
between \(\blaxg{Q}\) and \(\blaxg{R}\) through the interface \(\data{names}(A)\),
with \(xy = z_1 z_n\). For all \(1 < i < n\) (the interface nodes) we have \(\dl{A}[z_i]
= \dl{A[z_i]}\). Let \(\alpha = \Gamma[x]\). There are two possibilities:

* odd edges in \(\blaxg{Q}\), even edges in \(\blaxg{R}\): we prove
by secondary induction on \(i\) that for all \(1 < i < n\), if \(i\) is odd then
\(A[z_i] = \alpha\), if it is even then \(A[z_i] = \dl{\alpha}\). If \(i = 2\)
(even) then \(z_1 z_2 \in E_{\blaxg{Q}}\), hence by the primary induction hypothesis

\[
A[z_2] = (\Gamma, A)[z_2] = \dl{(\Gamma, A)[z_1]} = \dl{\Gamma[z_1]}
= \dl{\Gamma[x]} = \dl{\alpha}.
\]

If \(i > 2\) and even, then \(z_{i-1} z_i \in E_{\blaxg{Q}}\); by the secondary
induction hypothesis \(A[z_{i-1}] = \alpha\), and by the primary hypothesis

\[
A[z_i] = (\Gamma, A)[z_i] = \dl{(\Gamma, A)[z_{i-1}]} = \dl{A[z_{i-1}]} = \dl{\alpha}.
\]

If \(i > 2\) and odd, then \(z_{i-1} z_i \in E_{\blaxg{R}}\); by the secondary
induction hypothesis \(A[z_{i-1}] = \dl{\alpha}\) hence \(\dl{A}[z_{i-1}] = \alpha\);
by the primary hypothesis

\[
\dl{A}[z_i] = (\Gamma, \dl{A})[z_i] = \dl{(\Gamma, \dl{A})[z_{i-1}]}
= \dl{\dl{A}[z_{i-1}]} = \dl{\alpha},
\]

therefore \(A[z_i] = \dl{\dl{\alpha}} = \alpha\). We conclude by cases on \(n\):
if \(n = 2\), then by the primary induction hypothesis

\[
\Gamma[y] = (\Gamma, A)[z_2] = \dl{(\Gamma, A)[z_1]} = \dl{\Gamma[x]};
\]

if \(n > 2\) and even, then \(z_{n-1} z_n \in E_{\blaxg{Q}}\) and \(A[z_{n-1}]
= \alpha\); by the primary induction hypothesis

\[
\Gamma[y] = (\Gamma, A)[z_n] = \dl{(\Gamma, A)[z_{n-1}]} = \dl{A[z_{n-1}]}
= \dl{\alpha} = \dl{\Gamma[x]};
\]

if \(n > 2\) and odd, then \(z_{n-1} z_n \in E_{\blaxg{R}}\) and \(A[z_{n-1}]
= \dl{\alpha}\), hence \(\dl{A}[z_{n-1}] = \alpha\); by the primary induction hypothesis

\[
\Gamma[y] = (\Gamma, \dl{A})[z_n] = \dl{(\Gamma, \dl{A})[z_{n-1}]}
= \dl{\dl{A}[z_{n-1}]} = \dl{\alpha} = \dl{\Gamma[x]}.
\]

* odd edges in \(\blaxg{R}\), even edges in \(\blaxg{Q}\): we proceed as
in the previous case, swapping \(Q\) with \(R\) and \(A\) with \(\dl{A}\).

By structural induction on \(P\). We prove the result only for the base case (i.e. the
axioms), all other cases are more or less immediate.

Case (i). \(P\) is an axiom rule application of the kind \(\rl[\{\dl{B},A\}]{ax}\)
with conclusion \(\th \Delta, \dl{B}, A\), where \(\Gamma = \Delta \cup \{\dl{B}\}\):

* if \(A = A_1 \lor A_2\) is a disjunction, then \(\data{inv}(P, A)\) has the form

\[
\prftree[r]{\rl{\lor}}
{\prfbyaxiom{\rl[\{\dl{B}_1, A_1\}]{ax}}{\th \Delta, \dl{B}_1, A_1, A_2}}
{\prfbyaxiom{\rl[\{\dl{B}_2, A_2\}]{ax}}{\th \Delta, \dl{B}_2, A_1, A_2}}
{\th \Delta, \dl{B}_1 \land \dl{B}_2, A_1, A_2}}
{\th \Delta, \dl{B}_1 \land \dl{B}_2, A_1 \lor A_2}
\]

where \(\dl{B} = \dl{B}_1 \land \dl{B}_2\). We have

\begin{align*}
\data{vh}(P) &= 1 + \data{deg}(\th \Delta, \dl{B}_1 \land \dl{B}_2, A_1 \lor A_2)\\
&= 1 + \data{deg}(\th \Delta)\\
&   \qquad\! + 1 + \data{deg}(\dl{B}_1) + \data{deg}(\dl{B}_2)\\
&   \qquad\! + 1 + \data{deg}(A_1) + \data{deg}(A_2)\\
&= 3 + \data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_1, A_2)
\end{align*}

\begin{align*}
\data{vh}(\data{inv}(P, A)) &= 2 + \max \{
1 + \data{deg}(\th \Delta, \dl{B}_1, A_1, A_2),
1 + \data{deg}(\th \Delta, \dl{B}_2, A_1, A_2)
\}\\
&= 3 + \max \{
\data{deg}(\th \Delta, \dl{B}_1, A_1, A_2),
\data{deg}(\th \Delta, \dl{B}_2, A_1, A_2)
\}.
\end{align*}

\[
\data{deg}(\th \Delta, \dl{B}_1, A_1, A_2), \data{deg}(\th \Delta, \dl{B}_2, A_1, A_2)
\leq \data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_1, A_2),
\]

hence \(\data{vh}(\data{inv}(P, A)) \leq \data{vh}(P)\);

* if \(A = A_1 \land A_2\) is a conjunction, then \(\data{inv}(P, A)\) has the form

\[
\prftree[r]{\rl{\land}}
{\prfbyaxiom{\rl[\{\dl{B}_1, A_1\}]{ax}}{\th \Delta, \dl{B}_1, \dl{B}_2, A_1}}
{\th \Delta, \dl{B}_1 \lor \dl{B}_2, A_1}}
{\prfbyaxiom{\rl[\{\dl{B}_2, A_2\}]{ax}}{\th \Delta, \dl{B}_1, \dl{B}_2, A_2}}
{\th \Delta, \dl{B}_1 \lor \dl{B}_2, A_2}}
{\th \Delta, \dl{B}_1 \land \dl{B}_2, A_1 \lor A_2}
\]

where \(\dl{B} = \dl{B}_1 \lor \dl{B}_2\). We have as before

\[
\data{vh}(P) = 3 + \data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_1, A_2)
\]

\begin{align*}
\data{vh}(\data{inv}(P, A)) &= 1 + \max \{
2 + \data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_1),
2 + \data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_2)
\}\\
&= 3 + \max \{
\data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_1),
\data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_2)
\},
\end{align*}

\[
\data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_1),
\data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_2)
\leq \data{deg}(\th \Delta, \dl{B}_1, \dl{B}_2, A_1, A_2),
\]

and again \(\data{vh}(\data{inv}(P, A)) \leq \data{vh}(P)\).

Case (ii). \(P\) is an axiom rule application of the kind \(\rl[\{\dl{B},C\}]{ax}\)
with conclusion \(\th \Delta, A, \dl{B}, C\), where \(\Gamma = \Delta \cup \{\dl{B}, C\}\):

* if \(A = A_1 \lor A_2\) is a disjunction, then \(\data{inv}(P, A)\) has the form

\[
\prftree[r]{\rl{\lor}}
{\prfbyaxiom{\rl[\{\dl{B},C\}]{ax}}{\th \Delta, A_1, A_2, \dl{B}, C}}
{\th \Delta, A_1 \lor A_2, \dl{B}, C}
\]

We have

\begin{align*}
\data{vh}(P) &= 1 + \data{deg}(\th \Delta, A_1 \lor A_2, \dl{B}, C)\\
&= 1 + \data{deg}(\th \Delta, \dl{B}, C)\\
&   \qquad\! + 1 + \data{deg}(A_1) + \data{deg}(A_2)\\
&= 2 + \data{deg}(\th \Delta, A_1, A_2, \dl{B}, C)
\end{align*}

\[
\data{vh}(\data{inv}(P, A)) = 2 + \data{deg}(\th \Delta, A_1, A_2, \dl{B}, C),
\]

hence a fortiori \(\data{vh}(\data{inv}(P, A)) \leq \data{vh}(P)\);

* if \(A = A_1 \land A_2\) is a conjunction, then \(\data{inv}(P, A)\) has the form

\[
\prftree[r]{\rl{\land}}
{\prfbyaxiom{\rl[\{\dl{B},C\}]{ax}}{\th \Delta, A_1, \dl{B}, C}}
{\prfbyaxiom{\rl[\{\dl{B},C\}]{ax}}{\th \Delta, A_2, \dl{B}, C}}
{\th \Delta, A_1 \land A_2, \dl{B}, C}
\]

We have as before

\[
\data{vh}(P) = 2 + \data{deg}(\th \Delta, A_1, A_2, \dl{B}, C)
\]

\begin{align*}
\data{vh}(\data{inv}(P, A)) &= 1 + \max \{
1 + \data{deg}(\th \Delta, A_1, \dl{B}, C),
1 + \data{deg}(\th \Delta, A_2, \dl{B}, C)
\}\\
&= 2 + \max \{
\data{deg}(\th \Delta, A_1, \dl{B}, C),
\data{deg}(\th \Delta, A_2, \dl{B}, C)
\}
\end{align*}

\[
\data{deg}(\th \Delta, A_1, \dl{B}, C),
\data{deg}(\th \Delta, A_2, \dl{B}, C)
\leq \data{deg}(\th \Delta, A_1, A_2, \dl{B}, C)
\]

hence \(\data{vh}(\data{inv}(P, A)) \leq \data{vh}(P)\).

§ PROOF OF THE SEMANTIC CUT-ADMISSIBILITY LEMMA

We devote the present section to the proof of <ref>,
which requires a somewhat involved construction. We start by fixing a set

\[
\data{Pol} = \{ {\circ}, {\bullet} \}
\]

of polarities. For \(p \in \data{Pol}\), we write \(\co{p}\) for the opposite
polarity, i.e. let \(\co{\circ} = {\bullet}\) and \(\co{\bullet} = {\circ}\). As background
data for the construction, we have to provide a pair of bl-graphs \(G_{\circ}, G_{\bullet}\)
and a finite set of names \(I \subseteq \mathcal{N}\) to act as the composition
interface. The two graphs are required to satisfy the following property:
there is a unique branch name \(X \subseteq \mathcal{N}\) such that, for all \(p \in
\data{Pol}\) and \(e \in E_{G_p}\), \(e \adin_{G_p}^I X\);

in other words, the two graphs must have collectively a unique branch up to names in
the interface. The restriction has two important consequences:

* all alternating paths between the two graphs through \(I\) are necessarily
\(X\)-labeled, hence composable;

* any edge can be added to any alternating path, without caring for its label.

More formally, let \(z_1, \ldots, z_n\) be an \(X\)-labeled alternating path between
\(G_{\circ}\) and \(G_{\bullet}\) through interface \(I\) (<ref>).
For any \(p \in \data{Pol}\) we call the path

* \(p\)-initial, if all odd edges are in \(G_p\) and all even edges in \(G_{\co{p}}\);

* \(p\)-final, if it is \(p\)-initial with even \(n\), or \(\co{p}\)-initial
with odd \(n\).

Because the graphs and interface – as well as the unique branch label – are fixed, from now
on we are going to speak simply of alternating paths, without mentioning the full expression
(\(X\)-labeled alt. paths between \(G_{\circ}\) and \(G_{\bullet}\) through interface \(I\)).
The following properties hold:

For all \(p \in \data{Pol}\) and edge \(xy \in E_{G_p}\), \(x,y\) is a \(p\)-initial
and \(p\)-final alternating path.

For any \(p, q \in \data{Pol}\), if \(z_1, \ldots, z_n\) is a \(p\)-initial and
\(q\)-final alternating path then \(z_n, \ldots, z_1\) is a \(q\)-initial and \(p\)-final
alternating path.

Let \(p \in \data{Pol}\), and let \(\vec{z} = z_1, \ldots, z_n\), \(\vec{w} =
w_1, \ldots, w_n\) be alternating paths such that \(\vec{z}\) is \(p\)-final,
\(\vec{w}\) is \(\co{p}\)-initial and \(z_n = w_1\): then

\[
\vec{zw} = z_1, \ldots, (z_n = w_1), \ldots, w_n
\]

is also an alternating path, \(q\)-initial iff so is \(\vec{z}\) and \(q\)-final
iff so is \(\vec{w}\).

The proofs are tedious but straightforward and we leave them to the interested reader.
The construction operates on finite sets \(\sigma\) of pairs with each pair of
the form

\[
\langle S, (v_1, \ldots, v_n) \rangle \in \sigma
\]

where \(S \subseteq I \times \data{Pol}\) is a set of name-polarity pairs (with names
from the interface \(I\)) and \(v_1, \ldots, v_n \in (V_{G_{\circ}} \cup V_{G_{\bullet}})^\ast\)
is a finite sequence of vertices from the two graphs. We call \(\sigma\) a state
of the construction. We distinguish consistent and live states based on
certain sets of local and global properties, respectively:

Call a state \(\sigma\) of the construction consistent if and only if all
pairs \(\langle S, (v_1, \ldots, v_n) \rangle \in \sigma\) satisfy the following conditions:

* mutual exclusion: at most one polarity is assigned to each name in \(S\),
i.e. for all \((x, p), (y, q) \in S\), \(x = y\) implies \(p = q\); equivalently,
if \((x, p) \in S\) then \((x, \co{p}) \notin S\).

* alternation: \(v_1, \ldots, v_n\) is an alternating path;

* inclusion: if \(v_1 \in I\) (resp. \(v_n \in I\)), then there is
\(p \in \data{Pol}\) such that \((v_1, p) \in S\) (resp. \((v_n, p) \in S\));

* coloring: if \((v_1, p) \in S\) (resp. \((v_n, p) \in S\)), then
the alternating path \(v_1, \ldots, v_n\) is \(p\)-initial (resp. \(p\)-final).

Consider now two sets \(S, T \subseteq I \times \data{Pol}\) of name-polarity pairs.
We say that \(S, T\) compose on name \(x \in \mathcal{N}\) (notation \(S \stackrel{x}{\bowtie} T\))
iff there is a polarity \(p \in \data{Pol}\) such that \((x, p) \in S\), \((x, \co{p}) \in T\)
and \(S \setminus \{(x,p)\} = T \setminus \{(x, \co{p})\}\).

Call a state \(\sigma\) of the construction live iff it is non-empty and,
for all \(\langle S, \vec{z} \rangle \in \sigma\) and \((x, p) \in S\), there is
\(\langle T, \vec{w} \rangle \in \sigma\) such that \(S \stackrel{x}{\bowtie} T\).

Now let us define for any state \(\sigma\) the set of live names of \(\sigma\):

\[
\data{names}(\sigma) = \{ x \in \mathcal{N} \mid \langle S, \vec{z} \rangle \in \sigma, (x, p) \in S \}.
\]

Call a state \(\sigma\) of the construction terminal iff for all \(\langle S,
\vec{z} \rangle \in \sigma\), \(S\) is empty; equivalently iff \(\data{names}(\sigma)
= \emptyset\).

Let \(\sigma\) be any consistent, live and terminal state: there is a pair \(\langle
S, \vec{z} \rangle \in \sigma\) such that \(\vec{z}\) is a complete alternating

By liveness \(\sigma\) is non-empty, i.e. there is at least one pair \(\langle S,
\vec{z} \rangle \in \sigma\). Let \(\vec{z} = z_1, \ldots, z_n\) and assume \(z_1 \in I\):
by the inclusion condition (consistency) there should be \(p \in \data{Pol}\) such that
\((z_1, p) \in S\), against the hypothesis that \(\sigma\) be terminal, hence \(z_1 \notin I\).
The same argument shows that \(z_n \notin I\).

If there is a consistent, live and terminal state, then there is a complete \(X\)-labeled
alternating path between \(G_{\circ}\) and \(G_{\bullet}\) through interface \(I\).

If there is a consistent, live and terminal state, then the composite bl-graph \(G_{\circ}
\odot_I G_{\bullet}\) has at least one edge.

We come now to the key lemma of this proof, showing that every consistent and live state
can be transformed into a consistent, live and terminal one in a finite number of steps.
Thus we reduce the problem of showing that the composite graph is non-empty to that of
constructing a consistent and live state.

For any consistent and live state \(\sigma\) such that \(\data{names}(\sigma)\)
is non-empty, there is a consistent and live state \(\tau\) such that

\[
\data{names}(\tau) \subsetneq \data{names}(\sigma).
\]

Because the interface \(I\) is finite by assumption, the set of live names of any state
must be finite, therefore we can reach a terminal one by iterating the reduction lemma
finitely many times:

If there is a consistent and live state, then there is a consistent, live and terminal state.

If there is a consistent and live state, then the composite bl-graph \(G_{\circ}
\odot_I G_{\bullet}\) has at least one edge.

By assumption there is \(x \in \data{names}(\sigma)\). We associate to every pair
\(\langle S, \vec{z} \rangle \in \sigma\) a new pair \(\langle S', \vec{z}' \rangle\)
constructed as follows, while simultaneously proving that the new pair satisfies all
consistency conditions (<ref>):

* if there is no \(p \in \data{Pol}\) such that \((x, p) \in S\), then let
\(S' = S\), \(\vec{z}' = \vec{z}\); all consistency conditions are clearly preserved;

* otherwise let \(\langle T, \vec{w} \rangle \in \sigma\) be the pair
such that \(S \stackrel{x}{\bowtie} T\), whose existence is guaranteed by liveness:
we have \(p \in \data{Pol}\) such that \((x, p) \in S\) and \((x, \co{p}) \in T\);

* let \(S' = S \setminus \{(x, p)\} = T \setminus \{(x, \co{p})\}\); since we
are just removing one pair, mutual exclusion is preserved;

* let \(\vec{z} = z_1, \ldots, z_n\) and \(\vec{w} = w_1, \ldots, w_n\);

* if both \(z_1, z_n \neq x\), then let \(\vec{z}' = \vec{z}\); the last three
consistency conditions are preserved because no endpoint is \(x\);

* if on the other hand \(w_1, w_n \neq x\), then let \(\vec{z}' = \vec{w}\);
the last three consistency conditions are preserved because no endpoint is \(x\)
and \(S' = T \setminus \{(x, \co{p})\}\);

* otherwise there are four mutually exclusive cases:

* if \(z_n = x, w_1 = x\) then let \(\vec{z}' = z_1, \ldots, (z_n = w_1), \ldots, w_n\);

* if \(z_n = x, w_n = x\) then let \(\vec{z}' = z_1, \ldots, (z_n = w_n), \ldots, w_1\);

* if \(z_1 = x, w_1 = x\) then let \(\vec{z}' = z_n, \ldots, (z_1 = w_1), \ldots, w_n\);

* if \(z_1 = x, w_n = x\) then let \(\vec{z}' = z_n, \ldots, (z_1 = w_n), \ldots, w_1\).

For the inclusion condition, observe that no repetition of vertices is allowed in
an alternating path; because the endpoint \(x\) has become internal in \(\vec{z}'\),
inclusion must still hold for the other endpoints. For alternation: \(\vec{z}'\) is
obtained by joining two sequences on \(x\), after possibly reversing them. Reversal
preserves alternating paths by <ref>; the composition is
correct (<ref>) because the two original pairs satisfy
the coloring condition, hence the first half is \(p\)-final and the second half
is \(\co{p}\)-initial. Finally, the coloring condition is preserved because the
endpoints preserve their original initiality and finality by <ref>.

Clearly the construction is performed in such a way that for any \(\langle S, \vec{z} \rangle
\in \sigma\), there is no \(p \in \data{Pol}\) such that \((x, p) \in S'\). We define
then \(\tau\) as

\[
\tau = \{ \langle S', \vec{z}' \rangle \mid \langle S, \vec{z} \rangle \in \sigma \}.
\]

Since \(\sigma\) is finite, so is \(\tau\), hence it is a consistent state. We have obviously

\[
\data{names}(\tau) \subseteq \data{names}(\sigma)
\]

and from what we said above we known that \(x \notin \data{names}(\tau)\), hence the
inclusion is strict, as required.

We have now to show that \(\tau\) is live (<ref>). It must be non-empty
because so is \(\sigma\); let then \(\langle S', \vec{z}' \rangle \in \tau\) and \((y, p)
\in S'\): by construction there is some pair \(\langle S, \vec{z} \rangle \in \sigma\)
such that \(S' = S \setminus \{(x, q)\}\), and by the liveness of \(\sigma\) there is
another pair \(\langle T, \vec{w} \rangle \in \sigma\) such that \(S \stackrel{y}{\bowtie}
T\). Then there is a pair \(\langle T', \vec{w}' \rangle \in \tau\) such that \(T' =
T \setminus \{(x, \co{q})\}\), and we have \(S' \stackrel{y}{\bowtie} T'\): remembering
that \(y \neq x\),

* \((y, p) \in (S \setminus \{(x, q)\}) = S'\);

* \((y, \co{p}) \in (T \setminus \{(x, \co{q})\}) = T'\);

* \(S' \setminus \{(y, p)\} = (S \setminus \{(y, p)\}) \setminus \{(x, q)\}\\
\null\qquad\qquad
= (T \setminus \{(y, \co{p})\}) \setminus \{(x, \co{q})\}
= T' \setminus \{(y, \co{p})\}\).

As announced above, we complete the proof of <ref> by
showing that a consistent and live state can be constructed. We start with an auxiliary

For any sharing-free named formula \(A\) and function

\[
f: \data{names}(A) \to \data{Pol}
\]

there is either \(X \in \data{Br}(A)\) such that \(fX = \{{\circ}\}\) or \(Y \in
\data{Br}(\dl{A})\) such that \(fY = \{{\bullet}\}\).

By induction on \(A\). If \(A = \nm{x}{\alpha}\) then \(\data{Br}(A) = \data{Br}(\dl{A})
= \{{x}\}\), and necessarily either \(f\{x\} = \{{\circ}\}\) or \(f\{x\} = \{{\bullet}\}\).

If \(A = B \land C\) (with \(\dl{A} = \dl{B} \lor \dl{C}\)) then \(\data{Br}(A) =
\data{Br}(B) \cup \data{Br}(C)\)). By induction hypothesis there is either \(X' \in
\data{Br}(B)\) such that \(fX' = \{{\circ}\}\) or \(Y' \in \data{Br}(\dl{B})\)
such that \(fY' = \{{\bullet}\}\). In the first case, let \(X = X'\) and we're done.
Otherwise, there is again by induction hypothesis either \(X'' \in \data{Br}(C)\)
s.t. \(fX'' = \{{\circ}\}\), or \(Y'' \in \data{Br}(\dl{C})\) s.t. \(fY'' = \{{\bullet}\}\).
If there is such a \(X''\), let \(X = X''\); otherwise, let \(Y = Y' \cup Y'' \in
\data{Br}(\dl{B} \lor \dl{C})\): we have \(fY = fY' \cup fY'' = \{{\bullet}\}\).

If \(A = B \lor C\), apply the same argument, swapping polarities and \(A\) with \(\dl{A}\).

We fix \(G_{\circ} = \blaxg{P}\), \(G_{\bullet} = \blaxg{Q}\) and \(I = \data{names}(A)\).
\(I\) is obviously finite, and because the context of the conclusions of \(P, Q\) is
atomic by hypothesis, the condition about branches is satisfied too (the unique branch
name \(X\) is the unique one in \(\data{Br}(\Gamma)\), i.e. \(\data{names}(\Gamma)\)).

We construct a state \(\sigma\) as follows:

\[
\sigma = \{ \langle f, (x,y) \rangle \mid f \in \data{Pol}^I, p \in \data{Pol}, xy \adin_{G_p} X \cup Y, fY = \{p\} \}.
\]

Let us unpack the construction first, then we shall prove that the state is consistent
and live. \(\data{Pol}^I\) is the set of all functions from \(I = \data{names}(A)\)
to \(\data{Pol}\) seen as sets of pairs, i.e. \(\data{Pol}^I \subseteq I \times \data{Pol}\);
we pair each \(f \in \data{Pol}^I\) with any finite sequence \(x,y\) of vertices
such that, for at least one polarity \(p \in \data{Pol}\), \(xy\) is an edge in \(G_p\),
and moreover one of its branch labels satisfies the following conditions:

* it is equal to \(X \cup Y\) for some \(Y\) (where \(X\) is the unique branch
name of \(\Gamma\) described above);

* it is such that \(fY = \{p\}\).

\(\sigma\) is clearly finite, hence a state. For consistency (<ref>),
let \(\langle f, (x,y) \rangle \in \sigma\):

* mutual exclusion: this condition can be read as asking that \(f\)
be the graph of a function, hence it is obviously satisfied;

* alternation: \(xy\) is an edge in either \(G_{\circ}\) or \(G_{\bullet}\)
by construction, hence an alternating path by <ref>;

* inclusion: because \(f\) is total, if \(x \in I\) then \((x, fx) \in f\),
and similarly for \(y\);

* coloring: let \((x, p) \in f\); by construction there is \(q \in
\data{Pol}\), \(Y \in \mathcal{N}\) such that \(xy \adin_{G_q} X \cup Y\) with
\(fY = \{q\}\). By <ref>, every branch name of \(G_q\)
is the union of the unique branch name \(X\) of \(\Gamma\) with some branch name
of either \(A\) (if \(q = {\circ}\)) or \(\dl{A}\) (if \(q = {\bullet}\)).
If \(q = {\circ}\), then, \(Y \in \data{Br}(A)\), otherwise \(Y \in \data{Br}(\dl{A})\).
By <ref> \(x \in X \cup Y\), and because \(x \in I\) we must
have \(x \in Y\). We know that \(fY = \{q\}\), hence in particular \(p = f(x) = q\).
The path \(x,y\) is obviously \(q\)-initial, hence \(p\)-initial. Analogous reasoning
shows that if \((y, p') \in f\), then the path is \(p'\)-final.

For liveness (<ref>) we argue first that \(\sigma\) is non-empty:
by <ref> above, there is for each \(f \in
\data{Pol}^I\) at least one branch \(Y \in \data{Br}(A)\) with \(fY = \{{\circ}\}\)
or \(Y \in \data{Br}(\dl{A})\) with \(fY = \{{\bullet}\}\). Let \(fY = \{p\}\);
by <ref>, \((X \cup Y) \in \data{Br}(G_p)\),
i.e. there is \(e \adin_{G_p} X \cup Y\). We have thus proven not just that \(\sigma\)
is non-empty, but also that for each \(f \in \data{Pol}^I\) there is at least one
pair \(\langle f, \vec{z} \rangle \in \sigma\).

Now let \(\langle f, \vec{z} \rangle \in \sigma\), \((x, p) \in f\); by inverting the polarity
assignment of \(x\) in \(f\) we obtain \(f' = (f \setminus \{(x,p)\}) \cup \{(x, \co{p})\}
\in \data{Pol}^I\). By the reasoning above there is \(\langle f', \vec{w} \rangle \in \sigma\),
and it is immediate by construction that \(f \stackrel{x}{\bowtie} f'\).

§ TOTALITY LEMMAS AND CORRECTNESS ALGORITHM FOR BLG

By structural induction on \(P\). If \(P\) ends with an axiom rule application,
the conclusion is equivalent to <ref>; if \(P\) ends with
a superposition rule application, it follows immediately from the induction hypothesis;
if \(P\) ends with a logical rule, we conclude from the induction hypothesis and
<ref>, points (ii) and (iii). The details
are left to the reader.

We have \(\data{names}(\Gamma, A, B) = \data{names}(\Gamma, A \lor B)\); \(\data{Br}(
\Gamma, A, B) = \data{Br}(\Gamma, A \lor B)\) by <ref>;
and finally \((\Gamma, A, B)[x] = (\Gamma, A \lor B)[x]\) for all \(x \in \data{names}(
\Gamma, A, B)\).

We have two prove two facts: (i) that \(G\) is effectively equal to the union
of the two restrictions, and (ii) that the two restrictions are total w.r.t. the
restricted conclusions. For fact (i), we have obviously

\[
\data{names}(\Gamma, A \land B) = \data{names}(\Gamma, A) \cup \data{names}(\Gamma, B).
\]

Then by construction \(V_{G \rst_{\Gamma, A}} = \data{names}(\Gamma, A)\) and
\(V_{G \rst_{\Gamma, B}} = \data{names}(\Gamma, B)\), hence \(V_G = V_{G \rst_{\Gamma, A}}
\cup V_{G \rst_{\Gamma, B}}\). Now let \(e \adin_G X\). By totality \(X \in \data{Br}(\Gamma,
A \land B)\); then by <ref> either \(X \in
\data{Br}(\Gamma, A)\) or \(X \in \data{Br}(\Gamma, B)\): in the first case we have
\(X \subseteq \data{names}(\Gamma, A)\) hence \(e \adin_{G \rst_{\Gamma, A}} X\);
similarly in the second case we have \(e \adin_{G \rst_{\Gamma, B}} X\). The reverse
inclusion is obvious.

For fact (ii), we have already argued that the two restriction have the appropriate vertex
sets (<ref>, point (i)); that all edges link dual atoms (<ref>,
point (iii)) follows from the fact that the edges come from \(G\), which satisfies the same
condition, and for all \(x \in \data{names}(\Gamma, A)\) (resp. \(\data{names}(\Gamma, B)\))
we have \((\Gamma, A \land B)[x] = (\Gamma, A)[x]\) (resp. \((\Gamma, B)[x]\)). Finally
we have to show that \(\data{Br}(G \rst_{\Gamma, A}) = \data{Br}(\Gamma, A)\) and
\(\data{Br}(G \rst_{\Gamma, B}) = \data{Br}(\Gamma, B)\) (<ref>, point (ii)).
The forward inclusions are proved already in <ref>.
For the reverse, let \(X \in \data{Br}(\Gamma, A)\) (resp. \(\data{Br}(\Gamma, B)\));
by totality there is \(e \adin_G X\), and because \(X \subseteq \data{names}(\Gamma, A)\)
(resp. \(\data{names}(\Gamma, B)\)) we have \(e \adin_{G \rst_{\Gamma, A}} X\) (resp.
\(e \adin_{G \rst_{\Gamma, B}} X\)).

§.§ Correctness algorithm for BLG

We work under the reasonable assumption that checking name equality requires constant time.
Let us start by recalling the definition of the size of \(\mathbf{G}\) (<ref>):

\[
\data{size}(\mathbf{G}) = \data{size}(\th \Gamma) + |V_G| + \sum_{e \adin_G X} |X|.
\]

The size of \(\th \Gamma\) (<ref>, <ref>) is by
<ref> the sum of the number of atom occurrences
in \(\Gamma\) (notation \(\data{\#at}(\th \Gamma)\)) with the number of logical symbols,
also called the degree of \(\Gamma\) (notation \(\data{deg}(\Gamma)\)). Because
\(\Gamma\) is sharing-free by hypothesis, the number of atom occurrences coincides with
the number of names, i.e. \(\data{\#at}(\th \Gamma) = |\data{names}(\Gamma)|\).

Observe also that the sum at the end of the expression is taken not over the set
of branches of \(G\), but over all edge-branch pairs, i.e. a branch may be counted
more than once if it has multiple edges. Because \(e \adin_G X\) implies \(e \subseteq X\),
i.e. no branch in a bl-graph is empty, the sum provides an upper bound to the
number of edge-branch pairs as well as to that of edges and branches, i.e. we have

\[
|E_G|, |\data{Br}(G)| \leq |{\adin_G}| \leq \data{size}(\mathbf{G}).
\]

We have to check three conditions separately (<ref>):

* \(V_G = \data{names}(\Gamma)\): checking name set equality is worst-case
polynomial in their cardinalities, and constructing the set \(\data{names}(\Gamma)\)
from \(\Gamma\) requires polynomial time in the size of \(\th \Gamma\);

* \(\data{Br}(G) = \data{Br}(\Gamma)\): this is the most complex problem.
Generating just one element in \(\data{Br}(\Gamma)\) amounts to persistently expanding
one branch of a \(\data{GS4}^\mathcal{N}\) derivation of \(\Gamma\) until an atomic
sequent is reached; the length of such a branch is known to be bounded by the
complexity degree of \(\th \Gamma\) <cit.>, hence the cost of generating
one branch name is polynomially bounded in the size of \(\th \Gamma\). However,
the total number of branches is in the worst case exponential in the complexity
degree of \(\th \Gamma\): thus we cannot take the naive approach of constructing
the whole set \(\data{Br}(\Gamma)\), then testing for equality. We describe an
informal algorithm: the idea is to generate the branch names of \(\Gamma\)
incrementally, match them with some element from the set \(\data{Br}(G)\) and
erase that element. For every matching attempt, either the algorithm fails or
the number of branches still to be matched decreases: in this way the number
of generated branch names is always bounded by the cardinality of \(\data{Br}(G)\).
Let \(S\) be the branch set to test (initially \(S = \data{Br}(G)\)), \(\Delta\)
the sequent to test against (initially \(\Delta = \Gamma\)); the algorithm has
three phases:

* problem reduction phase: if the sequent \(\Delta\) to test
against contains a disjunction, i.e. is of the form \(\Delta', A \lor B\),
then replace it with \(\Delta', A, B\). If it contains no disjunction but
at least a conjunction, i.e. is of the form \(\Delta', A \land B\), then
replace it with \(\Delta', A\) and append \(\Delta', B\) to a list of
sequents to test against later. By <ref>,
the set of branches to test against has not changed;

* matching phase: if the sequent \(\Delta\) to test against is atomic,
then it has a unique branch \(X = \data{names}(\Delta)\). We search for that branch
in \(S\): if not found, then \(X \in \data{Br}(\Gamma)\) but \(X \notin \data{Br}(G)\),
and we stop; if found, we erase \(X\) from \(S\) and move on to the backtracking

* backtracking phase: if both \(S\) and the list of delayed sequents are
empty, then we're done. If \(S\) is empty but the list is not, then some branches
are missing from \(\data{Br}(G)\) and we stop. If \(S\) has some elements but
the list is empty, then there are excess branches in \(\data{Br}(G)\) and we
stop. If both are non-empty, we pick the first element of the list as the new
\(\Delta\), erase it from the list and move back to the reduction phase.

It is clear that the number of steps in the reduction phase is bounded by the complexity
degree of the active sequent \(\Delta\), which always decreases: when it reaches zero,
we move to the matching phase. The matching phase either fails or decreases the
size of the set \(B\); once the set \(B\) becomes empty, the algorithm stops:
thus the size of \(B\) bounds the number of future reduction phases. Observe now that
a reduction step requires polynomial time in the size of the active sequent;
a matching step requires polynomial time in the cardinality of the generated branch
and the sum of the cardinalities of all elements of \(B\). Backtracking steps require
constant time. Every measure mentioned above is itself bounded by \(\data{size}(\mathbf{G})\).
We have then a polynomial bound on the execution time of the algorithm with parameter
\((\data{size}(\mathbf{G}))^3\).

* for all \(xy \in E_G\), \(\Gamma[x] = \dl{\Gamma[y]}\): we observed at the
beginning of the proof that \(\data{size}(\mathbf{G})\) bounds \(|E_G|\); finding
the atom associated to a given name in \(\Gamma\) is polynomial in the size
of \(\th \Gamma\).

[{xα, uα}]ax
þxx-1α, yα, uu-1α
þxx-2α yα, uu-2α
[{zα, uα}]ax
þzα, wα, uα
þzα wα, uα
þ(xx-3α yα) (zα wα), uu-3α
[{yα, uα}]ax
þxα, yα, uα
þxα yα, uα
[{wα, uα}]ax
þzα, ww-1α, uu-4α
þzα ww-2α, uu-5α
þ(xα yα) (zα ww-3α), uu-6α
þ(xx-4α yα) (zα ww-4α)

[remember picture, overlay, thick, blue]

([yshift=2pt]x-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]u-1.north);
([yshift=2pt]w-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]u-4.north);

([yshift=2pt]x-4.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]x-3.south);
([yshift=2pt]x-3.north) .. controls ++(0,5pt) and ++(0,-5pt) .. ([yshift=-1pt]x-2.south);
([yshift=2pt]x-2.north) .. controls ++(0,2pt) and ++(0,-2pt) .. ([yshift=-1pt]x-1.south);

([yshift=1pt]u-2.north) .. controls ++(0,4pt) and ++(0,-4pt) .. ([yshift=-1pt]u-1.south);
([yshift=1pt]u-3.north) .. controls ++(0,10pt) and ++(0,-7pt) .. ([yshift=-1pt]u-2.south);

([yshift=1pt]w-4.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]w-3.south);
([yshift=1pt]w-3.north) .. controls ++(0,8pt) and ++(0,-4pt) .. ([yshift=-1pt]w-2.south);
([yshift=1pt]w-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. ([yshift=-1pt]w-1.south);

([yshift=2pt]u-5.north) .. controls ++(0,3pt) and ++(0,-3pt) .. ([yshift=-1pt]u-4.south);
([yshift=2pt]u-6.north) .. controls ++(0,5pt) and ++(0,-5pt) .. ([yshift=-1pt]u-5.south);

[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]u-3.south) – ([yshift=-2.3em]u-3.south) – ([yshift=-2.3em]u-6.south) – ([yshift=-1pt]u-6.south);

The initial derivation, where the conjunction in the conclusion is not
introduced by the last rule. Assume names \(x, y, z, w, u \in \mathcal{N}\)
are pairwise distinct.

[{xα, uα}]ax
þxx-1α, yα, uu-1α
þxx-2α yα, uu-2α
[{yα, uα}]ax
þxα, yα, uα
þxα yα, uu-3α
þxx-3α yα
[{zα, uα}]ax
þzα, wα, uα
þzα wα, uu-6α
[{wα, uα}]ax
þzα, ww-1α, uu-4α
þzα ww-2α, uu-5α
þzα ww-3α
þ(xx-4α yα) (zα ww-4α)

[remember picture, overlay, thick, blue]

([yshift=2pt]x-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]u-1.north);
([yshift=2pt]w-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]u-4.north);

([yshift=2pt]x-4.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]x-3.south);
([yshift=2pt]x-3.north) .. controls ++(0,8pt) and ++(0,-8pt) .. ([yshift=-1pt]x-2.south);
([yshift=2pt]x-2.north) .. controls ++(0,2pt) and ++(0,-2pt) .. ([yshift=-1pt]x-1.south);

([yshift=1pt]u-2.north) .. controls ++(0,4pt) and ++(0,-4pt) .. ([yshift=-1pt]u-1.south);

([yshift=1pt]w-4.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]w-3.south);
([yshift=1pt]w-3.north) .. controls ++(0,10pt) and ++(0,-7pt) .. ([yshift=-1pt]w-2.south);
([yshift=1pt]w-2.north) .. controls ++(0,3pt) and ++(0,-3pt) .. ([yshift=-1pt]w-1.south);

([yshift=2pt]u-5.north) .. controls ++(0,3pt) and ++(0,-3pt) .. ([yshift=-1pt]u-4.south);

[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]u-2.south) – ([yshift=-3em]u-2.south) – ([shift=(-5em,-3em)]u-3.south)
– ([shift=(-5em,-1em)]u-3.south) – ([yshift=-1em]u-3.south) – ([yshift=-1pt]u-3.south);
[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]u-5.south) – ([yshift=-3em]u-5.south) – ([yshift=-3em]u-6.south) – ([yshift=-1pt]u-6.south);

The transformed derivation, after isolating the conjuction. The two halves of the original alternating path
are now disconnected.

[math nodes]
x –[bend left] y –[bend right] z –[bend left] w;
x –[bend right] w;

[math nodes]
x –[bend left] y -!- z –[bend left] w;
x –[bend right, opacity=0] w;

The axiom graph of the original derivation (left) and that of the transformed
one (right).

A derivation with cuts whose axiom graph decreases when isolating the conjunction
in its conclusion.

[{xα, tα}]ax
þxα, yα, zβ, tα, vα
[{xα, tα}]ax
þxα, yα, zβ, tα, wβ
þxα, yα, zβ, tα, vα wβ
[{yα, vα}]ax
þxα, yy-l-1α, zβ, uβ, vv-l-1α
[{zβ, wβ}]ax
þxα, yα, zβ, uβ, wβ
þxα, yy-l-2α, zβ, uβ, vv-l-2α wβ
þxα, yy-l-3α, zβ, tα uβ, vv-l-3α wβ
[{tα, vα}]ax
þxα, yα, zβ, tt-r-1α, vv-r-1α, wβ
þxα, yα, zβ, tt-r-2α, vv-r-2α wβ
[{uβ, wβ}]ax
þxα, yα, zβ, uβ, vα, wβ
þxα, yα, zβ, uβ, vα wβ
þxα, yα, zβ, tt-r-3α uβ, vv-r-3α wβ
þxα, yy-4α, zβ, tt-4α uβ

[remember picture, overlay, thick, blue]

([yshift=2pt]y-l-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]v-l-1.north);
([yshift=2pt]t-r-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]v-r-1.north);

([yshift=2pt]y-4.north) .. controls ++(0,30pt) and ++(0,-20pt) .. ([yshift=-1pt]y-l-3.south);
([yshift=2pt]y-l-3.north) .. controls ++(0,25pt) and ++(0,-10pt) .. ([yshift=-1pt]y-l-2.south);
([yshift=2pt]y-l-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]y-l-1.south);

([yshift=1pt]v-l-3.north) .. controls ++(0,15pt) and ++(0,-20pt) .. ([yshift=-1pt]v-l-2.south);
([yshift=1pt]v-l-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]v-l-1.south);

([yshift=1pt]t-4.north) .. controls ++(0,30pt) and ++(0,-20pt) .. ([yshift=-1pt]t-r-3.south);
([yshift=1pt]t-r-3.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]t-r-2.south);
([yshift=1pt]t-r-2.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]t-r-1.south);

([yshift=2pt]v-r-3.north) .. controls ++(0,15pt) and ++(0,-7pt) .. ([yshift=-1pt]v-r-2.south);
([yshift=2pt]v-r-2.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]v-r-1.south);

[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]v-l-3.south) – ([yshift=-3.3em]v-l-3.south) – ([yshift=-3.3em]v-r-3.south) – ([yshift=-1pt]v-r-3.south);

The initial derivation, where the conjunction in the conclusion is not
introduced by the last rule. Assume names \(x, y, z, t, u, v, w \in \mathcal{N}\)
are pairwise distinct.

[{xα, tα}]ax
þxα, yα, zβ, tα, vα
[{xα, tα}]ax
þxα, yα, zβ, tα, wβ
þxα, yα, zβ, tα, vv-lα wβ
[{tα, vα}]ax
þxα, yα, zβ, tt-r-1α, vv-r-1α, wβ
þxα, yα, zβ, tt-r-2α, vv-r-2α wβ
þxα, yα, zβ, tt-r-3α
[{yα, vα}]ax
þxα, yy-l-1α, zβ, uβ, vv-l-1α
[{zβ, wβ}]ax
þxα, yα, zβ, uβ, wβ
þxα, yy-l-2α, zβ, uβ, vv-l-2α wβ
[{uβ, wβ}]ax
þxα, yα, zβ, uβ, vα, wβ
þxα, yα, zβ, uβ, vv-rα wβ
þxα, yy-l-3α, zβ, uβ
þxα, yy-4α, zβ, tt-4α uβ

[remember picture, overlay, thick, blue]

([yshift=2pt]y-l-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]v-l-1.north);
([yshift=2pt]t-r-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]v-r-1.north);

([yshift=2pt]y-4.north) .. controls ++(0,30pt) and ++(0,-20pt) .. ([yshift=-1pt]y-l-3.south);
([yshift=2pt]y-l-3.north) .. controls ++(0,25pt) and ++(0,-10pt) .. ([yshift=-1pt]y-l-2.south);
([yshift=2pt]y-l-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]y-l-1.south);

([yshift=1pt]v-l-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]v-l-1.south);

([yshift=1pt]t-4.north) .. controls ++(0,30pt) and ++(0,-20pt) .. ([yshift=-1pt]t-r-3.south);
([yshift=1pt]t-r-3.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]t-r-2.south);
([yshift=1pt]t-r-2.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]t-r-1.south);

([yshift=2pt]v-r-2.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]v-r-1.south);

[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]v-l-2.south) – ([yshift=-4.7em]v-l-2.south) – ([yshift=-4.7em]v-r.south) – ([yshift=-1pt]v-r.south);
[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]v-r-2.south) – ([yshift=-4.7em]v-r-2.south) – ([yshift=-4.7em]v-l.south) – ([yshift=-1pt]v-l.south);

The transformed derivation, after isolating the conjuction. The two halves of the original alternating path
are now disconnected.

[math nodes]
x -!- y -!- z -!- t -!- u;
x –[bend left] t;
z –[bend left] u;
y –[bend right] t;

[math nodes]
x -!- y -!- z -!- t -!- u;
x –[bend left] t;
z –[bend left] u;
y –[bend right, opacity=0] t;

The axiom graph of the original derivation (left) and that of the transformed
one (right).

A derivation with cuts whose axiom graph decreases when isolating the conjunction
in its conclusion. The lost path does not visibly cross a conjunction.

þxβ, yβ, zz-l-1α, tt-l-1α, vα, wα
þxβ, yβ, zα, uα, vα, wα
þxβ, yβ, zz-l-2α, tt-l-2α uα, vα, wα
þxβ, yβ, sα, tα, vα, wα
þxβ, yβ, ss-l-1α, uu-l-1α, vα, wα
þxβ, yβ, ss-l-2α, tα uu-l-2α, vα, wα
þxβ, yβ, zz-l-3α ss-l-3α, tt-l-3α uu-l-3α, vα, wα
þxβ, yβ, (zz-l-4α ss-l-4α) (tt-l-4α uu-l-4α), vα, wα
þxβ, yβ, zz-r-1α, ss-r-1α, vα, wα
þxβ, yβ, zz-r-2α ss-r-2α, vα, wα
þxβ, yβ, tt-r-1α, uα, vv-r-1α, wα
þxβ, yβ, tα, uu-r-1α, vα, ww-r-1α
þxβ, yβ, tt-r-2α, uu-r-2α, vv-r-2α, ww-r-2α
þxβ, yβ, tt-r-3α uu-r-3α, vv-r-3α, ww-r-3α
þxβ, yβ, (zz-r-3α ss-r-3α) (tt-r-4α uu-r-4α), vv-r-4α, ww-r-4α
þxβ, yβ, vv-5α, ww-5α

[remember picture, overlay, thick, blue]

([yshift=2pt]z-l-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]t-l-1.north);
([yshift=2pt]s-l-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]u-l-1.north);
([yshift=2pt]z-r-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]s-r-1.north);
([yshift=2pt]t-r-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]v-r-1.north);
([yshift=2pt]u-r-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]w-r-1.north);

([yshift=1pt]z-l-4.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]z-l-3.south);
([yshift=1pt]z-l-3.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]z-l-2.south);
([yshift=1pt]z-l-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]z-l-1.south);

([yshift=2pt]s-l-4.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]s-l-3.south);
([yshift=2pt]s-l-3.north) .. controls ++(0,20pt) and ++(0,-10pt) .. ([yshift=-1pt]s-l-2.south);
([yshift=2pt]s-l-2.north) .. controls ++(0,15pt) and ++(0,-5pt) .. ([yshift=-1pt]s-l-1.south);

([yshift=2pt]t-l-4.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]t-l-3.south);
([yshift=2pt]t-l-3.north) .. controls ++(0,20pt) and ++(0,-10pt) .. ([yshift=-1pt]t-l-2.south);
([yshift=2pt]t-l-2.north) .. controls ++(0,15pt) and ++(0,-5pt) .. ([yshift=-1pt]t-l-1.south);

([yshift=1pt]u-l-4.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]u-l-3.south);
([yshift=1pt]u-l-3.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]u-l-2.south);
([yshift=1pt]u-l-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]u-l-1.south);

([yshift=2pt]z-r-3.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]z-r-2.south);
([yshift=2pt]z-r-2.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]z-r-1.south);

([yshift=1pt]s-r-3.north) .. controls ++(0,20pt) and ++(0,-10pt) .. ([yshift=-1pt]s-r-2.south);
([yshift=1pt]s-r-2.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]s-r-1.south);

([yshift=1pt]t-r-4.north) .. controls ++(0,25pt) and ++(0,-10pt) .. ([yshift=-1pt]t-r-3.south);
([yshift=1pt]t-r-3.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]t-r-2.south);
([yshift=1pt]t-r-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]t-r-1.south);

([yshift=2pt]u-r-4.north) .. controls ++(0,20pt) and ++(0,-15pt) .. ([yshift=-1pt]u-r-3.south);
([yshift=2pt]u-r-3.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]u-r-2.south);
([yshift=2pt]u-r-2.north) .. controls ++(0,15pt) and ++(0,-5pt) .. ([yshift=-1pt]u-r-1.south);

([yshift=2pt]v-5.north) .. controls ++(0,35pt) and ++(0,-25pt) .. ([yshift=-1pt]v-r-4.south);
([yshift=2pt]v-r-4.north) .. controls ++(0,15pt) and ++(0,-20pt) .. ([yshift=-1pt]v-r-3.south);
([yshift=2pt]v-r-3.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]v-r-2.south);
([yshift=2pt]v-r-2.north) .. controls ++(0,15pt) and ++(0,-5pt) .. ([yshift=-1pt]v-r-1.south);

([yshift=1pt]w-5.north) .. controls ++(0,20pt) and ++(0,-30pt) .. ([yshift=-1pt]w-r-4.south);
([yshift=1pt]w-r-4.north) .. controls ++(0,10pt) and ++(0,-25pt) .. ([yshift=-1pt]w-r-3.south);
([yshift=1pt]w-r-3.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]w-r-2.south);
([yshift=1pt]w-r-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]w-r-1.south);

[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]z-l-4.south) – ([yshift=-5em]z-l-4.south) – ([yshift=-5em]z-r-3.south) – ([yshift=-1pt]z-r-3.south);
[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]s-l-4.south) – ([yshift=-6em]s-l-4.south) – ([yshift=-6em]s-r-3.south) – ([yshift=-1pt]s-r-3.south);
[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]t-l-4.south) – ([yshift=-3em]t-l-4.south) – ([yshift=-3em]t-r-4.south) – ([yshift=-1pt]t-r-4.south);
[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]u-l-4.south) – ([yshift=-4em]u-l-4.south) – ([yshift=-4em]u-r-4.south) – ([yshift=-1pt]u-r-4.south);

The initial derivation, with a unique cut-rule. Assume names \(x, y, z, s, t, u,
v, w \in \mathcal{N}\) are pairwise distinct. There is an alternating path
connecting \(\nm{v}{\dl{\alpha}}\) with \(\nm{w}{\alpha}\). Because the conclusion
is atomic, there is only one branch name up to names in the interface, hence all
edges are compatible.

þxβ, yβ, zz-l-1α, tt-l-1α, vα, wα
þxβ, yβ, zα, uα, vα, wα
þxβ, yβ, zz-l-2α, tt-l-2α uα, vα, wα
þxβ, yβ, sα, tα, vα, wα
þxβ, yβ, ss-l-1α, uu-l-1α, vα, wα
þxβ, yβ, ss-l-2α, tα uu-l-2α, vα, wα
þxβ, yβ, zz-l-3α ss-l-3α, tt-l-3α uu-l-3α, vα, wα
þxβ, yβ, zz-r-1α, ss-r-1α, tα uα, vα, wα
þxβ, yβ, zz-r-2α ss-r-2α, tα uα, vα, wα
þxβ, yβ, tt-l-4α uu-l-4α, vα, wα
þxβ, yβ, tt-r-1α, uα, vv-r-1α, wα
þxβ, yβ, tα, uu-r-1α, vα, ww-r-1α
þxβ, yβ, tt-r-2α, uu-r-2α, vv-r-2α, ww-r-2α
þxβ, yβ, tt-r-3α uu-r-3α, vv-r-3α, ww-r-3α
þxβ, yβ, vv-4α, ww-4α

[remember picture, overlay, thick, blue]

[red] ([yshift=2pt]z-l-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]t-l-1.north);
[black] ([yshift=2pt]s-l-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]u-l-1.north);
([yshift=2pt]z-r-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]s-r-1.north);
([yshift=2pt]t-r-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]v-r-1.north);
([yshift=2pt]u-r-1.north) .. controls ++(0,1.3em) and ++(0,1.3em) .. ([yshift=2pt]w-r-1.north);

([yshift=1pt]z-l-3.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]z-l-2.south);
([yshift=1pt]z-l-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]z-l-1.south);

([yshift=2pt]s-l-3.north) .. controls ++(0,20pt) and ++(0,-10pt) .. ([yshift=-1pt]s-l-2.south);
([yshift=2pt]s-l-2.north) .. controls ++(0,15pt) and ++(0,-5pt) .. ([yshift=-1pt]s-l-1.south);

([yshift=2pt]t-l-4.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]t-l-3.south);
([yshift=2pt]t-l-3.north) .. controls ++(0,20pt) and ++(0,-10pt) .. ([yshift=-1pt]t-l-2.south);
([yshift=2pt]t-l-2.north) .. controls ++(0,15pt) and ++(0,-5pt) .. ([yshift=-1pt]t-l-1.south);

([yshift=1pt]u-l-4.north) .. controls ++(0,25pt) and ++(0,-10pt) .. ([yshift=-1pt]u-l-3.south);
([yshift=1pt]u-l-3.north) .. controls ++(0,15pt) and ++(0,-15pt) .. ([yshift=-1pt]u-l-2.south);
([yshift=1pt]u-l-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]u-l-1.south);

([yshift=2pt]z-r-2.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]z-r-1.south);

([yshift=1pt]s-r-2.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]s-r-1.south);

([yshift=1pt]t-r-3.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]t-r-2.south);
([yshift=1pt]t-r-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]t-r-1.south);

([yshift=2pt]u-r-3.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]u-r-2.south);
([yshift=2pt]u-r-2.north) .. controls ++(0,15pt) and ++(0,-5pt) .. ([yshift=-1pt]u-r-1.south);

([yshift=2pt]v-4.north) .. controls ++(0,35pt) and ++(0,-25pt) .. ([yshift=-1pt]v-r-3.south);
([yshift=2pt]v-r-3.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]v-r-2.south);
([yshift=2pt]v-r-2.north) .. controls ++(0,15pt) and ++(0,-5pt) .. ([yshift=-1pt]v-r-1.south);

([yshift=1pt]w-4.north) .. controls ++(0,20pt) and ++(0,-30pt) .. ([yshift=-1pt]w-r-3.south);
([yshift=1pt]w-r-3.north) .. controls ++(0,7pt) and ++(0,-7pt) .. ([yshift=-1pt]w-r-2.south);
([yshift=1pt]w-r-2.north) .. controls ++(0,10pt) and ++(0,-10pt) .. ([yshift=-1pt]w-r-1.south);

[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]z-l-3.south) – ([yshift=-5em]z-l-3.south) – ([yshift=-5em]z-r-2.south) – ([yshift=-1pt]z-r-2.south);
[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]s-l-3.south) – ([yshift=-4em]s-l-3.south) – ([yshift=-4em]s-r-2.south) – ([yshift=-1pt]s-r-2.south);
[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]t-l-4.south) – ([yshift=-3.5em]t-l-4.south) – ([yshift=-3.5em]t-r-3.south) – ([yshift=-1pt]t-r-3.south);
[draw, densely dashed, semithick, rounded corners=1em]
([yshift=-1pt]u-l-4.south) – ([yshift=-4.5em]u-l-4.south) – ([yshift=-4.5em]u-r-3.south) – ([yshift=-1pt]u-r-3.south);

A logical cut-reduction step has been applied (see <ref>).
The conjunction \(\nm{t}{\dl{\alpha}} \land \nm{u}{\alpha}\) is now outside the
interface of the upper cut: the alternating path that connects \(\nm{t}{\dl{\alpha}}\)
with \(\nm{u}{\alpha}\) must be omitted when computing the interpretation, as it
uses edges from incompatible branches (highlighted in red and black). As a result,
the edge between \(\nm{v}{\dl{\alpha}}\) and \(\nm{w}{\alpha}\) is lost.

[math nodes]
x -!- y -!- v -!- w;
x –[bend left, "\(\scriptstyle \{x,y,v,w\}\)"] y;
v –[bend left, "\(\scriptstyle \{x,y,v,w\}\)"] w;

[math nodes]
x -!- y -!- v -!- w;
x –[bend left, "\(\scriptstyle \{x,y,v,w\}\)"] y;

The branch-labeled axiom graph of the original derivation (left) and that
of the reduced one (right).

A derivation whose branch-labeled axiom graph decreases when a logical cut-reduction
step is applied.


# Integer Sequences from Circle Divisions in Rational Billiards

Daniel Jaud

###### Abstract

We study rational circular billiards. By viewing the trajectory formed after
each reflection point to another inside the circle as the number of circle
divisions into regions we derive a general formula for the number of division
regions after each reflection. This will give rise to an integer division
sequence. Restricting to the special cases $\vartheta=\frac{q}{2q+1}\cdot
2\pi$ we show that the number of regions after each reflection $n$ is
beautifully related to Gauss ’s arithmetic series.

Keywords— rational billiards, circle division, integer sequence, arithmetic
series

###### Contents

  1. 1 Introduction and setup
  2. 2 Number of intersecting lines
  3. 3 General formula for circle division sequence
  4. 4 Discussion of the special case $\vartheta=\frac{p}{2p+1}\cdot 2\pi$
  5. 5 Conclusion and Outlook

##  1 Introduction and setup

The simplest realization of a billiard table is given by a circular region
$\cal C$. Here we are interested in the trajectory of the billiard ball which
is considered to be a point particle moving inside the boundary of the circle
with unit velocity and bouncing elastically along the boundary $\partial\cal
C$. Due to the elastic collision the incident and reflected angle $\alpha$
with respect to the normal to the boundary are identical. Further, because of
rotational symmetry the system is fully described by the angle $\vartheta$
made by two consecutive scattering points with the circle [6, 3] (see figure
1).

$P_{0}$circle tangent$\vartheta$$\alpha$$\beta$$\beta$ Figure 1: Graphical
representation of the billiard trajectory, the incident angle $\alpha$ and the
angle $\vartheta$ between two consecutive reflection points.

From the figure we determine $\vartheta$, depending on the incident angle
$\alpha$, to be

$\vartheta=\pi-2\alpha.$ (1)

The natural question of this problem is for which values of $\vartheta$
closed, i.e. periodic, orbits exist. This means how do we need to choose the
value of $\vartheta$ such that after a given number of collisions $n$ the
billiard ball returns to its initial position $P_{0}$. Obviously, due to
rotational symmetry this case applies if

$\displaystyle q\cdot\vartheta$ $\displaystyle=2\pi\cdot p$ (2)
$\displaystyle\leftrightarrow\vartheta$ $\displaystyle=\frac{p}{q}\cdot 2\pi,$
(3)

where $q,p\in\mathbb{N}$ such that $gcd(p,q)=1$ and
$\frac{p}{q}<\frac{1}{2}$111The cases $p/q>1/2$ simply correspond to a
billiard ball moving in the opposite direction, i.e. clockwise. Since this
gives no new insights to the systems behavior we restrict to the cases smaller
or equal $1/2$.. The result tells us that if $\vartheta$ is a rational
multiple of $2\pi$ we always end up with periodic orbits [6]. $q$ determines
the number of periods that the circle is surrounded before returning to
$P_{0}$.

The trajectory forms in general regular star shaped figures consisting of $q$
corners equally distributed along $\partial{\cal C}$222If $p=1$ the trajectory
describes regular polygons. Star shaped figures arise for $p\geq 2$.. Two
consecutive star corners $P_{i}$ and $P_{i+1}$ ($i\in\\{0;1;\dots;q-1\\}$)
lying on $\partial\cal C$ form an angle of $\vartheta/p$ with the circle (see
figure 2). Thus the parameter $p$ tells us that from one scattering point to
the next $p-1$ corner points lie in between. If $n$ is the number of
scattering then the billiard trajectory follows the path formed by the star
corners

$P_{i}=P_{p\cdot n~{}\mbox{\small mod}~{}q},$ (4)

where in polar coordinates (circle radius $R$) the positions of $P_{i}$ are
given by

$P_{i}\left(R\cos\left(\frac{\vartheta}{p}\cdot i\cdot
2\pi\right),R\sin\left(\frac{\vartheta}{p}\cdot i\cdot 2\pi\right)\right).$
(5)

$P_{0}$$P_{1}$$P_{2}$$P_{3}$$P_{4}$$\vartheta/p$$(p-1)$ star corners between
Figure 2: Example for a $5-$star formed by the trajectory corresponding to
$\vartheta=\frac{2}{5}\cdot 2\pi$.

In the following sections we are interested in deriving a general formula for
the number of regions the circle is divided by the billiard trajectory after
each scattering $n$. Thereby, we continue as follows: In section 2 we are
going to show that any two billiard trajectories intersect only in a single
point, i.e. it doesn’t occur that three or more paths cross in a single point.
This is a rather technical side remark to the main results that we will
develop in section 3. In particular, we will derive a general formula for the
number of circle divisions after each scattering. The final section 4 will be
dealing with the special cases when

$\vartheta=\frac{p}{2p+1}\cdot 2\pi~{}~{}~{}~{}~{}p\in\mathbb{N}.$ (6)

In these cases the general formula of section 3 will be significantly
simplified containing the well known Gauß formula for the integer series

$\sum_{i=1}^{n}i=\frac{n\cdot(n+1)}{2}.$ (7)

##  2 Number of intersecting lines

######  Theorem 2.1.

In rational circular billiards there only intersect two lines formed by the
billiard trajectory in a single point.

###### Proof.

For the proof we consider the rotational angle $\vartheta=\frac{p}{q}\cdot
2\pi$, where $gcd(p,q)=1$ and $\frac{p}{q}<\frac{1}{2}$. The trajectory forms
a regular star shaped geometry with reflection points $P_{i}$ on the circle
are determined by the angle
$\Theta_{i}=i\cdot\frac{\vartheta}{p},~{}i\in\\{0;\dots;p-1\\}$, i.e.
$\Theta_{i}=\angle P_{0}MP_{i}$. We thus can consider the following setup of
possible intersecting lines (see figure 3) where without loss of generality
due to the rotational symmetry we can restrict to the case when the billiard
ball starts at the point $P_{0}$ characterized by $\Theta_{0}$.

$\Theta_{i}$$r_{i}$$\alpha$$S_{i}$$P_{i}$$P_{0}$$M$ Figure 3: Possible
intersecting trajectory lines.

The angle $\alpha$, i.e. the scattering angle with respect to the circle
normal, is given by $\displaystyle\alpha=\frac{\pi-\vartheta}{2}$. Making use
of the law of sines one obtains for the distance $r_{i}$ of the intersection
point $S_{i}$ with respect to the circle center $M$ (radius of the circle
$R$):

$r_{i}=R\cdot\frac{\sin(\alpha)}{\sin(\pi-\alpha-\frac{\Theta_{i}}{2})}=R\cdot\frac{\cos(\frac{p}{q}\pi)}{\cos(\frac{p}{q}\pi-\frac{i}{q}{\pi})}.$
(8)

Since holds

$0<\frac{p}{q}\pi-\frac{i}{q}{\pi}<\frac{\pi}{2}~{}~{}~{}\forall
i\in\\{0;\dots;p-1\\}$ (9)

the $\cos(\frac{p}{q}\pi-\frac{i}{q}{\pi})$ in the denominator is strictly
monotonic increasing. This implies that $r_{i}$ is strictly monotonic
decreasing resulting in the fact that there exist no intersection points
$S_{i}$ resulting from intersecting more than two trajectory lines. ∎

As a direct consequence of the proof it results that the intersection points
of the trajectories (intersections along $\partial\cal C$ not counted) again
lie on $p-1$ different circles of radii $r_{i}$ (see figur 4).

${\cal C}_{0}$${\cal C}_{1}$

Figure 4: left: Star shaped formed by billiards with
$\vartheta=\frac{3}{7}\cdot 2\pi$. right: Intersection points of the
trajectories aligned on circles of radii $r_{i}$.

Interestingly, each subregion ${\cal C}_{i}$ made by smaller circles of radii
$r_{i}$ again give rise to valid periodic orbits where the angle $\vartheta$
with respect to ${\cal C}_{i}$ changes according to

$\vartheta\rightarrow\vartheta_{i}=\frac{p-i}{q}2\pi~{}~{}~{}~{}~{}~{}i\in\\{0;\dots;p-1\\}.$
(10)

See, for example, the blue circle in figure 4 corresponding in the example to
${\cal C}_{1}$.

As a direct consequence of the above shown result for the radii $r_{i}$ we see
that when the ball returns to its initial point $P_{0}$ the circle has been
divided into $p\cdot q+1$ regions.

###### Proof.

Let $\partial{\cal C}_{i}$ be the circle of radius $r_{i}$ with
$i\in\\{0;\dots,p-1\\}$. For $i=p-1$, i.e. the smallest circle, $\partial{\cal
C}_{p-1}$ is the boundary for a regular polygon of $q$ corners, i.e. enclosing
one region. Each additional circle $\partial{\cal C}_{i}$ for $0<i<p-2$ is the
boundary of a star shaped figure adding $q$ additional regions (see the yellow
regions in figure 5 for $\partial{\cal C}_{p-2}$) for each circle except for
$i=0$ where we have the $q$ regions formed by the star’s corners and $q$
regions from the outer circle $\partial{\cal C}_{0}$ with the next inner
circle $\partial{\cal C}_{1}$ (see green and blue regions in figure 5). Thus
the total number of regions $f_{total}$ is given by

$f_{total}=1+\left(\sum_{i=1}^{p-2}q\right)+2q=pq+1.$ (11)

Figure 5: Graphical representation of enclosed regions by each circle.

∎

Equation (11) is in agreement with Euler’s formula [1] for planar graphs

$f=1+e-v$ (12)

where we excluded the region outside of the circle (thus number 1 instead of
2), $f$ is the number of faces, $e$ the number of edges and $v$ the number of
vertices, i.e. in our case all line intersections including the reflection
points in the circle. In our setup, i.e. when the billiard ball has performed
a whole periodic orbit, it holds

$\displaystyle e$ $\displaystyle=2pq,$ (13) $\displaystyle v$
$\displaystyle=pq,$ (14)

and thus

$f=f_{total}=2pq-pq+1=pq+1.$ (15)

##  3 General formula for circle division sequence

In this section we derive a general formula for the division of the circle in
regions by the rational billiard trajectory with $\vartheta=\frac{p}{q}\cdot
2\pi$. It turns out that it is useful to rewrite $q$ in terms of $p$ as

$q=mp+r,$ (16)

with $m=\lfloor\frac{q}{p}\rfloor\in\mathbb{N}$ and the rest term
$r\in\\{1;2;\dots;p-1\\}$. With this definition we can now turn to the circle
division starting with the circular region ${\cal C}$ and a billiard ball
starting from the initial positions $P_{0}$. The initial number of divided
regions such is $f_{0}=1$. For each consecutive scattering $i\geq 1$ the
circle is divided in one additional region as long as no whole circle
surrounding is performed, i.e. the maximum number for $i_{max}$ reflections is
given by

$\displaystyle i_{max,1}\cdot\vartheta$ $\displaystyle<2\pi$ (17)
$\displaystyle\leftrightarrow i_{max,1}$
$\displaystyle<\frac{2\pi}{\vartheta}=\frac{q}{p}=\frac{mp+r}{p}=m+\frac{r}{p}$
(18) $\displaystyle\rightarrow i_{max,1}$
$\displaystyle=m+\lfloor\frac{r}{p}\rfloor.$ (19)

If $n$ is the number of straight paths of the billiard ball trajectory we thus
have for the circle division of the first $m$ reflections

$f_{m}=\sum_{n=0}^{m+\lfloor\frac{r}{p}\rfloor}1.$ (20)

Note that since $r<p$ the term $\lfloor\frac{r}{p}\rfloor$ may be omitted.
Nevertheless $\lfloor\frac{r}{p}\rfloor$ will appear in the following terms
again and will play a crucial role for the general formula, thus we keep it at
this point in the sum. The sequence of circle division regions $f_{n}$
generated by the trajectory for the first $m$ scatterings thus is given by
(see for a graphical representation figure 6 left)

$f_{n}:1\underbrace{\xrightarrow{+1}2\xrightarrow{+1}3\xrightarrow{+1}\dots\xrightarrow{+1}}_{m-times}m+1.$
(21)

Figure 6: left: First $m$ divisions for $\vartheta=\frac{3}{4\cdot 3+2}\cdot
2\pi$. middle: first performance of a rotation greater than $2\pi$ right:
following $m-1+\lfloor\frac{2r}{p}\rfloor-\lfloor\frac{r}{p}\rfloor$ divisions
for $2\pi<n\cdot\vartheta<4\pi$

In the next step the trajectory is going to cross the initial point $P_{0}$
for the first time and thus will cross the line generated by the first path
(see figure 6 middle). As a direct consequence for the path with $n=m+1$ the
circle is divided into two additional regions since one line is crossed. The
number of divisions for the first $m+1$ steps thus reads

$f_{m+1}=\left(\sum_{n=0}^{m+\lfloor\frac{r}{p}\rfloor}1\right)+2,$ (22)

resulting in the sequence

$f_{n}:1\underbrace{\xrightarrow{+1}2\xrightarrow{+1}3\xrightarrow{+1}\dots\xrightarrow{+1}}_{m-times}m+1\xrightarrow{+2}m+3.$
(23)

Having performed the first $m+1$ steps the following paths (see figure 6
right) will always cross two lines since two consecutive scattering points
will always inhabit one scattering point from the first $m$ paths. From
crossing two lines one will generate three new regions each time. The number
of reflections $i_{max,2}$ in this situation that can be performed in this way
can be determined by the knowledge of the rotation angle performed in the
first $(m+1)$ reflections, which then crossed the initial point $P_{0}$ once
and the restriction, that the point $P_{0}$ isn’t crossed twice, i.e.

$\displaystyle
i_{max,2}\cdot\vartheta+(m+1+\lfloor\frac{r}{p}\rfloor)\cdot\vartheta$
$\displaystyle<4\pi$ (24) $\displaystyle\leftrightarrow i_{max,2}$
$\displaystyle<\frac{4\pi}{\vartheta}-m-1-\lfloor\frac{r}{p}\rfloor=m-1-\lfloor\frac{r}{p}\rfloor+\frac{2r}{p}$
(25) $\displaystyle\rightarrow i_{max,2}$
$\displaystyle=m-1+\lfloor\frac{2r}{p}\rfloor-\lfloor\frac{r}{p}\rfloor.$ (26)

For the total number of regions thus produced in the first
$2m+\lfloor\frac{2r}{p}\rfloor$ thus follows

$f_{2m+\lfloor\frac{2r}{p}\rfloor}=\left(\sum_{n=0}^{m+\lfloor\frac{r}{p}\rfloor}1\right)+2+\left(\sum_{n=m+2+\lfloor\frac{r}{p}\rfloor}^{2m+\lfloor\frac{2r}{p}\rfloor}3\right)$
(27)

and for the related region sequence

$f_{n}:1\underbrace{\xrightarrow{+1}2\xrightarrow{+1}3\xrightarrow{+1}\dots\xrightarrow{+1}}_{m-times}m+1\xrightarrow{+2}m+3\underbrace{\xrightarrow{+3}m+6\xrightarrow{+3}\dots\xrightarrow{+3}}_{m-1+\lfloor\frac{2r}{p}\rfloor-\lfloor\frac{r}{p}\rfloor~{}times}m+3+3\cdot\left(m-1+\lfloor\frac{2r}{p}\rfloor\right).$
(28)

We can extend this logic to a full periodic orbit. Each time when the
trajectory crosses the initial point $P_{0}$ we obtain an even number of new
regions since an odd number of lines is crossed. For the paths in between an
even number of lines is crossed resulting in generating an odd number of new
regions each. This pattern continues until the last round. The general formula
for the number of regions thus is given by

$f_{total}=1+\left(\sum_{n=1}^{m+\lfloor\frac{r}{p}\rfloor}1\right)+2+\left(\sum_{n=m+2+\lfloor\frac{r}{p}\rfloor}^{2m+\lfloor\frac{2r}{p}\rfloor}3\right)+4+\left(\sum_{n=2m+2+\lfloor\frac{2r}{p}\rfloor}^{3m+\lfloor\frac{3r}{p}\rfloor}5\right)+\dots$

$\dots+\left(\sum_{n=(p-1)m+2+\lfloor\frac{(p-1)r}{p}\rfloor}^{pm+r+1}2p-1\right)$
(29)

with the associated division sequence

$f_{n}:1\underbrace{\xrightarrow{+1}\dots\xrightarrow{+1}}_{m~{}times}m+1\xrightarrow{+2}m+3\underbrace{\xrightarrow{+3}\dots\xrightarrow{+3}}_{m-1+\lfloor\frac{2r}{p}\rfloor-\lfloor\frac{r}{p}\rfloor~{}times}m+3+3\cdot\left(m-1+\lfloor\frac{2r}{p}\rfloor-\lfloor\frac{r}{p}\rfloor\right)\xrightarrow{+4}\dots$

$\dots\underbrace{\xrightarrow{+2p-1}\dots\xrightarrow{+2p-1}}_{m-1+\lfloor\frac{pr}{p}\rfloor-\lfloor\frac{(p-1)r}{p}\rfloor~{}times}p\cdot(mp+r)+1=pq+1.$
(30)

Note that the last sum in (29) runs to $pm+r+1$ instead of $pm+r$, i.e. there
is one additional summand $2p-1$ resulting from the fact that the very last
path ends exactly on the initial point $P_{0}$ and thus it crosses the same
number of lines as the paths before.

As a small remark concerning the floor function holds $\lfloor\frac{k\cdot
r}{p}\rfloor\in\\{0;\dots;r-1\\}~{}\forall k\in\\{1;\dots;p-1\\}$.

An interesting simplification takes place when for the rest term holds $r=1$.
In these cases the sequence of the number of regions is simplified by the fact
that

$\lfloor\frac{k}{p}\rfloor=0~{}\forall k\in\\{1;\dots;p-1\\}.$ (31)

The simplified version of (29) thus reads

$f_{total}(r=1)=1+\left(\sum_{n=1}^{m}1\right)+2+\left(\sum_{n=m+2}^{2m}3\right)+\dots+\left(\sum_{n=(p-1)m+2}^{pm+2}2p-1\right)$
(32)

resulting in an integer sequence of alternating $(m-1)$ summations except the
first $m$ and last $m$ reflections

$f_{n}:1\underbrace{\xrightarrow{+1}\dots\xrightarrow{+1}}_{m~{}times}m+1\xrightarrow{+2}m+3\underbrace{\xrightarrow{+3}\dots\xrightarrow{+3}}_{(m-1)~{}times}4m\xrightarrow{+4}4m+4\underbrace{\xrightarrow{+5}\dots\xrightarrow{+5}}_{(m-1)~{}times}\dots\underbrace{\xrightarrow{+2p-1}\dots\xrightarrow{+2p-1}}_{m~{}times}pq+1.$
(33)

To illustrate the last formula one should consider the example
$\vartheta=\frac{3}{13}\cdot 2\pi$, i.e. $(p,m,r)=(3,4,1)$ shown in figure 7.
The sequence for the regions reads

$f_{n}:1\underbrace{\rightarrow 2\rightarrow 3\rightarrow
4\rightarrow}_{4~{}times~{}+1}5\rightarrow 7\underbrace{\rightarrow
10\rightarrow 13\rightarrow}_{3~{}times~{}+3}16\rightarrow
20\underbrace{\rightarrow 25\rightarrow 30\rightarrow
35\rightarrow}_{4~{}times~{}+5}40.$ (34)

$f_{1}=2$

$f_{2}=3$

$f_{3}=4$

$f_{4}=5$

$f_{5}=7$

$f_{6}=10$

$f_{7}=13$

$f_{8}=16$

$f_{9}=20$

$f_{10}=25$

$f_{11}=30$

$f_{12}=35$

$f_{13}=40$

Figure 7: Graphical representation for the division sequence in the case
$\vartheta=\frac{3}{13}\cdot 2\pi$.

##  4 Discussion of the special case $\vartheta=\frac{p}{2p+1}\cdot 2\pi$

Considering the case $(m,r)=(2,1)$ corresponding to angles
$\vartheta=\frac{p}{2p+1}\cdot 2\pi$ formula (29) for the number of regions
$f_{n}$ significantly simplifies to

$f_{n}=1+1+1+2+3+4+\dots+2p-2+2p-1+2p-1,$ (35)

If $n$ is the number of performed scatterings assuming we start with $0\leq
n\leq 2p+1$ the above sequence can be rewritten in terms of a formula for
$f_{n}$ depending on $n$ as

$\boxed{f_{n}=2-\delta_{n,0}+\sum_{i=1}^{n-1}i-\delta_{2p+1,n}=2-1\cdot(\delta_{n,0}+\delta_{n,2p+1})+\frac{n\cdot(n-1)}{2}}$
(36)

This formula tells us that despite of the first scattering ($n=1$) and the
last scattering ($n=2p+1$) the number of circle divisions performed by the
billiard ball trajectory is related to integer sequence of arithmetic series

$f_{n+1}=f_{n}+(n-1)$ (37)

which starts with $f_{0}=1$ and $f=1=2$. Further $\delta_{i,j}$ represents the
Kronecker-Delta defined by

$\delta_{i,j}=\begin{cases}1&if~{}i=j\\\ 0&otherwise\end{cases}$ (38)

Formula (36) states our main (applicable) result of this paper and extends the
already known examples of circle divisions either by lines [8, 7] or by chords
[4, 2, 5].

In particular, if $n=2p+1$ scatterings are performed, we again obtain the
total number of regions that the circle has been divided in by the periodic
trajectory

$f_{total}=f_{2p+1}=2-1+\frac{(2p+1)\cdot(2p+1-1)}{2}=pq+1,$ (39)

where again $2p+1$ was defined as $q$ and thus matching with equation (11).

As an example the sequence for the number of regions for circle divisions of
the example in figure 8 is given by

$f_{n}:1\xrightarrow{+1}2\xrightarrow{+1}3\xrightarrow{+2}5\xrightarrow{+3}8\xrightarrow{+4}12\xrightarrow{+5}17\xrightarrow{+6-1}22$
(40)

$f_{0}=1$

$f_{1}=2$

$f_{2}=3$

$f_{3}=5$

$f_{4}=8$

$f_{5}=12$

$f_{6}=17$

$f_{7}=22$

Figure 8: Billiard paths and number of circle divisions for
$\vartheta=\frac{3}{7}\cdot 2\pi$.

It is remarkable that the integer sequence

$\sum_{i}i,$ (41)

which is known in many different areas of pure mathematics and physics also
appears in the circle divisions of billiard trajectories for each angle
$\vartheta=\frac{p}{2p+1}\cdot 2\pi,~{}p\in\mathbb{N}$, now.

##  5 Conclusion and Outlook

In this paper we have provided a general formula for the region division
sequence of a rational billiard path inside a circle. By this we have analyzed
another examples of circle divisions besides the already known cases of
divisions produced by chords or by lines. We have presented a simple formula
for the number of regions following after each scattering $n$ for certain
angles $\vartheta=\frac{p}{2p+1}\cdot 2\pi$, $p\in\mathbb{N}$. In particular,
this formula containes a arithmetic series.

For future works it will be interesting to see if similar sequences arise from
elliptical, triangular or general polygonal domains.

## References

  * [1] L. W. Berman & G. I. Williams, Exploring Polyhedra and Discovering Euler’s Formula, Resources for Teaching Discrete Mathematics, Mathematical Association of America, 2009.
  * [2] J. H. Conway & R. K. Guy, How Many Regions - The Book of Numbers, New York: Springer-Verlag, pp. 76-79, 1996.
  * [3] H. Masur & S. Tabachnikov, Rational billiards and flat structures, Handbook of Dynamical Systems, Volume 1, Part A, Pages 1015-1089, 2002.
  * [4] M. Noy, A Short Solution of a Problem in Combinatorial Geometry, Math. Mag. 69, 52-53, 1996.
  * [5] C. Rodriguez-Lucaterc, The Moser’s formula for the division of the circle by chords problem revisited, arXiv:1701.08155 [math.CO]
  * [6] U. A. Rozikov, An Introduction to Mathematical Billiards, World Scientific Publishing Co. Pte. Ltd. (2019).
  * [7] D. Wells, The Penguin Dictionary of Curious and Interesting Numbers, Middlesex, England: Penguin Books, p. 31, 1986.
  * [8] A. M. Yaglom & I. M. Yaglom, Challenging Mathematical Problems with Elementary Solutions, Vol. 1. New York: Dover, pp. 102-106, 1987.

A special thanks to Jan Bickel for a useful discussion.