 As noted in Dunn 1993, 1996, if contraposition is assumed, double negation introduction \(A \vdash \osim \osim A\) is mutually derivable with constructive contraposition \(A \vdash \osim B \slashrel B \vdash \osim A\), and if constructive contraposition is assumed, double negation elimination is mutually derivable with classical contraposition \(\osim A \vdash B \slashrel \osim B \vdash A\). Note also that in the presence of double negation introduction and elimination, one can derive \(\osim A \vdash \osim B \, / \, B \vdash A\). The demonstrations use only reflexivity and transitivity of the derivability relation \(\vdash\). As a result, the above list of negation laws leads to the following unbalanced “kite” of negations (cf. Dunn and Zhou 2005):