{ 
es:EO. e:E.
[P:{a:E| loc(a) = loc(e)} 
]
((a:{a:E| loc(a) = loc(e)} . Dec(P[a]))
(e'
e.P[e'] 
P[e]
e'e.(
(P[e'] P[e])) 
e''
(e',e].P[e''] P[e])) }
{ Proof }
Definitions occuring in Statement :
alle-between3: e(e1,e2].P[e],
alle-le: ee'.P[e],
existse-le: ee'.P[e],
es-loc: loc(e),
es-E: E,
event_ordering: EO,
Id: Id,
decidable: Dec(P),
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
all: x:A. B[x],
iff: P Q,
not: A,
implies: P Q,
or: P Q,
and: P Q,
set: {x:A| B[x]} ,
function: x:A B[x],
equal: s = t
Definitions :
all: x:A. B[x],
uall: [x:A]. B[x],
prop: ,
implies: P Q,
so_apply: x[s],
member: t T,
decidable: Dec(P),
exists: x:A. B[x],
or: P Q,
iff: P Q,
btrue: tt,
bfalse: ff,
and: P Q,
rev_implies: P Q,
false: False,
assert: 
b,
ifthenelse: if b then t else f fi ,
true: True,
alle-le: ee'.P[e],
existse-le: ee'.P[e],
alle-between3: e(e1,e2].P[e],
cand: A c B,
guard: {T},
not: A,
uimplies: b supposing a,
es-locl: (e <loc e')
Lemmas :
Id_wf,
es-loc_wf,
decidable_wf,
es-E_wf,
event_ordering_wf,
not_wf,
btrue_wf,
bfalse_wf,
iff_wf,
bool_wf,
btrue_neq_bfalse,
iff_imp_equal_bool,
false_wf,
true_wf,
last-transition,
es-le_wf,
es-locl_wf,
es-le-loc
\mforall{}es:EO. \mforall{}e:E.
\mforall{}[P:\{a:E| loc(a) = loc(e)\} {}\mrightarrow{} \mBbbP{}]
((\mforall{}a:\{a:E| loc(a) = loc(e)\} . Dec(P[a]))
{}\mRightarrow{} (\mforall{}e'\mleq{}e.P[e'] \mLeftarrow{}{}\mRightarrow{} P[e] \mvee{} \mexists{}e'\mleq{}e.(\mneg{}(P[e'] \mLeftarrow{}{}\mRightarrow{} P[e])) \mwedge{} \mforall{}e''\mmember{}(e',e].P[e''] \mLeftarrow{}{}\mRightarrow{} P[e]))
Date html generated:
2011_08_16-AM-10_53_24
Last ObjectModification:
2011_06_18-AM-09_26_45
Home
Index