{ 
es:EO. e,e':E. (es-init(es;e) 
loc e' 
loc(e') = loc(e)) }
{ Proof }
Definitions occuring in Statement :
es-init: es-init(es;e),
es-le: e loc e' ,
es-loc: loc(e),
es-E: E,
event_ordering: EO,
Id: Id,
all: x:A. B[x],
iff: P Q,
equal: s = t
Definitions :
member: t 
T,
equal: s = t,
function: x:A 
B[x],
all: x:A. B[x],
es-le: e loc e' ,
event_ordering: EO,
es-E: E,
es-loc: loc(e),
Id: Id,
universe: Type,
prop: 
,
es-init: es-init(es;e),
subtype_rel: A 
r B,
strong-subtype: strong-subtype(A;B),
apply: f a,
record-select: r.x,
dep-isect: Error :dep-isect,
infix_ap: x f y,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
record+: record+,
implies: P Q,
limited-type: LimitedType,
sqequal: s ~ t,
es-pred: pred(e),
union: left + right,
or: P 
Q,
rev_implies: P Q,
product: x:A 
B[x],
and: P 
Q,
iff: P Q,
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
tactic: Error :tactic,
true: True
Lemmas :
es-init-le,
es-le-loc,
es-loc-init,
es-init_wf,
Id_wf,
es-loc_wf,
es-E_wf,
event_ordering_wf,
es-init-eq,
es-le_wf
\mforall{}es:EO. \mforall{}e,e':E. (es-init(es;e) \mleq{}loc e' \mLeftarrow{}{}\mRightarrow{} loc(e') = loc(e))
Date html generated:
2010_08_27-AM-09_27_27
Last ObjectModification:
2010_06_03-PM-12_39_10
Home
Index