---

Step * of Lemma eo-forward-before

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

1
1. Info : Type
2. es : EO+(Info)
⊢ ∀e,b:E.  (b ≤loc e  ⇒ (before(e) = filter(λa.b ≤loc a;before(e)) ∈ (E List)))

---

Latex:


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


By

(Auto  THEN  RepeatFor  3  (MoveToConcl  (-1)))

---

Home Index