---

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


1. es : EO@i'
2. e' : E@i
3. a : E@i
4. ∀a1:E
     ((a1 < a)
     ⇒ e' ≤loc a1 
     ⇒ (filter(λev.e' ≤loc ev;before(a1) @ [a1]) = [e' / filter(λev.e' <loc ev;before(a1) @ [a1])] ∈ (E List)))
5. e' ≤loc a @i
6. ¬↑first(a)
7. e' ≤loc a 
8. ¬(e' <loc a)
⊢ (filter(λev.e' ≤loc ev;before(pred(a)) @ [pred(a)]) @ [a])
= [e' / (filter(λev.e' <loc ev;before(pred(a)) @ [pred(a)]) @ [])]
∈ (E List)
BY
{ Subst' filter(λev.e' ≤loc ev;before(pred(a)) @ [pred(a)]) ~ [] 0 }

1
.....equality..... 
1. es : EO@i'
2. e' : E@i
3. a : E@i
4. ∀a1:E
     ((a1 < a)
     ⇒ e' ≤loc a1 
     ⇒ (filter(λev.e' ≤loc ev;before(a1) @ [a1]) = [e' / filter(λev.e' <loc ev;before(a1) @ [a1])] ∈ (E List)))
5. e' ≤loc a @i
6. ¬↑first(a)
7. e' ≤loc a 
8. ¬(e' <loc a)
⊢ filter(λev.e' ≤loc ev;before(pred(a)) @ [pred(a)]) ~ []

2
1. es : EO@i'
2. e' : E@i
3. a : E@i
4. ∀a1:E
     ((a1 < a)
     ⇒ e' ≤loc a1 
     ⇒ (filter(λev.e' ≤loc ev;before(a1) @ [a1]) = [e' / filter(λev.e' <loc ev;before(a1) @ [a1])] ∈ (E List)))
5. e' ≤loc a @i
6. ¬↑first(a)
7. e' ≤loc a 
8. ¬(e' <loc a)
⊢ ([] @ [a]) = [e' / (filter(λev.e' <loc ev;before(pred(a)) @ [pred(a)]) @ [])] ∈ (E List)

---

Latex:



1.  es  :  EO@i'
2.  e'  :  E@i
3.  a  :  E@i
4.  \mforall{}a1:E
          ((a1  <  a)
          {}\mRightarrow{}  e'  \mleq{}loc  a1 
          {}\mRightarrow{}  (filter(\mlambda{}ev.e'  \mleq{}loc  ev;before(a1)  @  [a1])
                =  [e'  /  filter(\mlambda{}ev.e'  <loc  ev;before(a1)  @  [a1])]))
5.  e'  \mleq{}loc  a  @i
6.  \mneg{}\muparrow{}first(a)
7.  e'  \mleq{}loc  a 
8.  \mneg{}(e'  <loc  a)
\mvdash{}  (filter(\mlambda{}ev.e'  \mleq{}loc  ev;before(pred(a))  @  [pred(a)])  @  [a])
=  [e'  /  (filter(\mlambda{}ev.e'  <loc  ev;before(pred(a))  @  [pred(a)])  @  [])]


By

Subst'  filter(\mlambda{}ev.e'  \mleq{}loc  ev;before(pred(a))  @  [pred(a)])  \msim{}  []  0

---

Home Index