 The theorems described, depending as they do on the order of application of the reductions, are sometimes called weak normalization theorems. There are also strong normalization theorems, to the effect that any derivation can be converted into one in normal form by application of the reductions in arbitrary order (Prawitz 1971). Their proof is necessarily less elementary. The theorems, and the methods used in their proof, are analogous to what is called “normalizability” theorems in the context of the lambda-calculus (detailed discussions can be found in, e.g., Troelstra &amp; Schwichtenberg 1996). There are also weaker theorems, called normal form theorems, stating that for any derivation there is a derivation in normal form of the same conclusion from the same premises, without saying anything about a procedure for converting a non-normal derivation into a normal one. Such theorems can be proven, e.g., semantically, by proving the completeness of a system restricted to normal derivations.