As n is arbitrary,

$$C C G L_{P}(\bigcup_{j\in N}X_{j})\subseteq\bigcap_{n\in N}C C G L_{P}(X_{n}).$$

This proves (i).
To prove (ii), let p ∈Tn∈N **CCGL**P (Xn). Then, for every n ∈ N, p ∈ **CCGL**P (Xn)
and so, for every n ∈ N, there is a minimal support Un = {Y
(n)
1 u
(n)
1**, . . . , Y** (n)
mn u
(n)
Mn
}
for p such that
$$|Y_{i}^{(n)}\cap X_{n}|\leq u_{i}^{(n)}\;\mathrm{for}\;i=1,\ldots,m_{n}$$
But there are only finitely many -minimal supports for P-CC -proof schemes for
p. Therefore there is a support U0 = {Z1w1**, . . . , Z**twt} for a P-CC -proof scheme
with conclusion p such that for infinitely many n's
$$|Z_{i}\cap X_{n}|\leq w_{i}{\mathrm{~for~}}i=1,\ldots,t.$$
But the sequence hXnin∈N is monotonically increasing. Therefore for all n ∈ N,

$|Z_{i}\cap X_{n}|\leq w_{i}$ for $i=1,\ldots,t$.  
But since each Ziis finite, then it must be the case that

$$|Z_{i}\cap\bigcup_{n i n N}X_{n}|\leq w_{i}{\mathrm{~for~}}i=1,\ldots,t.$$

so that p ∈ **CCGL**P (Sn∈N Xn). ✷
We note that, alternatively, one can easily give a direct reduction of our CC -
programs to normal logic programs using the methods of [FL05] and the distributivity result of [LTT99]. Such reduction, of course, lead to an exponential blow up in the size of the representation.

## 6 Conclusions

We note that investigations of proof systems in a related area, SAT, play a key role in establishing lower bounds on the complexity of algorithms for finding the models. We wonder if there are analogous results in ASP. For achieving such a goal, we need to find and investigate proof systems for ASP. One candidate for such a proof system is provided in this paper by using P-proof schemes. We wonder if such a proof system can be used to develop a deeper understanding of the complexity issues related to finding stable models.