---

Step * 1 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 (InstHyp [⌈e'⌉] (-7)⋅ THENA (RWW "eo-forward-locl eo-forward-le" 0 THEN Auto THEN (RelRST THEN Auto)⋅))
   THEN RWO "eo-forward-forward" (-1)
   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  (InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-7)\mcdot{}
              THENA  (RWW  "eo-forward-locl  eo-forward-le"  0  THEN  Auto  THEN  (RelRST  THEN  Auto)\mcdot{})
              )
  THEN  RWO  "eo-forward-forward"  (-1)
  THEN  Auto
  THEN  Auto)\mcdot{}

---

Home Index