Nuprl Lemma : es-first-le

es:EO. ∀e,e':E.  (e ≤loc e' supposing ((loc(e) loc(e') ∈ Id) and (↑first(e)))


Definitions occuring in Statement :  es-le: e ≤loc e'  es-first: first(e) es-loc: loc(e) es-E: E event_ordering: EO Id: Id assert: b uimplies: supposing a all: x:A. B[x] equal: t ∈ T
Lemmas :  assert_witness es-first_wf2 es-first-implies equal_wf Id_wf es-loc_wf assert_wf es-E_wf event_ordering_wf es-le-not-locl
\mforall{}es:EO.  \mforall{}e,e':E.    (e  \mleq{}loc  e'  )  supposing  ((loc(e)  =  loc(e'))  and  (\muparrow{}first(e)))

Date html generated: 2015_07_17-AM-08_38_55
Last ObjectModification: 2015_01_27-PM-02_41_50

Home Index