---

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

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[start:E]. ∀[e1:E]. ∀[e:E].
  uiff((no X between e1 and e);(no X between e1 and e)) supposing (loc(e) = loc(e1) ∈ Id) ∧ (loc(e1) = loc(start) ∈ Id)
BY
{ ((Auto
    THEN Auto
    THEN (Assert e1 ≤loc e  BY
                (BLemma `eo-forward-E-member` THEN Auto))
    THEN (Assert start ≤loc e1  BY
                (BLemma `eo-forward-E-member` THEN Auto))
    THEN Try ((RelRST THEN Auto)⋅))
   THEN skip{(UnfoldTopAb (-3)
              THEN UnfoldTopAb 0
              THEN ParallelOp -3
              THEN Auto
              THEN Try (((InstHyp [⌜e'⌝] (-7)⋅ THENA Auto)
                         THEN RWW "eo-forward-forward" (-1)
                         THEN RWW "eo-forward-forward" 0
                         THEN Auto)))}⋅
   ) }

1
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)

2
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)

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[start:E].  \mforall{}[e1:E].  \mforall{}[e:E].
    uiff((no  X  between  e1  and  e);(no  X  between  e1  and  e))  supposing  (loc(e)  =  loc(e1))  \mwedge{}  (loc(e1)  =  lo\000Cc(start))


By

---

Latex:
((Auto
    THEN  Auto
    THEN  (Assert  e1  \mleq{}loc  e    BY
                            (BLemma  `eo-forward-E-member`  THEN  Auto))
    THEN  (Assert  start  \mleq{}loc  e1    BY
                            (BLemma  `eo-forward-E-member`  THEN  Auto))
    THEN  Try  ((RelRST  THEN  Auto)\mcdot{}))
  THEN  skip\{(UnfoldTopAb  (-3)
                        THEN  UnfoldTopAb  0
                        THEN  ParallelOp  -3
                        THEN  Auto
                        THEN  Try  (((InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  (-7)\mcdot{}  THENA  Auto)
                                              THEN  RWW  "eo-forward-forward"  (-1)
                                              THEN  RWW  "eo-forward-forward"  0
                                              THEN  Auto)))\}\mcdot{}
  )

---

Home Index