 For the normalization result of von Plato and Siders, we will choose, as our classicizing rule, the principle of Indirect Proof: a formula, \(A\), may be asserted after a subproof, with hypothesis \(\neg A\), having a pair of contradictory formulas, \(B\) and \(\neg B\), as items. The possibility of normalization then depends on our being able to modify derivations to eliminate cases where a formula, \(C\), is obtained by Indirect Proof and is then used as the (major) premiss of an elimination rule to obtain another formula, \(D\): we might call manoeuvres like this in a derivation “classicizing detours”. This is illustrated in  figure 8.