{ 
es:EO. s:FSet{E}. i:Id. (i 
locs(s) 
e:E. ((loc(e) = i) 
e s)) }
{ Proof }
Definitions occuring in Statement :
es-fset-loc: i locs(s),
es-loc: loc(e),
es-eq: es-eq(es),
es-E: E,
event_ordering: EO,
Id: Id,
all: x:A. B[x],
exists: x:A. B[x],
iff: P Q,
and: P Q,
equal: s = t,
fset: FSet{s},
fset-member: a s
Definitions :
all: x:A. B[x],
iff: P Q,
es-fset-loc: i locs(s),
exists: x:A. B[x],
and: P Q,
member: t T,
implies: P Q,
cand: A c B,
rev_implies: P Q,
prop: 
,
subtype: S 
T,
assert: 
b,
null: null(as),
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
or: P 
Q,
not: 
A,
bfalse: ff,
false: False,
guard: {T}
Lemmas :
es-fset-at-property,
es-fset-at_wf,
not_wf,
assert_wf,
null_wf3,
top_wf,
es-E_wf,
Id_wf,
es-loc_wf,
fset-member_wf,
es-eq_wf,
iff_wf,
l_member_wf,
no_repeats_wf,
sorted-by_wf,
es-le_wf,
fset_wf,
event_ordering_wf,
cons_member,
false_wf,
true_wf,
nil_member
\mforall{}es:EO. \mforall{}s:FSet\{E\}. \mforall{}i:Id. (i \mmember{} locs(s) \mLeftarrow{}{}\mRightarrow{} \mexists{}e:E. ((loc(e) = i) \mwedge{} e \mmember{} s))
Date html generated:
2011_08_16-AM-11_05_47
Last ObjectModification:
2010_09_24-PM-08_51_40
Home
Index