---

Step * 1 1 of Lemma es-hist-iseg


1. [Info] : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. e : E@i
6. loc(e2) = loc(e1) ∈ Id
7. e ≤loc e2 @i
8. e1 ≤loc e 
⊢ [e1, e] ≤ [e1, e2]
BY
{ ((InstLemma `es-interval-iseg` [⌜es⌝; ⌜e2⌝; ⌜e⌝; ⌜e1⌝])⋅ THENA Auto) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. e : E@i
6. loc(e2) = loc(e1) ∈ Id
7. e ≤loc e2 @i
8. e1 ≤loc e 
9. [e1, e] ≤ [e1, e2] ⇐⇒ e ≤loc e2 
⊢ [e1, e] ≤ [e1, e2]

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  e1  :  E@i
4.  e2  :  E@i
5.  e  :  E@i
6.  loc(e2)  =  loc(e1)
7.  e  \mleq{}loc  e2  @i
8.  e1  \mleq{}loc  e 
\mvdash{}  [e1,  e]  \mleq{}  [e1,  e2]


By

---

Latex:
((InstLemma  `es-interval-iseg`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e2\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}e1\mkleeneclose{}])\mcdot{}  THENA  Auto)

---

Home Index