---

Step * of Lemma es-interface-predecessors-sorted-by-locl

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.  sorted-by(λx,y. (x <loc y);≤(X)(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) ⇒ sorted-by(λx,y. (x <loc y);≤(X)(e1)))
⊢ sorted-by(λx,y. (x <loc y);≤(X)(e))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.    sorted-by(\mlambda{}x,y.  (x  <loc  y);\mleq{}(X)(e))


By

---

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

---

Home Index