---

Step * 1 1 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)
⊢ e' ≤loc e 
⇒ (filter(λev.e' ≤loc ev;(before(pred(e)) @ [pred(e)]) @ [e])
   = (if e' <loc e then [e'] else [] fi  @ filter(λev.e' <loc ev;before(pred(e)) @ [pred(e)]) @ [e])
   ∈ (E List))
BY
{ ((D 0 THENA Auto)
   THEN Fold `es-le-before` 0
   THEN (RWO "filter_append_sq" 0 THENA Auto)
   THEN Reduce 0
   THEN OldAutoSplit
   THEN Try ((D (-1) THEN Complete (Auto)))
   THEN (RWO "append_assoc_sq<" 0 THENA Auto)
   THEN (EqCD THEN Auto)
   THEN Try (Trivial)
   THEN Thin (-1)) }

1
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' ≤loc e @i
⊢ filter(λev.e' ≤loc ev;≤loc(pred(e)))
= (if e' <loc e then [e'] else [] fi  @ filter(λev.e' <loc ev;≤loc(pred(e))))
∈ (E List)

---

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)
\mvdash{}  e'  \mleq{}loc  e 
{}\mRightarrow{}  (filter(\mlambda{}ev.e'  \mleq{}loc  ev;(before(pred(e))  @  [pred(e)])  @  [e])
      =  (if  e'  <loc  e  then  [e']  else  []  fi 
          @  filter(\mlambda{}ev.e'  <loc  ev;before(pred(e))  @  [pred(e)])
          @  [e]))


By

((D  0  THENA  Auto)
  THEN  Fold  `es-le-before`  0
  THEN  (RWO  "filter\_append\_sq"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  OldAutoSplit
  THEN  Try  ((D  (-1)  THEN  Complete  (Auto)))
  THEN  (RWO  "append\_assoc\_sq<"  0  THENA  Auto)
  THEN  (EqCD  THEN  Auto)
  THEN  Try  (Trivial)
  THEN  Thin  (-1))

---

Home Index