A new proof of normalization for NS4

In 1965 Dag Prawitz presented an extension of Gentzen-type systems of Natural Deduction to modal concepts, obtaining three new systems of Natural Deduction for S4. Maria da Paz Medeiros showed in 2006 that the proof of normalization for classical S4 does not hold and proposed a new proof of normalization for a logically equivalent system, the NS4. However, two problems in the proof of a lemma used by Medeiros in her proof were presented by Andou Yuuki in 2010. This paper introduces a new proof of normalization for NS4.