(α) (X \ X ′) ∩ F¯ 6= ∅**, or** (β) (X \ X ′) ∩ G¯ 6= ∅**, or** (γ) (X \ X ′) ∩ H¯ 6= ∅.

If condition (α**) occurs, according to both the hypothesis and Definition 16**
(page 17), then there exist Pi, r , a s.t Pi ∈ SP, r ∈ S
′1(Pi), aPi ∈ (X \ X ′)∩ F¯ , and r **has the form** a
′
Pi ←not aPi**. Now, since** aPi ∈ (X \ X
′) ∩ F¯ **, it holds that** aPi ∈ X
and a
′
Pi 6∈ X (otherwise, according to r , X **would not be a model of** P
′u ∪ C¯ **). Now,**
since X ′ ⊆ X **, it holds that** a
′
Pi 6∈ X ′**. Therefore, there exists a social rule** r ∈ P
′u∪C¯
s.t. r is false w.r.t. X ′. As a consequence, X ′**is not a model of** P
′u ∪ C¯ **and we have**
reached a contradiction. This concludes the proof of case (b**), condition (**α).

In case (b), if condition (β**) holds, then according to both the hypothesis and**
Definition 16 (page 17), either:
(i) There exist Pi, r , a
′**s.t.** Pi ∈ SP, r ∈ S
′1(Pi), a
′
Pi
∈ (X \ X ′) ∩ G¯ and r has the form aPi ←not a
′
Pi
, or
(ii) There exist Pi, r , a **s.t.** Pi ∈ SP, r ∈ S
′
3
(Pi), aPi ∈ X¯ , saPi ∈ (X \ X ′) ∩ G¯
and r **has the form** failPi ←not failPi, aPi,not saPi.

If item (i) is true, then r **is false w.r.t.** X
′**, since** a
′
Pi 6∈ X
′ and aPi 6∈ X
′**. Thus,**
X
′**is not a model of** P
′u ∪ C¯ **and we have reached a contradiction.**
If item (ii) holds, then r is false w.r.t. X ′**, since, according to the hypothesis,**
saPi ∈ X . Therefore, aPi ∈ X . As a result, saPi 6∈ X ′ and aPi ∈ X ′**. Thus,** X ′is not a model of of P
′u ∪ C¯ **and we have reached a contradiction. This concludes the**
proof of case (b), condition (β). Now we give the proof when condition (γ**) holds.**
In case (b), if condition (γ) holds, then there exist Pi, h s.t. Pi ∈ SP and hPi ∈
(X \ X ′) ∩ H¯ . Since X ′**is a model of** P
′u ∪ C¯ **, according to Definitions 12 and 21**
(pages 15 and 22), there exists some aPiin F¯ ∪ G¯ s.t. aPi ∈ (X \ X ′**). Therefore,**
either condition (α) or condition (β) of case (b**) occurs and it is easy to see that** we have reached a contradiction. Now we have concluded the proof **of the theorem.**

## List Of Symbols And Abbreviations

[ ]P **Operator that produces a set of auxiliary atoms labelled w.r.t.**
P **and used in the translation process**
Γ
′**() The mapping from SOLP programs to traditional logic programs**
Pˆ A logic program obtained from P **after a rewriting of the tolerance rules occurring in it**
LPA **The non-disjunctive fragment of logic programming with aggregates supported by the DLV system**
SOS(P1, · · · ,Pn) The set of all social models of P1, **· · ·** ,Pn U(P1, · · · ,Pn**) The set of all the possible combinations of autonomous fixpoints**
of the SOLP programs P1, **· · ·** ,Pn OKAY (P**) The set of** okay **rules of the COLP program** P
ΨP (s) The translation of a single SC s of a SOLP program P