---

Step * of Lemma member-interface-predecessors-subtype

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E(X). ∀e':{a:E(X)| loc(a) = loc(e) ∈ Id} .  ((e' ∈ ≤(X)(e)) ⇐⇒ e' ≤loc e )
BY
{ (InstLemma `member-interface-predecessors` [] THEN RepeatFor 4 (ParallelLast') THEN RWO "-1<" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `member-interface-predecessors`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index