By structural induction on .
If , has subterm , which must be reduced to eliminate to obtain a canonical form. Moreover, there is only one atomic leaf. So
Suppose . Normalisation requires elimination of the root of . Since the third argument has head , only
will do so. Every derivation (minimum-length or otherwise) will have to apply that rule at some point. Without loss of generality, apply it at the beginning. Then
Note is terminal by definition of complex indirect constant -systems. So