Theorem 26. Let Γ be obtained from {x : A}, where A is a CSL-formula, by applying an arbitrary sequen e of rules respe ting denition 25. Then Γ is nite.

Proof. Suppose by absurdity that Γ is not nite. Sin
e the stati rules (and also the (F) rule) may only add a nite of number of formulas for ea
h label, Γ

```
must 
     ontain an innite number of labels generated by the dynami
                                                       rules, either
                                                                

```

(F2⇔) or (F2) (or both).

Let Γ 
ontain innitely many labels introdu
ed by (F2⇔). Sin
e the number of negative ⇔ formulas is nite, there must be one formula, say ¬(B ⇔
C), su
h that for an innite sequen
e of labels x1, . . . , xi**, . . .**, xi: ¬(B ⇔
C) ∈ Γ . By blo
king 
ondition (2b) we then have that for every i, ΠΓ (xi) 6⊆
ΠΓ (x1)**, . . . , Π**Γ (xi) 6⊆ ΠΓ (xi−1). But this is impossible sin
e ea
h ΠΓ (xi) is nite (namely bounded by O(|A|)) and the rules are non-de
reasing wrt. ΠΓ (xi)
(an appli ation of a rule an never remove formulas from ΠΓ (xi)).

Let now Γ 
ontain innitely many labels introdu
ed by (F2). That is to say, Γ 
ontains xi: ¬yi¬B for innitely many xi and yi
. If all yi are distin
t, Γ must 
ontain in parti
ular innitely many formulas x : ¬yi for a xed x.

The reason is that xi: ¬yi¬B may only be introdu
ed by applying (T⇔), thus there must be innitely many yi: B ⇔ C ∈ Γ . By the systemati pro
edure, the rule (T ⇔) has been applied to a label x for every yi: B ⇔ C ∈ Γ generating x : ¬yi¬B for all yi
. But then we an nd a ontradi tion with respe t to blo king ondition (3b) as in the previous ase, sin e for ea h i we would have ΠΓ (yi) 6⊆ ΠΓ (y1)**, . . . , Π**Γ (yi) 6⊆ ΠΓ (yi−1) . We 
an 
on
lude that Γ 
annot ontain xi: ¬yi¬B , for innitely many distin
t yi and distin
t xi
. We are left with the ase Γ 
ontains xi: ¬y¬B for a xed y and innitely many xi
.

In this ase, by blo king ondition (3
), we have that for ea h i, Box+
Γ,y,xi 6⊆
Box+
Γ,y,x1

, . . . , Box+
Γ,y,xi 6⊆ Box+
Γ,xi−1

. But again this is impossible given the fa t that ea h Box+
Γ,y,xi is nite (bounded by O(|A|)) and that the rules are nonde reasing wrt. the sets Box+
Γ
.

To prove ompleteness, we will onsider tableau sets saturated under blo king. A tableau set Γ is saturated under blo
king i (a) it is build a

ording to Denition 25 (b) No further rules an be applied to it. It is easy to see that if Γ

```
is saturated under blo
                             king, it satises all the saturation 
                                                                          onditions in Denition
                                                                                                       

```

22 ex ept possibly for onditions (F ⇔).(iii) and (Fx).(ii).

By the termination theorem, we get that any tableau set generated from an initial set ontaining just a CSL formula, will be either 
losed or saturated under blo king in a nite number of steps.

```
We now show that an open tableau set saturated under blo
                                        king 
                                            an be
                                               

```

extended to an open saturated tableau set, that is satisfying all onditions of denition 22. By means of theorem 21 we obtain the ompleteness of the terminating pro edure.

Theorem 27. If Γ is saturated and open under blo
king, then there exists an open and saturated set Γ
∗
su h that for al l A ∈ LCSL , if x : A ∈ Γ then A ∈ Γ
∗
.