{ 
[es:EO]. [e,e':E].
(e, e') ~ [] supposing (
first(e')) 
((
first(e')) 
pred(e') 
loc e ) }
{ Proof }
Definitions occuring in Statement :
es-open-interval: (e, e'),
es-le: e loc e' ,
es-pred: pred(e),
es-first: first(e),
es-E: E,
event_ordering: EO,
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
not: A,
or: P Q,
and: P Q,
nil: [],
sqequal: s ~ t
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
or: P Q,
and: P Q,
not: A,
es-open-interval: (e, e'),
member: t 
T,
l_all: (xL.P[x]),
so_apply: x[s],
all: x:A. B[x],
implies: P 
Q,
prop: 
,
cand: A c B,
iff: P 
Q,
false: False
Lemmas :
equal-nil-sq-nil,
es-E_wf,
es-open-interval_wf,
filter_is_nil,
es-bless_wf,
es-before_wf,
assert-es-bless,
assert_wf,
l_member_wf,
es-first_wf,
not_wf,
es-le_wf,
es-pred_wf,
event_ordering_wf,
member-es-before,
btrue_neq_bfalse,
assert_elim,
es-locl-first,
es-locl-iff,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity,
es-le_weakening
\mforall{}[es:EO]. \mforall{}[e,e':E]. (e, e') \msim{} [] supposing (\muparrow{}first(e')) \mvee{} ((\mneg{}\muparrow{}first(e')) \mwedge{} pred(e') \mleq{}loc e )
Date html generated:
2011_08_16-AM-10_39_19
Last ObjectModification:
2011_06_18-AM-09_18_10
Home
Index