Nuprl Lemma : member-eo-forward-E

[Info:Type]. ∀[eo:EO+(Info)]. ∀[e,e':E].  e' ∈ supposing (loc(e') loc(e) ∈ Id)  e ≤loc e' 


Proof




Definitions occuring in Statement :  eo-forward: eo.e event-ordering+: EO+(Info) es-le: e ≤loc e'  es-loc: loc(e) es-E: E Id: Id uimplies: supposing a uall: [x:A]. B[x] implies:  Q member: t ∈ T universe: Type equal: t ∈ T
Lemmas :  Id_wf es-loc_wf event-ordering+_subtype es-le_wf es-E_wf event-ordering+_wf eo-forward-E-subtype2
\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e,e':E].    e'  \mmember{}  E  supposing  (loc(e')  =  loc(e))  {}\mRightarrow{}  e  \mleq{}loc  e' 



Date html generated: 2015_07_17-PM-00_02_45
Last ObjectModification: 2015_01_28-AM-00_31_45

Home Index