{ 
es:EO. as,bs:E List.
(loc-ordered(es;as)
loc-ordered(es;bs)
(as = bs 
e:E. ((e 
as) (e bs)))) }
{ Proof }
Definitions occuring in Statement :
loc-ordered: loc-ordered(es;L),
es-E: E,
event_ordering: EO,
all: x:A. B[x],
iff: P Q,
implies: P Q,
list: type List,
equal: s = t,
l_member: (x l)
Definitions :
all: x:A. B[x],
implies: P Q,
member: t T,
so_lambda: 
x y.t[x; y],
not: 
A,
loc-ordered: loc-ordered(es;L),
so_apply: x[s1;s2],
and: P 
Q,
trans: Trans(T;x,y.E[x; y]),
false: False,
prop: 
Lemmas :
l-ordered-equality,
es-E_wf,
es-locl_wf,
es-locl-antireflexive,
event_ordering_wf,
pes-axioms
\mforall{}es:EO. \mforall{}as,bs:E List.
(loc-ordered(es;as) {}\mRightarrow{} loc-ordered(es;bs) {}\mRightarrow{} (as = bs \mLeftarrow{}{}\mRightarrow{} \mforall{}e:E. ((e \mmember{} as) \mLeftarrow{}{}\mRightarrow{} (e \mmember{} bs))))
Date html generated:
2011_08_16-AM-10_26_52
Last ObjectModification:
2010_09_24-PM-09_14_49
Home
Index