---

Step * of Lemma es-closed-open-interval-forward

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2,e:E].  ([e1;e2) = [e1;e2) ∈ (E List)) supposing (e ≤loc e1  and e1 ≤loc e2 )
BY
{ (Auto
   THEN (RWO "es-closed-open-interval-eq-before" 0 THENA Auto)
   THEN (InstLemma `eo-forward-forward` [⌈Info⌉;⌈es⌉;⌈e⌉;⌈e1⌉]⋅ THENA Auto)) }

1
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e : E
6. e1 ≤loc e2 
7. e ≤loc e1 
8. es.e.e1 = es.e1 ∈ EO+(Info)
⊢ before(e2) = before(e2) ∈ (E List)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2,e:E].
    ([e1;e2)  =  [e1;e2))  supposing  (e  \mleq{}loc  e1    and  e1  \mleq{}loc  e2  )


By

(Auto
  THEN  (RWO  "es-closed-open-interval-eq-before"  0  THENA  Auto)
  THEN  (InstLemma  `eo-forward-forward`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index