The proposed algorithms for eliminating cuts in the provability calculus GLS do not terminate

A completeness theorem for a cutfree fragment of the calculus exists in
Sambin 1982, but syntactic manipulations on proofs containing
cuts have not been fully understood. We say that a proof pi is
in Sambin Normal Form (SNF) if and only if the last inference rule in
pi is the cut-rule, and the last inference-rule applied in each
subtree is the GLR rule. A positive result is presented; a normal
form theorem, saying that every proof pi in GLS can be rewritten
to a proof pi* where every occurence of a cut is in SNF.
In this paper we prove, using our Normal Form Theorem, that the
proposed algorithms for eliminating cuts in propositional provability
sequential calculi, as presented Leivant 1981 and
Valentini 1983, do not terminate. A small proof, named epsilon, shall
do the job, proving that both algorithms diverge.

We do this by introducing concepts for reasoning about
concrete proofs where concrete regions in the proofs are translated to
regular expressions. The regular expressions and the grammar describing
the reduction sequences derived from epsilon, gives the
appropriate language for describing non-termination in proof theory.