{ 
[es:EO]. [i:Id]. [e:E].
uiff(failure-known(es;e;i);x@i.e c
x 
(
es-effective(es;x))) }
{ Proof }
Definitions occuring in Statement :
es-effective: es-effective(es;e),
failure-known: failure-known(es;e;i),
es-causle: e c e',
alle-at: e@i.P[e],
es-E: E,
event_ordering: EO,
Id: Id,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
not: A,
implies: P Q
Definitions :
uall: [x:A]. B[x],
uiff: uiff(P;Q),
failure-known: failure-known(es;e;i),
alle-at: e@i.P[e],
implies: P Q,
not: A,
es-effective: es-effective(es;e),
all: x:A. B[x],
exists: 
x:A. B[x],
and: P 
Q,
member: t 
T,
uimplies: b supposing a,
prop: 
,
false: False,
cand: A c B,
Id: Id,
sq_type: SQType(T),
guard: {T}
Lemmas :
es-causle_wf,
Id_wf,
es-loc_wf,
es-E_wf,
not_wf,
event_ordering_wf,
subtype_base_sq,
atom2_subtype_base
\mforall{}[es:EO]. \mforall{}[i:Id]. \mforall{}[e:E]. uiff(failure-known(es;e;i);\mforall{}x@i.e c\mleq{} x {}\mRightarrow{} (\mneg{}es-effective(es;x)))
Date html generated:
2011_08_16-AM-11_10_25
Last ObjectModification:
2011_06_18-AM-09_42_36
Home
Index