Nuprl Lemma : es-prior-interface-causl

[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.  (prior(X)(e) < e) supposing ↑e ∈b prior(X)


Proof




Definitions occuring in Statement :  es-prior-interface: prior(X) eclass-val: X(e) in-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-causl: (e < e') es-E: E assert: b uimplies: supposing a uall: [x:A]. B[x] top: Top all: x:A. B[x] universe: Type
Lemmas :  es-prior-interface-locl es-causl_weakening eclass-val_wf2 es-prior-interface_wf es-E-interface_wf assert_wf in-eclass_wf es-prior-interface_wf0 es-interface-subtype_rel2 es-E_wf event-ordering+_subtype event-ordering+_wf top_wf subtype_top eclass_wf

Latex:
\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.    (prior(X)(e)  <  e)  supposing  \muparrow{}e  \mmember{}\msubb{}  prior(X)



Date html generated: 2015_07_21-PM-02_47_43
Last ObjectModification: 2015_01_27-PM-07_33_37

Home Index