Nuprl Lemma : iseg-es-before
∀es:EO. ∀e',e:E. ((e' <loc e) ⇒ ≤loc(e') ≤ before(e))
Proof
Definitions occuring in Statement :
es-le-before: ≤loc(e),
es-before: before(e),
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
iseg: l1 ≤ l2,
all: ∀x:A. B[x],
implies: P ⇒ Q
Lemmas :
es-before-decomp,
es-locl_wf,
es-E_wf,
event_ordering_wf,
member-es-before,
equal_wf,
list_wf,
append_wf,
es-le-before_wf2,
subtype_rel_list,
es-le_wf,
append_assoc
\mforall{}es:EO. \mforall{}e',e:E. ((e' <loc e) {}\mRightarrow{} \mleq{}loc(e') \mleq{} before(e))
Date html generated:
2015_07_17-AM-08_44_15
Last ObjectModification:
2015_01_27-PM-02_28_50
Home
Index