---

Step * of Lemma es-open-interval-ordered

∀es:EO. ∀e1,e2:E.  l-ordered(E;e1,e2.(e1 <loc e2);(e1, e2))
BY
{ (Auto
   THEN Unfold `l-ordered` 0
   THEN Auto
   THEN RenameVar `e3' (-3)
   THEN RenameVar `e4' (-2)
   THEN Unfold `es-open-interval` (-1)
   THEN (RWO "l_before_filter" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN RW assert_pushdownC (-1)
   THEN Auto
   THEN FLemma `l_before-es-before` [-1]
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e1,e2:E.    l-ordered(E;e1,e2.(e1  <loc  e2);(e1,  e2))


By

(Auto
  THEN  Unfold  `l-ordered`  0
  THEN  Auto
  THEN  RenameVar  `e3'  (-3)
  THEN  RenameVar  `e4'  (-2)
  THEN  Unfold  `es-open-interval`  (-1)
  THEN  (RWO  "l\_before\_filter"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto
  THEN  FLemma  `l\_before-es-before`  [-1]
  THEN  Auto)

---

Home Index