The main idea of this cumbersome formalization can be traced to the first papers by Kripke on semantic treatment of modal and intuitionistic logic. The completeness proof given there used proof search trees for an elegant formulation in terms of indexed tableaux \(\sigma_ 1 S_ 1; \sigma_ 2 S_ 2; \dots; \sigma_ n S_ n\), where \(S_ i\) are sequents \(\Gamma_ i\to \Delta_ i\) and indices \(\sigma_ i\) play the role of possible worlds. The author's system can be obtained from this schema (never mentioned in the paper) roughly by imposing the restriction that \(\sigma_ i\) are linearly ordered and at most one \(\Delta_ i\) can be non-empty (and then it is a singleton). In fact, a language of S4-like intuitionistic modal logic is used.