Nuprl Lemma : es-direct-prior-no-es-locl
[es:EO]. [e:E]. e1,e2:E. (e1 
es-direct-prior(es;e) 
e2 es-direct-prior(es;e) (
(e1 <loc e2)))
Proof not projected
Definitions occuring in Statement :
es-direct-prior: es-direct-prior(es;e),
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
uall: [x:A]. B[x],
all: x:A. B[x],
not: A,
implies: P Q,
bag-member: x bs
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
es-direct-prior: es-direct-prior(es;e),
not: A,
member: t T,
false: False,
uiff: uiff(P;Q),
and: P 
Q,
so_lambda: 
x.t[x],
bag-maximals: bag-maximals(bg;R),
uimplies: b supposing a,
so_apply: x[s],
iff: P 
Q,
prop: 
,
guard: {T},
subtype: S 
T
Lemmas :
bag-member-remove-repeats,
bag-maximals-max,
es-E_wf,
bag-member-filter,
bag-maximal?_wf,
assert_of_bnot,
es-blocl_wf,
not_functionality_wrt_iff,
assert_wf,
es-locl_wf,
es-blocl-iff,
bag-member_wf,
bag-remove-repeats_wf,
es-eq_wf,
bag-maximals_wf,
es-pred-list_wf,
bag_qinc,
bnot_wf,
event_ordering_wf
\mforall{}[es:EO]. \mforall{}[e:E].
\mforall{}e1,e2:E. (e1 \mdownarrow{}\mmember{} es-direct-prior(es;e) {}\mRightarrow{} e2 \mdownarrow{}\mmember{} es-direct-prior(es;e) {}\mRightarrow{} (\mneg{}(e1 <loc e2)))
Date html generated:
2012_01_23-PM-12_08_43
Last ObjectModification:
2011_11_29-PM-08_01_39
Home
Index