---

Step * 1 of Lemma es-interval-non-zero


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. e ≤loc e' @i
⊢ 0 < ||[e, e']||
BY
{ ((InstLemma `pos_length` [⌈E⌉; ⌈[e, e']⌉])⋅ THEN Auto) }

1
.....antecedent..... 
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. e ≤loc e' @i
⊢ ¬([e, e'] = [] ∈ (E List))

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  e  \mleq{}loc  e'  @i
\mvdash{}  0  <  ||[e,  e']||


By

((InstLemma  `pos\_length`  [\mkleeneopen{}E\mkleeneclose{};  \mkleeneopen{}[e,  e']\mkleeneclose{}])\mcdot{}  THEN  Auto)

---

Home Index