---

Step * 1 1 1 1 3 1 of Lemma es-interval-open-interval


1. es : EO@i'
2. e : E@i
3. ∀e1:E
     ((e1 < e)
     ⇒ (∀e':E. (e' ≤loc e1  ⇒ ([e', e1] = (if e' <loc e1 then [e'] else [] fi  @ (e', e1) @ [e1]) ∈ (E List)))))
4. e' : E@i
5. ¬↑first(e)
6. e' = e ∈ E
7. ¬(e' <loc e)
⊢ filter(λev.e ≤loc ev;≤loc(pred(e))) = filter(λev.e <loc ev;≤loc(pred(e))) ∈ (E List)
BY
{ ((Assert ≤loc(pred(e)) ∈ E List BY
          Auto)
   THEN (RWO "filter_is_nil" 0 THEN Auto)
   THEN (BLemma `l_all_iff` THENM Reduce 0)
   THEN Auto
   THEN (RWO "assert-es-bless assert-es-ble" 0 THENA Auto)
   THEN (RWO "member-es-le-before" (-1) THENA Auto)
   THEN ParallelOp (-4)
   THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  (\mforall{}e':E
                      (e'  \mleq{}loc  e1    {}\mRightarrow{}  ([e',  e1]  =  (if  e'  <loc  e1  then  [e']  else  []  fi    @  (e',  e1)  @  [e1])))))
4.  e'  :  E@i
5.  \mneg{}\muparrow{}first(e)
6.  e'  =  e
7.  \mneg{}(e'  <loc  e)
\mvdash{}  filter(\mlambda{}ev.e  \mleq{}loc  ev;\mleq{}loc(pred(e)))  =  filter(\mlambda{}ev.e  <loc  ev;\mleq{}loc(pred(e)))


By

((Assert  \mleq{}loc(pred(e))  \mmember{}  E  List  BY
                Auto)
  THEN  (RWO  "filter\_is\_nil"  0  THEN  Auto)
  THEN  (BLemma  `l\_all\_iff`  THENM  Reduce  0)
  THEN  Auto
  THEN  (RWO  "assert-es-bless  assert-es-ble"  0  THENA  Auto)
  THEN  (RWO  "member-es-le-before"  (-1)  THENA  Auto)
  THEN  ParallelOp  (-4)
  THEN  Auto)

---

Home Index