Nuprl Lemma : es-before-partition

[es:EO].

[e,e':E]. before(e) = (

loc(e') @ (e', e)) supposing (e' <loc e)

Proof not projected

Definitions occuring in Statement : es-open-interval: (e, e'), es-le-before:

loc(e), es-before: before(e), es-locl: (e <loc e'), es-E: E, event_ordering: EO, append: as @ bs, uimplies: b supposing a, uall:

[x:A]. B[x], list: type List, equal: s = t
Definitions : uall:

[x:A]. B[x], uimplies: b supposing a, member: t

T, all:

x:A. B[x], implies: P

Q, prop:

Lemmas : es-le-before-partition, es-le_weakening, es-locl_wf, es-E_wf, event_ordering_wf

\mforall{}[es:EO]. \mforall{}[e,e':E]. before(e) = (\mleq{}loc(e') @ (e', e)) supposing (e' <loc e) Date html generated: 2012_01_23-PM-12_11_13 Last ObjectModification: 2011_12_13-AM-10_31_21 Home Index