Nuprl Lemma : es-le-before-filter
es:EO. e,b:E. (b 
loc e 
(loc(b) = filter(
a.a loc b;loc(e))))
Proof not projected
Definitions occuring in Statement :
es-le-before: loc(e),
es-ble: e loc e',
es-le: e loc e' ,
es-E: E,
event_ordering: EO,
all: x:A. B[x],
implies: P Q,
set: {x:A| B[x]} ,
lambda: x.A[x],
list: type List,
equal: s = t,
filter: filter(P;l)
Definitions :
member: t 
T,
implies: P Q,
all: x:A. B[x],
prop: 
,
subtype: S 
T,
so_lambda: 
x.t[x],
uall: [x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
and: P 
Q,
iff: P 
Q
Lemmas :
event_ordering_wf,
es-E_wf,
es-le_wf,
es-le-before_wf2,
es-ble_wf,
filter_type,
subtype_rel_self,
subtype_rel_sets,
assert_wf,
subtype_rel_list,
assert-es-ble
\mforall{}es:EO. \mforall{}e,b:E. (b \mleq{}loc e {}\mRightarrow{} (\mleq{}loc(b) = filter(\mlambda{}a.a \mleq{}loc b;\mleq{}loc(e))))
Date html generated:
2012_01_23-PM-12_10_51
Last ObjectModification:
2011_12_13-AM-11_07_47
Home
Index