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 not projected
Definitions occuring in Statement :
es-interval: [e, e'],
es-le: e loc e' ,
es-E: E,
event_ordering: EO,
all: x:A. B[x],
iff: P Q,
implies: P Q,
iseg: l1 l2
Definitions :
member: t 
T,
prop: 
,
all: x:A. B[x],
implies: P Q,
so_lambda: 
x.t[x],
and: P 
Q,
rev_implies: P Q,
iff: P Q,
es-le: e loc e' ,
or: P 
Q,
guard: {T},
cand: A c B,
true: True,
squash: 
T,
not: 
A,
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
false: False
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-le-pred,
or_functionality_wrt_iff,
iff_functionality_wrt_iff,
iseg_append_single,
es-locl_transitivity1,
es-interval-one-one,
es-interval-eq,
true_wf,
squash_wf,
es-le_antisymmetry,
es-le-loc,
es-le-not-locl,
member-es-interval,
member_singleton,
iseg_member,
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:
2012_01_23-PM-12_10_08
Last ObjectModification:
2011_12_13-AM-10_32_11
Home
Index