---

Step * of Lemma es-le-before-filter

∀es:EO. ∀e,b:E.  (b ≤loc e  ⇒ (≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ ({a:E| a ≤loc b }  List)))
BY
{ (Auto THEN Assert ⌈≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ (E List)⌉⋅) }

1
.....assertion..... 
1. es : EO@i'
2. e : E@i
3. b : E@i
4. b ≤loc e @i
⊢ ≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ (E 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)
⊢ ≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ ({a:E| a ≤loc b }  List)

---

Latex:


\mforall{}es:EO.  \mforall{}e,b:E.    (b  \mleq{}loc  e    {}\mRightarrow{}  (\mleq{}loc(b)  =  filter(\mlambda{}a.a  \mleq{}loc  b;\mleq{}loc(e))))


By

(Auto  THEN  Assert  \mkleeneopen{}\mleq{}loc(b)  =  filter(\mlambda{}a.a  \mleq{}loc  b;\mleq{}loc(e))\mkleeneclose{}\mcdot{})

---

Home Index