Nuprl Lemma : eo-strict-forward_wf

[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E].  (eo>e ∈ EO+(Info))


Proof




Definitions occuring in Statement :  eo-strict-forward: eo>e event-ordering+: EO+(Info) es-E: E uall: [x:A]. B[x] member: t ∈ T universe: Type
Lemmas :  eo-restrict_wf_extended bor_wf es-bless_wf bnot_wf eq_id_wf es-loc_wf es-E_wf event-ordering+_subtype event-ordering+_wf
\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].    (eo>e  \mmember{}  EO+(Info))



Date html generated: 2015_07_17-PM-00_06_54
Last ObjectModification: 2015_01_28-AM-00_11_41

Home Index