simple. Since s **is well-formed,** cond(s) = [l, h**]. Thus, according to Definition 13**
(page 16), there exists a set of rules S = {r1} ∪ {si| 1 ≤ i 6= j ≤ n} ⊆ (C¯ ∪ Q**) s.t.:**

r1 : ρ(s)Pj ← l ≤ #count{K : (g(s))(K)Pj, K 6= j } ≤ h
si : (g(s))(i)Pj ←Vb∈content(s)
bPi ∧Vs
′∈**skel**(s)
ρ(s
$$\stackrel{\mathrm{̃}}{\neq}j\}\leq h$$ $$(s^{\prime})_{\mathcal{P}_{j}}$$
)Pj(1 ≤ i 6= j ≤ n)
Moreover, for each r ∈ (C¯ ∪ Q) \ S **and for each** t ∈ S, head(r ) 6= head(t).

Now, observe that, since ρ(s)Pj ∈ M and M is a stable model of C¯ ∪Q**, according**
to the definition of aggregate functions (Dell'Armi et al. 2003), there exists a set
∆′ ⊆ {(g(s))(i)Pj| 1 ≤ i 6= j ≤ n} s.t. l ≤ |∆′| ≤ h and ∀x ∈ ∆′, x **is true w.r.t.**
M . Thus, there exists ∆′′ ⊆ S \ {r1} s.t. l ≤ |∆′′| = |∆′| = |∆| ≤ h **and s.t. for**
each si ∈ ∆′′, head(si) is true w.r.t. M . Since M is a stable model of C¯ ∪ Q**, for**
each si ∈ ∆′′, body(si) is true w.r.t. M . Now, note that for each i **s.t.** si ∈ ∆′′,
body(si) = Vb∈content(s)
bPi ∧Vs
′∈**skel**(s)
ρ(s
′)Pj.

Thus, for each i **s.t.** si ∈ ∆′′,Vb∈content(s)
bPiis true w.r.t. M and Vs
′∈**skel**(s)
ρ(s
′)Pj is true w.r.t. M .

Now, since ¯I ⊆ M and according to Definition 13 (page 16), for each i **s.t.**
si ∈ ∆′′,Vb∈content(s)
bPiis true w.r.t. ¯I. Since for each i s.t. si ∈ ∆′′, bPi**is a**
literal labelled w.r.t. Pi, it is easy to see that for each i s.t. si ∈ ∆′′ **and for each**
b ∈ content(s), b is true for Pi w.r.t. ¯I**. Moreover, by induction hypothesis, for**
each s
′ ∈ skel(s), s
′is true for Pj **w.r.t.** ¯I.

Thus, we have obtained that cond(s) = [l, h] and there exists a set D ⊆ {i | 1 ≤ i 6= j ≤ n} s.t. l ≤ |D| ≤ h and for each i ∈ D s.t. Pi ∈ SP **and for each**
a ∈ content(s), it holds that a is true w.r.t. P **and for each** s
′ ∈ skel(s), s
′**is true**
for Pj w.r.t. ¯I. According to Definition 8 (page 11), we have proven that s **is true** for Pj w.r.t. ¯I**. This concludes the proof of the lemma.**
Theorem 2 **(see page 22)**
Given a SOLP collection SP = {P1, · · · ,Pn}, it holds that A = B**, where:**
A = SM (P
′u ∪ C(P1, · · · ,Pn)) and B = {F¯ ∪ G¯ ∪ H¯ | F¯ =S1≤i≤n
(F
i)Pi ∧ F
i ∈ AFP(Pi) ∧ F¯ ∈ SOS(P1, · · · ,Pn) ∧ (1)
G¯ =S1≤i≤n
(Gi)Pi ∧ (Gi)Pi = [F
i]Pi \ (F
i)Pi ∧ (2)
H¯ =S1≤i≤n
(H i)Pi ∧ (H i)Pi =Ss∈MSC Pi SAT Pi F¯(s)}**. (3)**
Proof Before starting with the proof, let us denote C(P1, · · · ,Pn**) by** C¯ .

(⊆). By contradiction, assume that ∀X ∈ A, X 6∈ B**. Observe that, according**
to Definitions 14, 17 and 20 (see pages 16, 18 and 20, respectively), it holds that X = F¯ ∪ G¯ ∪ H¯ such that F¯ ∩ G¯ = ∅, G¯ ∩ H¯ = ∅, F¯ ∩ H¯ = ∅**. Thus, we prove that**
either condition (1), (2), or (3) is false. We consider each condition **separately.**
Condition (1). In case condition (1) is false, it holds that F¯ 6∈ SOS(P1, **· · ·** ,Pn).

It follows that either:
(a) ∃i | (F
i)Pi ⊆ F¯ ∧ F
i 6∈ AFP(Pi), or