Some of the literals in tg p\#; p\# may be added by operators in but none of the literals in tg p\#; p\#can be deleted by an operator in without reestablishing this literal by another operator after its deletion. Because contains only operators with unconditional effects, it adds and deletes the same literals regardless of the initial state.

Let us now assume that there exists a literal l tg p\#; p\#that is not added by . This implies that l I
1 and we have to distinguish three cases:
1. l fi(2n , from which we conclude that l I
2.

2. l ti p\#; ;  I
1, which also implies that l I
2.

3. l ti q ; L with q 6 p\#and L ffq ; f:q ; ;g. Because we assumed that the statetranslation functions are quasi-local on 2n, l must be a universal literal. If l is universal for ti, then we will have l I
2 because the possible initial states contain positive and negative literals as well as no literal for some elements from 2n. If l is universal for tg , it is present in G1 and in G2 for the same reason. Further, because l is not added by and is a valid plan from I
2 to G2, it must also be part of of I
2.
In other words, all literals l tg p\#; p\#that are not added by are already in I
1 and I
2.

From that we conclude that

```
                       Res I
                            
                            2; )  tg p#; p#:
Now let

```

G00 2 tg (2n  p\#; I\#
2  f:p\#fg(2n ;
G000 2 G00 2 tg p\#; p\#
tg (2n; I\#
2  f:p\#p\#fg(2n :
Because tg is modular, it is clear that G2  G00 2 and therefore Res I
2; )  G00 2 . Because achieves G00 2 as well as tg p\#; p\#, it follows that (again because tg is modular), achieves also G000 2 .

Since h 2n; I2; I\#
2  f:p\#p\#gi does not have any plan, there should not be any plan for h 2n; I
2; G000 2 i. The fact that is a plan for this instance implies that f cannot be a compilation scheme, which is the desired contradiction.

Using Propositions 4 and 5 as well as Theorem 9, this result can be generalized as follows (see also Table 1). Corollary 12 SBIC , SBC *, and* SLIC *cannot be compiled to* SBI *or any formalism specializing* SBI

preserving plan size linearly.

This answers the question of whether more space efficient compilation schemes from SLC to S than the one proposed by Gazen and Knoblock (1997) are possible. Even assuming unbounded computational resources for the compilation process, a more space efficient compilation scheme is impossible—provided that the compilation should preserve plan size linearly.8If we allow polynomially larger plans, then efficient compilation schemes are possible (see Section 6).