---

Step * 1 of Lemma es-E-interface_functionality-iff


1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. Y : EClass(Top)
5. {e:E| ↑e ∈b X}  ⊆r {e:E| ↑e ∈b Y} 
6. e : E
7. ↑e ∈b X
⊢ ↑e ∈b Y
BY
{ (GenConcl ⌈e = a ∈ {e:E| ↑e ∈b Y} ⌉⋅ THEN Auto THEN SubsumeC ⌈{e:E| ↑e ∈b X} ⌉⋅ THEN Auto)⋅ }

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  Y  :  EClass(Top)
5.  \{e:E|  \muparrow{}e  \mmember{}\msubb{}  X\}    \msubseteq{}r  \{e:E|  \muparrow{}e  \mmember{}\msubb{}  Y\} 
6.  e  :  E
7.  \muparrow{}e  \mmember{}\msubb{}  X
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  Y


By

(GenConcl  \mkleeneopen{}e  =  a\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  SubsumeC  \mkleeneopen{}\{e:E|  \muparrow{}e  \mmember{}\msubb{}  X\}  \mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index