---

Step * 2 of Lemma eo-forward-no-classrel-in-interval


1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. start : E
6. e1 : E
7. e : E
8. loc(e) = loc(e1) ∈ Id
9. loc(e1) = loc(start) ∈ Id
10. (no X between e1 and e)
11. e1 ≤loc e 
12. start ≤loc e1 
⊢ (no X between e1 and e)
BY
{ (UnfoldTopAb (-3)
   THEN UnfoldTopAb 0
   THEN ParallelOp -3
   THEN Auto
   THEN Try ((RelRST THEN Auto))
   THEN (All (RWO "eo-forward-forward eo-forward-le eo-forward-locl") THENA Auto)
   THEN Try ((BackThruSomeHyp THEN Auto))
   THEN Auto)⋅ }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
4.  es  :  EO+(Info)
5.  start  :  E
6.  e1  :  E
7.  e  :  E
8.  loc(e)  =  loc(e1)
9.  loc(e1)  =  loc(start)
10.  (no  X  between  e1  and  e)
11.  e1  \mleq{}loc  e 
12.  start  \mleq{}loc  e1 
\mvdash{}  (no  X  between  e1  and  e)


By

(UnfoldTopAb  (-3)
  THEN  UnfoldTopAb  0
  THEN  ParallelOp  -3
  THEN  Auto
  THEN  Try  ((RelRST  THEN  Auto))
  THEN  (All  (RWO  "eo-forward-forward  eo-forward-le  eo-forward-locl")  THENA  Auto)
  THEN  Try  ((BackThruSomeHyp  THEN  Auto))
  THEN  Auto)\mcdot{}

---

Home Index