The first set is ∆. The second set (which includes the case in which a = ⊥) is a set of **⊥ → ⊥**. Indeed, each a X = ⊥, and since X |= Γ, X doesn't satisfy any F and then F
X = ⊥.

For part (b) it is easy to verify that the **while** loop iterates as long as Y 6|= ∆,
so that Z |= ∆. Now assume, in sake of contradiction, that there is a set Z
′
that satisfies ∆ and that is not a superset of Z. Consider, in the execution of the algorithm, the first atom a 6∈ Z
′added to Y , and that value of Y ⊆ Z
′to which a has been added to. This means that ∆ contains a formula G → a such that Y |= G. Recall that G stands for a formula of the form F
X , where F is a formula with aggregates with monotone and antimonotone aggregates only and without implications (other than negations) or equivalences. Consequently, by Lemma 15, Z
′|= G. On the other hand, a 6∈ Z
′, so Z
′ 6|= G → a, contradicting the hypothesis that Z
′is a model of ∆.

## 4.10 Proof Of Proposition 17

Lemma 16. Let F and G *two propositional formulas, and let* F
′ and G′*the result* of replacing each occurrence of an atom a in F and G *with a propositional formula* H. If F and G *are strongly equivalent to each other then* F
′ and G′ are strongly equivalent to each other. Proof. It follows from Proposition 5, in view of the following fact: if F and G are equivalent in the logic of here-and-there to each other then F
′and G′are equivalent in the logic of here-and-there to each other.

Lemma 17. Let F and G be two propositional formulas that are AND-OR combinations of ⊤, ⊥ and atoms only. If F and G are classically equivalent to each other then they are strongly equivalent to each other also.

Proof. In view of Proposition 5, it is sufficient to show that, for every set X of atoms, F
X is classically equivalent to GX. By Lemma 2 we can distribute the reduct operator in F
X to its atoms. If follows that F
X is classically equivalent to F with all occurrences of atoms that don't belong to X replaced by ⊥, and similarly for GX . The fact that F
X is classically equivalent to GX now follows from the classical equivalence between F and G.

Next Lemma immediately follows from our definition of satisfaction of aggregates (Section 3.1 of this paper), and the definition of [L ≤ S] and [S ≤ U] and Proposition 1 from [Ferraris and Lifschitz, 2005b].

Lemma 18. For every weight constraints L ≤ S and S ≤ U and any set X of atoms,