Proposition 4. *For any theory, its models in the sense of equilibrium logic are* identical to its stable models.

Proof. A set Y of atoms is an equilibrium model of Γ iff
(Y, Y ) |= Γ and, for all proper subsets X of Y , (X, Y ) 6|= Γ.

In view of Proposition 3, this is equivalent to the condition Y |= ΓYand, for all proper subsets X of Y , X 6|= ΓY.

which means that Y is a stable model of Γ.

## 4.2 Proof Of Propositions 1 And 2

We first need the recursive definition of reduct for programs with nested expressions from [Lifschitz *et al.*, 1999]. The *reduct* F
X of a nested expression F relative to a set X of atoms, as follows:
- a X = a, ⊥X = ⊥ and ⊤X = ⊤,
- (F ∧ G)
X = F
X ∧ GX and (F ∨ G)
X = F
X ∨ GX ,
- (¬F)
X =
(⊥ , if X |= F ,
⊤ , otherwise, Then the reduct (F ← G)
X of a rule F ← G with with nested expression is defined as F
X ← GX , and the reduct ΠX of a program with nested expressions as the union of the reduct of its rules. Lemma 3. *The reduct* F
X of a nested expression F is equivalent, in the sense of classical logic, to the nested expression obtained from F
X *by replacing all atoms* that do not belong to X by ⊥.

Proof. The proof is by structural induction on F.

- When F is ⊥ or ⊤ then F
X = F = F
X .

- For an atom a, a X = a. The claim is immediate.

- Let F be a negation ¬G . If X |= G then F
X = ⊥ = F
X; otherwise, F
X = ¬⊥ = ⊤ = F
X.

- for F = G ⊗ H(**⊗ ∈ {∨**,∧}), F
X is GX ⊗ HX, and, by Lemma 2, F
X is equivalent to GX ⊗HX. The claim now follows by the induction hypothesis.