Nuprl Lemma : member-es-pred-list-base
es:EO. e,e':es-base-E(es). ((e' 
es-pred-list(es;e)) 
(e' < e) 
(
(es-dom(es) e')))
Proof not projected
Definitions occuring in Statement :
es-pred-list: es-pred-list(es;e),
es-causl: (e < e'),
es-dom: es-dom(es),
es-base-E: es-base-E(es),
event_ordering: EO,
assert: b,
all: x:A. B[x],
iff: P Q,
and: P Q,
apply: f a,
l_member: (x l)
Definitions :
member: t T,
es-pred-list: es-pred-list(es;e),
all: x:A. B[x],
rev_implies: P Q,
iff: P Q,
implies: P Q,
and: P Q,
uall: [x:A]. B[x],
prop: 
Lemmas :
event_ordering_wf,
es-base-E_wf,
member_filter,
iff_functionality_wrt_iff,
assert_wf,
and_wf,
es-causl-wf-base
\mforall{}es:EO. \mforall{}e,e':es-base-E(es). ((e' \mmember{} es-pred-list(es;e)) \mLeftarrow{}{}\mRightarrow{} (e' < e) \mwedge{} (\muparrow{}(es-dom(es) e')))
Date html generated:
2012_01_23-PM-12_08_06
Last ObjectModification:
2011_12_13-AM-10_32_46
Home
Index