---

Step * of Lemma eo-forward-le-before

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e,b:E].  ≤loc(e) = filter(λa.b ≤loc a;≤loc(e)) ∈ (E List) supposing b ≤loc e 
BY
{ Auto }

1
1. Info : Type
2. es : EO+(Info)
3. e : E
4. b : E
5. b ≤loc e 
⊢ ≤loc(e) = filter(λa.b ≤loc a;≤loc(e)) ∈ (E List)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e,b:E].    \mleq{}loc(e)  =  filter(\mlambda{}a.b  \mleq{}loc  a;\mleq{}loc(e))  supposing  b  \mleq{}loc  e 


By

Auto

---

Home Index