---

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


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)
BY
{ (Unfold `es-le-before` 0 THEN (RWO "filter_append" 0 THENA Auto)) }

1
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)

---

Latex:



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


By

(Unfold  `es-le-before`  0  THEN  (RWO  "filter\_append"  0  THENA  Auto))

---

Home Index