---

Step * of Lemma member-interface-predecessors

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E. ∀e':E(X).  ((e' ∈ ≤(X)(e)) ⇐⇒ e' ≤loc e )
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN CausalInd') }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E@i
5. ∀e1:E. ((e1 < e) ⇒ (∀e':E(X). ((e' ∈ ≤(X)(e1)) ⇐⇒ e' ≤loc e1 )))
⊢ ∀e':E(X). ((e' ∈ ≤(X)(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))  \mLeftarrow{}{}\mRightarrow{}  e'  \mleq{}loc  e  )


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  CausalInd')

---

Home Index