Let X ⊆ At be given. We consider two cases.

Case 1: X is cofinite, X = At \ {q1**, . . . , q**i}. We need to prove two inclusions,
(a) f(X) ⊆ GLP (X) and (b) GLP (X) ⊆ f(X).

For (a), note that if p ∈ f(X), then the clause p ← ¬q1**, . . . ,**¬qi belongs to P.

Hence p ← belongs to PX and p ∈ GLP (X). For (b), note that if p ∈ GLP (X), then given the form of the clauses in P, there must be some clause p ← ¬qi1

, . . . ,¬qij in P where {qi1

, . . . , qij
} ⊆ {q1**, . . . , q**i}.

But this means that p ∈ f(At \ {qi1

, . . . , qij
}). Since f is antimonote and At \
{q1, . . . , qi} ⊆ At \ {qi1

, . . . , qij
}, we must have

```
f(At \ {qi1
         
         , . . . , qij
                }) ⊆ f(At \ {q1, . . . , qi}) = f(X)

```

and, hence, p ∈ f(X). Thus GLP (X) ⊆ f(X).

Case 2: X is not cofinite. Let {q0, q1**, . . .**} be an enumeration of At \ X. Let Yi = At \ {q0**, . . . , q**i}. Then, clearly, X ⊆ Yi for all i ∈ N. Moreover the sequence hYiii∈N is monotonically decreasing and Ti∈N Yi = X. Therefore, by our assumptions on the operator f,

$$f(X)=\bigcup_{i\in N}f(Y_{i}).$$

Again, we need to prove two inclusions, (a) f(X) ⊆ GLP (X) and (b) GLP (X) ⊆
f(X). For (a), note that if p ∈ f(X), then for some i ∈ N, p ∈ F(Yi). Therefore, for that i, p ← ¬q0**, . . . ,**¬qiis a clause in P. But then X ∩ {q0**, . . . , q**i} = ∅ so that the clause p ← is in PX and p ∈ GLP (X). For the proof of (b), note that if p ∈ GLP (X), then because of the syntactic form of the clauses in our program there are atoms r0**, . . . , r**k so that the clause p ←
¬r0**, . . . ,**¬rk belongs to the program P, and r0**, . . . , r**k ∈/ X. Thus {r0, . . . , rk} ⊆
{q0, q1**, . . .**} and, hence, for some i ∈ N, {r0, . . . , rk} ⊆ {q0**, . . . , q**i}. Now, consider such a Yi. Since Yiis cofinite, it follows from Case 1 that f(Yi) = GLP (Yi).

Since X ⊆ Yi, f(Yi) ⊆ f(X) by the antimonotonicity of f. But p ∈ GLP (Yi) because r0**, . . . , r**k ∈/ Yi and, hence, p ∈ f(Yi). But since f(Yi) ⊆ f(X), p ∈ f(X)
as desired. ✷
We are now ready to prove the next result of this paper.

Proposition 4.6 Let P be a normal propositional program. The following are equivalent:
(a) P *is an* FSP*-program.*