Effective Cut-elimination for a Fragment of Modal mu-calculus

A non-effective cut-elimination proof for modal mu-calculus has been given by G. J?ger, M. Kretz and T. Studer. Later an effective proof has been given for a subsystem M ₁ with non-iterated fixpoints and positive endsequents. Using a new device we give an effective cut-elimination proof for M ₁ without restriction to positive sequents.