OR Exists y1:TO U T5. in(x,y1)) FORALL x:TO U T4 U T5. NOT (Exists y1:T1 U T2. at(x,y1) AND Exists y1:TO U T5. in(x,y1))
TIM :  DOMAIN  INVARIANTS:
x0: airplane(x0)   = 2 x0: airport(x0)   = 3 x0: city(x0)   = 3
(x0,x1): in-city(x0,x1)   = 6 x0: location(x0)   = 6 x0: obj(x0)   = 8 x0: truck(x0)   = 3

## Tim: Attribute Spaces:

Objects, x, in T1 U T2 can have property:
Exists y1:T0 U T4 U T5. at(y1,x);
Objects, x, in TO U T5 can have property: Exists y1:T0 U T4 U T5. in(y1,x); Objects, x, in T5 all have property: airplane(x);
Objects, x, in T2 all have property: airport(x); Objects, x, in T3 all have property: city(x); Objects, x, in T1 U T2 all have property: Exists y1:T3. in-city(x,y1);
Objects, x, in T3 all have property: Exists y1:T1 U T2. in-city(y1,x);
Objects, x, in T1 U T2 all have property: location(x);
Objects, x, in T4 all have property: obj(x);
Objects, x, in TO all have property: truck(x);

## Tim :  Operator  Parameter  Restrictions :

drive(x1:T0,x2:T1 U T2,x3:T1 U T2,x4:T3)
fly(x1:T5,x2:T2,x3:T2) unload(x1:T0 U T4 U T5,x2:T0 U T5,x3:T1 U T2)
load-plane(x1:T4,x2:T5,x3:T1 U T2)
load-truck(x1:T4,x2:T0,x3:T1 U T2)
TIM: ADDITIONAL STATE INVARIANTS, USING SUB-STATE ANALYSIS: