{ 
es:EO. e,e':E. (
e <loc e' 
(e <loc e')) }
{ Proof }
Definitions occuring in Statement :
es-bless: e <loc e',
es-locl: (e <loc e'),
es-E: E,
event_ordering: EO,
assert: b,
all: x:A. B[x],
iff: P Q
Definitions :
decidable: Dec(P),
limited-type: LimitedType,
uiff: uiff(P;Q),
Id: Id,
eq_lnk: a = b,
es-eq-E: e = e',
bnot: 
b,
bimplies: p q,
band: p 
q,
bor: p 
q,
not: A,
es-causl: (e < e'),
apply: f a,
set: {x:A| B[x]} ,
top: Top,
es-pred-list: es-pred-list(es;e),
es-loc: loc(e),
eq_id: a = b,
lambda: 
x.A[x],
filter: filter(P;l),
es-eq: es-eq(es),
deq-member: deq-member(eq;x;L),
universe: Type,
prop: 
,
rev_implies: P Q,
l_member: (x 
l),
implies: P Q,
es-locl: (e <loc e'),
assert: b,
es-bless: e <loc e',
iff: P Q,
and: P Q,
product: x:A 
B[x],
event_ordering: EO,
es-E: E,
all: x:A. B[x],
function: x:A 
B[x],
uall: [x:A]. B[x],
isect: 
x:A. B[x],
equal: s = t,
member: t T,
Auto: Error :Auto,
CollapseTHENA: Error :CollapseTHENA,
CollapseTHEN: Error :CollapseTHEN,
RepUR: Error :RepUR,
tactic: Error :tactic,
MaAuto: Error :MaAuto
Lemmas :
assert_wf,
rev_implies_wf,
iff_wf,
member-es-pred-list,
and_functionality_wrt_iff,
l_member_wf,
es-E_wf,
es-causl_wf,
iff_functionality_wrt_iff,
es-locl_wf,
member_filter,
es-loc_wf,
eq_id_wf,
es-pred-list_wf,
filter_wf,
es-eq_wf,
deq-member_wf,
assert-deq-member,
event_ordering_wf,
Id_wf,
iff_weakening_uiff,
and_functionality_wrt_uiff3,
assert-eq-id,
decidable_wf,
decidable__es-causl
\mforall{}es:EO. \mforall{}e,e':E. (\muparrow{}e <loc e' \mLeftarrow{}{}\mRightarrow{} (e <loc e'))
Date html generated:
2011_08_16-AM-10_33_56
Last ObjectModification:
2010_11_23-PM-04_20_36
Home
Index