An instance of the cut rule is called analytic if the cut formula already appears as a subformula of the lower sequent. For example, the cut is analytic because the cut formula is contained in . Analytic cut can be seen as a deep inference rule. In classical and modal logic it corresponds to a…