---

Step * of Lemma es-open-interval-nil

∀[es:EO]. ∀[e,e':E].  (e, e') ~ [] supposing (↑first(e')) ∨ ((¬↑first(e')) ∧ pred(e') ≤loc e )
BY
{ (Auto
   THEN (Unfold `es-open-interval` 0
         THEN RWO "filter_is_nil" 0
         THEN Auto
         THEN (BLemma `l_all_iff` THEN Auto)
         THEN Reduce 0
         THEN (D 0 THENA Auto)
         THEN (RWO "assert-es-bless" (-1) THENA Auto))⋅
   ) }

1
1. es : EO
2. e : E
3. e' : E
4. (↑first(e')) ∨ ((¬↑first(e')) ∧ pred(e') ≤loc e )
5. x : E@i
6. (x ∈ before(e'))@i
7. (e <loc x)
⊢ False

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    (e,  e')  \msim{}  []  supposing  (\muparrow{}first(e'))  \mvee{}  ((\mneg{}\muparrow{}first(e'))  \mwedge{}  pred(e')  \mleq{}loc  e  )


By

(Auto
  THEN  (Unfold  `es-open-interval`  0
              THEN  RWO  "filter\_is\_nil"  0
              THEN  Auto
              THEN  (BLemma  `l\_all\_iff`  THEN  Auto)
              THEN  Reduce  0
              THEN  (D  0  THENA  Auto)
              THEN  (RWO  "assert-es-bless"  (-1)  THENA  Auto))\mcdot{}
  )

---

Home Index