---

Step * of Lemma member-interface-predecessors2

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E. ∀e':E(X).  ((e' ∈ ≤(X)(e)) ⇒ e' ≤loc e )
BY
{ (Auto THEN RepUR ``es-interface-predecessors eclass-events`` -1 THEN Assert ⌜(e' ∈ filter(λe.e ∈b X;≤loc(e)))⌝⋅) }

1
.....assertion..... 
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E@i
5. e' : E(X)@i
6. (e' ∈ filter(λe.e ∈b X;≤loc(e)))@i
⊢ (e' ∈ filter(λe.e ∈b X;≤loc(e)))

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E@i
5. e' : E(X)@i
6. (e' ∈ filter(λe.e ∈b X;≤loc(e)))@i
7. (e' ∈ filter(λe.e ∈b X;≤loc(e)))
⊢ e' ≤loc e 

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.  \mforall{}e':E(X).    ((e'  \mmember{}  \mleq{}(X)(e))  {}\mRightarrow{}  e'  \mleq{}loc  e  )


By

---

Latex:
(Auto
  THEN  RepUR  ``es-interface-predecessors  eclass-events``  -1
  THEN  Assert  \mkleeneopen{}(e'  \mmember{}  filter(\mlambda{}e.e  \mmember{}\msubb{}  X;\mleq{}loc(e)))\mkleeneclose{}\mcdot{})

---

Home Index