It is at the point of extension of the space that the problem arises. The following states are added:  off1, touched1 ,  on1, touched1 ,  off1, touched1, touched1 , touched1  and ssse tended because the two, apparently identical, properties might in general refer to different aguments.

The problem here is due to the fact that touched 1 is actually an increasing attribute but this does not become apparent in the PRSs. The consequence is that mixed spaces are constructed. A mixed space is a property space containing hidden attributes. T I M detects hidden attributes by checking, on extension, that no new state contains a state already generated from the same initial state starting point. Thus, on extension of the mixed space above, TIM would detect the hidden attribute when the state on 1 , touched 1 , touched 1 is constructed, because this state contains the state on 1 that initiated this extension.

Having detected the hidden attribute there are two possibilities: either TIM can convert the mixed space into an attribute space, in which case no invariants will be constructed, or it can attempt to identify the attribute and split the mixed space into an attribute space and a property space containing the state-valued components of the mixed space. We take this option and split the state. This allows us to infer invariants concerning the state-valued properties.

TIM takes the difference between the including and included states and, foreach distinct property in the difference, processes the rules by culting any rule containing that property into two rules, at least one of which will be an attribute rule. The following method is used to cut the rules. In the following, attr+ indicates one or more occurrences of the attribute-valued property and the commais overloaded to mean both bag conjunction and bag union. If the rule is of the form:
enablers st art adds, attr+
then the two new rules will be of the forms:

$$e\,n\,a b l e r s,\,\,s t a r t\qquad n\,u l l\qquad a t t\,r^{+}$$

and

$$e\,n a b l e r s\ \ \ \ \ s t a r t\ \ \ \ \ a\,d d s$$
$\frac{1}{2}-\frac{1}{2}=-\frac{2}{2}+1=\frac{2}{2}$. 
If the rule is of the form:

$$e\,n a b l e r s\qquad a t\,t r^{+},\,\,p r e c s$$
$$a\,d l\,\mathrm{s}$$

then the two new rules are of the forms:

$$e n a b l e r s,\,p r e c s\qquad a t\,t r$$
$$n u l l$$

and

$$e n a b l e r s,\,a t t r\qquad p r e c s$$
$$a\,d s$$

The rule cutting separates the attribute-valued properties from the state-valued properties. Now pure attribute and property spaces can be constructed. However we do not discard the original mixed space because it has been used in determining the type structure of