---

Step * 1 of Lemma es-le-before-filter

.....assertion..... 
1. es : EO@i'
2. e : E@i
3. b : E@i
4. b ≤loc e @i
⊢ ≤loc(b) = filter(λa.a ≤loc b;≤loc(e)) ∈ (E List)
BY
{ ((MoveToConcl (-1) THEN MoveToConcl (-2)) THEN CausalInd' THEN Auto) }

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

---

Latex:


.....assertion..... 
1.  es  :  EO@i'
2.  e  :  E@i
3.  b  :  E@i
4.  b  \mleq{}loc  e  @i
\mvdash{}  \mleq{}loc(b)  =  filter(\mlambda{}a.a  \mleq{}loc  b;\mleq{}loc(e))


By

((MoveToConcl  (-1)  THEN  MoveToConcl  (-2))  THEN  CausalInd'  THEN  Auto)

---

Home Index