---

Step * 1 of Lemma eo-forward-before


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

1
1. Info : Type
2. es : EO+(Info)
3. e : E@i
4. ∀e1:E. ((e1 < e) ⇒ (∀b:E. (b ≤loc e1  ⇒ (before(e1) = filter(λa.b ≤loc a;before(e1)) ∈ (E List)))))
5. b : E@i
6. b ≤loc e @i
⊢ before(e) = filter(λa.b ≤loc a;before(e)) ∈ (E List)

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
\mvdash{}  \mforall{}e,b:E.    (b  \mleq{}loc  e    {}\mRightarrow{}  (before(e)  =  filter(\mlambda{}a.b  \mleq{}loc  a;before(e))))


By

(CausalInd'  THEN  Auto)

---

Home Index