---

Step * of Lemma es-interface-predecessors-iseg

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

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E(X)@i
5. ∀e1:E(X). ((e1 < e) ⇒ (∀e':E(X). (≤(X)(e') ≤ ≤(X)(e1) ⇐⇒ e' ≤loc e1 )))
6. e' : E(X)@i
⊢ ≤(X)(e') ≤ ≤(X)(e) ⇐⇒ e' ≤loc e 

---

Latex:

---

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


By

---

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

---

Home Index