{ 
es:EO. as:E List.
(loc-ordered(es;as)
(P:{e:E| (e 
as)} 
. loc-ordered(es;filter(P;as)))) }
{ Proof }
Definitions occuring in Statement :
loc-ordered: loc-ordered(es;L),
es-E: E,
event_ordering: EO,
bool: ,
all: x:A. B[x],
implies: P Q,
set: {x:A| B[x]} ,
function: x:A B[x],
list: type List,
filter: filter(P;l),
l_member: (x l)
Definitions :
all: x:A. B[x],
implies: P Q,
loc-ordered: loc-ordered(es;L),
member: t T,
l-ordered: l-ordered(T;x,y.R[x; y];L),
prop: 
,
iff: P 
Q,
and: P 
Q
Lemmas :
list-subtype,
es-E_wf,
l_member_wf,
bool_wf,
loc-ordered_wf,
event_ordering_wf,
l_before-filter,
l_before_wf,
filter_wf2,
subtype_rel_list
\mforall{}es:EO. \mforall{}as:E List. (loc-ordered(es;as) {}\mRightarrow{} (\mforall{}P:\{e:E| (e \mmember{} as)\} {}\mrightarrow{} \mBbbB{}. loc-ordered(es;filter(P;as)))\000C)
Date html generated:
2011_08_16-AM-10_26_56
Last ObjectModification:
2010_09_24-PM-09_14_45
Home
Index