2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/230662We prove the strong normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system.Submitted to APALLogicLogic in Computer Sciencetext