{ 
es:EO
[P:E 
]
e:E
((e':E. (e' c
e 
Dec(P[e'])))
((e':E. (e' c e (
P[e'])))
(
m:E
(m c e 
P[m] (x:E. (((m < x) x c e) (P[x]))))))) }
{ Proof }
Definitions occuring in Statement :
es-causle: e c e',
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
decidable: Dec(P),
uall: [x:A]. B[x],
prop: ,
so_apply: x[s],
all: x:A. B[x],
exists: x:A. B[x],
not: A,
implies: P Q,
or: P Q,
and: P Q,
function: x:A B[x]
Definitions :
all: x:A. B[x],
uall: [x:A]. B[x],
prop: ,
implies: P Q,
so_apply: x[s],
member: t 
T,
so_lambda: 
x.t[x],
or: P Q,
guard: {T},
and: P Q,
cand: A c B,
exists: x:A. B[x],
le: A B,
not: A,
false: False,
uimplies: b supposing a,
nat: 
,
strongwellfounded: SWellFounded(R[x; y]),
decidable: Dec(P),
es-causle: e c e',
sq_type: SQType(T)
Lemmas :
es-E_wf,
es-causle_wf,
decidable_wf,
event_ordering_wf,
es-causl-swellfnd,
decidable__existse-causle,
not_wf,
nat_wf,
decidable__cand,
decidable__equal_nat,
max-of-intset,
le_wf,
es-causl_wf,
subtype_base_sq,
set_subtype_base,
int_subtype_base
\mforall{}es:EO
\mforall{}[P:E {}\mrightarrow{} \mBbbP{}]
\mforall{}e:E
((\mforall{}e':E. (e' c\mleq{} e {}\mRightarrow{} Dec(P[e'])))
{}\mRightarrow{} ((\mforall{}e':E. (e' c\mleq{} e {}\mRightarrow{} (\mneg{}P[e'])))
\mvee{} (\mexists{}m:E. (m c\mleq{} e \mwedge{} P[m] \mwedge{} (\mforall{}x:E. (((m < x) \mwedge{} x c\mleq{} e) {}\mRightarrow{} (\mneg{}P[x])))))))
Date html generated:
2011_08_16-AM-11_20_01
Last ObjectModification:
2011_06_20-AM-00_24_56
Home
Index