Nuprl Lemma : es-E-interface-conditional-subtype2

[Info:Type]. ∀[es:EO+(Info)]. ∀[X,Y:EClass(Top)].  (E(Y) ⊆E([X?Y]))


Proof




Definitions occuring in Statement :  es-E-interface: E(X) cond-class: [X?Y] eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) subtype_rel: A ⊆B uall: [x:A]. B[x] top: Top universe: Type
Lemmas :  cond-class-subtype2 top_wf eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X,Y:EClass(Top)].    (E(Y)  \msubseteq{}r  E([X?Y]))



Date html generated: 2015_07_17-PM-00_57_26
Last ObjectModification: 2015_01_27-PM-10_45_38

Home Index