Nuprl Lemma : es-interval-iseg
∀es:EO. ∀e3,e2,e1:E. (e1 ≤loc e2 ⇒ e1 ≤loc e3 ⇒ ([e1, e2] ≤ [e1, e3] ⇐⇒ e2 ≤loc e3 ))
Proof
Definitions occuring in Statement :
es-interval: [e, e'],
es-le: e ≤loc e' ,
es-E: E,
event_ordering: EO,
iseg: l1 ≤ l2,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
implies: P ⇒ Q
Lemmas :
all_wf,
es-E_wf,
es-le_wf,
iff_wf,
iseg_wf,
es-interval_wf,
es-locl_wf,
es-le-iff,
es-pred_wf,
es-pred-locl,
es-interval-less,
es-locl_transitivity1,
es-le-pred,
or_wf,
equal_wf,
iseg_append_single,
list_wf,
iff_weakening_equal,
es-le_weakening,
es-interval-one-one,
es-interval-eq,
cons_wf,
nil_wf,
es-causle_antisymmetry,
es-causle_weakening_locl,
es-le-self,
and_wf,
es-le-not-locl,
es-le-loc,
member-es-interval,
iseg_member,
member_singleton,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity,
iseg_weakening
\mforall{}es:EO. \mforall{}e3,e2,e1:E. (e1 \mleq{}loc e2 {}\mRightarrow{} e1 \mleq{}loc e3 {}\mRightarrow{} ([e1, e2] \mleq{} [e1, e3] \mLeftarrow{}{}\mRightarrow{} e2 \mleq{}loc e3 ))
Date html generated:
2015_07_17-AM-08_42_33
Last ObjectModification:
2015_02_04-AM-07_08_26
Home
Index