In our proofs we mostly omit sortal predicates such as Time(t), Region(r) and so on. Proof of Scenario 5 If there is a small object and a open container in reach, then the agent can reach for the object, put it into the container, and then withdraw his hand from the container. As with most logical proofs of projection, this is largely a matter of tracing frame inferences, with the occasional causal inference. Given: C.5.A.A: UprightContainer(Ta5,Ob5,Rc5). C.5.A.B: DC(Place(Ta5,Ox5),Rc5). C.5.A.C: SmallSet(Union(Contents(Ta5,Rc5),Singleton(Ox5),Rc5)). C.5.A.D: AllStable(Ta5). C.5.A.E: EmptyHanded(Ta5). C.5.A.F: Graspable(Ta5,Ox5). C.5.A.G: Reachable(Ta5,Rc5). C.5.A.H: Ox5 != Agent != Ob5. C.5.A.I: OutsideContainer(Place(Ta5,Agent),Place(Ta5,Ob5)). C.5.A.J: SafelyMovable(Ta5,Ox5). C.5.A.K: SmallObject(Ox5). Infer: Feasible(Ta5,Tb5,LoadUprightContainer(Ox5,Ob5). Lemma 5.A forall(ta,tb,r,o) Region(r) ^ Occurs(ta,tb,TravelTo(r)) ^ EmptyHanded(ta) ^ AllStable(ta) ^ Object(o) ^ o != Agent => Place(tb,o) = Place(ta,o) ^ AllStable(tb) Proof by contradiction. Assume: 5A.1 Region(Rp) 5A.2 Occurs(Tp,Tq,TravelTo(Rp)). 5A.3 EmptyHanded(Tp). 5A.4 AllStable(Tp) 5A.5 Object(O). 5A.6 O != Agent But 5A.7 not [Place(Tq,O) = Place(Tp,O) ^ AllStable(Tq)] Infer: 5A.8 Lt(Tp,Tq). 5A.2 + T.E.A.A 5A.9 Place(Tq,O) != Place(Tp,O)) V not AllStable(Tq). 5A.7 Assume: 5A.10: Place(Tq,O) != Place(Tp,O). 5A.11. Moves(Tp,Tq,O). M.R.D.A + 5A.8 + 5A.9 + T.I.D.A. 5A.12 Place(Tq,O) != Place(Tp,O) => Moves(Tp,Tq,O). Discharge 5A.11 against 5A.8 5A.13 forall (o) not Grasp(Tp,o). 5A.3 + M.G.D.A. 5A.14 forall (o) o = Agent V Stable(Tp,o). 5A.13 + 5A.4 + M.O.D.J Assume 5A.15 not AllStable(Tq). 5A.16 exist(ox) ox != Agent ^ not Stable(Tq,ox) ^ not Grasp(Tq,ox) 5A.15 + M.O.D.J 5A.17 not Stable(Tq,Ox) 5A.16, named 5A.18 Ox != Agent 5A.16 5A.18a Stable(Tp,Ox). 5A.14 + 5A.18 5A.18b Moves(Tp,Tq,Ox). M.R.A.D + 5A.17 + 5A.18a + 5A.8. 5A.19 not AllStable(Tq) => exists(ox) ox != Agent ^ Moves(Tp,Tq,Ox) Discharge 5A.16, 5A.18b against 5A.13. 5A.20 exists(ox) ox !=Agent ^ Moves(Tp,Tq,ox). 5A.9 + 5A.12 + 5A.6 + 5A.19 5A.21 Ox != Agent. 5A.20, naming 5A.22 Moves(Tp,Tq,Ox) 5A.20. 5A.23 exists (tc,td,oy,ry) TimeIntervalOverlap(tc,td,Tp,Tq) ^ PossiblyMovedBy(tc,Ox,oy) ^ [Occurs(tc,td,MovesTo(oy,ry)) V Falling(tc,td,oy)]. M.R.A.A + 5A.21 + 5A.22 5A.24 TimeOverlap(Tc,Td,Tp,Tq). 5A.23, naming. 5A.25 Occurs(Tc,Td,MovesTo(Oy,Ry)) V Falling(Tc,Td,Oy) 5A.23 5A.26 exists(tm) Lt(Tc,tm) ^ Lt(tm,Td) ^ Lt(tq,Tm) ^ Lt(tm,Tq).T.I.D.D + 5A.25 5A.27 Lt(Tc,Tm). 5A.26 + naming. 5A.28 Lt(Tm,Td). 5A.26 5A.29 Lt(Tp,Tm). 5A.26 5A.30 Lt(Tm,Tq). 5A.26 5A.31 Released(Tp,Tq,Oy). M.O.D.E + 5A.2 5A.32 not Grasp(Tm,Oy). M.G.D.D + 5A.31 + 5A.29 + 5A.30. 5A.33 not Grasps(Tc,Td,Oy). 5A.32 + 5A.27 + 5A.28 + M.G.D.B (contrapositive). 5A.34 not Occurs(Tc,Td,MovesTo(Oy,Ry)). 5A.33 + M.O.D.G. (contrapositive) 5A.35 Falling(Tc,Td,Oy). 5A.25 + 5A.34. 5A.36 Grasp(Tc,Oy). M.O.A.B + 5A.35 5A.36a Oy != Agent. M.G.A.D + 5A.36 5A.37 Ordered(Tc,Tp). T.I.A.E + 5A.27 + 5A.29 5A.38 Lt(Tc,Tp) V Lt(Tp,Tc) V Tc=Tp. T.I.D.B + 5A.37. 5A.39 Tc != Tp. 5A.13 + 5A.36. Assume 5A.40 Lt(Tc,Tp) 5A.41 Lt(Tp,Td). T.I.A.B + 5A.29 + 5A.28. 5A.42 not Stable(Tp,Oy). M.O.A.B + 5A.35 + 5A.40 + 5A.41. 5A.43. Contradiction. M.O.D.J + 5A.42 + 5A.4 + 5A.14 + 5A.36a 5A.44 not Lt(Tc,Tp). Discharge 5A.43 against 5A.40. Assume 5A.45 Lt(Tp,Tc). 5A.46 Lt(Tc,Tq). T.I.A.B + 5A.27 + 5A.30. 5A.47 not Grasp(Tc,Oy). M.G.D.D + 5A.31 + 5A.45 + 5A.46. 5A.48 Contradiction 5A.49 not Lt(Tp,Tc). Discharge 5A.48 against 5A.45 5A.50 Contradiction. 5A.38 + 5A.39 + 5A.44 + 5A.49. QED. Lemma 5.A proven. Lemma 5B: FaceConn(ra,rb) ^ DC(rb,rc) => not P(ra,rc). Proof of the contrapositive: Assume 5B.1 P(Ra,Rc) 5B.2 DC(Rb,Rb) Infer 5B.3 DC(Ra,Rb) S.B.A.I + 5B.1 + 5B.2 5B.4 not C(Ra,Rb) 5B.3 + S.B.D.D 5B.5 not EC(Ra,Rb) 5B.4 + S.B.D.C 5B.6 not FaceConn(Ra,Rb) 5B.5 + S.C.D.A 5B.7: FaceConn(ra,rb) ^ DC(rb,rc) => not P(ra,rc) Discharge 5B.7 against 5B.1, 5B.2, rearrange Lemma 5C: SimpleUprightContainer(t,ob,rc) ^ Object(ox) => [UContained(t,ox,ob) <=> P(Place(t,ox),rc)] Proof: Assume 5C.1 SimpleUprightContainer(T,Ob,Rc) 5C.2 SimpleUprightContainerShape(Place(T,Ob),Rc). 5C.1 + O.R.D.D 5C.3 UprightContainerShape(Place(T,Ob),Rc). 5C.2 + S.C.D.F 5C.3 forall(rd) UprightContainerShape(Place(T,Ob),rd) 5C.2 + S.C.D.F => P(rd,Rc) Assume 5C.4 UContained(T,Ox,Ob). 5C.5 exists(rc) UprightContainer(T,Ob,rc) ^ P(Place(T,Ox),rc) 5C.4 + O.C.D.C 5C.6 UprightContainer(T,Ob,Rca) 5C.5 + naming 5C.7 P(Place(T,Ox),Rca) 5C.5 + naming 5C.8 UprightContainerShape(Place(T,Ob),Rca). 5C.6 + O.R.D.C 5C.9 P(Rca,Rc). 5C.3 + 5C.8 5C.10 P(Place(T,Ox),Rc). S.B.A.B + 5C.7 + 5C.9 5C.11 forall(o) UContained(T,o,Ob) => P(Place(T,o,Rc). Discharge 5C.10 against 5C.4 5C.12 UprightContainer(T,Ob,Rc). 5C.3 + O.R.D.C. 5C.13 forall(o) Object(o) ^ P(Place(T,o),Rc) => UContained(T,o,Ob) O.C.D.C + 5C.13 Infer: SimpleUprightContainer(t,ob,rc) ^ Object(ox) => [UContained(t,ox,ob) <=> P(Place(t,ox),rc)] Combine 5C.13, 5C.11, discharge against 5C.1. Lemma 5.D DR(r,ra) ^ DR(r,rb) => DR(r,RUnion(ra,rb)) Proof of contrapositive Assume 5D.1 not DR(R,Runion(Ra,Rb)). Infer 5D.2 O(R,RUnion(Ra,Rb)). 5D.1 + S.B.D.B 5D.3 O(R,Ra) V O(R,Rb). 5D.2 + S.B.A.H 5D.4 not(DR(R,Ra) ^ DR(R,Rb)). 5D.3 + S.B.D.B 5D.5 forall(r,ra) DR(r,ra) ^ DR(r,rb) => DR(r,RUnion(ra,rb)) Discharge 5D.4 against 5D.1, take contrapositive Lemma 5.E NoObstacles(t,ra) ^ NoObstacles(t,rb) => NoObstacles(t,RUnion(ra,rb) Assume:5E.1 NoObstacles(T,Ra). 5E.2 NoObstacles(T,Rb). 5E.3 forall(o) Object(o) ^ o != Agent => DR(Place(T,o),Ra). M.F.D.A + 5E.1 5E.4 forall(o) Object(o) ^ o != Agent => DR(Place(T,o),Rb). M.F.D.A + 5E.2 5E.5 forall(o) Object(o) ^ o != Agent => DR(Place(T,o),RUnion(Ra,Rb)). Lemma5D + SE.3 + SE.4 5E.6 NoObstacles(T,RUnion(Ra,Rb)). M.F.D.A + SE.6 QED Lemma 5.E Lemma 5.F forall(ta,tb,r,o) Region(r) ^ Occurs(ta,tb,TravelTo(r)) ^ EmptyHanded(ta) ^ AllStable(ta) ^ Feasible(ta,TravelTo(rx)) => Feasible(tb,TravelTo(rx)) Assume: 5F.1 Region(R). 5F.2 Occurs(Ta,Tb,TravelTo(R)). 5F.3 EmptyHanded(Ta) 5F.4 AllStable(Ta) 5F.5 Feasible(Ta,TravelTo(Rx)) Infer: 5F.6 forall(o) o!= Agent => Place(Tb,o) = Place(Ta,o) Lemma 5.A + 5F.2 + 5F.3 + 5F.4 5F.7 exists(tc) Occurs(Ta,tc,TravelTo(Rx)). T.E.D.A + 5F.5 5F.8 Occurs(Ta,Tc,TravelTo(Rx)). 5F.7, Naming. 5F.9 exists(rw) Trajectory(Place(Ta,Agent),Rx,rw) ^ M.F.A.G + StaysIn(Ta,Tc,Agent,rw) ^ 5F.3 + 5F.4 + NoObstacles(Ta,rw). 5F.8 5F.10 Trajectory(Place(Ta,Agent),Rx,Rw). 5F.9, naming 5F.11 NoObstacles(Ta,Rw) 5F.9, naming 5F.12 exists(ry) Trajectory(Place(Ta,Agent),R,ry) ^ M.F.A.G + 5F.3 + NoObstacles(Ta,ry). 5F.4 + 5F.2 5F.13 Trajectory(Place(Ta,Agent),R,Ry). 5F.12, naming 5F.14 NoObstacles(Ta,Ry) 5F.12, naming 5F.15 Trajectory(R,Rx,RUnion(Ry,Rw)). M.F.A.D + M.F.A.E + 5F.10 + 5F.13 5F.15 NoObstacles(Ta,RUnion(Ry,Rw)). Lemma 5.E + 5F.11 + 5F.14 5F.16 NoObstacles(Tb,RUnion(Ry,Rw)). M.F.D.A + 5F.6 + 5F.15 5F.17 AllStable(Tb). Lemma 5.A + 5F.2 + 5F.3 + 5F.4 5F.18 EmptyHanded(Tb). 5F.2 + M.O.D.E + M.G.D.D + T.I.D.A + M.G.D.A 5F.19 exists(td) Occurs(Tb,td,TravelTo(Rx)) M.F.A.H + 5F.18 + 5F.17 + 5F.16 + 5F.15. 5F.20 Feasible(Tb,TravelTo(Rx)). T.E.D.A + 5F.19 Lemma 5.G forall(ta,tb,r,o) Region(r) ^ Occurs(ta,tb,TravelTo(r)) ^ EmptyHanded(ta) ^ AllStable(ta) ^ Reachable(ta,rd) => Reachable(tb,rd) Assume: 5G.1 Region(R). 5G.2 Occurs(Ta,Tb,TravelTo(R)). 5G.3 EmptyHanded(Ta) 5G.4 AllStable(Ta) 5G.5 Reachable(Ta,Rd) Infer 5G.6 exists(rx) IntConn(RUnion(rx,Rd)) ^ Feasible(Ta,TravelTo(rx)). A.C.D.D + 5G.5 5G.7 IntConn(RUnion(Rx,Rd)) 5G.7, naming 5G.8 Feasible(Ta,TravelTo(Rx)). 5G.7, naming 5G.9 Feasible(Tb,TravelTo(Rx)). Lemma 5.F + 5G.2 + 5G.3 + 5G.5 + 5G.8 5G.10 Reachable(Tb,Rd). A.C.D.D + 5G.9 + 5G.7. Proof of Case 5 5.1 exists(tm1,ra) Occurs(Ta5,tm1,TravelTo(ra)) ^ CanGrasp(tm1,Ox5). C.5.A.F + M.F.D.B 5.2 Occurs(Ta5,Tm1,TravelTo(Ra1)). 5.1, naming 5.3 CanGrasp(Tm1,Ox5) 5.1 5.4 forall(o) Object(o) ^ o != Agent => Lemma 5.A + 5.2 + C.5.A.D + Place(Tm,o) = Place(Ta5,o) C.5.A.E 5.5 AllStable(Tm1) Lemma 5.A + 5.2 + C.5.A.D + C.5.A.E 5.6 Place(Tm1,Ob5) = Place(Ta5,Ob5) C.5.A.H + 5.4. 5.7 SimpleUprightContainerShape(Place(Ta5,Ob5),Rc5). C.5.A.A + O.R.D.D 5.8 SimpleUprightContainerShape(Place(Tm1,Ob5),Rc5). 5.7 + 5.6 5.9 SimpleUprightContainer(Tm1,Ob5,Rc5) 5.8 + O.R.D.D 5.10 Place(Tm1,Agent) = Ra1 5.2 + M.O.D.E. 5.11 FaceConn(Place(Tm1,Agent),Place(Tm1,Ox5)) 5.3 + M.G.A.B 5.12 Place(Tm1,Ox5) = Place(Ta5,Ox5). C.5.A.H + 5.4. 5.13 DC(Place(Tm1,Ox5),Rc5). C.5.A.B + 5.12 5.14 not P(Place(Tm1,Agent),Rc5). Lemma 5B + 5.13 + 5.11. 5.15 not UContained(Tm1,Agent,Ob5). Lemma 5C + 5.9 + 5.14. 5.16 not Element(Agent,UContents(Tm1,Ob5)) 5.15 + O.C.D.E Assume 5.17 Element(Oy,UContents(Tm1,Ob5)) 5.18 Oy != Agent. 5.17 + 5.16 5.19 UContained(Tm1,Oy,Ob5) 5.17 + O.C.D.E. 5.20 P(Place(Tm1,Oy),Rc5). Lemma 5C + 5.9 + 5.19 5.21 Place(Tm1,Oy) = Place(Ta5,Oy). 5.4 + 5.18. 5.22 P(Place(Ta5,Oy),Rc5). 5.20 + 5.21 5.23 UContained(Ta5,Oy,Ob5) 5.22 + 5.7 + Lemma 5C 5.24 Element(Oy,UContents(Ta5,Ob5)) 5.23 + O.C.D.E 5.22 forall(oy) Element(oy,UContents(Tm1,Ob5)) Element(oy,UContents(Ta5,Ob5)) Discharge 5.21 against 5.14. 5.23 forall(oy) Element(oy,UContents(Tm1,Ob5)) V Element(oy,Singleton(Ox5)) => Element(oy,UContents(Ta5,Ob5)) V Element(oy,Singleton(Ox5)). 5.22 5.24 forall(oy) Element(oy,Union(UContents(Tm1,Ob5),Singleton(Ox5))) => Element(oy,Union(UContents(Ta5,Ob5),Singleton(Ox5))) 5.23 + O.S.D.F 5.25 Subset(Union(UContents(Tm1,Ob5),Singleton(Ox5)), Union(UContents(Ta5,Ob5),Singleton(Ox5)). 5.24 + O.S.D.C 5.26 SmallSet(Union(Contents(Tm1,Ob5),Singleton(Ox5)), Rc5). O.F.A.F + 5.25 + C.5.A.C 5.27 Lt(Ta5,Tm1) 5.2 + T.E.A.A 5.28 EmptyHanded(Tm1) 5.2 + M.O.D.E + M.G.D.D + T.I.D.A + M.G.D.A 5.29 Reachable(Tm1,Ra1) Lemma 5.G + 5.2 + C.5.A.D + C.5.A.E + C.5.A.G 5.30 UprightContainer(Tm1,Ob5,Rc5) 5.9 + O.R.D.D + S.C.D.F 5.31 Feasible(Tm1,PutInUC(Ox5,Ob5)) A.C.A.A + 5.30 + 5.3 + 5.26 + 5.29. 5.32 exists(tm2) Occurs(Tm1,tm2,PutInUC(Ox5,Ob5)). T.E.D.A + 5.31 5.33 Occurs(Tm1,Tm2,PutInUC(Ox5,Ob5)). 5.32 + naming 5.34 exists(rc,rx) UprightContainer(Tm1,Ob5,rc) ^ P(rx,rc) ^ A.C.D.C + 5.33 Occurs(Tm1,Tm2,SafeMoveTo(Ox5,rx)) ^ OV(Place(t,Agent),rc) 5.35 Occurs(Tm1,Tm2,SafeMoveTo(Ox5,Rx6)) 5.34 + naming 5.36 UprightContainer(Tm1,Ob5,Rc6) 5.34 + naming 5.37 P(Rx6,Rc6.) 5.34 + naming 5.38 OV(Place(Tm1,Agent),Rc6) 5.34 + naming 5.39 Feasible(Ta5,TravelTo(Place(Ta5,Agent))). M.F.A.I + M.O.D.D + M.O.D.E + M.O.D.F 5.40 Feasible(Tm1,TravelTo(Place(Ta5,Agent))). Lemma 5.F + 5.2 + 5.5 + C.5.A.E + 5.39 5.45 OpenContainer(Tm1,Ob5,Rc6). O.R.D.C + S.C.A.C + O.R.D.A + 5.36 5.46 not P(Place(Tm1,Agent,Rc6). S.B.D.F + 5.38 5.47 DR(Place(Ta5,Agent),Rc6) S.C.D.H + O.R.D.B + 5.45 + C.5.A.I 5.48 Feasible(Tm2,TravelTo(Place(Ta5,Agent))). M.M.A.B + 5.35 + 5.45 + 5.37 + 5.40 + 5.47 + 5.46 5.49 exists(tb5) Occurs(Tm2,tb5,TravelTo(Place(Ta5,Agent))) T.E.D.A + 5.48 5.50 Occurs(Tm2,Tb5,TravelTo(Place(Ta5,Agent))). 5.49, naming 5.51 Occurs(Tm1,Tb5,Sequence(PutInUc(Ox5,Ob5),TravelTo(Place(Ta5,Agent))) A.C.D.A + 5.33 + 5.50 5.52 Occurs(Ta5,Tb5,Sequence(TravelTo(Ra5), Sequence(PutInUc(Ox5,Ob5),TravelTo(Place(Ta5,Agent)))) A.C.D.A + 5.2 + 5,51 5.53 Occurs(Ta5,Tb5,LoadOpenContainer(Ox5,Ob5)). A.C.D.B + C.5.A.K + 5.52. QED Scenario 5.