---

Step * 2 of Lemma es-le-before-filter


1. es : EO@i'
2. e : E@i
3. b : E@i
4. b ≤loc e @i
5. ≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ (E List)
⊢ ≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ ({a:E| a ≤loc b }  List)
BY
{ Assert ⌈filter(λa.a ≤loc b;≤loc(e)) ∈ {a:E| a ≤loc b }  List⌉⋅ }

1
.....assertion..... 
1. es : EO@i'
2. e : E@i
3. b : E@i
4. b ≤loc e @i
5. ≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ (E List)
⊢ filter(λa.a ≤loc b;≤loc(e)) ∈ {a:E| a ≤loc b }  List

2
1. es : EO@i'
2. e : E@i
3. b : E@i
4. b ≤loc e @i
5. ≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ (E List)
6. filter(λa.a ≤loc b;≤loc(e)) ∈ {a:E| a ≤loc b }  List
⊢ ≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ ({a:E| a ≤loc b }  List)

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  b  :  E@i
4.  b  \mleq{}loc  e  @i
5.  \mleq{}loc(b)  =  filter(\mlambda{}a.a  \mleq{}loc  b;\mleq{}loc(e))
\mvdash{}  \mleq{}loc(b)  =  filter(\mlambda{}a.a  \mleq{}loc  b;\mleq{}loc(e))


By

Assert  \mkleeneopen{}filter(\mlambda{}a.a  \mleq{}loc  b;\mleq{}loc(e))  \mmember{}  \{a:E|  a  \mleq{}loc  b  \}    List\mkleeneclose{}\mcdot{}

---

Home Index