 The proof­ system in Gargov and Goranko (1993) makes use of a complex rule (called COV) where the formula schema containing the active part of the rule can be arbitrarily large; in fact, the active part is embedded under arbitrarily deep nestings of modal operators. Blackburn and Tzakova (1999) shows that satisfaction operators can be used to formulate an axiom system in a more standard format, using a simpler rule called PASTE, such that the system is still complete when extended with pure axions. 