---

Step * 1 1 of Lemma eo-forward-le-before


1. Info : Type
2. es : EO+(Info)
3. e : E
4. b : E
5. b ≤loc e 
⊢ (before(e) @ [e]) = (filter(λa.b ≤loc a;before(e)) @ filter(λa.b ≤loc a;[e])) ∈ (E List)
BY
{ ((Reduce 0 THEN AutoSplit) THEN EqCD THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e  :  E
4.  b  :  E
5.  b  \mleq{}loc  e 
\mvdash{}  (before(e)  @  [e])  =  (filter(\mlambda{}a.b  \mleq{}loc  a;before(e))  @  filter(\mlambda{}a.b  \mleq{}loc  a;[e]))


By

((Reduce  0  THEN  AutoSplit)  THEN  EqCD  THEN  Auto)

---

Home Index