In our proofs we mostly omit sortal predicates such as Time(t), Region(r)
and so on.

Scenario 4.



iIf the situation depicted in figure 4} (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.4.A.A: forall(t)  Place(t,Ob4) = Place(Ta,Ob4).  Ob4 is fixed.
C.4.A.B: CombinedContainer(Place(Ta,Ob4), RRed, RInside)
C.4.A.C: P(Place(Ta4,Os4),RInside).
C.4.A.D: Outside(RGreen, RUnion(Place(Ta,Ob4),RRed)). 
C.4.A.E: P(Place(Tb4,Os4),RGreen).
C.4.A.F: Lt(Ta4,Tb4).


Proof of Scenario 4.

Lemma 4.A. P(u,v) ^ DR(v,w) => DR(u,w).
     Proof of contrapositive. 
     4A.1 Assume P(U,V) and not DR(U,W).
     4A.2 O(U,W). S.B.D.B + 4A.1.
     4A.3 exists(X) P(X,U) ^ P(X,W). S.B.D.A + 4A.2
     4A.4 exists(X) P(X,V) ^ P(X,W)  4A.3 and S.B.A.B
     4A.5 O(V,W). S.B.D.A.
     4A.6 not DR(V,W). S.B.D.B
Discharge and rearrange.

Lemma 4.B. Outside(u,v) ^ P(w,u) ^ Cavity(x,v) => not P(w,x). 
    4B.1 Assume Outside(U,V) ^ P(W,U) ^ Cavity(X,V)
    4B.2 DR(U,X)   S.C.D.C.
    4B.3 DR(W,X).  Lemma 4.A + 4B.2
    4B.4 not P(W,X). Lemma 2.D and 4B.3
Discharge


4.1 Cavity(RInside,RUnion(Place(Ta4,Ob4),RRed)) C.4.A.B + S.C.D.E
4.2 exists(h) Constant(Ta4,Tb4,h) ^ Slice(Ta4,h) = RInside.
        H.I.A.D + C.4.A.F.  Call this HC.
4.3 Constant(Ta4,Tb4,HC).  4.2.
4.4 Slice(Ta4,HC) = RInside. 4.2
4.5 exists(h) Constant(Ta4,Tb4,h) ^ Slice(Ta4,h) = RUnion(Place(Ta4,Ob4),RRed).
        H.I.A.D + C.4.A.F.  Call this HB.
4.6 Constant(Ta4,Tb4,HB).  4.5.
4.7 Slice(Ta4,HB) = RUnion(Place(Ta4,Ob4),RRed)). 4.5
4.8 PersistentCavity(Ta4,Tb4,HC,HB). H.C.A.E + 4.3 + 4.6 + 4.7.
4.9 NoExitCavity(Ta4,Tb4,HC,HB). 4.8 + H.C.D.A.
4.10 Continuous(Ta4,Tb4,HPlace(Os4)). H.I.A.A + C.4.A.F.
4.11 Slice(Ta4,HPlace(Os4)) = Place(Ta4,Os4). H.I.A.B.
4.12 P(Slice(Ta4,HPlace(Os4)),Slice(Ta4,HC)). C.4.A.C + 4.11 + 4.4.
4.13 not P(Place(Tb4,Os4), RInside).  Lemma 4.B, C.4.A.E, C.4.A.D.
4.14 Slice(Tb4,HPlace(Os4)) = Place(Tb4,Os4). H.I.A.B.
4.15 Slice(Tb4,HC) = Slice(Ta4,HC). H.I.D.B + 4.3
4.16 not P(Slice(Tb4,HPlace(Os4)),Slice(Tb4,HC)).  
                                   4.13 + 4.14 + 4.15 + 4.4.
4.17 exists(tm) Lt(T4a,tm) ^ Lt(tm,T4b) ^ 
                O(Slice(tm,HPlace(Os4)),Slice(tm,HB)).
                      H.C.A.B + 4.9 + 4.10 + 4.12 + 4.16.
               Call this Tm.
4.18 Lt(T4a,Tm) ^ Lt(Tm,T4b). 4.17.
4.19 O(Slice(Tm,HPlace(Os4)),Slice(Tm,HB)). 4.17
4.20 Slice(Tm,HB) = Slice(T4a,HB). H.I.D.B + 4.6,
4.21 Place(Tm,Ob4) = Place(T4a,Ob4). C.4.A.A
4.22 Slice(Tm,HB) = RUnion(Place(Tm,Ob4), RRed). 4.20 + 4.7 + 4.21
4.23 Slice(Tm,HPlace(Os4)) = Place(Tm,Os4). H.I.A.B.
4.24 O(Place(Tm,Os4),RUnion(Place(Tm,Ob4),RRed)). 4.19 + 4.22 + 4.23
4.25 O(Place(Tm,Os4),Place(Tm,Ob4)) V O(Place(Tm,Os4),RRed).  S.B.A.H + 4.24
4.26 DR(Place(Tm,Os4),Place(Tm,Ob4)). O.T.A.B + C.4.A.G.
4.27 O(Place(Tm,Os4),RRed).  4.25 + 4.26 + S.B.D.B.
4.28 exists (tm) Lt(Ta4,tm) ^ Lt(tm,Tb4) ^ O(Place(tm,Os4),RRed). 
        Existential abstraction from 4.17, 4.27.