Nuprl Lemma : es-interval-sorted-by

es:EO. ∀e1,e2:E.  sorted-by(λe1,e2. (e1 <loc e2);[e1, e2])


Proof




Definitions occuring in Statement :  es-interval: [e, e'] es-locl: (e <loc e') es-E: E event_ordering: EO sorted-by: sorted-by(R;L) all: x:A. B[x] lambda: λx.A[x]
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] iff: ⇐⇒ Q and: P ∧ Q implies:  Q l-ordered: l-ordered(T;x,y.R[x; y];L) prop:

Latex:
\mforall{}es:EO.  \mforall{}e1,e2:E.    sorted-by(\mlambda{}e1,e2.  (e1  <loc  e2);[e1,  e2])



Date html generated: 2016_05_16-AM-09_36_00
Last ObjectModification: 2015_12_28-PM-09_44_59

Theory : new!event-ordering


Home Index