Inference 3.



If the situation depicted in figure 3 (from Smith, Dechter,
Tenenbaum, and Vul, 2013) is modified so that the red region is flush against
the green region, then the ball must reach the red region before it
can reach the green region.


Given: 
C.3.A.1: Fixed(Ob3).
C.3.A.2: CombinedContainer(Place(Ta,Ob3), RRed, RInside)
C.3.A.3: P(Place(Ta3,Os3),RInside).
C.3.A.4: Outside(RGreen, RUnion(Place(Ta,Ob3),RRed)). 
C.3.A.5: P(Place(Tb3,Os3),RGreen).
C.3.A.6: Lt(Ta3,Tb3).
C.3.A.7: Os3 != Ob3


Proof of Inference 3. 
(Note: Numbering of lemmas is non-sequential.)


Proof of Inference 3.

3.1 Cavity(RInside,RUnion(Place(Ta3,Ob3),RRed))               C3A2 + SCD4
3.2 exists(h) Constant(Ta3,Tb3,h) ^ Slice(Ta3,h) = RInside.   HIA3 + C3A6  
3.3 Constant(Ta3,Tb3,HC).                                     Naming 3.2.
3.4 Slice(Ta3,HC) = RInside.                                  Naming 3.2
3.5 exists(h) Constant(Ta3,Tb3,h) ^                           HIA3 + C3A6  
	 Slice(Ta3,h) = RUnion(Place(Ta3,Ob3),RRed).
3.6 Constant(Ta3,Tb3,HB).                                     Naming 3.5
3.7 Slice(Ta3,HB) = RUnion(Place(Ta3,Ob3),RRed)).             Naming 3.5
3.8 PersistentCavity(Ta3,Tb3,HC,HB).              HCA4 + 3.1 + 3.3 + 3.6 + 3.7
3.9 NoExitCavity(Ta3,Tb3,HC,HB).                              HCD1 + 3.8  
3.10 Continuous(Ta3,Tb3,HPlace(Os3)).                         HIA1 + C3A6
3.11 Slice(Ta3,HPlace(Os3)) = Place(Ta3,Os3).                 HIA2.
3.12 P(Slice(Ta3,HPlace(Os3)),Slice(Ta3,HC)).          C3A3 + 3.11 + 3.4
3.13 not P(Place(Tb3,Os3), RInside).          LemS.F + C3A5 + C3A4 + 3.1
3.14 Slice(Tb3,HPlace(Os3)) = Place(Tb3,Os3).                 HIA2.
3.15 Slice(Tb3,HC) = Slice(Ta3,HC).                           HID3 + 3.3
3.16 not P(Slice(Tb3,HPlace(Os3)),Slice(Tb3,HC)).  3.13 + 3.14 + 3.15 + 3.4
3.17 exists(tm) Lt(T3a,tm) ^ Lt(tm,T3b) ^            HCA2+3.9+3.10+3.12+    
                O(Slice(tm,HPlace(Os3)),Slice(tm,HB)).         3.16+Lem1.A 
3.18 Lt(T3a,Tm) ^ Lt(Tm,T3b).                               Naming 3.17.
3.19 O(Slice(Tm,HPlace(Os3)),Slice(Tm,HB)).                 Naming 3.17
3.20 Slice(Tm,HB) = Slice(T3a,HB).                            HID3 + 3.6
3.21 Place(Tm,Ob3) = Place(T3a,Ob3).                  C3A1 + MSA4 + MOD2
3.22 Slice(Tm,HB) = RUnion(Place(Tm,Ob3), RRed).       3.20 + 3.7 + 3.21
3.23 Slice(Tm,HPlace(Os3)) = Place(Tm,Os3).                   HIA2
3.24 O(Place(Tm,Os3),RUnion(Place(Tm,Ob3),RRed)).      3.19 + 3.22 + 3.23
3.25 O(Place(Tm,Os3),Place(Tm,Ob3)) V O(Place(Tm,Os3),RRed).  SBA4 + 3.24
3.26 DR(Place(Tm,Os3),Place(Tm,Ob3)).                         OTA1 + C.3.A.7.
3.27 O(Place(Tm,Os3),RRed).                             SBD3 + 3.25 + 3.26  
3.28 exists (tm) Lt(Ta3,tm) ^ Lt(tm,Tb3) ^ O(Place(tm,Os3),RRed). 
        Existential abstraction from 3.18, 3.27.