  This paper studies a formalisation of intuitionistic logic by Negri and von
Plato which has general introduction and elimination rules. The philosophical
importance of the system is expounded. Definitions of `maximal formula',
`segment' and `maximal segment' suitable to the system are formulated and
corresponding reduction procedures for maximal formulas and permutative
reduction procedures for maximal segments given. Alternatives to the main
method used are also considered. It is shown that deductions in the system
convert into normal form and that deductions in normal form have the subformula
property.
