 The normal form result holds for classical propositional logic (CPL) in the connectives \(\osim\), \(\wedge\), \(\vee\), and \(\rightarrow\). As Humberstone points out, it fails for the negation, conjunction, disjunction fragment of CPL, since in classical propositional logic the Bendall normal form (bnf) of a conjunction of atomic formulas \((p \wedge \osim q)\) is \(\osim (p \rightarrow q)\). Moreover, the translation of \((\osim p \rightarrow q)\) into bnf is \((p \vee q)\), and the translation of \(\osim \osim p\) is \(p\). These pairs of formulas are not logically equivalent in intuitionistic propositional logic (IPL). The translation of \((\osim p \rightarrow \osim q)\) into bnf is \((q \rightarrow p)\), which is not logically equivalent to \((\osim p \rightarrow \osim q)\) in N3 and N4. An in-depth investigation of sequent calculi using formulas prefixed by an assertion sign [+] or a rejection sign [–], understood as non-embeddable force indicators, can be found in Bendall 1978, Humberstone 2000a.