{ 
es:EO. e:E. P:Top. e
[e,e).P[e] }
{ Proof }
Definitions occuring in Statement :
alle-between1: e[e1,e2).P[e],
es-E: E,
event_ordering: EO,
top: Top,
so_apply: x[s],
all: x:A. B[x]
Definitions :
all: x:A. B[x],
alle-between1: e[e1,e2).P[e],
implies: P 
Q,
member: t T,
not: 
A,
false: False,
prop: 
Lemmas :
es-locl-antireflexive,
es-locl_wf,
es-le_wf,
top_wf,
es-E_wf,
event_ordering_wf,
es-le-trans2
\mforall{}es:EO. \mforall{}e:E. \mforall{}P:Top. \mforall{}e\mmember{}[e,e).P[e]
Date html generated:
2011_08_16-AM-10_46_30
Last ObjectModification:
2010_09_24-PM-09_02_44
Home
Index