something on it, but it cannot be both clear and have something on it. The reason we cannot infer this as an invariant is because it would be asserted to hold for every object in the attribute space, including the table, even though it is not actually true of the table (the table can have things on it and still be clear).

## 2.7.1 Sub-Space Analysis On Property And Attribute Spaces

The solution to the problem of loss of invariants is to decompose any property or attribute ssss turally identical to a property space. Attribute sub-spaces are identified but not used, as no invariants can be obtained from them. Property sub-spaces can be obtained by analyssssse sub-spaces from property and attribute spaces is that the properties are not partitioned in sub-spaces as they are in the property and attribute spaces. The original property or attribute space is not discarded and the sub-spaces are not used for determining the types of objects. The only role of the sub-space analysis is to enable the construction of additional invariants.

We now consider the Blocks domain described in the previous section as an example of the benefits of sub-space analysis. At the point of invariant construction the types of the domain objects have been identified by their property and attribute space membership, so table is already known to be of a different type to that of the blocks. This is because table is not a member of the property space for on 1 . Therefore, two sub-spaces can be constructed from the attribute space, one for the type 11, of blocks, and one for the type 01, of tables. No sub-spaces can be constructed from the property space because it contains only one type of object. The rules associated with the sub-spaces will be all of the rules from the original attribute space that are enabled by objects of the appropriate type. The second of the two sub-spaces is an attribute sub-space because of the inclusion of the increasing attribute transition rule. At this stage the two sub-spaces are as follows:

$$o n_{2},\,c l e a r_{1}$$
$\begin{array}{cccc}on_2&clear_1,&clear_1&on_2&black A,&block B,&block C,\\ table_1&null&clear_1,&on_2&clear_1,&table\\ clear_1&on_2&\end{array}$
The attribute sub-space will not be used for invariant construction because it contains an attribute transition rule and would result in incorrect invariants (as is the case for attribute spaces), so there is nothing to be gained from developing it further. However, the state sub-space is now completed by the addition of the states associated with the objects in the ssss

$$\begin{array}{l l l}{o n_{2}}&{}&{}&{c l}\end{array}$$
$$o n_{2},\,c l e a r_{1}$$  $$o n_{2},\,c l e a r_{1}$$
$$\begin{array}{l}{{t a b l e_{1}}}\\ {{c l e a r_{1}}}\end{array}$$
$clear_{1}$, $clear_{1}$$on_{2}$$blockA$, $blockB$, $blockC$, $on_{2}$, $clear_{1}$$on_{2}$$clear_{1}$$on_{2}$
From the new state sub-space we can infer the following invanants, using the type name Block to stand for the type vector 11. We infer the identity invariant:

$x:Block\quad(\quad y\quad z\quad(on(y,x)\quad on(z,x)\quad y=z))$.  