Proposition 18 For any monotone or antimonotone PDB-aggregates A *of the form (6)*
where F1, . . . , Fn are atoms, Atr *is strongly equivalent to (9).*
Proof. Let S be {F1 = w1, . . . , Fn = wn}. Lemma 20 says that Atr is classically equivalent to (9) for every formulas F1, . . . , Fn in S. We can then prove the claim of this proposition using Lemma 17, by showing that both Atr and (9) can be strongly equivalently rewritten as AND-OR combinations of
- F1, . . . , Fn, ⊤, ⊥, if A is monotone, and
- ¬F1, . . . ,¬Fn, ⊤, ⊥, if A is antimonotone.

About (9), this has already been shown in the proof of Proposition 17, while, about Atr, this is shown by Lemma 21. Indeed, each G(I,{1,...,n})is a (possibly empty)
conjunction of terms of the form Fi, and each G(∅,I)is a (possibly empty) conjunction of terms of the form ¬Fi, since each Fiis an atom.

## 4.12 Proof Of Proposition 19

We observe, first of all, that the definition of satisfaction of FLP-aggregates and FLP-programs in [Faber *et al.*, 2004] is equivalent to ours. The definition of a reduct is different, however. Next lemma is easily provable by structural induction.

Lemma 22. For any nested expression F *without negations and any two sets* X
and Y *of atoms such that* Y ⊆ X, Y |= F
X iff Y |= F.

Lemma 23. For any FLP-aggregate A and any set X of atoms, if X |= A *then* Y |= A
X iff Y |= A.

Proof. Let A have the form (6). Since X |= A, AX has the form oph{F
X
1 = w1, . . . , F X
n = wn**}i ≺** N.

In case of FLP-aggregates, each Fiis a conjunction of atoms. Then, by Lemma 22, Y |= F
X
iiff Y |= Fi. The claim immediately follows from the definition of satisfaction of aggregates.

Proposition 19. The stable models of a positive FLP-program under our semantics are identical to its stable models in the sense of *[Faber* et al.*, 2004].*