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