Nuprl Lemma : assert-es-ble-base
es:EO. e,e':es-base-E(es). (
e 
loc e' 
(((es-dom(es) e)) 
(loc(e) = loc(e')) (e < e')) 
(e = e'))
Proof not projected
Definitions occuring in Statement :
es-ble: e loc e',
es-causl: (e < e'),
es-loc: loc(e),
es-dom: es-dom(es),
es-base-E: es-base-E(es),
event_ordering: EO,
Id: Id,
assert: b,
all: x:A. B[x],
iff: P Q,
or: P Q,
and: P Q,
apply: f a,
equal: s = t
Definitions :
member: t 
T,
reduce: reduce(f;k;as),
filter: filter(P;l),
es-ble: e loc e',
all: x:A. B[x],
implies: P Q,
rev_implies: P Q,
iff: P Q,
and: P Q,
or: P Q,
uall: [x:A]. B[x],
prop: 
Lemmas :
event_ordering_wf,
es-base-E_wf,
es-causl-wf-base,
es-pred-list-wf-base,
es-loc-wf-base,
es-eq-wf-base,
assert-deq-member,
iff_functionality_wrt_iff,
Id_wf,
equal_wf,
es-dom_wf,
assert_wf,
and_wf,
or_wf
\mforall{}es:EO. \mforall{}e,e':es-base-E(es).
(\muparrow{}e \mleq{}loc e' \mLeftarrow{}{}\mRightarrow{} ((\muparrow{}(es-dom(es) e)) \mwedge{} (loc(e) = loc(e')) \mwedge{} (e < e')) \mvee{} (e = e'))
Date html generated:
2012_01_23-PM-12_09_51
Last ObjectModification:
2011_12_13-AM-10_32_26
Home
Index