{ 
es:EO
[P:E 
]
((e:E. Dec(P[e]))
(v:E
(P[v]
(e':E
((e' < v)
P[e']
(
e':E. es-p-immediate-pred(es;
e.P[e])[v;e'])))))) }
{ Proof }
Definitions occuring in Statement :
es-p-immediate-pred: es-p-immediate-pred(es;P),
es-causl: (e < e'),
es-E: E,
event_ordering: EO,
decidable: Dec(P),
uall: [x:A]. B[x],
prop: ,
so_apply: x[s1;s2],
so_apply: x[s],
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
lambda: x.A[x],
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,
exists: x:A. B[x],
and: P 
Q,
iff: P 
Q,
rev_implies: P Q,
so_lambda: 
x.t[x],
assert: 
b,
isl: isl(x),
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
true: True,
false: False,
length: ||as||,
not: 
A,
ycomb: Y,
l_exists: (xL. P[x]),
l_all: (xL.P[x]),
cand: A c B,
or: P 
Q,
select: l[i],
le_int: i 
z j,
bnot: 
b,
lt_int: i <z j,
top: Top,
subtype: S 
T,
guard: {T},
so_apply: x[s1;s2],
es-p-immediate-pred: es-p-immediate-pred(es;P),
decidable: Dec(P),
uimplies: b supposing a,
uiff: uiff(P;Q),
l_member: (x l),
nat: 
,
sq_type: SQType(T)
Lemmas :
es-causl_wf,
es-E_wf,
decidable_wf,
event_ordering_wf,
filter_wf,
es-pred-list_wf,
isl_wf,
not_wf,
iff_wf,
l_member_wf,
assert_wf,
all_functionality_wrt_iff,
iff_functionality_wrt_iff,
iff_transitivity,
member_filter,
and_functionality_wrt_iff,
member-es-pred-list,
true_wf,
false_wf,
pos_length2,
member_null,
length_wf1,
cons_member,
decidable__equal_int,
subtype_base_sq,
int_subtype_base,
l_all_wf2,
es-causl_irreflexivity,
non_neg_length,
length_wf_nat,
top_wf,
length_cons,
l_exists_cons,
decidable__es-causl,
l_exists_wf,
l_all_cons,
es-causl_transitivity2,
es-causle_weakening,
es-p-immediate-pred_wf
\mforall{}es:EO
\mforall{}[P:E {}\mrightarrow{} \mBbbP{}]
((\mforall{}e:E. Dec(P[e]))
{}\mRightarrow{} (\mforall{}v:E
(P[v] {}\mRightarrow{} (\mforall{}e':E. ((e' < v) {}\mRightarrow{} P[e'] {}\mRightarrow{} (\mexists{}e':E. es-p-immediate-pred(es;\mlambda{}e.P[e])[v;e']))))))
Date html generated:
2011_08_16-AM-11_13_54
Last ObjectModification:
2011_06_20-AM-00_21_13
Home
Index