for **Choices(**P1) ⊆ Ato(P1) ∪ Ath(P1) and **Choices(**P2) ⊆ Ato(P2) ∪ Ath(P2), and
(Ato(P1) ∪ Ath(P1)) ∩ (Ato(P2) ∪ Ath(P2**)) =** ∅. Sin
e TrNLP(P1) ⊔ TrNLP(P2) = TrNLP(P1 ⊔ P2)
holds, TrNLP is also modular. Thus TrNLP satises 
onditions 2 and 3 in Denition 4.27.

We are left to show that reveal(P, H) ≡m reveal(TrNLP(P), H)
for any smodels program module P = h**P, I, O, H**i and its translation TrNLP(P) =
h**R, I, O, H** ∪ H′i. Note that SM(P) = SM(reveal(P, H)) and SM(TrNLP(P**)) =**
SM(reveal(TrNLP(P), H)), and the additional restri
tion imposed by revealing is that the bije tion between these sets of stable models needs to be su h that their pro je tions over At(P), not just over Atv(P), 
oin
ide.

We dene a fun tion f **: SM(**P) → 2 At(TrNLP(P)) su h that f(M) = M ∪ {a | a ∈ **Choices(**P) \ M}.

Clearly M = f(M) ∩ At(P). We need to show that
(i) given any M ∈ SM(P), f(M) ∈ SM(TrNLP(P)); and
(ii) f : SM(P) → SM(TrNLP(P)) is a bije
tion.

Note that for any atom a ∈ **Choices(**P), it holds that a ∈ f(M) if and only if a 6∈ M
if and only if a 6∈ f(M).

(i) We show that N = f(M) ∈ SM(TrNLP(P)) for any M ∈ SM(P):
Assume rst N 6|= RN,I, that is, there is a rule r in RN,I that is not satised by N .

If Head(r) ∈ At(P), then r is of the form a ← B′ \ I and there are two possibilities:

1. There is a rule a ← B′, ∼C, ∼a ∈ R 
orresponding to a 
hoi
e rule {A} ←
B′, ∼C ∈ P su
h that a ∈ A, a 6∈ N , B′ ∩I ⊆ N , and C ∩N = ∅. Sin
e a 6∈ N
implies a ∈ N , r is satised in N , a 
ontradi
tion.

2. There is a rule a ← B′, ∼C
′ ∈ R 
orresponding to a weight rule r
′ =
a ← w ≤ {B = WB, ∼C = WC } ∈ P su
h that B′ ⊆ B , C
′ ⊆ C , w ≤
Pb∈B′ wb +Pc∈C′ wc , B′ ∩ I ⊆ N , and C
′ ∩ N = ∅. Sin
e N 6|= r we must have a 6∈ N (whi
h implies a 6∈ M ) and B′ \ I ⊆ N . Thus B′ ⊆ N
whi h implies B′ ⊆ M . Moreover, C
′ ∩ N = ∅ implies C
′ ∩ M = ∅. But then w ≤Pb∈B′∩M wb +Pc∈C′\M wc . Sin
e B′ ⊆ B and C
′ ⊆ C , we have w ≤Pb∈B∩M wb +Pc∈C\M wc and M 6|= r
′
, a ontradi tion.

Otherwise ea h r ∈ RN,I is of the form a, in whi
h 
ase there is a rule a ← ∼a ∈ R
and a 6∈ N . Sin
e a 6∈ N implies a ∈ N , then N |= r, a 
ontradi
tion. Thus N |= RN,I, and furthermore N \ I |= RN,I.

Assume now N \I 6= LM(RN,I ), that is, there is N′ ⊂ N \I su
h that N′|= RN,I.

We dene M′ = N′∩At(P) and show M′|= P M,I, whi
h 
ontradi
ts the assumption M \ I = LM(P M,I ), sin
e M′ ⊂ M \ I . Assume that there is a rule r ∈ P M,I su
h that M′ 6|= r. There are two possibilities: