Gentzen's rules provide a complete system that does not require the cut rule. For many logical systems, cut elimination (showing that uses of the cut rule may be eliminated from any sound proof) is a major theorem. For us it is a simple consequence of the reduction procedure.