Strong normalization proofs for cut elimination in Gentzen's sequent calculi
Elias Bittar · Banach Center Publications · 1999
We define an equivalent variant $LK_{sp}$ of the Gentzen sequent calculus $LK$. In $LK_{sp}$ weakenings or contractions can be performed in parallel. This modification allows us to interpret a symmetrical system of mix elimination rules $