is reachable from I by application of a valid linearised plan formed from ground instances of operator schemas in O, then for any o   Os, the P-projection of St for o, St p, is in Ss.

## Proof:

The proof is by induction on the length of the plan that yields the state St. In the base case the plan contains no operator instances so St = I. The P-projection of I for o is in Ss, by definition of the first phase of the property space construction process described in Section 2.4.

Suppose St is generated by a plan of length k 1, with last step a and penultimate state pre-St. Let the P-projection of pre-St for o be pre-Ste. By the inductive hypothesis, this state is in Ss. If a does not affect the state of o, then the P-projection of St for o will be pre-Sif, and therefore in Ss trivially. Otherwise, consider the operator schema, 0, from which a is formed. As described in Section 2.7, no constants appear in Op 0 p and all variables in the body of Op are parameters of Op. Let the initial collection of PRSs constructed from Op, for those parameters instantiated with oin the creation of a, be the set PRS 1 ...PRS n where every PRS i has the form:
precs :

$\begin{array}{l}p r e c s\ \colon\\ d e l e t e d\_p r e c s\ \colon\\ x d\_o l e s\ \mathrm{or}t s\ \colon\end{array}$
add_elements :

$$\begin{array}{c}{{P_{i}}}\\ {{D_{i}}}\\ {{A_{i}}}\end{array}$$

and the initial collection is the collection formed prior to splitting.

For each value of i the ith PRS will lead to the construction of k 1 transition rules, where k is the size of the bag intersection, X i , of D i and A i . The k rules will be of the following form:

$\square$
Xi (Pi c

$$(P_{i}\qquad c$$
$$c\quad\quad c)$$

and the remaining rule will be of the form:

$\int_{\mathbb{R}}^{2}$. 
$$\begin{array}{r l r l r l}{{\left(D_{i}\quad X_{i}\right)}}&{{}}&{{\left(D_{i}\quad X_{i}\right)}}&{{}}&{{\left(A_{i}\quad X_{i}\right)}}\end{array}$$
We refer to the latter rule for PRS; as the ith complex rule. A subset of the n complex rules will contain a property in Ps in either the start or the finish and will, therefore, be relevant to the transition from pre-St to St. It can be observed that these m complex rules (PRS 1 ...PRS m without loss of generality) must be in P because of the uniting process described in 2.3.

We define pres(a)~ to be the P-projection of the preconditions of a for o. Similarly, adds(a) 2 and dels(a) 2 are defined to be the P-projections of the add and delete lists respectively. By construction of the PRSs, defined in Section 3.1,

pres(a) = adds(a), = dels(a)p =