In our proofs we mostly omit sortal predicates such as Time(t), Region(r) and so on. Scenario 2 Infer object characteristics from behavior. If the stuff Os2 is contained in Ob2 at one time and outside at another, then Ob2 is not a rigid object. Note: the order of Ta2,Tb2 is not specified. C.2.A.A: CContained(Ta2,Os2,Singleton(Ob2)). C.2.A.B: Outside(Place(Tb2,Os2),Place(Tb2,Ob2)). C.2.A.C: Ordered(Ta2,Tb2). Infer: not RigidObject(Ob2). Proof of Scenario 2: Lemma 2.A forall(u,v) O(u,v) <=> O(v,u). Proof. S.B.D.A. Lemma 2.B forall(u,v) DR(u,v) <=> DR(v,u). Proof: Lemma 2.A + S.B.D.B Lemma 2.C: forall(u,v) P(u,v) => O(u,v). Proof: S.B.D.A + S.B.A.C Lemma 2.D: forall(u,v) P(u,v) => not DR(u,v). Proof. Lemma 2.C + S.B.D.B Lemma 2.E: forall(u,v) Outside(u,v) => not Contained(u,v) Proof: 2E.1 Assume Outside(U,V) 2E.2 forall(w) Cavity(w,V) => DR(U,w). 2C.1 + S.C.D.C 2E.3 forall(w) Cavity(w,V) => not P(w,U). 2C.2 + Lemmas 2.B, 2.D 2E.4 not Contained(U,V). 2E.3 + S.C.D.D 2E.5: forall(u,v) Outside(u,v) => not Contained(u,v) Discharge 2E.4 against 2E.1. Lemma 2.F forall(t,o,s) Time(t) ^ Object(o) ^ ObjectSet(s) => [CContained(t,o,s) <=> exists(rc) ClosedContainer(t,s,rc) ^ P(Place(t,ox),rc) <=> exists(rs) OSPlace(t,s,rs) ^ Contained(Place(t,ox),rs) ] Proof: O.C.D.A, O.R.D.A, S.C.D.D. Lemma 2.G. forall(t,os,ob) Time(t) ^ Object(os) ^ Object(ob) => [CContained(t,os,Singleton(ob)) <=> Contained(t,Place(t,os),Place(t,ob))] Proof: By O.T.A.F, OSPlace(t,Singleton(ob),rs) <=> Place(t,ob)=rs. The result then follows from lemma 2.F. From Scenario 1 we can abstract the general rule Lemma 2.H forall [ob,ox,ta,tb] RigidObject(ob) ^ CContained(ta,ox,Singleton(ob)) ^ Object(ox) Lt(ta,tb) ^ ob != ox => CContained(tb,ox,Singleton(ob)). We can similarly prove the general rule. 2.2. forall [ob,ox,ta,tb] RigidObject(ob) ^ CContained(ta,ox,Singleton(ob)) ^ Object(ox) Lt(tb,ta) ^ ob != ox => CContained(tb,ox,Singleton(ob)). This is identical to Lemma 2.H except for the order of time points. The proof is the same as the proof of Scenario 1 except for the following replacements: 13. NoEntranceCavity(Ta1,Tb1,Hc1,HPlace(Ob1)). 11 + H.C.D.A. The proof of 20 depends on H.C.A.D 21. Leq3(Tb1,Tb1,Ta1). The proof of 22 depends on H.C.A.C. Lemma 2.I forall [ob,ox,ta,tb] RigidObject(ob) ^ CContained(ta,ox,Singleton(ob)) ^ Object(ox) Ordered(ta,tb) ^ ob != ox => CContained(tb,ox,Singleton(ob)). (Same again, except for replacing Lt(ta,tb) by Ordered(ta,tb).) Proof: From Lemma 2.H, 2.2 and T.I.D.B. We have proven both cases Lt(ta,tb) and Lt(tb,ta); and the case ta=tb is trivial. Equivalently: 2.4. forall [ob,ox,ta,tb] CContained(ta,ox,Singleton(ob)) ^ not CContained(tb,ox,Singleton(ob)) ^ Object(ox) ^ Ordered(ta,tb) ^ ob != ox => not RigidObject(ob) 2.5. Outside(Place(Tb2,Os2),Place(Tb2,Ob2)). C.2.A.B 2.6. not Contained(Place(Tb2,Os2),Place(Tb2,Ob2)). 2.5 + Lemma 2.E 2.7 not CContained(Tb2,Os2,Ob2). 2.6 + Lemma 2.G. 2.8. not RigidObject(Ob2). 2.4 + C.2.A.A + 2.7 + C.2.A.C + C.2.A.D.