Eliminating deficiencies: the complete picture.

We now prove by induction on the number of possible deficiencies that every deficiency in x w.r.t. y can be eliminated in an adequate way. (For the time being we only consider the harder case when intermediate worlds do exist.) Adequate means that all the S_xsuccessors of y that are defined for this purpose contain all the $\Box$-formulas of x' ( xR_e^Bx'Ry). The new worlds should not provoke new deficiencies in x. And all of them should lie B-critically above x.

• If you only have $E_0 \rhd F_0$ as possible deficiency in x and this is indeed a deficiency, i.e. $E_0 \in y$, you can apply lemma 5.4. This yields a y' such that $F_0 \in y'$, $x \prec_{\mbox{\footnotesize {B}}} y' \mbox{ and } x' \subset_{\Box} y'$. This y is taken to be maximal w.r.t. the $\Box$-inclusion. You can thus safely define yS_xy' and no new deficiencies will emerge in x w.r.t. y, for they have to be amongst the possible deficiencies. The model is closed under the frame conditions.

• If the possible deficiencies are $E_0 \rhd F_0 , \ldots , E_n \rhd F_n$, one can make use of lemma 5.5 to derive n! useful sentences. Also the corresponding set $\mathcal{D}$ is formed by the same method as before. Let again $F_{i_1}, \ldots , F_{i_k}$ be all the F's that do not occur as such in $\mathcal{D}$. Lemma 5.6 guarantees the existence of a subset $\mathcal{D'}$which has, for every F_j that occurs in $\mathcal{D}$, one disjunct that contains both F_j and $\neg E_{i_1}, \ldots , \neg E_{i_k}$. For every disjunct in $\mathcal{D'}$ a corresponding world can be found where that very disjunct holds. This world will also lie B-critically above x.
  But one does not meet all the requirements like this. For the worlds only contain a finite part of the box formulas in x', namely the $\Box C$ that was included in all the n! formulas. This calls for compactness again. Let $\Box C_1 , \Box C_2 , \Box C_3 , \ldots$ be an enumeration of all the box formulas in x'. Let $\Box X_i := \Box \bigwedge \hspace{-2.5mm} \bigwedge_{j=1}^i C_j$. For every $\Box X_i$ a set $\mathcal{D'}$ as above is formed. As only a finite number of partitions is possible for $\mathcal{D'}$, one specific partition must show up infinitely many times. With respect to every individual world of this (or better corresponding to this) partition the compactness theorem can be applied to obtain a set of worlds. All of these worlds will contain some F_j, all of $\neg F_{i_1}, \ldots , \neg F_{i_k}$, and all the $\Box C \in x'$. They can also be taken maximal w.r.t. $\Box$-inclusion.  This set of worlds is called $\mathcal{D}_{x,x'}^y$. So $F_{i_1}, \ldots , F_{i_k}$ do not occur in $\mathcal{D}_{x,x'}^y$. For these remaining k possible deficiencies you can apply the induction hypothesis while ignoring the n-k+1 other possible deficiencies. Note that if k=n+1 the whole situation becomes very trivial. So, without loss of generality, we can assume that k < n+1. Applying the induction hypothesis yields a whole net of B-critical successors of x solving all the k deficiencies disregarding the other n-k+1 possible deficiencies. Every world in this net contains all the $\Box$-formulas of x'. All the individual members of this net are maximal w.r.t. $\Box$-inclusion. By ``attaching'' this B-critical net to y, k deficiencies are solved but some deficiencies among the other n-k+1 possible ones may ``have become active''. You eliminate these deficiencies by defining an S_x arrow from every world in the B-critical net to every world in $\mathcal{D}_{x,x'}^y$. S_x on $\mathcal{D}_{x,x'}^y$ is defined such that $\mathcal{D}_{x,x'}^y$ is completely S_x-connected. After having done so, no deficiency in x remains w.r.t. any of the newly defined worlds. If $E_i \rhd F_i$ belongs to the group of k it is, if necessary, eliminated in the B-critical net. If $E_i \rhd F_i$belongs to the group of n-k+1, there is always an S_x-arrow to a world in $\mathcal{D}_{x,x'}^y$ where F_i holds. In this world E_j cannot hold for any $E_j \rhd F_j$ from the group of k. So indeed all the deficiencies are eliminated. Moreover transitivity of the S_x relation is guaranteed. The process described here will be referred to as the process of making an S_x^y-block.

If there is a deficiency in x w.r.t. y and there is no intermediate world, the situation becomes even easier. Again the process of eliminating this deficiency in x w.r.t. y shall be referred to as the process of making an S_x^y-block. If in a general setting the process of making an S_x^y-block is mentioned, either one of these two is meant, depending on the presence of intermediate worlds. The process of making an S_x^y-block in the case of no intermediate worlds can inductively be described as follows.

• Let y be in the S_x^y-block.
• begin As long as deficiencies in x exist w.r.t. some world y in the S_x^y-block, apply lemma 5.2 to obtain y''such that y'' resolves this deficiency by setting y'S_xy'' and xRy''. As the whole S_x^y-block is in at most one B-critical cone of x, there is no ambiguity in applying lemma 5.2. Now make the whole S_x^y-block completely S_x-connected.
  end

As there is only a finite number of possible deficiencies, this process must come to an end.