
## Γ2 = Γ ∪ {Y : **B, Y** : ¬X¬A}.

where y ∈ LabΓ . As Γ is satisable in M under f , we have that f(x) ∈
(A ⇔ B)M . By 
laim 1, for all y ∈ LabΓ we have f(y) ∈ (¬¬A)M (as AM

annot be empty) and f(y) ∈ (B → ¬x¬A)M . We then have two 
ases:
- either f(y) ∈ (¬B)M , and then Γ1 is satisable.

- or f(y) ∈ BM and then f(y) ∈ (¬x¬A)M . Γ2 is then satisable.

 (F1 ⇔). Let x : ¬(A ⇔ B) ∈ Γ . The rule will generate three tableau sets:
Γ1 = Γ ∪ {x : ¬A}

## Γ2 = Γ ∪ {X : B}

Γ3 = Γ ∪ {x : ¬**A, x** : ¬B}
As Γ is satisable in M under f , we have f(x) ∈ ¬(A ⇔ B)M . By 
laim 1, we have that f(x) ∈ (¬A)M or ∃y(y ∈ BM and y ∈ (x¬A)M).

If f(x) ∈ (¬A)M , then Γ1 is satisable. If not, we have two 
ases:
- either f(x) ∈ BM , and thus Γ2 is satisable.

- either f(x) ∈ (¬B)M , and then there is some ob je
t y
′ ∈ ∆ su
h that y
′ ∈ BM and y
′ ∈ (x¬A)M , so that y
′ 6= f(x). Sin
e the relation ≺x satises the 
entering property, we have x ≺x y
′
. And from y
′ ∈ (x¬A)M , we 
an dedu
e that f(x) ∈ (¬A)M , thus making Γ3 satisable.

 (F2 ⇔). This rule will generate the following set:

## Γ1 = Γ ∪ {Y : X¬**A, Y** : B}

```
  where y /∈ LabΓ . As shown in the proof for (F1 ⇔), sin
e x : ¬(A ⇔ B), x :
  ¬A, x : ¬B belong to Γ and Γ satisable in M by f , we have that there
  exists some y
             ′ ∈ ∆ su
h that y
  ′ ∈ (B ⊓ x¬A)M . We 
onstru
t a CSLmapping f
           ′ by taking ∀u 6= y, f
                              ′(u) = f(u); and f
                                              ′(y) = y
                                                     ′
                                                     . It's then easy
                                                                  
  to show that f
              ′
               is a CSL-mapping, and that Γ1 is satisable in M under f
                                                                 ′
                                                                  .
                                                                  
 (F2x). Let z : ¬x¬A, x : ¬A. This rule will generate the following tableau
  set:
     
                   Γ1 = Γ ∪ {y <x z, y : A, y : x¬A}.

```

where y /∈ LabΓ . Sin
e Γ is satisable in M under f , we have that f(z) ∈
(¬x¬A)M . Therefore we have that ∃y
′ ∈ ∆ su
h that y
′ ∈ AM and y
′ ≺x f(z). We then let y
′′ ∈ min
≺x

{y
′| y
′ ∈ ∆ ∧ y
′ ∈ AM ∧ y
′ ≺x f(z)}.

As ≺x satises the limit assumption, y
′′ exists, and it's easy to see that y
′′ ∈ (x¬A)M (if not it would not be minimal). As y /∈ LabΓ , we dene

```
a new CSL-mapping f
                    ′ by taking ∀u 6= y, f′(u) = f(u), and f(y) = y
                                                                ′′
                                                                 .
                                                                 

It's then easy to 
                       he
                           k that f
                                      ′
                                        is indeed a CSL-mapping, and that Γ1 is

```

satisable in M under f
′
.