 More precisely, let \(\cL_{\left\{ \Box_{1} \right\}}\) and \(\cL_{\left\{ \Box_{2} \right\}}\) be the languages of the system to be combined, and let \(\cM_1\) and \(\cM_2\) be their correspondent classes of models. Let \(h_1\) be a transfer mapping, taking a world of any model in \(\cM_1\), and returning a pair consisting of a model \(M_2\) in \(\cM_2\) and a world \(w_2\) in \(M_2\); let \(h_2\) be a transfer mapping in the other direction, taking a world of any model in \(\cM_2\), and returning a pair consisting of a model \(M_1\) in \(\cM_1\) and a world \(w_1\) in \(M_1\). Formulas of the language \(\cL_{\left\{ \Box_{1}, \Box_{2} \right\}}\) can be evaluated in either tuples of the form \(\langle h_1, h_2, M_1, w_1 \rangle\) (with \(w_1\) in \(M_1 = \langle W_1, R_1, V_1 \rangle\) and \(M_1\) in \(\cM_1)\) or else tuples of the form \(\langle h_1, h_2, M_2, w_2 \rangle\) (with \(w_2\) in \(M_2 = \langle W_2, R_2, V_2 \rangle\) and \(M_2\) in \(\cM_2)\). In the first case, the semantic interpretation of Boolean operators is as usual; for the modality \(\Box_{1}\),